[STATEMENT]
lemma red_external_ta_satisfiable:
  fixes final
  assumes "P,t \<turnstile> \<langle>a\<bullet>M(vs), h\<rangle> -ta\<rightarrow>ext \<langle>va, h'\<rangle>"
  shows "\<exists>s. final_thread.actions_ok final s t ta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s. final_thread.actions_ok final s t ta
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s. final_thread.actions_ok final s t ta
[PROOF STEP]
note [simp] =
    final_thread.actions_ok_iff final_thread.cond_action_oks.simps final_thread.cond_action_ok.simps
    lock_ok_las_def finfun_upd_apply wset_actions_ok_def has_lock_may_lock
    and [intro] =
    free_thread_id.intros
    and [cong] = conj_cong
[PROOF STATE]
proof (state)
this:
final_thread.actions_ok ?final ?s ?t ?ta = (lock_ok_las (locks ?s) ?t \<lbrace>?ta\<rbrace>\<^bsub>l\<^esub> \<and> thread_oks (thr ?s) \<lbrace>?ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks ?final ?s ?t \<lbrace>?ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset ?s) ?t \<lbrace>?ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts ?s) \<lbrace>?ta\<rbrace>\<^bsub>i\<^esub>)
final_thread.cond_action_oks ?final ?s ?t [] = True
final_thread.cond_action_oks ?final ?s ?t (?ct # ?cts) = (final_thread.cond_action_ok ?final ?s ?t ?ct \<and> final_thread.cond_action_oks ?final ?s ?t ?cts)
final_thread.cond_action_ok ?final ?s ?t (Join ?T) = (case thr ?s ?T of None \<Rightarrow> True | \<lfloor>(x, ln)\<rfloor> \<Rightarrow> ?t \<noteq> ?T \<and> ?final x \<and> ln = no_wait_locks \<and> wset ?s ?T = None)
final_thread.cond_action_ok ?final ?s ?t Yield = True
lock_ok_las ?ls ?t ?las \<equiv> \<forall>l. lock_actions_ok (?ls $ l) ?t (?las $ l)
?f(?a $:= ?b) $ ?a' = (if ?a = ?a' then ?b else ?f $ ?a')
wset_actions_ok ?ws ?t ?was = (if Notified \<in> set ?was then ?ws ?t = \<lfloor>PostWS WSNotified\<rfloor> else if WokenUp \<in> set ?was then ?ws ?t = \<lfloor>PostWS WSWokenUp\<rfloor> else ?ws ?t = None)
has_lock ?l ?t \<Longrightarrow> may_lock ?l ?t
?ts ?t = None \<Longrightarrow> free_thread_id ?ts ?t
\<lbrakk>?P = ?P'; ?P' \<Longrightarrow> ?Q = ?Q'\<rbrakk> \<Longrightarrow> (?P \<and> ?Q) = (?P' \<and> ?Q')

goal (1 subgoal):
 1. \<exists>s. final_thread.actions_ok final s t ta
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>

goal (1 subgoal):
 1. \<exists>s. final_thread.actions_ok final s t ta
[PROOF STEP]
by cases(fastforce intro: exI[where x="(K$ None)(a $:= \<lfloor>(t, 0)\<rfloor>)"] exI[where x="(K$ None)"])+
[PROOF STATE]
proof (state)
this:
\<exists>s. final_thread.actions_ok final s t ta

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma red_external_aggr_ta_satisfiable:
  fixes final
  assumes "(ta, va, h') \<in> red_external_aggr P t a M vs h"
  shows "\<exists>s. final_thread.actions_ok final s t ta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s. final_thread.actions_ok final s t ta
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s. final_thread.actions_ok final s t ta
[PROOF STEP]
note [simp] =
    final_thread.actions_ok_iff final_thread.cond_action_oks.simps final_thread.cond_action_ok.simps
    lock_ok_las_def finfun_upd_apply wset_actions_ok_def has_lock_may_lock
    and [intro] =
    free_thread_id.intros
    and [cong] = conj_cong
[PROOF STATE]
proof (state)
this:
final_thread.actions_ok ?final ?s ?t ?ta = (lock_ok_las (locks ?s) ?t \<lbrace>?ta\<rbrace>\<^bsub>l\<^esub> \<and> thread_oks (thr ?s) \<lbrace>?ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks ?final ?s ?t \<lbrace>?ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset ?s) ?t \<lbrace>?ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts ?s) \<lbrace>?ta\<rbrace>\<^bsub>i\<^esub>)
final_thread.cond_action_oks ?final ?s ?t [] = True
final_thread.cond_action_oks ?final ?s ?t (?ct # ?cts) = (final_thread.cond_action_ok ?final ?s ?t ?ct \<and> final_thread.cond_action_oks ?final ?s ?t ?cts)
final_thread.cond_action_ok ?final ?s ?t (Join ?T) = (case thr ?s ?T of None \<Rightarrow> True | \<lfloor>(x, ln)\<rfloor> \<Rightarrow> ?t \<noteq> ?T \<and> ?final x \<and> ln = no_wait_locks \<and> wset ?s ?T = None)
final_thread.cond_action_ok ?final ?s ?t Yield = True
lock_ok_las ?ls ?t ?las \<equiv> \<forall>l. lock_actions_ok (?ls $ l) ?t (?las $ l)
?f(?a $:= ?b) $ ?a' = (if ?a = ?a' then ?b else ?f $ ?a')
wset_actions_ok ?ws ?t ?was = (if Notified \<in> set ?was then ?ws ?t = \<lfloor>PostWS WSNotified\<rfloor> else if WokenUp \<in> set ?was then ?ws ?t = \<lfloor>PostWS WSWokenUp\<rfloor> else ?ws ?t = None)
has_lock ?l ?t \<Longrightarrow> may_lock ?l ?t
?ts ?t = None \<Longrightarrow> free_thread_id ?ts ?t
\<lbrakk>?P = ?P'; ?P' \<Longrightarrow> ?Q = ?Q'\<rbrakk> \<Longrightarrow> (?P \<and> ?Q) = (?P' \<and> ?Q')

goal (1 subgoal):
 1. \<exists>s. final_thread.actions_ok final s t ta
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(ta, va, h') \<in> red_external_aggr P t a M vs h
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(ta, va, h') \<in> red_external_aggr P t a M vs h

goal (1 subgoal):
 1. \<exists>s. final_thread.actions_ok final s t ta
[PROOF STEP]
by(fastforce simp add: red_external_aggr_def split_beta ta_upd_simps split: if_split_asm intro: exI[where x="Map.empty"] exI[where x="(K$ None)(a $:= \<lfloor>(t, 0)\<rfloor>)"] exI[where x="K$ None"])
[PROOF STATE]
proof (state)
this:
\<exists>s. final_thread.actions_ok final s t ta

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma heap_copy_loc_deterministic:
  assumes det: "deterministic_heap_ops"
  and copy: "heap_copy_loc a a' al h ops h'" "heap_copy_loc a a' al h ops' h''"
  shows "ops = ops' \<and> h' = h''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ops = ops' \<and> h' = h''
[PROOF STEP]
using copy
[PROOF STATE]
proof (prove)
using this:
heap_copy_loc a a' al h ops h'
heap_copy_loc a a' al h ops' h''

goal (1 subgoal):
 1. ops = ops' \<and> h' = h''
[PROOF STEP]
by(auto elim!: heap_copy_loc.cases dest: deterministic_heap_ops_readD[OF det] deterministic_heap_ops_writeD[OF det])


[STATEMENT]
lemma heap_copies_deterministic:
  assumes det: "deterministic_heap_ops"
  and copy: "heap_copies a a' als h ops h'" "heap_copies a a' als h ops' h''"
  shows "ops = ops' \<and> h' = h''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ops = ops' \<and> h' = h''
[PROOF STEP]
using copy
[PROOF STATE]
proof (prove)
using this:
heap_copies a a' als h ops h'
heap_copies a a' als h ops' h''

goal (1 subgoal):
 1. ops = ops' \<and> h' = h''
[PROOF STEP]
apply(induct arbitrary: ops' h'')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>h ops' h''. heap_copies a a' [] h ops' h'' \<Longrightarrow> [] = ops' \<and> h = h''
 2. \<And>al h ob h' als obs h'' ops' h''a. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>ops' h''a. heap_copies a a' als h' ops' h''a \<Longrightarrow> obs = ops' \<and> h'' = h''a; heap_copies a a' (al # als) h ops' h''a\<rbrakk> \<Longrightarrow> ob @ obs = ops' \<and> h'' = h''a
[PROOF STEP]
apply(fastforce elim!: heap_copies_cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' ops' h''a. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>ops' h''a. heap_copies a a' als h' ops' h''a \<Longrightarrow> obs = ops' \<and> h'' = h''a; heap_copies a a' (al # als) h ops' h''a\<rbrakk> \<Longrightarrow> ob @ obs = ops' \<and> h'' = h''a
[PROOF STEP]
apply(erule heap_copies_cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' ops' h''a oba h'a obsa. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>ops' h''a. heap_copies a a' als h' ops' h''a \<Longrightarrow> obs = ops' \<and> h'' = h''a; ops' = oba @ obsa; heap_copy_loc a a' al h oba h'a; heap_copies a a' als h'a obsa h''a\<rbrakk> \<Longrightarrow> ob @ obs = ops' \<and> h'' = h''a
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' ops' h''a oba h'a obsa. \<lbrakk>heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h''; \<And>ops' h''a. heap_copies a a' als h' ops' h''a \<Longrightarrow> obs = ops' \<and> h'' = h''a; heap_copy_loc a a' al h oba h'a; heap_copies a a' als h'a obsa h''a\<rbrakk> \<Longrightarrow> ob @ obs = oba @ obsa \<and> h'' = h''a
[PROOF STEP]
apply(drule (1) heap_copy_loc_deterministic[OF det])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' ops' h''a oba h'a obsa. \<lbrakk>heap_copies a a' als h' obs h''; \<And>ops' h''a. heap_copies a a' als h' ops' h''a \<Longrightarrow> obs = ops' \<and> h'' = h''a; heap_copy_loc a a' al h oba h'a; heap_copies a a' als h'a obsa h''a; ob = oba \<and> h' = h'a\<rbrakk> \<Longrightarrow> ob @ obs = oba @ obsa \<and> h'' = h''a
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' ops' h''a oba h'a obsa. \<lbrakk>heap_copies a a' als h'a obs h''; \<And>ops' h''a. heap_copies a a' als h'a ops' h''a \<Longrightarrow> obs = ops' \<and> h'' = h''a; heap_copy_loc a a' al h oba h'a; heap_copies a a' als h'a obsa h''a\<rbrakk> \<Longrightarrow> oba @ obs = oba @ obsa \<and> h'' = h''a
[PROOF STEP]
apply(unfold same_append_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>al h ob h' als obs h'' ops' h''a oba h'a obsa. \<lbrakk>heap_copies a a' als h'a obs h''; \<And>ops' h''a. heap_copies a a' als h'a ops' h''a \<Longrightarrow> obs = ops' \<and> h'' = h''a; heap_copy_loc a a' al h oba h'a; heap_copies a a' als h'a obsa h''a\<rbrakk> \<Longrightarrow> obs = obsa \<and> h'' = h''a
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma heap_clone_deterministic:
  assumes det: "deterministic_heap_ops"
  and clone: "heap_clone P h a h' obs" "heap_clone P h a h'' obs'"
  shows "h' = h'' \<and> obs = obs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h' = h'' \<and> obs = obs'
[PROOF STEP]
using clone
[PROOF STATE]
proof (prove)
using this:
heap_clone P h a h' obs
heap_clone P h a h'' obs'

goal (1 subgoal):
 1. h' = h'' \<and> obs = obs'
[PROOF STEP]
by(auto 4 4 elim!: heap_clone.cases dest: heap_copies_deterministic[OF det] deterministic_heap_ops_allocateD[OF det] has_fields_fun)


[STATEMENT]
lemma red_external_deterministic:
  fixes final
  assumes det: "deterministic_heap_ops"
  and red: "P,t \<turnstile> \<langle>a\<bullet>M(vs), (shr s)\<rangle> -ta\<rightarrow>ext \<langle>va, h'\<rangle>" "P,t \<turnstile> \<langle>a\<bullet>M(vs), (shr s)\<rangle> -ta'\<rightarrow>ext \<langle>va', h''\<rangle>"
  and aok: "final_thread.actions_ok final s t ta" "final_thread.actions_ok final s t ta'"
  shows "ta = ta' \<and> va = va' \<and> h' = h''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ta = ta' \<and> va = va' \<and> h' = h''
[PROOF STEP]
using red aok
[PROOF STATE]
proof (prove)
using this:
P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>
final_thread.actions_ok final s t ta
final_thread.actions_ok final s t ta'

goal (1 subgoal):
 1. ta = ta' \<and> va = va' \<and> h' = h''
[PROOF STEP]
apply(simp add: final_thread.actions_ok_iff lock_ok_las_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>; P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
[PROOF STEP]
apply(erule red_external.cases)
[PROOF STATE]
proof (prove)
goal (26 subgoals):
 1. \<And>C. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 2. \<And>C. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 3. \<And>C. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 4. \<And>C. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 5. \<And>C. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 6. \<And>C. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 7. \<And>C. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 8. \<And>C. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 9. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = shr s\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 10. \<lbrakk>P,t \<turnstile> \<langle>a\<bullet>M(vs),shr s\<rangle> -ta'\<rightarrow>ext \<langle>va',h''\<rangle>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = shr s\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
A total of 26 subgoals...
[PROOF STEP]
apply(erule_tac [!] red_external.cases)
[PROOF STATE]
proof (prove)
goal (676 subgoals):
 1. \<And>C Ca. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = start; vs = []; ta' = \<lbrace>NewThread (addr2thread_id a) (Ca, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va' = RetVal Unit; h'' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type Ca\<rfloor>; P \<turnstile> Ca \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 2. \<And>C Ca. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = start; vs = []; ta' = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va' = RetEXC IllegalThreadState; h'' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type Ca\<rfloor>; P \<turnstile> Ca \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 3. \<And>C Ca. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = join; vs = []; ta' = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va' = RetVal Unit; h'' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type Ca\<rfloor>; P \<turnstile> Ca \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 4. \<And>C Ca. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = join; vs = []; ta' = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va' = RetEXC InterruptedException; h'' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type Ca\<rfloor>; P \<turnstile> Ca \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 5. \<And>C Ca. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = interrupt; vs = []; ta' = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va' = RetVal Unit; h'' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type Ca\<rfloor>; P \<turnstile> Ca \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 6. \<And>C Ca. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = interrupt; vs = []; ta' = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va' = RetVal Unit; h'' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type Ca\<rfloor>; P \<turnstile> Ca \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 7. \<And>C Ca. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = isInterrupted; vs = []; ta' = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va' = RetVal (Bool True); h'' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type Ca\<rfloor>; P \<turnstile> Ca \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 8. \<And>C Ca. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = isInterrupted; vs = []; ta' = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va' = RetVal (Bool False); h'' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type Ca\<rfloor>; P \<turnstile> Ca \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 9. \<And>C. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = wait; vs = []; ta' = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va' = RetEXC InterruptedException; h'' = shr s\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
 10. \<And>C. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta\<rbrace>\<^bsub>i\<^esub>; (\<forall>l. lock_actions_ok (locks s $ l) t (\<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> $ l)) \<and> thread_oks (thr s) \<lbrace>ta'\<rbrace>\<^bsub>t\<^esub> \<and> final_thread.cond_action_oks final s t \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> wset_actions_ok (wset s) t \<lbrace>ta'\<rbrace>\<^bsub>w\<^esub> \<and> interrupt_actions_ok (interrupts s) \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) (shr s), ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = shr s; typeof_addr (shr s) a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread; M = wait; vs = []; ta' = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va' = RetStaySame; h'' = shr s\<rbrakk> \<Longrightarrow> ta = ta' \<and> va = va' \<and> h' = h''
A total of 676 subgoals...
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (34 subgoals):
 1. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [Unlock, Lock]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset s t = None \<and> t \<in> interrupts s; \<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [UnlockFail]) $ l); ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = shr s; M = wait; vs = []; ta' = \<lbrace>(UnlockFail, a)\<rbrace>; va' = RetEXC IllegalMonitorState; h'' = shr s\<rbrakk> \<Longrightarrow> \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace> = \<lbrace>(UnlockFail, a)\<rbrace> \<and> addr_of_sys_xcpt InterruptedException = addr_of_sys_xcpt IllegalMonitorState
 2. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [Unlock, Lock]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset s t = None \<and> t \<in> interrupts s; wset_actions_ok (wset s) t [Notified]; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = shr s; M = wait; vs = []; ta' = \<lbrace>Notified\<rbrace>; va' = RetVal Unit; h'' = shr s\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [Unlock, Lock]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset s t = None \<and> t \<in> interrupts s; wset_actions_ok (wset s) t [WokenUp]; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = shr s; M = wait; vs = []; ta' = \<lbrace>WokenUp, ClearInterrupt t, ObsInterrupted t\<rbrace>; va' = RetEXC InterruptedException; h'' = shr s\<rbrakk> \<Longrightarrow> \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace> = \<lbrace>WokenUp, ClearInterrupt t, ObsInterrupted t\<rbrace>
 4. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [Unlock, Lock, ReleaseAcquire]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset_actions_ok (wset s) t [Suspend a] \<and> t \<notin> interrupts s; (\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [UnlockFail]) $ l)) \<and> wset s t = None; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = shr s; M = wait; vs = []; ta' = \<lbrace>(UnlockFail, a)\<rbrace>; va' = RetEXC IllegalMonitorState; h'' = shr s\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [Unlock, Lock, ReleaseAcquire]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset_actions_ok (wset s) t [Suspend a] \<and> t \<notin> interrupts s; wset_actions_ok (wset s) t [Notified]; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = shr s; M = wait; vs = []; ta' = \<lbrace>Notified\<rbrace>; va' = RetVal Unit; h'' = shr s\<rbrakk> \<Longrightarrow> False
 6. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [Unlock, Lock, ReleaseAcquire]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset_actions_ok (wset s) t [Suspend a] \<and> t \<notin> interrupts s; wset_actions_ok (wset s) t [WokenUp]; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = shr s; M = wait; vs = []; ta' = \<lbrace>WokenUp, ClearInterrupt t, ObsInterrupted t\<rbrace>; va' = RetEXC InterruptedException; h'' = shr s\<rbrakk> \<Longrightarrow> False
 7. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [Unlock, Lock, ReleaseAcquire]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset_actions_ok (wset s) t [Suspend a] \<and> t \<notin> interrupts s; wset s t = None; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = shr s; M = wait; vs = []; ta' = \<lbrace>(Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va' = RetVal Unit; h'' = shr s; spurious_wakeups\<rbrakk> \<Longrightarrow> False
 8. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [UnlockFail]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset s t = None; (\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [Unlock, Lock]) $ l)) \<and> t \<in> interrupts s; ta = \<lbrace>(UnlockFail, a)\<rbrace>; va = RetEXC IllegalMonitorState; h' = shr s; M = wait; vs = []; ta' = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va' = RetEXC InterruptedException; h'' = shr s\<rbrakk> \<Longrightarrow> \<lbrace>(UnlockFail, a)\<rbrace> = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace> \<and> addr_of_sys_xcpt IllegalMonitorState = addr_of_sys_xcpt InterruptedException
 9. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [UnlockFail]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset s t = None; (\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [Unlock, Lock, ReleaseAcquire]) $ l)) \<and> wset_actions_ok (wset s) t [Suspend a] \<and> t \<notin> interrupts s; ta = \<lbrace>(UnlockFail, a)\<rbrace>; va = RetEXC IllegalMonitorState; h' = shr s; M = wait; vs = []; ta' = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va' = RetStaySame; h'' = shr s\<rbrakk> \<Longrightarrow> False
 10. \<lbrakk>(\<forall>l. lock_actions_ok (locks s $ l) t ((K$ [])(a $:= [UnlockFail]) $ l)) \<and> final_thread.cond_action_oks final s t [] \<and> wset s t = None; wset_actions_ok (wset s) t [Notified]; ta = \<lbrace>(UnlockFail, a)\<rbrace>; va = RetEXC IllegalMonitorState; h' = shr s; M = wait; vs = []; ta' = \<lbrace>Notified\<rbrace>; va' = RetVal Unit; h'' = shr s\<rbrakk> \<Longrightarrow> False
A total of 34 subgoals...
[PROOF STEP]
apply(auto simp add: finfun_upd_apply wset_actions_ok_def dest: heap_clone_deterministic[OF det] split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wset s t = None; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = shr s; M = wait; vs = []; ta' = \<lbrace>(Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va' = RetVal Unit; h'' = shr s; spurious_wakeups; final_thread.cond_action_oks final s t []; t \<notin> interrupts s; has_lock (locks s $ a) t; may_lock (locks s $ a) t\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ta = \<lbrace>(Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetVal Unit; h' = shr s; spurious_wakeups; M = wait; vs = []; ta' = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va' = RetStaySame; h'' = shr s; final_thread.cond_action_oks final s t []; wset s t = None; t \<notin> interrupts s; has_lock (locks s $ a) t; may_lock (locks s $ a) t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using deterministic_heap_ops_no_spurious_wakeups[OF det]
[PROOF STATE]
proof (prove)
using this:
\<not> spurious_wakeups

goal (2 subgoals):
 1. \<lbrakk>wset s t = None; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = shr s; M = wait; vs = []; ta' = \<lbrace>(Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va' = RetVal Unit; h'' = shr s; spurious_wakeups; final_thread.cond_action_oks final s t []; t \<notin> interrupts s; has_lock (locks s $ a) t; may_lock (locks s $ a) t\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>ta = \<lbrace>(Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetVal Unit; h' = shr s; spurious_wakeups; M = wait; vs = []; ta' = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va' = RetStaySame; h'' = shr s; final_thread.cond_action_oks final s t []; wset s t = None; t \<notin> interrupts s; has_lock (locks s $ a) t; may_lock (locks s $ a) t\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sha1blocklen: "length (sha1block b x A B C D E) = 160"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (sha1block b x A B C D E) = 160
[PROOF STEP]
proof (induct b x A B C D E rule: sha1block.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b A B C D E. length (sha1block b [] A B C D E) = 160
 2. \<And>b v va A B C D E. (\<And>x xa xb xc xd xe. \<lbrakk>x = sha1compressstart 79 b A B C D E; xa = addmod32 A (select x 0 31); xb = addmod32 B (select x 32 63); xc = addmod32 C (select x 64 95); xd = addmod32 D (select x 96 127); xe = addmod32 E (select x 128 159)\<rbrakk> \<Longrightarrow> length (sha1block (getblock (v # va)) (delblock (v # va)) xa xb xc xd E) = 160) \<Longrightarrow> length (sha1block b (v # va) A B C D E) = 160
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>b A B C D E. length (sha1block b [] A B C D E) = 160
 2. \<And>b v va A B C D E. (\<And>x xa xb xc xd xe. \<lbrakk>x = sha1compressstart 79 b A B C D E; xa = addmod32 A (select x 0 31); xb = addmod32 B (select x 32 63); xc = addmod32 C (select x 64 95); xd = addmod32 D (select x 96 127); xe = addmod32 E (select x 128 159)\<rbrakk> \<Longrightarrow> length (sha1block (getblock (v # va)) (delblock (v # va)) xa xb xc xd E) = 160) \<Longrightarrow> length (sha1block b (v # va) A B C D E) = 160
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (sha1block b_ [] A_ B_ C_ D_ E_) = 160
[PROOF STEP]
by (simp add: Let_def addmod32len)
[PROOF STATE]
proof (state)
this:
length (sha1block b_ [] A_ B_ C_ D_ E_) = 160

goal (1 subgoal):
 1. \<And>b v va A B C D E. (\<And>x xa xb xc xd xe. \<lbrakk>x = sha1compressstart 79 b A B C D E; xa = addmod32 A (select x 0 31); xb = addmod32 B (select x 32 63); xc = addmod32 C (select x 64 95); xd = addmod32 D (select x 96 127); xe = addmod32 E (select x 128 159)\<rbrakk> \<Longrightarrow> length (sha1block (getblock (v # va)) (delblock (v # va)) xa xb xc xd E) = 160) \<Longrightarrow> length (sha1block b (v # va) A B C D E) = 160
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>b v va A B C D E. (\<And>x xa xb xc xd xe. \<lbrakk>x = sha1compressstart 79 b A B C D E; xa = addmod32 A (select x 0 31); xb = addmod32 B (select x 32 63); xc = addmod32 C (select x 64 95); xd = addmod32 D (select x 96 127); xe = addmod32 E (select x 128 159)\<rbrakk> \<Longrightarrow> length (sha1block (getblock (v # va)) (delblock (v # va)) xa xb xc xd E) = 160) \<Longrightarrow> length (sha1block b (v # va) A B C D E) = 160
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = sha1compressstart 79 b_ A_ B_ C_ D_ E_; ?xa = addmod32 A_ (select ?x 0 31); ?xb = addmod32 B_ (select ?x 32 63); ?xc = addmod32 C_ (select ?x 64 95); ?xd = addmod32 D_ (select ?x 96 127); ?xe = addmod32 E_ (select ?x 128 159)\<rbrakk> \<Longrightarrow> length (sha1block (getblock (v_ # va_)) (delblock (v_ # va_)) ?xa ?xb ?xc ?xd E_) = 160

goal (1 subgoal):
 1. \<And>b v va A B C D E. (\<And>x xa xb xc xd xe. \<lbrakk>x = sha1compressstart 79 b A B C D E; xa = addmod32 A (select x 0 31); xb = addmod32 B (select x 32 63); xc = addmod32 C (select x 64 95); xd = addmod32 D (select x 96 127); xe = addmod32 E (select x 128 159)\<rbrakk> \<Longrightarrow> length (sha1block (getblock (v # va)) (delblock (v # va)) xa xb xc xd E) = 160) \<Longrightarrow> length (sha1block b (v # va) A B C D E) = 160
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x = sha1compressstart 79 b_ A_ B_ C_ D_ E_; ?xa = addmod32 A_ (select ?x 0 31); ?xb = addmod32 B_ (select ?x 32 63); ?xc = addmod32 C_ (select ?x 64 95); ?xd = addmod32 D_ (select ?x 96 127); ?xe = addmod32 E_ (select ?x 128 159)\<rbrakk> \<Longrightarrow> length (sha1block (getblock (v_ # va_)) (delblock (v_ # va_)) ?xa ?xb ?xc ?xd E_) = 160
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x = sha1compressstart 79 b_ A_ B_ C_ D_ E_; ?xa = addmod32 A_ (select ?x 0 31); ?xb = addmod32 B_ (select ?x 32 63); ?xc = addmod32 C_ (select ?x 64 95); ?xd = addmod32 D_ (select ?x 96 127); ?xe = addmod32 E_ (select ?x 128 159)\<rbrakk> \<Longrightarrow> length (sha1block (getblock (v_ # va_)) (delblock (v_ # va_)) ?xa ?xb ?xc ?xd E_) = 160

goal (1 subgoal):
 1. length (sha1block b_ (v_ # va_) A_ B_ C_ D_ E_) = 160
[PROOF STEP]
by (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
length (sha1block b_ (v_ # va_) A_ B_ C_ D_ E_) = 160

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sha1len: "length (sha1 m) = 160"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (sha1 m) = 160
[PROOF STEP]
unfolding sha1 Let_def sha1blocklen
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 160 = 160
[PROOF STEP]
..


[STATEMENT]
lemma move_keeps_length:"\<parallel>ext v\<parallel> = \<parallel>ext (move ts ts' v)\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>ext v\<parallel> = \<parallel>ext (move ts ts' v)\<parallel>
[PROOF STEP]
using real_int.shift_keeps_length
[PROOF STATE]
proof (prove)
using this:
\<parallel>?r\<parallel> = \<parallel> shift ?r ?x\<parallel>

goal (1 subgoal):
 1. \<parallel>ext v\<parallel> = \<parallel>ext (move ts ts' v)\<parallel>
[PROOF STEP]
by (simp add: move_def)


[STATEMENT]
lemma move_keeps_lanes:"lan v = lan (move ts ts' v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lan v = lan (move ts ts' v)
[PROOF STEP]
using move_def
[PROOF STATE]
proof (prove)
using this:
move ?ts ?ts' ?v = \<lparr>ext =  shift ext ?v pos ?ts' (own ?v) - pos ?ts (own ?v), lan = lan ?v, own = own ?v\<rparr>

goal (1 subgoal):
 1. lan v = lan (move ts ts' v)
[PROOF STEP]
by simp


[STATEMENT]
lemma move_keeps_owner:"own v = own (move ts ts' v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. own v = own (move ts ts' v)
[PROOF STEP]
using move_def
[PROOF STATE]
proof (prove)
using this:
move ?ts ?ts' ?v = \<lparr>ext =  shift ext ?v pos ?ts' (own ?v) - pos ?ts (own ?v), lan = lan ?v, own = own ?v\<rparr>

goal (1 subgoal):
 1. own v = own (move ts ts' v)
[PROOF STEP]
by simp


[STATEMENT]
lemma move_nothing :"move ts ts v = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. move ts ts v = v
[PROOF STEP]
using real_int.shift_zero move_def
[PROOF STATE]
proof (prove)
using this:
 shift ?r 0 = ?r
move ?ts ?ts' ?v = \<lparr>ext =  shift ext ?v pos ?ts' (own ?v) - pos ?ts (own ?v), lan = lan ?v, own = own ?v\<rparr>

goal (1 subgoal):
 1. move ts ts v = v
[PROOF STEP]
by simp


[STATEMENT]
lemma move_trans:
  "(ts \<^bold>\<Rightarrow> ts') \<and> (ts' \<^bold>\<Rightarrow>ts'') \<longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts \<^bold>\<Rightarrow> ts' \<and> ts' \<^bold>\<Rightarrow> ts'' \<longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ts \<^bold>\<Rightarrow> ts' \<and> ts' \<^bold>\<Rightarrow> ts'' \<Longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
assume assm:"(ts \<^bold>\<Rightarrow> ts') \<and> (ts' \<^bold>\<Rightarrow>ts'')"
[PROOF STATE]
proof (state)
this:
ts \<^bold>\<Rightarrow> ts' \<and> ts' \<^bold>\<Rightarrow> ts''

goal (1 subgoal):
 1. ts \<^bold>\<Rightarrow> ts' \<and> ts' \<^bold>\<Rightarrow> ts'' \<Longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
have
    "(pos ts'' (own v)) - pos ts (own v)
      = (pos ts'' (own v) + pos ts' (own v)) - ( pos ts (own v) + pos ts' (own v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pos ts'' (own v) - pos ts (own v) = pos ts'' (own v) + pos ts' (own v) - (pos ts (own v) + pos ts' (own v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pos ts'' (own v) - pos ts (own v) = pos ts'' (own v) + pos ts' (own v) - (pos ts (own v) + pos ts' (own v))

goal (1 subgoal):
 1. ts \<^bold>\<Rightarrow> ts' \<and> ts' \<^bold>\<Rightarrow> ts'' \<Longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
have
    "move ts' ts'' (move ts ts' v) =
    \<lparr> ext =
    shift (ext (move ts ts' v))
      (pos ts'' (own (move ts ts' v)) - pos ts' (own (move ts ts' v))),
     lan = lan (move ts ts' v),
     own = own (move ts ts' v) \<rparr> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own (move ts ts' v)) - pos ts' (own (move ts ts' v)), lan = lan (move ts ts' v), own = own (move ts ts' v)\<rparr>
[PROOF STEP]
using move_def
[PROOF STATE]
proof (prove)
using this:
move ?ts ?ts' ?v = \<lparr>ext =  shift ext ?v pos ?ts' (own ?v) - pos ?ts (own ?v), lan = lan ?v, own = own ?v\<rparr>

goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own (move ts ts' v)) - pos ts' (own (move ts ts' v)), lan = lan (move ts ts' v), own = own (move ts ts' v)\<rparr>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own (move ts ts' v)) - pos ts' (own (move ts ts' v)), lan = lan (move ts ts' v), own = own (move ts ts' v)\<rparr>

goal (1 subgoal):
 1. ts \<^bold>\<Rightarrow> ts' \<and> ts' \<^bold>\<Rightarrow> ts'' \<Longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
hence "move ts' ts'' (move ts ts' v) =
 \<lparr> ext = shift (ext (move ts ts' v)) (pos ts'' (own v) - pos ts' (own  v)),
  lan = lan  v, own = own  v \<rparr> "
[PROOF STATE]
proof (prove)
using this:
move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own (move ts ts' v)) - pos ts' (own (move ts ts' v)), lan = lan (move ts ts' v), own = own (move ts ts' v)\<rparr>

goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own v) - pos ts' (own v), lan = lan v, own = own v\<rparr>
[PROOF STEP]
using move_def
[PROOF STATE]
proof (prove)
using this:
move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own (move ts ts' v)) - pos ts' (own (move ts ts' v)), lan = lan (move ts ts' v), own = own (move ts ts' v)\<rparr>
move ?ts ?ts' ?v = \<lparr>ext =  shift ext ?v pos ?ts' (own ?v) - pos ?ts (own ?v), lan = lan ?v, own = own ?v\<rparr>

goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own v) - pos ts' (own v), lan = lan v, own = own v\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own v) - pos ts' (own v), lan = lan v, own = own v\<rparr>

goal (1 subgoal):
 1. ts \<^bold>\<Rightarrow> ts' \<and> ts' \<^bold>\<Rightarrow> ts'' \<Longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own v) - pos ts' (own v), lan = lan v, own = own v\<rparr>
[PROOF STEP]
show "move ts' ts'' (move ts ts' v) = move ts ts'' v"
[PROOF STATE]
proof (prove)
using this:
move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own v) - pos ts' (own v), lan = lan v, own = own v\<rparr>

goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own v) - pos ts' (own v), lan = lan v, own = own v\<rparr> \<Longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
have f2: "\<forall>x0 x1. (x1::real) + x0 = x0 + x1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x0 x1. x1 + x0 = x0 + x1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x0 x1. x1 + x0 = x0 + x1

goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own v) - pos ts' (own v), lan = lan v, own = own v\<rparr> \<Longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
have
      "pos ts'' (own v)
          + -1*pos ts' (own v)+(pos ts' (own v) + -1*pos ts (own v))
        = pos ts'' (own v) + - 1 * pos ts (own v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pos ts'' (own v) + - 1 * pos ts' (own v) + (pos ts' (own v) + - 1 * pos ts (own v)) = pos ts'' (own v) + - 1 * pos ts (own v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pos ts'' (own v) + - 1 * pos ts' (own v) + (pos ts' (own v) + - 1 * pos ts (own v)) = pos ts'' (own v) + - 1 * pos ts (own v)

goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own v) - pos ts' (own v), lan = lan v, own = own v\<rparr> \<Longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
pos ts'' (own v) + - 1 * pos ts' (own v) + (pos ts' (own v) + - 1 * pos ts (own v)) = pos ts'' (own v) + - 1 * pos ts (own v)
[PROOF STEP]
have
      "(shift (ext v) ((pos ts'' (own v)) + ( -1 *  pos ts (own v)))) =
       shift (shift  (ext v) (pos ts' (own v) + - 1 * pos ts (own v)))
          (pos ts'' (own v) + - 1 * pos ts' (own v))"
[PROOF STATE]
proof (prove)
using this:
pos ts'' (own v) + - 1 * pos ts' (own v) + (pos ts' (own v) + - 1 * pos ts (own v)) = pos ts'' (own v) + - 1 * pos ts (own v)

goal (1 subgoal):
 1.  shift ext v pos ts'' (own v) + - 1 * pos ts (own v) =  shift  shift ext v pos ts' (own v) + - 1 * pos ts (own v) pos ts'' (own v) + - 1 * pos ts' (own v)
[PROOF STEP]
by (metis f2 real_int.shift_additivity)
[PROOF STATE]
proof (state)
this:
 shift ext v pos ts'' (own v) + - 1 * pos ts (own v) =  shift  shift ext v pos ts' (own v) + - 1 * pos ts (own v) pos ts'' (own v) + - 1 * pos ts' (own v)

goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = \<lparr>ext =  shift ext (move ts ts' v) pos ts'' (own v) - pos ts' (own v), lan = lan v, own = own v\<rparr> \<Longrightarrow> move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
 shift ext v pos ts'' (own v) + - 1 * pos ts (own v) =  shift  shift ext v pos ts' (own v) + - 1 * pos ts (own v) pos ts'' (own v) + - 1 * pos ts' (own v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 shift ext v pos ts'' (own v) + - 1 * pos ts (own v) =  shift  shift ext v pos ts' (own v) + - 1 * pos ts (own v) pos ts'' (own v) + - 1 * pos ts' (own v)

goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
using move_def f2
[PROOF STATE]
proof (prove)
using this:
 shift ext v pos ts'' (own v) + - 1 * pos ts (own v) =  shift  shift ext v pos ts' (own v) + - 1 * pos ts (own v) pos ts'' (own v) + - 1 * pos ts' (own v)
move ?ts ?ts' ?v = \<lparr>ext =  shift ext ?v pos ?ts' (own ?v) - pos ?ts (own ?v), lan = lan ?v, own = own ?v\<rparr>
\<forall>x0 x1. x1 + x0 = x0 + x1

goal (1 subgoal):
 1. move ts' ts'' (move ts ts' v) = move ts ts'' v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
move ts' ts'' (move ts ts' v) = move ts ts'' v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
move ts' ts'' (move ts ts' v) = move ts ts'' v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma move_stability_res:"(ts\<^bold>\<midarrow>r(c)\<^bold>\<rightarrow>ts') \<longrightarrow> move ts ts' v = v"
  and move_stability_clm: "(ts\<^bold>\<midarrow>c(c,n)\<^bold>\<rightarrow>ts') \<longrightarrow> move ts ts' v = v"
  and move_stability_wdr:"(ts\<^bold>\<midarrow>wdr(c,n)\<^bold>\<rightarrow>ts') \<longrightarrow> move ts ts' v = v"
  and move_stability_wdc:"(ts\<^bold>\<midarrow>wdc(c)\<^bold>\<rightarrow>ts') \<longrightarrow> move ts ts' v = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<longrightarrow> move ts ts' v = v &&& ts \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts' \<longrightarrow> move ts ts' v = v) &&& ts \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts' \<longrightarrow> move ts ts' v = v &&& ts \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts' \<longrightarrow> move ts ts' v = v
[PROOF STEP]
using create_reservation_def create_claim_def withdraw_reservation_def
    withdraw_claim_def move_def move_nothing
[PROOF STATE]
proof (prove)
using this:
?ts \<^bold>\<midarrow>r( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := res ?ts ?c \<squnion> clm ?ts ?c) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot) \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts
?ts \<^bold>\<midarrow>c( ?c, ?n ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = res ?ts \<and> dyn ?ts' = dyn ?ts \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts \<and> |clm ?ts ?c| = 0 \<and> |res ?ts ?c| = 1 \<and> (?n + 1 \<^bold>\<in> res ?ts ?c \<or> ?n - 1 \<^bold>\<in> res ?ts ?c) \<and> clm ?ts' = (clm ?ts)(?c := Abs_nat_int {?n})
?ts \<^bold>\<midarrow>wdr( ?c, ?n ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = (res ?ts)(?c := Abs_nat_int {?n}) \<and> dyn ?ts' = dyn ?ts \<and> clm ?ts' = clm ?ts \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts \<and> ?n \<^bold>\<in> res ?ts ?c \<and> |res ?ts ?c| = 2
?ts \<^bold>\<midarrow>wdc( ?c ) \<^bold>\<rightarrow> ?ts' \<equiv> pos ?ts' = pos ?ts \<and> res ?ts' = res ?ts \<and> dyn ?ts' = dyn ?ts \<and> physical_size ?ts' = physical_size ?ts \<and> braking_distance ?ts' = braking_distance ?ts \<and> clm ?ts' = (clm ?ts)(?c := bot)
move ?ts ?ts' ?v = \<lparr>ext =  shift ext ?v pos ?ts' (own ?v) - pos ?ts (own ?v), lan = lan ?v, own = own ?v\<rparr>
move ?ts ?ts ?v = ?v

goal (1 subgoal):
 1. (ts \<^bold>\<midarrow>r( c ) \<^bold>\<rightarrow> ts' \<longrightarrow> move ts ts' v = v &&& ts \<^bold>\<midarrow>c( c, n ) \<^bold>\<rightarrow> ts' \<longrightarrow> move ts ts' v = v) &&& ts \<^bold>\<midarrow>wdr( c, n ) \<^bold>\<rightarrow> ts' \<longrightarrow> move ts ts' v = v &&& ts \<^bold>\<midarrow>wdc( c ) \<^bold>\<rightarrow> ts' \<longrightarrow> move ts ts' v = v
[PROOF STEP]
by (auto)+


[STATEMENT]
lemma Right_Coset_eq_iff:
  assumes "x \<in> G" and "y \<in> G"
  shows "H |\<cdot> x = (H |\<cdot> y) \<longleftrightarrow> H |\<cdot> x \<inter> (H |\<cdot> y) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (H |\<cdot> x = H |\<cdot> y) = (H |\<cdot> x \<inter> (H |\<cdot> y) \<noteq> {})
[PROOF STEP]
using assms Right_Coset_is_orbit
[PROOF STATE]
proof (prove)
using this:
x \<in> G
y \<in> G
?x \<in> G \<Longrightarrow> H |\<cdot> ?x = orbit.Class ?x

goal (1 subgoal):
 1. (H |\<cdot> x = H |\<cdot> y) = (H |\<cdot> x \<inter> (H |\<cdot> y) \<noteq> {})
[PROOF STEP]
by (metis Int_absorb orbit.disjoint orbit.natural.map_closed orbit.non_vacuous)


[STATEMENT]
lemma sumset_translate_eq_right:
  assumes "A \<subseteq> G" and "B \<subseteq> G" and "x \<in> G"
  shows "(sumset A {x} = sumset B {x}) \<longleftrightarrow>  A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sumset A {x} = sumset B {x}) = (A = B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
B \<subseteq> G
x \<in> G

goal (1 subgoal):
 1. (sumset A {x} = sumset B {x}) = (A = B)
[PROOF STEP]
by (smt (verit, best) Diff_Int_distrib2 Diff_eq_empty_iff
 Int_Un_eq(1) Int_absorb2 Un_Diff_cancel2 Un_commute insert_disjoint(2)
subset_refl sumset_is_empty_iff sumsetdiff_sing)


[STATEMENT]
lemma sumset_translate_eq_left:
  assumes "A \<subseteq> G" and "B \<subseteq> G" and "x \<in> G"
  shows " (sumset {x} A = sumset {x} B) \<longleftrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sumset {x} A = sumset {x} B) = (A = B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
B \<subseteq> G
x \<in> G

goal (1 subgoal):
 1. (sumset {x} A = sumset {x} B) = (A = B)
[PROOF STEP]
by (simp add: sumset_commute sumset_translate_eq_right)


[STATEMENT]
lemma differenceset_translate_eq_right:
  assumes "A \<subseteq> G" and "B \<subseteq> G" and "x \<in> G"
  shows "(differenceset A {x} = differenceset B {x}) \<longleftrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (differenceset A {x} = differenceset B {x}) = (A = B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
B \<subseteq> G
x \<in> G

goal (1 subgoal):
 1. (differenceset A {x} = differenceset B {x}) = (A = B)
[PROOF STEP]
by (metis Int_absorb2 differenceset_commute minus_minusset minusset_subset_carrier
    sumset_translate_eq_left)


[STATEMENT]
lemma sumset_inter_union_subset:
 "sumset (A \<inter> B) (A \<union> B) \<subseteq> sumset A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset (A \<inter> B) (A \<union> B) \<subseteq> sumset A B
[PROOF STEP]
by (metis Int_Diff_Un Int_Un_eq(2) Un_subset_iff sumset_commute sumset_subset_Un(2)
    sumset_subset_Un2)


[STATEMENT]
lemma differenceset_group_eq:
  "G = differenceset G G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G = differenceset G G
[PROOF STEP]
using equalityE minusset_eq minusset_triv subset_antisym sumset_D(1) sumset_subset_carrier
    sumset_mono image_mono Int_absorb
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?A = ?B; \<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
minusset ?A = local.inverse ` (?A \<inter> G)
minusset {\<zero>} = {\<zero>}
\<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> ?A = ?B
sumset ?A {\<zero>} = ?A \<inter> G
sumset ?A ?B \<subseteq> G
\<lbrakk>?A' \<subseteq> ?A; ?B' \<subseteq> ?B\<rbrakk> \<Longrightarrow> sumset ?A' ?B' \<subseteq> sumset ?A ?B
?A \<subseteq> ?B \<Longrightarrow> ?f ` ?A \<subseteq> ?f ` ?B
?A \<inter> ?A = ?A

goal (1 subgoal):
 1. G = differenceset G G
[PROOF STEP]
by metis


[STATEMENT]
lemma card_sumset_singleton_subset_eq:
  assumes "a \<in> G" and "A \<subseteq> G"
  shows "card (sumset {a} A) = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (sumset {a} A) = card A
[PROOF STEP]
using assms card_sumset_singleton_eq card.infinite card_sumset_0_iff' le_iff_inf sumset_commute
[PROOF STATE]
proof (prove)
using this:
a \<in> G
A \<subseteq> G
finite ?A \<Longrightarrow> card (sumset ?A {?a}) = (if ?a \<in> G then card (?A \<inter> G) else 0)
infinite ?A \<Longrightarrow> card ?A = 0
(card (sumset ?A ?B) = 0) = (card (?A \<inter> G) = 0 \<or> card (?B \<inter> G) = 0)
(?x \<le> ?y) = (inf ?x ?y = ?x)
sumset ?A ?B = sumset ?B ?A

goal (1 subgoal):
 1. card (sumset {a} A) = card A
[PROOF STEP]
by metis


[STATEMENT]
lemma card_differenceset_singleton_mem_eq:
  assumes "a \<in> G" and "A \<subseteq> G"
  shows "card A = card (differenceset A {a})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card A = card (differenceset A {a})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> G
A \<subseteq> G

goal (1 subgoal):
 1. card A = card (differenceset A {a})
[PROOF STEP]
by (metis card_minusset' card_sumset_singleton_subset_eq differenceset_commute
  minusset_subset_carrier)


[STATEMENT]
lemma card_singleton_differenceset_eq:
  assumes "a \<in> G" and "A \<subseteq> G"
  shows "card A = card (differenceset {a} A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card A = card (differenceset {a} A)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> G
A \<subseteq> G

goal (1 subgoal):
 1. card A = card (differenceset {a} A)
[PROOF STEP]
by (metis card_minusset' card_sumset_singleton_subset_eq minusset_subset_carrier)


[STATEMENT]
lemma sumset_eq_Union_left:
  assumes "A \<subseteq> G"
  shows "sumset A B = (\<Union> a \<in> A. sumset {a} B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset A B = (\<Union>a\<in>A. sumset {a} B)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sumset A B \<subseteq> (\<Union>a\<in>A. sumset {a} B)
 2. (\<Union>a\<in>A. sumset {a} B) \<subseteq> sumset A B
[PROOF STEP]
show "sumset A B \<subseteq> (\<Union> a \<in> A. sumset {a} B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset A B \<subseteq> (\<Union>a\<in>A. sumset {a} B)
[PROOF STEP]
using assms sumset.cases Int_absorb2 Int_iff UN_iff singletonI sumset.sumsetI
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
\<lbrakk>?a \<in> sumset ?A ?B; \<And>a b. \<lbrakk>?a = a \<oplus> b; a \<in> ?A; a \<in> G; b \<in> ?B; b \<in> G\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
?A \<subseteq> ?B \<Longrightarrow> ?A \<inter> ?B = ?A
(?c \<in> ?A \<inter> ?B) = (?c \<in> ?A \<and> ?c \<in> ?B)
(?b \<in> \<Union> (?B ` ?A)) = (\<exists>x\<in>?A. ?b \<in> ?B x)
?a \<in> {?a}
\<lbrakk>?a \<in> ?A; ?a \<in> G; ?b \<in> ?B; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> sumset ?A ?B

goal (1 subgoal):
 1. sumset A B \<subseteq> (\<Union>a\<in>A. sumset {a} B)
[PROOF STEP]
by (smt (verit, del_insts) subsetI)
[PROOF STATE]
proof (state)
this:
sumset A B \<subseteq> (\<Union>a\<in>A. sumset {a} B)

goal (1 subgoal):
 1. (\<Union>a\<in>A. sumset {a} B) \<subseteq> sumset A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Union>a\<in>A. sumset {a} B) \<subseteq> sumset A B
[PROOF STEP]
show "(\<Union> a \<in> A. sumset {a} B) \<subseteq> sumset A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>a\<in>A. sumset {a} B) \<subseteq> sumset A B
[PROOF STEP]
using sumset
[PROOF STATE]
proof (prove)
using this:
sumset ?A ?B = (\<Union>a\<in>?A \<inter> G. \<Union>b\<in>?B \<inter> G. {a \<oplus> b})

goal (1 subgoal):
 1. (\<Union>a\<in>A. sumset {a} B) \<subseteq> sumset A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Union>a\<in>A. sumset {a} B) \<subseteq> sumset A B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumset_eq_Union_right:
  assumes "B \<subseteq> G"
  shows "sumset A B = (\<Union> b \<in> B. sumset A {b})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset A B = (\<Union>b\<in>B. sumset A {b})
[PROOF STEP]
using assms sumset_commute sumset_eq_Union_left
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> G
sumset ?A ?B = sumset ?B ?A
?A \<subseteq> G \<Longrightarrow> sumset ?A ?B = (\<Union>a\<in>?A. sumset {a} ?B)

goal (1 subgoal):
 1. sumset A B = (\<Union>b\<in>B. sumset A {b})
[PROOF STEP]
by (metis (no_types, lifting) Sup.SUP_cong)


[STATEMENT]
lemma sumset_singletons_eq:
  assumes "a \<in> G" and "b \<in> G"
  shows "sumset {a} {b} = {a \<oplus> b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {a} {b} = {a \<oplus> b}
[PROOF STEP]
using assms sumset.simps subset_antisym
[PROOF STATE]
proof (prove)
using this:
a \<in> G
b \<in> G
(?a \<in> sumset ?A ?B) = (\<exists>a b. ?a = a \<oplus> b \<and> a \<in> ?A \<and> a \<in> G \<and> b \<in> ?B \<and> b \<in> G)
\<lbrakk>?A \<subseteq> ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> ?A = ?B

goal (1 subgoal):
 1. sumset {a} {b} = {a \<oplus> b}
[PROOF STEP]
by auto


[STATEMENT]
lemma sumset_eq_subset_differenceset:
  assumes "K \<subseteq> G" and "K \<noteq> {}" and "A \<subseteq> G" and "sumset A K = sumset B K"
  shows "A \<subseteq> differenceset (sumset B K) K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> differenceset (sumset B K) K
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> differenceset (sumset B K) K
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> differenceset (sumset B K) K
[PROOF STEP]
assume ha: "a \<in> A"
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> differenceset (sumset B K) K
[PROOF STEP]
obtain k where hk: "k \<in> K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. k \<in> K \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
K \<noteq> {}

goal (1 subgoal):
 1. (\<And>k. k \<in> K \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
k \<in> K

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> differenceset (sumset B K) K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
k \<in> K
[PROOF STEP]
have "a \<oplus> k \<in> sumset B K"
[PROOF STATE]
proof (prove)
using this:
k \<in> K

goal (1 subgoal):
 1. a \<oplus> k \<in> sumset B K
[PROOF STEP]
using assms sumset.sumsetI ha
[PROOF STATE]
proof (prove)
using this:
k \<in> K
K \<subseteq> G
K \<noteq> {}
A \<subseteq> G
sumset A K = sumset B K
\<lbrakk>?a \<in> ?A; ?a \<in> G; ?b \<in> ?B; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> sumset ?A ?B
a \<in> A

goal (1 subgoal):
 1. a \<oplus> k \<in> sumset B K
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<oplus> k \<in> sumset B K

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> differenceset (sumset B K) K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<oplus> k \<in> sumset B K
[PROOF STEP]
have "a \<oplus> (k \<ominus> k) \<in> differenceset (sumset B K) K"
[PROOF STATE]
proof (prove)
using this:
a \<oplus> k \<in> sumset B K

goal (1 subgoal):
 1. a \<oplus> k \<ominus> k \<in> differenceset (sumset B K) K
[PROOF STEP]
using hk assms ha minusset.minussetI
    subset_iff sumset.sumsetI
[PROOF STATE]
proof (prove)
using this:
a \<oplus> k \<in> sumset B K
k \<in> K
K \<subseteq> G
K \<noteq> {}
A \<subseteq> G
sumset A K = sumset B K
a \<in> A
\<lbrakk>?a \<in> ?A; ?a \<in> G\<rbrakk> \<Longrightarrow> local.inverse ?a \<in> minusset ?A
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)
\<lbrakk>?a \<in> ?A; ?a \<in> G; ?b \<in> ?B; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> sumset ?A ?B

goal (1 subgoal):
 1. a \<oplus> k \<ominus> k \<in> differenceset (sumset B K) K
[PROOF STEP]
by (smt (verit) associative composition_closed inverse_closed)
[PROOF STATE]
proof (state)
this:
a \<oplus> k \<ominus> k \<in> differenceset (sumset B K) K

goal (1 subgoal):
 1. \<And>x. x \<in> A \<Longrightarrow> x \<in> differenceset (sumset B K) K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<oplus> k \<ominus> k \<in> differenceset (sumset B K) K
[PROOF STEP]
show "a \<in> differenceset (sumset B K) K"
[PROOF STATE]
proof (prove)
using this:
a \<oplus> k \<ominus> k \<in> differenceset (sumset B K) K

goal (1 subgoal):
 1. a \<in> differenceset (sumset B K) K
[PROOF STEP]
using hk ha subsetD assms right_unit
[PROOF STATE]
proof (prove)
using this:
a \<oplus> k \<ominus> k \<in> differenceset (sumset B K) K
k \<in> K
a \<in> A
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B
K \<subseteq> G
K \<noteq> {}
A \<subseteq> G
sumset A K = sumset B K
?a \<in> G \<Longrightarrow> ?a \<oplus> \<zero> = ?a

goal (1 subgoal):
 1. a \<in> differenceset (sumset B K) K
[PROOF STEP]
by (metis invertible invertible_right_inverse)
[PROOF STATE]
proof (state)
this:
a \<in> differenceset (sumset B K) K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Left_Coset_eq_sumset:
  assumes "x \<in> G"
  shows "sumset {x} H = x \<cdot>| H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset {x} H = x \<cdot>| H
[PROOF STEP]
using assms Left_Coset_memI sumset.simps
[PROOF STATE]
proof (prove)
using this:
x \<in> G
?h \<in> ?H \<Longrightarrow> ?x \<oplus> ?h \<in> ?x \<cdot>| ?H
(?a \<in> sumset ?A ?B) = (\<exists>a b. ?a = a \<oplus> b \<and> a \<in> ?A \<and> a \<in> G \<and> b \<in> ?B \<and> b \<in> G)

goal (1 subgoal):
 1. sumset {x} H = x \<cdot>| H
[PROOF STEP]
by fastforce


[STATEMENT]
lemma sumset_subgroup_eq_iff:
  assumes "a \<in> G" and "b \<in> G"
  shows "sumset {a} H = sumset {b} H \<longleftrightarrow>
    (sumset {a} H) \<inter> (sumset {b} H) \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sumset {a} H = sumset {b} H) = (sumset {a} H \<inter> sumset {b} H \<noteq> {})
[PROOF STEP]
using Right_Coset_eq_iff assms Left_Coset_eq_sumset Left_equals_Right_coset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> G; ?y \<in> G\<rbrakk> \<Longrightarrow> (Right_Coset H ?x = Right_Coset H ?y) = (Right_Coset H ?x \<inter> Right_Coset H ?y \<noteq> {})
a \<in> G
b \<in> G
?x \<in> G \<Longrightarrow> sumset {?x} H = ?x \<cdot>| H
?g \<in> G \<Longrightarrow> ?g \<cdot>| H = Right_Coset H ?g

goal (1 subgoal):
 1. (sumset {a} H = sumset {b} H) = (sumset {a} H \<inter> sumset {b} H \<noteq> {})
[PROOF STEP]
by presburger


[STATEMENT]
lemma card_divide_sumset:
  assumes "A \<subseteq> G"
  shows "card H dvd card (sumset A H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card H dvd card (sumset A H)
[PROOF STEP]
proof(cases "finite H \<and> finite A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite H \<and> finite A \<Longrightarrow> card H dvd card (sumset A H)
 2. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
case hfin: True
[PROOF STATE]
proof (state)
this:
finite H \<and> finite A

goal (2 subgoals):
 1. finite H \<and> finite A \<Longrightarrow> card H dvd card (sumset A H)
 2. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite H \<and> finite A
[PROOF STEP]
have hfinsum: "\<And> X. X \<in> ((\<lambda> a. sumset {a} H) ` A) \<Longrightarrow> finite X"
[PROOF STATE]
proof (prove)
using this:
finite H \<and> finite A

goal (1 subgoal):
 1. \<And>X. X \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> finite X
[PROOF STEP]
using finite_sumset
[PROOF STATE]
proof (prove)
using this:
finite H \<and> finite A
\<lbrakk>finite ?A; finite ?B\<rbrakk> \<Longrightarrow> finite (sumset ?A ?B)

goal (1 subgoal):
 1. \<And>X. X \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> finite X
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?X \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> finite ?X

goal (2 subgoals):
 1. finite H \<and> finite A \<Longrightarrow> card H dvd card (sumset A H)
 2. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?X \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> finite ?X

goal (2 subgoals):
 1. finite H \<and> finite A \<Longrightarrow> card H dvd card (sumset A H)
 2. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
have "pairwise disjnt ((\<lambda> a. sumset {a} H) ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairwise disjnt ((\<lambda>a. sumset {a} H) ` A)
[PROOF STEP]
using pairwise_imageI disjnt_def sumset_subgroup_eq_iff subset_eq assms
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. \<lbrakk>x \<in> ?A; y \<in> ?A; x \<noteq> y; ?f x \<noteq> ?f y\<rbrakk> \<Longrightarrow> ?P (?f x) (?f y)) \<Longrightarrow> pairwise ?P (?f ` ?A)
disjnt ?A ?B = (?A \<inter> ?B = {})
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> (sumset {?a} H = sumset {?b} H) = (sumset {?a} H \<inter> sumset {?b} H \<noteq> {})
(?A \<subseteq> ?B) = (\<forall>x\<in>?A. x \<in> ?B)
A \<subseteq> G

goal (1 subgoal):
 1. pairwise disjnt ((\<lambda>a. sumset {a} H) ` A)
[PROOF STEP]
by (smt (verit, best))
[PROOF STATE]
proof (state)
this:
pairwise disjnt ((\<lambda>a. sumset {a} H) ` A)

goal (2 subgoals):
 1. finite H \<and> finite A \<Longrightarrow> card H dvd card (sumset A H)
 2. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pairwise disjnt ((\<lambda>a. sumset {a} H) ` A)

goal (2 subgoals):
 1. finite H \<and> finite A \<Longrightarrow> card H dvd card (sumset A H)
 2. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
have "card H dvd sum card ((\<lambda> a. sumset {a} H) ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card H dvd sum card ((\<lambda>a. sumset {a} H) ` A)
[PROOF STEP]
proof(intro dvd_sum)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> card H dvd card a
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. a \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> card H dvd card a
[PROOF STEP]
assume "X \<in> (\<lambda> a. sumset {a} H) ` A"
[PROOF STATE]
proof (state)
this:
X \<in> (\<lambda>a. sumset {a} H) ` A

goal (1 subgoal):
 1. \<And>a. a \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> card H dvd card a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<in> (\<lambda>a. sumset {a} H) ` A
[PROOF STEP]
show "card H dvd card X"
[PROOF STATE]
proof (prove)
using this:
X \<in> (\<lambda>a. sumset {a} H) ` A

goal (1 subgoal):
 1. card H dvd card X
[PROOF STEP]
using dvd_refl
[PROOF STATE]
proof (prove)
using this:
X \<in> (\<lambda>a. sumset {a} H) ` A
?a dvd ?a

goal (1 subgoal):
 1. card H dvd card X
[PROOF STEP]
using Left_equals_Right_coset Right_Coset_cardinality assms Left_Coset_eq_sumset
[PROOF STATE]
proof (prove)
using this:
X \<in> (\<lambda>a. sumset {a} H) ` A
?a dvd ?a
?g \<in> G \<Longrightarrow> ?g \<cdot>| H = Right_Coset H ?g
?x \<in> G \<Longrightarrow> card (Right_Coset H ?x) = card H
A \<subseteq> G
?x \<in> G \<Longrightarrow> sumset {?x} H = ?x \<cdot>| H

goal (1 subgoal):
 1. card H dvd card X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card H dvd card X

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card H dvd sum card ((\<lambda>a. sumset {a} H) ` A)

goal (2 subgoals):
 1. finite H \<and> finite A \<Longrightarrow> card H dvd card (sumset A H)
 2. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?X \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> finite ?X
pairwise disjnt ((\<lambda>a. sumset {a} H) ` A)
card H dvd sum card ((\<lambda>a. sumset {a} H) ` A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?X \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> finite ?X
pairwise disjnt ((\<lambda>a. sumset {a} H) ` A)
card H dvd sum card ((\<lambda>a. sumset {a} H) ` A)

goal (1 subgoal):
 1. card H dvd card (sumset A H)
[PROOF STEP]
using assms sumset_eq_Union_left card_Union_disjoint
[PROOF STATE]
proof (prove)
using this:
?X \<in> (\<lambda>a. sumset {a} H) ` A \<Longrightarrow> finite ?X
pairwise disjnt ((\<lambda>a. sumset {a} H) ` A)
card H dvd sum card ((\<lambda>a. sumset {a} H) ` A)
A \<subseteq> G
?A \<subseteq> G \<Longrightarrow> sumset ?A ?B = (\<Union>a\<in>?A. sumset {a} ?B)
\<lbrakk>pairwise disjnt ?C; \<And>A. A \<in> ?C \<Longrightarrow> finite A\<rbrakk> \<Longrightarrow> card (\<Union> ?C) = sum card ?C

goal (1 subgoal):
 1. card H dvd card (sumset A H)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
card H dvd card (sumset A H)

goal (1 subgoal):
 1. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (finite H \<and> finite A)

goal (1 subgoal):
 1. \<not> (finite H \<and> finite A) \<Longrightarrow> card H dvd card (sumset A H)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (finite H \<and> finite A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (finite H \<and> finite A)

goal (1 subgoal):
 1. card H dvd card (sumset A H)
[PROOF STEP]
using assms card_sumset_0_iff
[PROOF STATE]
proof (prove)
using this:
\<not> (finite H \<and> finite A)
A \<subseteq> G
\<lbrakk>?A \<subseteq> G; ?B \<subseteq> G\<rbrakk> \<Longrightarrow> (card (sumset ?A ?B) = 0) = (card ?A = 0 \<or> card ?B = 0)

goal (1 subgoal):
 1. card H dvd card (sumset A H)
[PROOF STEP]
by (metis card_eq_0_iff dvd_0_right sub subsetI)
[PROOF STATE]
proof (state)
this:
card H dvd card (sumset A H)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumset_subgroup_eq_Class_Union:
  assumes "A \<subseteq> G"
  shows "sumset A H = (\<Union> (Class ` A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset A H = \<Union> (Class ` A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sumset A H \<subseteq> \<Union> (Class ` A)
 2. \<Union> (Class ` A) \<subseteq> sumset A H
[PROOF STEP]
show "sumset A H \<subseteq> \<Union> (Class ` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sumset A H \<subseteq> \<Union> (Class ` A)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sumset A H \<Longrightarrow> x \<in> \<Union> (Class ` A)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> sumset A H \<Longrightarrow> x \<in> \<Union> (Class ` A)
[PROOF STEP]
assume "x \<in> sumset A H"
[PROOF STATE]
proof (state)
this:
x \<in> sumset A H

goal (1 subgoal):
 1. \<And>x. x \<in> sumset A H \<Longrightarrow> x \<in> \<Union> (Class ` A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> sumset A H
[PROOF STEP]
obtain a b where ha: "a \<in> A" and "b \<in> H" and "x = a \<oplus> b"
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset A H

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<in> A; b \<in> H; x = a \<oplus> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sumset.cases
[PROOF STATE]
proof (prove)
using this:
x \<in> sumset A H
\<lbrakk>?a \<in> sumset ?A ?B; \<And>a b. \<lbrakk>?a = a \<oplus> b; a \<in> ?A; a \<in> G; b \<in> ?B; b \<in> G\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<in> A; b \<in> H; x = a \<oplus> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> A
b \<in> H
x = a \<oplus> b

goal (1 subgoal):
 1. \<And>x. x \<in> sumset A H \<Longrightarrow> x \<in> \<Union> (Class ` A)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
b \<in> H
x = a \<oplus> b
[PROOF STEP]
have "x \<in> Class a"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
b \<in> H
x = a \<oplus> b

goal (1 subgoal):
 1. x \<in> Class a
[PROOF STEP]
using Left_Coset_Class_unit Left_Coset_eq_sumset assms
[PROOF STATE]
proof (prove)
using this:
a \<in> A
b \<in> H
x = a \<oplus> b
?g \<in> G \<Longrightarrow> ?g \<cdot>| H = Class ?g
?x \<in> G \<Longrightarrow> sumset {?x} H = ?x \<cdot>| H
A \<subseteq> G

goal (1 subgoal):
 1. x \<in> Class a
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> Class a

goal (1 subgoal):
 1. \<And>x. x \<in> sumset A H \<Longrightarrow> x \<in> \<Union> (Class ` A)
[PROOF STEP]
thus "x \<in> \<Union> (Class ` A)"
[PROOF STATE]
proof (prove)
using this:
x \<in> Class a

goal (1 subgoal):
 1. x \<in> \<Union> (Class ` A)
[PROOF STEP]
using ha
[PROOF STATE]
proof (prove)
using this:
x \<in> Class a
a \<in> A

goal (1 subgoal):
 1. x \<in> \<Union> (Class ` A)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x \<in> \<Union> (Class ` A)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sumset A H \<subseteq> \<Union> (Class ` A)

goal (1 subgoal):
 1. \<Union> (Class ` A) \<subseteq> sumset A H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (Class ` A) \<subseteq> sumset A H
[PROOF STEP]
show "\<Union> (Class ` A) \<subseteq> sumset A H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (Class ` A) \<subseteq> sumset A H
[PROOF STEP]
proof(intro Union_least)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. X \<in> Class ` A \<Longrightarrow> X \<subseteq> sumset A H
[PROOF STEP]
fix X
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>X. X \<in> Class ` A \<Longrightarrow> X \<subseteq> sumset A H
[PROOF STEP]
assume "X \<in> Class ` A"
[PROOF STATE]
proof (state)
this:
X \<in> Class ` A

goal (1 subgoal):
 1. \<And>X. X \<in> Class ` A \<Longrightarrow> X \<subseteq> sumset A H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X \<in> Class ` A
[PROOF STEP]
obtain a where "a \<in> A" and "X = Class a"
[PROOF STATE]
proof (prove)
using this:
X \<in> Class ` A

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> A; X = Class a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> A
X = Class a

goal (1 subgoal):
 1. \<And>X. X \<in> Class ` A \<Longrightarrow> X \<subseteq> sumset A H
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a \<in> A
X = Class a

goal (1 subgoal):
 1. \<And>X. X \<in> Class ` A \<Longrightarrow> X \<subseteq> sumset A H
[PROOF STEP]
hence "{a} \<subseteq> A"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
X = Class a

goal (1 subgoal):
 1. {a} \<subseteq> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a} \<subseteq> A

goal (1 subgoal):
 1. \<And>X. X \<in> Class ` A \<Longrightarrow> X \<subseteq> sumset A H
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a \<in> A
X = Class a
{a} \<subseteq> A
[PROOF STEP]
show "X \<subseteq> sumset A H"
[PROOF STATE]
proof (prove)
using this:
a \<in> A
X = Class a
{a} \<subseteq> A

goal (1 subgoal):
 1. X \<subseteq> sumset A H
[PROOF STEP]
using Left_Coset_Class_unit
      Left_Coset_eq_sumset assms sumset_mono subset_refl in_mono
[PROOF STATE]
proof (prove)
using this:
a \<in> A
X = Class a
{a} \<subseteq> A
?g \<in> G \<Longrightarrow> ?g \<cdot>| H = Class ?g
?x \<in> G \<Longrightarrow> sumset {?x} H = ?x \<cdot>| H
A \<subseteq> G
\<lbrakk>?A' \<subseteq> ?A; ?B' \<subseteq> ?B\<rbrakk> \<Longrightarrow> sumset ?A' ?B' \<subseteq> sumset ?A ?B
?A \<subseteq> ?A
?A \<subseteq> ?B \<Longrightarrow> ?x \<in> ?A \<longrightarrow> ?x \<in> ?B

goal (1 subgoal):
 1. X \<subseteq> sumset A H
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
X \<subseteq> sumset A H

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> (Class ` A) \<subseteq> sumset A H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Class_image_sumset_subgroup_eq:
  assumes "A \<subseteq> G"
  shows "Class ` (sumset A H) = Class ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Class ` sumset A H = Class ` A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Class ` sumset A H \<subseteq> Class ` A
 2. Class ` A \<subseteq> Class ` sumset A H
[PROOF STEP]
show "Class ` sumset A H \<subseteq> Class ` A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Class ` sumset A H \<subseteq> Class ` A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Class ` sumset A H \<Longrightarrow> x \<in> Class ` A
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Class ` sumset A H \<Longrightarrow> x \<in> Class ` A
[PROOF STEP]
assume "x \<in> Class ` sumset A H"
[PROOF STATE]
proof (state)
this:
x \<in> Class ` sumset A H

goal (1 subgoal):
 1. \<And>x. x \<in> Class ` sumset A H \<Longrightarrow> x \<in> Class ` A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Class ` sumset A H
[PROOF STEP]
obtain c where hc: "c \<in> sumset A H" and "x = Class c"
[PROOF STATE]
proof (prove)
using this:
x \<in> Class ` sumset A H

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> sumset A H; x = Class c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c \<in> sumset A H
x = Class c

goal (1 subgoal):
 1. \<And>x. x \<in> Class ` sumset A H \<Longrightarrow> x \<in> Class ` A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c \<in> sumset A H
x = Class c

goal (1 subgoal):
 1. \<And>x. x \<in> Class ` sumset A H \<Longrightarrow> x \<in> Class ` A
[PROOF STEP]
obtain a b where ha: "a \<in> A" and "b \<in> H" and "c = a \<oplus> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<in> A; b \<in> H; c = a \<oplus> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using hc sumset.cases
[PROOF STATE]
proof (prove)
using this:
c \<in> sumset A H
\<lbrakk>?a \<in> sumset ?A ?B; \<And>a b. \<lbrakk>?a = a \<oplus> b; a \<in> ?A; a \<in> G; b \<in> ?B; b \<in> G\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>a b. \<lbrakk>a \<in> A; b \<in> H; c = a \<oplus> b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> A
b \<in> H
c = a \<oplus> b

goal (1 subgoal):
 1. \<And>x. x \<in> Class ` sumset A H \<Longrightarrow> x \<in> Class ` A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c \<in> sumset A H
x = Class c
a \<in> A
b \<in> H
c = a \<oplus> b
[PROOF STEP]
show "x \<in> Class ` A"
[PROOF STATE]
proof (prove)
using this:
c \<in> sumset A H
x = Class c
a \<in> A
b \<in> H
c = a \<oplus> b

goal (1 subgoal):
 1. x \<in> Class ` A
[PROOF STEP]
using ha Class_eq CongruenceI assms composition_closed
      sumset.cases Partition_def commutative image_eqI left_unit sub unit_closed
[PROOF STATE]
proof (prove)
using this:
c \<in> sumset A H
x = Class c
a \<in> A
b \<in> H
c = a \<oplus> b
a \<in> A
(?a, ?b) \<in> Congruence \<Longrightarrow> Class ?a = Class ?b
\<lbrakk>?a = ?b \<oplus> ?k; ?a \<in> G; ?b \<in> G; ?k \<in> H\<rbrakk> \<Longrightarrow> (?a, ?b) \<in> Congruence
A \<subseteq> G
\<lbrakk>?a \<in> G; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> G
\<lbrakk>?a \<in> sumset ?A ?B; \<And>a b. \<lbrakk>?a = a \<oplus> b; a \<in> ?A; a \<in> G; b \<in> ?B; b \<in> G\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
Partition = Class ` G
\<lbrakk>?x \<in> G; ?y \<in> G\<rbrakk> \<Longrightarrow> ?x \<oplus> ?y = ?y \<oplus> ?x
\<lbrakk>?b = ?f ?x; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?b \<in> ?f ` ?A
?a \<in> G \<Longrightarrow> \<zero> \<oplus> ?a = ?a
?a \<in> H \<Longrightarrow> ?a \<in> G
\<zero> \<in> G

goal (1 subgoal):
 1. x \<in> Class ` A
[PROOF STEP]
by (smt (verit, ccfv_threshold) Block_self Class_cong Normal_def)
[PROOF STATE]
proof (state)
this:
x \<in> Class ` A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Class ` sumset A H \<subseteq> Class ` A

goal (1 subgoal):
 1. Class ` A \<subseteq> Class ` sumset A H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Class ` A \<subseteq> Class ` sumset A H
[PROOF STEP]
show "Class ` A \<subseteq> Class ` sumset A H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Class ` A \<subseteq> Class ` sumset A H
[PROOF STEP]
using assms right_unit subsetD subsetI sumset.sumsetI
    unit_closed
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
?a \<in> G \<Longrightarrow> ?a \<oplus> \<zero> = ?a
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B
\<lbrakk>?a \<in> ?A; ?a \<in> G; ?b \<in> ?B; ?b \<in> G\<rbrakk> \<Longrightarrow> ?a \<oplus> ?b \<in> sumset ?A ?B
\<zero> \<in> G

goal (1 subgoal):
 1. Class ` A \<subseteq> Class ` sumset A H
[PROOF STEP]
by (smt (verit, del_insts) image_subset_iff sub_unit_closed)
[PROOF STATE]
proof (state)
this:
Class ` A \<subseteq> Class ` sumset A H

goal:
No subgoals!
[PROOF STEP]
qed