[STATEMENT]
theorem HPhase1or2ReadThen_HInv4c:
  "\<lbrakk> HPhase1or2ReadThen s s' p d r; HInv4c s q\<rbrakk>
          \<Longrightarrow> HInv4c s' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>HPhase1or2ReadThen s s' p d r; HInv4c s q\<rbrakk> \<Longrightarrow> HInv4c s' q
[PROOF STEP]
by(blast dest: HPhase1or2ReadThen_HInv4c_p
                 HPhase1or2ReadThen_HInv4c_q)


[STATEMENT]
lemma HStartBallot_HInv4d_q:
  assumes act: "HStartBallot s  s' p"
  and inv: "HInv4d s q"
  and pnq: "p\<noteq>q"
  shows "HInv4d s' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
from act pnq
[PROOF STATE]
proof (chain)
picking this:
HStartBallot s s' p
p \<noteq> q
[PROOF STEP]
have disk': "disk s'=disk s"
   and dblock': "dblock s' q=dblock s q"
[PROOF STATE]
proof (prove)
using this:
HStartBallot s s' p
p \<noteq> q

goal (1 subgoal):
 1. disk s' = disk s &&& dblock s' q = dblock s q
[PROOF STEP]
by(auto simp add: StartBallot_def)
[PROOF STATE]
proof (state)
this:
disk s' = disk s
dblock s' q = dblock s q

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
from act pnq
[PROOF STATE]
proof (chain)
picking this:
HStartBallot s s' p
p \<noteq> q
[PROOF STEP]
have blocksRead': "\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q"
[PROOF STATE]
proof (prove)
using this:
HStartBallot s s' p
p \<noteq> q

goal (1 subgoal):
 1. \<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q
[PROOF STEP]
by(auto simp add: StartBallot_def InitializePhase_def allRdBlks_def)
[PROOF STATE]
proof (state)
this:
\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
with disk' dblock'
[PROOF STATE]
proof (chain)
picking this:
disk s' = disk s
dblock s' q = dblock s q
\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q
[PROOF STEP]
have "blocksOf s' q \<subseteq> blocksOf s q"
[PROOF STATE]
proof (prove)
using this:
disk s' = disk s
dblock s' q = dblock s q
\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q

goal (1 subgoal):
 1. blocksOf s' q \<subseteq> blocksOf s q
[PROOF STEP]
by(auto simp add: allRdBlks_def blocksOf_def rdBy_def, blast)
[PROOF STATE]
proof (state)
this:
blocksOf s' q \<subseteq> blocksOf s q

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
from subsetD[OF this] inv
[PROOF STATE]
proof (chain)
picking this:
?c \<in> blocksOf s' q \<Longrightarrow> ?c \<in> blocksOf s q
HInv4d s q
[PROOF STEP]
have "\<forall>bk\<in>blocksOf s' q.
           \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal(disk s d q)"
[PROOF STATE]
proof (prove)
using this:
?c \<in> blocksOf s' q \<Longrightarrow> ?c \<in> blocksOf s q
HInv4d s q

goal (1 subgoal):
 1. \<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)
[PROOF STEP]
by(auto simp add: HInv4d_def)
[PROOF STATE]
proof (state)
this:
\<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
with disk'
[PROOF STATE]
proof (chain)
picking this:
disk s' = disk s
\<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
disk s' = disk s
\<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
by(auto simp add: HInv4d_def)
[PROOF STATE]
proof (state)
this:
HInv4d s' q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HFail_HInv4d_q:
  assumes act: "HFail s  s' p"
  and inv: "HInv4d s q"
  and pnq: "p\<noteq>q"
  shows "HInv4d s' q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
from act pnq
[PROOF STATE]
proof (chain)
picking this:
HFail s s' p
p \<noteq> q
[PROOF STEP]
have disk': "disk s'=disk s"
   and dblock': "dblock s' q=dblock s q"
[PROOF STATE]
proof (prove)
using this:
HFail s s' p
p \<noteq> q

goal (1 subgoal):
 1. disk s' = disk s &&& dblock s' q = dblock s q
[PROOF STEP]
by(auto simp add: Fail_def)
[PROOF STATE]
proof (state)
this:
disk s' = disk s
dblock s' q = dblock s q

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
from act pnq
[PROOF STATE]
proof (chain)
picking this:
HFail s s' p
p \<noteq> q
[PROOF STEP]
have blocksRead': "\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q"
[PROOF STATE]
proof (prove)
using this:
HFail s s' p
p \<noteq> q

goal (1 subgoal):
 1. \<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q
[PROOF STEP]
by(auto simp add: Fail_def InitializePhase_def allRdBlks_def)
[PROOF STATE]
proof (state)
this:
\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
with disk' dblock'
[PROOF STATE]
proof (chain)
picking this:
disk s' = disk s
dblock s' q = dblock s q
\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q
[PROOF STEP]
have "blocksOf s' q \<subseteq> blocksOf s q"
[PROOF STATE]
proof (prove)
using this:
disk s' = disk s
dblock s' q = dblock s q
\<forall>q. allRdBlks s' q \<subseteq> allRdBlks s q

goal (1 subgoal):
 1. blocksOf s' q \<subseteq> blocksOf s q
[PROOF STEP]
by(auto simp add: allRdBlks_def blocksOf_def rdBy_def, blast)
[PROOF STATE]
proof (state)
this:
blocksOf s' q \<subseteq> blocksOf s q

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
from subsetD[OF this] inv
[PROOF STATE]
proof (chain)
picking this:
?c \<in> blocksOf s' q \<Longrightarrow> ?c \<in> blocksOf s q
HInv4d s q
[PROOF STEP]
have "\<forall>bk\<in>blocksOf s' q.
          \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal(disk s d q)"
[PROOF STATE]
proof (prove)
using this:
?c \<in> blocksOf s' q \<Longrightarrow> ?c \<in> blocksOf s q
HInv4d s q

goal (1 subgoal):
 1. \<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)
[PROOF STEP]
by(auto simp add: HInv4d_def)
[PROOF STATE]
proof (state)
this:
\<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
with disk'
[PROOF STATE]
proof (chain)
picking this:
disk s' = disk s
\<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
disk s' = disk s
\<forall>bk\<in>blocksOf s' q. \<exists>D\<in>MajoritySet. \<forall>d\<in>D. bal bk \<le> mbal (disk s d q)

goal (1 subgoal):
 1. HInv4d s' q
[PROOF STEP]
by(auto simp add: HInv4d_def)
[PROOF STATE]
proof (state)
this:
HInv4d s' q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma listI_assn_subst:
  assumes "i\<notin>I "" i<length xs "
  shows "listI_assn (insert i I) A (xs[i:=x1]) (xsi[i := x2]) = A x1 x2 * listI_assn I A xs xsi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. listI_assn (insert i I) A (xs[i := x1]) (xsi[i := x2]) = A x1 x2 * listI_assn I A xs xsi
[PROOF STEP]
by (smt (z3) assms(1) assms(2) length_list_update listI_assn_def listI_assn_insert nth_list_update_eq pure_false star_false_left star_false_right subst_not_in)


[STATEMENT]
lemma step_thread_Some_NoneD:
  assumes det: "\<alpha>.deterministic I"
  and step: "step_thread update_state s t' = \<lfloor>(t, None, \<sigma>')\<rfloor>"
  and invar: "state_invar s" "state_\<alpha> s \<in> I"
  shows "\<exists>x ln n. thr_\<alpha> (thr s) t = \<lfloor>(x, ln)\<rfloor> \<and> ln $ n > 0 \<and> \<not> waiting (ws_\<alpha> (wset s) t) \<and> may_acquire_all (locks s) t ln \<and> \<sigma>' = update_state (K$ [], [], [], [], [], convert_RA ln)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x ln n. thr_\<alpha> (thr s) t = \<lfloor>(x, ln)\<rfloor> \<and> 0 < ln $ n \<and> \<not> waiting (ws_\<alpha> (wset s) t) \<and> may_acquire_all (locks s) t ln \<and> \<sigma>' = update_state (K$ [], [], [], [], [], convert_RA ln)
[PROOF STEP]
using assms step_thread_correct(1)[OF det _ invar(1), of "\<lambda>_ _. True", of id update_state t']
[PROOF STATE]
proof (prove)
using this:
\<alpha>.deterministic I
step_thread update_state s t' = \<lfloor>(t, None, \<sigma>')\<rfloor>
state_invar s
state_\<alpha> s \<in> I
\<lbrakk>True; state_\<alpha> s \<in> I\<rbrakk> \<Longrightarrow> map_option (apsnd (apsnd id)) (step_thread update_state s t') = \<alpha>.step_thread (id \<circ> update_state) (state_\<alpha> s) t'

goal (1 subgoal):
 1. \<exists>x ln n. thr_\<alpha> (thr s) t = \<lfloor>(x, ln)\<rfloor> \<and> 0 < ln $ n \<and> \<not> waiting (ws_\<alpha> (wset s) t) \<and> may_acquire_all (locks s) t ln \<and> \<sigma>' = update_state (K$ [], [], [], [], [], convert_RA ln)
[PROOF STEP]
by(fastforce simp add: map_option.id dest: \<alpha>.step_thread_Some_NoneD[OF sym])


[STATEMENT]
lemma evimage_empty [simp]: "f \<inverse>\<^bsub>n\<^esub> {} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<inverse>\<^bsub>n\<^esub> {} = {}
[PROOF STEP]
by blast