[STATEMENT]
theorem ccomp_bigstep:
 "(c, s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c), t, stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c, s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c), t, stk)
[PROOF STEP]
proof (induction arbitrary: stk rule: big_step_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>x a s stk. ccomp (x ::= a) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (x ::= a)), s(x := aval a s), stk)
 3. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 4. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 6. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 7. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
case (Assign x a s)
[PROOF STATE]
proof (state)
this:

goal (7 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>x a s stk. ccomp (x ::= a) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (x ::= a)), s(x := aval a s), stk)
 3. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 4. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 6. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 7. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp (x ::= a) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (x ::= a)), s(x := aval a s), stk)
[PROOF STEP]
by (fastforce simp: fun_upd_def cong: if_cong)
[PROOF STATE]
proof (state)
this:
ccomp (x ::= a) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (x ::= a)), s(x := aval a s), stk)

goal (6 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 3. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 6. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 3. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 6. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
case (Seq c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3)
[PROOF STATE]
proof (state)
this:
(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2
(c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3
ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, ?stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, ?stk)
ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, ?stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, ?stk)

goal (6 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 3. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 6. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
let ?cc\<^sub>1 = "ccomp c\<^sub>1"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 3. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 6. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
let ?cc\<^sub>2 = "ccomp c\<^sub>2"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 3. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 6. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
have "?cc\<^sub>1 @ ?cc\<^sub>2 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size ?cc\<^sub>1, s\<^sub>2, stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk)
[PROOF STEP]
using Seq.IH(1)
[PROOF STATE]
proof (prove)
using this:
ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, ?stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, ?stk)

goal (1 subgoal):
 1. ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk)

goal (6 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 3. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 6. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk)

goal (6 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 3. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 6. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
have "?cc\<^sub>1 @ ?cc\<^sub>2 \<turnstile> (size ?cc\<^sub>1, s\<^sub>2, stk) \<rightarrow>*
    (size (?cc\<^sub>1 @ ?cc\<^sub>2), s\<^sub>3, stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (size (ccomp c\<^sub>1), s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>1 @ ccomp c\<^sub>2), s\<^sub>3, stk)
[PROOF STEP]
using Seq.IH(2)
[PROOF STATE]
proof (prove)
using this:
ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, ?stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, ?stk)

goal (1 subgoal):
 1. ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (size (ccomp c\<^sub>1), s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>1 @ ccomp c\<^sub>2), s\<^sub>3, stk)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (size (ccomp c\<^sub>1), s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>1 @ ccomp c\<^sub>2), s\<^sub>3, stk)

goal (6 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3 stk. \<lbrakk>(c\<^sub>1, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk); (c\<^sub>2, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>2), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
 3. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 5. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 6. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk)
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (size (ccomp c\<^sub>1), s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>1 @ ccomp c\<^sub>2), s\<^sub>3, stk)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c\<^sub>1), s\<^sub>2, stk)
ccomp c\<^sub>1 @ ccomp c\<^sub>2 \<turnstile> (size (ccomp c\<^sub>1), s\<^sub>2, stk) \<rightarrow>* (size (ccomp c\<^sub>1 @ ccomp c\<^sub>2), s\<^sub>3, stk)

goal (1 subgoal):
 1. ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)
[PROOF STEP]
by simp (blast intro: star_trans)
[PROOF STATE]
proof (state)
this:
ccomp (c\<^sub>1;; c\<^sub>2) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (c\<^sub>1;; c\<^sub>2)), s\<^sub>3, stk)

goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
case (WhileTrue b s\<^sub>1 c s\<^sub>2 s\<^sub>3)
[PROOF STATE]
proof (state)
this:
bval b s\<^sub>1
(c, s\<^sub>1) \<Rightarrow> s\<^sub>2
(WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3
ccomp c \<turnstile> (0, s\<^sub>1, ?stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, ?stk)
ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, ?stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, ?stk)

goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
let ?cc = "ccomp c"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
let ?cb = "bcomp (b, False, size ?cc + 1)"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
let ?cw = "ccomp (WHILE b DO c)"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
have "?cw \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size ?cb, s\<^sub>1, stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk)
[PROOF STEP]
using \<open>bval b s\<^sub>1\<close>
[PROOF STATE]
proof (prove)
using this:
bval b s\<^sub>1

goal (1 subgoal):
 1. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk)

goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk)

goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
have "?cw \<turnstile> (size ?cb, s\<^sub>1, stk) \<rightarrow>* (size ?cb + size ?cc, s\<^sub>2, stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk)
[PROOF STEP]
using WhileTrue.IH(1)
[PROOF STATE]
proof (prove)
using this:
ccomp c \<turnstile> (0, s\<^sub>1, ?stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, ?stk)

goal (1 subgoal):
 1. ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk)

goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk)

goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
have "?cw \<turnstile> (size ?cb + size ?cc, s\<^sub>2, stk) \<rightarrow>* (0, s\<^sub>2, stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk) \<rightarrow>* (0, s\<^sub>2, stk)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk) \<rightarrow>* (0, s\<^sub>2, stk)

goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk) \<rightarrow>* (0, s\<^sub>2, stk)

goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
have "?cw \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size ?cw, s\<^sub>3, stk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
by (rule WhileTrue.IH(2))
[PROOF STATE]
proof (state)
this:
ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)

goal (5 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
 5. \<And>b s\<^sub>1 c s\<^sub>2 s\<^sub>3 stk. \<lbrakk>bval b s\<^sub>1; (c, s\<^sub>1) \<Rightarrow> s\<^sub>2; \<And>stk. ccomp c \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, stk); (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3; \<And>stk. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)\<rbrakk> \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk)
ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk)
ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk) \<rightarrow>* (0, s\<^sub>2, stk)
ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk)
ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)), s\<^sub>1, stk) \<rightarrow>* (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk)
ccomp (WHILE b DO c) \<turnstile> (size (bcomp (b, False, size (ccomp c) + 1)) + size (ccomp c), s\<^sub>2, stk) \<rightarrow>* (0, s\<^sub>2, stk)
ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)

goal (1 subgoal):
 1. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
[PROOF STEP]
by (blast intro: star_trans)
[PROOF STATE]
proof (state)
this:
ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)

goal (4 subgoals):
 1. \<And>s stk. ccomp SKIP \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp SKIP), s, stk)
 2. \<And>b s c\<^sub>1 t c\<^sub>2 stk. \<lbrakk>bval b s; (c\<^sub>1, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>1 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>1), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 3. \<And>b s c\<^sub>2 t c\<^sub>1 stk. \<lbrakk>\<not> bval b s; (c\<^sub>2, s) \<Rightarrow> t; \<And>stk. ccomp c\<^sub>2 \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp c\<^sub>2), t, stk)\<rbrakk> \<Longrightarrow> ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2)), t, stk)
 4. \<And>b s c stk. \<not> bval b s \<Longrightarrow> ccomp (WHILE b DO c) \<turnstile> (0, s, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s, stk)
[PROOF STEP]
qed fastforce+


[STATEMENT]
lemma impCE2 [elim!]:
 "\<lbrakk>P \<longrightarrow> Q; \<not> P \<Longrightarrow> R; P \<Longrightarrow> Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<longrightarrow> Q; \<not> P \<Longrightarrow> R; \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
by blast


[STATEMENT]
lemma Suc_lessI2 [intro!]:
 "\<lbrakk>m < n; m \<noteq> n - 1\<rbrakk> \<Longrightarrow> Suc m < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < n; m \<noteq> n - 1\<rbrakk> \<Longrightarrow> Suc m < n
[PROOF STEP]
by simp


[STATEMENT]
lemma vwalkI_subgraph:
  assumes "vwalk p H"
  assumes "subgraph H G"
  shows "vwalk p G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwalk p G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. set p \<subseteq> verts G
 2. set (vwalk_arcs p) \<subseteq> arcs_ends G
 3. p \<noteq> []
[PROOF STEP]
show "set p \<subseteq> verts G" and "p \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set p \<subseteq> verts G &&& p \<noteq> []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwalk p H
subgraph H G

goal (1 subgoal):
 1. set p \<subseteq> verts G &&& p \<noteq> []
[PROOF STEP]
by (auto simp add: subgraph_def vwalk_def)
[PROOF STATE]
proof (state)
this:
set p \<subseteq> verts G
p \<noteq> []

goal (1 subgoal):
 1. set (vwalk_arcs p) \<subseteq> arcs_ends G
[PROOF STEP]
have "set (vwalk_arcs p) \<subseteq> arcs_ends H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (vwalk_arcs p) \<subseteq> arcs_ends H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vwalk p H
subgraph H G

goal (1 subgoal):
 1. set (vwalk_arcs p) \<subseteq> arcs_ends H
[PROOF STEP]
by (simp add: vwalk_def)
[PROOF STATE]
proof (state)
this:
set (vwalk_arcs p) \<subseteq> arcs_ends H

goal (1 subgoal):
 1. set (vwalk_arcs p) \<subseteq> arcs_ends G
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (vwalk_arcs p) \<subseteq> arcs_ends H

goal (1 subgoal):
 1. set (vwalk_arcs p) \<subseteq> arcs_ends G
[PROOF STEP]
have "\<dots> \<subseteq> arcs_ends G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arcs_ends H \<subseteq> arcs_ends G
[PROOF STEP]
using \<open>subgraph H G\<close>
[PROOF STATE]
proof (prove)
using this:
subgraph H G

goal (1 subgoal):
 1. arcs_ends H \<subseteq> arcs_ends G
[PROOF STEP]
by (rule arcs_ends_mono)
[PROOF STATE]
proof (state)
this:
arcs_ends H \<subseteq> arcs_ends G

goal (1 subgoal):
 1. set (vwalk_arcs p) \<subseteq> arcs_ends G
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set (vwalk_arcs p) \<subseteq> arcs_ends G
[PROOF STEP]
show "set (vwalk_arcs p) \<subseteq> arcs_ends G"
[PROOF STATE]
proof (prove)
using this:
set (vwalk_arcs p) \<subseteq> arcs_ends G

goal (1 subgoal):
 1. set (vwalk_arcs p) \<subseteq> arcs_ends G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set (vwalk_arcs p) \<subseteq> arcs_ends G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vpathI_subgraph:
  assumes "vpath p G"
  assumes "subgraph G H"
  shows "vpath p H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vpath p H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vpath p G
subgraph G H

goal (1 subgoal):
 1. vpath p H
[PROOF STEP]
by (auto intro: vwalkI_subgraph)


[STATEMENT]
lemma (in loopfree_digraph) vpathI_arc:
  assumes "(a,b) \<in> arcs_ends G"
  shows "vpath [a,b] G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vpath [a, b] G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<rightarrow> b

goal (1 subgoal):
 1. vpath [a, b] G
[PROOF STEP]
by (intro vpathI vwalkI) (auto intro: adj_in_verts adj_not_same)


[STATEMENT]
lemma node_ptr_kinds_M_eq:
  assumes "|h \<turnstile> object_ptr_kinds_M|\<^sub>r = |h' \<turnstile> object_ptr_kinds_M|\<^sub>r"
  shows "|h \<turnstile> node_ptr_kinds_M|\<^sub>r = |h' \<turnstile> node_ptr_kinds_M|\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |h \<turnstile> node_ptr_kinds_M|\<^sub>r = |h' \<turnstile> node_ptr_kinds_M|\<^sub>r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
|h \<turnstile> object_ptr_kinds_M|\<^sub>r = |h' \<turnstile> object_ptr_kinds_M|\<^sub>r

goal (1 subgoal):
 1. |h \<turnstile> node_ptr_kinds_M|\<^sub>r = |h' \<turnstile> node_ptr_kinds_M|\<^sub>r
[PROOF STEP]
by(auto simp add: node_ptr_kinds_M_defs object_ptr_kinds_M_defs node_ptr_kinds_def)


[STATEMENT]
lemma node_ptr_kinds_M_reads:
  "reads (\<Union>object_ptr. {preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing)}) node_ptr_kinds_M h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reads (\<Union>object_ptr. {preserved (get_M object_ptr RObject.nothing)}) node_ptr_kinds_M h h'
[PROOF STEP]
using object_ptr_kinds_M_reads
[PROOF STATE]
proof (prove)
using this:
reads (\<Union>object_ptr. {preserved (get_M object_ptr RObject.nothing)}) object_ptr_kinds_M ?h ?h'

goal (1 subgoal):
 1. reads (\<Union>object_ptr. {preserved (get_M object_ptr RObject.nothing)}) node_ptr_kinds_M h h'
[PROOF STEP]
apply (simp add: reads_def node_ptr_kinds_M_defs node_ptr_kinds_def
      object_ptr_kinds_M_reads preserved_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h h'. (\<forall>y. h \<turnstile> get_M y RObject.nothing \<rightarrow>\<^sub>r () = h' \<turnstile> get_M y RObject.nothing \<rightarrow>\<^sub>r ()) \<longrightarrow> (\<forall>x. (x = sorted_list_of_set (fset (object_ptr_kinds h))) = (x = sorted_list_of_set (fset (object_ptr_kinds h'))))) \<Longrightarrow> (\<forall>y. h \<turnstile> get_M y RObject.nothing \<rightarrow>\<^sub>r () = h' \<turnstile> get_M y RObject.nothing \<rightarrow>\<^sub>r ()) \<longrightarrow> (\<forall>x. (sorted_list_of_set ((\<lambda>x. the (cast x)) ` (Collect is_node_ptr_kind \<inter> fset (object_ptr_kinds h))) = x) = (sorted_list_of_set ((\<lambda>x. the (cast x)) ` (Collect is_node_ptr_kind \<inter> fset (object_ptr_kinds h'))) = x))
[PROOF STEP]
by (smt object_ptr_kinds_preserved_small preserved_def unit_all_impI)


[STATEMENT]
lemma get_M_Object_preserved1 [simp]:
  "(\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)) \<Longrightarrow> h \<turnstile> put_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr setter v \<rightarrow>\<^sub>h h'
    \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
apply(cases "cast node_ptr = object_ptr")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; cast node_ptr = object_ptr\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
 2. \<lbrakk>\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; cast node_ptr \<noteq> object_ptr\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
by(auto simp add: put_M_defs get_M_defs ObjectMonad.get_M_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def preserved_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def
      bind_eq_Some_conv
      split: option.splits)


[STATEMENT]
lemma get_M_Object_preserved2 [simp]:
  "cast node_ptr \<noteq> object_ptr \<Longrightarrow> h \<turnstile> put_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr setter v \<rightarrow>\<^sub>h h'
    \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cast node_ptr \<noteq> object_ptr; h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
by(auto simp add: put_M_defs get_M_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def ObjectMonad.get_M_defs preserved_def
      split: option.splits dest: get_heap_E)


[STATEMENT]
lemma get_M_Object_preserved3 [simp]:
  "h \<turnstile> put_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr setter v \<rightarrow>\<^sub>h h' \<Longrightarrow> (\<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x))
    \<Longrightarrow> preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x)\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
apply(cases "cast node_ptr \<noteq> object_ptr")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); cast node_ptr \<noteq> object_ptr\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
 2. \<lbrakk>h \<turnstile> put_M node_ptr setter v \<rightarrow>\<^sub>h h'; \<And>x. getter (cast (setter (\<lambda>_. v) x)) = getter (cast x); \<not> cast node_ptr \<noteq> object_ptr\<rbrakk> \<Longrightarrow> preserved (get_M object_ptr getter) h h'
[PROOF STEP]
by(auto simp add: put_M_defs get_M_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def ObjectMonad.get_M_defs preserved_def
      split: option.splits bind_splits dest: get_heap_E)


[STATEMENT]
lemma get_M_Object_preserved4 [simp]:
  "cast node_ptr \<noteq> object_ptr \<Longrightarrow> h \<turnstile> put_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr setter v \<rightarrow>\<^sub>h h'
      \<Longrightarrow> preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr getter) h h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cast node_ptr \<noteq> object_ptr; h \<turnstile> put_M object_ptr setter v \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> preserved (get_M node_ptr getter) h h'
[PROOF STEP]
by(auto simp add: ObjectMonad.put_M_defs get_M_defs get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def ObjectMonad.get_M_defs preserved_def
      split: option.splits dest: get_heap_E)


[STATEMENT]
lemma get_node_ptr_simp [simp]:
  "get\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h) = (if ptr = cast node_ptr then cast obj else get node_ptr h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get node_ptr (put ptr obj h) = (if ptr = cast node_ptr then cast obj else get node_ptr h)
[PROOF STEP]
by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)


[STATEMENT]
lemma node_ptr_kinds_simp [simp]:
  "node_ptr_kinds (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)
                = node_ptr_kinds h |\<union>| (if is_node_ptr_kind ptr then {|the (cast ptr)|} else {||})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. node_ptr_kinds (put ptr obj h) = node_ptr_kinds h |\<union>| (if is_node_ptr_kind ptr then {|the (cast ptr)|} else {||})
[PROOF STEP]
by(auto simp add: node_ptr_kinds_def)


[STATEMENT]
lemma type_wf_put_I:
  assumes "type_wf h"
  assumes "ObjectClass.type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
  assumes "is_node_ptr_kind ptr \<Longrightarrow> is_node_kind obj"
  shows "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf (put ptr obj h)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
NodeClass.type_wf h
ObjectClass.type_wf (put ptr obj h)
is_node_ptr_kind ptr \<Longrightarrow> is_node_kind obj

goal (1 subgoal):
 1. NodeClass.type_wf (put ptr obj h)
[PROOF STEP]
apply(auto simp add: type_wf_defs split: option.splits)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ObjectClass.type_wf (put ptr obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; is_node_ptr_kind ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
 2. \<And>node_ptr. \<lbrakk>ObjectClass.type_wf (put (cast node_ptr) obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h; ptr = cast node_ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
[PROOF STEP]
using cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none is_node_kind_def
[PROOF STATE]
proof (prove)
using this:
(cast ?obj = None) = (\<nexists>node. cast node = ?obj)
is_node_kind ?ptr = (cast ?ptr \<noteq> None)

goal (2 subgoals):
 1. \<lbrakk>ObjectClass.type_wf (put ptr obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; is_node_ptr_kind ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
 2. \<And>node_ptr. \<lbrakk>ObjectClass.type_wf (put (cast node_ptr) obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h; ptr = cast node_ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>node_ptr. \<lbrakk>ObjectClass.type_wf (put (cast node_ptr) obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h; ptr = cast node_ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
[PROOF STEP]
using cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>N\<^sub>o\<^sub>d\<^sub>e_none is_node_kind_def
[PROOF STATE]
proof (prove)
using this:
(cast ?obj = None) = (\<nexists>node. cast node = ?obj)
is_node_kind ?ptr = (cast ?ptr \<noteq> None)

goal (1 subgoal):
 1. \<And>node_ptr. \<lbrakk>ObjectClass.type_wf (put (cast node_ptr) obj h); is_node_kind obj; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h; ptr = cast node_ptr\<rbrakk> \<Longrightarrow> \<exists>y. cast y = obj
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma type_wf_put_ptr_not_in_heap_E:
  assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
  assumes "ptr |\<notin>| object_ptr_kinds h"
  shows "type_wf h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
NodeClass.type_wf (put ptr obj h)
ptr |\<notin>| object_ptr_kinds h

goal (1 subgoal):
 1. NodeClass.type_wf h
[PROOF STEP]
by(auto simp add: type_wf_defs elim!: ObjectMonad.type_wf_put_ptr_not_in_heap_E
      split: option.splits if_splits)


[STATEMENT]
lemma type_wf_put_ptr_in_heap_E:
  assumes "type_wf (put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr obj h)"
  assumes "ptr |\<in>| object_ptr_kinds h"
  assumes "ObjectClass.type_wf h"
  assumes "is_node_ptr_kind ptr \<Longrightarrow> is_node_kind (the (get ptr h))"
  shows "type_wf h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
NodeClass.type_wf (put ptr obj h)
ptr |\<in>| object_ptr_kinds h
ObjectClass.type_wf h
is_node_ptr_kind ptr \<Longrightarrow> is_node_kind (the (get ptr h))

goal (1 subgoal):
 1. NodeClass.type_wf h
[PROOF STEP]
apply(auto simp add: type_wf_defs split: option.splits if_splits)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y node_ptr. \<lbrakk>ptr |\<in>| object_ptr_kinds h; ObjectClass.type_wf h; is_node_kind (the (get ptr h)); is_node_ptr_kind ptr; ObjectClass.type_wf (put ptr (cast y) h); \<forall>node_ptr\<in>fset (node_ptr_kinds h). ptr = cast node_ptr \<or> (\<exists>y. get node_ptr h = Some y); obj = cast y; node_ptr |\<in>| node_ptr_kinds h\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h = Some y
[PROOF STEP]
by (metis ObjectClass.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf bind.bind_lunit finite_set_in get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def is_node_kind_def option.exhaust_sel)


[STATEMENT]
lemma node_ptr_kinds_small:
  assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
  shows "node_ptr_kinds h = node_ptr_kinds h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. node_ptr_kinds h = node_ptr_kinds h'
[PROOF STEP]
by(simp add: node_ptr_kinds_def preserved_def object_ptr_kinds_preserved_small[OF assms])


[STATEMENT]
lemma node_ptr_kinds_preserved:
  assumes "writes SW setter h h'"
  assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
  assumes "\<And>h h'. \<forall>w \<in> SW. h \<turnstile> w \<rightarrow>\<^sub>h h'
            \<longrightarrow> (\<forall>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h')"
  shows "node_ptr_kinds h = node_ptr_kinds h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. node_ptr_kinds h = node_ptr_kinds h'
[PROOF STEP]
using writes_small_big[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reflp (\<lambda>h h'. \<forall>w\<in>SW. ?h4 h h' \<turnstile> w \<rightarrow>\<^sub>h ?h'5 h h' \<longrightarrow> (\<forall>object_ptr. preserved (get_M object_ptr RObject.nothing) (?h4 h h') (?h'5 h h'))); transp (\<lambda>h h'. \<forall>w\<in>SW. ?h4 h h' \<turnstile> w \<rightarrow>\<^sub>h ?h'5 h h' \<longrightarrow> (\<forall>object_ptr. preserved (get_M object_ptr RObject.nothing) (?h4 h h') (?h'5 h h')))\<rbrakk> \<Longrightarrow> \<forall>w\<in>SW. ?h4 h h' \<turnstile> w \<rightarrow>\<^sub>h ?h'5 h h' \<longrightarrow> (\<forall>object_ptr. preserved (get_M object_ptr RObject.nothing) (?h4 h h') (?h'5 h h'))

goal (1 subgoal):
 1. node_ptr_kinds h = node_ptr_kinds h'
[PROOF STEP]
apply(simp add: reflp_def transp_def preserved_def node_ptr_kinds_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ha h'a. \<lbrakk>\<forall>x. (\<exists>w\<in>SW. ha x x \<turnstile> w \<rightarrow>\<^sub>h h'a x x) \<longrightarrow> (\<forall>object_ptr. ha x x \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a x x \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ()); \<forall>x y. ((\<exists>w\<in>SW. ha x y \<turnstile> w \<rightarrow>\<^sub>h h'a x y) \<longrightarrow> (\<forall>object_ptr. ha x y \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a x y \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ())) \<longrightarrow> (\<forall>z. ((\<exists>w\<in>SW. ha y z \<turnstile> w \<rightarrow>\<^sub>h h'a y z) \<longrightarrow> (\<forall>object_ptr. ha y z \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a y z \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ())) \<longrightarrow> (\<exists>w\<in>SW. ha x z \<turnstile> w \<rightarrow>\<^sub>h h'a x z) \<longrightarrow> (\<forall>object_ptr. ha x z \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a x z \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ()))\<rbrakk> \<Longrightarrow> (\<exists>w\<in>SW. ha h h' \<turnstile> w \<rightarrow>\<^sub>h h'a h h') \<longrightarrow> (\<forall>object_ptr. ha h h' \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r () = h'a h h' \<turnstile> get_M object_ptr RObject.nothing \<rightarrow>\<^sub>r ())) \<Longrightarrow> (the \<circ> cast) |`| ffilter is_node_ptr_kind (object_ptr_kinds h) = (the \<circ> cast) |`| ffilter is_node_ptr_kind (object_ptr_kinds h')
[PROOF STEP]
by (metis assms object_ptr_kinds_preserved)


[STATEMENT]
lemma type_wf_preserved_small:
  assumes "\<And>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
  assumes "\<And>node_ptr. preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr RNode.nothing) h h'"
  shows "type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
using type_wf_preserved allI[OF assms(2), of id, simplified]
[PROOF STATE]
proof (prove)
using this:
ObjectClass.type_wf ?h = ObjectClass.type_wf ?h'
\<forall>x. preserved (get_M x RNode.nothing) h h'

goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
apply(auto simp add: type_wf_defs)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>node_ptr. \<lbrakk>\<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'; \<forall>x. preserved (get_M x RNode.nothing) h h'; ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h'\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h' = Some y
 2. \<And>node_ptr. \<lbrakk>\<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'; \<forall>x. preserved (get_M x RNode.nothing) h h'; ObjectClass.type_wf h'; \<forall>node_ptr\<in>fset (node_ptr_kinds h'). \<exists>y. get node_ptr h' = Some y; node_ptr |\<in>| node_ptr_kinds h\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h = Some y
[PROOF STEP]
apply(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)]
      split: option.splits)[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>node_ptr. \<lbrakk>\<forall>x. ((\<exists>y. get x h = Some y) \<or> get x h' = None) \<and> (get x h = None \<or> (\<exists>y. get x h' = Some y)); ObjectClass.type_wf h; \<forall>node_ptr\<in>fset (node_ptr_kinds h'). \<exists>y. get node_ptr h = Some y; node_ptr |\<in>| node_ptr_kinds h'; \<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h' = Some y
 2. \<And>node_ptr. \<lbrakk>\<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'; \<forall>x. preserved (get_M x RNode.nothing) h h'; ObjectClass.type_wf h'; \<forall>node_ptr\<in>fset (node_ptr_kinds h'). \<exists>y. get node_ptr h' = Some y; node_ptr |\<in>| node_ptr_kinds h\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h = Some y
[PROOF STEP]
apply (metis notin_fset option.simps(3))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>node_ptr. \<lbrakk>\<And>h h'. ObjectClass.type_wf h = ObjectClass.type_wf h'; \<forall>x. preserved (get_M x RNode.nothing) h h'; ObjectClass.type_wf h'; \<forall>node_ptr\<in>fset (node_ptr_kinds h'). \<exists>y. get node_ptr h' = Some y; node_ptr |\<in>| node_ptr_kinds h\<rbrakk> \<Longrightarrow> \<exists>y. get node_ptr h = Some y
[PROOF STEP]
by(auto simp add: preserved_def get_M_defs node_ptr_kinds_small[OF assms(1)]
      split: option.splits, force)[1]


[STATEMENT]
lemma type_wf_preserved:
  assumes "writes SW setter h h'"
  assumes "h \<turnstile> setter \<rightarrow>\<^sub>h h'"
  assumes "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h'
           \<Longrightarrow> \<forall>object_ptr. preserved (get_M\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t object_ptr RObject.nothing) h h'"
  assumes "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h'
           \<Longrightarrow> \<forall>node_ptr. preserved (get_M\<^sub>N\<^sub>o\<^sub>d\<^sub>e node_ptr RNode.nothing) h h'"
  shows "type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
have "\<And>h h' w. w \<in> SW \<Longrightarrow> h \<turnstile> w \<rightarrow>\<^sub>h h' \<Longrightarrow> type_wf h = type_wf h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
using assms type_wf_preserved_small
[PROOF STATE]
proof (prove)
using this:
writes SW setter h h'
h \<turnstile> setter \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> \<forall>object_ptr. preserved (get_M object_ptr RObject.nothing) ?h ?h'
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> \<forall>node_ptr. preserved (get_M node_ptr RNode.nothing) ?h ?h'
\<lbrakk>\<And>object_ptr. preserved (get_M object_ptr RObject.nothing) ?h ?h'; \<And>node_ptr. preserved (get_M node_ptr RNode.nothing) ?h ?h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf ?h = NodeClass.type_wf ?h'

goal (1 subgoal):
 1. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf ?h = NodeClass.type_wf ?h'

goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
with assms(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
writes SW setter h h'
h \<turnstile> setter \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf ?h = NodeClass.type_wf ?h'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
writes SW setter h h'
h \<turnstile> setter \<rightarrow>\<^sub>h h'
\<lbrakk>?w \<in> SW; ?h \<turnstile> ?w \<rightarrow>\<^sub>h ?h'\<rbrakk> \<Longrightarrow> NodeClass.type_wf ?h = NodeClass.type_wf ?h'

goal (1 subgoal):
 1. NodeClass.type_wf h = NodeClass.type_wf h'
[PROOF STEP]
apply(rule writes_small_big)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> ?w1 h h' w \<in> SW
 2. \<And>h h' w. \<lbrakk>w \<in> SW; h \<turnstile> w \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> h \<turnstile> ?w1 h h' w \<rightarrow>\<^sub>h h'
 3. reflp (\<lambda>h h'. NodeClass.type_wf h = NodeClass.type_wf h')
 4. transp (\<lambda>h h'. NodeClass.type_wf h = NodeClass.type_wf h')
[PROOF STEP]
by(auto simp add: reflp_def transp_def)
[PROOF STATE]
proof (state)
this:
NodeClass.type_wf h = NodeClass.type_wf h'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reverseN_drop: "reverseN n xs acc = drop (length xs - n) (rev xs) @ acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reverseN n xs acc = drop (length xs - n) (rev xs) @ acc
[PROOF STEP]
unfolding reverseN_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev (take n xs) @ acc = drop (length xs - n) (rev xs) @ acc
[PROOF STEP]
using rev_take
[PROOF STATE]
proof (prove)
using this:
rev (take ?i ?xs) = drop (length ?xs - ?i) (rev ?xs)

goal (1 subgoal):
 1. rev (take n xs) @ acc = drop (length xs - n) (rev xs) @ acc
[PROOF STEP]
by blast


[STATEMENT]
lemma reverseN_step: "xs \<noteq> [] \<Longrightarrow> reverseN n (tl xs) (hd xs # acc) = reverseN (Suc n) xs acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> reverseN n (tl xs) (hd xs # acc) = reverseN (Suc n) xs acc
[PROOF STEP]
by (simp add: take_Suc)


[STATEMENT]
lemma reverseN_finish: "reverseN n [] acc = acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reverseN n [] acc = acc
[PROOF STEP]
by (simp)


[STATEMENT]
lemma reverseN_tl_hd: "0 < n \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> reverseN n xs ys = reverseN (n - (Suc 0)) (tl xs) (hd xs #ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; xs \<noteq> []\<rbrakk> \<Longrightarrow> reverseN n xs ys = reverseN (n - Suc 0) (tl xs) (hd xs # ys)
[PROOF STEP]
by (simp add: reverseN_step del: reverseN_def)


[STATEMENT]
lemma reverseN_nth: "n < length xs \<Longrightarrow> x = xs ! n \<Longrightarrow> x # reverseN n xs ys = reverseN (Suc n) xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; x = xs ! n\<rbrakk> \<Longrightarrow> x # reverseN n xs ys = reverseN (Suc n) xs ys
[PROOF STEP]
by (simp add: take_Suc_conv_app_nth)


[STATEMENT]
lemma step_list [simp]: "invar common \<Longrightarrow> list (step common) = list common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar common \<Longrightarrow> Common.list (step common) = Common.list common
[PROOF STEP]
proof(induction common rule: step_state.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>current idle. invar (state.Idle current idle) \<Longrightarrow> Common.list (step (state.Idle current idle)) = Common.list (state.Idle current idle)
 2. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
case (1 idle)
[PROOF STATE]
proof (state)
this:
invar (state.Idle idle idle_)

goal (2 subgoals):
 1. \<And>current idle. invar (state.Idle current idle) \<Longrightarrow> Common.list (step (state.Idle current idle)) = Common.list (state.Idle current idle)
 2. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (state.Idle idle idle_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (state.Idle idle idle_)

goal (1 subgoal):
 1. Common.list (step (state.Idle idle idle_)) = Common.list (state.Idle idle idle_)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Common.list (step (state.Idle idle idle_)) = Common.list (state.Idle idle idle_)

goal (1 subgoal):
 1. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
case (2 current aux new moved)
[PROOF STATE]
proof (state)
this:
invar (Copy current aux new moved)

goal (1 subgoal):
 1. \<And>current aux new moved. invar (Copy current aux new moved) \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)

goal (1 subgoal):
 1. Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
proof(cases current)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>invar (Copy current aux new moved); current = Current x1 x2 x3 x4\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
case (Current extra added old remained)
[PROOF STATE]
proof (state)
this:
current = Current extra added old remained

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>invar (Copy current aux new moved); current = Current x1 x2 x3 x4\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
with 2
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
current = Current extra added old remained
[PROOF STEP]
have aux_not_empty: "aux \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)
current = Current extra added old remained

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

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>invar (Copy current aux new moved); current = Current x1 x2 x3 x4\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
from 2 Current
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
current = Current extra added old remained
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)
current = Current extra added old remained

goal (1 subgoal):
 1. Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
proof(cases "remained \<le> Suc moved")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>invar (Copy current aux new moved); current = Current extra added old remained; remained \<le> Suc moved\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
 2. \<lbrakk>invar (Copy current aux new moved); current = Current extra added old remained; \<not> remained \<le> Suc moved\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
remained \<le> Suc moved

goal (2 subgoals):
 1. \<lbrakk>invar (Copy current aux new moved); current = Current extra added old remained; remained \<le> Suc moved\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
 2. \<lbrakk>invar (Copy current aux new moved); current = Current extra added old remained; \<not> remained \<le> Suc moved\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
with 2 Current
[PROOF STATE]
proof (chain)
picking this:
invar (Copy current aux new moved)
current = Current extra added old remained
remained \<le> Suc moved
[PROOF STEP]
have "remained - length new = 1"
[PROOF STATE]
proof (prove)
using this:
invar (Copy current aux new moved)
current = Current extra added old remained
remained \<le> Suc moved

goal (1 subgoal):
 1. remained - length new = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
remained - length new = 1

goal (2 subgoals):
 1. \<lbrakk>invar (Copy current aux new moved); current = Current extra added old remained; remained \<le> Suc moved\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
 2. \<lbrakk>invar (Copy current aux new moved); current = Current extra added old remained; \<not> remained \<le> Suc moved\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
with True Current 2 aux_not_empty
[PROOF STATE]
proof (chain)
picking this:
remained \<le> Suc moved
current = Current extra added old remained
invar (Copy current aux new moved)
aux \<noteq> []
remained - length new = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
remained \<le> Suc moved
current = Current extra added old remained
invar (Copy current aux new moved)
aux \<noteq> []
remained - length new = 1

goal (1 subgoal):
 1. Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
by(auto simp: )
[PROOF STATE]
proof (state)
this:
Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)

goal (1 subgoal):
 1. \<lbrakk>invar (Copy current aux new moved); current = Current extra added old remained; \<not> remained \<le> Suc moved\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>invar (Copy current aux new moved); current = Current extra added old remained; \<not> remained \<le> Suc moved\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> remained \<le> Suc moved

goal (1 subgoal):
 1. \<lbrakk>invar (Copy current aux new moved); current = Current extra added old remained; \<not> remained \<le> Suc moved\<rbrakk> \<Longrightarrow> Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
with Current
[PROOF STATE]
proof (chain)
picking this:
current = Current extra added old remained
\<not> remained \<le> Suc moved
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
current = Current extra added old remained
\<not> remained \<le> Suc moved

goal (1 subgoal):
 1. Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)
[PROOF STEP]
by(auto simp: aux_not_empty reverseN_step Suc_diff_Suc simp del: reverseN_def)
[PROOF STATE]
proof (state)
this:
Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Common.list (step (Copy current aux new moved)) = Common.list (Copy current aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_list_current [simp]: "invar common \<Longrightarrow> list_current (step common) = list_current common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar common \<Longrightarrow> list_current (step common) = list_current common
[PROOF STEP]
by(cases common)(auto split: current.splits)


[STATEMENT]
lemma push_list [simp]: "list (push x common) = x # list common"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Common.list (Common.push x common) = x # Common.list common
[PROOF STEP]
proof(induction x common rule: push.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x current stack stackSize. Common.list (Common.push x (state.Idle current (idle.Idle stack stackSize))) = x # Common.list (state.Idle current (idle.Idle stack stackSize))
 2. \<And>x current aux new moved. Common.list (Common.push x (Copy current aux new moved)) = x # Common.list (Copy current aux new moved)
[PROOF STEP]
case (1 x stack stackSize)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x current stack stackSize. Common.list (Common.push x (state.Idle current (idle.Idle stack stackSize))) = x # Common.list (state.Idle current (idle.Idle stack stackSize))
 2. \<And>x current aux new moved. Common.list (Common.push x (Copy current aux new moved)) = x # Common.list (Copy current aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Common.list (Common.push x (state.Idle stack (idle.Idle stackSize stackSize_))) = x # Common.list (state.Idle stack (idle.Idle stackSize stackSize_))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Common.list (Common.push x (state.Idle stack (idle.Idle stackSize stackSize_))) = x # Common.list (state.Idle stack (idle.Idle stackSize stackSize_))

goal (1 subgoal):
 1. \<And>x current aux new moved. Common.list (Common.push x (Copy current aux new moved)) = x # Common.list (Copy current aux new moved)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x current aux new moved. Common.list (Common.push x (Copy current aux new moved)) = x # Common.list (Copy current aux new moved)
[PROOF STEP]
case (2 x current aux new moved)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>x current aux new moved. Common.list (Common.push x (Copy current aux new moved)) = x # Common.list (Copy current aux new moved)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Common.list (Common.push x (Copy current aux new moved)) = x # Common.list (Copy current aux new moved)
[PROOF STEP]
by(induction x current rule: Current.push.induct) auto
[PROOF STATE]
proof (state)
this:
Common.list (Common.push x (Copy current aux new moved)) = x # Common.list (Copy current aux new moved)

goal:
No subgoals!
[PROOF STEP]
qed