theory TMLCorrect imports TML TMS2 begin definition write_count :: "nat \ nat" where "write_count n \ n div 2" definition step_correspondence :: "TML.State \ T \ TML.PC \ TMS2.InternalAction option" where "step_correspondence cs t a \ case a of Read1 \ if loc cs t = glb cs then Some (DoRead (addr cs t) (write_count (loc cs t))) else None | Write5 \ Some (DoWrite (addr cs t) (val cs t)) | Commit1 \ if even (loc cs t) then Some (DoCommitReadOnly (write_count (loc cs t))) else None | Commit2 \ Some DoCommitWriter | _ \ None " definition writes :: "TML.State \ TMS2.State \ L \ V option" where "writes cs0 as0 \ case (writer cs0) of Some w \ write_set as0 w | None \ Map.empty" definition global_rel :: "TML.State \ TMS2.State \ bool" where "global_rel cs0 as0 \ store cs0 = apply_partial (latest_store as0) (writes cs0 as0) \ write_count (glb cs0) = max_index as0" definition validity_prop :: "TML.State \ TMS2.State \ T \ bool" where "validity_prop cs as t \ begin_index as t \ write_count (loc cs t) \ (read_consistent (store_at as (write_count (loc cs t))) (read_set as t))" definition in_flight :: "TML.State \ TMS2.State \ T \ bool" where "in_flight cs as t \ (even (loc cs t) \ write_set as t = Map.empty) \ validity_prop cs as t" definition txn_rel :: "TML.PC Event \ TML.State \ TMS2.State \ T \ bool" where "txn_rel e cs0 as0 t \ tml_pre cs0 t e \ (case e of External BeginInv \ status as0 t = NotStarted | Internal Begin1 \ status as0 t = BeginResponding | Internal Begin2 \ status as0 t = BeginResponding \ (begin_index as0 t \ write_count (loc cs0 t)) | External BeginResp \ status as0 t = BeginResponding \ (begin_index as0 t \ write_count (loc cs0 t)) | Internal Read1 \ status as0 t = Pending (ReadPending (addr cs0 t)) \ in_flight cs0 as0 t | Internal Read2 \ ((status as0 t = ReadResponding (val cs0 t)) \ (status as0 t = Pending(ReadPending (addr cs0 t)) \ loc cs0 t \ glb cs0)) \ in_flight cs0 as0 t | External (ReadResp v) \ status as0 t = ReadResponding (val cs0 t) \ in_flight cs0 as0 t | Internal Write1 \ status as0 t = Pending (WritePending (addr cs0 t) (val cs0 t)) \ in_flight cs0 as0 t | Internal Write2 \ status as0 t = Pending (WritePending (addr cs0 t) (val cs0 t)) \ write_set as0 t = Map.empty \ validity_prop cs0 as0 t | Internal Write4 \ status as0 t = Pending (WritePending (addr cs0 t) (val cs0 t)) \ validity_prop cs0 as0 t | Internal Write5 \ status as0 t = Pending (WritePending (addr cs0 t) (val cs0 t)) \ validity_prop cs0 as0 t | External WriteResp \ status as0 t = WriteResponding \ validity_prop cs0 as0 t | Internal Commit1 \ status as0 t = Pending CommitPending \ in_flight cs0 as0 t | Internal Commit2 \ status as0 t = Pending CommitPending \ in_flight cs0 as0 t | External CommitResp \ status as0 t = CommitResponding | External Abort \ status as0 t \ {NotStarted, Ready, CommitResponding, Committed, Aborted} | External Cancel \ False | _ \ ( status as0 t = Ready \ in_flight cs0 as0 t)) " lemmas unfold_txn_rel = txn_rel_def in_flight_def lemmas unfold_coupled_auts = TML.unfold_tml TMS2.unfold_tms2 Utilities.all_utilities RWMemory.all_simps ext_enabled_def lemma validity_prop_stable_stutter: "\tml_pre cs at a; t \ at; write_count (loc cs t) : dom (stores as); validity_prop cs as t\ \ validity_prop (tml_eff cs at a) as t" by (cases rule: TML.Event_split[where b=a], auto simp add: validity_prop_def unfold_coupled_auts write_count_def split: splits option.split) (metis (full_types) option.simps(5))+ lemma validity_prop_stable_external: "\tml_pre cs at (External ac); ac \ BeginInv \ t \ at; validity_prop cs as t\ \ validity_prop (tml_eff cs at (External ac)) (tms_eff as at (External ac)) t" by (cases ac) (auto simp add: validity_prop_def unfold_coupled_auts write_count_def split: splits option.split) lemma write_count_in_domain: assumes "b \ {External BeginInv, Internal Begin1, External CommitResp, External Abort}" and "tml_pre cs t b" and "txn_rel b cs as t" and "global_rel cs as" and "TML.txn_inv b cs t" shows "write_count (State.loc cs t) \ max_index as" using assms by (cases rule: TML.Event_split[where b=b]) (fastforce simp add: unfold_txn_rel global_rel_def TML.txn_inv_def write_count_def unfold_coupled_auts div_le_mono)+ lemma index_is_valid: assumes "global_rel cs as" and "TML.txn_inv (Internal pc) cs t" and " pc = Commit2 \ (pc = Commit1 \ even (loc cs t)) \ (pc = Read1 \ loc cs t = glb cs)" and "tml_pre cs t (Internal pc)" and "validity_prop cs as t" shows "valid_index as t (write_count (loc cs t))" proof - show ?thesis using assms by(auto simp add: tml_pre_def TML.txn_inv_def global_rel_def valid_index_def write_count_def validity_prop_def) qed lemma precondition_external: assumes "TML.txn_inv (External ac) cs0 at" and "txn_rel (External ac) cs0 as0 at" and "tml_pre cs0 at (External ac)" shows "tms_pre as0 at (External ac)" using assms by (cases ac) (simp_all add: TML.txn_inv_def unfold_txn_rel unfold_coupled_auts) lemma precondition_internal_step: assumes "TML.txn_inv (Internal pc) cs0 at" and "global_rel cs0 as0" and "txn_rel (Internal pc) cs0 as0 at" and "tml_pre cs0 at (Internal pc)" and "step_correspondence cs0 at pc = Some ai" shows "tms_pre as0 at (Internal ai)" proof - {assume st: "pc = Read1 \ loc cs0 at = glb cs0 \ ai = DoRead (addr cs0 at) (write_count (loc cs0 at))" have vi: "valid_index as0 at (write_count (loc cs0 at))" using st assms index_is_valid[where t=at and cs="cs0" and as="as0"] by(simp add: tml_pre_def unfold_txn_rel) from st vi have ?thesis using assms by(simp add: unfold_txn_rel TMS2.unfold_pre)} moreover {assume st: "pc = Write5 \ ai = DoWrite (addr cs0 at) (val cs0 at)" from st have ?thesis using assms by (simp add: unfold_txn_rel TMS2.unfold_pre)} moreover {assume st: "pc = Commit1 \ even (loc cs0 at) \ ai = DoCommitReadOnly (write_count (loc cs0 at))" have vi: "valid_index as0 at (write_count (loc cs0 at))" using st assms index_is_valid[where t=at and cs="cs0" and as="as0"] by(simp add: tml_pre_def unfold_txn_rel) from st vi have ?thesis using assms by(simp add: unfold_txn_rel TMS2.unfold_pre)} moreover {assume st: "pc = Commit2 \ ai = DoCommitWriter" have vi: "valid_index as0 at (write_count (loc cs0 at))" using st assms index_is_valid[where t=at and cs="cs0" and as="as0"] by(simp add: tml_pre_def unfold_txn_rel) from st vi have ?thesis using assms by(simp add: unfold_coupled_auts unfold_txn_rel global_rel_def TML.txn_inv_def option.case_eq_if)} ultimately show ?thesis using assms by (cases rule: TML.Event_split[where b="Internal pc"]) (simp_all add: step_correspondence_def split: if_splits) qed lemma global_rel_preserved_external: assumes "global_rel cs0 as0" and "txn_rel (External ac) cs0 as0 at" and "tml_pre cs0 at (External ac)" and "tms_pre as0 at (External ac)" shows "global_rel (tml_eff cs0 at (External ac)) (tms_eff as0 at (External ac))" using assms by (cases ac) (simp_all add: writes_def global_rel_def unfold_coupled_auts split: option.split) lemma txn_rel_preserved_external_self: assumes "TML.txn_inv (External ac) cs0 at" and "TMS2.txn_inv (External ac) as0 at" and "global_rel cs0 as0" and "txn_rel (External ac) cs0 as0 at" and "tml_pre cs0 at (External ac)" shows "txn_rel b (tml_eff cs0 at (External ac)) (tms_eff as0 at (External ac)) at" proof - { assume "ac=BeginResp" from this have ?thesis using assms by (cases rule: TML.Event_split[where b="b"]) (simp_all add: unfold_txn_rel unfold_coupled_auts TMS2.txn_inv_def TML.txn_inv_def validity_prop_def) } moreover { assume "ac=WriteResp" from this have ?thesis using assms validity_prop_stable_external[where at=at and t=at and ac="ac" and cs=cs0 and as=as0] by (cases rule: TML.Event_split[where b="b"]) (auto simp add: unfold_txn_rel unfold_coupled_auts TML.txn_inv_def TMS2.txn_inv_def) } moreover { assume ac: "ac\BeginResp \ ac\WriteResp" from this ac have ?thesis using assms validity_prop_stable_external[where at=at and t=at and ac="ac" and cs=cs0 and as=as0] by(cases ac, cases rule: TML.Event_split[where b="b"]) (simp_all add: unfold_txn_rel global_rel_def unfold_coupled_auts split: TMS2.splits) } ultimately show ?thesis by auto qed lemma txn_rel_preserved_external_other: assumes "t \ at" and "TML.txn_inv b cs0 t" and "txn_rel b cs0 as0 t" and "tml_pre cs0 at (External ac)" shows "txn_rel b (tml_eff cs0 at (External ac)) (tms_eff as0 at (External ac)) t" using assms validity_prop_stable_external[where at=at and t=t and ac="ac" and cs=cs0 and as=as0] by (cases ac) (cases rule: TML.Event_split[where b="b"], simp_all add: unfold_txn_rel unfold_coupled_auts)+ lemma global_rel_preserved_internal_stutter: assumes "TML.global_inv cs0" and "TML.txn_inv a cs0 at" and "global_rel cs0 as0" and "txn_rel a cs0 as0 at" and a: "a = Internal pc" and "tml_pre cs0 at a" and sc: "step_correspondence cs0 at pc = None" shows "global_rel (tml_eff cs0 at a) as0" proof - {assume "pc = Begin1" from this have ?thesis using assms by(simp_all add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def)} moreover {assume "pc = Begin2" from this have ?thesis using assms by(simp_all add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def)} moreover {assume "pc = Read1 \ loc cs0 at \ glb cs0" from this have ?thesis using assms by(simp_all add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def)} moreover {assume "pc = Read2" from this have ?thesis using assms by(simp_all add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def)} moreover {assume "pc = Write1" from this have ?thesis using assms by(simp_all add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def)} moreover {assume "pc = Write2" from this have ?thesis using assms by(simp add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def write_count_def TML.txn_inv_def TML.global_inv_def, force)} moreover {assume "pc = Write4" from this have ?thesis using assms by(simp_all add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def)} moreover {assume "pc = Commit1 \ odd (loc cs0 at)" from this have ?thesis using assms by(simp_all add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def)} ultimately show ?thesis using assms by (cases rule: TML.Event_split[where b="Internal pc"]) (simp_all add: step_correspondence_def split: if_splits) qed lemma global_rel_preserved_internal_step: assumes "TML.global_inv cs0" and "TML.txn_inv (Internal pc) cs0 at" and "stores_domain as0" and "global_rel cs0 as0" and "txn_rel (Internal pc) cs0 as0 at" and "tml_pre cs0 at (Internal pc)" and "tms_pre as0 at (Internal ai)" and "step_correspondence cs0 at pc = Some ai" shows "global_rel (tml_eff cs0 at (Internal pc)) (tms_eff as0 at (Internal ai))" proof - {assume "pc = Read1 \ loc cs0 at = glb cs0 \ ai = DoRead (addr cs0 at) (write_count (loc cs0 at))" from this have ?thesis using assms by(auto simp add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def TML.global_inv_def)} moreover {assume "pc = Write5 \ ai = DoWrite (addr cs0 at) (val cs0 at)" from this have ?thesis using assms by (simp add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def TML.txn_inv_def apply_partial_simp)} moreover {assume pc: "pc = Commit1 \ even (loc cs0 at) \ ai = DoCommitReadOnly (write_count (loc cs0 at))" from this have ?thesis using pc assms by(auto simp add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def TML.global_inv_def)} moreover {assume "pc = Commit2 \ ai = DoCommitWriter" from this have ?thesis using assms by(auto simp add: global_rel_def unfold_txn_rel unfold_coupled_auts writes_def write_count_def TML.txn_inv_def TML.global_inv_def TMS2.stores_update_do_commit_writer stores_domain_def)} ultimately show ?thesis using assms by (cases rule: TML.Event_split[where b="Internal pc"]) (simp_all add: step_correspondence_def split: if_splits) qed lemma txn_rel_self_preserved_internal_step: assumes "TML.global_inv cs0" and "TML.txn_inv (Internal pc) cs0 at" and "global_rel cs0 as0" and "txn_rel (Internal pc) cs0 as0 at" and "tml_pre cs0 at (Internal pc)" and "step_correspondence cs0 at pc = Some ai" shows "txn_rel b (tml_eff cs0 at (Internal pc)) (tms_eff as0 at (Internal ai)) at" proof - {assume st: "pc = Read1 \ loc cs0 at = glb cs0 \ ai = DoRead (addr cs0 at) (write_count (loc cs0 at)) \ (addr cs0 at) : dom (write_set as0 at)" from st have ?thesis using assms by (auto simp add: unfold_txn_rel unfold_coupled_auts validity_prop_def TML.txn_inv_def writes_def global_rel_def split: TMS2.splits option.split)} moreover {assume st: "pc = Read1 \ loc cs0 at = glb cs0 \ ai = DoRead (addr cs0 at) (write_count (loc cs0 at)) \ (addr cs0 at) \ dom (write_set as0 at)" from st have ?thesis using assms by (auto simp add: TML.global_inv_def unfold_txn_rel unfold_coupled_auts validity_prop_def TML.txn_inv_def writes_def global_rel_def split: TMS2.splits option.split)} moreover {assume st: "pc = Write5 \ ai = DoWrite (addr cs0 at) (val cs0 at)" from st have ?thesis using assms by (auto simp add: unfold_txn_rel TML.txn_inv_def unfold_coupled_auts validity_prop_def split: TMS2.splits option.split)} moreover {assume st: "pc = Commit1 \ even (loc cs0 at) \ ai = DoCommitReadOnly (write_count (loc cs0 at))" from st have ?thesis using assms by (auto simp add: unfold_txn_rel unfold_coupled_auts validity_prop_def split: TMS2.splits option.split)} moreover {assume st: "pc = Commit2 \ ai = DoCommitWriter" from st have ?thesis using assms by (auto simp add: unfold_txn_rel unfold_coupled_auts validity_prop_def split: TMS2.splits option.split)} ultimately show ?thesis using assms by (cases rule: TML.Event_split[where b="Internal pc"]) (auto simp add: step_correspondence_def unfold_coupled_auts) qed lemma txn_rel_other_preserved_internal_step: assumes "TML.global_inv cs0" and "TML.txn_inv (Internal pc) cs0 at" and "global_rel cs0 as0" and "txn_rel (Internal pc) cs0 as0 at" and "tml_pre cs0 at (Internal pc)" and "t \ at" and "TML.txn_inv b cs0 t" and "txn_rel b cs0 as0 t" and "step_correspondence cs0 at pc = Some ai" shows "txn_rel b (tml_eff cs0 at (Internal pc)) (tms_eff as0 at (Internal ai)) t" proof - {assume st: "pc = Read1 \ loc cs0 at = glb cs0 \ ai = DoRead (addr cs0 at) (write_count (loc cs0 at)) \ (addr cs0 at) : dom (write_set as0 at)" from st have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (auto simp add: unfold_txn_rel unfold_coupled_auts validity_prop_def)} moreover {assume st: "pc = Read1 \ loc cs0 at = glb cs0 \ ai = DoRead (addr cs0 at) (write_count (loc cs0 at)) \ (addr cs0 at) \ dom (write_set as0 at)" from st have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (auto simp add: unfold_txn_rel unfold_coupled_auts validity_prop_def)} moreover {assume st: "pc = Write5 \ ai = DoWrite (addr cs0 at) (val cs0 at)" from st have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (auto simp add: unfold_txn_rel unfold_coupled_auts validity_prop_def)} moreover {assume st: "pc = Commit1 \ even (loc cs0 at) \ ai = DoCommitReadOnly (write_count (loc cs0 at))" from st have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (auto simp add: unfold_txn_rel unfold_coupled_auts validity_prop_def)} moreover {assume st: "pc = Commit2 \ ai = DoCommitWriter" have ai: "b \ {External BeginInv, Internal Begin1, External CommitResp, External Abort} \ tml_pre cs0 t b \ write_count (State.loc cs0 t) \ max_index as0" using assms st using write_count_in_domain by (auto) (* TODO could be cleaned up *) from st ai have ?thesis using assms read_consistent_stable[where s="as0" and at=at and a="Internal ai" and n="write_count (loc cs0 t)" and t=t] by (cases rule: TML.Event_split[where b = b], simp_all) (auto simp add: TML.txn_inv_def unfold_txn_rel unfold_coupled_auts validity_prop_def write_count_def)} ultimately show ?thesis using assms by (cases rule: TML.Event_split[where b="Internal pc"]) (auto simp add: step_correspondence_def unfold_coupled_auts split: if_splits) qed lemma txn_rel_self_preserved_stutter: assumes "TML.global_inv cs0" and "TML.txn_inv (Internal pc) cs0 at" and "\ c. TMS2.txn_inv c as0 at" and "global_rel cs0 as0" and "txn_rel (Internal pc) cs0 as0 at" and "tml_pre cs0 at (Internal pc)" and "step_correspondence cs0 at pc = None" shows "txn_rel b (tml_eff cs0 at (Internal pc)) as0 at" proof - {assume pc: "pc = Begin1" from pc assms spec[where P="\ c. TMS2.txn_inv c as0 at" and x="External BeginResp"] (*TODO eek*) have mi: "begin_index as0 at \ max_index as0" by(simp add: unfold_txn_rel unfold_coupled_auts TMS2.txn_inv_def) from this pc have ?thesis using assms by(simp_all add: global_rel_def unfold_txn_rel unfold_coupled_auts split: TMS2.splits )} moreover {assume "pc = Begin2" from this have ?thesis using assms by(auto simp add: global_rel_def unfold_txn_rel TMS2.txn_inv_def unfold_coupled_auts split: TML.PC.split Status.split TMS2.splits option.split)} moreover {assume "pc = Read1 \ loc cs0 at \ glb cs0" from this have ?thesis using assms by (simp_all add: unfold_txn_rel unfold_coupled_auts validity_prop_def split: TMS2.splits )} moreover {assume "pc = Read2" from this have ?thesis using assms by(auto simp add: TML.global_inv_def unfold_txn_rel unfold_coupled_auts validity_prop_def split: TMS2.splits option.split)} moreover {assume "pc = Write1" from this have ?thesis using assms by(simp_all add: unfold_txn_rel unfold_coupled_auts validity_prop_def split: TMS2.splits)} moreover {assume "pc = Write2" from this have ?thesis using assms by(simp_all add: unfold_txn_rel TML.txn_inv_def unfold_coupled_auts validity_prop_def split: TMS2.splits)} moreover {assume "pc = Write4" from this have ?thesis using assms by(auto simp add: option.case_eq_if unfold_txn_rel TML.global_inv_def TML.txn_inv_def unfold_coupled_auts validity_prop_def write_count_def split: TMS2.splits) (metis domI domIff option.sel)+ } moreover {assume "pc = Commit1 \ odd (loc cs0 at)" from this have ?thesis using assms by(simp_all add: unfold_txn_rel unfold_coupled_auts validity_prop_def split: TMS2.splits)} ultimately show ?thesis using assms by (cases rule: TML.Event_split[where b="Internal pc"]) (simp_all add: step_correspondence_def split: if_splits) qed lemma txn_rel_other_preserved_stutter: assumes "TML.global_inv cs0" and "TML.txn_inv (Internal pc) cs0 at" and "stores_domain as0" and "global_rel cs0 as0" and "txn_rel (Internal pc) cs0 as0 at" and "tml_pre cs0 at (Internal pc)" and "t \ at" and "txn_rel b cs0 as0 t" and "TML.txn_inv b cs0 t" and "step_correspondence cs0 at pc = None" shows "txn_rel b (tml_eff cs0 at (Internal pc)) as0 t" proof - {assume "pc = Begin1" from this have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (simp_all add: global_rel_def unfold_txn_rel unfold_coupled_auts validity_prop_def)} moreover {assume st : "pc = Begin2" have ai : "b \ {External BeginInv, Internal Begin1, External CommitResp, External Abort} \ tml_pre cs0 t b \ write_count (loc cs0 t) : dom (stores as0)" using write_count_in_domain assms by (auto simp add: stores_domain_def domD) from validity_prop_stable_stutter assms ai have vp : "b \ {External BeginInv, Internal Begin1, External CommitResp, External Abort} \ tml_pre cs0 t b \ validity_prop cs0 as0 t \ validity_prop (tml_eff cs0 at (Internal pc)) as0 t" by (auto) from st vp have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (auto simp add: unfold_txn_rel unfold_coupled_auts) } moreover {assume "pc = Read1 \ loc cs0 at \ glb cs0" from this have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (simp_all add: option.case_eq_if global_rel_def unfold_txn_rel TML.txn_inv_def unfold_coupled_auts validity_prop_def)} moreover {assume "pc = Read2" from this have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (simp_all add: option.case_eq_if global_rel_def unfold_txn_rel TML.txn_inv_def unfold_coupled_auts validity_prop_def)} moreover {assume "pc = Write1" from this have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (simp_all add: option.case_eq_if global_rel_def unfold_txn_rel TML.txn_inv_def unfold_coupled_auts validity_prop_def)} moreover {assume st: "pc = Write2" have ai : "b \ {External BeginInv, Internal Begin1, External CommitResp, External Abort} \ tml_pre cs0 t b \ write_count (loc cs0 t) : dom (stores as0)" using write_count_in_domain assms by (auto simp add: stores_domain_def domD) from validity_prop_stable_stutter assms ai have vp : "b \ {External BeginInv, Internal Begin1, External CommitResp, External Abort} \ tml_pre cs0 t b \ validity_prop cs0 as0 t \ validity_prop (tml_eff cs0 at (Internal pc)) as0 t" by (simp) from st vp have ?thesis using assms by(cases rule: TML.Event_split[where b = b], simp_all add: unfold_txn_rel unfold_coupled_auts write_count_def ) (auto simp add: TML.txn_inv_def TML.global_inv_def unfold_txn_rel unfold_coupled_auts write_count_def split: if_splits)} moreover {assume "pc = Write4" from this have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (simp_all add: option.case_eq_if global_rel_def unfold_txn_rel TML.txn_inv_def unfold_coupled_auts validity_prop_def)} moreover {assume "pc = Commit1 \ odd (loc cs0 at)" from this have ?thesis using assms by (cases rule: TML.Event_split[where b = b]) (simp_all add: option.case_eq_if global_rel_def unfold_txn_rel TML.txn_inv_def unfold_coupled_auts validity_prop_def)} ultimately show ?thesis using assms by (cases rule: TML.Event_split[where b="Internal pc"]) (simp_all add: step_correspondence_def split: if_splits) qed definition sim_rel :: "TML.State \ TMS2.State \ bool" where "sim_rel cs as \ global_rel cs as \ (\ a t. txn_rel a cs as t)" lemma sim_rel_start: "TML.start cs \ \ as. TMS2.start as \ sim_rel cs as" apply(rule exI[where x= TMS2.default_start], insert default_is_start, simp) apply(auto simp add: sim_rel_def global_rel_def write_count_def writes_def unfold_txn_rel unfold_coupled_auts default_start_def mem_initial_def domD split: option.split Event.split Action.split InternalAction.split PC.split) apply(simp add: dom_def) done lemma sim_rel_external: "standard_sim_ext_step TML TMS2 sim_rel" apply(unfold standard_sim_ext_step_def sim_rel_def) apply(insert invariant_elim[OF TML.total_inv], simp) apply(insert invariant_elim[OF TMS2.total_inv], simp) apply(insert precondition_external global_rel_preserved_external txn_rel_preserved_external_other txn_rel_preserved_external_self) by metis lemma sim_rel_stutter: "standard_sim_stutter TML TMS2 step_correspondence sim_rel" apply(unfold standard_sim_stutter_def sim_rel_def) apply(insert invariant_elim[OF TML.total_inv], simp) apply(insert invariant_elim[OF TMS2.total_inv], simp) apply(insert global_rel_preserved_internal_stutter txn_rel_self_preserved_stutter txn_rel_other_preserved_stutter) by metis lemma sim_rel_internal_step: "standard_sim_int_step TML TMS2 step_correspondence sim_rel" apply(unfold standard_sim_int_step_def sim_rel_def) apply(insert invariant_elim[OF TML.total_inv], simp) apply(insert invariant_elim[OF TMS2.total_inv], simp) apply(insert precondition_internal_step global_rel_preserved_internal_step txn_rel_self_preserved_internal_step txn_rel_other_preserved_internal_step) by metis lemma TML_simulation: "standard_simulation TML TMS2 step_correspondence sim_rel" by(insert sim_rel_start sim_rel_external sim_rel_stutter sim_rel_internal_step, auto simp add: standard_simulation_def) lemma TML_correct: "traces (ioa TML) \ traces (ioa TMS2)" using standard_simulation_trace_inclusion TML_simulation by metis end