[STATEMENT]
lemma pbval_bval_part: "pbval b (part s) = bval b s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pbval b (part s) = bval b s
[PROOF STEP]
apply(induct b)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. pbval (Bc x) (part s) = bval (Bc x) s
 2. \<And>b. pbval b (part s) = bval b s \<Longrightarrow> pbval (bexp.Not b) (part s) = bval (bexp.Not b) s
 3. \<And>b1 b2. \<lbrakk>pbval b1 (part s) = bval b1 s; pbval b2 (part s) = bval b2 s\<rbrakk> \<Longrightarrow> pbval (And b1 b2) (part s) = bval (And b1 b2) s
 4. \<And>x1a x2a. pbval (Less x1a x2a) (part s) = bval (Less x1a x2a) s
[PROOF STEP]
by (auto simp: paval_aval_part)


[STATEMENT]
lemma part_paval_aval: "part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))
[PROOF STEP]
apply(rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. part (s(x := aval a s)) xa = (part s(x \<mapsto> paval a (part s))) xa
[PROOF STEP]
apply(case_tac "xa=x")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa = x \<Longrightarrow> part (s(x := aval a s)) xa = (part s(x \<mapsto> paval a (part s))) xa
 2. \<And>xa. xa \<noteq> x \<Longrightarrow> part (s(x := aval a s)) xa = (part s(x \<mapsto> paval a (part s))) xa
[PROOF STEP]
unfolding part_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa = x \<Longrightarrow> Some ((s(x := aval a s)) xa) = ((\<lambda>v. Some (s v))(x \<mapsto> paval a (\<lambda>v. Some (s v)))) xa
 2. \<And>xa. xa \<noteq> x \<Longrightarrow> Some ((s(x := aval a s)) xa) = ((\<lambda>v. Some (s v))(x \<mapsto> paval a (\<lambda>v. Some (s v)))) xa
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aval a s = paval a (\<lambda>v. Some (s v))
[PROOF STEP]
by (metis (full_types) domIff map_le_def map_le_substate_conv option.distinct(1) part_def paval_aval2 subsetI)


[STATEMENT]
lemma full_to_part: "(C, s) \<Rightarrow> m \<Down> s' \<Longrightarrow>  (C, part s) \<Rightarrow>\<^sub>A m \<Down> part s' "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, s) \<Rightarrow> m \<Down> s' \<Longrightarrow> (C, part s) \<Rightarrow>\<^sub>A m \<Down> part s'
[PROOF STEP]
apply(induct rule: big_step_t_induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s. (SKIP, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 2. \<And>x a s. (x ::= a, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part (s(x := aval a s))
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
 4. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 5. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 6. \<And>b s c. \<not> bval b s \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
[PROOF STEP]
using Skip
[PROOF STATE]
proof (prove)
using this:
(SKIP, ?s) \<Rightarrow>\<^sub>A Suc 0 \<Down> ?s

goal (7 subgoals):
 1. \<And>s. (SKIP, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 2. \<And>x a s. (x ::= a, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part (s(x := aval a s))
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
 4. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 5. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 6. \<And>b s c. \<not> bval b s \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x a s. (x ::= a, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part (s(x := aval a s))
 2. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
 3. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 4. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 5. \<And>b s c. \<not> bval b s \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 6. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
[PROOF STEP]
apply (subst Assign)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>x a s. vars a \<union> {x} \<subseteq> dom (part s)
 2. \<And>x a s. paval a (part s) = ?v10 x a s
 3. \<And>x a s. part (s(x := aval a s)) = part s(x \<mapsto> ?v10 x a s)
 4. \<And>x a s. True
 5. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
 6. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 7. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 8. \<And>b s c. \<not> bval b s \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 9. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
[PROOF STEP]
using part_paval_aval
[PROOF STATE]
proof (prove)
using this:
part (?s(?x := aval ?a ?s)) = part ?s(?x \<mapsto> paval ?a (part ?s))

goal (9 subgoals):
 1. \<And>x a s. vars a \<union> {x} \<subseteq> dom (part s)
 2. \<And>x a s. paval a (part s) = ?v10 x a s
 3. \<And>x a s. part (s(x := aval a s)) = part s(x \<mapsto> ?v10 x a s)
 4. \<And>x a s. True
 5. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
 6. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 7. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A y \<Down> part t
 8. \<And>b s c. \<not> bval b s \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 9. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
[PROOF STEP]
apply(simp_all add: )
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; z = x + y; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (c1;; c2, part s1) \<Rightarrow>\<^sub>A x + y \<Down> part s3
 2. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = Suc x; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A Suc x \<Down> part t
 3. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = Suc x; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A Suc x \<Down> part t
 4. \<And>b s c. \<lbrakk>\<not> bval b s; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 5. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; Suc (x + y) = z; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
[PROOF STEP]
apply(rule Seq)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; z = x + y; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (c1, part s1) \<Rightarrow>\<^sub>A ?x31 c1 s1 x s2 c2 y s3 z \<Down> ?s2.31 c1 s1 x s2 c2 y s3 z
 2. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; z = x + y; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (c2, ?s2.31 c1 s1 x s2 c2 y s3 z) \<Rightarrow>\<^sub>A ?y31 c1 s1 x s2 c2 y s3 z \<Down> part s3
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow> x \<Down> s2; (c1, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (c2, s2) \<Rightarrow> y \<Down> s3; (c2, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; z = x + y; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> x + y = ?x31 c1 s1 x s2 c2 y s3 z + ?y31 c1 s1 x s2 c2 y s3 z
 4. \<And>b s c1 x t y c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = Suc x; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A Suc x \<Down> part t
 5. \<And>b s c2 x t y c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; y = Suc x; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A Suc x \<Down> part t
 6. \<And>b s c. \<lbrakk>\<not> bval b s; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; Suc (x + y) = z; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A z \<Down> part s3
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b s c1 x t c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A Suc x \<Down> part t
 2. \<And>b s c2 x t c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A Suc x \<Down> part t
 3. \<And>b s c. \<lbrakk>\<not> bval b s; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 4. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A Suc (x + y) \<Down> part s3
[PROOF STEP]
apply(rule IfTrue)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>b s c1 x t c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (part s)
 2. \<And>b s c1 x t c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> dom (part t) = dom (part s)
 3. \<And>b s c1 x t c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> pbval b (part s)
 4. \<And>b s c1 x t c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (c1, part s) \<Rightarrow>\<^sub>A ?x40 b s c1 x t c2 \<Down> part t
 5. \<And>b s c1 x t c2. \<lbrakk>bval b s; (c1, s) \<Rightarrow> x \<Down> t; (c1, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> Suc x = ?x40 b s c1 x t c2 + 1
 6. \<And>b s c2 x t c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A Suc x \<Down> part t
 7. \<And>b s c. \<lbrakk>\<not> bval b s; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 8. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A Suc (x + y) \<Down> part s3
[PROOF STEP]
apply (auto simp: pbval_bval_part)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b s c2 x t c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, part s) \<Rightarrow>\<^sub>A Suc x \<Down> part t
 2. \<And>b s c. \<lbrakk>\<not> bval b s; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 3. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A Suc (x + y) \<Down> part s3
[PROOF STEP]
apply(rule IfFalse)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>b s c2 x t c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (part s)
 2. \<And>b s c2 x t c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> dom (part t) = dom (part s)
 3. \<And>b s c2 x t c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> \<not> pbval b (part s)
 4. \<And>b s c2 x t c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (c2, part s) \<Rightarrow>\<^sub>A ?x47 b s c2 x t c1 \<Down> part t
 5. \<And>b s c2 x t c1. \<lbrakk>\<not> bval b s; (c2, s) \<Rightarrow> x \<Down> t; (c2, part s) \<Rightarrow>\<^sub>A x \<Down> part t; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> Suc x = ?x47 b s c2 x t c1 + 1
 6. \<And>b s c. \<lbrakk>\<not> bval b s; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 7. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A Suc (x + y) \<Down> part s3
[PROOF STEP]
apply (auto simp: pbval_bval_part)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b s c. \<lbrakk>\<not> bval b s; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s) \<Rightarrow>\<^sub>A Suc 0 \<Down> part s
 2. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A Suc (x + y) \<Down> part s3
[PROOF STEP]
apply(rule WhileFalse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b s c. \<lbrakk>\<not> bval b s; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (part s)
 2. \<And>b s c. \<lbrakk>\<not> bval b s; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> \<not> pbval b (part s)
 3. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A Suc (x + y) \<Down> part s3
[PROOF STEP]
apply (auto simp: pbval_bval_part)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, part s1) \<Rightarrow>\<^sub>A Suc (x + y) \<Down> part s3
[PROOF STEP]
apply(rule WhileTrue)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> pbval b (part s1)
 2. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> vars b \<subseteq> dom (part s1)
 3. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (c, part s1) \<Rightarrow>\<^sub>A ?x57 b s1 c x s2 y s3 \<Down> ?s2.57 b s1 c x s2 y s3
 4. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> (WHILE b DO c, ?s2.57 b s1 c x s2 y s3) \<Rightarrow>\<^sub>A ?y57 b s1 c x s2 y s3 \<Down> part s3
 5. \<And>b s1 c x s2 y s3. \<lbrakk>bval b s1; (c, s1) \<Rightarrow> x \<Down> s2; (c, part s1) \<Rightarrow>\<^sub>A x \<Down> part s2; (WHILE b DO c, s2) \<Rightarrow> y \<Down> s3; (WHILE b DO c, part s2) \<Rightarrow>\<^sub>A y \<Down> part s3; \<And>s x a. part (s(x := aval a s)) = part s(x \<mapsto> paval a (part s))\<rbrakk> \<Longrightarrow> 1 + ?x57 b s1 c x s2 y s3 + ?y57 b s1 c x s2 y s3 = Suc (x + y)
[PROOF STEP]
apply (auto simp: pbval_bval_part)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma part_to_full': "(C, ps) \<Rightarrow>\<^sub>A m \<Down> ps' \<Longrightarrow> (C, emb ps s) \<Rightarrow> m \<Down> emb ps' s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, ps) \<Rightarrow>\<^sub>A m \<Down> ps' \<Longrightarrow> (C, emb ps s) \<Rightarrow> m \<Down> emb ps' s
[PROOF STEP]
proof (induct rule: big_step_t_part_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>sa. (SKIP, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 2. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v)\<rbrakk> \<Longrightarrow> (x ::= a, emb ps s) \<Rightarrow> Suc 0 \<Down> emb ps' s
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c1, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (c2, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
 4. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 5. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 6. \<And>b sa c. \<lbrakk>vars b \<subseteq> dom sa; \<not> pbval b sa\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
[PROOF STEP]
case (Assign a x ps v ps')
[PROOF STATE]
proof (state)
this:
vars a \<union> {x} \<subseteq> dom ps
paval a ps = v
ps' = ps(x \<mapsto> v)

goal (7 subgoals):
 1. \<And>sa. (SKIP, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 2. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v)\<rbrakk> \<Longrightarrow> (x ::= a, emb ps s) \<Rightarrow> Suc 0 \<Down> emb ps' s
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c1, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (c2, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
 4. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 5. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 6. \<And>b sa c. \<lbrakk>vars b \<subseteq> dom sa; \<not> pbval b sa\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
[PROOF STEP]
have z: "paval a ps = aval a (emb ps s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. paval a ps = aval a (emb ps s)
[PROOF STEP]
apply(rule paval_aval_vars)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars a \<subseteq> dom ps
[PROOF STEP]
using Assign(1)
[PROOF STATE]
proof (prove)
using this:
vars a \<union> {x} \<subseteq> dom ps

goal (1 subgoal):
 1. vars a \<subseteq> dom ps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
paval a ps = aval a (emb ps s)

goal (7 subgoals):
 1. \<And>sa. (SKIP, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 2. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v)\<rbrakk> \<Longrightarrow> (x ::= a, emb ps s) \<Rightarrow> Suc 0 \<Down> emb ps' s
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c1, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (c2, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
 4. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 5. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 6. \<And>b sa c. \<lbrakk>vars b \<subseteq> dom sa; \<not> pbval b sa\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
[PROOF STEP]
have g :"emb ps' s = (emb ps s)(x:=aval a (emb ps s) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emb ps' s = (emb ps s)(x := aval a (emb ps s))
[PROOF STEP]
apply(simp only: Assign z[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. emb (ps(x \<mapsto> v)) s = (emb ps s)(x := v)
[PROOF STEP]
unfolding emb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>va. case (ps(x \<mapsto> v)) va of None \<Rightarrow> s va | Some r \<Rightarrow> r) = (\<lambda>v. case ps v of None \<Rightarrow> s v | Some r \<Rightarrow> r)(x := v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
emb ps' s = (emb ps s)(x := aval a (emb ps s))

goal (7 subgoals):
 1. \<And>sa. (SKIP, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 2. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v)\<rbrakk> \<Longrightarrow> (x ::= a, emb ps s) \<Rightarrow> Suc 0 \<Down> emb ps' s
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c1, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (c2, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
 4. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 5. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 6. \<And>b sa c. \<lbrakk>vars b \<subseteq> dom sa; \<not> pbval b sa\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ::= a, emb ps s) \<Rightarrow> Suc 0 \<Down> emb ps' s
[PROOF STEP]
apply(simp only: g)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x ::= a, emb ps s) \<Rightarrow> Suc 0 \<Down> (emb ps s)(x := aval a (emb ps s))
[PROOF STEP]
by(rule big_step_t.Assign)
[PROOF STATE]
proof (state)
this:
(x ::= a, emb ps s) \<Rightarrow> Suc 0 \<Down> emb ps' s

goal (6 subgoals):
 1. \<And>sa. (SKIP, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 2. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c1, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (c2, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; z = x + y\<rbrakk> \<Longrightarrow> (c1;; c2, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
 3. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c1, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 4. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; (c2, emb ps s) \<Rightarrow> x \<Down> emb ps' s; y = x + 1\<rbrakk> \<Longrightarrow> (IF b THEN c1 ELSE c2, emb ps s) \<Rightarrow> y \<Down> emb ps' s
 5. \<And>b sa c. \<lbrakk>vars b \<subseteq> dom sa; \<not> pbval b sa\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb sa s) \<Rightarrow> Suc 0 \<Down> emb sa s
 6. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; (c, emb s1 s) \<Rightarrow> x \<Down> emb s2 s; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; (WHILE b DO c, emb s2 s) \<Rightarrow> y \<Down> emb s3 s; 1 + x + y = z\<rbrakk> \<Longrightarrow> (WHILE b DO c, emb s1 s) \<Rightarrow> z \<Down> emb s3 s
[PROOF STEP]
qed (auto simp: pbval_bval_vars[symmetric])


[STATEMENT]
lemma part_to_full: "(C, part s) \<Rightarrow>\<^sub>A m \<Down> part s' \<Longrightarrow> (C, s) \<Rightarrow> m \<Down> s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, part s) \<Rightarrow>\<^sub>A m \<Down> part s' \<Longrightarrow> (C, s) \<Rightarrow> m \<Down> s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (C, part s) \<Rightarrow>\<^sub>A m \<Down> part s' \<Longrightarrow> (C, s) \<Rightarrow> m \<Down> s'
[PROOF STEP]
assume "(C, part s) \<Rightarrow>\<^sub>A m \<Down> part s'"
[PROOF STATE]
proof (state)
this:
(C, part s) \<Rightarrow>\<^sub>A m \<Down> part s'

goal (1 subgoal):
 1. (C, part s) \<Rightarrow>\<^sub>A m \<Down> part s' \<Longrightarrow> (C, s) \<Rightarrow> m \<Down> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(C, part s) \<Rightarrow>\<^sub>A m \<Down> part s'
[PROOF STEP]
have "(C, emb (part s) s) \<Rightarrow> m \<Down> emb (part s') s"
[PROOF STATE]
proof (prove)
using this:
(C, part s) \<Rightarrow>\<^sub>A m \<Down> part s'

goal (1 subgoal):
 1. (C, emb (part s) s) \<Rightarrow> m \<Down> emb (part s') s
[PROOF STEP]
by (rule part_to_full')
[PROOF STATE]
proof (state)
this:
(C, emb (part s) s) \<Rightarrow> m \<Down> emb (part s') s

goal (1 subgoal):
 1. (C, part s) \<Rightarrow>\<^sub>A m \<Down> part s' \<Longrightarrow> (C, s) \<Rightarrow> m \<Down> s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(C, emb (part s) s) \<Rightarrow> m \<Down> emb (part s') s
[PROOF STEP]
show "(C, s) \<Rightarrow> m \<Down> s'"
[PROOF STATE]
proof (prove)
using this:
(C, emb (part s) s) \<Rightarrow> m \<Down> emb (part s') s

goal (1 subgoal):
 1. (C, s) \<Rightarrow> m \<Down> s'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(C, s) \<Rightarrow> m \<Down> s'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma part_full_equiv: "(C, s) \<Rightarrow> m \<Down> s' \<longleftrightarrow> (C, part s) \<Rightarrow>\<^sub>A m \<Down> part s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, s) \<Rightarrow> m \<Down> s' = (C, part s) \<Rightarrow>\<^sub>A m \<Down> part s'
[PROOF STEP]
using part_to_full full_to_part
[PROOF STATE]
proof (prove)
using this:
(?C, part ?s) \<Rightarrow>\<^sub>A ?m \<Down> part ?s' \<Longrightarrow> (?C, ?s) \<Rightarrow> ?m \<Down> ?s'
(?C, ?s) \<Rightarrow> ?m \<Down> ?s' \<Longrightarrow> (?C, part ?s) \<Rightarrow>\<^sub>A ?m \<Down> part ?s'

goal (1 subgoal):
 1. (C, s) \<Rightarrow> m \<Down> s' = (C, part s) \<Rightarrow>\<^sub>A m \<Down> part s'
[PROOF STEP]
by metis


[STATEMENT]
lemma big_step_t3_gt0: "(C, ps) \<Rightarrow>\<^sub>A x \<Down> ps' \<Longrightarrow> x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, ps) \<Rightarrow>\<^sub>A x \<Down> ps' \<Longrightarrow> 0 < x
[PROOF STEP]
apply(induct rule: big_step_t_part_induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s. 0 < Suc 0
 2. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v)\<rbrakk> \<Longrightarrow> 0 < Suc 0
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; 0 < x; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; 0 < y; z = x + y\<rbrakk> \<Longrightarrow> 0 < z
 4. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; 0 < x; y = x + 1\<rbrakk> \<Longrightarrow> 0 < y
 5. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; 0 < x; y = x + 1\<rbrakk> \<Longrightarrow> 0 < y
 6. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s\<rbrakk> \<Longrightarrow> 0 < Suc 0
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; 0 < x; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; 0 < y; 1 + x + y = z\<rbrakk> \<Longrightarrow> 0 < z
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma big_step_t3_same: "(C, ps) \<Rightarrow>\<^sub>A m \<Down> ps' ==>  ps = ps' on UNIV - lvars C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, ps) \<Rightarrow>\<^sub>A m \<Down> ps' \<Longrightarrow> ps = ps' on UNIV - lvars C
[PROOF STEP]
apply(induct rule: big_step_t_part_induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s. s = s on UNIV - lvars SKIP
 2. \<And>a x ps v ps'. \<lbrakk>vars a \<union> {x} \<subseteq> dom ps; paval a ps = v; ps' = ps(x \<mapsto> v)\<rbrakk> \<Longrightarrow> ps = ps' on UNIV - lvars (x ::= a)
 3. \<And>c1 s1 x s2 c2 y s3 z. \<lbrakk>(c1, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 = s2 on UNIV - lvars c1; (c2, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 = s3 on UNIV - lvars c2; z = x + y\<rbrakk> \<Longrightarrow> s1 = s3 on UNIV - lvars (c1;; c2)
 4. \<And>b ps ps' c1 x y c2. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; pbval b ps; (c1, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps = ps' on UNIV - lvars c1; y = x + 1\<rbrakk> \<Longrightarrow> ps = ps' on UNIV - lvars (IF b THEN c1 ELSE c2)
 5. \<And>b ps ps' c2 x y c1. \<lbrakk>vars b \<subseteq> dom ps; dom ps' = dom ps; \<not> pbval b ps; (c2, ps) \<Rightarrow>\<^sub>A x \<Down> ps'; ps = ps' on UNIV - lvars c2; y = x + 1\<rbrakk> \<Longrightarrow> ps = ps' on UNIV - lvars (IF b THEN c1 ELSE c2)
 6. \<And>b s c. \<lbrakk>vars b \<subseteq> dom s; \<not> pbval b s\<rbrakk> \<Longrightarrow> s = s on UNIV - lvars (WHILE b DO c)
 7. \<And>b s1 c x s2 y s3 z. \<lbrakk>pbval b s1; vars b \<subseteq> dom s1; (c, s1) \<Rightarrow>\<^sub>A x \<Down> s2; s1 = s2 on UNIV - lvars c; (WHILE b DO c, s2) \<Rightarrow>\<^sub>A y \<Down> s3; s2 = s3 on UNIV - lvars (WHILE b DO c); 1 + x + y = z\<rbrakk> \<Longrightarrow> s1 = s3 on UNIV - lvars (WHILE b DO c)
[PROOF STEP]
by (auto simp: sep_disj_fun_def plus_fun_def)


[STATEMENT]
lemma avalDirekt3_correct: " (x ::= N v, ps) \<Rightarrow>\<^sub>A m \<Down> ps' \<Longrightarrow> paval' a ps = Some v \<Longrightarrow>  (x ::= a, ps) \<Rightarrow>\<^sub>A m \<Down> ps'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x ::= N v, ps) \<Rightarrow>\<^sub>A m \<Down> ps'; paval' a ps = Some v\<rbrakk> \<Longrightarrow> (x ::= a, ps) \<Rightarrow>\<^sub>A m \<Down> ps'
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>paval' a ps = Some v; ps' = ps(x \<mapsto> v); m = Suc 0; ps x = Some y\<rbrakk> \<Longrightarrow> (x ::= a, ps) \<Rightarrow>\<^sub>A Suc 0 \<Down> ps(x \<mapsto> v)
[PROOF STEP]
apply(subst Assign)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>y. \<lbrakk>paval' a ps = Some v; ps' = ps(x \<mapsto> v); m = Suc 0; ps x = Some y\<rbrakk> \<Longrightarrow> vars a \<union> {x} \<subseteq> dom ps
 2. \<And>y. \<lbrakk>paval' a ps = Some v; ps' = ps(x \<mapsto> v); m = Suc 0; ps x = Some y\<rbrakk> \<Longrightarrow> paval a ps = ?v6 y
 3. \<And>y. \<lbrakk>paval' a ps = Some v; ps' = ps(x \<mapsto> v); m = Suc 0; ps x = Some y\<rbrakk> \<Longrightarrow> ps(x \<mapsto> v) = ps(x \<mapsto> ?v6 y)
 4. \<And>y. \<lbrakk>paval' a ps = Some v; ps' = ps(x \<mapsto> v); m = Suc 0; ps x = Some y\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
by (auto simp: paval_paval' paval'dom)


[STATEMENT]
lemma separate_othogonal_commuted': assumes
    "\<And>ps n. P (ps,n) \<Longrightarrow> ps = 0"
    "\<And>ps n. Q (ps,n) \<Longrightarrow> n = 0"
  shows "(P ** Q) s \<longleftrightarrow> P (0,snd s) \<and> Q (fst s,0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q) s = (P (0::'a, snd s) \<and> Q (fst s, 0::'b))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P (?ps, ?n) \<Longrightarrow> ?ps = (0::'a)
Q (?ps, ?n) \<Longrightarrow> ?n = (0::'b)

goal (1 subgoal):
 1. (P \<and>* Q) s = (P (0::'a, snd s) \<and> Q (fst s, 0::'b))
[PROOF STEP]
unfolding sep_conj_def
[PROOF STATE]
proof (prove)
using this:
P (?ps, ?n) \<Longrightarrow> ?ps = (0::'a)
Q (?ps, ?n) \<Longrightarrow> ?n = (0::'b)

goal (1 subgoal):
 1. (\<exists>x y. x ## y \<and> s = x + y \<and> P x \<and> Q y) = (P (0::'a, snd s) \<and> Q (fst s, 0::'b))
[PROOF STEP]
by force


[STATEMENT]
lemma separate_othogonal_commuted: assumes
    "\<And>ps n. P (ps,n) \<Longrightarrow> ps = 0"
    "\<And>ps n. Q (ps,n) \<Longrightarrow> n = 0"
  shows "(P ** Q) (ps,n) \<longleftrightarrow> P (0,n) \<and> Q (ps,0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q) (ps, n) = (P (0::'a, n) \<and> Q (ps, 0::'b))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P (?ps, ?n) \<Longrightarrow> ?ps = (0::'a)
Q (?ps, ?n) \<Longrightarrow> ?n = (0::'b)

goal (1 subgoal):
 1. (P \<and>* Q) (ps, n) = (P (0::'a, n) \<and> Q (ps, 0::'b))
[PROOF STEP]
unfolding sep_conj_def
[PROOF STATE]
proof (prove)
using this:
P (?ps, ?n) \<Longrightarrow> ?ps = (0::'a)
Q (?ps, ?n) \<Longrightarrow> ?n = (0::'b)

goal (1 subgoal):
 1. (\<exists>x y. x ## y \<and> (ps, n) = x + y \<and> P x \<and> Q y) = (P (0::'a, n) \<and> Q (ps, 0::'b))
[PROOF STEP]
by force


[STATEMENT]
lemma separate_othogonal: assumes
    "\<And>ps n. P (ps,n) \<Longrightarrow> n = 0"
    "\<And>ps n. Q (ps,n) \<Longrightarrow> ps = 0"
  shows "(P ** Q) (ps,n) \<longleftrightarrow> P (ps,0) \<and> Q (0,n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and>* Q) (ps, n) = (P (ps, 0::'b) \<and> Q (0::'a, n))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P (?ps, ?n) \<Longrightarrow> ?n = (0::'b)
Q (?ps, ?n) \<Longrightarrow> ?ps = (0::'a)

goal (1 subgoal):
 1. (P \<and>* Q) (ps, n) = (P (ps, 0::'b) \<and> Q (0::'a, n))
[PROOF STEP]
unfolding sep_conj_def
[PROOF STATE]
proof (prove)
using this:
P (?ps, ?n) \<Longrightarrow> ?n = (0::'b)
Q (?ps, ?n) \<Longrightarrow> ?ps = (0::'a)

goal (1 subgoal):
 1. (\<exists>x y. x ## y \<and> (ps, n) = x + y \<and> P x \<and> Q y) = (P (ps, 0::'b) \<and> Q (0::'a, n))
[PROOF STEP]
by force


[STATEMENT]
lemma assumes "  ((\<lambda>(s, n). P (s, n) \<and> vars b \<subseteq> dom s) \<and>* (\<lambda>(s, c). s = 0 \<and> c = Suc 0)) (ps, n)"
shows "\<exists> n'. P (ps, n') \<and> vars b \<subseteq> dom ps \<and> n = Suc n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n'. P (ps, n') \<and> vars b \<subseteq> dom ps \<and> n = Suc n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n'. P (ps, n') \<and> vars b \<subseteq> dom ps \<and> n = Suc n'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>(s, n). P (s, n) \<and> vars b \<subseteq> dom s) \<and>* (\<lambda>(s, c). s = 0 \<and> c = Suc 0)) (ps, n)
[PROOF STEP]
obtain x y where " x ## y" and "(ps, n) = x + y"
      and 2: "(case x of (s, n) \<Rightarrow> P (s, n) \<and> vars b \<subseteq>  dom s)"
      and "(case y of (s, c) \<Rightarrow> s = 0 \<and> c = Suc 0)"
[PROOF STATE]
proof (prove)
using this:
((\<lambda>(s, n). P (s, n) \<and> vars b \<subseteq> dom s) \<and>* (\<lambda>(s, c). s = 0 \<and> c = Suc 0)) (ps, n)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x ## y; (ps, n) = x + y; case x of (s, n) \<Rightarrow> P (s, n) \<and> vars b \<subseteq> dom s; case y of (s, c) \<Rightarrow> s = 0 \<and> c = Suc 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding sep_conj_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x y. x ## y \<and> (ps, n) = x + y \<and> (case x of (s, n) \<Rightarrow> P (s, n) \<and> vars b \<subseteq> dom s) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = Suc 0)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x ## y; (ps, n) = x + y; case x of (s, n) \<Rightarrow> P (s, n) \<and> vars b \<subseteq> dom s; case y of (s, c) \<Rightarrow> s = 0 \<and> c = Suc 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x ## y
(ps, n) = x + y
case x of (s, n) \<Rightarrow> P (s, n) \<and> vars b \<subseteq> dom s
case y of (s, c) \<Rightarrow> s = 0 \<and> c = Suc 0

goal (1 subgoal):
 1. \<exists>n'. P (ps, n') \<and> vars b \<subseteq> dom ps \<and> n = Suc n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x ## y
(ps, n) = x + y
case x of (s, n) \<Rightarrow> P (s, n) \<and> vars b \<subseteq> dom s
case y of (s, c) \<Rightarrow> s = 0 \<and> c = Suc 0
[PROOF STEP]
have "y = (0, Suc 0)" and f: "fst x = ps" and n: "n = snd x + Suc 0"
[PROOF STATE]
proof (prove)
using this:
x ## y
(ps, n) = x + y
case x of (s, n) \<Rightarrow> P (s, n) \<and> vars b \<subseteq> dom s
case y of (s, c) \<Rightarrow> s = 0 \<and> c = Suc 0

goal (1 subgoal):
 1. y = (0, Suc 0) &&& fst x = ps &&& n = snd x + Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = (0, Suc 0)
fst x = ps
n = snd x + Suc 0

goal (1 subgoal):
 1. \<exists>n'. P (ps, n') \<and> vars b \<subseteq> dom ps \<and> n = Suc n'
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
case x of (s, n) \<Rightarrow> P (s, n) \<and> vars b \<subseteq> dom s
y = (0, Suc 0)
fst x = ps
n = snd x + Suc 0
[PROOF STEP]
have "P (ps, snd x) \<and> vars b \<subseteq> dom ps \<and> n = Suc (snd x)"
[PROOF STATE]
proof (prove)
using this:
case x of (s, n) \<Rightarrow> P (s, n) \<and> vars b \<subseteq> dom s
y = (0, Suc 0)
fst x = ps
n = snd x + Suc 0

goal (1 subgoal):
 1. P (ps, snd x) \<and> vars b \<subseteq> dom ps \<and> n = Suc (snd x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (ps, snd x) \<and> vars b \<subseteq> dom ps \<and> n = Suc (snd x)

goal (1 subgoal):
 1. \<exists>n'. P (ps, n') \<and> vars b \<subseteq> dom ps \<and> n = Suc n'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P (ps, snd x) \<and> vars b \<subseteq> dom ps \<and> n = Suc (snd x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P (ps, snd x) \<and> vars b \<subseteq> dom ps \<and> n = Suc (snd x)

goal (1 subgoal):
 1. \<exists>n'. P (ps, n') \<and> vars b \<subseteq> dom ps \<and> n = Suc n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>n'. P (ps, n') \<and> vars b \<subseteq> dom ps \<and> n = Suc n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sep_reorder_dollar_aux:
    "NO_MATCH ($X) A \<Longrightarrow> ($B ** A) = (A ** $B)"
    "($X ** $Y) = $(X+Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (NO_MATCH ($ X) A \<Longrightarrow> ($ B \<and>* A) = (A \<and>* $ B)) &&& ($ X \<and>* $ Y) = $ (X + Y)
[PROOF STEP]
apply (auto simp: sep_simplify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($ X \<and>* $ Y) = $ (X + Y)
[PROOF STEP]
unfolding dollar_def sep_conj_def sep_disj_prod_def sep_disj_nat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>h. \<exists>x y. (fst x ## fst y \<and> True) \<and> h = x + y \<and> (case x of (s, c) \<Rightarrow> s = 0 \<and> c = X) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = Y)) = (\<lambda>(s, c). s = 0 \<and> c = X + Y)
[PROOF STEP]
by auto


[STATEMENT]
lemma stardiff: assumes "(P \<and>* $m) (ps, n)"
  shows  P: "P (ps, n - m)" and "m\<le>n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (ps, n - m) &&& m \<le> n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(P \<and>* $ m) (ps, n)

goal (1 subgoal):
 1. P (ps, n - m) &&& m \<le> n
[PROOF STEP]
unfolding sep_conj_def dollar_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x y. x ## y \<and> (ps, n) = x + y \<and> P x \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = m)

goal (1 subgoal):
 1. P (ps, n - m) &&& m \<le> n
[PROOF STEP]
by auto


[STATEMENT]
lemma [simp]: "(Q ** $0) = Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Q \<and>* $ 0) = Q
[PROOF STEP]
unfolding dollar_def sep_conj_def sep_disj_prod_def sep_disj_nat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>h. \<exists>x y. (fst x ## fst y \<and> True) \<and> h = x + y \<and> Q x \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = 0)) = Q
[PROOF STEP]
by auto


[STATEMENT]
lemma orthogonal_split: assumes "(embP Q \<and>* $ n) = (embP P \<and>* $ m)"
  shows "(Q = P \<and> n = m) \<or> Q = (\<lambda>s. False) \<and> P = (\<lambda>s. False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q = P \<and> n = m \<or> Q = (\<lambda>s. False) \<and> P = (\<lambda>s. False)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(embP Q \<and>* $ n) = (embP P \<and>* $ m)

goal (1 subgoal):
 1. Q = P \<and> n = m \<or> Q = (\<lambda>s. False) \<and> P = (\<lambda>s. False)
[PROOF STEP]
unfolding embP_def dollar_def
[PROOF STATE]
proof (prove)
using this:
((\<lambda>(s, n). Q s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = n)) = ((\<lambda>(s, n). P s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = m))

goal (1 subgoal):
 1. Q = P \<and> n = m \<or> Q = (\<lambda>s. False) \<and> P = (\<lambda>s. False)
[PROOF STEP]
apply (auto intro!: ext)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>((\<lambda>(s, n). Q s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = n)) = ((\<lambda>(s, n). P s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = m)); Q s; Q x\<rbrakk> \<Longrightarrow> P x
 2. \<And>s x. \<lbrakk>((\<lambda>(s, n). Q s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = n)) = ((\<lambda>(s, n). P s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = m)); Q s; P x\<rbrakk> \<Longrightarrow> Q x
 3. \<And>s. \<lbrakk>((\<lambda>(s, n). Q s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = n)) = ((\<lambda>(s, n). P s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = m)); n \<noteq> m; Q s\<rbrakk> \<Longrightarrow> False
 4. \<And>s x. \<lbrakk>((\<lambda>(s, n). Q s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = n)) = ((\<lambda>(s, n). P s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = m)); P s; Q x\<rbrakk> \<Longrightarrow> P x
 5. \<And>s x. \<lbrakk>((\<lambda>(s, n). Q s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = n)) = ((\<lambda>(s, n). P s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = m)); P s; P x\<rbrakk> \<Longrightarrow> Q x
 6. \<And>s. \<lbrakk>((\<lambda>(s, n). Q s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = n)) = ((\<lambda>(s, n). P s \<and> n = 0) \<and>* (\<lambda>(s, c). s = 0 \<and> c = m)); n \<noteq> m; P s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding sep_conj_def
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> Q s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = n)) = (\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> P s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = m)); Q s; Q x\<rbrakk> \<Longrightarrow> P x
 2. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> Q s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = n)) = (\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> P s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = m)); Q s; P x\<rbrakk> \<Longrightarrow> Q x
 3. \<And>s. \<lbrakk>(\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> Q s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = n)) = (\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> P s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = m)); n \<noteq> m; Q s\<rbrakk> \<Longrightarrow> False
 4. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> Q s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = n)) = (\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> P s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = m)); P s; Q x\<rbrakk> \<Longrightarrow> P x
 5. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> Q s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = n)) = (\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> P s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = m)); P s; P x\<rbrakk> \<Longrightarrow> Q x
 6. \<And>s. \<lbrakk>(\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> Q s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = n)) = (\<lambda>h. \<exists>x y. x ## y \<and> h = x + y \<and> (case x of (s, n) \<Rightarrow> P s \<and> n = 0) \<and> (case y of (s, c) \<Rightarrow> s = 0 \<and> c = m)); n \<noteq> m; P s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); Q s; Q x\<rbrakk> \<Longrightarrow> P x
 2. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); Q s; P x\<rbrakk> \<Longrightarrow> Q x
 3. \<And>s. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); n \<noteq> m; Q s\<rbrakk> \<Longrightarrow> False
 4. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); P s; Q x\<rbrakk> \<Longrightarrow> P x
 5. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); P s; P x\<rbrakk> \<Longrightarrow> Q x
 6. \<And>s. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); n \<noteq> m; P s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
unfolding  sep_disj_prod_def  plus_prod_def
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); Q s; Q x\<rbrakk> \<Longrightarrow> P x
 2. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); Q s; P x\<rbrakk> \<Longrightarrow> Q x
 3. \<And>s. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); n \<noteq> m; Q s\<rbrakk> \<Longrightarrow> False
 4. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); P s; Q x\<rbrakk> \<Longrightarrow> P x
 5. \<And>s x. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); P s; P x\<rbrakk> \<Longrightarrow> Q x
 6. \<And>s. \<lbrakk>(\<lambda>h. \<exists>a. h = (a, n) \<and> Q a) = (\<lambda>h. \<exists>a. h = (a, m) \<and> P a); n \<noteq> m; P s\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis fst_conv snd_conv)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma F: assumes "(embP Q \<and>* $ n) = (embP P \<and>* $ m)"
  obtains (blub) "Q = P" and "n = m" |
          (da)  "Q = (\<lambda>s. False)" and "P = (\<lambda>s. False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>Q = P; n = m\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>Q = (\<lambda>s. False); P = (\<lambda>s. False)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms orthogonal_split
[PROOF STATE]
proof (prove)
using this:
(embP Q \<and>* $ n) = (embP P \<and>* $ m)
(embP ?Q \<and>* $ ?n) = (embP ?P \<and>* $ ?m) \<Longrightarrow> ?Q = ?P \<and> ?n = ?m \<or> ?Q = (\<lambda>s. False) \<and> ?P = (\<lambda>s. False)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>Q = P; n = m\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>Q = (\<lambda>s. False); P = (\<lambda>s. False)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma T: assumes "(embP Q \<and>* $ n) = (embP P \<and>* $ m)"
  obtains (blub) x::nat where "Q = P" and "n = m" and "x=x" |
          (da)  "Q = (\<lambda>s. False)" and "P = (\<lambda>s. False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>Q = P; n = m; x = x\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>Q = (\<lambda>s. False); P = (\<lambda>s. False)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms orthogonal_split
[PROOF STATE]
proof (prove)
using this:
(embP Q \<and>* $ n) = (embP P \<and>* $ m)
(embP ?Q \<and>* $ ?n) = (embP ?P \<and>* $ ?m) \<Longrightarrow> ?Q = ?P \<and> ?n = ?m \<or> ?Q = (\<lambda>s. False) \<and> ?P = (\<lambda>s. False)

goal (1 subgoal):
 1. \<lbrakk>\<And>x. \<lbrakk>Q = P; n = m; x = x\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>Q = (\<lambda>s. False); P = (\<lambda>s. False)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma "(x \<hookrightarrow> -) (s,n) \<Longrightarrow> x \<in> dom s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<hookrightarrow> -) (s, n) \<Longrightarrow> x \<in> dom s
[PROOF STEP]
unfolding maps_to_ex_def pointsto_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xa. case (s, n) of (s, c) \<Rightarrow> s = [x \<mapsto> xa] \<and> c = 0 \<Longrightarrow> x \<in> dom s
[PROOF STEP]
by auto


[STATEMENT]
lemma cnv_I: "cnv x x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cnv x x
[PROOF STEP]
unfolding cnv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x
[PROOF STEP]
by simp


[STATEMENT]
lemma Frame'_conv: "Frame P Q F = Frame' (P ** \<box>) \<box> (Q ** \<box>) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Frame P Q F = Frame' (P \<and>* \<box>) \<box> (Q \<and>* \<box>) F
[PROOF STEP]
unfolding Frame_def Frame'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s. P s \<longrightarrow> (Q \<and>* F) s) = (\<forall>s. (\<box> \<and>* P \<and>* \<box>) s \<longrightarrow> ((Q \<and>* \<box>) \<and>* F) s)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Frame'I: "Frame' (P ** \<box>) \<box> (Q ** \<box>) F \<Longrightarrow> cnv F F' \<Longrightarrow> Frame P Q F'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Frame' (P \<and>* \<box>) \<box> (Q \<and>* \<box>) F; cnv F F'\<rbrakk> \<Longrightarrow> Frame P Q F'
[PROOF STEP]
unfolding Frame_def Frame'_def cnv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. (\<box> \<and>* P \<and>* \<box>) s \<longrightarrow> ((Q \<and>* \<box>) \<and>* F) s; F = F'\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (Q \<and>* F') s
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma FrameD: assumes "Frame P Q F" " P s "
  shows "(F ** Q) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F \<and>* Q) s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Frame P Q F
P s

goal (1 subgoal):
 1. (F \<and>* Q) s
[PROOF STEP]
unfolding Frame_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s. P s \<longrightarrow> (Q \<and>* F) s
P s

goal (1 subgoal):
 1. (F \<and>* Q) s
[PROOF STEP]
by (auto simp: sep_conj_commute)


[STATEMENT]
lemma Frame'_match: "Frame' (P ** P') \<box> Q F \<Longrightarrow> Frame' (x \<hookrightarrow> v ** P) P' (x \<hookrightarrow> v ** Q) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Frame' (P \<and>* P') \<box> Q F \<Longrightarrow> Frame' (x \<hookrightarrow> v \<and>* P) P' (x \<hookrightarrow> v \<and>* Q) F
[PROOF STEP]
unfolding Frame_def Frame'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. (\<box> \<and>* P \<and>* P') s \<longrightarrow> (Q \<and>* F) s \<Longrightarrow> \<forall>s. (P' \<and>* x \<hookrightarrow> v \<and>* P) s \<longrightarrow> ((x \<hookrightarrow> v \<and>* Q) \<and>* F) s
[PROOF STEP]
apply (auto simp: sep_conj_ac)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (P \<and>* P') (a, b) \<longrightarrow> (F \<and>* Q) (a, b); (P \<and>* P' \<and>* x \<hookrightarrow> v) (a, b)\<rbrakk> \<Longrightarrow> (F \<and>* Q \<and>* x \<hookrightarrow> v) (a, b)
[PROOF STEP]
by (metis (no_types, opaque_lifting) prod.collapse sep.mult_assoc sep_conj_impl1)


[STATEMENT]
lemma R: assumes "\<And>s. (A imp B) s" shows "((A ** $n) imp (B ** $n)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<and>* $ n) s \<longrightarrow> (B \<and>* $ n) s
[PROOF STEP]
proof (safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (A \<and>* $ n) s \<Longrightarrow> (B \<and>* $ n) s
[PROOF STEP]
assume "(A \<and>* $ n) s"
[PROOF STATE]
proof (state)
this:
(A \<and>* $ n) s

goal (1 subgoal):
 1. (A \<and>* $ n) s \<Longrightarrow> (B \<and>* $ n) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(A \<and>* $ n) s
[PROOF STEP]
obtain h1 h2 where A: "A h1"  and n: "$n h2" and disj: "h1 ## h2" "s = h1+h2"
[PROOF STATE]
proof (prove)
using this:
(A \<and>* $ n) s

goal (1 subgoal):
 1. (\<And>h1 h2. \<lbrakk>A h1; $ n h2; h1 ## h2; s = h1 + h2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding sep_conj_def
[PROOF STATE]
proof (prove)
using this:
\<exists>x y. x ## y \<and> s = x + y \<and> A x \<and> $ n y

goal (1 subgoal):
 1. (\<And>h1 h2. \<lbrakk>A h1; $ n h2; h1 ## h2; s = h1 + h2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A h1
$ n h2
h1 ## h2
s = h1 + h2

goal (1 subgoal):
 1. (A \<and>* $ n) s \<Longrightarrow> (B \<and>* $ n) s
[PROOF STEP]
from assms A
[PROOF STATE]
proof (chain)
picking this:
A ?s \<longrightarrow> B ?s
A h1
[PROOF STEP]
have B: "B h1"
[PROOF STATE]
proof (prove)
using this:
A ?s \<longrightarrow> B ?s
A h1

goal (1 subgoal):
 1. B h1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B h1

goal (1 subgoal):
 1. (A \<and>* $ n) s \<Longrightarrow> (B \<and>* $ n) s
[PROOF STEP]
show "(B ** $n) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (B \<and>* $ n) s
[PROOF STEP]
using B n disj
[PROOF STATE]
proof (prove)
using this:
B h1
$ n h2
h1 ## h2
s = h1 + h2

goal (1 subgoal):
 1. (B \<and>* $ n) s
[PROOF STEP]
unfolding sep_conj_def
[PROOF STATE]
proof (prove)
using this:
B h1
$ n h2
h1 ## h2
s = h1 + h2

goal (1 subgoal):
 1. \<exists>x y. x ## y \<and> s = x + y \<and> B x \<and> $ n y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(B \<and>* $ n) s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Frame'_matchdollar:  assumes "Frame' (P ** P' ** $(n-m)) \<box> Q F" and nm: "n\<ge>m"
  shows "Frame' ($n ** P) P' ($m ** Q) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Frame' ($ n \<and>* P) P' ($ m \<and>* Q) F
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
Frame' (P \<and>* P' \<and>* $ (n - m)) \<box> Q F

goal (1 subgoal):
 1. Frame' ($ n \<and>* P) P' ($ m \<and>* Q) F
[PROOF STEP]
unfolding Frame_def Frame'_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s. (\<box> \<and>* P \<and>* P' \<and>* $ (n - m)) s \<longrightarrow> (Q \<and>* F) s

goal (1 subgoal):
 1. \<forall>s. (P' \<and>* $ n \<and>* P) s \<longrightarrow> (($ m \<and>* Q) \<and>* F) s
[PROOF STEP]
apply (auto simp: sep_conj_ac)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (P \<and>* P' \<and>* $ (n - m)) (a, b) \<longrightarrow> (F \<and>* Q) (a, b); (P \<and>* P' \<and>* $ n) (a, b)\<rbrakk> \<Longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (P \<and>* P' \<and>* $ (n - m)) (a, b) \<longrightarrow> (F \<and>* Q) (a, b); (P \<and>* P' \<and>* $ n) (a, b)\<rbrakk> \<Longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
case (1 a b)
[PROOF STATE]
proof (state)
this:
\<forall>a b. (P \<and>* P' \<and>* $ (n - m)) (a, b) \<longrightarrow> (F \<and>* Q) (a, b)
(P \<and>* P' \<and>* $ n) (a, b)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (P \<and>* P' \<and>* $ (n - m)) (a, b) \<longrightarrow> (F \<and>* Q) (a, b); (P \<and>* P' \<and>* $ n) (a, b)\<rbrakk> \<Longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
have g: "((P \<and>* P' \<and>* $ n) imp (F \<and>* Q \<and>* $ m)) (a, b)
        \<longleftrightarrow> (((P \<and>* P' \<and>* $(n-m)) ** $m) imp ((F \<and>* Q) \<and>* $ m)) (a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)) = (((P \<and>* P' \<and>* $ (n - m)) \<and>* $ m) (a, b) \<longrightarrow> ((F \<and>* Q) \<and>* $ m) (a, b))
[PROOF STEP]
by(simp add: nm sep_reorder_dollar)
[PROOF STATE]
proof (state)
this:
((P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)) = (((P \<and>* P' \<and>* $ (n - m)) \<and>* $ m) (a, b) \<longrightarrow> ((F \<and>* Q) \<and>* $ m) (a, b))

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (P \<and>* P' \<and>* $ (n - m)) (a, b) \<longrightarrow> (F \<and>* Q) (a, b); (P \<and>* P' \<and>* $ n) (a, b)\<rbrakk> \<Longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
have "((P \<and>* P' \<and>* $ n) imp (F \<and>* Q \<and>* $ m)) (a, b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
apply(subst g)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((P \<and>* P' \<and>* $ (n - m)) \<and>* $ m) (a, b) \<longrightarrow> ((F \<and>* Q) \<and>* $ m) (a, b)
[PROOF STEP]
apply(rule R)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. (P \<and>* P' \<and>* $ (n - m)) s \<longrightarrow> (F \<and>* Q) s
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
\<forall>a b. (P \<and>* P' \<and>* $ (n - m)) (a, b) \<longrightarrow> (F \<and>* Q) (a, b)

goal (1 subgoal):
 1. \<And>s. (P \<and>* P' \<and>* $ (n - m)) s \<longrightarrow> (F \<and>* Q) s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (P \<and>* P' \<and>* $ (n - m)) (a, b) \<longrightarrow> (F \<and>* Q) (a, b); (P \<and>* P' \<and>* $ n) (a, b)\<rbrakk> \<Longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
have "(P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)"
[PROOF STATE]
proof (prove)
using this:
(P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)

goal (1 subgoal):
 1. (P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. (P \<and>* P' \<and>* $ (n - m)) (a, b) \<longrightarrow> (F \<and>* Q) (a, b); (P \<and>* P' \<and>* $ n) (a, b)\<rbrakk> \<Longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)

goal (1 subgoal):
 1. (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
using 1(2)
[PROOF STATE]
proof (prove)
using this:
(P \<and>* P' \<and>* $ n) (a, b) \<longrightarrow> (F \<and>* Q \<and>* $ m) (a, b)
(P \<and>* P' \<and>* $ n) (a, b)

goal (1 subgoal):
 1. (F \<and>* Q \<and>* $ m) (a, b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(F \<and>* Q \<and>* $ m) (a, b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Frame'_nomatch: " Frame' P (p ** P') (x \<hookrightarrow> v ** Q) F\<Longrightarrow> Frame' (p ** P) P' (x \<hookrightarrow> v ** Q) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Frame' P (p \<and>* P') (x \<hookrightarrow> v \<and>* Q) F \<Longrightarrow> Frame' (p \<and>* P) P' (x \<hookrightarrow> v \<and>* Q) F
[PROOF STEP]
unfolding  Frame'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. ((p \<and>* P') \<and>* P) s \<longrightarrow> ((x \<hookrightarrow> v \<and>* Q) \<and>* F) s \<Longrightarrow> \<forall>s. (P' \<and>* p \<and>* P) s \<longrightarrow> ((x \<hookrightarrow> v \<and>* Q) \<and>* F) s
[PROOF STEP]
by (auto simp: sep_conj_ac)


[STATEMENT]
lemma Frame'_nomatchempty: " Frame' P P' (x \<hookrightarrow> v ** Q) F\<Longrightarrow> Frame' (\<box> ** P) P' (x \<hookrightarrow> v ** Q) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Frame' P P' (x \<hookrightarrow> v \<and>* Q) F \<Longrightarrow> Frame' (\<box> \<and>* P) P' (x \<hookrightarrow> v \<and>* Q) F
[PROOF STEP]
unfolding  Frame'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. (P' \<and>* P) s \<longrightarrow> ((x \<hookrightarrow> v \<and>* Q) \<and>* F) s \<Longrightarrow> \<forall>s. (P' \<and>* \<box> \<and>* P) s \<longrightarrow> ((x \<hookrightarrow> v \<and>* Q) \<and>* F) s
[PROOF STEP]
by (auto simp: sep_conj_ac)


[STATEMENT]
lemma Frame'_end: " Frame' P \<box> \<box> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Frame' P \<box> \<box> P
[PROOF STEP]
unfolding  Frame'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. (\<box> \<and>* P) s \<longrightarrow> (\<box> \<and>* P) s
[PROOF STEP]
by (auto simp: sep_conj_ac)


[STATEMENT]
lemma symeval_c: "symeval P (N v) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symeval P (N v) v
[PROOF STEP]
unfolding symeval_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s n. P (s, n) \<longrightarrow> paval' (N v) s = Some v
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma symeval_v: assumes "Frame P (x \<hookrightarrow> v) F"
  shows "symeval P (V x) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symeval P (V x) v
[PROOF STEP]
unfolding symeval_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s n. P (s, n) \<longrightarrow> paval' (V x) s = Some v
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s n. P (s, n) \<Longrightarrow> s x = Some v
[PROOF STEP]
apply (drule FrameD[OF assms])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s n. (F \<and>* x \<hookrightarrow> v) (s, n) \<Longrightarrow> s x = Some v
[PROOF STEP]
unfolding sep_conj_def pointsto_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s n. \<exists>xa y. xa ## y \<and> (s, n) = xa + y \<and> F xa \<and> (case y of (s, c) \<Rightarrow> s = [x \<mapsto> v] \<and> c = 0) \<Longrightarrow> s x = Some v
[PROOF STEP]
apply (auto simp: plus_fun_conv)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma symeval_plus: assumes "symeval P e1 v1" "symeval P e2 v2"
  shows "symeval P (Plus e1 e2) (v1+v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symeval P (Plus e1 e2) (v1 + v2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
symeval P e1 v1
symeval P e2 v2

goal (1 subgoal):
 1. symeval P (Plus e1 e2) (v1 + v2)
[PROOF STEP]
unfolding symeval_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s n. P (s, n) \<longrightarrow> paval' e1 s = Some v1
\<forall>s n. P (s, n) \<longrightarrow> paval' e2 s = Some v2

goal (1 subgoal):
 1. \<forall>s n. P (s, n) \<longrightarrow> paval' (Plus e1 e2) s = Some (v1 + v2)
[PROOF STEP]
by auto


[STATEMENT]
lemma symevalb_c: "symevalb P (Bc v) v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symevalb P (Bc v) v
[PROOF STEP]
unfolding symevalb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s n. P (s, n) \<longrightarrow> pbval' (Bc v) s = Some v
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma symevalb_and: assumes "symevalb P e1 v1" "symevalb P e2 v2"
  shows "symevalb P (And e1 e2) (v1 \<and> v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symevalb P (And e1 e2) (v1 \<and> v2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
symevalb P e1 v1
symevalb P e2 v2

goal (1 subgoal):
 1. symevalb P (And e1 e2) (v1 \<and> v2)
[PROOF STEP]
unfolding symevalb_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s n. P (s, n) \<longrightarrow> pbval' e1 s = Some v1
\<forall>s n. P (s, n) \<longrightarrow> pbval' e2 s = Some v2

goal (1 subgoal):
 1. \<forall>s n. P (s, n) \<longrightarrow> pbval' (And e1 e2) s = Some (v1 \<and> v2)
[PROOF STEP]
by auto


[STATEMENT]
lemma symevalb_not:  assumes "symevalb P e v"
  shows "symevalb P (Not e) (\<not> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symevalb P (bexp.Not e) (\<not> v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
symevalb P e v

goal (1 subgoal):
 1. symevalb P (bexp.Not e) (\<not> v)
[PROOF STEP]
unfolding symevalb_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s n. P (s, n) \<longrightarrow> pbval' e s = Some v

goal (1 subgoal):
 1. \<forall>s n. P (s, n) \<longrightarrow> pbval' (bexp.Not e) s = Some (\<not> v)
[PROOF STEP]
by auto


[STATEMENT]
lemma symevalb_less: assumes "symeval P e1 v1" "symeval P e2 v2"
  shows "symevalb P (Less e1 e2) (v1 < v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. symevalb P (Less e1 e2) (v1 < v2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
symeval P e1 v1
symeval P e2 v2

goal (1 subgoal):
 1. symevalb P (Less e1 e2) (v1 < v2)
[PROOF STEP]
unfolding symevalb_def symeval_def
[PROOF STATE]
proof (prove)
using this:
\<forall>s n. P (s, n) \<longrightarrow> paval' e1 s = Some v1
\<forall>s n. P (s, n) \<longrightarrow> paval' e2 s = Some v2

goal (1 subgoal):
 1. \<forall>s n. P (s, n) \<longrightarrow> pbval' (Less e1 e2) s = Some (v1 < v2)
[PROOF STEP]
by auto


[STATEMENT]
lemma coprime_poly_0:
  "poly p x \<noteq> 0 \<or> poly q x \<noteq> 0" if "coprime p q"
  for x :: "'a :: field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poly p x \<noteq> (0::'a) \<or> poly q x \<noteq> (0::'a)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (poly p x \<noteq> (0::'a) \<or> poly q x \<noteq> (0::'a)) \<Longrightarrow> False
[PROOF STEP]
assume " \<not> (poly p x \<noteq> 0 \<or> poly q x \<noteq> 0)"
[PROOF STATE]
proof (state)
this:
\<not> (poly p x \<noteq> (0::'a) \<or> poly q x \<noteq> (0::'a))

goal (1 subgoal):
 1. \<not> (poly p x \<noteq> (0::'a) \<or> poly q x \<noteq> (0::'a)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (poly p x \<noteq> (0::'a) \<or> poly q x \<noteq> (0::'a))
[PROOF STEP]
have "[:-x, 1:] dvd p" "[:-x, 1:] dvd q"
[PROOF STATE]
proof (prove)
using this:
\<not> (poly p x \<noteq> (0::'a) \<or> poly q x \<noteq> (0::'a))

goal (1 subgoal):
 1. [:- x, 1::'a:] dvd p &&& [:- x, 1::'a:] dvd q
[PROOF STEP]
by (simp_all add: poly_eq_0_iff_dvd)
[PROOF STATE]
proof (state)
this:
[:- x, 1::'a:] dvd p
[:- x, 1::'a:] dvd q

goal (1 subgoal):
 1. \<not> (poly p x \<noteq> (0::'a) \<or> poly q x \<noteq> (0::'a)) \<Longrightarrow> False
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
coprime p q
[:- x, 1::'a:] dvd p
[:- x, 1::'a:] dvd q
[PROOF STEP]
have "is_unit [:-x, 1:]"
[PROOF STATE]
proof (prove)
using this:
coprime p q
[:- x, 1::'a:] dvd p
[:- x, 1::'a:] dvd q

goal (1 subgoal):
 1. is_unit [:- x, 1::'a:]
[PROOF STEP]
by (rule coprime_common_divisor)
[PROOF STATE]
proof (state)
this:
is_unit [:- x, 1::'a:]

goal (1 subgoal):
 1. \<not> (poly p x \<noteq> (0::'a) \<or> poly q x \<noteq> (0::'a)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_unit [:- x, 1::'a:]
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
is_unit [:- x, 1::'a:]

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smult_cancel:
  fixes p::"'a::idom poly"
  assumes "c\<noteq>0" and smult: "smult c p = smult c q"
  shows "p=q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
have "smult c (p-q)=0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smult c (p - q) = 0
[PROOF STEP]
using smult
[PROOF STATE]
proof (prove)
using this:
smult c p = smult c q

goal (1 subgoal):
 1. smult c (p - q) = 0
[PROOF STEP]
by (metis diff_self smult_diff_right)
[PROOF STATE]
proof (state)
this:
smult c (p - q) = 0

goal (1 subgoal):
 1. p = q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
smult c (p - q) = 0

goal (1 subgoal):
 1. p = q
[PROOF STEP]
using \<open>c\<noteq>0\<close>
[PROOF STATE]
proof (prove)
using this:
smult c (p - q) = 0
c \<noteq> (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed