[STATEMENT]
lemma exec_move_Seq1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (e;;e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e;; e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
proof(rule ext iffI)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e;; e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e;; e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
fix ta h' s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e;; e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e;; e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
assume "?lhs ta h' s'"
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e;; e') h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e;; e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e;; e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compE2 e @ Pop # compE2 e') (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (e;; e') h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e @ Pop # compE2 e') (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e @ Pop # compE2 e') (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (e;; e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e;; e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
thus "?rhs ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ Pop # compE2 e') (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ Pop # compE2 e') (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
using pc
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ Pop # compE2 e') (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'
pc < length (compE2 e)

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(rule exec_meth_take_xt)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (e;; e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
qed(rule exec_move_SeqI1)


[STATEMENT]
lemma exec_move_SeqI2:
  assumes exec: "exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc' ,xcp')"
  shows "exec_move ci P t (e';;e) h (stk, loc, (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', (Suc (length (compE2 e') + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) ((compE2 e' @ [Pop]) @ compE2 e) (compxE2 e' 0 0 @ shift (length (compE2 e' @ [Pop])) (compxE2 e 0 0)) t h (stk, loc, (length ((compE2 e') @ [Pop]) + pc), xcp) ta h' (stk', loc', (length ((compE2 e') @ [Pop]) + pc'), xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ((compE2 e' @ [Pop]) @ compE2 e) (compxE2 e' 0 0 @ shift (length (compE2 e' @ [Pop])) (compxE2 e 0 0)) t h (stk, loc, length (compE2 e' @ [Pop]) + pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Pop]) + pc', xcp')
[PROOF STEP]
by(rule append_exec_meth_xt) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ((compE2 e' @ [Pop]) @ compE2 e) (compxE2 e' 0 0 @ shift (length (compE2 e' @ [Pop])) (compxE2 e 0 0)) t h (stk, loc, length (compE2 e' @ [Pop]) + pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Pop]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 e' @ [Pop]) @ compE2 e) (compxE2 e' 0 0 @ shift (length (compE2 e' @ [Pop])) (compxE2 e 0 0)) t h (stk, loc, length (compE2 e' @ [Pop]) + pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Pop]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
by(simp add: shift_compxE2 exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_Seq2:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (e';;e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta
                                h' (stk', loc', Suc (length (compE2 e') + pc'), xcp') =
         exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp') = exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
let ?E = "compE2 e' @ [Pop]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')

goal (2 subgoals):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (?E @ compE2 e) (compxE2 e' 0 0 @ shift (length ?E) (compxE2 e 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ((compE2 e' @ [Pop]) @ compE2 e) (compxE2 e' 0 0 @ shift (length (compE2 e' @ [Pop])) (compxE2 e 0 0)) t h (stk, loc, length (compE2 e' @ [Pop]) + pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Pop]) + pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ((compE2 e' @ [Pop]) @ compE2 e) (compxE2 e' 0 0 @ shift (length (compE2 e' @ [Pop])) (compxE2 e 0 0)) t h (stk, loc, length (compE2 e' @ [Pop]) + pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Pop]) + pc', xcp')

goal (2 subgoals):
 1. exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp') \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
from exec_meth_drop_xt[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>pcs (compxE2 e' 0 0) \<subseteq> {..<length (compE2 e' @ [Pop])}; jump_ok (compE2 e) 0 ?n\<rbrakk> \<Longrightarrow> exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Pop]) + pc' - length (compE2 e' @ [Pop]), xcp')
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pcs (compxE2 e' 0 0) \<subseteq> {..<length (compE2 e' @ [Pop])}; jump_ok (compE2 e) 0 ?n\<rbrakk> \<Longrightarrow> exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Pop]) + pc' - length (compE2 e' @ [Pop]), xcp')

goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>pcs (compxE2 e' 0 0) \<subseteq> {..<length (compE2 e' @ [Pop])}; jump_ok (compE2 e) 0 ?n\<rbrakk> \<Longrightarrow> exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Pop]) + pc' - length (compE2 e' @ [Pop]), xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (e';; e) h (stk, loc, Suc (length (compE2 e') + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e') + pc'), xcp')
[PROOF STEP]
qed(rule exec_move_SeqI2)


[STATEMENT]
lemma exec_move_CondI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (if (e) e1 else e2)) (compxE2 (if (e) e1 else e2) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_Cond1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
proof(rule ext iffI)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
let ?E = "IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
let ?xt = "compxE2 e1 (Suc 0) 0 @ compxE2 e2 (Suc (Suc (length (compE2 e1)))) 0"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
fix ta h' s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
assume "?lhs ta h' s'"
[PROOF STATE]
proof (state)
this:
exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
hence "exec_meth ci (compP2 P) (compE2 e @ ?E) (compxE2 e 0 0 @ shift (length (compE2 e)) ?xt) t h (stk, loc, pc, xcp) ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e1 (Suc 0) 0 @ compxE2 e2 (Suc (Suc (length (compE2 e1)))) 0)) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2 ac_simps)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e1 (Suc 0) 0 @ compxE2 e2 (Suc (Suc (length (compE2 e1)))) 0)) t h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
thus "?rhs ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e1 (Suc 0) 0 @ compxE2 e2 (Suc (Suc (length (compE2 e1)))) 0)) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e1 (Suc 0) 0 @ compxE2 e2 (Suc (Suc (length (compE2 e1)))) 0)) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
using pc
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e1 (Suc 0) 0 @ compxE2 e2 (Suc (Suc (length (compE2 e1)))) 0)) t h (stk, loc, pc, xcp) ta h' s'
pc < length (compE2 e)

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(rule exec_meth_take_xt)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
qed(rule exec_move_CondI1)


[STATEMENT]
lemma exec_move_CondI2:
  assumes exec: "exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (if (e) e1 else e2) h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', (Suc (length (compE2 e) + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) @ compE2 e1) @ Goto (1 + int (length (compE2 e2))) # compE2 e2) ((compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))])) (compxE2 e1 0 0)) @ (compxE2 e2 (Suc (Suc (length (compE2 e) + length (compE2 e1)))) 0)) t h (stk, loc, (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc), xcp) ta h' (stk', loc', (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc'), xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) @ compE2 e1) @ Goto (1 + int (length (compE2 e2))) # compE2 e2) ((compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))])) (compxE2 e1 0 0)) @ compxE2 e2 (Suc (Suc (length (compE2 e) + length (compE2 e1)))) 0) t h (stk, loc, length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc', xcp')
[PROOF STEP]
by -(rule exec_meth_append_xt, rule append_exec_meth_xt, auto)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) @ compE2 e1) @ Goto (1 + int (length (compE2 e2))) # compE2 e2) ((compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))])) (compxE2 e1 0 0)) @ compxE2 e2 (Suc (Suc (length (compE2 e) + length (compE2 e1)))) 0) t h (stk, loc, length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) @ compE2 e1) @ Goto (1 + int (length (compE2 e2))) # compE2 e2) ((compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))])) (compxE2 e1 0 0)) @ compxE2 e2 (Suc (Suc (length (compE2 e) + length (compE2 e1)))) 0) t h (stk, loc, length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
by(simp add: shift_compxE2 exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_Cond2:
  assumes pc: "pc < length (compE2 e1)"
  shows "exec_move ci P t (if (e) e1 else e2) h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', (Suc (length (compE2 e) + pc')), xcp') = exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') = exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
let ?E1 = "compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
let ?E2 = "Goto (1 + int (length (compE2 e2))) # compE2 e2"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')

goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (?E1 @ compE2 e1 @ ?E2) (compxE2 e 0 0 @ shift (length ?E1) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 (Suc 0) 0))) t h (stk, loc, length ?E1 + pc, xcp) ta h' (stk', loc', length ?E1 + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ((compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) @ compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))])) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 (Suc 0) 0))) t h (stk, loc, length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2 ac_simps)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ((compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) @ compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))])) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 (Suc 0) 0))) t h (stk, loc, length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc', xcp')

goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) @ compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))])) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 (Suc 0) 0))) t h (stk, loc, length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) @ compE2 e1 @ Goto (1 + int (length (compE2 e2))) # compE2 e2) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))])) (compxE2 e1 0 0 @ shift (length (compE2 e1)) (compxE2 e2 (Suc 0) 0))) t h (stk, loc, length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (2 + int (length (compE2 e1)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by -(rule exec_meth_take_xt,drule exec_meth_drop_xt,auto simp add: pc)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
qed(rule exec_move_CondI2)


[STATEMENT]
lemma exec_move_CondI3:
  assumes exec: "exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
let ?E = "compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
let ?xt = "compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (?E @ compE2 e2) (?xt @ shift (length ?E) (compxE2 e2 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ((compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) @ compE2 e2) ((compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0) @ shift (length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))])) (compxE2 e2 0 0)) t h (stk, loc, length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc', xcp')
[PROOF STEP]
by(rule append_exec_meth_xt) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ((compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) @ compE2 e2) ((compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0) @ shift (length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))])) (compxE2 e2 0 0)) t h (stk, loc, length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) @ compE2 e2) ((compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0) @ shift (length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))])) (compxE2 e2 0 0)) t h (stk, loc, length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
by(simp add: shift_compxE2 exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_Cond3:
  "exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta
                                      h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp') =
   exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp') = exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp') \<Longrightarrow> exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
let ?E = "compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp') \<Longrightarrow> exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
let ?xt = "compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp') \<Longrightarrow> exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')

goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp') \<Longrightarrow> exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) (?E @ compE2 e2) (?xt @ shift (length ?E) (compxE2 e2 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) ((compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) @ compE2 e2) ((compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0) @ shift (length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))])) (compxE2 e2 0 0)) t h (stk, loc, length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc', xcp')
[PROOF STEP]
by(simp add: shift_compxE2 exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) ((compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) @ compE2 e2) ((compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0) @ shift (length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))])) (compxE2 e2 0 0)) t h (stk, loc, length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc', xcp')

goal (2 subgoals):
 1. exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp') \<Longrightarrow> exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) @ compE2 e2) ((compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0) @ shift (length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))])) (compxE2 e2 0 0)) t h (stk, loc, length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) ((compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) @ compE2 e2) ((compxE2 e 0 0 @ compxE2 e1 (Suc (length (compE2 e))) 0) @ shift (length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))])) (compxE2 e2 0 0)) t h (stk, loc, length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ IfFalse (2 + int (length (compE2 e1))) # compE2 e1 @ [Goto (1 + int (length (compE2 e2)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e2) (compxE2 e2 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by -(drule exec_meth_drop_xt, auto)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t e2 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (if (e) e1 else e2) h (stk, loc, Suc (Suc (length (compE2 e) + length (compE2 e1) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + length (compE2 e1) + pc')), xcp')
[PROOF STEP]
qed(rule exec_move_CondI3)


[STATEMENT]
lemma exec_move_WhileI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (while (e) e') h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (while (e) e') h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (while (e) e')) (compxE2 (while (e) e') 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma (in ab_group_add) uminus_minus_left_commute:
  "- a - (b + c) = - b - (a + c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - a - (b + c) = - b - (a + c)
[PROOF STEP]
by (simp add: algebra_simps)


[STATEMENT]
lemma exec_move_While1:
  assumes pc: "pc < length (compE2 e)"
  shows "exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
proof(rule ext iffI)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
let ?E = "IfFalse (3 + int (length (compE2 e'))) # compE2 e' @ [Pop, Goto (- int (length (compE2 e)) + (-2 - int (length (compE2 e')))), Push Unit]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
let ?xt = "compxE2 e' (Suc 0) 0"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
fix ta h' s'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
assume "?lhs ta h' s'"
[PROOF STATE]
proof (state)
this:
exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e @ ?E) (compxE2 e 0 0 @ shift (length (compE2 e)) ?xt) t h (stk, loc, pc, xcp) ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e @ IfFalse (3 + int (length (compE2 e'))) # compE2 e' @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by (simp add: exec_move_def shift_compxE2 algebra_simps uminus_minus_left_commute)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e @ IfFalse (3 + int (length (compE2 e'))) # compE2 e' @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'

goal (2 subgoals):
 1. \<And>x xa xb. exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t e h (stk, loc, pc, xcp) x xa xb
 2. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
thus "?rhs ta h' s'"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ IfFalse (3 + int (length (compE2 e'))) # compE2 e' @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ IfFalse (3 + int (length (compE2 e'))) # compE2 e' @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
using pc
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e @ IfFalse (3 + int (length (compE2 e'))) # compE2 e' @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e)) (compxE2 e' (Suc 0) 0)) t h (stk, loc, pc, xcp) ta h' s'
pc < length (compE2 e)

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' s'
[PROOF STEP]
by(rule exec_meth_take_xt)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' s'

goal (1 subgoal):
 1. \<And>x xa xb. exec_move ci P t e h (stk, loc, pc, xcp) x xa xb \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, pc, xcp) x xa xb
[PROOF STEP]
qed(rule exec_move_WhileI1)


[STATEMENT]
lemma exec_move_WhileI2:
  assumes exec: "exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (while (e) e1) h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', (Suc (length (compE2 e) + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (while (e) e1) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (while (e) e1) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
let ?E = "compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (while (e) e1) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
let ?E' = "[Pop, Goto (- int (length (compE2 e)) + (-2 - int (length (compE2 e1)))), Push Unit]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (while (e) e1) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e1 h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (while (e) e1) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) ((?E @ compE2 e1) @ ?E') (compxE2 e 0 0 @ shift (length ?E) (compxE2 e1 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e1) (compxE2 e1 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]) @ compE2 e1) @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e1)))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (3 + int (length (compE2 e1)))])) (compxE2 e1 0 0)) t h (stk, loc, length (compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]) + pc', xcp')
[PROOF STEP]
by -(rule exec_meth_append, rule append_exec_meth_xt, auto)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]) @ compE2 e1) @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e1)))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (3 + int (length (compE2 e1)))])) (compxE2 e1 0 0)) t h (stk, loc, length (compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (while (e) e1) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]) @ compE2 e1) @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e1)))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (3 + int (length (compE2 e1)))])) (compxE2 e1 0 0)) t h (stk, loc, length (compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (3 + int (length (compE2 e1)))]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (while (e) e1) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
by (simp add: shift_compxE2 exec_move_def algebra_simps uminus_minus_left_commute)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (while (e) e1) h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_While2:
  assumes pc: "pc < length (compE2 e')"
  shows "exec_move ci P t (while (e) e') h (stk, loc, (Suc (length (compE2 e) + pc)), xcp) ta
                                    h' (stk', loc', (Suc (length (compE2 e) + pc')), xcp') =
         exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') = exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
let ?E = "compE2 e @ [IfFalse (3 + int (length (compE2 e')))]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
let ?E' = "[Pop, Goto (- int (length (compE2 e)) + (-2 - int (length (compE2 e')))), Push Unit]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')

goal (2 subgoals):
 1. exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) ((?E @ compE2 e') @ ?E') (compxE2 e 0 0 @ shift (length ?E) (compxE2 e' 0 0)) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) @ compE2 e') @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))])) (compxE2 e' 0 0)) t h (stk, loc, length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2 algebra_simps uminus_minus_left_commute)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) @ compE2 e') @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))])) (compxE2 e' 0 0)) t h (stk, loc, length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc', xcp')

goal (2 subgoals):
 1. exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) @ compE2 e') @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))])) (compxE2 e' 0 0)) t h (stk, loc, length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) @ compE2 e') @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))])) (compxE2 e' 0 0)) t h (stk, loc, length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e') (compxE2 e' 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
using pc
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) @ compE2 e') @ [Pop, Goto (- int (length (compE2 e)) + (- 2 - int (length (compE2 e')))), Push Unit]) (compxE2 e 0 0 @ shift (length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))])) (compxE2 e' 0 0)) t h (stk, loc, length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [IfFalse (3 + int (length (compE2 e')))]) + pc', xcp')
pc < length (compE2 e')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e') (compxE2 e' 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by -(drule exec_meth_take, simp, drule exec_meth_drop_xt, auto)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (while (e) e') h (stk, loc, Suc (length (compE2 e) + pc), xcp) ta h' (stk', loc', Suc (length (compE2 e) + pc'), xcp')
[PROOF STEP]
qed(rule exec_move_WhileI2)


[STATEMENT]
lemma exec_move_ThrowI:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (throw e) h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (throw e) h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (throw e)) (compxE2 (throw e) 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_Throw:
  "pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (throw e) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_move ci P t (throw e) h (stk, loc, pc, xcp) = exec_move ci P t e h (stk, loc, pc, xcp)
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pc < length (compE2 e) \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (throw e)) (compxE2 (throw e) 0 0) t h (stk, loc, pc, xcp) = exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp)
[PROOF STEP]
by(auto intro!: ext intro: exec_meth_take)


[STATEMENT]
lemma exec_move_TryI1:
  "exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (try e catch(C V) e') h s ta h' s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t e h s ta h' s' \<Longrightarrow> exec_move ci P t (try e catch(C V) e') h s ta h' s'
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h s ta h' s' \<Longrightarrow> exec_meth ci (compP2 P) (compE2 (try e catch(C V) e')) (compxE2 (try e catch(C V) e') 0 0) t h s ta h' s'
[PROOF STEP]
by auto


[STATEMENT]
lemma exec_move_TryI2:
  assumes exec: "exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  shows "exec_move ci P t (try e' catch(C V) e) h (stk, loc, Suc (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e') + pc')), xcp')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (try e' catch(C V) e) h (stk, loc, Suc (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e') + pc')), xcp')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (try e' catch(C V) e) h (stk, loc, Suc (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e') + pc')), xcp')
[PROOF STEP]
let ?e = "compE2 e' @ [Goto (int(size (compE2 e))+2), Store V]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. exec_move ci P t (try e' catch(C V) e) h (stk, loc, Suc (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e') + pc')), xcp')
[PROOF STEP]
from exec
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t e h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (try e' catch(C V) e) h (stk, loc, Suc (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e') + pc')), xcp')
[PROOF STEP]
hence "exec_meth ci (compP2 P) ((?e @ compE2 e) @ []) ((compxE2 e' 0 0 @ shift (length ?e) (compxE2 e 0 0)) @ [(0, length (compE2 e'), \<lfloor>C\<rfloor>, Suc (length (compE2 e')), 0)]) t h (stk, loc, (length ?e + pc), xcp) ta h' (stk', loc', (length ?e + pc'), xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (((compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V]) @ compE2 e) @ []) ((compxE2 e' 0 0 @ shift (length (compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V])) (compxE2 e 0 0)) @ [(0, length (compE2 e'), \<lfloor>C\<rfloor>, Suc (length (compE2 e')), 0)]) t h (stk, loc, length (compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V]) + pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V]) + pc', xcp')
[PROOF STEP]
by(rule exec_meth_append_xt[OF append_exec_meth_xt]) auto
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (((compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V]) @ compE2 e) @ []) ((compxE2 e' 0 0 @ shift (length (compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V])) (compxE2 e 0 0)) @ [(0, length (compE2 e'), \<lfloor>C\<rfloor>, Suc (length (compE2 e')), 0)]) t h (stk, loc, length (compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V]) + pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (try e' catch(C V) e) h (stk, loc, Suc (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e') + pc')), xcp')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V]) @ compE2 e) @ []) ((compxE2 e' 0 0 @ shift (length (compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V])) (compxE2 e 0 0)) @ [(0, length (compE2 e'), \<lfloor>C\<rfloor>, Suc (length (compE2 e')), 0)]) t h (stk, loc, length (compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V]) + pc, xcp) ta h' (stk', loc', length (compE2 e' @ [Goto (int (length (compE2 e)) + 2), Store V]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t (try e' catch(C V) e) h (stk, loc, Suc (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e') + pc')), xcp')
[PROOF STEP]
by(simp add: eval_nat_numeral shift_compxE2 exec_move_def)
[PROOF STATE]
proof (state)
this:
exec_move ci P t (try e' catch(C V) e) h (stk, loc, Suc (Suc (length (compE2 e') + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e') + pc')), xcp')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_move_Try2:
  "exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta
                                     h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp') =
   exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')"
  (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp') = exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')
[PROOF STEP]
let ?E = "compE2 e @ [Goto (int(size (compE2 e'))+2), Store V]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')
[PROOF STEP]
let ?xt = "[(0, length (compE2 e), \<lfloor>C\<rfloor>, Suc (length (compE2 e)), 0)]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')
[PROOF STEP]
assume lhs: ?lhs
[PROOF STATE]
proof (state)
this:
exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')

goal (2 subgoals):
 1. exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')
[PROOF STEP]
hence pc: "pc < length (compE2 e')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')

goal (1 subgoal):
 1. pc < length (compE2 e')
[PROOF STEP]
by(fastforce elim!: exec_meth.cases simp add: exec_move_def match_ex_table_append match_ex_entry dest: match_ex_table_pcsD)
[PROOF STATE]
proof (state)
this:
pc < length (compE2 e')

goal (2 subgoals):
 1. exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')
[PROOF STEP]
from lhs
[PROOF STATE]
proof (chain)
picking this:
exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')
[PROOF STEP]
have "exec_meth ci (compP2 P) ((?E @ compE2 e') @ []) ((compxE2 e 0 0 @ shift (length ?E) (compxE2 e' 0 0)) @ ?xt) t h (stk, loc, length ?E + pc, xcp) ta h' (stk', loc', length ?E + pc', xcp')"
[PROOF STATE]
proof (prove)
using this:
exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (((compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) @ compE2 e') @ []) ((compxE2 e 0 0 @ shift (length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V])) (compxE2 e' 0 0)) @ [(0, length (compE2 e), \<lfloor>C\<rfloor>, Suc (length (compE2 e)), 0)]) t h (stk, loc, length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc', xcp')
[PROOF STEP]
by(simp add: exec_move_def shift_compxE2 ac_simps)
[PROOF STATE]
proof (state)
this:
exec_meth ci (compP2 P) (((compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) @ compE2 e') @ []) ((compxE2 e 0 0 @ shift (length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V])) (compxE2 e' 0 0)) @ [(0, length (compE2 e), \<lfloor>C\<rfloor>, Suc (length (compE2 e)), 0)]) t h (stk, loc, length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc', xcp')

goal (2 subgoals):
 1. exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp') \<Longrightarrow> exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
 2. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')
[PROOF STEP]
thus ?rhs
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) @ compE2 e') @ []) ((compxE2 e 0 0 @ shift (length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V])) (compxE2 e' 0 0)) @ [(0, length (compE2 e), \<lfloor>C\<rfloor>, Suc (length (compE2 e)), 0)]) t h (stk, loc, length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
unfolding exec_move_def
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) @ compE2 e') @ []) ((compxE2 e 0 0 @ shift (length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V])) (compxE2 e' 0 0)) @ [(0, length (compE2 e), \<lfloor>C\<rfloor>, Suc (length (compE2 e)), 0)]) t h (stk, loc, length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc', xcp')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e') (compxE2 e' 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
using pc
[PROOF STATE]
proof (prove)
using this:
exec_meth ci (compP2 P) (((compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) @ compE2 e') @ []) ((compxE2 e 0 0 @ shift (length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V])) (compxE2 e' 0 0)) @ [(0, length (compE2 e), \<lfloor>C\<rfloor>, Suc (length (compE2 e)), 0)]) t h (stk, loc, length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc, xcp) ta h' (stk', loc', length (compE2 e @ [Goto (int (length (compE2 e')) + 2), Store V]) + pc', xcp')
pc < length (compE2 e')

goal (1 subgoal):
 1. exec_meth ci (compP2 P) (compE2 e') (compxE2 e' 0 0) t h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')
[PROOF STEP]
by-(drule exec_meth_drop_xt[OF exec_meth_take_xt'], auto)
[PROOF STATE]
proof (state)
this:
exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp')

goal (1 subgoal):
 1. exec_move ci P t e' h (stk, loc, pc, xcp) ta h' (stk', loc', pc', xcp') \<Longrightarrow> exec_move ci P t (try e catch(C V) e') h (stk, loc, Suc (Suc (length (compE2 e) + pc)), xcp) ta h' (stk', loc', Suc (Suc (length (compE2 e) + pc')), xcp')
[PROOF STEP]
qed(rule exec_move_TryI2)


[STATEMENT]
lemma exec_move_raise_xcp_pcD:
  "exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', Some a) \<Longrightarrow> pc' = pc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>) \<Longrightarrow> pc' = pc
[PROOF STEP]
apply(cases "compE2 E ! pc")
[PROOF STATE]
proof (prove)
goal (24 subgoals):
 1. \<And>x1. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = Load x1\<rbrakk> \<Longrightarrow> pc' = pc
 2. \<And>x2. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = Store x2\<rbrakk> \<Longrightarrow> pc' = pc
 3. \<And>x3. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = Push x3\<rbrakk> \<Longrightarrow> pc' = pc
 4. \<And>x4. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = New x4\<rbrakk> \<Longrightarrow> pc' = pc
 5. \<And>x5. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = NewArray x5\<rbrakk> \<Longrightarrow> pc' = pc
 6. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = ALoad\<rbrakk> \<Longrightarrow> pc' = pc
 7. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = AStore\<rbrakk> \<Longrightarrow> pc' = pc
 8. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = ALength\<rbrakk> \<Longrightarrow> pc' = pc
 9. \<And>x91 x92. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = Getfield x91 x92\<rbrakk> \<Longrightarrow> pc' = pc
 10. \<And>x101 x102. \<lbrakk>exec_move ci P t E h (stk, loc, pc, None) ta h' (stk', loc', pc', \<lfloor>a\<rfloor>); compE2 E ! pc = Putfield x101 x102\<rbrakk> \<Longrightarrow> pc' = pc
A total of 24 subgoals...
[PROOF STEP]
apply(auto simp add: exec_move_def elim!: exec_meth.cases split: if_split_asm sum.split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x141 x142 aa ab ac ad b x ae af ag va. \<lbrakk>pc < length (compE2 E); ci_app ci (Invoke x141 x142) (compP2 P) h stk loc undefined undefined pc []; compE2 E ! pc = Invoke x141 x142; ta = (aa, map (convert_new_thread_action (extNTA2JVM (compP2 P))) ag, ab, ac, ad, b); stk ! x142 \<noteq> Null; method (compP2 P) (class_type_of (the (typeof_addr h (the_Addr (stk ! x142))))) x141 = (x, ae, af, None); case va of RetVal v \<Rightarrow> \<lfloor>a\<rfloor> = None \<and> [(stk', loc', undefined, undefined, pc')] = [(v # drop (Suc x142) stk, loc, undefined, undefined, pc + 1)] | RetExc aa \<Rightarrow> \<lfloor>a\<rfloor> = \<lfloor>aa\<rfloor> \<and> [(stk', loc', undefined, undefined, pc')] = [(stk, loc, undefined, undefined, pc)] | RetStaySame \<Rightarrow> \<lfloor>a\<rfloor> = None \<and> [(stk', loc', undefined, undefined, pc')] = [(stk, loc, undefined, undefined, pc)]; ((aa, ag, ab, ac, ad, b), va, h') \<in> red_external_aggr (compP2 P) t (the_Addr (stk ! x142)) x141 (rev (take x142 stk)) h\<rbrakk> \<Longrightarrow> pc' = pc
[PROOF STEP]
apply(auto split: extCallRet.split_asm simp add: split_beta)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma \<tau>exec_methI [intro]:
  "\<lbrakk> exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<epsilon> h s'; xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc) \<rbrakk>
   \<Longrightarrow> \<tau>exec_meth ci P ins xt t h (stk, loc, pc, xcp) s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc)\<rbrakk> \<Longrightarrow> \<tau>exec_meth ci P ins xt t h (stk, loc, pc, xcp) s'
[PROOF STEP]
by(simp add: \<tau>exec_meth_def)


[STATEMENT]
lemma \<tau>exec_methE [elim]:
  assumes "\<tau>exec_meth ci P ins xt t h s s'"
  obtains stk loc pc xcp
  where "s = (stk, loc, pc, xcp)"
  and "exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<epsilon> h s'"
  and "xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>stk loc pc xcp. \<lbrakk>s = (stk, loc, pc, xcp); exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>exec_meth ci P ins xt t h s s'

goal (1 subgoal):
 1. (\<And>stk loc pc xcp. \<lbrakk>s = (stk, loc, pc, xcp); exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s)(auto simp add: \<tau>exec_meth_def)


[STATEMENT]
lemma \<tau>Exec_methr_refl: "\<tau>Exec_methr ci P ins xt t h s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_methr ci P ins xt t h s s
[PROOF STEP]
..


[STATEMENT]
lemma \<tau>Exec_methr_step':
  "\<lbrakk> \<tau>Exec_methr ci P ins xt t h s (stk', loc', pc', xcp');
     \<tau>exec_meth ci P ins xt t h (stk', loc', pc', xcp') s' \<rbrakk>
  \<Longrightarrow> \<tau>Exec_methr ci P ins xt t h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_methr ci P ins xt t h s (stk', loc', pc', xcp'); \<tau>exec_meth ci P ins xt t h (stk', loc', pc', xcp') s'\<rbrakk> \<Longrightarrow> \<tau>Exec_methr ci P ins xt t h s s'
[PROOF STEP]
by(rule rtranclp.rtrancl_into_rtrancl)


[STATEMENT]
lemma \<tau>Exec_methr_step:
  "\<lbrakk> \<tau>Exec_methr ci P ins xt t h s (stk', loc', pc', xcp');
     exec_meth ci P ins xt t h (stk', loc', pc', xcp') \<epsilon> h s';
     xcp' = None \<Longrightarrow> \<tau>instr P h stk' (ins ! pc') \<rbrakk>
  \<Longrightarrow> \<tau>Exec_methr ci P ins xt t h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_methr ci P ins xt t h s (stk', loc', pc', xcp'); exec_meth ci P ins xt t h (stk', loc', pc', xcp') \<lbrace>\<rbrace> h s'; xcp' = None \<Longrightarrow> \<tau>instr P h stk' (ins ! pc')\<rbrakk> \<Longrightarrow> \<tau>Exec_methr ci P ins xt t h s s'
[PROOF STEP]
by(erule \<tau>Exec_methr_step')(rule \<tau>exec_methI)


[STATEMENT]
lemma \<tau>Exec_methr_cases [consumes 1, case_names refl step]:
  assumes "\<tau>Exec_methr ci P ins xt t h s s'"
  obtains "s = s'"
  | stk' loc' pc' xcp'
    where "\<tau>Exec_methr ci P ins xt t h s (stk', loc', pc', xcp')"
       "exec_meth ci P ins xt t h (stk', loc', pc', xcp') \<epsilon> h s'"
       "xcp' = None \<Longrightarrow> \<tau>instr P h stk' (ins ! pc')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s = s' \<Longrightarrow> thesis; \<And>stk' loc' pc' xcp'. \<lbrakk>\<tau>Exec_methr ci P ins xt t h s (stk', loc', pc', xcp'); exec_meth ci P ins xt t h (stk', loc', pc', xcp') \<lbrace>\<rbrace> h s'; xcp' = None \<Longrightarrow> \<tau>instr P h stk' (ins ! pc')\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_methr ci P ins xt t h s s'

goal (1 subgoal):
 1. \<lbrakk>s = s' \<Longrightarrow> thesis; \<And>stk' loc' pc' xcp'. \<lbrakk>\<tau>Exec_methr ci P ins xt t h s (stk', loc', pc', xcp'); exec_meth ci P ins xt t h (stk', loc', pc', xcp') \<lbrace>\<rbrace> h s'; xcp' = None \<Longrightarrow> \<tau>instr P h stk' (ins ! pc')\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(rule rtranclp.cases)(auto elim!: \<tau>exec_methE)


[STATEMENT]
lemma \<tau>Exec_methr_induct [consumes 1, case_names refl step]:
  "\<lbrakk> \<tau>Exec_methr ci P ins xt t h s s';
     Q s;
     \<And>stk loc pc xcp s'. \<lbrakk> \<tau>Exec_methr ci P ins xt t h s (stk, loc, pc, xcp); exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<epsilon> h s';
                          xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc); Q (stk, loc, pc, xcp) \<rbrakk> \<Longrightarrow> Q s' \<rbrakk>
  \<Longrightarrow> Q s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_methr ci P ins xt t h s s'; Q s; \<And>stk loc pc xcp s'. \<lbrakk>\<tau>Exec_methr ci P ins xt t h s (stk, loc, pc, xcp); exec_meth ci P ins xt t h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; xcp = None \<Longrightarrow> \<tau>instr P h stk (ins ! pc); Q (stk, loc, pc, xcp)\<rbrakk> \<Longrightarrow> Q s'\<rbrakk> \<Longrightarrow> Q s'
[PROOF STEP]
by(erule (1) rtranclp_induct)(blast elim: \<tau>exec_methE)


[STATEMENT]
lemma \<tau>Exec_methr_trans:
  "\<lbrakk> \<tau>Exec_methr ci P ins xt t h s s'; \<tau>Exec_methr ci P ins xt t h s' s'' \<rbrakk> \<Longrightarrow> \<tau>Exec_methr ci P ins xt t h s s''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_methr ci P ins xt t h s s'; \<tau>Exec_methr ci P ins xt t h s' s''\<rbrakk> \<Longrightarrow> \<tau>Exec_methr ci P ins xt t h s s''
[PROOF STEP]
by(rule rtranclp_trans)


[STATEMENT]
lemma \<tau>exec_moveI:
  "\<lbrakk> exec_move ci P t e h (stk, loc, pc, xcp) \<epsilon> h s'; \<tau>move2 P h stk e pc xcp \<rbrakk>
  \<Longrightarrow> \<tau>exec_move ci P t e h (stk, loc, pc, xcp) s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_move ci P t e h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; \<tau>move2 P h stk e pc xcp\<rbrakk> \<Longrightarrow> \<tau>exec_move ci P t e h (stk, loc, pc, xcp) s'
[PROOF STEP]
by(simp add: \<tau>exec_move_def)


[STATEMENT]
lemma \<tau>exec_moveE:
  assumes "\<tau>exec_move ci P t e h (stk, loc, pc, xcp) s'"
  obtains "exec_move ci P t e h (stk, loc, pc, xcp) \<epsilon> h s'" "\<tau>move2 P h stk e pc xcp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>exec_move ci P t e h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; \<tau>move2 P h stk e pc xcp\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>exec_move ci P t e h (stk, loc, pc, xcp) s'

goal (1 subgoal):
 1. (\<lbrakk>exec_move ci P t e h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; \<tau>move2 P h stk e pc xcp\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add: \<tau>exec_move_def)


[STATEMENT]
lemma \<tau>exec_movesI:
  "\<lbrakk> exec_moves ci P t es h (stk, loc, pc, xcp) \<epsilon> h s'; \<tau>moves2 P h stk es pc xcp \<rbrakk>
  \<Longrightarrow> \<tau>exec_moves ci P t es h (stk, loc, pc, xcp) s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_moves ci P t es h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; \<tau>moves2 P h stk es pc xcp\<rbrakk> \<Longrightarrow> \<tau>exec_moves ci P t es h (stk, loc, pc, xcp) s'
[PROOF STEP]
by(simp add: \<tau>exec_moves_def)


[STATEMENT]
lemma \<tau>exec_movesE:
  assumes "\<tau>exec_moves ci P t es h (stk, loc, pc, xcp) s'"
  obtains "exec_moves ci P t es h (stk, loc, pc, xcp) \<epsilon> h s'" "\<tau>moves2 P h stk es pc xcp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>exec_moves ci P t es h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; \<tau>moves2 P h stk es pc xcp\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<tau>exec_moves ci P t es h (stk, loc, pc, xcp) s'

goal (1 subgoal):
 1. (\<lbrakk>exec_moves ci P t es h (stk, loc, pc, xcp) \<lbrace>\<rbrace> h s'; \<tau>moves2 P h stk es pc xcp\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add: \<tau>exec_moves_def)


[STATEMENT]
lemma \<tau>exec_move_conv_\<tau>exec_meth:
  "\<tau>exec_move ci P t e = \<tau>exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_move ci P t e = \<tau>exec_meth ci (compP2 P) (compE2 e) (compxE2 e 0 0) t
[PROOF STEP]
by(auto simp add: \<tau>exec_move_def exec_move_def \<tau>move2_iff compP2_def intro!: ext \<tau>exec_methI elim!: \<tau>exec_methE)


[STATEMENT]
lemma \<tau>exec_moves_conv_\<tau>exec_meth:
  "\<tau>exec_moves ci P t es = \<tau>exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>exec_moves ci P t es = \<tau>exec_meth ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t
[PROOF STEP]
by(auto simp add: \<tau>exec_moves_def exec_moves_def \<tau>moves2_iff compP2_def intro!: ext \<tau>exec_methI elim!: \<tau>exec_methE)


[STATEMENT]
lemma \<tau>Execsr_refl: "\<tau>Exec_movesr ci P t e h s s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movesr ci P t e h s s
[PROOF STEP]
by(rule rtranclp.rtrancl_refl)


[STATEMENT]
lemma \<tau>Execr_step:
  "\<lbrakk> \<tau>Exec_mover ci P t e h s (stk', loc', pc', xcp');
     exec_move ci P t e h (stk', loc', pc', xcp') \<epsilon> h s';
     \<tau>move2 P h stk' e pc' xcp' \<rbrakk>
  \<Longrightarrow> \<tau>Exec_mover ci P t e h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_mover ci P t e h s (stk', loc', pc', xcp'); exec_move ci P t e h (stk', loc', pc', xcp') \<lbrace>\<rbrace> h s'; \<tau>move2 P h stk' e pc' xcp'\<rbrakk> \<Longrightarrow> \<tau>Exec_mover ci P t e h s s'
[PROOF STEP]
by(rule rtranclp.rtrancl_into_rtrancl)(auto elim: \<tau>exec_moveI)


[STATEMENT]
lemma \<tau>Execsr_step:
  "\<lbrakk> \<tau>Exec_movesr ci P t es h s (stk', loc', pc', xcp');
     exec_moves ci P t es h (stk', loc', pc', xcp') \<epsilon> h s';
     \<tau>moves2 P h stk' es pc' xcp' \<rbrakk>
  \<Longrightarrow> \<tau>Exec_movesr ci P t es h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_movesr ci P t es h s (stk', loc', pc', xcp'); exec_moves ci P t es h (stk', loc', pc', xcp') \<lbrace>\<rbrace> h s'; \<tau>moves2 P h stk' es pc' xcp'\<rbrakk> \<Longrightarrow> \<tau>Exec_movesr ci P t es h s s'
[PROOF STEP]
by(rule rtranclp.rtrancl_into_rtrancl)(auto elim: \<tau>exec_movesI)


[STATEMENT]
lemma \<tau>Exect_step:
  "\<lbrakk> \<tau>Exec_movet ci P t e h s (stk', loc', pc', xcp');
     exec_move ci P t e h (stk', loc', pc', xcp') \<epsilon> h s';
     \<tau>move2 P h stk' e pc' xcp' \<rbrakk>
  \<Longrightarrow> \<tau>Exec_movet ci P t e h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_movet ci P t e h s (stk', loc', pc', xcp'); exec_move ci P t e h (stk', loc', pc', xcp') \<lbrace>\<rbrace> h s'; \<tau>move2 P h stk' e pc' xcp'\<rbrakk> \<Longrightarrow> \<tau>Exec_movet ci P t e h s s'
[PROOF STEP]
by(rule tranclp.trancl_into_trancl)(auto intro: \<tau>exec_moveI)


[STATEMENT]
lemma \<tau>Execst_step:
  "\<lbrakk> \<tau>Exec_movest ci P t es h s (stk', loc', pc', xcp');
     exec_moves ci P t es h (stk', loc', pc', xcp') \<epsilon> h s';
     \<tau>moves2 P h stk' es pc' xcp' \<rbrakk>
  \<Longrightarrow> \<tau>Exec_movest ci P t es h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_movest ci P t es h s (stk', loc', pc', xcp'); exec_moves ci P t es h (stk', loc', pc', xcp') \<lbrace>\<rbrace> h s'; \<tau>moves2 P h stk' es pc' xcp'\<rbrakk> \<Longrightarrow> \<tau>Exec_movest ci P t es h s s'
[PROOF STEP]
by(rule tranclp.trancl_into_trancl)(auto intro: \<tau>exec_movesI)


[STATEMENT]
lemma \<tau>Exect1step:
  "\<lbrakk> exec_move ci P t e h s \<epsilon> h s';
     \<tau>move2 P h (fst s) e (fst (snd (snd s))) (snd (snd (snd s))) \<rbrakk>
  \<Longrightarrow> \<tau>Exec_movet ci P t e h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_move ci P t e h s \<lbrace>\<rbrace> h s'; \<tau>move2 P h (fst s) e (fst (snd (snd s))) (snd (snd (snd s)))\<rbrakk> \<Longrightarrow> \<tau>Exec_movet ci P t e h s s'
[PROOF STEP]
by(rule tranclp.r_into_trancl)(cases s, auto intro: \<tau>exec_moveI)


[STATEMENT]
lemma \<tau>Execst1step:
  "\<lbrakk> exec_moves ci P t es h s \<epsilon> h s';
     \<tau>moves2 P h (fst s) es (fst (snd (snd s))) (snd (snd (snd s))) \<rbrakk>
  \<Longrightarrow> \<tau>Exec_movest ci P t es h s s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>exec_moves ci P t es h s \<lbrace>\<rbrace> h s'; \<tau>moves2 P h (fst s) es (fst (snd (snd s))) (snd (snd (snd s)))\<rbrakk> \<Longrightarrow> \<tau>Exec_movest ci P t es h s s'
[PROOF STEP]
by(rule tranclp.r_into_trancl)(cases s, auto intro: \<tau>exec_movesI)


[STATEMENT]
lemma \<tau>Execr_induct [consumes 1, case_names refl step]:
  assumes major: "\<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')"
  and refl: "Q stk loc pc xcp"
  and step: "\<And>stk' loc' pc' xcp' stk'' loc'' pc'' xcp''.
             \<lbrakk> \<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp');
               \<tau>exec_move ci P t e h (stk', loc', pc', xcp') (stk'', loc'', pc'', xcp''); Q stk' loc' pc' xcp' \<rbrakk>
             \<Longrightarrow> Q stk'' loc'' pc'' xcp''"
  shows "Q stk'' loc'' pc'' xcp''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q stk'' loc'' pc'' xcp''
[PROOF STEP]
using major refl
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_mover ci P t e h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')
Q stk loc pc xcp

goal (1 subgoal):
 1. Q stk'' loc'' pc'' xcp''
[PROOF STEP]
by(rule rtranclp_induct4)(rule step)


[STATEMENT]
lemma \<tau>Execsr_induct [consumes 1, case_names refl step]:
  assumes major: "\<tau>Exec_movesr ci P t es h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')"
  and refl: "Q stk loc pc xcp"
  and step: "\<And>stk' loc' pc' xcp' stk'' loc'' pc'' xcp''.
             \<lbrakk> \<tau>Exec_movesr ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp');
               \<tau>exec_moves ci P t es h (stk', loc', pc', xcp') (stk'', loc'', pc'', xcp''); Q stk' loc' pc' xcp' \<rbrakk>
             \<Longrightarrow> Q stk'' loc'' pc'' xcp''"
  shows "Q stk'' loc'' pc'' xcp''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q stk'' loc'' pc'' xcp''
[PROOF STEP]
using major refl
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_movesr ci P t es h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')
Q stk loc pc xcp

goal (1 subgoal):
 1. Q stk'' loc'' pc'' xcp''
[PROOF STEP]
by(rule rtranclp_induct4)(rule step)


[STATEMENT]
lemma \<tau>Exect_induct [consumes 1, case_names base step]:
  assumes major: "\<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')"
  and base: "\<And>stk' loc' pc' xcp'. \<tau>exec_move ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> Q stk' loc' pc' xcp'"
  and step: "\<And>stk' loc' pc' xcp' stk'' loc'' pc'' xcp''.
             \<lbrakk> \<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk', loc', pc', xcp');
               \<tau>exec_move ci P t e h (stk', loc', pc', xcp') (stk'', loc'', pc'', xcp''); Q stk' loc' pc' xcp' \<rbrakk>
             \<Longrightarrow> Q stk'' loc'' pc'' xcp''"
  shows "Q stk'' loc'' pc'' xcp''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q stk'' loc'' pc'' xcp''
[PROOF STEP]
using major
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_movet ci P t e h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')

goal (1 subgoal):
 1. Q stk'' loc'' pc'' xcp''
[PROOF STEP]
by(rule tranclp_induct4)(erule base step)+


[STATEMENT]
lemma \<tau>Execst_induct [consumes 1, case_names base step]:
  assumes major: "\<tau>Exec_movest ci P t es h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')"
  and base: "\<And>stk' loc' pc' xcp'. \<tau>exec_moves ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') \<Longrightarrow> Q stk' loc' pc' xcp'"
  and step: "\<And>stk' loc' pc' xcp' stk'' loc'' pc'' xcp''.
             \<lbrakk> \<tau>Exec_movest ci P t es h (stk, loc, pc, xcp) (stk', loc', pc', xcp');
               \<tau>exec_moves ci P t es h (stk', loc', pc', xcp') (stk'', loc'', pc'', xcp''); Q stk' loc' pc' xcp' \<rbrakk>
             \<Longrightarrow> Q stk'' loc'' pc'' xcp''"
  shows "Q stk'' loc'' pc'' xcp''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q stk'' loc'' pc'' xcp''
[PROOF STEP]
using major
[PROOF STATE]
proof (prove)
using this:
\<tau>Exec_movest ci P t es h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')

goal (1 subgoal):
 1. Q stk'' loc'' pc'' xcp''
[PROOF STEP]
by(rule tranclp_induct4)(erule base step)+


[STATEMENT]
lemma \<tau>Exec_mover_\<tau>Exec_methr:
  "\<tau>Exec_mover ci P t e = \<tau>Exec_methr ci (compP2 P) (compE2 e) (compxE2 e 0 0) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_mover ci P t e = \<tau>Exec_methr ci (compP2 P) (compE2 e) (compxE2 e 0 0) t
[PROOF STEP]
by(simp only: \<tau>exec_move_conv_\<tau>exec_meth)


[STATEMENT]
lemma \<tau>Exec_movesr_\<tau>Exec_methr:
  "\<tau>Exec_movesr ci P t es = \<tau>Exec_methr ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movesr ci P t es = \<tau>Exec_methr ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t
[PROOF STEP]
by(simp only: \<tau>exec_moves_conv_\<tau>exec_meth)


[STATEMENT]
lemma \<tau>Exec_movet_\<tau>Exec_metht:
  "\<tau>Exec_movet ci P t e = \<tau>Exec_metht ci (compP2 P) (compE2 e) (compxE2 e 0 0) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movet ci P t e = \<tau>Exec_metht ci (compP2 P) (compE2 e) (compxE2 e 0 0) t
[PROOF STEP]
by(simp only: \<tau>exec_move_conv_\<tau>exec_meth)


[STATEMENT]
lemma \<tau>Exec_movest_\<tau>Exec_metht:
  "\<tau>Exec_movest ci P t es = \<tau>Exec_metht ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>Exec_movest ci P t es = \<tau>Exec_metht ci (compP2 P) (compEs2 es) (compxEs2 es 0 0) t
[PROOF STEP]
by(simp only: \<tau>exec_moves_conv_\<tau>exec_meth)


[STATEMENT]
lemma \<tau>Exec_mover_trans:
  "\<lbrakk> \<tau>Exec_mover ci P t e h s s'; \<tau>Exec_mover ci P t e h s' s'' \<rbrakk> \<Longrightarrow> \<tau>Exec_mover ci P t e h s s''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<tau>Exec_mover ci P t e h s s'; \<tau>Exec_mover ci P t e h s' s''\<rbrakk> \<Longrightarrow> \<tau>Exec_mover ci P t e h s s''
[PROOF STEP]
by(rule rtranclp_trans)