[STATEMENT]
lemma all_val:
  assumes "\<forall> (v::var \<Rightarrow> 'a::lrv). \<exists> v'. (\<forall> x \<in> vars p. v' x = v x) \<and> (p \<lbrace>v'\<rbrace> = 0)"
  shows "p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = 0
[PROOF STEP]
proof (subst zero_coeff_zero, rule allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. coeff p v = 0
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. coeff p v = 0
[PROOF STEP]
show "coeff p x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff p x = 0
[PROOF STEP]
proof (cases "x \<in> vars p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
 2. x \<notin> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> vars p

goal (2 subgoals):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
 2. x \<notin> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> vars p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> vars p

goal (1 subgoal):
 1. coeff p x = 0
[PROOF STEP]
using coeff_zero[of p x]
[PROOF STATE]
proof (prove)
using this:
x \<notin> vars p
(coeff p x \<noteq> 0) = (x \<in> vars p)

goal (1 subgoal):
 1. coeff p x = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coeff p x = 0

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> vars p

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
have "(0::'a::lrv) \<noteq> (1::'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<noteq> (1::'a)
[PROOF STEP]
using zero_neq_one
[PROOF STATE]
proof (prove)
using this:
(0::?'a) \<noteq> (1::?'a)

goal (1 subgoal):
 1. (0::'a) \<noteq> (1::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<noteq> (1::'a)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
let ?v = "\<lambda> x'. if x = x' then 1 else 0::'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
obtain v' where "\<forall> x \<in> vars p. v' x = ?v x" "p \<lbrace>v'\<rbrace> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v'. \<lbrakk>\<forall>xa\<in>vars p. v' xa = (if x = xa then 1::'a else (0::'a)); p \<lbrace> v' \<rbrace> = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>v. \<exists>v'. (\<forall>x\<in>vars p. v' x = v x) \<and> p \<lbrace> v' \<rbrace> = (0::'a)

goal (1 subgoal):
 1. (\<And>v'. \<lbrakk>\<forall>xa\<in>vars p. v' xa = (if x = xa then 1::'a else (0::'a)); p \<lbrace> v' \<rbrace> = (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (erule_tac x="?v" in allE) auto
[PROOF STATE]
proof (state)
this:
\<forall>xa\<in>vars p. v' xa = (if x = xa then 1::'a else (0::'a))
p \<lbrace> v' \<rbrace> = (0::'a)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>xa\<in>vars p. v' xa = (if x = xa then 1::'a else (0::'a))
p \<lbrace> v' \<rbrace> = (0::'a)
[PROOF STEP]
have "\<forall> x' \<in> vars p. v' x' = (if x = x' then 1 else 0)" "p \<lbrace>v'\<rbrace> = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>xa\<in>vars p. v' xa = (if x = xa then 1::'a else (0::'a))
p \<lbrace> v' \<rbrace> = (0::'a)

goal (1 subgoal):
 1. \<forall>x'\<in>vars p. v' x' = (if x = x' then 1::'a else (0::'a)) &&& p \<lbrace> v' \<rbrace> = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x'\<in>vars p. v' x' = (if x = x' then 1::'a else (0::'a))
p \<lbrace> v' \<rbrace> = (0::'a)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
let ?fp = "Rep_linear_poly p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
have "{x. ?fp x \<noteq> 0 \<and> v' x \<noteq> (0 :: 'a)} = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. Rep_linear_poly p x \<noteq> 0 \<and> v' x \<noteq> (0::'a)} = {x}
[PROOF STEP]
using \<open>x \<in> vars p\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> vars p

goal (1 subgoal):
 1. {x. Rep_linear_poly p x \<noteq> 0 \<and> v' x \<noteq> (0::'a)} = {x}
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
x \<in> map_fun Rep_linear_poly id fun_vars p

goal (1 subgoal):
 1. {x. Rep_linear_poly p x \<noteq> 0 \<and> v' x \<noteq> (0::'a)} = {x}
[PROOF STEP]
proof (safe, simp_all)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>Rep_linear_poly p x \<noteq> 0; Rep_linear_poly p xa \<noteq> 0; v' xa \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> xa = x
 2. \<lbrakk>Rep_linear_poly p x \<noteq> 0; v' x = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix x'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>Rep_linear_poly p x \<noteq> 0; Rep_linear_poly p xa \<noteq> 0; v' xa \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> xa = x
 2. \<lbrakk>Rep_linear_poly p x \<noteq> 0; v' x = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "v' x' \<noteq> 0" "Rep_linear_poly p x' \<noteq> 0"
[PROOF STATE]
proof (state)
this:
v' x' \<noteq> (0::'a)
Rep_linear_poly p x' \<noteq> 0

goal (2 subgoals):
 1. \<And>xa. \<lbrakk>Rep_linear_poly p x \<noteq> 0; Rep_linear_poly p xa \<noteq> 0; v' xa \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> xa = x
 2. \<lbrakk>Rep_linear_poly p x \<noteq> 0; v' x = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v' x' \<noteq> (0::'a)
Rep_linear_poly p x' \<noteq> 0
[PROOF STEP]
show "x' = x"
[PROOF STATE]
proof (prove)
using this:
v' x' \<noteq> (0::'a)
Rep_linear_poly p x' \<noteq> 0

goal (1 subgoal):
 1. x' = x
[PROOF STEP]
using \<open>\<forall> x' \<in> vars p. v' x' = (if x = x' then 1 else 0)\<close>
[PROOF STATE]
proof (prove)
using this:
v' x' \<noteq> (0::'a)
Rep_linear_poly p x' \<noteq> 0
\<forall>x'\<in>vars p. v' x' = (if x = x' then 1::'a else (0::'a))

goal (1 subgoal):
 1. x' = x
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
v' x' \<noteq> (0::'a)
Rep_linear_poly p x' \<noteq> 0
\<forall>x'\<in>map_fun Rep_linear_poly id fun_vars p. v' x' = (if x = x' then 1::'a else (0::'a))

goal (1 subgoal):
 1. x' = x
[PROOF STEP]
by (erule_tac x="x'" in ballE) (simp_all split: if_splits)
[PROOF STATE]
proof (state)
this:
x' = x

goal (1 subgoal):
 1. \<lbrakk>Rep_linear_poly p x \<noteq> 0; v' x = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Rep_linear_poly p x \<noteq> 0; v' x = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "v' x = 0" "Rep_linear_poly p x \<noteq> 0"
[PROOF STATE]
proof (state)
this:
v' x = (0::'a)
Rep_linear_poly p x \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>Rep_linear_poly p x \<noteq> 0; v' x = (0::'a)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v' x = (0::'a)
Rep_linear_poly p x \<noteq> 0
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
v' x = (0::'a)
Rep_linear_poly p x \<noteq> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>\<forall> x' \<in> vars p. v' x' = (if x = x' then 1 else 0)\<close>
[PROOF STATE]
proof (prove)
using this:
v' x = (0::'a)
Rep_linear_poly p x \<noteq> 0
\<forall>x'\<in>vars p. v' x' = (if x = x' then 1::'a else (0::'a))

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>0 \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
v' x = (0::'a)
Rep_linear_poly p x \<noteq> 0
\<forall>x'\<in>vars p. v' x' = (if x = x' then 1::'a else (0::'a))
(0::'a) \<noteq> (1::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
v' x = (0::'a)
Rep_linear_poly p x \<noteq> 0
\<forall>x'\<in>map_fun Rep_linear_poly id fun_vars p. v' x' = (if x = x' then 1::'a else (0::'a))
(0::'a) \<noteq> (1::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{x. Rep_linear_poly p x \<noteq> 0 \<and> v' x \<noteq> (0::'a)} = {x}

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
have "p \<lbrace>v'\<rbrace> = (\<Sum>x\<in>{v. ?fp v \<noteq> 0}. ?fp x *R v' x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<lbrace> v' \<rbrace> = (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0}. Rep_linear_poly p x *R v' x)
[PROOF STEP]
unfolding valuate_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun Rep_linear_poly id fun_valuate p v' = (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0}. Rep_linear_poly p x *R v' x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<lbrace> v' \<rbrace> = (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0}. Rep_linear_poly p x *R v' x)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p \<lbrace> v' \<rbrace> = (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0}. Rep_linear_poly p x *R v' x)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
have "... = (\<Sum>x\<in>{v. ?fp v \<noteq> 0 \<and> v' v \<noteq> 0}. ?fp x *R v' x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0}. Rep_linear_poly p x *R v' x) = (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)}. Rep_linear_poly p x *R v' x)
[PROOF STEP]
apply (rule sum.mono_neutral_left[THEN sym])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {v. Rep_linear_poly p v \<noteq> 0}
 2. {v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)} \<subseteq> {v. Rep_linear_poly p v \<noteq> 0}
 3. \<forall>i\<in>{v. Rep_linear_poly p v \<noteq> 0} - {v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)}. Rep_linear_poly p i *R v' i = (0::'a)
[PROOF STEP]
using Rep_linear_poly[of p]
[PROOF STATE]
proof (prove)
using this:
Rep_linear_poly p \<in> {c. Abstract_Linear_Poly.inv c}

goal (3 subgoals):
 1. finite {v. Rep_linear_poly p v \<noteq> 0}
 2. {v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)} \<subseteq> {v. Rep_linear_poly p v \<noteq> 0}
 3. \<forall>i\<in>{v. Rep_linear_poly p v \<noteq> 0} - {v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)}. Rep_linear_poly p i *R v' i = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0}. Rep_linear_poly p x *R v' x) = (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)}. Rep_linear_poly p x *R v' x)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0}. Rep_linear_poly p x *R v' x) = (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)}. Rep_linear_poly p x *R v' x)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
have "... = ?fp x *R v' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)}. Rep_linear_poly p x *R v' x) = Rep_linear_poly p x *R v' x
[PROOF STEP]
using \<open>{x. ?fp x \<noteq> 0 \<and> v' x \<noteq> (0 :: 'a)} = {x}\<close>
[PROOF STATE]
proof (prove)
using this:
{x. Rep_linear_poly p x \<noteq> 0 \<and> v' x \<noteq> (0::'a)} = {x}

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)}. Rep_linear_poly p x *R v' x) = Rep_linear_poly p x *R v' x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)}. Rep_linear_poly p x *R v' x) = Rep_linear_poly p x *R v' x

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. Rep_linear_poly p v \<noteq> 0 \<and> v' v \<noteq> (0::'a)}. Rep_linear_poly p x *R v' x) = Rep_linear_poly p x *R v' x

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
have "... = ?fp x *R 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_linear_poly p x *R v' x = Rep_linear_poly p x *R (1::'a)
[PROOF STEP]
using \<open>x \<in> vars p\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> vars p

goal (1 subgoal):
 1. Rep_linear_poly p x *R v' x = Rep_linear_poly p x *R (1::'a)
[PROOF STEP]
using \<open>\<forall> x' \<in> vars p. v' x' = (if x = x' then 1 else 0)\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> vars p
\<forall>x'\<in>vars p. v' x' = (if x = x' then 1::'a else (0::'a))

goal (1 subgoal):
 1. Rep_linear_poly p x *R v' x = Rep_linear_poly p x *R (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rep_linear_poly p x *R v' x = Rep_linear_poly p x *R (1::'a)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<lbrace> v' \<rbrace> = Rep_linear_poly p x *R v' x
Rep_linear_poly p x *R v' x = Rep_linear_poly p x *R (1::'a)
[PROOF STEP]
have "p \<lbrace>v'\<rbrace> = ?fp x *R 1"
[PROOF STATE]
proof (prove)
using this:
p \<lbrace> v' \<rbrace> = Rep_linear_poly p x *R v' x
Rep_linear_poly p x *R v' x = Rep_linear_poly p x *R (1::'a)

goal (1 subgoal):
 1. p \<lbrace> v' \<rbrace> = Rep_linear_poly p x *R (1::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p \<lbrace> v' \<rbrace> = Rep_linear_poly p x *R (1::'a)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<lbrace> v' \<rbrace> = Rep_linear_poly p x *R (1::'a)
[PROOF STEP]
have "coeff p x *R (1::'a)= 0"
[PROOF STATE]
proof (prove)
using this:
p \<lbrace> v' \<rbrace> = Rep_linear_poly p x *R (1::'a)

goal (1 subgoal):
 1. coeff p x *R (1::'a) = (0::'a)
[PROOF STEP]
using \<open>p \<lbrace>v'\<rbrace> = 0\<close>
[PROOF STATE]
proof (prove)
using this:
p \<lbrace> v' \<rbrace> = Rep_linear_poly p x *R (1::'a)
p \<lbrace> v' \<rbrace> = (0::'a)

goal (1 subgoal):
 1. coeff p x *R (1::'a) = (0::'a)
[PROOF STEP]
unfolding coeff_def
[PROOF STATE]
proof (prove)
using this:
p \<lbrace> v' \<rbrace> = Rep_linear_poly p x *R (1::'a)
p \<lbrace> v' \<rbrace> = (0::'a)

goal (1 subgoal):
 1. map_fun Rep_linear_poly id fun_coeff p x *R (1::'a) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coeff p x *R (1::'a) = (0::'a)

goal (1 subgoal):
 1. x \<in> vars p \<Longrightarrow> coeff p x = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
coeff p x *R (1::'a) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
coeff p x *R (1::'a) = (0::'a)

goal (1 subgoal):
 1. coeff p x = 0
[PROOF STEP]
using rational_vector.scale_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
coeff p x *R (1::'a) = (0::'a)
(?a *R ?x = (0::?'a)) = (?a = 0 \<or> ?x = (0::?'a))

goal (1 subgoal):
 1. coeff p x = 0
[PROOF STEP]
using \<open>0 \<noteq> 1\<close>
[PROOF STATE]
proof (prove)
using this:
coeff p x *R (1::'a) = (0::'a)
(?a *R ?x = (0::?'a)) = (?a = 0 \<or> ?x = (0::?'a))
(0::'a) \<noteq> (1::'a)

goal (1 subgoal):
 1. coeff p x = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
coeff p x = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
coeff p x = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valuate_lp_monom: "((lp_monom c x) \<lbrace>v\<rbrace>) = c * (v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lp_monom c x \<lbrace> v \<rbrace> = c * v x
[PROOF STEP]
proof (transfer, simp, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>c x v. (\<Sum>x\<in>{v. x = v \<and> (x = v \<longrightarrow> c \<noteq> 0)}. c * v x) = c * v x
[PROOF STEP]
case (1 c x v)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>c x v. (\<Sum>x\<in>{v. x = v \<and> (x = v \<longrightarrow> c \<noteq> 0)}. c * v x) = c * v x
[PROOF STEP]
have id: "{v. x = v \<and> (x = v \<longrightarrow> c \<noteq> 0)} = (if c = 0 then {} else {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v. x = v \<and> (x = v \<longrightarrow> c \<noteq> 0)} = (if c = 0 then {} else {x})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v. x = v \<and> (x = v \<longrightarrow> c \<noteq> 0)} = (if c = 0 then {} else {x})

goal (1 subgoal):
 1. \<And>c x v. (\<Sum>x\<in>{v. x = v \<and> (x = v \<longrightarrow> c \<noteq> 0)}. c * v x) = c * v x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. x = v \<and> (x = v \<longrightarrow> c \<noteq> 0)}. c * v x) = c * v x
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>(if c = 0 then {} else {x}). c * v x) = c * v x
[PROOF STEP]
by (cases "c = 0", auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. x = v \<and> (x = v \<longrightarrow> c \<noteq> 0)}. c * v x) = c * v x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valuate_lp_monom_1[simp]: "((lp_monom 1 x) \<lbrace>v\<rbrace>) = v x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lp_monom 1 x \<lbrace> v \<rbrace> = v x
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma coeff_lp_monom [simp]:
  shows "coeff (lp_monom c v) v' = (if v = v' then c else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (lp_monom c v) v' = (if v = v' then c else 0)
[PROOF STEP]
by (transfer, auto)


[STATEMENT]
lemma vars_uminus [simp]: "vars (-p) = vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (- p) = vars p
[PROOF STEP]
unfolding uminus_linear_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (- 1 *R p) = vars p
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma vars_plus [simp]: "vars (p1 + p2) \<subseteq> vars p1 \<union> vars p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (p1 + p2) \<subseteq> vars p1 \<union> vars p2
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma vars_minus [simp]: "vars (p1 - p2) \<subseteq> vars p1 \<union> vars p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (p1 - p2) \<subseteq> vars p1 \<union> vars p2
[PROOF STEP]
unfolding minus_linear_poly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (p1 + - p2) \<subseteq> vars p1 \<union> vars p2
[PROOF STEP]
using vars_plus[of p1 "-p2"] vars_uminus[of p2]
[PROOF STATE]
proof (prove)
using this:
vars (p1 + - p2) \<subseteq> vars p1 \<union> vars (- p2)
vars (- p2) = vars p2

goal (1 subgoal):
 1. vars (p1 + - p2) \<subseteq> vars p1 \<union> vars p2
[PROOF STEP]
by simp


[STATEMENT]
lemma vars_lp_monom: "vars (lp_monom r x) = (if r = 0 then {} else {x})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (lp_monom r x) = (if r = 0 then {} else {x})
[PROOF STEP]
by (transfer, auto)


[STATEMENT]
lemma vars_scaleRat1: "vars (c *R p) \<subseteq> vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (c *R p) \<subseteq> vars p
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma vars_scaleRat: "c \<noteq> 0 \<Longrightarrow> vars(c *R p) = vars p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<noteq> 0 \<Longrightarrow> vars (c *R p) = vars p
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma vars_Var [simp]: "vars (Var x) = {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (Var x) = {x}
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma coeff_Var1 [simp]: "coeff (Var x) x = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (Var x) x = 1
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma coeff_Var2: "x \<noteq> y \<Longrightarrow> coeff (Var x) y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y \<Longrightarrow> coeff (Var x) y = 0
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma valuate_depend:
  assumes "\<forall> x \<in> vars p. v x = v' x"
  shows "(p \<lbrace>v\<rbrace>) = (p \<lbrace>v'\<rbrace>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<lbrace> v \<rbrace> = p \<lbrace> v' \<rbrace>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>vars p. v x = v' x

goal (1 subgoal):
 1. p \<lbrace> v \<rbrace> = p \<lbrace> v' \<rbrace>
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma valuate_update_x_lemma:
  fixes v1 v2 :: "'a::rational_vector valuation"
  assumes
    "\<forall>y. f y \<noteq> 0 \<longrightarrow> y \<noteq> x \<longrightarrow> v1 y = v2 y"
    "finite {v. f v \<noteq> 0}"
  shows
    "(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
proof (cases "f x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f x = 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
 2. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f x = 0

goal (2 subgoals):
 1. f x = 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
 2. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f x = 0
[PROOF STEP]
have "\<forall>y. f y \<noteq> 0 \<longrightarrow> v1 y = v2 y"
[PROOF STATE]
proof (prove)
using this:
f x = 0

goal (1 subgoal):
 1. \<forall>y. f y \<noteq> 0 \<longrightarrow> v1 y = v2 y
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
f x = 0
\<forall>y. f y \<noteq> 0 \<longrightarrow> y \<noteq> x \<longrightarrow> v1 y = v2 y

goal (1 subgoal):
 1. \<forall>y. f y \<noteq> 0 \<longrightarrow> v1 y = v2 y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. f y \<noteq> 0 \<longrightarrow> v1 y = v2 y

goal (2 subgoals):
 1. f x = 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
 2. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. f y \<noteq> 0 \<longrightarrow> v1 y = v2 y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>y. f y \<noteq> 0 \<longrightarrow> v1 y = v2 y

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
using \<open>f x = 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>y. f y \<noteq> 0 \<longrightarrow> v1 y = v2 y
f x = 0

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)

goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
f x \<noteq> 0

goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
let ?A = "{v. f v \<noteq> 0}" and ?Ax = "{v. v \<noteq> x \<and> f v \<noteq> 0}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
have "?A = ?Ax \<union> {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {v. f v \<noteq> 0} = {v. v \<noteq> x \<and> f v \<noteq> 0} \<union> {x}
[PROOF STEP]
using \<open>f x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
f x \<noteq> 0

goal (1 subgoal):
 1. {v. f v \<noteq> 0} = {v. v \<noteq> x \<and> f v \<noteq> 0} \<union> {x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{v. f v \<noteq> 0} = {v. v \<noteq> x \<and> f v \<noteq> 0} \<union> {x}

goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{v. f v \<noteq> 0} = {v. v \<noteq> x \<and> f v \<noteq> 0} \<union> {x}
[PROOF STEP]
have "(\<Sum>x\<in>?A. f x *R v1 x) = f x *R v1 x + (\<Sum>x\<in>?Ax. f x *R v1 x)"
    "(\<Sum>x\<in>?A. f x *R v2 x) = f x *R v2 x + (\<Sum>x\<in>?Ax. f x *R v2 x)"
[PROOF STATE]
proof (prove)
using this:
{v. f v \<noteq> 0} = {v. v \<noteq> x \<and> f v \<noteq> 0} \<union> {x}

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) = f x *R v1 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v1 x) &&& (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x) = f x *R v2 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
{v. f v \<noteq> 0} = {v. v \<noteq> x \<and> f v \<noteq> 0} \<union> {x}
finite {v. f v \<noteq> 0}

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) = f x *R v1 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v1 x) &&& (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x) = f x *R v2 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) = f x *R v1 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v1 x)
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x) = f x *R v2 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v2 x)

goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) = f x *R v1 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v1 x)
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x) = f x *R v2 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v2 x)

goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
have "\<forall> y \<in> ?Ax. v1 y = v2 y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. v1 y = v2 y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>y. f y \<noteq> 0 \<longrightarrow> y \<noteq> x \<longrightarrow> v1 y = v2 y
finite {v. f v \<noteq> 0}

goal (1 subgoal):
 1. \<forall>y\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. v1 y = v2 y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. v1 y = v2 y

goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. v1 y = v2 y

goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
have "f x *R v1 x + f x *R (v2 x - v1 x) = f x *R v2 x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x *R v1 x + f x *R (v2 x - v1 x) = f x *R v2 x
[PROOF STEP]
by (subst rational_vector.scale_right_diff_distrib) auto
[PROOF STATE]
proof (state)
this:
f x *R v1 x + f x *R (v2 x - v1 x) = f x *R v2 x

goal (1 subgoal):
 1. f x \<noteq> 0 \<Longrightarrow> (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) = f x *R v1 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v1 x)
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x) = f x *R v2 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v2 x)
\<forall>y\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. v1 y = v2 y
f x *R v1 x + f x *R (v2 x - v1 x) = f x *R v2 x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) = f x *R v1 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v1 x)
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x) = f x *R v2 x + (\<Sum>x\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. f x *R v2 x)
\<forall>y\<in>{v. v \<noteq> x \<and> f v \<noteq> 0}. v1 y = v2 y
f x *R v1 x + f x *R (v2 x - v1 x) = f x *R v2 x

goal (1 subgoal):
 1. (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. f v \<noteq> 0}. f x *R v2 x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valuate_update_x:
  fixes v1 v2 :: "'a::rational_vector valuation"
  assumes "\<forall>y \<in> vars lp. y\<noteq>x \<longrightarrow> v1 y = v2 y"
  shows "lp \<lbrace>v1\<rbrace>  + coeff lp x *R (v2 x - v1 x) = (lp \<lbrace>v2\<rbrace>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lp \<lbrace> v1 \<rbrace> + coeff lp x *R (v2 x - v1 x) = lp \<lbrace> v2 \<rbrace>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>vars lp. y \<noteq> x \<longrightarrow> v1 y = v2 y

goal (1 subgoal):
 1. lp \<lbrace> v1 \<rbrace> + coeff lp x *R (v2 x - v1 x) = lp \<lbrace> v2 \<rbrace>
[PROOF STEP]
unfolding valuate_def vars_def coeff_def
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>map_fun Rep_linear_poly id fun_vars lp. y \<noteq> x \<longrightarrow> v1 y = v2 y

goal (1 subgoal):
 1. map_fun Rep_linear_poly id fun_valuate lp v1 + map_fun Rep_linear_poly id fun_coeff lp x *R (v2 x - v1 x) = map_fun Rep_linear_poly id fun_valuate lp v2
[PROOF STEP]
using valuate_update_x_lemma[of "Rep_linear_poly lp" x v1 v2] Rep_linear_poly
[PROOF STATE]
proof (prove)
using this:
\<forall>y\<in>map_fun Rep_linear_poly id fun_vars lp. y \<noteq> x \<longrightarrow> v1 y = v2 y
\<lbrakk>\<forall>y. Rep_linear_poly lp y \<noteq> 0 \<longrightarrow> y \<noteq> x \<longrightarrow> v1 y = v2 y; finite {v. Rep_linear_poly lp v \<noteq> 0}\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>{v. Rep_linear_poly lp v \<noteq> 0}. Rep_linear_poly lp x *R v1 x) + Rep_linear_poly lp x *R (v2 x - v1 x) = (\<Sum>x\<in>{v. Rep_linear_poly lp v \<noteq> 0}. Rep_linear_poly lp x *R v2 x)
Rep_linear_poly ?x \<in> {c. Abstract_Linear_Poly.inv c}

goal (1 subgoal):
 1. map_fun Rep_linear_poly id fun_valuate lp v1 + map_fun Rep_linear_poly id fun_coeff lp x *R (v2 x - v1 x) = map_fun Rep_linear_poly id fun_valuate lp v2
[PROOF STEP]
by auto


[STATEMENT]
lemma vars_zero: "vars 0 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars 0 = {}
[PROOF STEP]
using zero_coeff_zero coeff_zero
[PROOF STATE]
proof (prove)
using this:
(?p = 0) = (\<forall>v. coeff ?p v = 0)
(coeff ?p ?x \<noteq> 0) = (?x \<in> vars ?p)

goal (1 subgoal):
 1. vars 0 = {}
[PROOF STEP]
by auto


[STATEMENT]
lemma vars_empty_zero: "vars lp = {} \<longleftrightarrow> lp = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vars lp = {}) = (lp = 0)
[PROOF STEP]
using zero_coeff_zero coeff_zero
[PROOF STATE]
proof (prove)
using this:
(?p = 0) = (\<forall>v. coeff ?p v = 0)
(coeff ?p ?x \<noteq> 0) = (?x \<in> vars ?p)

goal (1 subgoal):
 1. (vars lp = {}) = (lp = 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma max_var_max:
  assumes "a \<in> vars lp"
  shows "max_var lp \<ge> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> max_var lp
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> vars lp

goal (1 subgoal):
 1. a \<le> max_var lp
[PROOF STEP]
by (auto simp add: finite_vars max_var_def vars_zero)


[STATEMENT]
lemma max_var_code[code]:
  "max_var lp = (let vl = vars_list lp
                in if vl = [] then 0 else foldl max (hd vl) (tl vl))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
proof (cases "lp = (0::linear_poly)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lp = 0 \<Longrightarrow> max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
 2. lp \<noteq> 0 \<Longrightarrow> max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
lp = 0

goal (2 subgoals):
 1. lp = 0 \<Longrightarrow> max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
 2. lp \<noteq> 0 \<Longrightarrow> max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lp = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lp = 0

goal (1 subgoal):
 1. max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
using set_vars_list[of lp]
[PROOF STATE]
proof (prove)
using this:
lp = 0
set (vars_list lp) = vars lp

goal (1 subgoal):
 1. max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
by (auto simp add: max_var_def vars_zero)
[PROOF STATE]
proof (state)
this:
max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))

goal (1 subgoal):
 1. lp \<noteq> 0 \<Longrightarrow> max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lp \<noteq> 0 \<Longrightarrow> max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
lp \<noteq> 0

goal (1 subgoal):
 1. lp \<noteq> 0 \<Longrightarrow> max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lp \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lp \<noteq> 0

goal (1 subgoal):
 1. max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
using set_vars_list[of lp, THEN sym]
[PROOF STATE]
proof (prove)
using this:
lp \<noteq> 0
vars lp = set (vars_list lp)

goal (1 subgoal):
 1. max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
using vars_empty_zero[of lp]
[PROOF STATE]
proof (prove)
using this:
lp \<noteq> 0
vars lp = set (vars_list lp)
(vars lp = {}) = (lp = 0)

goal (1 subgoal):
 1. max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))
[PROOF STEP]
unfolding max_var_def Let_def
[PROOF STATE]
proof (prove)
using this:
lp \<noteq> 0
vars lp = set (vars_list lp)
(vars lp = {}) = (lp = 0)

goal (1 subgoal):
 1. (if lp = 0 then 0 else Max (vars lp)) = (if vars_list lp = [] then 0 else foldl max (hd (vars_list lp)) (tl (vars_list lp)))
[PROOF STEP]
using Max.set_eq_fold[of "hd (vars_list lp)" "tl (vars_list lp)"]
[PROOF STATE]
proof (prove)
using this:
lp \<noteq> 0
vars lp = set (vars_list lp)
(vars lp = {}) = (lp = 0)
Max (set (hd (vars_list lp) # tl (vars_list lp))) = fold max (tl (vars_list lp)) (hd (vars_list lp))

goal (1 subgoal):
 1. (if lp = 0 then 0 else Max (vars lp)) = (if vars_list lp = [] then 0 else foldl max (hd (vars_list lp)) (tl (vars_list lp)))
[PROOF STEP]
by (cases "vars_list lp", auto simp: foldl_conv_fold intro!: fold_cong)
[PROOF STATE]
proof (state)
this:
max_var lp = (let vl = vars_list lp in if vl = [] then 0 else foldl max (hd vl) (tl vl))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_monom_vars_not_empty:
  "is_monom l \<Longrightarrow> vars l \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_monom l \<Longrightarrow> vars l \<noteq> {}
[PROOF STEP]
by (auto simp add: is_monom_def vars_list_def) (auto simp add: vars_def)


[STATEMENT]
lemma monom_var_in_vars:
  "is_monom l \<Longrightarrow> monom_var l \<in> vars l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_monom l \<Longrightarrow> monom_var l \<in> vars l
[PROOF STEP]
using vars_zero
[PROOF STATE]
proof (prove)
using this:
vars 0 = {}

goal (1 subgoal):
 1. is_monom l \<Longrightarrow> monom_var l \<in> vars l
[PROOF STEP]
by (auto simp add: monom_var_def max_var_def is_monom_vars_not_empty finite_vars is_monom_def)


[STATEMENT]
lemma zero_is_no_monom[simp]: "\<not> is_monom 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_monom 0
[PROOF STEP]
using is_monom_vars_not_empty vars_zero
[PROOF STATE]
proof (prove)
using this:
is_monom ?l \<Longrightarrow> vars ?l \<noteq> {}
vars 0 = {}

goal (1 subgoal):
 1. \<not> is_monom 0
[PROOF STEP]
by blast


[STATEMENT]
lemma is_monom_monom_coeff_not_zero:
  "is_monom l \<Longrightarrow> monom_coeff l \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_monom l \<Longrightarrow> monom_coeff l \<noteq> 0
[PROOF STEP]
by (simp add: coeff_zero monom_var_in_vars monom_coeff_def)


[STATEMENT]
lemma list_two_elements:
  "\<lbrakk>y \<in> set l; x \<in> set l; length l = Suc 0; y \<noteq> x\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<in> set l; x \<in> set l; length l = Suc 0; y \<noteq> x\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (induct l) auto


[STATEMENT]
lemma is_monom_vars_monom_var:
  assumes "is_monom l"
  shows "vars l = {monom_var l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars l = {monom_var l}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vars l = {monom_var l}
[PROOF STEP]
have "\<And>x. \<lbrakk>is_monom l; x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_monom l; x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_monom l; x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_monom l; x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = x
[PROOF STEP]
assume "is_monom l" "x \<in> vars l"
[PROOF STATE]
proof (state)
this:
is_monom l
x \<in> vars l

goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_monom l; x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_monom l
x \<in> vars l
[PROOF STEP]
have "x \<in> set (vars_list l)"
[PROOF STATE]
proof (prove)
using this:
is_monom l
x \<in> vars l

goal (1 subgoal):
 1. x \<in> set (vars_list l)
[PROOF STEP]
using finite_vars
[PROOF STATE]
proof (prove)
using this:
is_monom l
x \<in> vars l
finite (vars ?p)

goal (1 subgoal):
 1. x \<in> set (vars_list l)
[PROOF STEP]
by (auto simp add: vars_list_def vars_def)
[PROOF STATE]
proof (state)
this:
x \<in> set (vars_list l)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_monom l; x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = x
[PROOF STEP]
show "monom_var l = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_var l = x
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. monom_var l \<noteq> x \<Longrightarrow> False
[PROOF STEP]
assume "monom_var l \<noteq> x"
[PROOF STATE]
proof (state)
this:
monom_var l \<noteq> x

goal (1 subgoal):
 1. monom_var l \<noteq> x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
monom_var l \<noteq> x
[PROOF STEP]
have "\<exists>y. monom_var l = y \<and> y \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
monom_var l \<noteq> x

goal (1 subgoal):
 1. \<exists>y. monom_var l = y \<and> y \<noteq> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>y. monom_var l = y \<and> y \<noteq> x

goal (1 subgoal):
 1. monom_var l \<noteq> x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. monom_var l = y \<and> y \<noteq> x
[PROOF STEP]
obtain y where "monom_var l = y" "y \<noteq> x"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. monom_var l = y \<and> y \<noteq> x

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>monom_var l = y; y \<noteq> x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
monom_var l = y
y \<noteq> x

goal (1 subgoal):
 1. monom_var l \<noteq> x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
monom_var l = y
y \<noteq> x
[PROOF STEP]
have "Rep_linear_poly l y \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
monom_var l = y
y \<noteq> x

goal (1 subgoal):
 1. Rep_linear_poly l y \<noteq> 0
[PROOF STEP]
using monom_var_in_vars \<open>is_monom l\<close>
[PROOF STATE]
proof (prove)
using this:
monom_var l = y
y \<noteq> x
is_monom ?l \<Longrightarrow> monom_var ?l \<in> vars ?l
is_monom l

goal (1 subgoal):
 1. Rep_linear_poly l y \<noteq> 0
[PROOF STEP]
by (auto simp add: vars_def)
[PROOF STATE]
proof (state)
this:
Rep_linear_poly l y \<noteq> 0

goal (1 subgoal):
 1. monom_var l \<noteq> x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Rep_linear_poly l y \<noteq> 0
[PROOF STEP]
have "y \<in> set (vars_list l)"
[PROOF STATE]
proof (prove)
using this:
Rep_linear_poly l y \<noteq> 0

goal (1 subgoal):
 1. y \<in> set (vars_list l)
[PROOF STEP]
using finite_vars
[PROOF STATE]
proof (prove)
using this:
Rep_linear_poly l y \<noteq> 0
finite (vars ?p)

goal (1 subgoal):
 1. y \<in> set (vars_list l)
[PROOF STEP]
by (auto simp add: vars_def vars_list_def)
[PROOF STATE]
proof (state)
this:
y \<in> set (vars_list l)

goal (1 subgoal):
 1. monom_var l \<noteq> x \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> set (vars_list l)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
y \<in> set (vars_list l)

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>x \<in> set (vars_list l)\<close> \<open>is_monom l\<close> \<open>y \<noteq> x\<close>
[PROOF STATE]
proof (prove)
using this:
y \<in> set (vars_list l)
x \<in> set (vars_list l)
is_monom l
y \<noteq> x

goal (1 subgoal):
 1. False
[PROOF STEP]
using list_two_elements
[PROOF STATE]
proof (prove)
using this:
y \<in> set (vars_list l)
x \<in> set (vars_list l)
is_monom l
y \<noteq> x
\<lbrakk>?y \<in> set ?l; ?x \<in> set ?l; length ?l = Suc 0; ?y \<noteq> ?x\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. False
[PROOF STEP]
by (simp add: is_monom_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
monom_var l = x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_monom l; ?x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = ?x

goal (1 subgoal):
 1. vars l = {monom_var l}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_monom l; ?x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = ?x
[PROOF STEP]
show "vars l = {monom_var l}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_monom l; ?x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = ?x

goal (1 subgoal):
 1. vars l = {monom_var l}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_monom l; ?x \<in> vars l\<rbrakk> \<Longrightarrow> monom_var l = ?x
is_monom l

goal (1 subgoal):
 1. vars l = {monom_var l}
[PROOF STEP]
by (auto simp add: monom_var_in_vars)
[PROOF STATE]
proof (state)
this:
vars l = {monom_var l}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma monom_valuate:
  assumes "is_monom m"
  shows "m\<lbrace>v\<rbrace> = (monom_coeff m) *R v (monom_var m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<lbrace> v \<rbrace> = monom_coeff m *R v (monom_var m)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_monom m

goal (1 subgoal):
 1. m \<lbrace> v \<rbrace> = monom_coeff m *R v (monom_var m)
[PROOF STEP]
using is_monom_vars_monom_var
[PROOF STATE]
proof (prove)
using this:
is_monom m
is_monom ?l \<Longrightarrow> vars ?l = {monom_var ?l}

goal (1 subgoal):
 1. m \<lbrace> v \<rbrace> = monom_coeff m *R v (monom_var m)
[PROOF STEP]
by (simp add: vars_def coeff_def monom_coeff_def valuate_def)


[STATEMENT]
lemma coeff_zero_simp [simp]:
  "coeff 0 v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff 0 v = 0
[PROOF STEP]
using zero_coeff_zero
[PROOF STATE]
proof (prove)
using this:
(?p = 0) = (\<forall>v. coeff ?p v = 0)

goal (1 subgoal):
 1. coeff 0 v = 0
[PROOF STEP]
by blast


[STATEMENT]
lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall> v. coeff p v = coeff q v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p = q) = (\<forall>v. coeff p v = coeff q v)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma poly_eqI:
  assumes "\<And>v. coeff p v = coeff q v"
  shows "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
using assms poly_eq_iff
[PROOF STATE]
proof (prove)
using this:
coeff p ?v = coeff q ?v
(?p = ?q) = (\<forall>v. coeff ?p v = coeff ?q v)

goal (1 subgoal):
 1. p = q
[PROOF STEP]
by simp


[STATEMENT]
lemma coeff_sum_list:
  assumes "distinct xs"
  shows "coeff (\<Sum>x\<leftarrow>xs. f x *R lp_monom 1 x) v = (if v \<in> set xs then f v else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (\<Sum>x\<leftarrow>xs. f x *R lp_monom 1 x) v = (if v \<in> set xs then f v else 0)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct xs

goal (1 subgoal):
 1. coeff (\<Sum>x\<leftarrow>xs. f x *R lp_monom 1 x) v = (if v \<in> set xs then f v else 0)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma linear_poly_sum:
  "p \<lbrace> v \<rbrace> = (\<Sum>x\<in>vars p. coeff p x *R v x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<lbrace> v \<rbrace> = (\<Sum>x\<in>vars p. coeff p x *R v x)
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma all_valuate_zero: assumes "\<And>(v::'a::lrv valuation). p \<lbrace>v\<rbrace> = 0"
  shows "p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = 0
[PROOF STEP]
using all_val assms
[PROOF STATE]
proof (prove)
using this:
\<forall>v. \<exists>v'. (\<forall>x\<in>vars ?p. v' x = v x) \<and> ?p \<lbrace> v' \<rbrace> = (0::?'a) \<Longrightarrow> ?p = 0
p \<lbrace> ?v \<rbrace> = (0::'a)

goal (1 subgoal):
 1. p = 0
[PROOF STEP]
by blast


[STATEMENT]
lemma linear_poly_eqI: assumes "\<And>(v::'a::lrv valuation). (p \<lbrace>v\<rbrace>) = (q \<lbrace>v\<rbrace>)"
  shows "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<lbrace> ?v \<rbrace> = q \<lbrace> ?v \<rbrace>

goal (1 subgoal):
 1. p = q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>v. p \<lbrace> v \<rbrace> = q \<lbrace> v \<rbrace>) \<Longrightarrow> p = q
[PROOF STEP]
have "(p - q) \<lbrace> v \<rbrace> = 0" for v::"'a::lrv valuation"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p - q \<lbrace> v \<rbrace> = (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<lbrace> ?v \<rbrace> = q \<lbrace> ?v \<rbrace>

goal (1 subgoal):
 1. p - q \<lbrace> v \<rbrace> = (0::'a)
[PROOF STEP]
by (subst valuate_minus) auto
[PROOF STATE]
proof (state)
this:
p - q \<lbrace> ?v \<rbrace> = (0::'a)

goal (1 subgoal):
 1. (\<And>v. p \<lbrace> v \<rbrace> = q \<lbrace> v \<rbrace>) \<Longrightarrow> p = q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p - q \<lbrace> ?v \<rbrace> = (0::'a)
[PROOF STEP]
have "p - q = 0"
[PROOF STATE]
proof (prove)
using this:
p - q \<lbrace> ?v \<rbrace> = (0::'a)

goal (1 subgoal):
 1. p - q = 0
[PROOF STEP]
by (intro all_valuate_zero) auto
[PROOF STATE]
proof (state)
this:
p - q = 0

goal (1 subgoal):
 1. (\<And>v. p \<lbrace> v \<rbrace> = q \<lbrace> v \<rbrace>) \<Longrightarrow> p = q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p - q = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p - q = 0

goal (1 subgoal):
 1. p = q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p = q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma monom_poly_assemble:
  assumes "is_monom p"
  shows "monom_coeff p *R lp_monom 1 (monom_var p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_coeff p *R lp_monom 1 (monom_var p) = p
[PROOF STEP]
by (simp add: assms linear_poly_eqI monom_valuate valuate_scaleRat)


[STATEMENT]
lemma coeff_sum: "coeff (sum (f :: _ \<Rightarrow> linear_poly) is) x = sum (\<lambda> i. coeff (f i) x) is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff (sum f is) x = (\<Sum>i\<in>is. coeff (f i) x)
[PROOF STEP]
by (induct "is" rule: infinite_finite_induct, auto)


[STATEMENT]
lemma step_deterministic:
  assumes "s1 \<rightarrow> s2" and "s1 \<rightarrow> s3"
  shows "s2 = s3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2 = s3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s1 \<rightarrow> s2
s1 \<rightarrow> s3

goal (1 subgoal):
 1. s2 = s3
[PROOF STEP]
apply (cases s1 s2 rule: step.cases)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>F f l pc d H R \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R \<Sigma> # st); s2 = Global.state.State F H (Frame f l (Suc pc) R (d # \<Sigma>) # st); next_instr (F_get F) f l pc = Some (IPush d)\<rbrakk> \<Longrightarrow> s2 = s3
 2. \<And>F f l pc H R d \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (d # \<Sigma>) # st); s2 = Global.state.State F H (Frame f l (Suc pc) R \<Sigma> # st); next_instr (F_get F) f l pc = Some IPop\<rbrakk> \<Longrightarrow> s2 = s3
 3. \<And>F f l pc n R d H \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R \<Sigma> # st); s2 = Global.state.State F H (Frame f l (Suc pc) R (d # \<Sigma>) # st); next_instr (F_get F) f l pc = Some (IGet n); n < length R; d = R ! n\<rbrakk> \<Longrightarrow> s2 = s3
 4. \<And>F f l pc n R R' d H \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (d # \<Sigma>) # st); s2 = Global.state.State F H (Frame f l (Suc pc) R' \<Sigma> # st); next_instr (F_get F) f l pc = Some (ISet n); n < length R; R' = R[n := d]\<rbrakk> \<Longrightarrow> s2 = s3
 5. \<And>F f l pc x H y d R \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (y # \<Sigma>) # st); s2 = Global.state.State F H (Frame f l (Suc pc) R (d # \<Sigma>) # st); next_instr (F_get F) f l pc = Some (ILoad x); heap_get H (x, y) = Some d\<rbrakk> \<Longrightarrow> s2 = s3
 6. \<And>F f l pc x H y d H' R \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (y # d # \<Sigma>) # st); s2 = Global.state.State F H' (Frame f l (Suc pc) R \<Sigma> # st); next_instr (F_get F) f l pc = Some (IStore x); heap_add H (x, y) d = H'\<rbrakk> \<Longrightarrow> s2 = s3
 7. \<And>F f l pc op ar \<Sigma> x H R st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R \<Sigma> # st); s2 = Global.state.State F H (Frame f l (Suc pc) R (x # drop ar \<Sigma>) # st); next_instr (F_get F) f l pc = Some (IOp op); \<AA>\<rr>\<ii>\<tt>\<yy> op = ar; ar \<le> length \<Sigma>; \<OO>\<pp> op (take ar \<Sigma>) = x\<rbrakk> \<Longrightarrow> s2 = s3
 8. \<And>F f l pc l\<^sub>t l\<^sub>f d l' H R \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (d # \<Sigma>) # st); s2 = Global.state.State F H (Frame f l' 0 R \<Sigma> # st); next_instr (F_get F) f l pc = Some (ICJump l\<^sub>t l\<^sub>f); is_true d \<and> l' = l\<^sub>t \<or> is_false d \<and> l' = l\<^sub>f\<rbrakk> \<Longrightarrow> s2 = s3
 9. \<And>F f l pc g gd \<Sigma> frame\<^sub>g H R st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R \<Sigma> # st); s2 = Global.state.State F H (frame\<^sub>g # Frame f l pc R \<Sigma> # st); next_instr (F_get F) f l pc = Some (ICall g); F_get F g = Some gd; arity gd \<le> length \<Sigma>; frame\<^sub>g = allocate_frame g gd (take (arity gd) \<Sigma>) uninitialized\<rbrakk> \<Longrightarrow> s2 = s3
 10. \<And>F g l\<^sub>g pc\<^sub>g gd \<Sigma>\<^sub>f \<Sigma>\<^sub>g frame\<^sub>f' f l\<^sub>f pc\<^sub>f R\<^sub>f H R\<^sub>g st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame g l\<^sub>g pc\<^sub>g R\<^sub>g \<Sigma>\<^sub>g # Frame f l\<^sub>f pc\<^sub>f R\<^sub>f \<Sigma>\<^sub>f # st); s2 = Global.state.State F H (frame\<^sub>f' # st); next_instr (F_get F) g l\<^sub>g pc\<^sub>g = Some IReturn; F_get F g = Some gd; arity gd \<le> length \<Sigma>\<^sub>f; length \<Sigma>\<^sub>g = return gd; frame\<^sub>f' = Frame f l\<^sub>f (Suc pc\<^sub>f) R\<^sub>f (\<Sigma>\<^sub>g @ drop (arity gd) \<Sigma>\<^sub>f)\<rbrakk> \<Longrightarrow> s2 = s3
[PROOF STEP]
apply (auto elim: step.cases dest: is_true_and_is_false_implies_False) [3]
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>F f l pc n R R' d H \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (d # \<Sigma>) # st); s2 = Global.state.State F H (Frame f l (Suc pc) R' \<Sigma> # st); next_instr (F_get F) f l pc = Some (ISet n); n < length R; R' = R[n := d]\<rbrakk> \<Longrightarrow> s2 = s3
 2. \<And>F f l pc x H y d R \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (y # \<Sigma>) # st); s2 = Global.state.State F H (Frame f l (Suc pc) R (d # \<Sigma>) # st); next_instr (F_get F) f l pc = Some (ILoad x); heap_get H (x, y) = Some d\<rbrakk> \<Longrightarrow> s2 = s3
 3. \<And>F f l pc x H y d H' R \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (y # d # \<Sigma>) # st); s2 = Global.state.State F H' (Frame f l (Suc pc) R \<Sigma> # st); next_instr (F_get F) f l pc = Some (IStore x); heap_add H (x, y) d = H'\<rbrakk> \<Longrightarrow> s2 = s3
 4. \<And>F f l pc op ar \<Sigma> x H R st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R \<Sigma> # st); s2 = Global.state.State F H (Frame f l (Suc pc) R (x # drop ar \<Sigma>) # st); next_instr (F_get F) f l pc = Some (IOp op); \<AA>\<rr>\<ii>\<tt>\<yy> op = ar; ar \<le> length \<Sigma>; \<OO>\<pp> op (take ar \<Sigma>) = x\<rbrakk> \<Longrightarrow> s2 = s3
 5. \<And>F f l pc l\<^sub>t l\<^sub>f d l' H R \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (d # \<Sigma>) # st); s2 = Global.state.State F H (Frame f l' 0 R \<Sigma> # st); next_instr (F_get F) f l pc = Some (ICJump l\<^sub>t l\<^sub>f); is_true d \<and> l' = l\<^sub>t \<or> is_false d \<and> l' = l\<^sub>f\<rbrakk> \<Longrightarrow> s2 = s3
 6. \<And>F f l pc g gd \<Sigma> frame\<^sub>g H R st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R \<Sigma> # st); s2 = Global.state.State F H (frame\<^sub>g # Frame f l pc R \<Sigma> # st); next_instr (F_get F) f l pc = Some (ICall g); F_get F g = Some gd; arity gd \<le> length \<Sigma>; frame\<^sub>g = allocate_frame g gd (take (arity gd) \<Sigma>) uninitialized\<rbrakk> \<Longrightarrow> s2 = s3
 7. \<And>F g l\<^sub>g pc\<^sub>g gd \<Sigma>\<^sub>f \<Sigma>\<^sub>g frame\<^sub>f' f l\<^sub>f pc\<^sub>f R\<^sub>f H R\<^sub>g st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame g l\<^sub>g pc\<^sub>g R\<^sub>g \<Sigma>\<^sub>g # Frame f l\<^sub>f pc\<^sub>f R\<^sub>f \<Sigma>\<^sub>f # st); s2 = Global.state.State F H (frame\<^sub>f' # st); next_instr (F_get F) g l\<^sub>g pc\<^sub>g = Some IReturn; F_get F g = Some gd; arity gd \<le> length \<Sigma>\<^sub>f; length \<Sigma>\<^sub>g = return gd; frame\<^sub>f' = Frame f l\<^sub>f (Suc pc\<^sub>f) R\<^sub>f (\<Sigma>\<^sub>g @ drop (arity gd) \<Sigma>\<^sub>f)\<rbrakk> \<Longrightarrow> s2 = s3
[PROOF STEP]
apply (auto elim: step.cases dest: is_true_and_is_false_implies_False) [3]
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>F f l pc op ar \<Sigma> x H R st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R \<Sigma> # st); s2 = Global.state.State F H (Frame f l (Suc pc) R (x # drop ar \<Sigma>) # st); next_instr (F_get F) f l pc = Some (IOp op); \<AA>\<rr>\<ii>\<tt>\<yy> op = ar; ar \<le> length \<Sigma>; \<OO>\<pp> op (take ar \<Sigma>) = x\<rbrakk> \<Longrightarrow> s2 = s3
 2. \<And>F f l pc l\<^sub>t l\<^sub>f d l' H R \<Sigma> st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R (d # \<Sigma>) # st); s2 = Global.state.State F H (Frame f l' 0 R \<Sigma> # st); next_instr (F_get F) f l pc = Some (ICJump l\<^sub>t l\<^sub>f); is_true d \<and> l' = l\<^sub>t \<or> is_false d \<and> l' = l\<^sub>f\<rbrakk> \<Longrightarrow> s2 = s3
 3. \<And>F f l pc g gd \<Sigma> frame\<^sub>g H R st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame f l pc R \<Sigma> # st); s2 = Global.state.State F H (frame\<^sub>g # Frame f l pc R \<Sigma> # st); next_instr (F_get F) f l pc = Some (ICall g); F_get F g = Some gd; arity gd \<le> length \<Sigma>; frame\<^sub>g = allocate_frame g gd (take (arity gd) \<Sigma>) uninitialized\<rbrakk> \<Longrightarrow> s2 = s3
 4. \<And>F g l\<^sub>g pc\<^sub>g gd \<Sigma>\<^sub>f \<Sigma>\<^sub>g frame\<^sub>f' f l\<^sub>f pc\<^sub>f R\<^sub>f H R\<^sub>g st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame g l\<^sub>g pc\<^sub>g R\<^sub>g \<Sigma>\<^sub>g # Frame f l\<^sub>f pc\<^sub>f R\<^sub>f \<Sigma>\<^sub>f # st); s2 = Global.state.State F H (frame\<^sub>f' # st); next_instr (F_get F) g l\<^sub>g pc\<^sub>g = Some IReturn; F_get F g = Some gd; arity gd \<le> length \<Sigma>\<^sub>f; length \<Sigma>\<^sub>g = return gd; frame\<^sub>f' = Frame f l\<^sub>f (Suc pc\<^sub>f) R\<^sub>f (\<Sigma>\<^sub>g @ drop (arity gd) \<Sigma>\<^sub>f)\<rbrakk> \<Longrightarrow> s2 = s3
[PROOF STEP]
apply (auto elim: step.cases dest: is_true_and_is_false_implies_False) [3]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>F g l\<^sub>g pc\<^sub>g gd \<Sigma>\<^sub>f \<Sigma>\<^sub>g frame\<^sub>f' f l\<^sub>f pc\<^sub>f R\<^sub>f H R\<^sub>g st. \<lbrakk>s1 \<rightarrow> s3; s1 = Global.state.State F H (Frame g l\<^sub>g pc\<^sub>g R\<^sub>g \<Sigma>\<^sub>g # Frame f l\<^sub>f pc\<^sub>f R\<^sub>f \<Sigma>\<^sub>f # st); s2 = Global.state.State F H (frame\<^sub>f' # st); next_instr (F_get F) g l\<^sub>g pc\<^sub>g = Some IReturn; F_get F g = Some gd; arity gd \<le> length \<Sigma>\<^sub>f; length \<Sigma>\<^sub>g = return gd; frame\<^sub>f' = Frame f l\<^sub>f (Suc pc\<^sub>f) R\<^sub>f (\<Sigma>\<^sub>g @ drop (arity gd) \<Sigma>\<^sub>f)\<rbrakk> \<Longrightarrow> s2 = s3
[PROOF STEP]
apply (auto elim: step.cases dest: is_true_and_is_false_implies_False) [1]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma step_right_unique: "right_unique step"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. right_unique (\<rightarrow>)
[PROOF STEP]
using step_deterministic
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s1.0 \<rightarrow> ?s2.0; ?s1.0 \<rightarrow> ?s3.0\<rbrakk> \<Longrightarrow> ?s2.0 = ?s3.0

goal (1 subgoal):
 1. right_unique (\<rightarrow>)
[PROOF STEP]
by (rule right_uniqueI)


[STATEMENT]
lemma final_finished:
  assumes "final F_get IReturn s"
  shows "finished step s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finished (\<rightarrow>) s
[PROOF STEP]
unfolding finished_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Ex ((\<rightarrow>) s)
[PROOF STEP]
proof (rule notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Ex ((\<rightarrow>) s) \<Longrightarrow> False
[PROOF STEP]
assume "\<exists>x. step s x"
[PROOF STATE]
proof (state)
this:
\<exists>x. s \<rightarrow> x

goal (1 subgoal):
 1. Ex ((\<rightarrow>) s) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>x. s \<rightarrow> x
[PROOF STEP]
obtain s' where "step s s'"
[PROOF STATE]
proof (prove)
using this:
\<exists>x. s \<rightarrow> x

goal (1 subgoal):
 1. (\<And>s'. s \<rightarrow> s' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<rightarrow> s'

goal (1 subgoal):
 1. Ex ((\<rightarrow>) s) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow> s'

goal (1 subgoal):
 1. False
[PROOF STEP]
using \<open>final F_get IReturn s\<close>
[PROOF STATE]
proof (prove)
using this:
s \<rightarrow> s'
final F_get IReturn s

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp: state_ok_def elim!: step.cases final.cases)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]: "cs_list l None = \<up>(l=[])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_list l None = \<up> (l = [])
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma [simp]:
  "cs_list l (Some p)
  = (\<exists>\<^sub>Ax ls. \<up>(l=x#ls) * lseg (x#ls) (Some p) (Some p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_list l (Some p) = (\<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p))
[PROOF STEP]
apply (rule ent_iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. cs_list l (Some p) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p)
 2. \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p) \<Longrightarrow>\<^sub>A cs_list l (Some p)
[PROOF STEP]
apply (cases l)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. l = [] \<Longrightarrow> cs_list l (Some p) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p)
 2. \<And>a list. l = a # list \<Longrightarrow> cs_list l (Some p) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p)
 3. \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p) \<Longrightarrow>\<^sub>A cs_list l (Some p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list. l = a # list \<Longrightarrow> cs_list l (Some p) \<Longrightarrow>\<^sub>A \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p)
 2. \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p) \<Longrightarrow>\<^sub>A cs_list l (Some p)
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p) \<Longrightarrow>\<^sub>A cs_list l (Some p)
[PROOF STEP]
apply (cases l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p) \<Longrightarrow>\<^sub>A cs_list l (Some p)
 2. \<And>a list. l = a # list \<Longrightarrow> \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p) \<Longrightarrow>\<^sub>A cs_list l (Some p)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> \<exists>\<^sub>Ax ls. \<up> (l = x # ls) * lseg (x # ls) (Some p) (Some p) \<Longrightarrow>\<^sub>A cs_list l (Some p)
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cs_prec:
  "precise cs_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise cs_list
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F'. h \<Turnstile> cs_list a p * F \<and>\<^sub>A cs_list a' p * F' \<Longrightarrow> a = a'
[PROOF STEP]
apply (case_tac p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' h p F F'. \<lbrakk>h \<Turnstile> cs_list a p * F \<and>\<^sub>A cs_list a' p * F'; p = None\<rbrakk> \<Longrightarrow> a = a'
 2. \<And>a a' h p F F' aa. \<lbrakk>h \<Turnstile> cs_list a p * F \<and>\<^sub>A cs_list a' p * F'; p = Some aa\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a' h p F F' aa. \<lbrakk>h \<Turnstile> cs_list a p * F \<and>\<^sub>A cs_list a' p * F'; p = Some aa\<rbrakk> \<Longrightarrow> a = a'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b F F' aaa x ls n xa lsa na. (aa, b) \<Turnstile> aaa \<mapsto>\<^sub>r Node xa na * lseg lsa na (Some aaa) * F \<and>\<^sub>A aaa \<mapsto>\<^sub>r Node x n * lseg ls n (Some aaa) * F' \<Longrightarrow> xa = x \<and> lsa = ls
[PROOF STEP]
apply (subgoal_tac "x=xa \<and> n=na", simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b F F' aaa x ls n xa lsa. \<lbrakk>(aa, b) \<Turnstile> aaa \<mapsto>\<^sub>r Node xa n * lseg lsa n (Some aaa) * F \<and>\<^sub>A aaa \<mapsto>\<^sub>r Node xa n * lseg ls n (Some aaa) * F'; x = xa\<rbrakk> \<Longrightarrow> lsa = ls
 2. \<And>aa b F F' aaa x ls n xa lsa na. (aa, b) \<Turnstile> aaa \<mapsto>\<^sub>r Node xa na * lseg lsa na (Some aaa) * F \<and>\<^sub>A aaa \<mapsto>\<^sub>r Node x n * lseg ls n (Some aaa) * F' \<Longrightarrow> x = xa \<and> n = na
[PROOF STEP]
apply (erule prec_frame_expl[OF lseg_prec1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b F F' aaa x ls n xa lsa. x = xa \<Longrightarrow> aaa \<mapsto>\<^sub>r Node xa n * lseg lsa n (Some aaa) * F \<Longrightarrow>\<^sub>A lseg lsa (?p18 aa b F F' aaa x ls n xa lsa) (Some (?q20 aa b F F' aaa x ls n xa lsa)) * ?q20 aa b F F' aaa x ls n xa lsa \<mapsto>\<^sub>r ?x21 aa b F F' aaa x ls n xa lsa * ?F1.16 aa b F F' aaa x ls n xa lsa
 2. \<And>aa b F F' aaa x ls n xa lsa. x = xa \<Longrightarrow> aaa \<mapsto>\<^sub>r Node xa n * lseg ls n (Some aaa) * F' \<Longrightarrow>\<^sub>A lseg ls (?p18 aa b F F' aaa x ls n xa lsa) (Some (?q20 aa b F F' aaa x ls n xa lsa)) * ?q20 aa b F F' aaa x ls n xa lsa \<mapsto>\<^sub>r ?x21 aa b F F' aaa x ls n xa lsa * ?F2.16 aa b F F' aaa x ls n xa lsa
 3. \<And>aa b F F' aaa x ls n xa lsa na. (aa, b) \<Turnstile> aaa \<mapsto>\<^sub>r Node xa na * lseg lsa na (Some aaa) * F \<and>\<^sub>A aaa \<mapsto>\<^sub>r Node x n * lseg ls n (Some aaa) * F' \<Longrightarrow> x = xa \<and> n = na
[PROOF STEP]
apply frame_inference
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b F F' aaa x ls n xa lsa. x = xa \<Longrightarrow> aaa \<mapsto>\<^sub>r Node xa n * lseg ls n (Some aaa) * F' \<Longrightarrow>\<^sub>A lseg ls n (Some aaa) * aaa \<mapsto>\<^sub>r Node xa n * ?F2.16 aa b F F' aaa x ls n xa lsa
 2. \<And>aa b F F' aaa x ls n xa lsa na. (aa, b) \<Turnstile> aaa \<mapsto>\<^sub>r Node xa na * lseg lsa na (Some aaa) * F \<and>\<^sub>A aaa \<mapsto>\<^sub>r Node x n * lseg ls n (Some aaa) * F' \<Longrightarrow> x = xa \<and> n = na
[PROOF STEP]
apply frame_inference
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b F F' aaa x ls n xa lsa na. (aa, b) \<Turnstile> aaa \<mapsto>\<^sub>r Node xa na * lseg lsa na (Some aaa) * F \<and>\<^sub>A aaa \<mapsto>\<^sub>r Node x n * lseg ls n (Some aaa) * F' \<Longrightarrow> x = xa \<and> n = na
[PROOF STEP]
apply (drule prec_frame[OF sngr_prec])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b F F' aaa x ls n xa lsa na. aaa \<mapsto>\<^sub>r Node xa na * lseg lsa na (Some aaa) * F \<Longrightarrow>\<^sub>A ?p60 aa b F F' aaa x ls n xa lsa na \<mapsto>\<^sub>r ?x60 aa b F F' aaa x ls n xa lsa na * ?F1.60 aa b F F' aaa x ls n xa lsa na
 2. \<And>aa b F F' aaa x ls n xa lsa na. aaa \<mapsto>\<^sub>r Node x n * lseg ls n (Some aaa) * F' \<Longrightarrow>\<^sub>A ?p60 aa b F F' aaa x ls n xa lsa na \<mapsto>\<^sub>r ?y60 aa b F F' aaa x ls n xa lsa na * ?F2.60 aa b F F' aaa x ls n xa lsa na
 3. \<And>aa b F F' aaa x ls n xa lsa na. ?x60 aa b F F' aaa x ls n xa lsa na = ?y60 aa b F F' aaa x ls n xa lsa na \<Longrightarrow> x = xa \<and> n = na
[PROOF STEP]
apply frame_inference
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b F F' aaa x ls n xa lsa na. aaa \<mapsto>\<^sub>r Node x n * lseg ls n (Some aaa) * F' \<Longrightarrow>\<^sub>A aaa \<mapsto>\<^sub>r ?y60 aa b F F' aaa x ls n xa lsa na * ?F2.60 aa b F F' aaa x ls n xa lsa na
 2. \<And>aa b F F' aaa x ls n xa lsa na. Node xa na = ?y60 aa b F F' aaa x ls n xa lsa na \<Longrightarrow> x = xa \<and> n = na
[PROOF STEP]
apply frame_inference
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b F F' aaa x ls n xa lsa na. Node xa na = Node x n \<Longrightarrow> x = xa \<and> n = na
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cs_imp_list_impl: "imp_list cs_list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list cs_list
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. precise cs_list
[PROOF STEP]
apply (rule cs_prec)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cs_empty_rule: "<emp> cs_empty <cs_list []>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> cs_empty <cs_list []>
[PROOF STEP]
unfolding cs_empty_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> return None <cs_list []>
[PROOF STEP]
by sep_auto


[STATEMENT]
lemma cs_empty_impl: "imp_list_empty cs_list cs_empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_empty cs_list cs_empty
[PROOF STEP]
by unfold_locales (sep_auto heap: cs_empty_rule)


[STATEMENT]
lemma cs_prepend_rule:
  "<cs_list l p> cs_prepend x p <cs_list (x#l)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <cs_list l p> cs_prepend x p <cs_list (x # l)>
[PROOF STEP]
apply (cases p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p = None \<Longrightarrow> <cs_list l p> cs_prepend x p <cs_list (x # l)>
 2. \<And>a. p = Some a \<Longrightarrow> <cs_list l p> cs_prepend x p <cs_list (x # l)>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p = None \<Longrightarrow> l = [] \<longrightarrow> <emp> cs_prepend x None <cs_list [x]>
 2. \<And>a. p = Some a \<Longrightarrow> <\<exists>\<^sub>Ax ls pp n. pp \<mapsto>\<^sub>r Node x n * lseg ls n (Some a) * \<up> (l = x # ls \<and> a = pp)> cs_prepend x (Some a) <cs_list (x # l)>
[PROOF STEP]
apply (sep_auto simp: cs_prepend.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. p = Some a \<Longrightarrow> <\<exists>\<^sub>Ax ls pp n. pp \<mapsto>\<^sub>r Node x n * lseg ls n (Some a) * \<up> (l = x # ls \<and> a = pp)> cs_prepend x (Some a) <cs_list (x # l)>
[PROOF STEP]
apply (sep_auto simp: cs_prepend.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cs_prepend_impl: "imp_list_prepend cs_list cs_prepend"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_prepend cs_list cs_prepend
[PROOF STEP]
by unfold_locales (sep_auto heap: cs_prepend_rule)


[STATEMENT]
lemma cs_append_rule:
  "<cs_list l p> cs_append x p <cs_list (l@[x])>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <cs_list l p> cs_append x p <cs_list (l @ [x])>
[PROOF STEP]
apply (cases p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p = None \<Longrightarrow> <cs_list l p> cs_append x p <cs_list (l @ [x])>
 2. \<And>a. p = Some a \<Longrightarrow> <cs_list l p> cs_append x p <cs_list (l @ [x])>
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p = None \<Longrightarrow> l = [] \<longrightarrow> <emp> cs_append x None <cs_list [x]>
 2. \<And>a. p = Some a \<Longrightarrow> <\<exists>\<^sub>Ax ls pp n. pp \<mapsto>\<^sub>r Node x n * lseg ls n (Some a) * \<up> (l = x # ls \<and> a = pp)> cs_append x (Some a) <cs_list (l @ [x])>
[PROOF STEP]
apply (sep_auto simp: cs_append.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. p = Some a \<Longrightarrow> <\<exists>\<^sub>Ax ls pp n. pp \<mapsto>\<^sub>r Node x n * lseg ls n (Some a) * \<up> (l = x # ls \<and> a = pp)> cs_append x (Some a) <cs_list (l @ [x])>
[PROOF STEP]
apply (sep_auto simp: cs_append.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xa ls n xb. \<lbrakk>p = Some a; l = xa # ls\<rbrakk> \<Longrightarrow> a \<mapsto>\<^sub>r Node x (Some xb) * xb \<mapsto>\<^sub>r Node xa n * lseg ls n (Some a) \<Longrightarrow>\<^sub>A xb \<mapsto>\<^sub>r Node xa (?n115 a xa ls n xb) * lseg (ls @ [x]) (?n115 a xa ls n xb) (Some xb)
[PROOF STEP]
apply (rule ent_frame_fwd)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a x ls n xb. \<lbrakk>p = Some a; l = x # ls\<rbrakk> \<Longrightarrow> ?P122 a x ls n xb \<Longrightarrow>\<^sub>A ?R122 a x ls n xb
 2. \<And>a xa ls n xb. \<lbrakk>p = Some a; l = xa # ls\<rbrakk> \<Longrightarrow> a \<mapsto>\<^sub>r Node x (Some xb) * xb \<mapsto>\<^sub>r Node xa n * lseg ls n (Some a) \<Longrightarrow>\<^sub>A ?P122 a xa ls n xb * ?F122 a xa ls n xb
 3. \<And>a xa ls n xb. \<lbrakk>p = Some a; l = xa # ls\<rbrakk> \<Longrightarrow> ?R122 a xa ls n xb * ?F122 a xa ls n xb \<Longrightarrow>\<^sub>A xb \<mapsto>\<^sub>r Node xa (?n115 a xa ls n xb) * lseg (ls @ [x]) (?n115 a xa ls n xb) (Some xb)
[PROOF STEP]
apply (rule_tac s=a in lseg_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xa ls n xb. \<lbrakk>p = Some a; l = xa # ls\<rbrakk> \<Longrightarrow> a \<mapsto>\<^sub>r Node x (Some xb) * xb \<mapsto>\<^sub>r Node xa n * lseg ls n (Some a) \<Longrightarrow>\<^sub>A lseg (?l126 a xa ls n xb) (?p126 a xa ls n xb) (Some a) * a \<mapsto>\<^sub>r Node (?x126 a xa ls n xb) (?q126 a xa ls n xb) * ?F122 a xa ls n xb
 2. \<And>a xa ls n xb. \<lbrakk>p = Some a; l = xa # ls\<rbrakk> \<Longrightarrow> lseg (?l126 a xa ls n xb @ [?x126 a xa ls n xb]) (?p126 a xa ls n xb) (?q126 a xa ls n xb) * ?F122 a xa ls n xb \<Longrightarrow>\<^sub>A xb \<mapsto>\<^sub>r Node xa (?n115 a xa ls n xb) * lseg (ls @ [x]) (?n115 a xa ls n xb) (Some xb)
[PROOF STEP]
(* frame_inference does no backtracking
    on instantiating schematics, hence we have to give it some help here. *)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a xa ls n xb. \<lbrakk>p = Some a; l = xa # ls\<rbrakk> \<Longrightarrow> a \<mapsto>\<^sub>r Node x (Some xb) * xb \<mapsto>\<^sub>r Node xa n * lseg ls n (Some a) \<Longrightarrow>\<^sub>A lseg (?l126 a xa ls n xb) (?p126 a xa ls n xb) (Some a) * a \<mapsto>\<^sub>r Node (?x126 a xa ls n xb) (?q126 a xa ls n xb) * ?F122 a xa ls n xb
 2. \<And>a xa ls n xb. \<lbrakk>p = Some a; l = xa # ls\<rbrakk> \<Longrightarrow> lseg (?l126 a xa ls n xb @ [?x126 a xa ls n xb]) (?p126 a xa ls n xb) (?q126 a xa ls n xb) * ?F122 a xa ls n xb \<Longrightarrow>\<^sub>A xb \<mapsto>\<^sub>r Node xa (?n115 a xa ls n xb) * lseg (ls @ [x]) (?n115 a xa ls n xb) (Some xb)
[PROOF STEP]
apply frame_inference
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a xa ls n xb. \<lbrakk>p = Some a; l = xa # ls\<rbrakk> \<Longrightarrow> lseg (ls @ [x]) n (Some xb) * xb \<mapsto>\<^sub>r Node xa n \<Longrightarrow>\<^sub>A xb \<mapsto>\<^sub>r Node xa (?n115 a xa ls n xb) * lseg (ls @ [x]) (?n115 a xa ls n xb) (Some xb)
[PROOF STEP]
apply (sep_auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cs_append_impl: "imp_list_append cs_list cs_append"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_append cs_list cs_append
[PROOF STEP]
by unfold_locales (sep_auto heap: cs_append_rule)


[STATEMENT]
lemma cs_pop_rule:
  "<cs_list (x#l) p> cs_pop p <\<lambda>(y,p'). cs_list l p' * true * \<up>(y=x)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <cs_list (x # l) p> cs_pop p <\<lambda>(y, p'). cs_list l p' * true * \<up> (y = x)>
[PROOF STEP]
apply (cases p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p = None \<Longrightarrow> <cs_list (x # l) p> cs_pop p <\<lambda>(y, p'). cs_list l p' * true * \<up> (y = x)>
 2. \<And>a. p = Some a \<Longrightarrow> <cs_list (x # l) p> cs_pop p <\<lambda>(y, p'). cs_list l p' * true * \<up> (y = x)>
[PROOF STEP]
apply (sep_auto simp: cs_pop.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. p = Some a \<Longrightarrow> <cs_list (x # l) p> cs_pop p <\<lambda>(y, p'). cs_list l p' * true * \<up> (y = x)>
[PROOF STEP]
apply (cases l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>p = Some a; l = []\<rbrakk> \<Longrightarrow> <cs_list (x # l) p> cs_pop p <\<lambda>(y, p'). cs_list l p' * true * \<up> (y = x)>
 2. \<And>a aa list. \<lbrakk>p = Some a; l = aa # list\<rbrakk> \<Longrightarrow> <cs_list (x # l) p> cs_pop p <\<lambda>(y, p'). cs_list l p' * true * \<up> (y = x)>
[PROOF STEP]
apply (sep_auto simp: cs_pop.simps dflt_simps: option.sel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list. \<lbrakk>p = Some a; l = aa # list\<rbrakk> \<Longrightarrow> <cs_list (x # l) p> cs_pop p <\<lambda>(y, p'). cs_list l p' * true * \<up> (y = x)>
[PROOF STEP]
apply (sep_auto
    simp: cs_pop.simps
    dflt_simps: option.sel
    eintros del: exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list pp na. \<lbrakk>p = Some a; l = aa # list; pp \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>n nb nc. ((\<exists>ab b. (ab, b) \<Turnstile> a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a)) \<longrightarrow> aa = n \<and> list = nb \<and> a = nc) \<and> (\<exists>nd. a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a) \<Longrightarrow>\<^sub>A nc \<mapsto>\<^sub>r Node n nd * lseg nb nd (Some a) * true)
[PROOF STEP]
(* Some unfortunate quantifier fiddling :( *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list pp na. \<lbrakk>p = Some a; l = aa # list; pp \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>n nb nc. ((\<exists>ab b. (ab, b) \<Turnstile> a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a)) \<longrightarrow> aa = n \<and> list = nb \<and> a = nc) \<and> (\<exists>nd. a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a) \<Longrightarrow>\<^sub>A nc \<mapsto>\<^sub>r Node n nd * lseg nb nd (Some a) * true)
[PROOF STEP]
apply (rule_tac x=aa in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list pp na. \<lbrakk>p = Some a; l = aa # list; pp \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>n nb. ((\<exists>ab b. (ab, b) \<Turnstile> a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a)) \<longrightarrow> aa = aa \<and> list = n \<and> a = nb) \<and> (\<exists>nc. a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a) \<Longrightarrow>\<^sub>A nb \<mapsto>\<^sub>r Node aa nc * lseg n nc (Some a) * true)
[PROOF STEP]
apply (rule_tac x=list in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list pp na. \<lbrakk>p = Some a; l = aa # list; pp \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>n. ((\<exists>ab b. (ab, b) \<Turnstile> a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a)) \<longrightarrow> aa = aa \<and> list = list \<and> a = n) \<and> (\<exists>nb. a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a) \<Longrightarrow>\<^sub>A n \<mapsto>\<^sub>r Node aa nb * lseg list nb (Some a) * true)
[PROOF STEP]
apply (rule_tac x=a in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list pp na. \<lbrakk>p = Some a; l = aa # list; pp \<noteq> a\<rbrakk> \<Longrightarrow> ((\<exists>ab b. (ab, b) \<Turnstile> a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a)) \<longrightarrow> aa = aa \<and> list = list \<and> a = a) \<and> (\<exists>n. a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a) \<Longrightarrow>\<^sub>A a \<mapsto>\<^sub>r Node aa n * lseg list n (Some a) * true)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list pp na. \<lbrakk>p = Some a; l = aa # list; pp \<noteq> a\<rbrakk> \<Longrightarrow> \<exists>n. a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a) \<Longrightarrow>\<^sub>A a \<mapsto>\<^sub>r Node aa n * lseg list n (Some a) * true
[PROOF STEP]
apply (rule exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list pp na. \<lbrakk>p = Some a; l = aa # list; pp \<noteq> a\<rbrakk> \<Longrightarrow> a \<mapsto>\<^sub>r Node aa na * pp \<mapsto>\<^sub>r Node aa na * lseg list na (Some a) \<Longrightarrow>\<^sub>A a \<mapsto>\<^sub>r Node aa (?n117 a aa list pp na) * lseg list (?n117 a aa list pp na) (Some a) * true
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cs_pop_impl: "imp_list_pop cs_list cs_pop"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_pop cs_list cs_pop
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l p. l \<noteq> [] \<Longrightarrow> <cs_list l p> cs_pop p <\<lambda>r. case r of (r, p') \<Rightarrow> cs_list (tl l) p' * \<up> (r = hd l)>\<^sub>t
[PROOF STEP]
apply (sep_auto heap: cs_pop_rule elim!: neq_NilE)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cs_rotate_rule:
  "<cs_list l p> cs_rotate p <cs_list (rotate1 l)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
[PROOF STEP]
apply (cases p)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. p = None \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
 2. \<And>a. p = Some a \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
[PROOF STEP]
apply (sep_auto simp: cs_rotate.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. p = Some a \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
[PROOF STEP]
apply (cases l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>p = Some a; l = []\<rbrakk> \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
 2. \<And>a aa list. \<lbrakk>p = Some a; l = aa # list\<rbrakk> \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list. \<lbrakk>p = Some a; l = aa # list\<rbrakk> \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
[PROOF STEP]
apply (case_tac list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa list. \<lbrakk>p = Some a; l = aa # list; list = []\<rbrakk> \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
 2. \<And>a aa list ab lista. \<lbrakk>p = Some a; l = aa # list; list = ab # lista\<rbrakk> \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa list. \<lbrakk>p = Some a; l = [aa]; list = []\<rbrakk> \<Longrightarrow> <\<exists>\<^sub>Ax ls pp n. pp \<mapsto>\<^sub>r Node x n * lseg ls n (Some a) * \<up> (aa = x \<and> [] = ls \<and> a = pp)> cs_rotate (Some a) <cs_list [aa]>
 2. \<And>a aa list ab lista. \<lbrakk>p = Some a; l = aa # list; list = ab # lista\<rbrakk> \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
[PROOF STEP]
apply (sep_auto simp: cs_rotate.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa list ab lista. \<lbrakk>p = Some a; l = aa # list; list = ab # lista\<rbrakk> \<Longrightarrow> <cs_list l p> cs_rotate p <cs_list (rotate1 l)>
[PROOF STEP]
apply (sep_auto simp: cs_rotate.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ab lista x pp na. \<lbrakk>p = Some a; l = x # ab # lista\<rbrakk> \<Longrightarrow> a \<mapsto>\<^sub>r Node x (Some pp) * pp \<mapsto>\<^sub>r Node ab na * lseg lista na (Some a) \<Longrightarrow>\<^sub>A pp \<mapsto>\<^sub>r Node ab (?n142 a ab lista x pp na) * lseg (lista @ [x]) (?n142 a ab lista x pp na) (Some pp)
[PROOF STEP]
apply (rule ent_frame_fwd)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a ab lista x pp na. \<lbrakk>p = Some a; l = x # ab # lista\<rbrakk> \<Longrightarrow> ?P149 a ab lista x pp na \<Longrightarrow>\<^sub>A ?R149 a ab lista x pp na
 2. \<And>a ab lista x pp na. \<lbrakk>p = Some a; l = x # ab # lista\<rbrakk> \<Longrightarrow> a \<mapsto>\<^sub>r Node x (Some pp) * pp \<mapsto>\<^sub>r Node ab na * lseg lista na (Some a) \<Longrightarrow>\<^sub>A ?P149 a ab lista x pp na * ?F149 a ab lista x pp na
 3. \<And>a ab lista x pp na. \<lbrakk>p = Some a; l = x # ab # lista\<rbrakk> \<Longrightarrow> ?R149 a ab lista x pp na * ?F149 a ab lista x pp na \<Longrightarrow>\<^sub>A pp \<mapsto>\<^sub>r Node ab (?n142 a ab lista x pp na) * lseg (lista @ [x]) (?n142 a ab lista x pp na) (Some pp)
[PROOF STEP]
apply (rule_tac s="a" in lseg_append)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a ab lista x pp na. \<lbrakk>p = Some a; l = x # ab # lista\<rbrakk> \<Longrightarrow> a \<mapsto>\<^sub>r Node x (Some pp) * pp \<mapsto>\<^sub>r Node ab na * lseg lista na (Some a) \<Longrightarrow>\<^sub>A lseg (?l153 a ab lista x pp na) (?p153 a ab lista x pp na) (Some a) * a \<mapsto>\<^sub>r Node (?x153 a ab lista x pp na) (?q153 a ab lista x pp na) * ?F149 a ab lista x pp na
 2. \<And>a ab lista x pp na. \<lbrakk>p = Some a; l = x # ab # lista\<rbrakk> \<Longrightarrow> lseg (?l153 a ab lista x pp na @ [?x153 a ab lista x pp na]) (?p153 a ab lista x pp na) (?q153 a ab lista x pp na) * ?F149 a ab lista x pp na \<Longrightarrow>\<^sub>A pp \<mapsto>\<^sub>r Node ab (?n142 a ab lista x pp na) * lseg (lista @ [x]) (?n142 a ab lista x pp na) (Some pp)
[PROOF STEP]
apply frame_inference
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a ab lista x pp na. \<lbrakk>p = Some a; l = x # ab # lista\<rbrakk> \<Longrightarrow> lseg (lista @ [x]) na (Some pp) * pp \<mapsto>\<^sub>r Node ab na \<Longrightarrow>\<^sub>A pp \<mapsto>\<^sub>r Node ab (?n142 a ab lista x pp na) * lseg (lista @ [x]) (?n142 a ab lista x pp na) (Some pp)
[PROOF STEP]
apply sep_auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cs_rotate_impl: "imp_list_rotate cs_list cs_rotate"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_list_rotate cs_list cs_rotate
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l p. <cs_list l p> cs_rotate p <cs_list (rotate1 l)>\<^sub>t
[PROOF STEP]
apply (sep_auto heap: cs_rotate_rule)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "<emp> test <\<lambda>r. \<up>(r=test_result) * true>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> test <\<lambda>r. \<up> (r = test_result)>\<^sub>t
[PROOF STEP]
unfolding test_def test_result_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <emp> cs_empty \<bind> (\<lambda>l. cs_append ''a'' l \<bind> (\<lambda>l. cs_append ''b'' l \<bind> (\<lambda>l. cs_append ''c'' l \<bind> (\<lambda>l. cs_prepend ''0'' l \<bind> (\<lambda>l. cs_rotate l \<bind> (\<lambda>l. cs_pop l \<bind> (\<lambda>(v1, l). cs_pop l \<bind> (\<lambda>(v2, l). cs_pop l \<bind> (\<lambda>(v3, l). cs_pop l \<bind> (\<lambda>(v4, l). return [v1, v2, v3, v4])))))))))) <\<lambda>r. \<up> (r = [''a'', ''b'', ''c'', ''0''])>\<^sub>t
[PROOF STEP]
apply (sep_auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma diamond_x_bot:
  "|x>bot = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > bot = n x
[PROOF STEP]
using n_mult_bot ndiamond_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
n ?x = n (?x * bot)
| ?x > ?y = n (?x * ?y * L)
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | x > bot = n x
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_x_1:
  "|x>1 = n(x * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > (1::'a) = n (x * L)
[PROOF STEP]
by (simp add: ndiamond_def)


[STATEMENT]
lemma diamond_x_L:
  "|x>L = n(x * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > L = n (x * L)
[PROOF STEP]
by (simp add: L_left_zero ndiamond_def mult_assoc)


[STATEMENT]
lemma diamond_x_top:
  "|x>top = n(x * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > top = n (x * L)
[PROOF STEP]
by (metis mult_assoc n_top_L ndiamond_def top_mult_top)


[STATEMENT]
lemma diamond_x_n:
  "|x>n(y) = n(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > n y = n (x * y)
[PROOF STEP]
by (simp add: n_mult ndiamond_def)


[STATEMENT]
lemma diamond_bot_y:
  "|bot>y = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | bot > y = bot
[PROOF STEP]
by (simp add: n_bot ndiamond_def)


[STATEMENT]
lemma diamond_1_y:
  "|1>y = n(y * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) > y = n (y * L)
[PROOF STEP]
by (simp add: ndiamond_def)


[STATEMENT]
lemma diamond_1_n:
  "|1>n(y) = n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | (1::'a) > n y = n y
[PROOF STEP]
by (simp add: diamond_1_y n_n_L)


[STATEMENT]
lemma diamond_L_y:
  "|L>y = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | L > y = (1::'a)
[PROOF STEP]
by (simp add: L_left_zero n_L ndiamond_def)


[STATEMENT]
lemma diamond_top_y:
  "|top>y = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | top > y = (1::'a)
[PROOF STEP]
by (metis sup_left_top sup_right_top diamond_L_y mult_right_dist_sup n_dist_sup n_top ndiamond_def)


[STATEMENT]
lemma diamond_n_y:
  "|n(x)>y = n(x) * n(y * L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x > y = n x * n (y * L)
[PROOF STEP]
by (simp add: n_export ndiamond_def mult_assoc)


[STATEMENT]
lemma diamond_n_bot:
  "|n(x)>bot = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x > bot = bot
[PROOF STEP]
by (simp add: n_bot n_mult_right_bot ndiamond_def)


[STATEMENT]
lemma diamond_n_1:
  "|n(x)>1 = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x > (1::'a) = n x
[PROOF STEP]
using diamond_1_n diamond_1_y diamond_x_1
[PROOF STATE]
proof (prove)
using this:
| (1::'a) > n ?y = n ?y
| (1::'a) > ?y = n (?y * L)
| ?x > (1::'a) = n (?x * L)

goal (1 subgoal):
 1. | n x > (1::'a) = n x
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_n_n:
  "|n(x)>n(y) = n(x) * n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x > n y = n x * n y
[PROOF STEP]
by (simp add: diamond_x_n n_export)


[STATEMENT]
lemma diamond_n_n_same:
  "|n(x)>n(x) = n(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x > n x = n x
[PROOF STEP]
by (simp add: diamond_n_n n_mult_idempotent)


[STATEMENT]
lemma diamond_left_dist_sup:
  "|x \<squnion> y>z = |x>z \<squnion> |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x \<squnion> y > z = | x > z \<squnion> | y > z
[PROOF STEP]
by (simp add: mult_right_dist_sup n_dist_sup ndiamond_def)


[STATEMENT]
lemma diamond_right_dist_sup:
  "|x>(y \<squnion> z) = |x>y \<squnion> |x>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > (y \<squnion> z) = | x > y \<squnion> | x > z
[PROOF STEP]
by (simp add: mult_left_dist_sup n_dist_sup ndiamond_def semiring.distrib_right)


[STATEMENT]
lemma diamond_associative:
  "|x * y>z = |x>(y * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * y > z = | x > (y * z)
[PROOF STEP]
by (simp add: ndiamond_def mult_assoc)


[STATEMENT]
lemma diamond_left_mult:
  "|x * y>z = |x>|y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x * y > z = | x > | y > z
[PROOF STEP]
using n_mult_ni ndiamond_def ni_def mult_assoc
[PROOF STATE]
proof (prove)
using this:
n (?x * ni ?y) = n (?x * ?y)
| ?x > ?y = n (?x * ?y * L)
ni ?x = n ?x * L
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. | x * y > z = | x > | y > z
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_right_mult:
  "|x>(y * z) = |x>|y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > (y * z) = | x > | y > z
[PROOF STEP]
using diamond_associative diamond_left_mult
[PROOF STATE]
proof (prove)
using this:
| ?x * ?y > ?z = | ?x > (?y * ?z)
| ?x * ?y > ?z = | ?x > | ?y > ?z

goal (1 subgoal):
 1. | x > (y * z) = | x > | y > z
[PROOF STEP]
by force


[STATEMENT]
lemma diamond_n_export:
  "|n(x) * y>z = n(x) * |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | n x * y > z = n x * | y > z
[PROOF STEP]
by (simp add: n_export ndiamond_def mult_assoc)


[STATEMENT]
lemma diamond_diamond_export:
  "||x>y>z = |x>y * |z>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | | x > y > z = | x > y * | z > (1::'a)
[PROOF STEP]
using diamond_n_y ndiamond_def
[PROOF STATE]
proof (prove)
using this:
| n ?x > ?y = n ?x * n (?y * L)
| ?x > ?y = n (?x * ?y * L)

goal (1 subgoal):
 1. | | x > y > z = | x > y * | z > (1::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_left_isotone:
  "x \<le> y \<Longrightarrow> |x>z \<le> |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> | x > z \<le> | y > z
[PROOF STEP]
by (metis diamond_left_dist_sup le_iff_sup)


[STATEMENT]
lemma diamond_right_isotone:
  "y \<le> z \<Longrightarrow> |x>y \<le> |x>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> z \<Longrightarrow> | x > y \<le> | x > z
[PROOF STEP]
by (metis diamond_right_dist_sup le_iff_sup)


[STATEMENT]
lemma diamond_isotone:
  "w \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> |w>x \<le> |y>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> | w > x \<le> | y > z
[PROOF STEP]
by (meson diamond_left_isotone diamond_right_isotone order_trans)


[STATEMENT]
lemma ndiamond_to_L:
  "\<parallel>x\<guillemotright>y = |x>n(y) * L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x \<guillemotright> y = | x > n y * L
[PROOF STEP]
by (simp add: diamond_x_n ndiamond_L_def)


[STATEMENT]
lemma ndiamond_from_L:
  "|x>y = n(\<parallel>x\<guillemotright>(y * L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x > y = n (\<parallel> x \<guillemotright> (y * L))
[PROOF STEP]
by (simp add: n_n_L ndiamond_def mult_assoc ndiamond_L_def)


[STATEMENT]
lemma diamond_L_ni:
  "\<parallel>x\<guillemotright>y = ni(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x \<guillemotright> y = ni (x * y)
[PROOF STEP]
by (simp add: ni_def ndiamond_L_def)


[STATEMENT]
lemma diamond_L_associative:
  "\<parallel>x * y\<guillemotright>z = \<parallel>x\<guillemotright>(y * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x * y \<guillemotright> z = \<parallel> x \<guillemotright> (y * z)
[PROOF STEP]
by (simp add: diamond_L_ni mult_assoc)


[STATEMENT]
lemma diamond_L_left_mult:
  "\<parallel>x * y\<guillemotright>z = \<parallel>x\<guillemotright>\<parallel>y\<guillemotright>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x * y \<guillemotright> z = \<parallel> x \<guillemotright> \<parallel> y \<guillemotright> z
[PROOF STEP]
using diamond_L_associative diamond_L_ni ni_mult
[PROOF STATE]
proof (prove)
using this:
\<parallel> ?x * ?y \<guillemotright> ?z = \<parallel> ?x \<guillemotright> (?y * ?z)
\<parallel> ?x \<guillemotright> ?y = ni (?x * ?y)
ni (?x * ni ?y) = ni (?x * ?y)

goal (1 subgoal):
 1. \<parallel> x * y \<guillemotright> z = \<parallel> x \<guillemotright> \<parallel> y \<guillemotright> z
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_L_right_mult:
  "\<parallel>x\<guillemotright>(y * z) = \<parallel>x\<guillemotright>\<parallel>y\<guillemotright>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x \<guillemotright> (y * z) = \<parallel> x \<guillemotright> \<parallel> y \<guillemotright> z
[PROOF STEP]
using diamond_L_associative diamond_L_left_mult
[PROOF STATE]
proof (prove)
using this:
\<parallel> ?x * ?y \<guillemotright> ?z = \<parallel> ?x \<guillemotright> (?y * ?z)
\<parallel> ?x * ?y \<guillemotright> ?z = \<parallel> ?x \<guillemotright> \<parallel> ?y \<guillemotright> ?z

goal (1 subgoal):
 1. \<parallel> x \<guillemotright> (y * z) = \<parallel> x \<guillemotright> \<parallel> y \<guillemotright> z
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_L_left_dist_sup:
  "\<parallel>x \<squnion> y\<guillemotright>z = \<parallel>x\<guillemotright>z \<squnion> \<parallel>y\<guillemotright>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x \<squnion> y \<guillemotright> z = \<parallel> x \<guillemotright> z \<squnion> \<parallel> y \<guillemotright> z
[PROOF STEP]
by (simp add: diamond_L_ni mult_right_dist_sup ni_dist_sup)


[STATEMENT]
lemma diamond_L_x_ni:
  "\<parallel>x\<guillemotright>ni(y) = ni(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel> x \<guillemotright> ni y = ni (x * y)
[PROOF STEP]
using n_mult_ni ni_def ndiamond_L_def
[PROOF STATE]
proof (prove)
using this:
n (?x * ni ?y) = n (?x * ?y)
ni ?x = n ?x * L
\<parallel> ?x \<guillemotright> ?y \<equiv> n (?x * ?y) * L

goal (1 subgoal):
 1. \<parallel> x \<guillemotright> ni y = ni (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_L_left_isotone:
  "x \<le> y \<Longrightarrow> \<parallel>x\<guillemotright>z \<le> \<parallel>y\<guillemotright>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<parallel> x \<guillemotright> z \<le> \<parallel> y \<guillemotright> z
[PROOF STEP]
using mult_left_isotone ni_def ni_isotone ndiamond_L_def
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z
ni ?x = n ?x * L
?x \<le> ?y \<Longrightarrow> ni ?x \<le> ni ?y
\<parallel> ?x \<guillemotright> ?y \<equiv> n (?x * ?y) * L

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<parallel> x \<guillemotright> z \<le> \<parallel> y \<guillemotright> z
[PROOF STEP]
by auto


[STATEMENT]
lemma diamond_L_right_isotone:
  "y \<le> z \<Longrightarrow> \<parallel>x\<guillemotright>y \<le> \<parallel>x\<guillemotright>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> z \<Longrightarrow> \<parallel> x \<guillemotright> y \<le> \<parallel> x \<guillemotright> z
[PROOF STEP]
using mult_right_isotone ni_def ni_isotone ndiamond_L_def
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
ni ?x = n ?x * L
?x \<le> ?y \<Longrightarrow> ni ?x \<le> ni ?y
\<parallel> ?x \<guillemotright> ?y \<equiv> n (?x * ?y) * L

goal (1 subgoal):
 1. y \<le> z \<Longrightarrow> \<parallel> x \<guillemotright> y \<le> \<parallel> x \<guillemotright> z
[PROOF STEP]
by auto