[STATEMENT]
lemma sc_exec_deterministic:
  assumes "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
  shows "multithreaded_base.deterministic JVM_final' (\<lambda>t xm ta x'm'. Predicate.eval (sc_mexec P t xm) (ta, x'm')) convert_RA
     (sc_jvm_state_invar P \<Phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multithreaded_base.deterministic JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. multithreaded_base.deterministic JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
from assms sc_deterministic_heap_ops
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog\<^bsub>\<Phi>\<^esub> P
\<not> sc_spurious_wakeups \<Longrightarrow> sc_deterministic_heap_ops ?P
[PROOF STEP]
have det: "multithreaded_base.deterministic JVM_final (sc_execute_mexec P) convert_RA {s. sc.execute.correct_state_ts P \<Phi> (thr s) (shr s)}"
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>\<Phi>\<^esub> P
\<not> sc_spurious_wakeups \<Longrightarrow> sc_deterministic_heap_ops ?P

goal (1 subgoal):
 1. multithreaded_base.deterministic JVM_final (sc_execute_mexec P) convert_RA {s. sc.execute.correct_state_ts P \<Phi> (thr s) (shr s)}
[PROOF STEP]
by(rule sc.execute.mexec_deterministic)(simp add: sc_spurious_wakeups)
[PROOF STATE]
proof (state)
this:
multithreaded_base.deterministic JVM_final (sc_execute_mexec P) convert_RA {s. sc.execute.correct_state_ts P \<Phi> (thr s) (shr s)}

goal (1 subgoal):
 1. multithreaded_base.deterministic JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multithreaded_base.deterministic JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
proof(rule multithreaded_base.determisticI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
fix s t x ta' x' m' ta'' x'' m''
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
assume inv: "s \<in> sc_jvm_state_invar P \<Phi>"
      and tst: "thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>"
      and exec1: "Predicate.eval (sc_mexec P t (x, shr s)) (ta', x', m')"
      and exec2: "Predicate.eval (sc_mexec P t (x, shr s)) (ta'', x'', m'')"
      and aok1: "final_thread.actions_ok JVM_final' s t ta'"
      and aok2: "final_thread.actions_ok JVM_final' s t ta''"
[PROOF STATE]
proof (state)
this:
s \<in> sc_jvm_state_invar P \<Phi>
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
pred.eval (sc_mexec P t (x, shr s)) (ta', x', m')
pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m'')
final_thread.actions_ok JVM_final' s t ta'
final_thread.actions_ok JVM_final' s t ta''

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
obtain xcp frs where x: "x = (xcp, frs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xcp frs. x = (xcp, frs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases x)
[PROOF STATE]
proof (state)
this:
x = (xcp, frs)

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
from inv tst x
[PROOF STATE]
proof (chain)
picking this:
s \<in> sc_jvm_state_invar P \<Phi>
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
x = (xcp, frs)
[PROOF STEP]
have correct: "sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))"
      and ok: "jvm_state'_ok P (xcp, shr s, frs)"
[PROOF STATE]
proof (prove)
using this:
s \<in> sc_jvm_state_invar P \<Phi>
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>
x = (xcp, frs)

goal (1 subgoal):
 1. sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs)) &&& jvm_state'_ok P (xcp, shr s, frs)
[PROOF STEP]
by(cases s, fastforce simp add: sc_jvm_state_invar_def sc.execute.correct_jvm_state_def dest: ts_okD)+
[PROOF STATE]
proof (state)
this:
sc.execute.correct_state P \<Phi> t (jvm_state_of_jvm_state' (xcp, shr s, frs))
jvm_state'_ok P (xcp, shr s, frs)

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
note eq = sc.exec_correct_state(1)[OF assms this]
[PROOF STATE]
proof (state)
this:
sc_exec P t (xcp, shr s, frs) = jvm_ta_state'_of_jvm_ta_state P ` JVM_heap_base.exec (\<lambda>x. x) (\<lambda>x. x) sc_spurious_wakeups (rm.empty ()) (sc_allocate P) sc_typeof_addr sc_heap_read sc_heap_write P t (jvm_state_of_jvm_state' (xcp, shr s, frs))

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
from exec1 exec2 x
[PROOF STATE]
proof (chain)
picking this:
pred.eval (sc_mexec P t (x, shr s)) (ta', x', m')
pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m'')
x = (xcp, frs)
[PROOF STEP]
have "sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta') (jvm_thread_state_of_jvm_thread_state' x', m')"
      and "sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta'') (jvm_thread_state_of_jvm_thread_state' x'', m'')"
[PROOF STATE]
proof (prove)
using this:
pred.eval (sc_mexec P t (x, shr s)) (ta', x', m')
pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m'')
x = (xcp, frs)

goal (1 subgoal):
 1. sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta') (jvm_thread_state_of_jvm_thread_state' x', m') &&& sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta'') (jvm_thread_state_of_jvm_thread_state' x'', m'')
[PROOF STEP]
by(auto simp add: sc.exec_1_def eq jvm_thread_action'_of_jvm_thread_action_def sc.execute.exec_1_iff)
[PROOF STATE]
proof (state)
this:
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta') (jvm_thread_state_of_jvm_thread_state' x', m')
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta'') (jvm_thread_state_of_jvm_thread_state' x'', m'')

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta') (jvm_thread_state_of_jvm_thread_state' x', m')
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta'') (jvm_thread_state_of_jvm_thread_state' x'', m'')

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
have "thr (jvm_mstate_of_jvm_mstate' s) t = \<lfloor>(jvm_thread_state_of_jvm_thread_state' x, no_wait_locks)\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thr (jvm_mstate_of_jvm_mstate' s) t = \<lfloor>(jvm_thread_state_of_jvm_thread_state' x, no_wait_locks)\<rfloor>
[PROOF STEP]
using tst
[PROOF STATE]
proof (prove)
using this:
thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>

goal (1 subgoal):
 1. thr (jvm_mstate_of_jvm_mstate' s) t = \<lfloor>(jvm_thread_state_of_jvm_thread_state' x, no_wait_locks)\<rfloor>
[PROOF STEP]
by(cases s) clarsimp
[PROOF STATE]
proof (state)
this:
thr (jvm_mstate_of_jvm_mstate' s) t = \<lfloor>(jvm_thread_state_of_jvm_thread_state' x, no_wait_locks)\<rfloor>

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
thr (jvm_mstate_of_jvm_mstate' s) t = \<lfloor>(jvm_thread_state_of_jvm_thread_state' x, no_wait_locks)\<rfloor>

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
have "final_thread.actions_ok JVM_final (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta')"
      and "final_thread.actions_ok JVM_final (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta') &&& sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta'')
[PROOF STEP]
using aok1 aok2
[PROOF STATE]
proof (prove)
using this:
final_thread.actions_ok JVM_final' s t ta'
final_thread.actions_ok JVM_final' s t ta''

goal (1 subgoal):
 1. sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta') &&& sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta'')
[PROOF STEP]
by -(case_tac [!] s,auto simp add: final_thread.actions_ok_iff elim: rev_iffD1[OF _ thread_oks_ts_change] cond_action_oks_final_change)
[PROOF STATE]
proof (state)
this:
sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta')
sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta'')

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta')
sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta'')

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
have "sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))
[PROOF STEP]
using inv
[PROOF STATE]
proof (prove)
using this:
s \<in> sc_jvm_state_invar P \<Phi>

goal (1 subgoal):
 1. sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))
[PROOF STEP]
by(cases s)(auto intro!: ts_okI simp add: sc_jvm_state_invar_def sc.execute.correct_jvm_state_def dest: ts_okD)
[PROOF STATE]
proof (state)
this:
sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta') (jvm_thread_state_of_jvm_thread_state' x', m')
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta'') (jvm_thread_state_of_jvm_thread_state' x'', m'')
thr (jvm_mstate_of_jvm_mstate' s) t = \<lfloor>(jvm_thread_state_of_jvm_thread_state' x, no_wait_locks)\<rfloor>
sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta')
sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta'')
sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))
[PROOF STEP]
have "jvm_thread_action_of_jvm_thread_action' ta' = jvm_thread_action_of_jvm_thread_action' ta'' \<and>
          jvm_thread_state_of_jvm_thread_state' x' = jvm_thread_state_of_jvm_thread_state' x'' \<and>
          m' = m''"
[PROOF STATE]
proof (prove)
using this:
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta') (jvm_thread_state_of_jvm_thread_state' x', m')
sc_execute_mexec P t (jvm_thread_state_of_jvm_thread_state' x, shr (jvm_mstate_of_jvm_mstate' s)) (jvm_thread_action_of_jvm_thread_action' ta'') (jvm_thread_state_of_jvm_thread_state' x'', m'')
thr (jvm_mstate_of_jvm_mstate' s) t = \<lfloor>(jvm_thread_state_of_jvm_thread_state' x, no_wait_locks)\<rfloor>
sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta')
sc.execute.exec_mthr.actions_ok (jvm_mstate_of_jvm_mstate' s) t (jvm_thread_action_of_jvm_thread_action' ta'')
sc.execute.correct_state_ts P \<Phi> (thr (jvm_mstate_of_jvm_mstate' s)) (shr (jvm_mstate_of_jvm_mstate' s))

goal (1 subgoal):
 1. jvm_thread_action_of_jvm_thread_action' ta' = jvm_thread_action_of_jvm_thread_action' ta'' \<and> jvm_thread_state_of_jvm_thread_state' x' = jvm_thread_state_of_jvm_thread_state' x'' \<and> m' = m''
[PROOF STEP]
by-(drule (4) multithreaded_base.deterministicD[OF det], simp_all)
[PROOF STATE]
proof (state)
this:
jvm_thread_action_of_jvm_thread_action' ta' = jvm_thread_action_of_jvm_thread_action' ta'' \<and> jvm_thread_state_of_jvm_thread_state' x' = jvm_thread_state_of_jvm_thread_state' x'' \<and> m' = m''

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
jvm_thread_action_of_jvm_thread_action' ta' = jvm_thread_action_of_jvm_thread_action' ta'' \<and> jvm_thread_state_of_jvm_thread_state' x' = jvm_thread_state_of_jvm_thread_state' x'' \<and> m' = m''

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
from exec1 exec2 x
[PROOF STATE]
proof (chain)
picking this:
pred.eval (sc_mexec P t (x, shr s)) (ta', x', m')
pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m'')
x = (xcp, frs)
[PROOF STEP]
have "(ta', (fst x', m', snd x')) \<in> sc_exec P t (xcp, shr s, frs)"
      and "(ta'', (fst x'', m'', snd x'')) \<in> sc_exec P t (xcp, shr s, frs)"
[PROOF STATE]
proof (prove)
using this:
pred.eval (sc_mexec P t (x, shr s)) (ta', x', m')
pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m'')
x = (xcp, frs)

goal (1 subgoal):
 1. (ta', fst x', m', snd x') \<in> sc_exec P t (xcp, shr s, frs) &&& (ta'', fst x'', m'', snd x'') \<in> sc_exec P t (xcp, shr s, frs)
[PROOF STEP]
by(auto simp add: sc.exec_1_def)
[PROOF STATE]
proof (state)
this:
(ta', fst x', m', snd x') \<in> sc_exec P t (xcp, shr s, frs)
(ta'', fst x'', m'', snd x'') \<in> sc_exec P t (xcp, shr s, frs)

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
hence "jvm_ta_state'_ok P (ta', (fst x', m', snd x'))"
      and "jvm_ta_state'_ok P (ta'', (fst x'', m'', snd x''))"
[PROOF STATE]
proof (prove)
using this:
(ta', fst x', m', snd x') \<in> sc_exec P t (xcp, shr s, frs)
(ta'', fst x'', m'', snd x'') \<in> sc_exec P t (xcp, shr s, frs)

goal (1 subgoal):
 1. jvm_ta_state'_ok P (ta', fst x', m', snd x') &&& jvm_ta_state'_ok P (ta'', fst x'', m'', snd x'')
[PROOF STEP]
by(blast intro: sc.exec_correct_state[OF assms correct ok])+
[PROOF STATE]
proof (state)
this:
jvm_ta_state'_ok P (ta', fst x', m', snd x')
jvm_ta_state'_ok P (ta'', fst x'', m'', snd x'')

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
hence "ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta')"
      and "ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')"
      and "x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x')"
      and "x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')"
[PROOF STATE]
proof (prove)
using this:
jvm_ta_state'_ok P (ta', fst x', m', snd x')
jvm_ta_state'_ok P (ta'', fst x'', m'', snd x'')

goal (1 subgoal):
 1. (ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta') &&& ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')) &&& x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x') &&& x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x'')\<rbrakk> \<Longrightarrow> ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta')
 2. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x'')\<rbrakk> \<Longrightarrow> ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')
 3. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x'')\<rbrakk> \<Longrightarrow> x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x')
 4. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x'')\<rbrakk> \<Longrightarrow> x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')
[PROOF STEP]
apply(case_tac [!] ta')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c d e f. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f)\<rbrakk> \<Longrightarrow> ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta')
 2. \<And>a b c d e f. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f)\<rbrakk> \<Longrightarrow> ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')
 3. \<And>a b c d e f. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f)\<rbrakk> \<Longrightarrow> x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x')
 4. \<And>a b c d e f. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f)\<rbrakk> \<Longrightarrow> x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')
[PROOF STEP]
apply(case_tac [!] ta'')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c d e f aa ba ca da ea fa. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa)\<rbrakk> \<Longrightarrow> ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta')
 2. \<And>a b c d e f aa ba ca da ea fa. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa)\<rbrakk> \<Longrightarrow> ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')
 3. \<And>a b c d e f aa ba ca da ea fa. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa)\<rbrakk> \<Longrightarrow> x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x')
 4. \<And>a b c d e f aa ba ca da ea fa. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa)\<rbrakk> \<Longrightarrow> x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')
[PROOF STEP]
apply(case_tac [!] x')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c d e f aa ba ca da ea fa ab bb. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa); x' = (ab, bb)\<rbrakk> \<Longrightarrow> ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta')
 2. \<And>a b c d e f aa ba ca da ea fa ab bb. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa); x' = (ab, bb)\<rbrakk> \<Longrightarrow> ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')
 3. \<And>a b c d e f aa ba ca da ea fa ab bb. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa); x' = (ab, bb)\<rbrakk> \<Longrightarrow> x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x')
 4. \<And>a b c d e f aa ba ca da ea fa ab bb. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa); x' = (ab, bb)\<rbrakk> \<Longrightarrow> x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')
[PROOF STEP]
apply(case_tac [!] x'')
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a b c d e f aa ba ca da ea fa ab bb ac bc. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa); x' = (ab, bb); x'' = (ac, bc)\<rbrakk> \<Longrightarrow> ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta')
 2. \<And>a b c d e f aa ba ca da ea fa ab bb ac bc. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa); x' = (ab, bb); x'' = (ac, bc)\<rbrakk> \<Longrightarrow> ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')
 3. \<And>a b c d e f aa ba ca da ea fa ab bb ac bc. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa); x' = (ab, bb); x'' = (ac, bc)\<rbrakk> \<Longrightarrow> x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x')
 4. \<And>a b c d e f aa ba ca da ea fa ab bb ac bc. \<lbrakk>jvm_ta_state'_ok P (ta', fst x', m', snd x'); jvm_ta_state'_ok P (ta'', fst x'', m'', snd x''); ta' = (a, b, c, d, e, f); ta'' = (aa, ba, ca, da, ea, fa); x' = (ab, bb); x'' = (ac, bc)\<rbrakk> \<Longrightarrow> x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')
[PROOF STEP]
apply(fastforce simp add: jvm_thread_action'_of_jvm_thread_action_def jvm_thread_action'_ok_def intro!: map_idI[symmetric] convert_new_thread_action_eqI dest: bspec)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta')
ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')
x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x')
x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')

goal (2 subgoals):
 1. \<And>s t x ta' x' m' ta'' x'' m''. \<lbrakk>s \<in> sc_jvm_state_invar P \<Phi>; thr s t = \<lfloor>(x, no_wait_locks)\<rfloor>; pred.eval (sc_mexec P t (x, shr s)) (ta', x', m'); pred.eval (sc_mexec P t (x, shr s)) (ta'', x'', m''); final_thread.actions_ok JVM_final' s t ta'; final_thread.actions_ok JVM_final' s t ta''\<rbrakk> \<Longrightarrow> ta' = ta'' \<and> x' = x'' \<and> m' = m''
 2. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
jvm_thread_action_of_jvm_thread_action' ta' = jvm_thread_action_of_jvm_thread_action' ta'' \<and> jvm_thread_state_of_jvm_thread_state' x' = jvm_thread_state_of_jvm_thread_state' x'' \<and> m' = m''
ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta')
ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')
x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x')
x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')
[PROOF STEP]
show "ta' = ta'' \<and> x' = x'' \<and> m' = m''"
[PROOF STATE]
proof (prove)
using this:
jvm_thread_action_of_jvm_thread_action' ta' = jvm_thread_action_of_jvm_thread_action' ta'' \<and> jvm_thread_state_of_jvm_thread_state' x' = jvm_thread_state_of_jvm_thread_state' x'' \<and> m' = m''
ta' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta')
ta'' = jvm_thread_action'_of_jvm_thread_action P (jvm_thread_action_of_jvm_thread_action' ta'')
x' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x')
x'' = jvm_thread_state'_of_jvm_thread_state P (jvm_thread_state_of_jvm_thread_state' x'')

goal (1 subgoal):
 1. ta' = ta'' \<and> x' = x'' \<and> m' = m''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ta' = ta'' \<and> x' = x'' \<and> m' = m''

goal (1 subgoal):
 1. invariant3p (multithreaded_base.redT JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
qed(rule invariant3p_sc_jvm_state_invar[OF assms])
[PROOF STATE]
proof (state)
this:
multithreaded_base.deterministic JVM_final' (\<lambda>t xm ta x'm'. pred.eval (sc_mexec P t xm) (ta, x'm')) convert_RA (sc_jvm_state_invar P \<Phi>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma JVM_rr:
  assumes "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
  shows
  "sc_scheduler
     JVM_final' (sc_mexec P) convert_RA
     (JVM_rr.round_robin P n0) (pick_wakeup_via_sel (\<lambda>s P. rm_sel s (\<lambda>(k,v). P k v))) JVM_rr.round_robin_invar
     (sc_jvm_state_invar P \<Phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc_scheduler JVM_final' (sc_mexec P) convert_RA (JVM_rr.round_robin P n0) (pick_wakeup_via_sel (\<lambda>s P. rm.sel s (\<lambda>(k, v). P k v))) JVM_rr.round_robin_invar (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
unfolding sc_scheduler_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scheduler JVM_final' (sc_mexec P) convert_RA (JVM_rr.round_robin P n0) (pick_wakeup_via_sel (\<lambda>s P. rm.sel s (\<lambda>(x, y). P x y))) JVM_rr.round_robin_invar rm.\<alpha> rm.invar rm.lookup rm.update rm.\<alpha> rm.invar rm.lookup rm.update rm.delete rm.iteratei rs.\<alpha> rs.invar rs.memb rs.ins rs.delete (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
apply(rule JVM_rr.round_robin_scheduler)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_rr.\<alpha>.deterministic P (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
apply(rule sc_exec_deterministic[OF assms])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma JVM_rnd:
  assumes "wf_jvm_prog\<^bsub>\<Phi>\<^esub> P"
  shows
  "sc_scheduler
    JVM_final' (sc_mexec P) convert_RA
    (JVM_rnd.random_scheduler P) (pick_wakeup_via_sel (\<lambda>s P. rm_sel s (\<lambda>(k,v). P k v))) (\<lambda>_ _. True)
    (sc_jvm_state_invar P \<Phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc_scheduler JVM_final' (sc_mexec P) convert_RA (JVM_rnd.random_scheduler P) JVM_rnd.pick_wakeup (\<lambda>_ _. True) (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
unfolding sc_scheduler_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scheduler JVM_final' (sc_mexec P) convert_RA (JVM_rnd.random_scheduler P) JVM_rnd.pick_wakeup (\<lambda>_ _. True) rm.\<alpha> rm.invar rm.lookup rm.update rm.\<alpha> rm.invar rm.lookup rm.update rm.delete rm.iteratei rs.\<alpha> rs.invar rs.memb rs.ins rs.delete (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
apply(rule JVM_rnd.random_scheduler_scheduler)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. JVM_rr.\<alpha>.deterministic P (sc_jvm_state_invar P \<Phi>)
[PROOF STEP]
apply(rule sc_exec_deterministic[OF assms])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma modifies_yields_valid_register:
    assumes "k < length p"
    shows "modifies (p!k) < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. modifies (p ! k) < n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. modifies (p ! k) < n
[PROOF STEP]
have "instruction_register_check n (p!k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. instruction_register_check n (p ! k)
[PROOF STEP]
using valid_program assms list_all_length program_register_check.simps
[PROOF STATE]
proof (prove)
using this:
program_register_check p n
k < length p
list_all ?P ?xs = (\<forall>n<length ?xs. ?P (?xs ! n))
program_register_check ?p ?n = list_all (instruction_register_check ?n) ?p

goal (1 subgoal):
 1. instruction_register_check n (p ! k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
instruction_register_check n (p ! k)

goal (1 subgoal):
 1. modifies (p ! k) < n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
instruction_register_check n (p ! k)

goal (1 subgoal):
 1. modifies (p ! k) < n
[PROOF STEP]
by (cases "p!k", auto simp: n_gt_0)
[PROOF STATE]
proof (state)
this:
modifies (p ! k) < n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma euclid:
  "PRE (\<lambda>s::nat store. s ''x'' = x \<and> s ''y'' = y)
   (WHILE (\<lambda>s. s ''y'' \<noteq> 0) INV (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y)
    DO
     (''z'' ::= (\<lambda>s. s ''y''));
     (''y'' ::= (\<lambda>s. s ''x'' mod s ''y''));
     (''x'' ::= (\<lambda>s. s ''z''))
    OD)
   POST (\<lambda>s. s ''x'' = gcd x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PRE (\<lambda>s. s ''x'' = x \<and> s ''y'' = y) (WHILE (\<lambda>s. s ''y'' \<noteq> 0) INV (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) DO (''z'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ; (''x'' ::= (\<lambda>s. s ''z'')) OD) POST (\<lambda>s. s ''x'' = gcd x y)
[PROOF STEP]
apply (rule sH_while_inv)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>s. s ''x'' = x \<and> s ''y'' = y \<longrightarrow> gcd (s ''x'') (s ''y'') = gcd x y
 2. \<forall>s. gcd (s ''x'') (s ''y'') = gcd x y \<and> \<not> s ''y'' \<noteq> 0 \<longrightarrow> s ''x'' = gcd x y
 3. PRE (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) \<sqinter> (\<lambda>s. s ''y'' \<noteq> 0) (''z'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ; (''x'' ::= (\<lambda>s. s ''z'')) POST (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>s. gcd (s ''x'') (s ''y'') = gcd x y \<and> s ''y'' = 0 \<longrightarrow> s ''x'' = gcd x y
 2. PRE (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) \<sqinter> (\<lambda>s. 0 < s ''y'') (''z'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ; (''x'' ::= (\<lambda>s. s ''z'')) POST (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PRE (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) \<sqinter> (\<lambda>s. 0 < s ''y'') (''z'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ; (''x'' ::= (\<lambda>s. s ''z'')) POST (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y)
[PROOF STEP]
apply (intro rel_kat.H_seq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. rel_kat.H ?r9 (''x'' ::= (\<lambda>s. s ''z'')) \<lceil>\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y\<rceil>
 2. rel_kat.H ?r10 (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ?r9
 3. rel_kat.H \<lceil>(\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) \<sqinter> (\<lambda>s. 0 < s ''y'')\<rceil> (''z'' ::= (\<lambda>s. s ''y'')) ?r10
[PROOF STEP]
apply (subst H_assign, simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PRE (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) \<sqinter> (\<lambda>s. 0 < s ''y'') (''z'' ::= (\<lambda>s. s ''y'')) POST (\<lambda>s. gcd ((s(''y'' := s ''x'' mod s ''y'', ''x'' := (s(''y'' := s ''x'' mod s ''y'')) ''z'')) ''x'') ((s(''y'' := s ''x'' mod s ''y'', ''x'' := (s(''y'' := s ''x'' mod s ''y'')) ''z'')) ''y'') = gcd x y)
[PROOF STEP]
apply (intro H_assign_var)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s. ((\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) \<sqinter> (\<lambda>s. 0 < s ''y'')) s \<longrightarrow> gcd ((s(''z'' := s ''y'', ''y'' := (s(''z'' := s ''y'')) ''x'' mod (s(''z'' := s ''y'')) ''y'', ''x'' := (s(''z'' := s ''y'', ''y'' := (s(''z'' := s ''y'')) ''x'' mod (s(''z'' := s ''y'')) ''y'')) ''z'')) ''x'') ((s(''z'' := s ''y'', ''y'' := (s(''z'' := s ''y'')) ''x'' mod (s(''z'' := s ''y'')) ''y'', ''x'' := (s(''z'' := s ''y'', ''y'' := (s(''z'' := s ''y'')) ''x'' mod (s(''z'' := s ''y'')) ''y'')) ''z'')) ''y'') = gcd x y
[PROOF STEP]
using gcd_red_nat
[PROOF STATE]
proof (prove)
using this:
gcd ?x ?y = gcd ?y (?x mod ?y)

goal (1 subgoal):
 1. \<forall>s. ((\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) \<sqinter> (\<lambda>s. 0 < s ''y'')) s \<longrightarrow> gcd ((s(''z'' := s ''y'', ''y'' := (s(''z'' := s ''y'')) ''x'' mod (s(''z'' := s ''y'')) ''y'', ''x'' := (s(''z'' := s ''y'', ''y'' := (s(''z'' := s ''y'')) ''x'' mod (s(''z'' := s ''y'')) ''y'')) ''z'')) ''x'') ((s(''z'' := s ''y'', ''y'' := (s(''z'' := s ''y'')) ''x'' mod (s(''z'' := s ''y'')) ''y'', ''x'' := (s(''z'' := s ''y'', ''y'' := (s(''z'' := s ''y'')) ''x'' mod (s(''z'' := s ''y'')) ''y'')) ''z'')) ''y'') = gcd x y
[PROOF STEP]
by auto


[STATEMENT]
lemma maximum:
  "PRE (\<lambda>s:: nat store. True)
   (IF (\<lambda>s. s ''x'' \<ge> s ''y'')
    THEN (''z'' ::= (\<lambda>s. s ''x''))
    ELSE (''z'' ::= (\<lambda>s. s ''y''))
    FI)
   POST (\<lambda>s. s ''z'' = max (s ''x'') (s ''y''))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PRE (\<lambda>s. True) (IF (\<lambda>s. s ''y'' \<le> s ''x'') THEN (''z'' ::= (\<lambda>s. s ''x'')) ELSE (''z'' ::= (\<lambda>s. s ''y'')) FI) POST (\<lambda>s. s ''z'' = max (s ''x'') (s ''y''))
[PROOF STEP]
by auto


[STATEMENT]
lemma integer_division:
  "PRE (\<lambda>s::nat store. s ''x'' \<ge> 0)
    (''q'' ::= (\<lambda>s. 0));
    (''r'' ::= (\<lambda>s. s ''x''));
    (WHILE (\<lambda>s. s ''y'' \<le> s ''r'') INV (\<lambda>s. s ''x'' = s ''q'' * s ''y'' + s ''r'' \<and> s ''r'' \<ge> 0)
     DO
      (''q'' ::= (\<lambda>s. s ''q'' + 1));
      (''r'' ::= (\<lambda>s. s ''r'' - s ''y''))
      OD)
   POST (\<lambda>s. s ''x'' = s ''q'' * s ''y'' + s ''r'' \<and> s ''r'' \<ge> 0 \<and> s ''r'' < s ''y'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PRE (\<lambda>s. 0 \<le> s ''x'') (''q'' ::= (\<lambda>s. 0)) ; (''r'' ::= (\<lambda>s. s ''x'')) ; (WHILE (\<lambda>s. s ''y'' \<le> s ''r'') INV (\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r'' \<and> 0 \<le> s ''r'') DO (''q'' ::= (\<lambda>s. s ''q'' + 1)) ; (''r'' ::= (\<lambda>s. s ''r'' - s ''y'')) OD) POST (\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r'' \<and> 0 \<le> s ''r'' \<and> s ''r'' < s ''y'')
[PROOF STEP]
apply (intro rel_kat.H_seq, subst sH_while_inv, simp_all)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>s. ?P3 s \<longrightarrow> s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r''
 2. PRE (\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r'') \<sqinter> (\<lambda>s. s ''y'' \<le> s ''r'') (''q'' ::= (\<lambda>s. Suc (s ''q''))) ; (''r'' ::= (\<lambda>s. s ''r'' - s ''y'')) POST (\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r'')
 3. rel_kat.H ?r1 (''r'' ::= (\<lambda>s. s ''x'')) \<lceil>?P3\<rceil>
 4. rel_kat.H \<lceil>\<lambda>s. True\<rceil> (''q'' ::= (\<lambda>s. 0)) ?r1
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. PRE (\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r'') \<sqinter> (\<lambda>s. s ''y'' \<le> s ''r'') (''q'' ::= (\<lambda>s. Suc (s ''q''))) ; (''r'' ::= (\<lambda>s. s ''r'' - s ''y'')) POST (\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r'')
 2. rel_kat.H ?r1 (''r'' ::= (\<lambda>s. s ''x'')) \<lceil>\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r''\<rceil>
 3. rel_kat.H \<lceil>\<lambda>s. True\<rceil> (''q'' ::= (\<lambda>s. 0)) ?r1
[PROOF STEP]
apply (intro rel_kat.H_seq)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. rel_kat.H ?r23 (''r'' ::= (\<lambda>s. s ''r'' - s ''y'')) \<lceil>\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r''\<rceil>
 2. rel_kat.H \<lceil>(\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r'') \<sqinter> (\<lambda>s. s ''y'' \<le> s ''r'')\<rceil> (''q'' ::= (\<lambda>s. Suc (s ''q''))) ?r23
 3. rel_kat.H ?r1 (''r'' ::= (\<lambda>s. s ''x'')) \<lceil>\<lambda>s. s ''x'' = s ''q'' \<cdot> s ''y'' + s ''r''\<rceil>
 4. rel_kat.H \<lceil>\<lambda>s. True\<rceil> (''q'' ::= (\<lambda>s. 0)) ?r1
[PROOF STEP]
by (subst H_assign, simp_all)+


[STATEMENT]
lemma imp_reverse:
  "PRE (\<lambda>s:: 'a list store. s ''x'' = X)
   (''y'' ::= (\<lambda>s. []));
   (WHILE (\<lambda>s. s ''x'' \<noteq> []) INV (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X)
    DO
     (''y'' ::= (\<lambda>s. hd (s ''x'') # s ''y''));
     (''x'' ::= (\<lambda>s. tl (s ''x'')))
    OD)
   POST (\<lambda>s. s ''y''= rev X )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PRE (\<lambda>s. s ''x'' = X) (''y'' ::= (\<lambda>s. [])) ; (WHILE (\<lambda>s. s ''x'' \<noteq> []) INV (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X) DO (''y'' ::= (\<lambda>s. hd (s ''x'') # s ''y'')) ; (''x'' ::= (\<lambda>s. tl (s ''x''))) OD) POST (\<lambda>s. s ''y'' = rev X)
[PROOF STEP]
apply (intro rel_kat.H_seq, rule sH_while_inv)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<forall>s. ?P1 s \<longrightarrow> rev (s ''x'') @ s ''y'' = rev X
 2. \<forall>s. rev (s ''x'') @ s ''y'' = rev X \<and> \<not> s ''x'' \<noteq> [] \<longrightarrow> s ''y'' = rev X
 3. PRE (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X) \<sqinter> (\<lambda>s. s ''x'' \<noteq> []) (''y'' ::= (\<lambda>s. hd (s ''x'') # s ''y'')) ; (''x'' ::= (\<lambda>s. tl (s ''x''))) POST (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X)
 4. PRE (\<lambda>s. s ''x'' = X) (''y'' ::= (\<lambda>s. [])) POST ?P1
[PROOF STEP]
apply auto[2]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. PRE (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X) \<sqinter> (\<lambda>s. s ''x'' \<noteq> []) (''y'' ::= (\<lambda>s. hd (s ''x'') # s ''y'')) ; (''x'' ::= (\<lambda>s. tl (s ''x''))) POST (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X)
 2. PRE (\<lambda>s. s ''x'' = X) (''y'' ::= (\<lambda>s. [])) POST (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X)
[PROOF STEP]
apply (rule rel_kat.H_seq, rule H_assign_var)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>s. ?P17 s \<longrightarrow> rev ((s(''x'' := tl (s ''x''))) ''x'') @ (s(''x'' := tl (s ''x''))) ''y'' = rev X
 2. PRE (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X) \<sqinter> (\<lambda>s. s ''x'' \<noteq> []) (''y'' ::= (\<lambda>s. hd (s ''x'') # s ''y'')) POST ?P17
 3. PRE (\<lambda>s. s ''x'' = X) (''y'' ::= (\<lambda>s. [])) POST (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X)
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. PRE (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X) \<sqinter> (\<lambda>s. s ''x'' \<noteq> []) (''y'' ::= (\<lambda>s. hd (s ''x'') # s ''y'')) POST (\<lambda>s. rev (tl (s ''x'')) @ s ''y'' = rev X)
 2. PRE (\<lambda>s. s ''x'' = X) (''y'' ::= (\<lambda>s. [])) POST (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X)
[PROOF STEP]
apply (rule H_assign_var)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>s. ((\<lambda>s. rev (s ''x'') @ s ''y'' = rev X) \<sqinter> (\<lambda>s. s ''x'' \<noteq> [])) s \<longrightarrow> rev (tl ((s(''y'' := hd (s ''x'') # s ''y'')) ''x'')) @ (s(''y'' := hd (s ''x'') # s ''y'')) ''y'' = rev X
 2. PRE (\<lambda>s. s ''x'' = X) (''y'' ::= (\<lambda>s. [])) POST (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X)
[PROOF STEP]
apply (clarsimp, metis append.simps(1) append.simps(2) append_assoc hd_Cons_tl rev.simps(2))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PRE (\<lambda>s. s ''x'' = X) (''y'' ::= (\<lambda>s. [])) POST (\<lambda>s. rev (s ''x'') @ s ''y'' = rev X)
[PROOF STEP]
by simp


[STATEMENT]
lemma bags_in_V: "t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> bag t \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> bag t \<subseteq> V
[PROOF STEP]
using bags_union Sup_upper mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
\<Union> {bag t |t. t \<in> V\<^bsub>T\<^esub>} = V
?x \<in> ?A \<Longrightarrow> ?x \<le> Sup ?A
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> bag t \<subseteq> V
[PROOF STEP]
by blast


[STATEMENT]
lemma bag_finite: "t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> finite (bag t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> finite (bag t)
[PROOF STEP]
using bags_in_V finite_subset finite_vertex_set
[PROOF STATE]
proof (prove)
using this:
?t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> bag ?t \<subseteq> V
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A
finite V

goal (1 subgoal):
 1. t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> finite (bag t)
[PROOF STEP]
by blast


[STATEMENT]
lemma bag_bound_V: "t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> card (bag t) \<le> card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> card (bag t) \<le> card V
[PROOF STEP]
by (simp add: bags_in_V card_mono finite_vertex_set)


[STATEMENT]
lemma bag_bound_V_empty: "\<lbrakk> V = {}; t \<in> V\<^bsub>T\<^esub> \<rbrakk> \<Longrightarrow> card (bag t) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>V = {}; t \<in> V\<^bsub>T\<^esub>\<rbrakk> \<Longrightarrow> card (bag t) = 0
[PROOF STEP]
using bag_bound_V
[PROOF STATE]
proof (prove)
using this:
?t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> card (bag ?t) \<le> card V

goal (1 subgoal):
 1. \<lbrakk>V = {}; t \<in> V\<^bsub>T\<^esub>\<rbrakk> \<Longrightarrow> card (bag t) = 0
[PROOF STEP]
by auto


[STATEMENT]
lemma empty_tree_empty_V: "V\<^bsub>T\<^esub> = {} \<Longrightarrow> V = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V\<^bsub>T\<^esub> = {} \<Longrightarrow> V = {}
[PROOF STEP]
using bags_union
[PROOF STATE]
proof (prove)
using this:
\<Union> {bag t |t. t \<in> V\<^bsub>T\<^esub>} = V

goal (1 subgoal):
 1. V\<^bsub>T\<^esub> = {} \<Longrightarrow> V = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma bags_exist: "v \<in> V \<Longrightarrow> \<exists>t \<in> V\<^bsub>T\<^esub>. v \<in> bag t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> V \<Longrightarrow> \<exists>t\<in>V\<^bsub>T\<^esub>. v \<in> bag t
[PROOF STEP]
using bags_union
[PROOF STATE]
proof (prove)
using this:
\<Union> {bag t |t. t \<in> V\<^bsub>T\<^esub>} = V

goal (1 subgoal):
 1. v \<in> V \<Longrightarrow> \<exists>t\<in>V\<^bsub>T\<^esub>. v \<in> bag t
[PROOF STEP]
using UnionE mem_Collect_eq
[PROOF STATE]
proof (prove)
using this:
\<Union> {bag t |t. t \<in> V\<^bsub>T\<^esub>} = V
\<lbrakk>?A \<in> \<Union> ?C; \<And>X. \<lbrakk>?A \<in> X; X \<in> ?C\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. v \<in> V \<Longrightarrow> \<exists>t\<in>V\<^bsub>T\<^esub>. v \<in> bag t
[PROOF STEP]
by auto


[STATEMENT]
lemma bag_cards_nonempty: "V \<noteq> {} \<Longrightarrow> bag_cards \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> bag_cards \<noteq> {}
[PROOF STEP]
using bag_cards_finite empty_tree_empty_V empty_Collect_eq ex_in_conv
[PROOF STATE]
proof (prove)
using this:
finite bag_cards
V\<^bsub>T\<^esub> = {} \<Longrightarrow> V = {}
({} = Collect ?P) = (\<forall>x. \<not> ?P x)
(\<exists>x. x \<in> ?A) = (?A \<noteq> {})

goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> bag_cards \<noteq> {}
[PROOF STEP]
by blast


[STATEMENT]
lemma max_bag_card_in_bag_cards: "V \<noteq> {} \<Longrightarrow> max_bag_card \<in> bag_cards"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> max_bag_card \<in> bag_cards
[PROOF STEP]
unfolding max_bag_card_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> Max bag_cards \<in> bag_cards
[PROOF STEP]
using Max_in bag_cards_finite bag_cards_nonempty
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Max ?A \<in> ?A
finite bag_cards
V \<noteq> {} \<Longrightarrow> bag_cards \<noteq> {}

goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> Max bag_cards \<in> bag_cards
[PROOF STEP]
by auto


[STATEMENT]
lemma max_bag_card_lower_bound_bag: "t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> max_bag_card \<ge> card (bag t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> card (bag t) \<le> max_bag_card
[PROOF STEP]
by (metis (mono_tags, lifting) Max_ge bag_cards_finite max_bag_card_def mem_Collect_eq)


[STATEMENT]
lemma max_bag_card_lower_bound_1: assumes "V \<noteq> {}" shows "max_bag_card > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < max_bag_card
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < max_bag_card
[PROOF STEP]
have "\<exists>v \<in> V. \<exists>t \<in> V\<^bsub>T\<^esub>. v \<in> bag t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v\<in>V. \<exists>t\<in>V\<^bsub>T\<^esub>. v \<in> bag t
[PROOF STEP]
using \<open>V \<noteq> {}\<close> bags_union
[PROOF STATE]
proof (prove)
using this:
V \<noteq> {}
\<Union> {bag t |t. t \<in> V\<^bsub>T\<^esub>} = V

goal (1 subgoal):
 1. \<exists>v\<in>V. \<exists>t\<in>V\<^bsub>T\<^esub>. v \<in> bag t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>v\<in>V. \<exists>t\<in>V\<^bsub>T\<^esub>. v \<in> bag t

goal (1 subgoal):
 1. 0 < max_bag_card
[PROOF STEP]
thus "max_bag_card > 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>v\<in>V. \<exists>t\<in>V\<^bsub>T\<^esub>. v \<in> bag t

goal (1 subgoal):
 1. 0 < max_bag_card
[PROOF STEP]
unfolding max_bag_card_def
[PROOF STATE]
proof (prove)
using this:
\<exists>v\<in>V. \<exists>t\<in>V\<^bsub>T\<^esub>. v \<in> bag t

goal (1 subgoal):
 1. 0 < Max bag_cards
[PROOF STEP]
using bag_finite
    card_gt_0_iff emptyE Max_gr_iff[OF bag_cards_finite bag_cards_nonempty[OF assms]]
[PROOF STATE]
proof (prove)
using this:
\<exists>v\<in>V. \<exists>t\<in>V\<^bsub>T\<^esub>. v \<in> bag t
?t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> finite (bag ?t)
(0 < card ?A) = (?A \<noteq> {} \<and> finite ?A)
?a \<in> {} \<Longrightarrow> ?P
(?x < Max bag_cards) = (\<exists>a\<in>bag_cards. ?x < a)

goal (1 subgoal):
 1. 0 < Max bag_cards
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < max_bag_card

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma max_bag_card_upper_bound_V: "V \<noteq> {} \<Longrightarrow> max_bag_card \<le> card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> max_bag_card \<le> card V
[PROOF STEP]
unfolding max_bag_card_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> Max bag_cards \<le> card V
[PROOF STEP]
using Max_le_iff[OF bag_cards_finite bag_cards_nonempty] bag_bound_V
[PROOF STATE]
proof (prove)
using this:
V \<noteq> {} \<Longrightarrow> (Max bag_cards \<le> ?x) = (\<forall>a\<in>bag_cards. a \<le> ?x)
?t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> card (bag ?t) \<le> card V

goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> Max bag_cards \<le> card V
[PROOF STEP]
by blast


[STATEMENT]
lemma width_upper_bound_V: "V \<noteq> {} \<Longrightarrow> width < card V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> width < card V
[PROOF STEP]
unfolding width_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> (if V\<^bsub>T\<^esub> = {} then 0 else max_bag_card - 1) < card V
[PROOF STEP]
using max_bag_card_upper_bound_V max_bag_card_lower_bound_1
    diff_less empty_tree_empty_V le_neq_implies_less less_imp_diff_less zero_less_one
[PROOF STATE]
proof (prove)
using this:
V \<noteq> {} \<Longrightarrow> max_bag_card \<le> card V
V \<noteq> {} \<Longrightarrow> 0 < max_bag_card
\<lbrakk>0 < ?n; 0 < ?m\<rbrakk> \<Longrightarrow> ?m - ?n < ?m
V\<^bsub>T\<^esub> = {} \<Longrightarrow> V = {}
\<lbrakk>?m \<le> ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> ?m < ?n
?j < ?k \<Longrightarrow> ?j - ?n < ?k
(0::?'a) < (1::?'a)

goal (1 subgoal):
 1. V \<noteq> {} \<Longrightarrow> (if V\<^bsub>T\<^esub> = {} then 0 else max_bag_card - 1) < card V
[PROOF STEP]
by presburger


[STATEMENT]
lemma width_bound_V_le: "width \<le> card V - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. width \<le> card V - 1
[PROOF STEP]
using width_upper_bound_V width_V_empty
[PROOF STATE]
proof (prove)
using this:
V \<noteq> {} \<Longrightarrow> width < card V
V = {} \<Longrightarrow> width = 0

goal (1 subgoal):
 1. width \<le> card V - 1
[PROOF STEP]
by (cases "V = {}") auto


[STATEMENT]
lemma width_lower_bound_1:
  assumes "v\<rightarrow>w"
  shows "width \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> width
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> width
[PROOF STEP]
obtain t where t: "t \<in> V\<^bsub>T\<^esub>" "v \<in> bag t" "w \<in> bag t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> V\<^bsub>T\<^esub>; v \<in> bag t; w \<in> bag t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bags_edges assms
[PROOF STATE]
proof (prove)
using this:
?v \<rightarrow> ?w \<Longrightarrow> \<exists>t\<in>V\<^bsub>T\<^esub>. ?v \<in> bag t \<and> ?w \<in> bag t
v \<rightarrow> w

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> V\<^bsub>T\<^esub>; v \<in> bag t; w \<in> bag t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> V\<^bsub>T\<^esub>
v \<in> bag t
w \<in> bag t

goal (1 subgoal):
 1. 1 \<le> width
[PROOF STEP]
have "card (bag t) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (bag t) \<noteq> 0
[PROOF STEP]
using t(1,2) bag_finite card_0_eq empty_iff
[PROOF STATE]
proof (prove)
using this:
t \<in> V\<^bsub>T\<^esub>
v \<in> bag t
?t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> finite (bag ?t)
finite ?A \<Longrightarrow> (card ?A = 0) = (?A = {})
(?c \<in> {}) = False

goal (1 subgoal):
 1. card (bag t) \<noteq> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
card (bag t) \<noteq> 0

goal (1 subgoal):
 1. 1 \<le> width
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (bag t) \<noteq> 0

goal (1 subgoal):
 1. 1 \<le> width
[PROOF STEP]
have "card (bag t) \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (bag t) \<noteq> 1
[PROOF STEP]
using t(2,3) assms no_loops
[PROOF STATE]
proof (prove)
using this:
v \<in> bag t
w \<in> bag t
v \<rightarrow> w
(?v, ?v) \<notin> E

goal (1 subgoal):
 1. card (bag t) \<noteq> 1
[PROOF STEP]
by (metis One_nat_def card_Suc_eq empty_iff insertE)
[PROOF STATE]
proof (state)
this:
card (bag t) \<noteq> 1

goal (1 subgoal):
 1. 1 \<le> width
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (bag t) \<noteq> 0
card (bag t) \<noteq> 1
[PROOF STEP]
have "card (bag t) \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
card (bag t) \<noteq> 0
card (bag t) \<noteq> 1

goal (1 subgoal):
 1. 2 \<le> card (bag t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 \<le> card (bag t)

goal (1 subgoal):
 1. 1 \<le> width
[PROOF STEP]
hence "max_bag_card > 1"
[PROOF STATE]
proof (prove)
using this:
2 \<le> card (bag t)

goal (1 subgoal):
 1. 1 < max_bag_card
[PROOF STEP]
using t(1) max_bag_card_lower_bound_bag
[PROOF STATE]
proof (prove)
using this:
2 \<le> card (bag t)
t \<in> V\<^bsub>T\<^esub>
?t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> card (bag ?t) \<le> max_bag_card

goal (1 subgoal):
 1. 1 < max_bag_card
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
1 < max_bag_card

goal (1 subgoal):
 1. 1 \<le> width
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
1 < max_bag_card

goal (1 subgoal):
 1. 1 \<le> width
[PROOF STEP]
unfolding width_def
[PROOF STATE]
proof (prove)
using this:
1 < max_bag_card

goal (1 subgoal):
 1. 1 \<le> (if V\<^bsub>T\<^esub> = {} then 0 else max_bag_card - 1)
[PROOF STEP]
using t(1)
[PROOF STATE]
proof (prove)
using this:
1 < max_bag_card
t \<in> V\<^bsub>T\<^esub>

goal (1 subgoal):
 1. 1 \<le> (if V\<^bsub>T\<^esub> = {} then 0 else max_bag_card - 1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
1 \<le> width

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma treewidth_cards_treewidth:
  "\<exists>(T :: nat Graph) bag. TreeDecomposition G T bag \<and> treewidth = TreeDecomposition.width T bag"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T bag. TreeDecomposition G T bag \<and> treewidth = TreeDecomposition.width T bag
[PROOF STEP]
using Min_in treewidth_cards_finite treewidth_cards_nonempty treewidth_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?A \<noteq> {}\<rbrakk> \<Longrightarrow> Min ?A \<in> ?A
finite treewidth_cards
treewidth_cards \<noteq> {}
treewidth \<equiv> Min treewidth_cards

goal (1 subgoal):
 1. \<exists>T bag. TreeDecomposition G T bag \<and> treewidth = TreeDecomposition.width T bag
[PROOF STEP]
by fastforce


[STATEMENT]
lemma treewidth_upper_bound_ex:
  "\<lbrakk> TreeDecomposition G (T :: nat Graph) bag; TreeDecomposition.width T bag \<le> n \<rbrakk> \<Longrightarrow> treewidth \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TreeDecomposition G T bag; TreeDecomposition.width T bag \<le> n\<rbrakk> \<Longrightarrow> treewidth \<le> n
[PROOF STEP]
unfolding treewidth_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>TreeDecomposition G T bag; TreeDecomposition.width T bag \<le> n\<rbrakk> \<Longrightarrow> Min treewidth_cards \<le> n
[PROOF STEP]
by (metis (mono_tags, lifting) Min_le dual_order.trans mem_Collect_eq treewidth_cards_finite)


[STATEMENT]
lemma left_partI [intro]: "\<lbrakk> v \<in> bag u; u \<in> T.left_tree s t \<rbrakk> \<Longrightarrow> v \<in> left_part s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> bag u; u \<in> T.left_tree s t\<rbrakk> \<Longrightarrow> v \<in> left_part s t
[PROOF STEP]
unfolding left_part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<in> bag u; u \<in> T.left_tree s t\<rbrakk> \<Longrightarrow> v \<in> \<Union> {bag u |u. u \<in> T.left_tree s t}
[PROOF STEP]
by blast


[STATEMENT]
lemma left_part_in_V: "left_part s t \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_part s t \<subseteq> V
[PROOF STEP]
unfolding left_part_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {bag u |u. u \<in> T.left_tree s t} \<subseteq> V
[PROOF STEP]
using T.left_tree_in_V bags_in_V
[PROOF STATE]
proof (prove)
using this:
T.left_tree ?s ?t \<subseteq> V\<^bsub>T\<^esub>
?t \<in> V\<^bsub>T\<^esub> \<Longrightarrow> bag ?t \<subseteq> V

goal (1 subgoal):
 1. \<Union> {bag u |u. u \<in> T.left_tree s t} \<subseteq> V
[PROOF STEP]
by blast


[STATEMENT]
lemma vertex_subtreeI [intro]: "\<lbrakk> t \<in> V\<^bsub>T\<^esub>; v \<in> bag t \<rbrakk> \<Longrightarrow> t \<in> vertex_subtree v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> V\<^bsub>T\<^esub>; v \<in> bag t\<rbrakk> \<Longrightarrow> t \<in> vertex_subtree v
[PROOF STEP]
unfolding vertex_subtree_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> V\<^bsub>T\<^esub>; v \<in> bag t\<rbrakk> \<Longrightarrow> t \<in> {t \<in> V\<^bsub>T\<^esub>. v \<in> bag t}
[PROOF STEP]
by blast


[STATEMENT]
lemma vertex_subtree_connected:
  assumes v: "v \<in> V" and s: "s \<in> vertex_subtree v" and t: "t \<in> vertex_subtree v"
    and xs: "s \<leadsto>xs\<leadsto>\<^bsub>T\<^esub> t"
  shows "set xs \<subseteq> vertex_subtree v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> vertex_subtree v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> V
s \<in> vertex_subtree v
t \<in> vertex_subtree v
s \<leadsto>xs\<leadsto>\<^bsub>T\<^esub> t

goal (1 subgoal):
 1. set xs \<subseteq> vertex_subtree v
[PROOF STEP]
proof (induct xs arbitrary: s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>v \<in> V; s \<in> vertex_subtree v; t \<in> vertex_subtree v; s \<leadsto>[]\<leadsto>\<^bsub>T\<^esub> t\<rbrakk> \<Longrightarrow> set [] \<subseteq> vertex_subtree v
 2. \<And>a xs s. \<lbrakk>\<And>s. \<lbrakk>v \<in> V; s \<in> vertex_subtree v; t \<in> vertex_subtree v; s \<leadsto>xs\<leadsto>\<^bsub>T\<^esub> t\<rbrakk> \<Longrightarrow> set xs \<subseteq> vertex_subtree v; v \<in> V; s \<in> vertex_subtree v; t \<in> vertex_subtree v; s \<leadsto>(a # xs)\<leadsto>\<^bsub>T\<^esub> t\<rbrakk> \<Longrightarrow> set (a # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>v \<in> V; ?s \<in> vertex_subtree v; t \<in> vertex_subtree v; ?s \<leadsto>xs\<leadsto>\<^bsub>T\<^esub> t\<rbrakk> \<Longrightarrow> set xs \<subseteq> vertex_subtree v
v \<in> V
s \<in> vertex_subtree v
t \<in> vertex_subtree v
s \<leadsto>(x # xs)\<leadsto>\<^bsub>T\<^esub> t

goal (2 subgoals):
 1. \<And>s. \<lbrakk>v \<in> V; s \<in> vertex_subtree v; t \<in> vertex_subtree v; s \<leadsto>[]\<leadsto>\<^bsub>T\<^esub> t\<rbrakk> \<Longrightarrow> set [] \<subseteq> vertex_subtree v
 2. \<And>a xs s. \<lbrakk>\<And>s. \<lbrakk>v \<in> V; s \<in> vertex_subtree v; t \<in> vertex_subtree v; s \<leadsto>xs\<leadsto>\<^bsub>T\<^esub> t\<rbrakk> \<Longrightarrow> set xs \<subseteq> vertex_subtree v; v \<in> V; s \<in> vertex_subtree v; t \<in> vertex_subtree v; s \<leadsto>(a # xs)\<leadsto>\<^bsub>T\<^esub> t\<rbrakk> \<Longrightarrow> set (a # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
 2. \<not> ?P \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
assume "xs = []"
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. ?P \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
 2. \<not> ?P \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
using Cons.prems(3,4)
[PROOF STATE]
proof (prove)
using this:
xs = []
t \<in> vertex_subtree v
s \<leadsto>(x # xs)\<leadsto>\<^bsub>T\<^esub> t

goal (1 subgoal):
 1. set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (x # xs) \<subseteq> vertex_subtree v

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
assume "xs \<noteq> []"
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
hence "last xs = t"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []

goal (1 subgoal):
 1. last xs = t
[PROOF STEP]
using Cons.prems(4) last.simps
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
s \<leadsto>(x # xs)\<leadsto>\<^bsub>T\<^esub> t
last (?x # ?xs) = (if ?xs = [] then ?x else last ?xs)

goal (1 subgoal):
 1. last xs = t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
last xs = t

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last xs = t

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
have "T.path xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T.path xs
[PROOF STEP]
using Cons.prems(4) T.walk_tl
[PROOF STATE]
proof (prove)
using this:
s \<leadsto>(x # xs)\<leadsto>\<^bsub>T\<^esub> t
T.walk ?xs \<Longrightarrow> T.walk (tl ?xs)

goal (1 subgoal):
 1. T.path xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
T.path xs

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T.path xs

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
have "hd xs \<in> vertex_subtree v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd xs \<in> vertex_subtree v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hd xs \<in> V\<^bsub>T\<^esub>
 2. v \<in> bag (hd xs)
[PROOF STEP]
have "hd xs \<in> set (s \<leadsto>\<^bsub>T\<^esub> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd xs \<in> set (s \<leadsto>\<^bsub>T\<^esub> t)
[PROOF STEP]
using T.unique_connecting_path_unique
[PROOF STATE]
proof (prove)
using this:
?v \<leadsto>?xs\<leadsto>\<^bsub>T\<^esub> ?w \<Longrightarrow> ?xs = ?v \<leadsto>\<^bsub>T\<^esub> ?w

goal (1 subgoal):
 1. hd xs \<in> set (s \<leadsto>\<^bsub>T\<^esub> t)
[PROOF STEP]
using Cons.prems(4) \<open>xs \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
?v \<leadsto>?xs\<leadsto>\<^bsub>T\<^esub> ?w \<Longrightarrow> ?xs = ?v \<leadsto>\<^bsub>T\<^esub> ?w
s \<leadsto>(x # xs)\<leadsto>\<^bsub>T\<^esub> t
xs \<noteq> []

goal (1 subgoal):
 1. hd xs \<in> set (s \<leadsto>\<^bsub>T\<^esub> t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd xs \<in> set (s \<leadsto>\<^bsub>T\<^esub> t)

goal (2 subgoals):
 1. hd xs \<in> V\<^bsub>T\<^esub>
 2. v \<in> bag (hd xs)
[PROOF STEP]
hence "bag s \<inter> bag t \<subseteq> bag (hd xs)"
[PROOF STATE]
proof (prove)
using this:
hd xs \<in> set (s \<leadsto>\<^bsub>T\<^esub> t)

goal (1 subgoal):
 1. bag s \<inter> bag t \<subseteq> bag (hd xs)
[PROOF STEP]
using bags_continuous Cons.prems(4) T.connected_in_V
[PROOF STATE]
proof (prove)
using this:
hd xs \<in> set (s \<leadsto>\<^bsub>T\<^esub> t)
\<lbrakk>?s \<in> V\<^bsub>T\<^esub>; ?u \<in> V\<^bsub>T\<^esub>; ?t \<in> set (?s \<leadsto>\<^bsub>T\<^esub> ?u)\<rbrakk> \<Longrightarrow> bag ?s \<inter> bag ?u \<subseteq> bag ?t
s \<leadsto>(x # xs)\<leadsto>\<^bsub>T\<^esub> t
T.connected ?v ?w \<Longrightarrow> ?v \<in> V\<^bsub>T\<^esub>
T.connected ?v ?w \<Longrightarrow> ?w \<in> V\<^bsub>T\<^esub>

goal (1 subgoal):
 1. bag s \<inter> bag t \<subseteq> bag (hd xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bag s \<inter> bag t \<subseteq> bag (hd xs)

goal (2 subgoals):
 1. hd xs \<in> V\<^bsub>T\<^esub>
 2. v \<in> bag (hd xs)
[PROOF STEP]
thus "v \<in> bag (hd xs)"
[PROOF STATE]
proof (prove)
using this:
bag s \<inter> bag t \<subseteq> bag (hd xs)

goal (1 subgoal):
 1. v \<in> bag (hd xs)
[PROOF STEP]
using Cons.prems(2,3)
[PROOF STATE]
proof (prove)
using this:
bag s \<inter> bag t \<subseteq> bag (hd xs)
s \<in> vertex_subtree v
t \<in> vertex_subtree v

goal (1 subgoal):
 1. v \<in> bag (hd xs)
[PROOF STEP]
unfolding vertex_subtree_def
[PROOF STATE]
proof (prove)
using this:
bag s \<inter> bag t \<subseteq> bag (hd xs)
s \<in> {t \<in> V\<^bsub>T\<^esub>. v \<in> bag t}
t \<in> {t \<in> V\<^bsub>T\<^esub>. v \<in> bag t}

goal (1 subgoal):
 1. v \<in> bag (hd xs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> bag (hd xs)

goal (1 subgoal):
 1. hd xs \<in> V\<^bsub>T\<^esub>
[PROOF STEP]
show "hd xs \<in> V\<^bsub>T\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd xs \<in> V\<^bsub>T\<^esub>
[PROOF STEP]
using T.connected_in_V(1) \<open>xs \<noteq> []\<close> \<open>T.path xs\<close>
[PROOF STATE]
proof (prove)
using this:
T.connected ?v ?w \<Longrightarrow> ?v \<in> V\<^bsub>T\<^esub>
xs \<noteq> []
T.path xs

goal (1 subgoal):
 1. hd xs \<in> V\<^bsub>T\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
hd xs \<in> V\<^bsub>T\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
hd xs \<in> vertex_subtree v

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xs \<noteq> []
last xs = t
T.path xs
hd xs \<in> vertex_subtree v
[PROOF STEP]
have "set xs \<subseteq> vertex_subtree v"
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
last xs = t
T.path xs
hd xs \<in> vertex_subtree v

goal (1 subgoal):
 1. set xs \<subseteq> vertex_subtree v
[PROOF STEP]
using Cons.hyps Cons.prems(1,3)
[PROOF STATE]
proof (prove)
using this:
xs \<noteq> []
last xs = t
T.path xs
hd xs \<in> vertex_subtree v
\<lbrakk>v \<in> V; ?s \<in> vertex_subtree v; t \<in> vertex_subtree v; ?s \<leadsto>xs\<leadsto>\<^bsub>T\<^esub> t\<rbrakk> \<Longrightarrow> set xs \<subseteq> vertex_subtree v
v \<in> V
t \<in> vertex_subtree v

goal (1 subgoal):
 1. set xs \<subseteq> vertex_subtree v
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set xs \<subseteq> vertex_subtree v

goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> vertex_subtree v

goal (1 subgoal):
 1. set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
using Cons.prems(2,4)
[PROOF STATE]
proof (prove)
using this:
set xs \<subseteq> vertex_subtree v
s \<in> vertex_subtree v
s \<leadsto>(x # xs)\<leadsto>\<^bsub>T\<^esub> t

goal (1 subgoal):
 1. set (x # xs) \<subseteq> vertex_subtree v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (x # xs) \<subseteq> vertex_subtree v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set (x # xs) \<subseteq> vertex_subtree v

goal (1 subgoal):
 1. \<And>s. \<lbrakk>v \<in> V; s \<in> vertex_subtree v; t \<in> vertex_subtree v; s \<leadsto>[]\<leadsto>\<^bsub>T\<^esub> t\<rbrakk> \<Longrightarrow> set [] \<subseteq> vertex_subtree v
[PROOF STEP]
qed simp


[STATEMENT]
lemma vertex_in_separator:
  assumes st: "s \<rightarrow>\<^bsub>T\<^esub> t" and v: "v \<in> left_part s t" "v \<in> left_part t s"
  shows "v \<in> bag s" "v \<in> bag t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> bag s &&& v \<in> bag t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<in> bag s
 2. v \<in> bag t
[PROOF STEP]
obtain u u' where u: "v \<in> bag u" "u \<in> T.left_tree s t" "v \<in> bag u'" "u' \<in> T.left_tree t s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u u'. \<lbrakk>v \<in> bag u; u \<in> T.left_tree s t; v \<in> bag u'; u' \<in> T.left_tree t s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
v \<in> left_part s t
v \<in> left_part t s

goal (1 subgoal):
 1. (\<And>u u'. \<lbrakk>v \<in> bag u; u \<in> T.left_tree s t; v \<in> bag u'; u' \<in> T.left_tree t s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding left_part_def
[PROOF STATE]
proof (prove)
using this:
v \<in> \<Union> {bag u |u. u \<in> T.left_tree s t}
v \<in> \<Union> {bag u |u. u \<in> T.left_tree t s}

goal (1 subgoal):
 1. (\<And>u u'. \<lbrakk>v \<in> bag u; u \<in> T.left_tree s t; v \<in> bag u'; u' \<in> T.left_tree t s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> bag u
u \<in> T.left_tree s t
v \<in> bag u'
u' \<in> T.left_tree t s

goal (2 subgoals):
 1. v \<in> bag s
 2. v \<in> bag t
[PROOF STEP]
have "s \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')
[PROOF STEP]
using T.left_tree_separates st u
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s \<rightarrow>\<^bsub>T\<^esub> ?t; ?u \<in> T.left_tree ?s ?t; ?u' \<in> T.left_tree ?t ?s\<rbrakk> \<Longrightarrow> ?s \<in> set (?u \<leadsto>\<^bsub>T\<^esub> ?u')
s \<rightarrow>\<^bsub>T\<^esub> t
v \<in> bag u
u \<in> T.left_tree s t
v \<in> bag u'
u' \<in> T.left_tree t s

goal (1 subgoal):
 1. s \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')

goal (2 subgoals):
 1. v \<in> bag s
 2. v \<in> bag t
[PROOF STEP]
thus "v \<in> bag s"
[PROOF STATE]
proof (prove)
using this:
s \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')

goal (1 subgoal):
 1. v \<in> bag s
[PROOF STEP]
using bags_continuous u
[PROOF STATE]
proof (prove)
using this:
s \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')
\<lbrakk>?s \<in> V\<^bsub>T\<^esub>; ?u \<in> V\<^bsub>T\<^esub>; ?t \<in> set (?s \<leadsto>\<^bsub>T\<^esub> ?u)\<rbrakk> \<Longrightarrow> bag ?s \<inter> bag ?u \<subseteq> bag ?t
v \<in> bag u
u \<in> T.left_tree s t
v \<in> bag u'
u' \<in> T.left_tree t s

goal (1 subgoal):
 1. v \<in> bag s
[PROOF STEP]
by (meson IntI T.left_treeE subsetCE)
[PROOF STATE]
proof (state)
this:
v \<in> bag s

goal (1 subgoal):
 1. v \<in> bag t
[PROOF STEP]
have "t \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')
[PROOF STEP]
using T.left_tree_separates' st u
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s \<rightarrow>\<^bsub>T\<^esub> ?t; ?u \<in> T.left_tree ?s ?t; ?u' \<in> T.left_tree ?t ?s\<rbrakk> \<Longrightarrow> ?t \<in> set (?u \<leadsto>\<^bsub>T\<^esub> ?u')
s \<rightarrow>\<^bsub>T\<^esub> t
v \<in> bag u
u \<in> T.left_tree s t
v \<in> bag u'
u' \<in> T.left_tree t s

goal (1 subgoal):
 1. t \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
t \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')

goal (1 subgoal):
 1. v \<in> bag t
[PROOF STEP]
thus "v \<in> bag t"
[PROOF STATE]
proof (prove)
using this:
t \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')

goal (1 subgoal):
 1. v \<in> bag t
[PROOF STEP]
using bags_continuous u
[PROOF STATE]
proof (prove)
using this:
t \<in> set (u \<leadsto>\<^bsub>T\<^esub> u')
\<lbrakk>?s \<in> V\<^bsub>T\<^esub>; ?u \<in> V\<^bsub>T\<^esub>; ?t \<in> set (?s \<leadsto>\<^bsub>T\<^esub> ?u)\<rbrakk> \<Longrightarrow> bag ?s \<inter> bag ?u \<subseteq> bag ?t
v \<in> bag u
u \<in> T.left_tree s t
v \<in> bag u'
u' \<in> T.left_tree t s

goal (1 subgoal):
 1. v \<in> bag t
[PROOF STEP]
by (meson IntI T.left_treeE subsetCE)
[PROOF STATE]
proof (state)
this:
v \<in> bag t

goal:
No subgoals!
[PROOF STEP]
qed