[STATEMENT]
lemma qf_not_q0: "qf \<notin> {q0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qf \<notin> {q0}
[PROOF STEP]
using qf_not_in_SQ q0_sub_SQ
[PROOF STATE]
proof (prove)
using this:
qf \<notin> SQ
{q0} \<subseteq> SQ

goal (1 subgoal):
 1. qf \<notin> {q0}
[PROOF STEP]
by auto


[STATEMENT]
lemma step_eps_closure_set_q0: "step_eps_closure_set {q0} bs = {q0} \<union>
  (nfa'.step_eps_closure_set {q0'} bs \<union> right.nfa'.step_eps_closure_set {q0''} bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set {q0} bs = {q0} \<union> (nfa'.step_eps_closure_set {q0'} bs \<union> right.nfa'.step_eps_closure_set {q0''} bs)
[PROOF STEP]
using step_eps_closure_set_unfold[OF step_eps_q0]
    insert_is_Un[of q0' "{q0''}"]
    step_eps_closure_set_split[of _ _ "{q0'}" "{q0''}"]
    step_eps_closure_set_cong[OF nfa'.q0_sub_Q]
    right.step_eps_closure_set_cong[OF right.nfa'.q0_sub_Q]
[PROOF STATE]
proof (prove)
using this:
step_eps_closure_set {q0} ?bs = {q0} \<union> step_eps_closure_set {q0', q0''} ?bs
{q0', q0''} = {q0'} \<union> {q0''}
NFA.step_eps_closure_set ?q0.0 ?transs ({q0'} \<union> {q0''}) ?bs = NFA.step_eps_closure_set ?q0.0 ?transs {q0'} ?bs \<union> NFA.step_eps_closure_set ?q0.0 ?transs {q0''} ?bs
step_eps_closure_set {q0'} ?bs = nfa'.step_eps_closure_set {q0'} ?bs
step_eps_closure_set {q0''} ?bs = right.nfa'.step_eps_closure_set {q0''} ?bs

goal (1 subgoal):
 1. step_eps_closure_set {q0} bs = {q0} \<union> (nfa'.step_eps_closure_set {q0'} bs \<union> right.nfa'.step_eps_closure_set {q0''} bs)
[PROOF STEP]
by auto


[STATEMENT]
lemma run_accept_eps_cong: "run_accept_eps {q0} bss bs \<longleftrightarrow>
  (nfa'.run_accept_eps {q0'} bss bs \<or> right.nfa'.run_accept_eps {q0''} bss bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps {q0} bss bs = (nfa'.run_accept_eps {q0'} bss bs \<or> right.nfa'.run_accept_eps {q0''} bss bs)
[PROOF STEP]
using run_accept_eps_Nil_cong run_accept_eps_Cons_cong
[PROOF STATE]
proof (prove)
using this:
run_accept_eps {q0} [] ?bs = (nfa'.run_accept_eps {q0'} [] ?bs \<or> right.nfa'.run_accept_eps {q0''} [] ?bs)
run_accept_eps {q0} (?cs # ?css) ?bs = (nfa'.run_accept_eps {q0'} (?cs # ?css) ?bs \<or> right.nfa'.run_accept_eps {q0''} (?cs # ?css) ?bs)

goal (1 subgoal):
 1. run_accept_eps {q0} bss bs = (nfa'.run_accept_eps {q0'} bss bs \<or> right.nfa'.run_accept_eps {q0''} bss bs)
[PROOF STEP]
by (cases bss) auto


[STATEMENT]
lemma step_symb_set_q0: "step_symb_set {q0} = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set {q0} = {}
[PROOF STEP]
unfolding NFA.step_symb_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q'. \<exists>q\<in>{q0}. step_symb q q'} = {}
[PROOF STEP]
using step_symb_q0
[PROOF STATE]
proof (prove)
using this:
\<not> step_symb q0 ?q

goal (1 subgoal):
 1. {q'. \<exists>q\<in>{q0}. step_symb q q'} = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma run_accept_eps_Nil: "run_accept_eps {q0} [] bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. run_accept_eps {q0} [] bs
[PROOF STEP]
unfolding NFA.run_accept_eps_def NFA.run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept_eps (foldl delta {q0} []) bs
[PROOF STEP]
using step_eps_accept_eps step_eps_q0
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>NFA.step_eps ?q0.0 ?transs ?bs ?q ?qf; ?q \<in> ?R\<rbrakk> \<Longrightarrow> NFA.accept_eps ?q0.0 ?qf ?transs ?R ?bs
step_eps ?bs q0 ?q = (?q \<in> {q0', qf})

goal (1 subgoal):
 1. accept_eps (foldl delta {q0} []) bs
[PROOF STEP]
by fastforce


[STATEMENT]
lemma rtranclp_step_eps_q0_q0': "(step_eps bs)\<^sup>*\<^sup>* q q' \<Longrightarrow> q = q0 \<Longrightarrow>
  q' \<in> {q0, qf} \<or> (q' \<in> nfa'.SQ \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q0' q')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* q q'; q = q0\<rbrakk> \<Longrightarrow> q' \<in> {q0, qf} \<or> q' \<in> nfa'.SQ \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q0' q'
[PROOF STEP]
apply (induction q q' rule: rtranclp.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. a = q0 \<Longrightarrow> a \<in> {q0, qf} \<or> a \<in> nfa'.SQ \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q0' a
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a = q0 \<Longrightarrow> b \<in> {q0, qf} \<or> b \<in> nfa'.SQ \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q0' b; step_eps bs b c; a = q0\<rbrakk> \<Longrightarrow> c \<in> {q0, qf} \<or> c \<in> nfa'.SQ \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q0' c
[PROOF STEP]
using step_eps_q0 step_eps_dest qf_not_in_SQ step_eps_cong_SQ nfa'.q0_sub_SQ
    nfa'.step_eps_closed[unfolded NFA.Q_def]
[PROOF STATE]
proof (prove)
using this:
step_eps ?bs q0 ?q = (?q \<in> {q0', qf})
NFA.step_eps ?q0.0 ?transs ?bs ?q ?q' \<Longrightarrow> ?q \<in> NFA.SQ ?q0.0 ?transs
qf \<notin> SQ
?q \<in> nfa'.SQ \<Longrightarrow> step_eps ?bs ?q ?q' = nfa'.step_eps ?bs ?q ?q'
{q0'} \<subseteq> nfa'.SQ
nfa'.step_eps ?bs ?q ?q' \<Longrightarrow> ?q' \<in> nfa'.SQ \<union> {q0}

goal (2 subgoals):
 1. \<And>a. a = q0 \<Longrightarrow> a \<in> {q0, qf} \<or> a \<in> nfa'.SQ \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q0' a
 2. \<And>a b c. \<lbrakk>(step_eps bs)\<^sup>*\<^sup>* a b; a = q0 \<Longrightarrow> b \<in> {q0, qf} \<or> b \<in> nfa'.SQ \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q0' b; step_eps bs b c; a = q0\<rbrakk> \<Longrightarrow> c \<in> {q0, qf} \<or> c \<in> nfa'.SQ \<and> (nfa'.step_eps bs)\<^sup>*\<^sup>* q0' c
[PROOF STEP]
by fastforce+


[STATEMENT]
lemma step_eps_closure_set_q0: "step_eps_closure_set {q0} bs \<subseteq> {q0, qf} \<union>
  (nfa'.step_eps_closure_set {q0'} bs \<inter> nfa'.SQ)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set {q0} bs \<subseteq> {q0, qf} \<union> nfa'.step_eps_closure_set {q0'} bs \<inter> nfa'.SQ
[PROOF STEP]
unfolding NFA.step_eps_closure_set_def NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>q\<in>{q0}. Collect ((step_eps bs)\<^sup>*\<^sup>* q)) \<subseteq> {q0, qf} \<union> (\<Union>q\<in>{q0'}. Collect ((nfa'.step_eps bs)\<^sup>*\<^sup>* q)) \<inter> nfa'.SQ
[PROOF STEP]
using rtranclp_step_eps_q0_q0'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(step_eps ?bs)\<^sup>*\<^sup>* ?q ?q'; ?q = q0\<rbrakk> \<Longrightarrow> ?q' \<in> {q0, qf} \<or> ?q' \<in> nfa'.SQ \<and> (nfa'.step_eps ?bs)\<^sup>*\<^sup>* q0' ?q'

goal (1 subgoal):
 1. (\<Union>q\<in>{q0}. Collect ((step_eps bs)\<^sup>*\<^sup>* q)) \<subseteq> {q0, qf} \<union> (\<Union>q\<in>{q0'}. Collect ((nfa'.step_eps bs)\<^sup>*\<^sup>* q)) \<inter> nfa'.SQ
[PROOF STEP]
by auto


[STATEMENT]
lemma delta_sub_nfa'_delta: "delta {q0} bs \<subseteq> nfa'.delta {q0'} bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta {q0} bs \<subseteq> nfa'.delta {q0'} bs
[PROOF STEP]
unfolding NFA.delta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set (step_eps_closure_set {q0} bs) \<subseteq> nfa'.step_symb_set (nfa'.step_eps_closure_set {q0'} bs)
[PROOF STEP]
using step_symb_set_mono[OF step_eps_closure_set_q0, unfolded step_symb_set_q0
    step_symb_set_qf step_symb_set_split insert_is_Un[of q0 "{qf}"]]
    step_symb_set_cong_SQ
[PROOF STATE]
proof (prove)
using this:
NFA.step_symb_set ?q0.0 ?transs (step_eps_closure_set {q0} ?bs1) \<subseteq> NFA.step_symb_set ?q0.0 ?transs {q0} \<union> NFA.step_symb_set ?q0.0 ?transs {qf} \<union> NFA.step_symb_set ?q0.0 ?transs (nfa'.step_eps_closure_set {q0'} ?bs1 \<inter> nfa'.SQ)
?R \<subseteq> nfa'.SQ \<Longrightarrow> step_symb_set ?R = nfa'.step_symb_set ?R

goal (1 subgoal):
 1. step_symb_set (step_eps_closure_set {q0} bs) \<subseteq> nfa'.step_symb_set (nfa'.step_eps_closure_set {q0'} bs)
[PROOF STEP]
by (metis boolean_algebra_cancel.sup0 inf_le2 step_symb_set_proj step_symb_set_q0
      step_symb_set_qf sup_commute)


[STATEMENT]
lemma step_eps_closure_set_q0_split: "step_eps_closure_set {q0} bs = {q0, qf} \<union>
  step_eps_closure_set {q0'} bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_eps_closure_set {q0} bs = {q0, qf} \<union> step_eps_closure_set {q0'} bs
[PROOF STEP]
unfolding NFA.step_eps_closure_set_def NFA.step_eps_closure_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>q\<in>{q0}. Collect ((step_eps bs)\<^sup>*\<^sup>* q)) = {q0, qf} \<union> (\<Union>q\<in>{q0'}. Collect ((step_eps bs)\<^sup>*\<^sup>* q))
[PROOF STEP]
using step_eps_qf step_eps_q0
[PROOF STATE]
proof (prove)
using this:
step_eps ?bs qf ?q = False
step_eps ?bs q0 ?q = (?q \<in> {q0', qf})

goal (1 subgoal):
 1. (\<Union>q\<in>{q0}. Collect ((step_eps bs)\<^sup>*\<^sup>* q)) = {q0, qf} \<union> (\<Union>q\<in>{q0'}. Collect ((step_eps bs)\<^sup>*\<^sup>* q))
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>bs q. \<not> step_eps bs qf q; \<And>bs q. step_eps bs q0 q = (q = q0' \<or> q = qf); x \<noteq> q0; (step_eps bs)\<^sup>*\<^sup>* q0 x; x \<noteq> qf\<rbrakk> \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* q0' x
 2. \<And>x. \<lbrakk>\<And>bs q. \<not> step_eps bs qf q; \<And>bs q. step_eps bs q0 q = (q = q0' \<or> q = qf); (step_eps bs)\<^sup>*\<^sup>* q0' x\<rbrakk> \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* q0 x
[PROOF STEP]
apply (metis rtranclp_unfold)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>bs q. \<not> step_eps bs qf q; \<And>bs q. step_eps bs q0 q = (q = q0' \<or> q = qf); (step_eps bs)\<^sup>*\<^sup>* q0' x\<rbrakk> \<Longrightarrow> (step_eps bs)\<^sup>*\<^sup>* q0 x
[PROOF STEP]
by (metis r_into_rtranclp rtranclp.rtrancl_into_rtrancl rtranclp_idemp)


[STATEMENT]
lemma delta_q0_q0': "delta {q0} bs = delta {q0'} bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta {q0} bs = delta {q0'} bs
[PROOF STEP]
unfolding NFA.delta_def step_eps_closure_set_q0_split step_symb_set_split
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set {q0, qf} \<union> step_symb_set (step_eps_closure_set {q0'} bs) = step_symb_set (step_eps_closure_set {q0'} bs)
[PROOF STEP]
unfolding NFA.delta_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step_symb_set {q0, qf} \<union> delta {q0'} bs = delta {q0'} bs
[PROOF STEP]
unfolding NFA.step_symb_set_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q'. \<exists>q\<in>{q0, qf}. step_symb q q'} \<union> delta {q0'} bs = delta {q0'} bs
[PROOF STEP]
using step_symb_q0 step_symb_dest qf_not_in_SQ
[PROOF STATE]
proof (prove)
using this:
\<not> step_symb q0 ?q
NFA.step_symb ?q0.0 ?transs ?q ?q' \<Longrightarrow> ?q \<in> NFA.SQ ?q0.0 ?transs
qf \<notin> SQ

goal (1 subgoal):
 1. {q'. \<exists>q\<in>{q0, qf}. step_symb q q'} \<union> delta {q0'} bs = delta {q0'} bs
[PROOF STEP]
by fastforce


[STATEMENT]
lemma action_loc_aux_compP [simp]: "action_loc_aux (compP f P) = action_loc_aux P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action_loc_aux (compP f P) = action_loc_aux P
[PROOF STEP]
by(auto 4 4 elim!: action_loc_aux_cases)


[STATEMENT]
lemma action_loc_compP: "action_loc (compP f P) = action_loc P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. action_loc (compP f P) = action_loc P
[PROOF STEP]
by simp


[STATEMENT]
lemma is_volatile_compP [simp]: "is_volatile (compP f P) = is_volatile P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_volatile (compP f P) = is_volatile P
[PROOF STEP]
proof(rule ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. is_volatile (compP f P) x = is_volatile P x
[PROOF STEP]
fix hT
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. is_volatile (compP f P) x = is_volatile P x
[PROOF STEP]
show "is_volatile (compP f P) hT = is_volatile P hT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_volatile (compP f P) hT = is_volatile P hT
[PROOF STEP]
by(cases hT) simp_all
[PROOF STATE]
proof (state)
this:
is_volatile (compP f P) hT = is_volatile P hT

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma saction_compP [simp]: "saction (compP f P) = saction P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. saction (compP f P) = saction P
[PROOF STEP]
by(simp add: saction.simps fun_eq_iff)


[STATEMENT]
lemma sactions_compP [simp]: "sactions (compP f P) = sactions P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sactions (compP f P) = sactions P
[PROOF STEP]
by(rule ext)(simp only: sactions_def, simp)


[STATEMENT]
lemma addr_locs_compP [simp]: "addr_locs (compP f P) = addr_locs P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_locs (compP f P) = addr_locs P
[PROOF STEP]
by(rule ext)(case_tac x, simp_all)


[STATEMENT]
lemma syncronizes_with_compP [simp]: "synchronizes_with (compP f P) = synchronizes_with P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. synchronizes_with (compP f P) = synchronizes_with P
[PROOF STEP]
by(simp add: synchronizes_with.simps fun_eq_iff)


[STATEMENT]
lemma sync_order_compP [simp]: "sync_order (compP f P) = sync_order P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync_order (compP f P) = sync_order P
[PROOF STEP]
by(simp add: sync_order_def fun_eq_iff)


[STATEMENT]
lemma sync_with_compP [simp]: "sync_with (compP f P) = sync_with P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync_with (compP f P) = sync_with P
[PROOF STEP]
by(simp add: sync_with_def fun_eq_iff)


[STATEMENT]
lemma po_sw_compP [simp]: "po_sw (compP f P) = po_sw P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. po_sw (compP f P) = po_sw P
[PROOF STEP]
by(simp add: po_sw_def fun_eq_iff)


[STATEMENT]
lemma happens_before_compP: "happens_before (compP f P) = happens_before P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. happens_before (compP f P) = happens_before P
[PROOF STEP]
by simp


[STATEMENT]
lemma addr_loc_default_compP [simp]: "addr_loc_default (compP f P) = addr_loc_default P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_loc_default (compP f P) = addr_loc_default P
[PROOF STEP]
proof(intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. addr_loc_default (compP f P) x xa = addr_loc_default P x xa
[PROOF STEP]
fix hT al
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. addr_loc_default (compP f P) x xa = addr_loc_default P x xa
[PROOF STEP]
show "addr_loc_default (compP f P) hT al = addr_loc_default P hT al"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. addr_loc_default (compP f P) hT al = addr_loc_default P hT al
[PROOF STEP]
by(cases "(P, hT, al)" rule: addr_loc_default.cases) simp_all
[PROOF STATE]
proof (state)
this:
addr_loc_default (compP f P) hT al = addr_loc_default P hT al

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma value_written_aux_compP [simp]: "value_written_aux (compP f P) = value_written_aux P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. value_written_aux (compP f P) = value_written_aux P
[PROOF STEP]
proof(intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. value_written_aux (compP f P) x xa = value_written_aux P x xa
[PROOF STEP]
fix a al
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. value_written_aux (compP f P) x xa = value_written_aux P x xa
[PROOF STEP]
show "value_written_aux (compP f P) a al = value_written_aux P a al"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. value_written_aux (compP f P) a al = value_written_aux P a al
[PROOF STEP]
by(cases "(P, a, al)" rule: value_written_aux.cases)(simp_all add: value_written_aux.simps)
[PROOF STATE]
proof (state)
this:
value_written_aux (compP f P) a al = value_written_aux P a al

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma value_written_compP [simp]: "value_written (compP f P) = value_written P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. value_written (compP f P) = value_written P
[PROOF STEP]
by(simp add: fun_eq_iff value_written.simps)


[STATEMENT]
lemma is_write_seen_compP [simp]: "is_write_seen (compP f P) = is_write_seen P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_write_seen (compP f P) = is_write_seen P
[PROOF STEP]
by(simp add: fun_eq_iff is_write_seen_def)


[STATEMENT]
lemma justification_well_formed_compP [simp]:
  "justification_well_formed (compP f P) = justification_well_formed P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. justification_well_formed (compP f P) = justification_well_formed P
[PROOF STEP]
by(simp add: fun_eq_iff justification_well_formed_def)


[STATEMENT]
lemma happens_before_committed_compP [simp]:
  "happens_before_committed (compP f P) = happens_before_committed P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. happens_before_committed (compP f P) = happens_before_committed P
[PROOF STEP]
by(simp add: fun_eq_iff happens_before_committed_def)


[STATEMENT]
lemma happens_before_committed_weak_compP [simp]:
  "happens_before_committed_weak (compP f P) = happens_before_committed_weak P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. happens_before_committed_weak (compP f P) = happens_before_committed_weak P
[PROOF STEP]
by(simp add: fun_eq_iff happens_before_committed_weak_def)


[STATEMENT]
lemma sync_order_committed_compP [simp]:
  "sync_order_committed (compP f P) = sync_order_committed P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sync_order_committed (compP f P) = sync_order_committed P
[PROOF STEP]
by(simp add: fun_eq_iff sync_order_committed_def)


[STATEMENT]
lemma value_written_committed_compP [simp]:
  "value_written_committed (compP f P) = value_written_committed P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. value_written_committed (compP f P) = value_written_committed P
[PROOF STEP]
by(simp add: fun_eq_iff value_written_committed_def)


[STATEMENT]
lemma uncommitted_reads_see_hb_compP [simp]:
  "uncommitted_reads_see_hb (compP f P) = uncommitted_reads_see_hb P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uncommitted_reads_see_hb (compP f P) = uncommitted_reads_see_hb P
[PROOF STEP]
by(simp add: fun_eq_iff uncommitted_reads_see_hb_def)


[STATEMENT]
lemma external_actions_committed_compP [simp]:
  "external_actions_committed (compP f P) = external_actions_committed P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. external_actions_committed (compP f P) = external_actions_committed P
[PROOF STEP]
by(simp add: fun_eq_iff external_actions_committed_def)


[STATEMENT]
lemma is_justified_by_compP [simp]: "is_justified_by (compP f P) = is_justified_by P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_justified_by (compP f P) = is_justified_by P
[PROOF STEP]
by(simp add: fun_eq_iff is_justified_by.simps)


[STATEMENT]
lemma is_weakly_justified_by_compP [simp]: "is_weakly_justified_by (compP f P) = is_weakly_justified_by P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_weakly_justified_by (compP f P) = is_weakly_justified_by P
[PROOF STEP]
by(simp add: fun_eq_iff is_weakly_justified_by.simps)


[STATEMENT]
lemma legal_execution_compP: "legal_execution (compP f P) = legal_execution P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. legal_execution (compP f P) = legal_execution P
[PROOF STEP]
by(simp add: fun_eq_iff gen_legal_execution.simps)


[STATEMENT]
lemma weakly_legal_execution_compP: "weakly_legal_execution (compP f P) = weakly_legal_execution P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_legal_execution (compP f P) = weakly_legal_execution P
[PROOF STEP]
by(simp add: fun_eq_iff gen_legal_execution.simps)


[STATEMENT]
lemma most_recent_write_for_compP [simp]:
  "most_recent_write_for (compP f P) = most_recent_write_for P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. most_recent_write_for (compP f P) = most_recent_write_for P
[PROOF STEP]
by(simp add: fun_eq_iff most_recent_write_for.simps)


[STATEMENT]
lemma sequentially_consistent_compP [simp]:
  "sequentially_consistent (compP f P) = sequentially_consistent P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sequentially_consistent (compP f P) = sequentially_consistent P
[PROOF STEP]
by(simp add: sequentially_consistent_def split_beta)


[STATEMENT]
lemma conflict_compP [simp]: "non_volatile_conflict (compP f P) = non_volatile_conflict P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_volatile_conflict (compP f P) = non_volatile_conflict P
[PROOF STEP]
by(simp add: fun_eq_iff non_volatile_conflict_def)


[STATEMENT]
lemma correctly_synchronized_compP [simp]:
  "correctly_synchronized (compP f P) = correctly_synchronized P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. correctly_synchronized (compP f P) = correctly_synchronized P
[PROOF STEP]
by(simp add: fun_eq_iff correctly_synchronized_def)


[STATEMENT]
lemma (in heap_base) heap_read_typed_compP [simp]:
  "heap_read_typed (compP f P) = heap_read_typed P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heap_read_typed (compP f P) = heap_read_typed P
[PROOF STEP]
by(intro ext)(simp add: heap_read_typed_def)


[STATEMENT]
theorem if_bisimJ2JVM_weak_bisim:
  assumes wf: "wf_J_prog P"
  shows "delay_bisimulation_diverge_final
    (red_mthr.mthr.if.redT P) (execd_mthr.mthr.if.redT (J2JVM P)) if_bisimJ2JVM if_tlsimJ2JVM
    red_mthr.if.m\<tau>move execd_mthr.if.m\<tau>move red_mthr.mthr.if.mfinal execd_mthr.mthr.if.mfinal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge_final (red_mthr.mthr.if.redT P) (execd_mthr.mthr.if.redT (J2JVM P)) if_bisimJ2JVM if_tlsimJ2JVM red_mthr.if.m\<tau>move execd_mthr.if.m\<tau>move red_mthr.mthr.if.mfinal execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply (simp only: if_bisimJ2JVM_def if_tlsimJ2JVM_def J2JVM_def o_apply)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge_final (red_mthr.mthr.if.redT P) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim red_red0.init_fin_bisim red_red0.init_fin_bisim_wait \<circ>\<^sub>B FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait \<circ>\<^sub>B if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim red_red0.init_fin_bisim \<circ>\<^sub>B FWbisimulation_base.mta_bisim red0_Red1'.init_fin_bisim \<circ>\<^sub>B (=) \<circ>\<^sub>B FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) red_mthr.if.m\<tau>move execd_mthr.if.m\<tau>move red_mthr.mthr.if.mfinal execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule delay_bisimulation_diverge_final_compose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. delay_bisimulation_diverge_final (red_mthr.mthr.if.redT P) ?trsys2.1 (FWbisimulation_base.mbisim red_red0.init_fin_bisim red_red0.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim red_red0.init_fin_bisim) red_mthr.if.m\<tau>move ?\<tau>move2.1 red_mthr.mthr.if.mfinal ?final2.1
 2. delay_bisimulation_diverge_final ?trsys2.1 (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait \<circ>\<^sub>B if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim red0_Red1'.init_fin_bisim \<circ>\<^sub>B (=) \<circ>\<^sub>B FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) ?\<tau>move2.1 execd_mthr.if.m\<tau>move ?final2.1 execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge.mthr_delay_bisimulation_diverge_final)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. FWdelay_bisimulation_diverge red_mthr.init_fin_final (red_mthr.init_fin P) ?final2.4 ?r2.4 red_red0.init_fin_bisim red_red0.init_fin_bisim_wait (red_mthr.init_fin_\<tau>move P) ?\<tau>move2.4
 2. delay_bisimulation_diverge_final (multithreaded_base.redT ?final2.4 ?r2.4 (map NormalAction \<circ> convert_RA)) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait \<circ>\<^sub>B if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim red0_Red1'.init_fin_bisim \<circ>\<^sub>B (=) \<circ>\<^sub>B FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) (\<tau>multithreaded.m\<tau>move ?\<tau>move2.4) execd_mthr.if.m\<tau>move (final_thread.mfinal ?final2.4) execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge.init_fin_FWdelay_bisimulation_diverge)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. FWdelay_bisimulation_diverge final_expr (\<lambda>t ((e, l), h) ta ((e', l'), h'). extTA2J P,P,t \<turnstile> \<langle>e,(h, l)\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle>) final_expr0 ?r2.6 (\<lambda>t. bisim_red_red0) (\<lambda>exs (e0, es0). \<not> final e0) (\<lambda>((e, x), h) ta s'. \<tau>move0 P h e \<and> ta = \<lbrace>\<rbrace>) ?\<tau>move2.6
 2. delay_bisimulation_diverge_final (multithreaded_base.redT red0_mthr.init_fin_final (multithreaded_base.init_fin final_expr0 ?r2.6) (map NormalAction \<circ> convert_RA)) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait \<circ>\<^sub>B if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim red0_Red1'.init_fin_bisim \<circ>\<^sub>B (=) \<circ>\<^sub>B FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) (\<tau>multithreaded.m\<tau>move (\<tau>multithreaded.init_fin_\<tau>move ?\<tau>move2.6)) execd_mthr.if.m\<tau>move (final_thread.mfinal red0_mthr.init_fin_final) execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule red_red0_FWbisim[OF wf_prog_wwf_prog[OF wf]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge_final (multithreaded_base.redT red0_mthr.init_fin_final (red0_mthr.init_fin P) (map NormalAction \<circ> convert_RA)) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait \<circ>\<^sub>B if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim red0_Red1'.init_fin_bisim \<circ>\<^sub>B (=) \<circ>\<^sub>B FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) (\<tau>multithreaded.m\<tau>move (red0_mthr.init_fin_\<tau>move P)) execd_mthr.if.m\<tau>move (final_thread.mfinal red0_mthr.init_fin_final) execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule delay_bisimulation_diverge_final_compose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. delay_bisimulation_diverge_final (multithreaded_base.redT red0_mthr.init_fin_final (red0_mthr.init_fin P) (map NormalAction \<circ> convert_RA)) ?trsys2.10 (FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim red0_Red1'.init_fin_bisim) (\<tau>multithreaded.m\<tau>move (red0_mthr.init_fin_\<tau>move P)) ?\<tau>move2.10 (final_thread.mfinal red0_mthr.init_fin_final) ?final2.10
 2. delay_bisimulation_diverge_final ?trsys2.10 (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) ((=) \<circ>\<^sub>B FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) ?\<tau>move2.10 execd_mthr.if.m\<tau>move ?final2.10 execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge.mthr_delay_bisimulation_diverge_final)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. FWdelay_bisimulation_diverge red0_mthr.init_fin_final (red0_mthr.init_fin P) ?final2.13 ?r2.13 red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait (red0_mthr.init_fin_\<tau>move P) ?\<tau>move2.13
 2. delay_bisimulation_diverge_final (multithreaded_base.redT ?final2.13 ?r2.13 (map NormalAction \<circ> convert_RA)) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) ((=) \<circ>\<^sub>B FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) (\<tau>multithreaded.m\<tau>move ?\<tau>move2.13) execd_mthr.if.m\<tau>move (final_thread.mfinal ?final2.13) execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge.init_fin_FWdelay_bisimulation_diverge)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. FWdelay_bisimulation_diverge final_expr0 (mred0 P) final_expr1 ?r2.15 (\<lambda>t. bisim_red0_Red1) bisim_wait01 (\<lambda>(es, h) ta s. \<tau>Move0 P h es \<and> ta = \<lbrace>\<rbrace>) ?\<tau>move2.15
 2. delay_bisimulation_diverge_final (multithreaded_base.redT Red1_mthr.init_fin_final (multithreaded_base.init_fin final_expr1 ?r2.15) (map NormalAction \<circ> convert_RA)) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) ((=) \<circ>\<^sub>B FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) (\<tau>multithreaded.m\<tau>move (\<tau>multithreaded.init_fin_\<tau>move ?\<tau>move2.15)) execd_mthr.if.m\<tau>move Red1_mthr.if.mfinal execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule red0_Red1'_FWweak_bisim[OF wf])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge_final (Red1_mthr.if.redT False (compP1 P)) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) ((=) \<circ>\<^sub>B FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) (Red1_mthr.if.m\<tau>move (compP1 P)) execd_mthr.if.m\<tau>move Red1_mthr.if.mfinal execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule delay_bisimulation_diverge_final_compose)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. delay_bisimulation_diverge_final (Red1_mthr.if.redT False (compP1 P)) ?trsys2.18 if_mbisim_Red1'_Red1 (=) (Red1_mthr.if.m\<tau>move (compP1 P)) ?\<tau>move2.18 Red1_mthr.if.mfinal ?final2.18
 2. delay_bisimulation_diverge_final ?trsys2.18 (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) ?\<tau>move2.18 execd_mthr.if.m\<tau>move ?final2.18 execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule delay_bisimulation_diverge_final.intro)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. delay_bisimulation_diverge (Red1_mthr.if.redT False (compP1 P)) ?trsys2.18 if_mbisim_Red1'_Red1 (=) (Red1_mthr.if.m\<tau>move (compP1 P)) ?\<tau>move2.18
 2. delay_bisimulation_final_base (Red1_mthr.if.redT False (compP1 P)) ?trsys2.18 if_mbisim_Red1'_Red1 (Red1_mthr.if.m\<tau>move (compP1 P)) ?\<tau>move2.18 Red1_mthr.if.mfinal ?final2.18
 3. delay_bisimulation_diverge_final ?trsys2.18 (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) ?\<tau>move2.18 execd_mthr.if.m\<tau>move ?final2.18 execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule bisimulation_into_delay.delay_bisimulation)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. bisimulation_into_delay (Red1_mthr.if.redT False (compP1 P)) ?trsys2.18 if_mbisim_Red1'_Red1 (=) (Red1_mthr.if.m\<tau>move (compP1 P)) ?\<tau>move2.18
 2. delay_bisimulation_final_base (Red1_mthr.if.redT False (compP1 P)) ?trsys2.18 if_mbisim_Red1'_Red1 (Red1_mthr.if.m\<tau>move (compP1 P)) ?\<tau>move2.18 Red1_mthr.if.mfinal ?final2.18
 3. delay_bisimulation_diverge_final ?trsys2.18 (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) ?\<tau>move2.18 execd_mthr.if.m\<tau>move ?final2.18 execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule if_Red1'_Red1_bisim_into_weak[OF compP1_pres_wf[OF wf]])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. delay_bisimulation_final_base (Red1_mthr.if.redT False (compP1 P)) (Red1_mthr.if.redT True (compP1 P)) if_mbisim_Red1'_Red1 (Red1_mthr.if.m\<tau>move (compP1 P)) (Red1_mthr.if.m\<tau>move (compP1 P)) Red1_mthr.if.mfinal ?final2.18
 2. delay_bisimulation_diverge_final (Red1_mthr.if.redT True (compP1 P)) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) (Red1_mthr.if.m\<tau>move (compP1 P)) execd_mthr.if.m\<tau>move ?final2.18 execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule bisimulation_final.delay_bisimulation_final_base)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bisimulation_final (Red1_mthr.if.redT False (compP1 P)) (Red1_mthr.if.redT True (compP1 P)) if_mbisim_Red1'_Red1 ?tlsim28 Red1_mthr.if.mfinal ?final2.18
 2. delay_bisimulation_diverge_final (Red1_mthr.if.redT True (compP1 P)) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) (Red1_mthr.if.m\<tau>move (compP1 P)) execd_mthr.if.m\<tau>move ?final2.18 execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule if_Red1'_Red1_bisimulation_final[OF compP1_pres_wf[OF wf]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge_final (Red1_mthr.if.redT True (compP1 P)) (execd_mthr.mthr.if.redT (compP2 (compP1 P))) (FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (FWbisimulation_base.mta_bisim Red1_execd.init_fin_bisim) (Red1_mthr.if.m\<tau>move (compP1 P)) execd_mthr.if.m\<tau>move Red1_mthr.if.mfinal execd_mthr.mthr.if.mfinal
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge.mthr_delay_bisimulation_diverge_final)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge Red1_mthr.init_fin_final (Red1_mthr.init_fin True (compP1 P)) exec_mthr.init_fin_final (execd_mthr.init_fin (compP2 (compP1 P))) Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait (Red1_mthr.init_fin_\<tau>move (compP1 P)) (execd_mthr.init_fin_\<tau>move (compP2 (compP1 P)))
[PROOF STEP]
apply(rule FWdelay_bisimulation_diverge.init_fin_FWdelay_bisimulation_diverge)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FWdelay_bisimulation_diverge final_expr1 (mred1 (compP1 P)) JVM_final (mexecd (compP2 (compP1 P))) wbisim1 (bisim_wait1JVM (compP2 (compP1 P))) (\<lambda>(exexs, h) ta s. \<tau>Move1 (compP1 P) h exexs \<and> ta = \<lbrace>\<rbrace>) (\<lambda>((xcp, frs), h) ta s. \<tau>Move2 (compP2 (compP1 P)) (xcp, h, frs) \<and> ta = \<lbrace>\<rbrace>)
[PROOF STEP]
apply(rule Red1_exec1_FWwbisim[OF compP1_pres_wf[OF wf]])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma if_bisimJ2JVM_start:
  assumes wf: "wf_J_prog P"
  and wf_start: "wf_start_state P C M vs"
  shows "if_bisimJ2JVM (init_fin_lift_state Running (J_start_state P C M vs))
                       (init_fin_lift_state Running (JVM_start_state (J2JVM P) C M vs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if_bisimJ2JVM (init_fin_lift_state Running (start_state J_local_start P C M vs)) (init_fin_lift_state Running (start_state JVM_local_start (J2JVM P) C M vs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_J_prog P
wf_start_state P C M vs

goal (1 subgoal):
 1. if_bisimJ2JVM (init_fin_lift_state Running (start_state J_local_start P C M vs)) (init_fin_lift_state Running (start_state JVM_local_start (J2JVM P) C M vs))
[PROOF STEP]
unfolding if_bisimJ2JVM_def J2JVM_def o_apply
[PROOF STATE]
proof (prove)
using this:
wf_J_prog P
wf_start_state P C M vs

goal (1 subgoal):
 1. (FWbisimulation_base.mbisim red_red0.init_fin_bisim red_red0.init_fin_bisim_wait \<circ>\<^sub>B FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait \<circ>\<^sub>B if_mbisim_Red1'_Red1 \<circ>\<^sub>B FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait) (init_fin_lift_state Running (start_state J_local_start P C M vs)) (init_fin_lift_state Running (start_state JVM_local_start (compP2 (compP1 P)) C M vs))
[PROOF STEP]
apply(intro bisim_composeI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim red_red0.init_fin_bisim red_red0.init_fin_bisim_wait (init_fin_lift_state Running (start_state J_local_start P C M vs)) ?s2.2
 2. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait ?s2.2 ?s2.3
 3. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> if_mbisim_Red1'_Red1 ?s2.3 ?s2.4
 4. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait ?s2.4 (init_fin_lift_state Running (start_state JVM_local_start (compP2 (compP1 P)) C M vs))
[PROOF STEP]
apply(rule FWbisimulation_base.init_fin_lift_state_mbisimI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> red_red0.mbisim (start_state J_local_start P C M vs) ?s'5
 2. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait (init_fin_lift_state Running ?s'5) ?s2.3
 3. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> if_mbisim_Red1'_Red1 ?s2.3 ?s2.4
 4. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait ?s2.4 (init_fin_lift_state Running (start_state JVM_local_start (compP2 (compP1 P)) C M vs))
[PROOF STEP]
apply(erule (1) bisim_J_J0_start[OF wf_prog_wwf_prog])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim red0_Red1'.init_fin_bisim red0_Red1'.init_fin_bisim_wait (init_fin_lift_state Running (J0_start_state P C M vs)) ?s2.3
 2. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> if_mbisim_Red1'_Red1 ?s2.3 ?s2.4
 3. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait ?s2.4 (init_fin_lift_state Running (start_state JVM_local_start (compP2 (compP1 P)) C M vs))
[PROOF STEP]
apply(rule FWbisimulation_base.init_fin_lift_state_mbisimI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> red0_Red1'.mbisim (J0_start_state P C M vs) ?s'10
 2. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> if_mbisim_Red1'_Red1 (init_fin_lift_state Running ?s'10) ?s2.4
 3. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait ?s2.4 (init_fin_lift_state Running (start_state JVM_local_start (compP2 (compP1 P)) C M vs))
[PROOF STEP]
apply(erule (1) bisim_J0_J1_start)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> if_mbisim_Red1'_Red1 (init_fin_lift_state Running (J1_start_state (compP1 P) C M vs)) ?s2.4
 2. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait ?s2.4 (init_fin_lift_state Running (start_state JVM_local_start (compP2 (compP1 P)) C M vs))
[PROOF STEP]
apply(erule if_bisim_J1_J1_start[OF compP1_pres_wf])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. wf_start_state P C M vs \<Longrightarrow> wf_start_state (compP1 P) C M vs
 2. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait (init_fin_lift_state Running (J1_start_state (compP1 P) C M vs)) (init_fin_lift_state Running (start_state JVM_local_start (compP2 (compP1 P)) C M vs))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> FWbisimulation_base.mbisim Red1_execd.init_fin_bisim Red1_execd.init_fin_bisim_wait (init_fin_lift_state Running (J1_start_state (compP1 P) C M vs)) (init_fin_lift_state Running (start_state JVM_local_start (compP2 (compP1 P)) C M vs))
[PROOF STEP]
apply(rule FWbisimulation_base.init_fin_lift_state_mbisimI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> Red1_execd.mbisim (J1_start_state (compP1 P) C M vs) (start_state JVM_local_start (compP2 (compP1 P)) C M vs)
[PROOF STEP]
apply(erule bisim_J1_JVM_start[OF compP1_pres_wf])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_start_state P C M vs \<Longrightarrow> wf_start_state (compP1 P) C M vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma red_Runs_eq_mexecd_Runs:
  fixes C M vs
  defines s: "s \<equiv> init_fin_lift_state Running (J_start_state P C M vs)"
  and comps: "cs \<equiv> init_fin_lift_state Running (JVM_start_state (J2JVM P) C M vs)"
  assumes wf: "wf_J_prog P"
  and wf_start: "wf_start_state P C M vs"
  shows "red_mthr.mthr.if.\<E> P s = execd_mthr.mthr.if.\<E> (J2JVM P) cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red_mthr.mthr.if.\<E> P s = execd_mthr.mthr.if.\<E> (J2JVM P) cs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red_mthr.mthr.if.\<E> P s = execd_mthr.mthr.if.\<E> (J2JVM P) cs
[PROOF STEP]
from wf wf_start
[PROOF STATE]
proof (chain)
picking this:
wf_J_prog P
wf_start_state P C M vs
[PROOF STEP]
have bisim: "if_bisimJ2JVM s cs"
[PROOF STATE]
proof (prove)
using this:
wf_J_prog P
wf_start_state P C M vs

goal (1 subgoal):
 1. if_bisimJ2JVM s cs
[PROOF STEP]
unfolding s comps
[PROOF STATE]
proof (prove)
using this:
wf_J_prog P
wf_start_state P C M vs

goal (1 subgoal):
 1. if_bisimJ2JVM (init_fin_lift_state Running (start_state J_local_start P C M vs)) (init_fin_lift_state Running (start_state JVM_local_start (J2JVM P) C M vs))
[PROOF STEP]
by(rule if_bisimJ2JVM_start)
[PROOF STATE]
proof (state)
this:
if_bisimJ2JVM s cs

goal (1 subgoal):
 1. red_mthr.mthr.if.\<E> P s = execd_mthr.mthr.if.\<E> (J2JVM P) cs
[PROOF STEP]
interpret divfin: delay_bisimulation_diverge_final
    "red_mthr.mthr.if.redT P"
    "execd_mthr.mthr.if.redT (J2JVM P)"
    "if_bisimJ2JVM"
    "if_tlsimJ2JVM"
    "red_mthr.if.m\<tau>move"
    "execd_mthr.if.m\<tau>move"
    "red_mthr.mthr.if.mfinal"
    "execd_mthr.mthr.if.mfinal"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delay_bisimulation_diverge_final (red_mthr.mthr.if.redT P) (execd_mthr.mthr.if.redT (J2JVM P)) if_bisimJ2JVM if_tlsimJ2JVM red_mthr.if.m\<tau>move execd_mthr.if.m\<tau>move red_mthr.mthr.if.mfinal execd_mthr.mthr.if.mfinal
[PROOF STEP]
using wf
[PROOF STATE]
proof (prove)
using this:
wf_J_prog P

goal (1 subgoal):
 1. delay_bisimulation_diverge_final (red_mthr.mthr.if.redT P) (execd_mthr.mthr.if.redT (J2JVM P)) if_bisimJ2JVM if_tlsimJ2JVM red_mthr.if.m\<tau>move execd_mthr.if.m\<tau>move red_mthr.mthr.if.mfinal execd_mthr.mthr.if.mfinal
[PROOF STEP]
by(rule if_bisimJ2JVM_weak_bisim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red_mthr.mthr.if.\<E> P s = execd_mthr.mthr.if.\<E> (J2JVM P) cs
[PROOF STEP]
show ?thesis (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red_mthr.mthr.if.\<E> P s = execd_mthr.mthr.if.\<E> (J2JVM P) cs
[PROOF STEP]
proof(intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
assume "E \<in> ?lhs"
[PROOF STATE]
proof (state)
this:
E \<in> red_mthr.mthr.if.\<E> P s

goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
E \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
obtain E' where E: "E = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))"
      and E': "red_mthr.if.mthr.\<tau>Runs s E'"
[PROOF STATE]
proof (prove)
using this:
E \<in> red_mthr.mthr.if.\<E> P s

goal (1 subgoal):
 1. (\<And>E'. \<lbrakk>E = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E')); red_mthr.if.mthr.\<tau>Runs s E'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding red_mthr.if.\<E>_conv_Runs
[PROOF STATE]
proof (prove)
using this:
E \<in> lconcat ` lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) ` llist_of_tllist ` Collect (red_mthr.if.mthr.\<tau>Runs s)

goal (1 subgoal):
 1. (\<And>E'. \<lbrakk>E = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E')); red_mthr.if.mthr.\<tau>Runs s E'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
E = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))
red_mthr.if.mthr.\<tau>Runs s E'

goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
from divfin.simulation_\<tau>Runs1[OF bisim E']
[PROOF STATE]
proof (chain)
picking this:
\<exists>tls2. divfin.\<tau>Runs cs tls2 \<and> tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E' tls2
[PROOF STEP]
obtain E'' where E'': "execd_mthr.if.mthr.\<tau>Runs cs E''"
      and tlsim: "tllist_all2 if_tlsimJ2JVM (option.rel_option if_bisimJ2JVM) E' E''"
[PROOF STATE]
proof (prove)
using this:
\<exists>tls2. divfin.\<tau>Runs cs tls2 \<and> tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E' tls2

goal (1 subgoal):
 1. (\<And>E''. \<lbrakk>execd_mthr.if.mthr.\<tau>Runs cs E''; tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E' E''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding J2JVM_def o_apply
[PROOF STATE]
proof (prove)
using this:
\<exists>tls2. \<tau>trsys.\<tau>Runs (multithreaded_base.redT exec_mthr.init_fin_final (execd_mthr.init_fin (compP2 (compP1 P))) (\<lambda>x. map NormalAction (convert_RA x))) execd_mthr.if.m\<tau>move cs tls2 \<and> tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E' tls2

goal (1 subgoal):
 1. (\<And>E''. \<lbrakk>\<tau>trsys.\<tau>Runs (multithreaded_base.redT exec_mthr.init_fin_final (execd_mthr.init_fin (compP2 (compP1 P))) (\<lambda>x. map NormalAction (convert_RA x))) execd_mthr.if.m\<tau>move cs E''; tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E' E''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
execd_mthr.if.mthr.\<tau>Runs cs E''
tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E' E''

goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
let ?E = "lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E''))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
from tlsim
[PROOF STATE]
proof (chain)
picking this:
tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E' E''
[PROOF STEP]
have "llist_all2 if_tlsimJ2JVM (llist_of_tllist E') (llist_of_tllist E'')"
[PROOF STATE]
proof (prove)
using this:
tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E' E''

goal (1 subgoal):
 1. divfin.Tlsiml (llist_of_tllist E') (llist_of_tllist E'')
[PROOF STEP]
by(rule tllist_all2D_llist_all2_llist_of_tllist)
[PROOF STATE]
proof (state)
this:
divfin.Tlsiml (llist_of_tllist E') (llist_of_tllist E'')

goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
hence "llist_all2 (=) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))
                             (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E''))"
[PROOF STATE]
proof (prove)
using this:
divfin.Tlsiml (llist_of_tllist E') (llist_of_tllist E'')

goal (1 subgoal):
 1. llist_all2 (=) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E')) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E''))
[PROOF STEP]
unfolding llist_all2_lmap1 llist_all2_lmap2
[PROOF STATE]
proof (prove)
using this:
divfin.Tlsiml (llist_of_tllist E') (llist_of_tllist E'')

goal (1 subgoal):
 1. llist_all2 (\<lambda>x y. (case x of (t, ta) \<Rightarrow> llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) = (case y of (t, ta) \<Rightarrow> llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>))) (llist_of_tllist E') (llist_of_tllist E'')
[PROOF STEP]
by(rule llist_all2_mono)(auto simp add: if_tlsimJ2JVM_def FWbisimulation_base.mta_bisim_def ta_bisim_def)
[PROOF STATE]
proof (state)
this:
llist_all2 (=) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E')) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E''))

goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
hence "?E = E"
[PROOF STATE]
proof (prove)
using this:
llist_all2 (=) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E')) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E''))

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) = E
[PROOF STEP]
unfolding llist.rel_eq E
[PROOF STATE]
proof (prove)
using this:
lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E') = lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) = E

goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) = E

goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
from E''
[PROOF STATE]
proof (chain)
picking this:
execd_mthr.if.mthr.\<tau>Runs cs E''
[PROOF STEP]
have "?E \<in> ?rhs"
[PROOF STATE]
proof (prove)
using this:
execd_mthr.if.mthr.\<tau>Runs cs E''

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
[PROOF STEP]
unfolding J2JVM_def o_apply execd_mthr.if.\<E>_conv_Runs
[PROOF STATE]
proof (prove)
using this:
\<tau>trsys.\<tau>Runs (multithreaded_base.redT exec_mthr.init_fin_final (execd_mthr.init_fin (compP2 (compP1 P))) (\<lambda>x. map NormalAction (convert_RA x))) execd_mthr.if.m\<tau>move cs E''

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) \<in> lconcat ` lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) ` llist_of_tllist ` Collect (\<tau>trsys.\<tau>Runs (multithreaded_base.redT exec_mthr.init_fin_final (execd_mthr.init_fin (compP2 (compP1 P))) (\<lambda>x. map NormalAction (convert_RA x))) execd_mthr.if.m\<tau>move cs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs

goal (2 subgoals):
 1. \<And>x. x \<in> red_mthr.mthr.if.\<E> P s \<Longrightarrow> x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
 2. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
finally (subst)
[PROOF STATE]
proof (chain)
picking this:
E \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
[PROOF STEP]
show "E \<in> ?rhs"
[PROOF STATE]
proof (prove)
using this:
E \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs

goal (1 subgoal):
 1. E \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
E \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs

goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
fix E
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
assume "E \<in> ?rhs"
[PROOF STATE]
proof (state)
this:
E \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs

goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
E \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs
[PROOF STEP]
obtain E' where E: "E = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))"
      and E': "execd_mthr.if.mthr.\<tau>Runs cs E'"
[PROOF STATE]
proof (prove)
using this:
E \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs

goal (1 subgoal):
 1. (\<And>E'. \<lbrakk>E = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E')); execd_mthr.if.mthr.\<tau>Runs cs E'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding execd_mthr.if.\<E>_conv_Runs J2JVM_def o_apply
[PROOF STATE]
proof (prove)
using this:
E \<in> lconcat ` lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) ` llist_of_tllist ` Collect (\<tau>trsys.\<tau>Runs (multithreaded_base.redT exec_mthr.init_fin_final (execd_mthr.init_fin (compP2 (compP1 P))) (\<lambda>x. map NormalAction (convert_RA x))) execd_mthr.if.m\<tau>move cs)

goal (1 subgoal):
 1. (\<And>E'. \<lbrakk>E = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E')); \<tau>trsys.\<tau>Runs (multithreaded_base.redT exec_mthr.init_fin_final (execd_mthr.init_fin (compP2 (compP1 P))) (\<lambda>x. map NormalAction (convert_RA x))) execd_mthr.if.m\<tau>move cs E'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
E = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))
execd_mthr.if.mthr.\<tau>Runs cs E'

goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
from divfin.simulation_\<tau>Runs2[OF bisim, simplified J2JVM_def o_apply, OF E']
[PROOF STATE]
proof (chain)
picking this:
\<exists>tls1. red_mthr.if.mthr.\<tau>Runs s tls1 \<and> tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) tls1 E'
[PROOF STEP]
obtain E'' where E'': "red_mthr.if.mthr.\<tau>Runs s E''"
      and tlsim: "tllist_all2 if_tlsimJ2JVM (option.rel_option if_bisimJ2JVM) E'' E'"
[PROOF STATE]
proof (prove)
using this:
\<exists>tls1. red_mthr.if.mthr.\<tau>Runs s tls1 \<and> tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) tls1 E'

goal (1 subgoal):
 1. (\<And>E''. \<lbrakk>red_mthr.if.mthr.\<tau>Runs s E''; tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E'' E'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
red_mthr.if.mthr.\<tau>Runs s E''
tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E'' E'

goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
let ?E = "lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E''))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
from tlsim
[PROOF STATE]
proof (chain)
picking this:
tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E'' E'
[PROOF STEP]
have "llist_all2 if_tlsimJ2JVM (llist_of_tllist E'') (llist_of_tllist E')"
[PROOF STATE]
proof (prove)
using this:
tllist_all2 if_tlsimJ2JVM (rel_option if_bisimJ2JVM) E'' E'

goal (1 subgoal):
 1. divfin.Tlsiml (llist_of_tllist E'') (llist_of_tllist E')
[PROOF STEP]
by(rule tllist_all2D_llist_all2_llist_of_tllist)
[PROOF STATE]
proof (state)
this:
divfin.Tlsiml (llist_of_tllist E'') (llist_of_tllist E')

goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
hence "llist_all2 (=) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E''))
                             (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))"
[PROOF STATE]
proof (prove)
using this:
divfin.Tlsiml (llist_of_tllist E'') (llist_of_tllist E')

goal (1 subgoal):
 1. llist_all2 (=) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))
[PROOF STEP]
unfolding llist_all2_lmap1 llist_all2_lmap2
[PROOF STATE]
proof (prove)
using this:
divfin.Tlsiml (llist_of_tllist E'') (llist_of_tllist E')

goal (1 subgoal):
 1. llist_all2 (\<lambda>x y. (case x of (t, ta) \<Rightarrow> llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) = (case y of (t, ta) \<Rightarrow> llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>))) (llist_of_tllist E'') (llist_of_tllist E')
[PROOF STEP]
by(rule llist_all2_mono)(auto simp add: if_tlsimJ2JVM_def FWbisimulation_base.mta_bisim_def ta_bisim_def)
[PROOF STATE]
proof (state)
this:
llist_all2 (=) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))

goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
hence "?E = E"
[PROOF STATE]
proof (prove)
using this:
llist_all2 (=) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) = E
[PROOF STEP]
unfolding llist.rel_eq E
[PROOF STATE]
proof (prove)
using this:
lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'') = lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E')

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) = lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) = E

goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) = E

goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
from E''
[PROOF STATE]
proof (chain)
picking this:
red_mthr.if.mthr.\<tau>Runs s E''
[PROOF STEP]
have "?E \<in> ?lhs"
[PROOF STATE]
proof (prove)
using this:
red_mthr.if.mthr.\<tau>Runs s E''

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
unfolding red_mthr.if.\<E>_conv_Runs
[PROOF STATE]
proof (prove)
using this:
red_mthr.if.mthr.\<tau>Runs s E''

goal (1 subgoal):
 1. lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) \<in> lconcat ` lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) ` llist_of_tllist ` Collect (red_mthr.if.mthr.\<tau>Runs s)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lconcat (lmap (\<lambda>(t, ta). llist_of (map (Pair t) \<lbrace>ta\<rbrace>\<^bsub>o\<^esub>)) (llist_of_tllist E'')) \<in> red_mthr.mthr.if.\<E> P s

goal (1 subgoal):
 1. \<And>x. x \<in> execd_mthr.mthr.if.\<E> (J2JVM P) cs \<Longrightarrow> x \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
finally (subst)
[PROOF STATE]
proof (chain)
picking this:
E \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
show "E \<in> ?lhs"
[PROOF STATE]
proof (prove)
using this:
E \<in> red_mthr.mthr.if.\<E> P s

goal (1 subgoal):
 1. E \<in> red_mthr.mthr.if.\<E> P s
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
E \<in> red_mthr.mthr.if.\<E> P s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
red_mthr.mthr.if.\<E> P s = execd_mthr.mthr.if.\<E> (J2JVM P) cs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma red_\<E>_eq_mexecd_\<E>:
  "\<lbrakk> wf_J_prog P; wf_start_state P C M vs \<rbrakk>
  \<Longrightarrow> J_\<E> P C M vs Running = JVMd_\<E> (J2JVM P) C M vs Running"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_J_prog P; wf_start_state P C M vs\<rbrakk> \<Longrightarrow> red_mthr.\<E>_start P J_local_start P C M vs Running = execd_mthr.\<E>_start (J2JVM P) JVM_local_start (J2JVM P) C M vs Running
[PROOF STEP]
by(simp only: red_Runs_eq_mexecd_Runs)


[STATEMENT]
theorem J2JVM_jmm_correct:
  assumes wf: "wf_J_prog P"
  and wf_start: "wf_start_state P C M vs"
  shows "legal_execution P (J_\<E> P C M vs Running) (E, ws) \<longleftrightarrow>
         legal_execution (J2JVM P) (JVMd_\<E> (J2JVM P) C M vs Running) (E, ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. legal_execution P (red_mthr.\<E>_start P J_local_start P C M vs Running) (E, ws) = legal_execution (J2JVM P) (execd_mthr.\<E>_start (J2JVM P) JVM_local_start (J2JVM P) C M vs Running) (E, ws)
[PROOF STEP]
by(simp only: red_\<E>_eq_mexecd_\<E>[OF assms] J2JVM_def o_apply compP1_def compP2_def legal_execution_compP)


[STATEMENT]
theorem J2JVM_jmm_correct_weak:
  assumes wf: "wf_J_prog P"
  and wf_start: "wf_start_state P C M vs"
  shows "weakly_legal_execution P (J_\<E> P C M vs Running) (E, ws) \<longleftrightarrow>
         weakly_legal_execution (J2JVM P) (JVMd_\<E> (J2JVM P) C M vs Running) (E, ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weakly_legal_execution P (red_mthr.\<E>_start P J_local_start P C M vs Running) (E, ws) = weakly_legal_execution (J2JVM P) (execd_mthr.\<E>_start (J2JVM P) JVM_local_start (J2JVM P) C M vs Running) (E, ws)
[PROOF STEP]
by(simp only: red_\<E>_eq_mexecd_\<E>[OF assms] J2JVM_def o_apply compP1_def compP2_def weakly_legal_execution_compP)


[STATEMENT]
theorem J2JVM_jmm_correctly_synchronized:
  assumes wf: "wf_J_prog P"
  and wf_start: "wf_start_state P C M vs"
  shows "correctly_synchronized (J2JVM P) (JVMd_\<E> (J2JVM P) C M vs Running) \<longleftrightarrow>
         correctly_synchronized P (J_\<E> P C M vs Running)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. correctly_synchronized (J2JVM P) (execd_mthr.\<E>_start (J2JVM P) JVM_local_start (J2JVM P) C M vs Running) = correctly_synchronized P (red_mthr.\<E>_start P J_local_start P C M vs Running)
[PROOF STEP]
by(simp only: red_\<E>_eq_mexecd_\<E>[OF assms] J2JVM_def o_apply compP1_def compP2_def correctly_synchronized_compP)


[STATEMENT]
lemma mono_Union:
assumes "mono Retr"
shows "Union (Retr ` Theta) \<le> Retr (Union Theta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (Retr ` Theta) \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (Retr ` Theta) \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
have "\<forall> theta' \<in> Retr ` Theta. theta' \<subseteq> Retr (Union Theta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>theta'\<in>Retr ` Theta. theta' \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr

goal (1 subgoal):
 1. \<forall>theta'\<in>Retr ` Theta. theta' \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
unfolding mono_def
[PROOF STATE]
proof (prove)
using this:
\<forall>theta theta'. theta \<subseteq> theta' \<longrightarrow> Retr theta \<subseteq> Retr theta'

goal (1 subgoal):
 1. \<forall>theta'\<in>Retr ` Theta. theta' \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>theta'\<in>Retr ` Theta. theta' \<subseteq> Retr (\<Union> Theta)

goal (1 subgoal):
 1. \<Union> (Retr ` Theta) \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>theta'\<in>Retr ` Theta. theta' \<subseteq> Retr (\<Union> Theta)

goal (1 subgoal):
 1. \<Union> (Retr ` Theta) \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Union> (Retr ` Theta) \<subseteq> Retr (\<Union> Theta)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mono_Un:
assumes "mono Retr"
shows "Retr theta Un Retr theta' \<subseteq> Retr (theta Un theta')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Retr theta \<union> Retr theta' \<subseteq> Retr (theta \<union> theta')
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr

goal (1 subgoal):
 1. Retr theta \<union> Retr theta' \<subseteq> Retr (theta \<union> theta')
[PROOF STEP]
unfolding mono_def
[PROOF STATE]
proof (prove)
using this:
\<forall>theta theta'. theta \<subseteq> theta' \<longrightarrow> Retr theta \<subseteq> Retr theta'

goal (1 subgoal):
 1. Retr theta \<union> Retr theta' \<subseteq> Retr (theta \<union> theta')
[PROOF STEP]
by (metis Un_least Un_upper1 Un_upper2)


[STATEMENT]
lemma sym_Union:
assumes "\<And>theta. theta \<in> Theta \<Longrightarrow> sym theta"
shows "sym (Union Theta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (\<Union> Theta)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?theta \<in> Theta \<Longrightarrow> sym ?theta

goal (1 subgoal):
 1. sym (\<Union> Theta)
[PROOF STEP]
unfolding sym_def
[PROOF STATE]
proof (prove)
using this:
?theta \<in> Theta \<Longrightarrow> \<forall>x y. (x, y) \<in> ?theta \<longrightarrow> (y, x) \<in> ?theta

goal (1 subgoal):
 1. \<forall>x y. (x, y) \<in> \<Union> Theta \<longrightarrow> (y, x) \<in> \<Union> Theta
[PROOF STEP]
by blast


[STATEMENT]
lemma sym_Un:
assumes "sym theta1" and "sym theta2"
shows "sym (theta1 Un theta2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (theta1 \<union> theta2)
[PROOF STEP]
using assms sym_Union[of "{theta1,theta2}"]
[PROOF STATE]
proof (prove)
using this:
sym theta1
sym theta2
(\<And>theta. theta \<in> {theta1, theta2} \<Longrightarrow> sym theta) \<Longrightarrow> sym (\<Union> {theta1, theta2})

goal (1 subgoal):
 1. sym (theta1 \<union> theta2)
[PROOF STEP]
by auto


[STATEMENT]
lemma simul_Union:
assumes "mono Retr"
and "\<And>theta. theta \<in> Theta \<Longrightarrow> simul Retr theta"
shows "simul Retr (Union Theta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simul Retr (\<Union> Theta)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simul Retr (\<Union> Theta)
[PROOF STEP]
have "\<forall> theta \<in> Theta. theta \<subseteq> Retr theta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>theta\<in>Theta. theta \<subseteq> Retr theta
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
?theta \<in> Theta \<Longrightarrow> simul Retr ?theta

goal (1 subgoal):
 1. \<forall>theta\<in>Theta. theta \<subseteq> Retr theta
[PROOF STEP]
unfolding simul_def
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
?theta \<in> Theta \<Longrightarrow> ?theta \<subseteq> Retr ?theta

goal (1 subgoal):
 1. \<forall>theta\<in>Theta. theta \<subseteq> Retr theta
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>theta\<in>Theta. theta \<subseteq> Retr theta

goal (1 subgoal):
 1. simul Retr (\<Union> Theta)
[PROOF STEP]
hence "Union Theta \<subseteq> Union (Retr ` Theta)"
[PROOF STATE]
proof (prove)
using this:
\<forall>theta\<in>Theta. theta \<subseteq> Retr theta

goal (1 subgoal):
 1. \<Union> Theta \<subseteq> \<Union> (Retr ` Theta)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Union> Theta \<subseteq> \<Union> (Retr ` Theta)

goal (1 subgoal):
 1. simul Retr (\<Union> Theta)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Union> Theta \<subseteq> \<Union> (Retr ` Theta)

goal (1 subgoal):
 1. simul Retr (\<Union> Theta)
[PROOF STEP]
have "... \<subseteq> Retr (Union Theta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (Retr ` Theta) \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
using mono_Union assms
[PROOF STATE]
proof (prove)
using this:
Bisim.mono ?Retr \<Longrightarrow> \<Union> (?Retr ` ?Theta) \<subseteq> ?Retr (\<Union> ?Theta)
Bisim.mono Retr
?theta \<in> Theta \<Longrightarrow> simul Retr ?theta

goal (1 subgoal):
 1. \<Union> (Retr ` Theta) \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
unfolding mono_def
[PROOF STATE]
proof (prove)
using this:
\<forall>theta theta'. theta \<subseteq> theta' \<longrightarrow> ?Retr theta \<subseteq> ?Retr theta' \<Longrightarrow> \<Union> (?Retr ` ?Theta) \<subseteq> ?Retr (\<Union> ?Theta)
\<forall>theta theta'. theta \<subseteq> theta' \<longrightarrow> Retr theta \<subseteq> Retr theta'
?theta \<in> Theta \<Longrightarrow> simul Retr ?theta

goal (1 subgoal):
 1. \<Union> (Retr ` Theta) \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (Retr ` Theta) \<subseteq> Retr (\<Union> Theta)

goal (1 subgoal):
 1. simul Retr (\<Union> Theta)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Union> Theta \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
have "Union Theta \<subseteq> Retr (Union Theta)"
[PROOF STATE]
proof (prove)
using this:
\<Union> Theta \<subseteq> Retr (\<Union> Theta)

goal (1 subgoal):
 1. \<Union> Theta \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Union> Theta \<subseteq> Retr (\<Union> Theta)

goal (1 subgoal):
 1. simul Retr (\<Union> Theta)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union> Theta \<subseteq> Retr (\<Union> Theta)

goal (1 subgoal):
 1. simul Retr (\<Union> Theta)
[PROOF STEP]
unfolding simul_def
[PROOF STATE]
proof (prove)
using this:
\<Union> Theta \<subseteq> Retr (\<Union> Theta)

goal (1 subgoal):
 1. \<Union> Theta \<subseteq> Retr (\<Union> Theta)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
simul Retr (\<Union> Theta)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma simul_Un:
assumes "mono Retr" and "simul Retr theta1" and "simul Retr theta2"
shows "simul Retr (theta1 Un theta2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simul Retr (theta1 \<union> theta2)
[PROOF STEP]
using assms simul_Union[of Retr "{theta1,theta2}"]
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
simul Retr theta1
simul Retr theta2
\<lbrakk>Bisim.mono Retr; \<And>theta. theta \<in> {theta1, theta2} \<Longrightarrow> simul Retr theta\<rbrakk> \<Longrightarrow> simul Retr (\<Union> {theta1, theta2})

goal (1 subgoal):
 1. simul Retr (theta1 \<union> theta2)
[PROOF STEP]
by auto


[STATEMENT]
lemma bisim_Union:
assumes "mono Retr" and "\<And>theta. theta \<in> Theta \<Longrightarrow> bisim Retr theta"
shows "bisim Retr (Union Theta)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisim Retr (\<Union> Theta)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
?theta \<in> Theta \<Longrightarrow> bisim Retr ?theta

goal (1 subgoal):
 1. bisim Retr (\<Union> Theta)
[PROOF STEP]
unfolding bisim_def
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
?theta \<in> Theta \<Longrightarrow> sym ?theta \<and> simul Retr ?theta

goal (1 subgoal):
 1. sym (\<Union> Theta) \<and> simul Retr (\<Union> Theta)
[PROOF STEP]
using sym_Union simul_Union
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
?theta \<in> Theta \<Longrightarrow> sym ?theta \<and> simul Retr ?theta
(\<And>theta. theta \<in> ?Theta \<Longrightarrow> sym theta) \<Longrightarrow> sym (\<Union> ?Theta)
\<lbrakk>Bisim.mono ?Retr; \<And>theta. theta \<in> ?Theta \<Longrightarrow> simul ?Retr theta\<rbrakk> \<Longrightarrow> simul ?Retr (\<Union> ?Theta)

goal (1 subgoal):
 1. sym (\<Union> Theta) \<and> simul Retr (\<Union> Theta)
[PROOF STEP]
by blast


[STATEMENT]
lemma bisim_Un:
assumes "mono Retr" and "bisim Retr theta1" and "bisim Retr theta2"
shows "bisim Retr (theta1 Un theta2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisim Retr (theta1 \<union> theta2)
[PROOF STEP]
using assms bisim_Union[of Retr "{theta1,theta2}"]
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
bisim Retr theta1
bisim Retr theta2
\<lbrakk>Bisim.mono Retr; \<And>theta. theta \<in> {theta1, theta2} \<Longrightarrow> bisim Retr theta\<rbrakk> \<Longrightarrow> bisim Retr (\<Union> {theta1, theta2})

goal (1 subgoal):
 1. bisim Retr (theta1 \<union> theta2)
[PROOF STEP]
by auto


[STATEMENT]
lemma bisim_bis[simp]:
assumes "mono Retr"
shows "bisim Retr (bis Retr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisim Retr (bis Retr)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr

goal (1 subgoal):
 1. bisim Retr (bis Retr)
[PROOF STEP]
unfolding mono_def
[PROOF STATE]
proof (prove)
using this:
\<forall>theta theta'. theta \<subseteq> theta' \<longrightarrow> Retr theta \<subseteq> Retr theta'

goal (1 subgoal):
 1. bisim Retr (bis Retr)
[PROOF STEP]
by (metis CollectD assms bis_def bisim_Union)


[STATEMENT]
lemma bis_raw_coind:
assumes "mono Retr" and "sym theta" and "theta \<subseteq> Retr theta"
shows "theta \<subseteq> bis Retr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
sym theta
theta \<subseteq> Retr theta

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
unfolding mono_def bis_def bisim_def simul_def
[PROOF STATE]
proof (prove)
using this:
\<forall>theta theta'. theta \<subseteq> theta' \<longrightarrow> Retr theta \<subseteq> Retr theta'
sym theta
theta \<subseteq> Retr theta

goal (1 subgoal):
 1. theta \<subseteq> \<Union> {theta. sym theta \<and> theta \<subseteq> Retr theta}
[PROOF STEP]
by blast


[STATEMENT]
lemma bis_prefix[simp]:
assumes "mono Retr"
shows "bis Retr \<subseteq> Retr (bis Retr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bis Retr \<subseteq> Retr (bis Retr)
[PROOF STEP]
by (metis assms bisim_bis bisim_def simul_def)


[STATEMENT]
lemma bis_coind:
assumes *: "mono Retr" and "sym theta" and **: "theta \<subseteq> Retr (theta Un (bis Retr))"
shows "theta \<subseteq> bis Retr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
let ?theta' = "theta Un (bis Retr)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
have "sym ?theta'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (theta \<union> bis Retr)
[PROOF STEP]
by (metis Bisim.sym_Un sym_bis assms)
[PROOF STATE]
proof (state)
this:
sym (theta \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sym (theta \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
have "?theta' \<subseteq> Retr ?theta'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<union> bis Retr \<subseteq> Retr (theta \<union> bis Retr)
[PROOF STEP]
by (metis assms mono_Un Un_least bis_prefix le_supI2 subset_trans)
[PROOF STATE]
proof (state)
this:
theta \<union> bis Retr \<subseteq> Retr (theta \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sym (theta \<union> bis Retr)
theta \<union> bis Retr \<subseteq> Retr (theta \<union> bis Retr)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sym (theta \<union> bis Retr)
theta \<union> bis Retr \<subseteq> Retr (theta \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
using * bis_raw_coind
[PROOF STATE]
proof (prove)
using this:
sym (theta \<union> bis Retr)
theta \<union> bis Retr \<subseteq> Retr (theta \<union> bis Retr)
Bisim.mono Retr
\<lbrakk>Bisim.mono ?Retr; sym ?theta; ?theta \<subseteq> ?Retr ?theta\<rbrakk> \<Longrightarrow> ?theta \<subseteq> bis ?Retr

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
theta \<subseteq> bis Retr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bis_coind2:
assumes *: "mono Retr" and
**: "theta \<subseteq> Retr (theta Un (bis Retr))" and
***: "theta ^-1 \<subseteq> Retr ((theta ^-1) Un (bis Retr))"
shows "theta \<subseteq> bis Retr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
let ?th = "theta Un theta ^-1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
have "sym ?th"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym (theta \<union> theta\<inverse>)
[PROOF STEP]
by (metis sym_Un_converse)
[PROOF STATE]
proof (state)
this:
sym (theta \<union> theta\<inverse>)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sym (theta \<union> theta\<inverse>)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sym (theta \<union> theta\<inverse>)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
have "?th \<subseteq> Retr (theta Un (bis Retr)) Un Retr (theta ^-1 Un (bis Retr))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> bis Retr) \<union> Retr (theta\<inverse> \<union> bis Retr)
[PROOF STEP]
using ** *** Un_mono
[PROOF STATE]
proof (prove)
using this:
theta \<subseteq> Retr (theta \<union> bis Retr)
theta\<inverse> \<subseteq> Retr (theta\<inverse> \<union> bis Retr)
\<lbrakk>?A \<subseteq> ?C; ?B \<subseteq> ?D\<rbrakk> \<Longrightarrow> ?A \<union> ?B \<subseteq> ?C \<union> ?D

goal (1 subgoal):
 1. theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> bis Retr) \<union> Retr (theta\<inverse> \<union> bis Retr)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> bis Retr) \<union> Retr (theta\<inverse> \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> bis Retr) \<union> Retr (theta\<inverse> \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
have "... \<subseteq> Retr ((theta Un (bis Retr)) Un (theta ^-1 Un (bis Retr)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Retr (theta \<union> bis Retr) \<union> Retr (theta\<inverse> \<union> bis Retr) \<subseteq> Retr (theta \<union> bis Retr \<union> (theta\<inverse> \<union> bis Retr))
[PROOF STEP]
using * mono_Un
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
Bisim.mono ?Retr \<Longrightarrow> ?Retr ?theta \<union> ?Retr ?theta' \<subseteq> ?Retr (?theta \<union> ?theta')

goal (1 subgoal):
 1. Retr (theta \<union> bis Retr) \<union> Retr (theta\<inverse> \<union> bis Retr) \<subseteq> Retr (theta \<union> bis Retr \<union> (theta\<inverse> \<union> bis Retr))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Retr (theta \<union> bis Retr) \<union> Retr (theta\<inverse> \<union> bis Retr) \<subseteq> Retr (theta \<union> bis Retr \<union> (theta\<inverse> \<union> bis Retr))

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Retr (theta \<union> bis Retr) \<union> Retr (theta\<inverse> \<union> bis Retr) \<subseteq> Retr (theta \<union> bis Retr \<union> (theta\<inverse> \<union> bis Retr))

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
have "... = Retr (?th Un (bis Retr))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Retr (theta \<union> bis Retr \<union> (theta\<inverse> \<union> bis Retr)) = Retr (theta \<union> theta\<inverse> \<union> bis Retr)
[PROOF STEP]
by (metis Un_assoc Un_commute Un_left_absorb)
[PROOF STATE]
proof (state)
this:
Retr (theta \<union> bis Retr \<union> (theta\<inverse> \<union> bis Retr)) = Retr (theta \<union> theta\<inverse> \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> theta\<inverse> \<union> bis Retr)
[PROOF STEP]
have "?th \<subseteq> Retr (?th Un (bis Retr))"
[PROOF STATE]
proof (prove)
using this:
theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> theta\<inverse> \<union> bis Retr)

goal (1 subgoal):
 1. theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> theta\<inverse> \<union> bis Retr)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> theta\<inverse> \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> theta\<inverse> \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sym (theta \<union> theta\<inverse>)
theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> theta\<inverse> \<union> bis Retr)
[PROOF STEP]
have "?th \<subseteq> bis Retr"
[PROOF STATE]
proof (prove)
using this:
sym (theta \<union> theta\<inverse>)
theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> theta\<inverse> \<union> bis Retr)

goal (1 subgoal):
 1. theta \<union> theta\<inverse> \<subseteq> bis Retr
[PROOF STEP]
using assms bis_coind
[PROOF STATE]
proof (prove)
using this:
sym (theta \<union> theta\<inverse>)
theta \<union> theta\<inverse> \<subseteq> Retr (theta \<union> theta\<inverse> \<union> bis Retr)
Bisim.mono Retr
theta \<subseteq> Retr (theta \<union> bis Retr)
theta\<inverse> \<subseteq> Retr (theta\<inverse> \<union> bis Retr)
\<lbrakk>Bisim.mono ?Retr; sym ?theta; ?theta \<subseteq> ?Retr (?theta \<union> bis ?Retr)\<rbrakk> \<Longrightarrow> ?theta \<subseteq> bis ?Retr

goal (1 subgoal):
 1. theta \<union> theta\<inverse> \<subseteq> bis Retr
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
theta \<union> theta\<inverse> \<subseteq> bis Retr

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
theta \<union> theta\<inverse> \<subseteq> bis Retr

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
theta \<subseteq> bis Retr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bis_raw_coind2:
assumes *: "mono Retr" and
**: "theta \<subseteq> Retr theta" and
***: "theta ^-1 \<subseteq> Retr (theta ^-1)"
shows "theta \<subseteq> bis Retr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
have "theta \<subseteq> Retr (theta Un (bis Retr))" and
  "theta ^-1 \<subseteq> Retr ((theta ^-1) Un (bis Retr))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. theta \<subseteq> Retr (theta \<union> bis Retr) &&& theta\<inverse> \<subseteq> Retr (theta\<inverse> \<union> bis Retr)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Bisim.mono Retr
theta \<subseteq> Retr theta
theta\<inverse> \<subseteq> Retr (theta\<inverse>)

goal (1 subgoal):
 1. theta \<subseteq> Retr (theta \<union> bis Retr) &&& theta\<inverse> \<subseteq> Retr (theta\<inverse> \<union> bis Retr)
[PROOF STEP]
by(metis mono_Un le_supI1 subset_trans)+
[PROOF STATE]
proof (state)
this:
theta \<subseteq> Retr (theta \<union> bis Retr)
theta\<inverse> \<subseteq> Retr (theta\<inverse> \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
theta \<subseteq> Retr (theta \<union> bis Retr)
theta\<inverse> \<subseteq> Retr (theta\<inverse> \<union> bis Retr)

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
using * bis_coind2
[PROOF STATE]
proof (prove)
using this:
theta \<subseteq> Retr (theta \<union> bis Retr)
theta\<inverse> \<subseteq> Retr (theta\<inverse> \<union> bis Retr)
Bisim.mono Retr
\<lbrakk>Bisim.mono ?Retr; ?theta \<subseteq> ?Retr (?theta \<union> bis ?Retr); ?theta\<inverse> \<subseteq> ?Retr (?theta\<inverse> \<union> bis ?Retr)\<rbrakk> \<Longrightarrow> ?theta \<subseteq> bis ?Retr

goal (1 subgoal):
 1. theta \<subseteq> bis Retr
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
theta \<subseteq> bis Retr

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mono_bis:
assumes "mono Retr1"  and "mono Retr2"
and "\<And> theta. Retr1 theta \<subseteq> Retr2 theta"
shows "bis Retr1 \<subseteq> bis Retr2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bis Retr1 \<subseteq> bis Retr2
[PROOF STEP]
by (metis assms bis_prefix bis_raw_coind subset_trans sym_bis)


[STATEMENT]
lemma weakenStatImpMonotonic:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   A :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q :: "('a, 'b, 'c) psi"
  and   B :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"

  assumes "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<A> Q"
  and     "A \<subseteq> B"

  shows "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<B> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<B> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<lessapprox>\<^sub>w<A> Q
A \<subseteq> B

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<B> Q
[PROOF STEP]
by(auto simp add: weakenStatImp_def)


[STATEMENT]
lemma weakenStatImpI:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   \<Psi>' :: 'b

  assumes "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
  and     "insertAssertion(extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame Q') \<Psi>"
  and     "(\<Psi>, P, Q') \<in> Rel"

  shows "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>
(\<Psi>, P, Q') \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
by(auto simp add: weakenStatImp_def)


[STATEMENT]
lemma weakenStatImpE:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   \<Psi>' :: 'b

  assumes "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q"

  obtains Q' where "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'" and "insertAssertion(extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame Q') \<Psi> " and "(\<Psi>, P, Q') \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'; insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>; (\<Psi>, P, Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'; insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>; (\<Psi>, P, Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: weakenStatImp_def)


[STATEMENT]
lemma weakStatImpWeakenStatImp:
  fixes \<Psi>  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"

  assumes cSim: "\<Psi> \<rhd> P \<lessapprox><Rel> Q"
  and     cStatEq: "\<And>\<Psi>' R S \<Psi>''. \<lbrakk>(\<Psi>', R, S) \<in> Rel; \<Psi>' \<simeq> \<Psi>''\<rbrakk> \<Longrightarrow> (\<Psi>'', R, S) \<in> Rel"

  shows "\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
from \<open>\<Psi> \<rhd> P \<lessapprox><Rel> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<lessapprox><Rel> Q
[PROOF STEP]
obtain Q' Q'' where QChain: "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
                  and PImpQ': "insertAssertion(extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame Q') \<Psi>"
                  and Q'Chain: "\<Psi> \<otimes> \<one> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''" and "(\<Psi> \<otimes> \<one>, P, Q'') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<lessapprox><Rel> Q

goal (1 subgoal):
 1. (\<And>Q' Q''. \<lbrakk>\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'; insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>; \<Psi> \<otimes> \<one> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''; (\<Psi> \<otimes> \<one>, P, Q'') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakStatImpE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>
\<Psi> \<otimes> \<one> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
(\<Psi> \<otimes> \<one>, P, Q'') \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
from Q'Chain Identity
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<one> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
?\<Psi> \<otimes> \<one> \<simeq> ?\<Psi>
[PROOF STEP]
have Q'Chain: "\<Psi> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<one> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
?\<Psi> \<otimes> \<one> \<simeq> ?\<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
[PROOF STEP]
by(rule tauChainStatEq)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
with QChain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
\<Psi> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
[PROOF STEP]
have "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
\<Psi> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''

goal (1 subgoal):
 1. \<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
from Q'Chain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
[PROOF STEP]
have "insertAssertion(extractFrame Q') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame Q'') \<Psi>"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''

goal (1 subgoal):
 1. insertAssertion (extractFrame Q') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>
[PROOF STEP]
by(rule statImpTauChainDerivative)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame Q') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
with PImpQ'
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>
insertAssertion (extractFrame Q') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>
[PROOF STEP]
have "insertAssertion(extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion(extractFrame Q'') \<Psi>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q') \<Psi>
insertAssertion (extractFrame Q') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>

goal (1 subgoal):
 1. insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>
[PROOF STEP]
by(rule FrameStatImpTrans)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
from \<open>(\<Psi> \<otimes> \<one>, P, Q'') \<in> Rel\<close> Identity
[PROOF STATE]
proof (chain)
picking this:
(\<Psi> \<otimes> \<one>, P, Q'') \<in> Rel
?\<Psi> \<otimes> \<one> \<simeq> ?\<Psi>
[PROOF STEP]
have "(\<Psi>, P, Q'') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi> \<otimes> \<one>, P, Q'') \<in> Rel
?\<Psi> \<otimes> \<one> \<simeq> ?\<Psi>

goal (1 subgoal):
 1. (\<Psi>, P, Q'') \<in> Rel
[PROOF STEP]
by(rule cStatEq)
[PROOF STATE]
proof (state)
this:
(\<Psi>, P, Q'') \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>
(\<Psi>, P, Q'') \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
insertAssertion (extractFrame P) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>
(\<Psi>, P, Q'') \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q
[PROOF STEP]
by(rule weakenStatImpI)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<lessapprox>\<^sub>w<Rel> Q

goal:
No subgoals!
[PROOF STEP]
qed