# Theory CompositionCorrectness

Up to index of Isabelle/HOL/HOLCF/Abortable_Linearizable_Modules

theory CompositionCorrectness
imports ALM
`(*Author: Giuliano Losa *)header {* Proof that the composition of two instances of the ALM automaton behaves like a single instance of the ALM automaton*}theory CompositionCorrectnessimports ALMbegindeclare  split_if_asm [split]declare  Let_def [simp]subsection {*A case split useful in the proofs*}definition  in_trans_cases_fun :: "nat => nat => (ALM_state * ALM_state) => (ALM_state * ALM_state) => bool"   -- {*Helper function used to decompose proofs*}  where "in_trans_cases_fun == % id1 id2 s t .   (EX ca ra. (fst s, Invoke ca ra, fst t) : ALM_trans 0 id1 & (snd s, Invoke ca ra, snd t) : ALM_trans id1 id2)  | (EX ca h ra. (fst s, Switch ca id1 h ra, fst t) : ALM_trans 0 id1 & (snd s, Switch ca id1 h ra, snd t) : ALM_trans id1 id2)  | (EX c id' h. fst t = fst s & (snd s, Commit c id' h, snd t) : ALM_trans id1 id2 & id1 <= id' & id' < id2)  | (EX c h r. fst t = fst s & (snd s, Switch c id2 h r, snd t) : ALM_trans id1 id2)  | (EX h . fst t = fst s & (snd s, Linearize id1 h, snd t) : ALM_trans id1 id2)  | (fst t = fst s & (snd s, Abort id1, snd t) : ALM_trans id1 id2)  | (EX h. fst t = fst s & (snd s, Initialize id1 h, snd t) : ALM_trans id1 id2)  | (EX ca ta ra. (fst s, Switch ca 0 ta ra, fst t) : ALM_trans 0 id1 & snd t = snd s)  | (EX ca id' h. (fst s, Commit ca id' h, fst t) : ALM_trans 0 id1 & snd t = snd s & id' < id1)  | (EX h . (fst s, Linearize 0 h, fst t) : ALM_trans 0 id1 & snd t = snd s)  | (EX h. (fst s, Initialize 0 h, fst t) : ALM_trans 0 id1 & snd t = snd s)  | ((fst s, Abort 0, fst t) : ALM_trans 0 id1 & snd t = snd s)"lemma  composeALMsE:  -- {*A rule for decomposing proofs*}  assumes "id1 ~= 0" and "id1 < id2" and in_trans_comp:"s -(a::ALM_action)--composeALMs id1 id2-> t"  shows decomp: "in_trans_cases_fun id1 id2 s t"proof -  from in_trans_comp and `id1 ~= 0` and `id1 < id2`  have "a : {act . EX c r h id' . 0 <= id' & id' < id2 & (      act = Invoke c r       | act : {Switch c 0 h r, Switch c id1 h r, Switch c id2 h r}      | act : {Linearize 0 h, Linearize id1 h}      | act : {Initialize 0 h, Initialize id1 h}      | act : {Abort 0, Abort id1}      | act : {Commit c id' h}     )}" by (auto simp add: composeALMs_def trans_of_def hide_def ALM_ioa_def par_def actions_def asig_inputs_def asig_outputs_def asig_internals_def asig_of_def ALM_asig_def)  with this obtain c r h id' where "0 <= id' & id' < id2 & a : { act .       act = Invoke c r       | act : {Switch c 0 h r, Switch c id1 h r, Switch c id2 h r}      | act : {Linearize 0 h, Linearize id1 h}      | act : {Initialize 0 h, Initialize id1 h}      | act : {Abort 0, Abort id1}      | act : {Commit c id' h}     }" by auto  moreover from in_trans_comp and `id1 ~= 0` and `id1 < id2`   have    "(a = Linearize 0 h | a = Abort 0 | a = Initialize 0 h | a = Switch c 0 h r | (a = Commit c id' h & id' < id1)) ==> ((fst s, a, fst t) : ALM_trans 0 id1 & snd s = snd t)"    and    "(a = Linearize id1 h | a = Abort id1 | a = Initialize id1 h | a = Switch c id2 h r | (a = Commit c id' h & id1 <= id' & id' < id2)) ==> (fst s = fst t & (snd s, a, snd t) : ALM_trans id1 id2)"    and     "(a = Switch c id1 h r | a = Invoke c r) ==> ((fst s, a, fst t) : ALM_trans 0 id1 & (snd s, a, snd t) : ALM_trans id1 id2)"     by (auto simp add: composeALMs_def trans_of_def hide_def ALM_ioa_def par_def actions_def asig_inputs_def asig_outputs_def asig_internals_def asig_of_def ALM_asig_def)  ultimately show ?thesis unfolding in_trans_cases_fun_def apply simp by(metis linorder_not_less)qedlemma  my_rule:"[|id1 ≠ 0; id1 < id2; s -a--composeALMs id1 id2-> t; [|in_trans_cases_fun id1 id2 s t|] ==> P|]  ==> P"  by (auto intro: composeALMsE[where s="s" and t="t" and a="a"])lemma  my_rule2:"[|0 < id1; id1 < id2; s -a--composeALMs id1 id2-> t; [|in_trans_cases_fun id1 id2 s t|] ==> P|]  ==> P"  by (auto intro: composeALMsE[where s="s" and t="t" and a="a"])subsection {*Invariants of a single ALM instance*}definition P1a :: "(ALM_state * ALM_state) => bool"   where  -- {*In ALM 1, a pending request of client c has client c as sender*}  "P1a == % s . let s1 = fst s; s2 = snd s in               ALL c . phase s1 c ∈ {Pending, Aborted} --> request_snd (pending s1 c) = c"definition P1b :: "(ALM_state * ALM_state) => bool"  where  -- {*In ALM 2, a pending request of client c has client c as sender*}  "P1b == % s . let s1 = fst s; s2 = snd s in               ALL c . phase s2 c ≠ Sleep --> request_snd (pending s2 c) = c"definition P2 :: "(ALM_state * ALM_state) => bool" where  "P2 == % s . let s1 = fst s; s2 = snd s in       (∀ c . phase s2 c = Sleep) --> (¬ initialized s2 ∧ hist s2 = [])"definition P3 :: "(ALM_state * ALM_state) => bool" where  "P3 == % s . let s1 = fst s; s2 = snd s in        ∀ c . (phase s2 c = Ready --> initialized s2)"definition P4 :: "(ALM_state * ALM_state) => bool"   where  -- {*The set of init histories of ALM 2 is empty when no client ever invoked anything*}  "P4 == % s . let s1 = fst s; s2 = snd s in      (∀ c . phase s2 c = Sleep) = (initHists s2 = {})"definition P5 :: "(ALM_state * ALM_state) => bool"   -- {*In ALM 1 a client never sleeps*}  where  "P5 == % s . let s1 = fst s; s2 = snd s in       ∀ c . phase s1 c ≠ Sleep"subsection {*Invariants of the composition of two ALM instances*}definition P6 :: "(ALM_state * ALM_state) => bool"   -- {*Non-interference accross instances*}  where  "P6 == % s . let s1 = fst s; s2 = snd s in                 (~ aborted s1 --> (ALL c . phase s2 c = Sleep)) & (ALL c . phase s1 c ~= Aborted = (phase s2 c = Sleep))"definition P7 :: "(ALM_state * ALM_state) => bool"   -- {*Before initialization of the ALM 2, pending requests are the same as in ALM 1 and no new requests may be accepted (phase is not Ready)*}  where  "P7 == % s . let s1 = fst s; s2 = snd s in               ALL c . phase s1 c = Aborted ∧ ¬ initialized s2 --> (pending s2 c = pending s1 c ∧ phase s2 c ∈ {Pending, Aborted})"definition P8 :: "(ALM_state * ALM_state) => bool"   -- {*Init histories of ALM 2 are built from the history of ALM 1 plus pending requests of ALM 1*}  where  "P8 == % s . let s1 = fst s; s2 = snd s in               ∀ h ∈ initHists s2 . h ∈ postfix_all (hist s1) (linearizations (pendingReqs s1))"definition P9 :: "(ALM_state * ALM_state) => bool"   -- {*ALM 2 does not abort before ALM 1 aborts*}  where  "P9 == % s . let s1 = fst s; s2 = snd s in              aborted s2 --> aborted s1"definition P10 :: "(ALM_state * ALM_state) => bool"   -- {*ALM 1 is always initialized and when ALM 2 is not initialized its history is empty*}  where  "P10 == % s . let s1 = fst s; s2 = snd s in              initialized s1 ∧ (¬ initialized s2 --> (hist s2 = []))"definition P11 :: "(ALM_state * ALM_state) => bool"   where  -- {*After ALM 2 has been invoked and before it is initialized, any request found in init histories after their longest common prefix is pending in ALM 1*}  "P11 == % s . let s1 = fst s; s2 = snd s in       ((∃ c . phase s2 c ≠ Sleep) ∧ ¬ initialized s2) --> initValidReqs s2 ⊆ pendingReqs s1"definition P12:: "(ALM_state * ALM_state) => bool"   where  -- {*After ALM 2 has been invoked and before it is initialized, the longest common prefix of the init histories of ALM 2 is buit from appending a set of request pending in ALM 1 to the history of ALM 1*}  "P12 == % s . let s1 = fst s; s2 = snd s in       (∃ c . phase s2 c ≠ Sleep) --> (∃ rs . l_c_p (initHists s2) = rs @ (hist s1) ∧ set rs ⊆ pendingReqs s1 ∧ distinct rs)"definition P13 :: "(ALM_state * ALM_state) => bool"   where  -- {*After ALM 2 has been invoked and before it is initialized, any history that may be chosen at initialization is a valid linearization of the concurrent history of ALM 1*}  "P13 == % s . let s1 = fst s; s2 = snd s in       ((∃ c . phase s2 c ≠ Sleep) ∧ ¬ initialized s2) --> postfix_all (l_c_p (initHists s2)) (linearizations (initValidReqs s2)) ⊆ postfix_all (hist s1) (linearizations (pendingReqs s1))"definition P14 :: "(ALM_state * ALM_state) => bool"   where  -- {*The history of ALM 1 is a postfix of the history of ALM 2 and requests appearing in ALM 2 after the history of ALM 1 are not in the history of ALM 1*}  "P14 == % s . let s1 = fst s; s2 = snd s in       (hist s2 ≠ [] ∨ initialized s2) --> (∃ rs .           hist s2 = rs @ (hist s1)           ∧ set rs ∩ set (hist s1) = {})"definition P15 :: "(ALM_state * ALM_state) => bool"   where  -- {*A client that hasn't yet invoked ALM 2 has no request commited in ALM 2 except for its pending request*}  "P15 == % s . let s1 = fst s; s2 = snd s in       ∀ r . let c = request_snd r in phase s2 c = Sleep ∧ r ∈ set (hist s2) --> (r ∈ set (hist s1) ∨ r ∈ pendingReqs s1)"subsection {*Proofs of invariance*}lemma invariant_imp: "[|invariant ioa P; ∀ s . P s --> Q s|] ==> invariant ioa Q"by (simp add:invariant_def)declare  phase.split [split]declare  phase.split_asm [split]declare  ALM_action.split [split]declare  ALM_action.split_asm [split]lemma dropWhile_lemma: "∀ ys . xs = ys @ zs ∧ hd zs = x ∧ zs ≠ [] ∧ x ∉ set ys --> dropWhile (λ x' . x' ≠ x) xs = zs"  -- {*A useful lemma about truncating histories*}proof  (induct xs, force)  fix a xs  assume "∀ ys . xs = ys @ zs ∧ hd zs = x ∧ zs ≠ [] ∧ x ∉ set ys --> dropWhile (λx'. x' ≠ x) xs = zs"  show "∀ ys . a # xs = ys @ zs ∧ hd zs = x ∧ zs ≠ [] ∧ x ∉ set ys --> dropWhile (λx'. x' ≠ x) (a # xs) = zs"  proof (rule allI, rule impI, cases "a = x")    fix ys    assume "a # xs = ys @ zs ∧ hd zs = x ∧ zs ≠ [] ∧ x ∉ set ys" and "a = x"    hence "x # xs = ys @ zs" and "x ∉ set ys" and "hd zs = x" and "zs ≠ []" by auto    from `x # xs = ys @ zs` and `x ∉ set ys` have "ys = []"   by (metis hd.simps hd_append hd_in_set)    with `a = x` and `x # xs = ys @ zs` show "dropWhile (λx'. x' ≠ x) (a # xs) = zs" by auto  next    fix ys    assume "a # xs = ys @ zs ∧ hd zs = x ∧ zs ≠ [] ∧ x ∉ set ys" and "a ≠ x"    hence "a # xs = ys @ zs" and "hd zs = x" and "zs ≠ []" and "x ∉ set ys" by auto    obtain ys' where "xs = ys' @ zs" and "x ∉ set ys'"    proof -      from `a # xs = ys @ zs` and `hd zs = x` and `a ≠ x` obtain ys' where "ys = a # ys'" apply clarify by (metis Cons_eq_append_conv hd.simps)      moreover with `x ∉ set ys` have "x ∉ set ys'" by auto      moreover from `ys = a # ys'` and `a # xs = ys @ zs` have "xs = ys' @ zs" by auto      ultimately show "(!!ys'. [|xs = ys' @ zs; x ∉ set ys'|] ==> thesis) ==> thesis" by auto    qed    with `∀ ys . xs = ys @ zs ∧ hd zs = x ∧ zs ≠ [] ∧ x ∉ set ys --> dropWhile (λx'. x' ≠ x) xs = zs` and `hd zs = x` and `zs ≠ []` have "dropWhile (λx'. x' ≠ x) xs = zs" by auto    with `a ≠ x` show "dropWhile (λx'. x' ≠ x) (a # xs) = zs" by auto  qedqedlemma P2_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P2"proof  (rule invariantI, auto)  fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P2 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P2_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P2 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  from `0 < id1` and `id1 < id2` and in_trans_comp show "P2 (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P2 (s1', s2')" using `P2 (s1, s2)` and `0 < id1` and `id1 < id2` apply(auto simp add: in_trans_cases_fun_def) apply (auto simp add: ALM_trans_def P2_def) done  qedqedlemma P5_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P5"proof  (rule invariantI, auto)  fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P5 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P5_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P5 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  from `0 < id1` and `id1 < id2` and in_trans_comp show "P5 (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P5 (s1', s2')" using `P5 (s1, s2)` and `0 < id1` and `id1 < id2` apply(auto simp add: in_trans_cases_fun_def) apply (auto simp add: ALM_trans_def P5_def) done  qedqedlemma  P6_invariant: "[|id1 ≠ 0 ; id1 < id2|] ==> invariant (composeALMs id1 id2) P6"proof  (rule invariantI, rule_tac [2] impI)   fix s  assume "s : starts_of (composeALMs id1 id2)" and "id1 ≠ 0"  thus "P6 s" by (simp add: starts_of_def composeALMs_def hide_def  ALM_ioa_def par_def ALM_start_def P6_def)next  fix s t a  assume "P6 s"  assume "id1 ≠ 0" and "id1 < id2" and "s -a--composeALMs id1 id2-> t"  thus "P6 t"   proof (rule my_rule)    assume "in_trans_cases_fun id1 id2 s t"    thus "P6 t" using `P6 s` and `id1 ≠ 0` and `id1 < id2`  apply(auto simp add: in_trans_cases_fun_def) apply (simp_all add: ALM_trans_def P6_def) apply (metis phase.simps(12) phase.simps(4) phase.simps(5)) apply (metis phase.simps(12) phase.simps(5)) apply (force simp add: ALM_trans_def P6_def) apply (force simp add: ALM_trans_def P6_def) apply (force simp add: ALM_trans_def P6_def)  apply (force simp add: ALM_trans_def P6_def) apply (force simp add: ALM_trans_def P6_def) apply (force simp add: ALM_trans_def P6_def) done  qedqedlemma  P9_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P9"proof  (rule invariantI, auto)   fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)"  thus "P9 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P9_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P9 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  have "P6 (s1, s2)"  proof -    from in_trans_comp and `reachable (composeALMs id1 id2) (s1, s2)` have "reachable (composeALMs id1 id2) (s1', s2')" by (auto intro: reachable.reachable_n)    with `reachable (composeALMs id1 id2) (s1, s2)` and `0 < id1` and `id1 < id2` and P6_invariant show "P6 (s1, s2)" unfolding invariant_def by auto  qed  from `0 < id1` and `id1 < id2` and in_trans_comp show "P9 (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P9 (s1', s2')" using `P9 (s1, s2)` and `P6 (s1, s2)` and `0 < id1` and `id1 < id2` apply(auto simp add: in_trans_cases_fun_def) apply (auto simp add: ALM_trans_def P9_def P6_def) done  qedqedlemma  P10_invariant: "[|id1 < id2; id1 ~= 0|] ==> invariant (composeALMs id1 id2) P10"proof  (rule invariantI, auto)   fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P10 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P10_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P10 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  from `0 < id1` and `id1 < id2` and in_trans_comp show "P10 (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P10 (s1', s2')" using `P10 (s1, s2)` and `0 < id1` and `id1 < id2` apply(auto simp add: in_trans_cases_fun_def) apply (auto simp add: ALM_trans_def P10_def) done  qedqedlemma P3_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P3"proof  (rule invariantI, auto)   fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P3 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P3_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P3 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  have "P10 (s1, s2)"  proof -    from in_trans_comp and `reachable (composeALMs id1 id2) (s1, s2)` have "reachable (composeALMs id1 id2) (s1', s2')" by (auto intro: reachable.reachable_n)    with `reachable (composeALMs id1 id2) (s1, s2)` and `0 < id1` and `id1 < id2` and P10_invariant show "P10 (s1, s2)" unfolding invariant_def by auto  qed  from `0 < id1` and `id1 < id2` and in_trans_comp show "P3 (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P3 (s1', s2')" using `P3 (s1, s2)` and `P10 (s1, s2)` and `0 < id1` and `id1 < id2` apply(auto simp add: in_trans_cases_fun_def) apply (auto simp add: ALM_trans_def P3_def P10_def) done  qedqedlemma  P7_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P7"proof  (rule invariantI, auto)   fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P7 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P7_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P7 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  have "P6 (s1, s2)" and "P10 (s1, s2)"  proof -    from in_trans_comp and `reachable (composeALMs id1 id2) (s1, s2)` have "reachable (composeALMs id1 id2) (s1', s2')" by (auto intro: reachable.reachable_n)    with `reachable (composeALMs id1 id2) (s1, s2)` and `0 < id1` and `id1 < id2` and P6_invariant and P10_invariant show "P6 (s1, s2)" and "P10 (s1, s2)" unfolding invariant_def by auto  qed  from `0 < id1` and `id1 < id2` and in_trans_comp show "P7 (s1', s2')"    proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P7 (s1', s2')" using `P7 (s1, s2)` and `P6 (s1, s2)` and `0 < id1` and `id1 < id2`    proof (auto simp add: in_trans_cases_fun_def)      fix ca ra      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Invoke ca ra, s1') ∈ ALM_trans 0 id1" and "(s2, Invoke ca ra, s2') ∈ ALM_trans id1 id2"      thus " P7 (s1', s2')"  by (auto simp add: ALM_trans_def P7_def)    next      fix ca h ra      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Switch ca id1 h ra, s1') ∈ ALM_trans 0 id1" and "(s2, Switch ca id1 h ra, s2') ∈ ALM_trans id1 id2"      thus " P7 (s1', s2')"  by (auto simp add: ALM_trans_def P7_def P6_def)    next      fix c id' h      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "(s2, Commit c id' h, s2') ∈ ALM_trans id1 id2" and "id1 ≤ id'" and "id' < id2"      thus " P7 (s1, s2')" using `P10 (s1, s2)` by (auto simp add: ALM_trans_def P7_def P10_def)    next      fix c h r      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Switch c id2 h r, s2') ∈ ALM_trans id1 id2"      thus " P7 (s1, s2')"  by (auto simp add: ALM_trans_def P7_def)    next      fix h      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Linearize id1 h, s2') ∈ ALM_trans id1 id2"      thus " P7 (s1, s2')" by (simp add: ALM_trans_def P7_def)     next      fix h      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Initialize id1 h, s2') ∈ ALM_trans id1 id2"      thus " P7 (s1, s2')"  by (auto simp add: ALM_trans_def P7_def)    next      fix ca ta ra      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Switch ca 0 ta ra, s1') ∈ ALM_trans 0 id1"      thus " P7 (s1', s2)"  by (auto simp add: ALM_trans_def P7_def)    next      fix ca id' h      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "id1 < id2" and "(s1, Commit ca id' h, s1') ∈ ALM_trans 0 id1" and "id' < id1"      thus " P7 (s1', s2)"  by (auto simp add: ALM_trans_def P7_def)    next      fix h      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Linearize 0 h, s1') ∈ ALM_trans 0 id1"      thus " P7 (s1', s2)"  by (auto simp add: ALM_trans_def P7_def)    next      fix h      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Initialize 0 h, s1') ∈ ALM_trans 0 id1"      thus " P7 (s1', s2)"  by (auto simp add: ALM_trans_def P7_def)    next      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Abort id1, s2') ∈ ALM_trans id1 id2"      thus " P7 (s1, s2')"  by (auto simp add: ALM_trans_def P7_def)    next      assume "P7 (s1, s2)" and "P6 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Abort 0, s1') ∈ ALM_trans 0 id1"      thus " P7 (s1', s2)"  by (auto simp add: ALM_trans_def P7_def)    qed  qedqedlemma  P4_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P4"proof  (rule invariantI, auto)   fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P4 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P4_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P4 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  have "P6 (s1, s2)"  proof -    from in_trans_comp and `reachable (composeALMs id1 id2) (s1, s2)` have "reachable (composeALMs id1 id2) (s1', s2')" by (auto intro: reachable.reachable_n)    with `reachable (composeALMs id1 id2) (s1, s2)` and `0 < id1` and `id1 < id2` and P6_invariant show "P6 (s1, s2)" unfolding invariant_def by auto  qed  from `0 < id1` and `id1 < id2` and in_trans_comp show "P4 (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P4 (s1', s2')" using `P4 (s1, s2)` and `0 < id1` and `id1 < id2` apply(auto simp add: in_trans_cases_fun_def) apply (auto simp add: ALM_trans_def P4_def) done  qedqedlemma  P8_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P8"proof  (rule invariantI, auto)   fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P8 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P8_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  have "P6 (s1, s2)" and "P10 (s1, s2)" and "P5 (s1, s2)" and "P4 (s1, s2)"  proof -    from in_trans_comp and `reachable (composeALMs id1 id2) (s1, s2)` have "reachable (composeALMs id1 id2) (s1', s2')" by (auto intro: reachable.reachable_n)    with `reachable (composeALMs id1 id2) (s1, s2)` and `0 < id1` and `id1 < id2` and P6_invariant and P10_invariant and P5_invariant and P4_invariant show "P6 (s1, s2)" and "P10 (s1, s2)" and "P5 (s1, s2)" and "P4 (s1, s2)" unfolding invariant_def by auto  qed  from `0 < id1` and `id1 < id2` and in_trans_comp show "P8 (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P8 (s1', s2')" using `P8 (s1, s2)` and `0 < id1` and `id1 < id2`     proof (auto simp add: in_trans_cases_fun_def)       fix ca ra      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and in_invoke_1:"(s1, Invoke ca ra, s1') ∈ ALM_trans 0 id1" and in_invoke_2:"(s2, Invoke ca ra, s2') ∈ ALM_trans id1 id2"      show "P8 (s1', s2')"      proof (cases "s1' = s1")        assume "s1' = s1"        with in_invoke_2 and `P8 (s1, s2)` show ?thesis by (auto simp add: ALM_trans_def P8_def)      next        assume "s1' ≠ s1"        with in_invoke_1 have "pendingReqs s1 ⊆ pendingReqs s1'" by (force simp add:pendingReqs_def ALM_trans_def)        moreover from in_invoke_1 have "hist s1' = hist s1" by (auto simp add:ALM_trans_def)        moreover from in_invoke_2 have "initHists s2' = initHists s2" by (auto simp add:ALM_trans_def)        moreover note `P8 (s1, s2)`         ultimately show ?thesis by (auto simp add: ALM_trans_def P8_def linearizations_def postfix_all_def)      qed    next      fix ca h ra      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and in_switch_1:"(s1, Switch ca id1 h ra, s1') ∈ ALM_trans 0 id1" and in_switch_2:"(s2, Switch ca id1 h ra, s2') ∈ ALM_trans id1 id2"      show "P8 (s1', s2')"       proof (auto simp add:P8_def)        fix h1        assume "h1 ∈ initHists s2'"        show "h1 ∈ postfix_all (hist s1') (linearizations (pendingReqs s1'))"        proof (cases "h1 ∈ initHists s2")          assume "h1 ∈ initHists s2"          moreover from in_switch_1 and `0 < id1` have "hist s1' = hist s1" and "pendingReqs s1' = pendingReqs s1" by (auto simp add:ALM_trans_def pendingReqs_def)           moreover note `P8 (s1, s2)`          ultimately show "h1 ∈ postfix_all (hist s1') (linearizations (pendingReqs s1'))" by (auto simp add:P8_def)        next          assume "h1 ∉ initHists s2"          with `h1 ∈ initHists s2'` and in_switch_2 have "h1 = h" by (auto simp add:ALM_trans_def)          with in_switch_1 and `0 < id1` and `P10 (s1, s2)` have "h1 ∈ postfix_all (hist s1) (linearizations (pendingReqs s1))" by (auto simp add:ALM_trans_def P10_def)          moreover from in_switch_1 and `0 < id1` have "hist s1' = hist s1" and "pendingReqs s1' = pendingReqs s1" by (auto simp add:ALM_trans_def pendingReqs_def)          ultimately show ?thesis by auto        qed      qed    next      fix c id' h      assume "P8 (s1, s2)" and "0 < id1" and "(s2, Commit c id' h, s2') ∈ ALM_trans id1 id2" and "id1 ≤ id'" and "id' < id2"      thus " P8 (s1, s2')"  by (auto simp add: ALM_trans_def P8_def)    next      fix c h r      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Switch c id2 h r, s2') ∈ ALM_trans id1 id2"      thus " P8 (s1, s2')"  by (auto simp add: ALM_trans_def P8_def)    next      fix h      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Linearize id1 h, s2') ∈ ALM_trans id1 id2"      thus " P8 (s1, s2')"  by (auto simp add: ALM_trans_def P8_def)    next      fix h      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Initialize id1 h, s2') ∈ ALM_trans id1 id2"      thus " P8 (s1, s2')"  by (auto simp add: ALM_trans_def P8_def)    next      fix ca ta ra      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Switch ca 0 ta ra, s1') ∈ ALM_trans 0 id1"      thus " P8 (s1', s2)" using `P5 (s1, s2)` by (auto simp add: ALM_trans_def P8_def P5_def)    next      fix ca id' h      assume "P8 (s1, s2)" and in_commit_1:"(s1, Commit ca id' h, s1') ∈ ALM_trans 0 id1"      from in_commit_1 have "pendingReqs s1' = pendingReqs s1" and "hist s1' = hist s1" by (auto simp add:pendingReqs_def ALM_trans_def)      with `P8 (s1, s2)` show "P8 (s1', s2)" by (auto simp add: ALM_trans_def P8_def pendingReqs_def)    next      fix h      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Linearize 0 h, s1') ∈ ALM_trans 0 id1"      thus "P8 (s1', s2)" using `P6 (s1, s2)` and `P4 (s1, s2)` by (auto simp add: ALM_trans_def P8_def P6_def P4_def)    next      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Abort id1, s2') ∈ ALM_trans id1 id2"      thus " P8 (s1, s2')"  by (auto simp add: ALM_trans_def P8_def)    next      fix h      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Initialize 0 h, s1') ∈ ALM_trans 0 id1"      thus " P8 (s1', s2)" using `P10 (s1, s2)` by (auto simp add: ALM_trans_def P8_def P10_def)    next      assume "P8 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Abort 0, s1') ∈ ALM_trans 0 id1"      thus " P8 (s1', s2)" by (auto simp add: ALM_trans_def P8_def pendingReqs_def)    qed  qedqedlemma  P12_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P12"proof  clarify   assume "id1 < id2" and "0 < id1"  with P8_invariant and P4_invariant have "invariant (composeALMs id1 id2) (λ (s1, s2) . P8 (s1, s2) ∧ P4 (s1, s2))" by (auto simp add:invariant_def)  moreover have "∀ s . P8 s ∧ P4 s--> P12 s"  proof auto    fix s1 s2    assume "P8 (s1, s2)" and "P4 (s1, s2)"    hence initHists_prop:"∀ h ∈ initHists s2 . (∃ h' . h = h' @ (hist s1) ∧ set h' ⊆ pendingReqs s1 ∧ distinct h')" by (auto simp add:P8_def postfix_all_def linearizations_def)    show "P12 (s1, s2)"    proof (simp add:P12_def, rule impI)      assume "∃ c . phase s2 c ≠ Sleep"      with `P4 (s1, s2)` have "initHists s2 ≠ {}" by (auto simp add:P4_def)      with l_c_p_lemma[of "initHists s2" "hist s1"] and initHists_prop       obtain rs where "l_c_p (initHists s2) = rs @ hist s1" by (auto simp add: suffixeq_def)      moreover have "set rs ⊆ pendingReqs s1"      proof -        from `initHists s2 ≠ {}` obtain h where "h ∈ initHists s2" by auto        with initHists_prop obtain h' where "h = h' @ (hist s1) ∧ set h' ⊆ pendingReqs s1" by auto        moreover from l_c_p_common_postfix[of "initHists s2"] and `h ∈ initHists s2` obtain h'' where "h = h'' @ (l_c_p (initHists s2))" by (auto simp add:common_postfix_p_def suffixeq_def)        moreover note `l_c_p (initHists s2) = rs @ hist s1`        ultimately show ?thesis by auto      qed      moreover have "distinct rs"      proof -        from `initHists s2 ≠ {}` obtain h where "h ∈ initHists s2" by auto        with initHists_prop obtain h' where "h = h' @ (hist s1)" and "distinct h'" by auto        with l_c_p_common_postfix[of "initHists s2"] and `h ∈ initHists s2` and `l_c_p (initHists s2) = rs @ hist s1` obtain h'' where "h' = h'' @ rs" apply (auto simp add:common_postfix_p_def suffixeq_def) by (metis `h = h' @ hist s1` append_assoc append_same_eq)        with `distinct h'` show ?thesis by auto      qed      ultimately show "∃rs. l_c_p (initHists s2) = rs @ hist s1 ∧ set rs ⊆ pendingReqs s1 ∧ distinct rs" by auto    qed  qed  ultimately show ?thesis by (auto intro:invariant_imp)qedlemma  P11_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P11"proof clarify    assume "id1 < id2" and "0 < id1"  with P8_invariant and P12_invariant and P6_invariant and P7_invariant have "invariant (composeALMs id1 id2) (λ (s1, s2) . P8 (s1, s2) ∧ P12 (s1, s2) ∧ P6 (s1, s2) ∧ P7 (s1, s2))" by (auto simp add:invariant_def)  moreover have "∀ s . P8 s ∧ P12 s ∧ P6 s ∧ P7 s --> P11 s"  proof auto    fix s1 s2    assume "P8 (s1, s2)" and "P12 (s1, s2)" and "P6 (s1, s2)" and "P7 (s1, s2)"    show "P11 (s1, s2)"    proof (simp add:P11_def initValidReqs_def, auto)      fix x c h      assume "phase s2 c ≠ Sleep"      with `P12 (s1, s2)` and `P8 (s1, s2)` have  initHists_prop:"∀ h ∈ initHists s2 . (∃ h' . h = h' @ (hist s1) ∧ set h' ⊆ pendingReqs s1)" and lcp_prop:"∃ rs . l_c_p (initHists s2) = rs @ (hist s1)" by (auto simp add:P12_def P8_def postfix_all_def linearizations_def)      assume "x ∉ set (l_c_p (initHists s2))" and "h ∈ initHists s2" and "x ∈ set h"      from initHists_prop and `h ∈ initHists s2` obtain h' where "h = h' @ (hist s1)" and "set h' ⊆ pendingReqs s1" by auto      moreover from lcp_prop obtain rs where "l_c_p (initHists s2) = rs @ (hist s1)" by auto      moreover note `x ∉ set (l_c_p (initHists s2))` and `x ∈ set h`      ultimately have "x ∈ set h'" by auto      with `set h' ⊆ pendingReqs s1` show "x ∈ pendingReqs s1" by auto    next      fix x c h      assume "phase s2 c ≠ Sleep" and "¬ initialized s2"      with `P12 (s1, s2)` have  lcp_prop:"∃ rs . l_c_p (initHists s2) = rs @ (hist s1)" by (auto simp add:P12_def P8_def postfix_all_def linearizations_def)      assume "x ∉ set (l_c_p (initHists s2))" and "x ∈ pendingReqs s2"      from `x ∉ set (l_c_p (initHists s2))` and lcp_prop have "x ∉ set (hist s1)" by auto      moreover obtain c' where "phase s1 c' = Aborted" and "x = pending s1 c'"      proof -        from `x ∈ pendingReqs s2` and `P6 (s1, s2)` obtain c' where "phase s1 c' = Aborted" and "x = pending s2 c'" by (force simp add:pendingReqs_def P6_def)        moreover with `¬ initialized s2` and  `P7 (s1, s2)` have "x = pending s1 c'" by (auto simp add:P7_def)        ultimately show "(!!c'. [|phase s1 c' = Aborted; x = pending s1 c'|] ==> thesis) ==> thesis" by auto      qed      ultimately show "x ∈ pendingReqs s1" by (auto simp add:pendingReqs_def)    qed  qed  ultimately show ?thesis by (auto intro:invariant_imp)qedlemma  P1a_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P1a"proof (rule invariantI, auto)    fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P1a (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P1a_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P1a (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  have "P5 (s1, s2)"  proof -    from in_trans_comp and `reachable (composeALMs id1 id2) (s1, s2)` have "reachable (composeALMs id1 id2) (s1', s2')" by (auto intro: reachable.reachable_n)    with `reachable (composeALMs id1 id2) (s1, s2)` and `0 < id1` and `id1 < id2` and P5_invariant show "P5 (s1, s2)" unfolding invariant_def by auto  qed  from `0 < id1` and `id1 < id2` and in_trans_comp show "P1a (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P1a (s1', s2')" using `P1a (s1, s2)` and `P5 (s1, s2)` and `0 < id1` and `id1 < id2` apply(auto simp add: in_trans_cases_fun_def) apply (auto simp add: ALM_trans_def P1a_def P5_def) done  qedqedlemma  P1b_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P1b"proof (rule invariantI, auto)    fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P1b (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P1b_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P1b (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  have "P1a (s1, s2)"  proof -    from in_trans_comp and `reachable (composeALMs id1 id2) (s1, s2)` have "reachable (composeALMs id1 id2) (s1', s2')" by (auto intro: reachable.reachable_n)    with `reachable (composeALMs id1 id2) (s1, s2)` and `0 < id1` and `id1 < id2` and P1a_invariant show "P1a (s1, s2)" unfolding invariant_def by auto  qed  from `0 < id1` and `id1 < id2` and in_trans_comp show "P1b (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P1b (s1', s2')" using `P1b (s1, s2)` and `P1a (s1, s2)` and `0 < id1` and `id1 < id2` apply(auto simp add: in_trans_cases_fun_def) apply (auto simp add: ALM_trans_def P1b_def P1a_def) done  qedqedlemma  P13_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P13"proof clarify    assume "id1 < id2" and "0 < id1"  with P11_invariant and P12_invariant have "invariant (composeALMs id1 id2) (λ (s1, s2) . P11 (s1, s2) ∧ P12 (s1, s2))" by (auto simp add:invariant_def)  moreover have "∀ s . P11 s ∧ P12 s --> P13 s"  proof auto    fix s1 s2    assume "P11 (s1, s2)" and "P12 (s1, s2)"    show "P13 (s1, s2)"    proof (simp add:P13_def, rule impI)      assume "(∃ c . phase s2 c ≠ Sleep) ∧ ¬ initialized s2"      with `P12 (s1, s2)` and `P11 (s1, s2)` obtain rs where initValidReqs_prop:"initValidReqs s2 ⊆ pendingReqs s1" and "l_c_p (initHists s2) = rs @ (hist s1)" and "set rs ⊆ pendingReqs s1" and "distinct rs" by (auto simp add:P12_def P11_def postfix_all_def linearizations_def)      moreover from `l_c_p (initHists s2) = rs @ (hist s1)` have "initValidReqs s2 ∩ set rs = {}" by (auto simp add:initValidReqs_def)      ultimately show "postfix_all (l_c_p (initHists s2)) (linearizations (initValidReqs s2)) ⊆ postfix_all (hist s1) (linearizations (pendingReqs s1))" by (force simp add: postfix_all_def linearizations_def)    qed  qed  ultimately show ?thesis by (auto intro:invariant_imp)qedlemma  P14_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P14"proof (rule invariantI, auto)    fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P14 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P14_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  have "P6 (s1, s2)" and "P13 (s1, s2)" and "P10 (s1, s2)" and "P2 (s1, s2)" and "P4 (s1, s2)"  proof -    from in_trans_comp and `reachable (composeALMs id1 id2) (s1, s2)` have "reachable (composeALMs id1 id2) (s1', s2')" by (auto intro: reachable.reachable_n)    with `reachable (composeALMs id1 id2) (s1, s2)` and `0 < id1` and `id1 < id2` and P6_invariant and P13_invariant and P10_invariant  and P4_invariant and P2_invariant show "P6 (s1, s2)" and "P13 (s1, s2)" and "P10 (s1, s2)" and "P2 (s1, s2)" and "P4 (s1, s2)" unfolding invariant_def by auto  qed  from `0 < id1` and `id1 < id2` and in_trans_comp show "P14 (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P14 (s1', s2')" using `P14 (s1, s2)` and `0 < id1` and `id1 < id2`     proof (auto simp add: in_trans_cases_fun_def)       fix ca ra      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Invoke ca ra, s1') ∈ ALM_trans 0 id1" and "(s2, Invoke ca ra, s2') ∈ ALM_trans id1 id2"      thus " P14 (s1', s2')"  by (auto simp add: ALM_trans_def P14_def)    next      fix ca h ra      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Switch ca id1 h ra, s1') ∈ ALM_trans 0 id1" and "(s2, Switch ca id1 h ra, s2') ∈ ALM_trans id1 id2"      thus " P14 (s1', s2')"  by (auto simp add: ALM_trans_def P14_def)    next      fix c id' h      assume "P14 (s1, s2)" and "0 < id1" and "(s2, Commit c id' h, s2') ∈ ALM_trans id1 id2" and "id1 ≤ id'" and "id' < id2"      thus " P14 (s1, s2')"  by (auto simp add: ALM_trans_def P14_def)    next      fix c h r      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Switch c id2 h r, s2') ∈ ALM_trans id1 id2"      thus " P14 (s1, s2')"  by (auto simp add: ALM_trans_def P14_def)    next      fix h      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Linearize id1 h, s2') ∈ ALM_trans id1 id2"      thus " P14 (s1, s2')" by (auto simp add: ALM_trans_def P14_def linearizations_def postfix_all_def pendingReqs_def)    next      fix h      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Initialize id1 h, s2') ∈ ALM_trans id1 id2"      thus " P14 (s1, s2')" using `P13 (s1, s2)` apply (auto simp add: ALM_trans_def P14_def P13_def linearizations_def postfix_all_def pendingReqs_def) prefer 2 apply force apply blast done    next      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Abort id1, s2') ∈ ALM_trans id1 id2"      thus " P14 (s1, s2')"  by (auto simp add: ALM_trans_def P14_def)    next      fix ca ta ra      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Switch ca 0 ta ra, s1') ∈ ALM_trans 0 id1"      thus " P14 (s1', s2)"  by (auto simp add: ALM_trans_def P14_def)    next      fix ca id' h      assume "P14 (s1, s2)" and "id1 < id2" and "(s1, Commit ca id' h, s1') ∈ ALM_trans 0 id1" and "id' < id1"      thus " P14 (s1', s2)"  by (auto simp add: ALM_trans_def P14_def)    next      fix h      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and in_lin:"(s1, Linearize 0 h, s1') ∈ ALM_trans 0 id1"      from in_lin have "¬ initialized s2" and "hist s2 = []" using `P6 (s1, s2)` and `P2 (s1, s2)` and `P10 (s1, s2)` and `P2 (s1, s2)` by (auto simp add: ALM_trans_def P14_def P6_def P10_def P2_def P2_def)      thus " P14 (s1', s2)" by (auto simp add:P14_def)    next      fix h      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Initialize 0 h, s1') ∈ ALM_trans 0 id1"      thus " P14 (s1', s2)" using `P10 (s1, s2)`by (auto simp add: ALM_trans_def P14_def P10_def)     next      assume "P14 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Abort 0, s1') ∈ ALM_trans 0 id1"      thus " P14 (s1', s2)"  by (auto simp add: ALM_trans_def P14_def)    qed  qedqedlemma  P15_invariant: "[|id1 < id2; id1 ≠ 0|] ==> invariant (composeALMs id1 id2) P15"proof (rule invariantI, auto)    fix s1 s2  assume "(s1, s2) : starts_of (composeALMs id1 id2)" and "0 < id1"  thus "P15 (s1, s2)" by (simp add: starts_of_def composeALMs_def hide_def ALM_ioa_def par_def ALM_start_def P15_def)next  fix s1 s2 s1' s2' act  assume "reachable (composeALMs id1 id2) (s1, s2)" and "P15 (s1, s2)" and "0 < id1" and "id1 < id2" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"  have "P13 (s1, s2)" and "P1b (s1, s2)" and "P6 (s1, s2)" and "P1a (s1, s2)" and "P5 (s1, s2)" and "P10 (s1, s2)"  proof -    from in_trans_comp and `reachable (composeALMs id1 id2) (s1, s2)` have "reachable (composeALMs id1 id2) (s1', s2')" by (auto intro: reachable.reachable_n)    with `reachable (composeALMs id1 id2) (s1, s2)` and `0 < id1` and `id1 < id2` and P13_invariant and P1b_invariant and P1a_invariant and P6_invariant and P5_invariant and P10_invariant  show "P13 (s1, s2)" and "P1b (s1, s2)" and "P6 (s1, s2)" and "P1a (s1, s2)"  and "P5 (s1, s2)" and "P10 (s1, s2)" unfolding invariant_def by auto  qed  from `0 < id1` and `id1 < id2` and in_trans_comp show "P15 (s1', s2')"   proof (rule my_rule2)     assume "in_trans_cases_fun id1 id2 (s1, s2) (s1', s2')"    thus "P15 (s1', s2')" using  `P15 (s1, s2)` and `0 < id1` and `id1 < id2`     proof (auto simp add: in_trans_cases_fun_def)       fix ca ra      assume "P15 (s1, s2)" and in_invoke1:"(s1, Invoke ca ra, s1') ∈ ALM_trans 0 id1" and in_invoke2:"(s2, Invoke ca ra, s2') ∈ ALM_trans id1 id2"      show "P15 (s1', s2')"       proof -        { assume "s1' = s1"          with `P15 (s1, s2)` and in_invoke1 and in_invoke2 and `0 < id1` and `id1 < id2`          have ?thesis by (auto simp add:ALM_trans_def P15_def)        } note case1 = this        { assume "s1' ≠ s1"          with in_invoke1 and in_invoke2 and `P6 (s1, s2)` have "s2' = s2" apply (auto simp add:ALM_trans_def P6_def) by (metis phase.simps(12) phase.simps(4))          with `s1' ≠ s1` and `P15 (s1, s2)` and in_invoke1 have ?thesis by (force simp add:P15_def ALM_trans_def pendingReqs_def) (*TODO: why is it working?*)        } note case2 = this        from case1 and case2 show ?thesis by auto      qed    next      fix ca h ra      assume "P15 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Switch ca id1 h ra, s1') ∈ ALM_trans 0 id1" and "(s2, Switch ca id1 h ra, s2') ∈ ALM_trans id1 id2"      thus " P15 (s1', s2')" by (auto simp add: ALM_trans_def P15_def pendingReqs_def)    next      fix c id' h      assume "P15 (s1, s2)" and "0 < id1" and "(s2, Commit c id' h, s2') ∈ ALM_trans id1 id2" and "id1 ≤ id'" and "id' < id2"      thus " P15 (s1, s2')"  by (auto simp add: ALM_trans_def P15_def)    next      fix c h r      assume "P15 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Switch c id2 h r, s2') ∈ ALM_trans id1 id2"      thus " P15 (s1, s2')"  by (auto simp add: ALM_trans_def P15_def)    next      fix h      assume in_lin:"(s2, Linearize id1 h, s2') ∈ ALM_trans id1 id2"      show "P15 (s1, s2')"      proof (auto simp add:P15_def)        fix r        assume "phase s2' (request_snd r) = Sleep" and "r ∈ set (hist s2')" and "r ∉ pendingReqs s1"        show "r ∈ set (hist s1)"        proof -          from `phase s2' (request_snd r) = Sleep` and in_lin have "phase s2 (request_snd r) = Sleep" by (auto simp add:ALM_trans_def)          with `P1b (s1, s2)` have "r ∉ pendingReqs s2" by (auto simp add:pendingReqs_def P1b_def)          with in_lin and `r ∈ set (hist s2')` have "r ∈ set (hist s2)" by (auto simp add:ALM_trans_def postfix_all_def linearizations_def)          with `phase s2 (request_snd r) = Sleep` and `P15 (s1, s2)` and `r ∉ pendingReqs s1` show ?thesis by (auto simp add:P15_def)        qed      qed    next      assume "P15 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s2, Abort id1, s2') ∈ ALM_trans id1 id2"      thus " P15 (s1, s2')"  by (auto simp add: ALM_trans_def P15_def)    next      fix h      assume in_init:"(s2, Initialize id1 h, s2') ∈ ALM_trans id1 id2"      show " P15 (s1, s2')"       proof (auto simp add:P15_def)        fix r        assume "phase s2' (request_snd r) = Sleep" and "r ∈ set (hist s2')" and "r ∉ pendingReqs s1"        show "r ∈ set (hist s1)"        proof -          from in_init and `P13 (s1, s2)`          have "hist s2' ∈ postfix_all (hist s1) (linearizations (pendingReqs s1))" by (auto simp add:ALM_trans_def P13_def)          with `r ∈ set (hist s2')` have "r ∈ set (hist s1) ∨ r ∈ pendingReqs s1" by (auto simp add: postfix_all_def linearizations_def)          with `r ∉ pendingReqs s1` show ?thesis by auto        qed      qed    next      fix ca ta ra      assume "(s1, Switch ca 0 ta ra, s1') ∈ ALM_trans 0 id1"      hence "s1' = s1" using `P5 (s1, s2)` by (auto simp add: ALM_trans_def P5_def)      thus "P15 (s1', s2)" using `P15 (s1, s2)` by auto    next      fix ca id' h      assume "P15 (s1, s2)" and "id1 < id2" and "(s1, Commit ca id' h, s1') ∈ ALM_trans 0 id1" and "id' < id1"      thus " P15 (s1', s2)" by (auto simp add: ALM_trans_def P15_def pendingReqs_def)    next      fix h      assume "P15 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Linearize 0 h, s1') ∈ ALM_trans 0 id1"      thus "P15 (s1', s2)" by (auto simp add: ALM_trans_def P15_def pendingReqs_def postfix_all_def)    next      fix h      assume "(s1, Initialize 0 h, s1') ∈ ALM_trans 0 id1"      hence "s1' = s1" using `P10 (s1, s2)` by (auto simp add: ALM_trans_def P10_def)      thus "P15 (s1', s2)" using `P15 (s1, s2)` by auto    next      assume "P15 (s1, s2)" and "0 < id1" and "id1 < id2" and "(s1, Abort 0, s1') ∈ ALM_trans 0 id1"      thus " P15 (s1', s2)"  by (auto simp add: ALM_trans_def P15_def pendingReqs_def)    qed  qedqedsubsection {*The refinement proof*}definition ref_mapping :: "(ALM_state * ALM_state) => ALM_state"   -- {*The refinement mapping between the composition of two ALMs and a single ALM*}  where  "ref_mapping ≡ λ (s1, s2) .     (|pending = λc. (if phase s1 c ≠ Aborted then pending s1 c else pending s2 c),      initHists = {},      phase = λc. (if phase s1 c ≠ Aborted then phase s1 c else phase s2 c),      hist = (if hist s2 = [] then hist s1 else hist s2),      aborted = aborted s2,      initialized = True|)),"theorem composition: "[|id1 ≠ 0; id1 < id2|] ==> ((composeALMs id1 id2) =<| (ALM_ioa 0 id2))"  -- {*The composition theorem*}proof -  assume "id1 ≠ 0" and "id1 < id2"  show "composeALMs id1 id2 =<| ALM_ioa 0 id2"  proof  (simp add: ioa_implements_def, rule conjI, rule_tac[2] conjI)     show same_input_sig:"inp (composeALMs id1 id2) = inp (ALM_ioa 0 id2)"     -- {*First we show that both automata have the same input and output signature*}      using  `id1 ≠ 0` and `id1 < id2` by  (simp add: composeALMs_def hide_def hide_asig_def  ALM_ioa_def asig_inputs_def asig_outputs_def asig_of_def ALM_asig_def par_def asig_comp_def, auto)    from `id1 ≠ 0` and `id1 < id2`     show same_output_sig:"out (composeALMs id1 id2) = out (ALM_ioa 0 id2)"       -- {*Then we show that output signatures match*}      by  (simp add:  asig_inputs_def asig_outputs_def asig_of_def composeALMs_def hide_def hide_asig_def ALM_ioa_def ALM_asig_def par_def asig_comp_def, auto)    show "traces (composeALMs id1 id2) <= traces (ALM_ioa 0 id2)"      -- {*Finally we show trace inclusion*}    proof  (rule trace_inclusion[where f=ref_mapping])       -- {*We use the mapping @{text ref_mapping}, defined before*}      from  same_input_sig and same_output_sig show "ext (composeALMs id1 id2) = ext (ALM_ioa 0 id2)"         -- {*First we show that they have the same external signature*}        by  (simp add: externals_def)    next      show "is_ref_map ref_mapping (composeALMs id1 id2) (ALM_ioa 0 id2)"        -- {*Then we show that @{text ref_mapping_comp} is a refinement mapping*}         apply (simp add: is_ref_map_def, auto, rename_tac s1 s2) prefer 2 apply (rename_tac s1 s2 s1' s2' act)       proof -        -- {*First we show that start states correspond*}        fix s1 s2        assume "(s1, s2) : starts_of (composeALMs id1 id2)"        thus "ref_mapping (s1, s2) : starts_of (ALM_ioa 0 id2)" using  `id1 ≠ 0` and `id1 < id2` by  (simp add:  ALM_ioa_def ALM_start_def starts_of_def composeALMs_def hide_def par_def ref_mapping_def)      next          -- {*Then we show the main property of a refinement mapping*}        fix s1 s2 s1' s2' act        assume reachable:"reachable (composeALMs id1 id2) (s1, s2)" and in_trans_comp:"(s1, s2) -act--composeALMs id1 id2-> (s1', s2')"        txt  {*We make the invariants available for later use*}        have "P6 (s1, s2)" and "P6 (s1', s2')" and "P9 (s1, s2)" and "P7 (s1, s2)" and "P10 (s1, s2)" and "P4 (s1, s2)" and "P5 (s1, s2)" and "P13 (s1, s2)" and "P1a (s1, s2)" and "P14 (s1, s2)" and "P14 (s1', s2')" and "P15 (s1, s2)" and "P2 (s1, s2)" and "P3 (s1, s2)"        proof  -          from reachable and in_trans_comp have "reachable (composeALMs id1 id2) (s1', s2')" by (rule reachable.reachable_n)          with P6_invariant and P9_invariant and P2_invariant and P7_invariant and P10_invariant and P4_invariant and P5_invariant and P13_invariant  and P1a_invariant and P14_invariant and P15_invariant  and P3_invariant `id1 ≠ 0` and `id1 < id2` and reachable          show "P6 (s1, s2)" and "P6 (s1', s2')" and "P9 (s1, s2)" and "P7 (s1, s2)" and "P10 (s1, s2)" and "P4 (s1, s2)" and "P5 (s1, s2)" and "P13 (s1, s2)" and "P1a (s1, s2)" and "P14 (s1, s2)"  and "P14 (s1', s2')"  and "P15 (s1, s2)"  and "P2 (s1, s2)" and "P3 (s1, s2)" by (auto simp add: invariant_def)        qed        let ?t = "ref_mapping (s1, s2)"        let ?t' = "ref_mapping (s1', s2')"        show "EX ex. move (ALM_ioa 0 id2) ex ?t act ?t'"          -- {* the main part of the proof *}        proof  (simp add: move_def, auto)           assume "act : ext (ALM_ioa 0 id2)"          hence "act : {act . EX c r . act = Invoke c r | (EX t . act = Switch c 0 t r)} Un {act . EX c tr . (EX id' . 0 <= id' & id' < id2 & act = Commit c id' tr) | (EX r . act = Switch c id2 tr r)}" by  (auto simp add: ALM_ioa_def ALM_asig_def externals_def asig_inputs_def asig_outputs_def asig_of_def)          with in_trans_comp show "EX ex. is_exec_frag (ALM_ioa 0 id2) (?t, ex) & Finite ex & laststate (?t, ex) = ?t' & mk_trace (ALM_ioa 0 id2)\$ex = [act!]"             -- {*If act is an external action of the composition, then there must be an execution of the spec with matching states and forming trace "act"*}             apply auto           proof -            fix c r            assume in_invoke:"(s1, s2) -Invoke c r--composeALMs id1 id2-> (s1', s2')"              -- {*If the current action is Invoke*}            show "EX ex. is_exec_frag (ALM_ioa 0 id2) (?t, ex) & Finite ex & laststate (?t, ex) = ?t' & mk_trace (ALM_ioa 0 id2)\$ex = [Invoke c r!]"            proof  -              let ?ex = "[(Invoke c r, ?t')!]"                (*First a bunch of trivial things*)              have "Finite ?ex" by auto              moreover have "laststate (?t, ?ex) = ?t'" by (simp add: laststate_def)              moreover have "mk_trace (ALM_ioa 0 id2)\$(?ex) = [Invoke c r!]" by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)                (*Proof that ?ex relates the mappings*)              moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)" (*CAN actually go automatically if you wait long enough: using in_invoke and `id1 ≠ 0` and `id1 < id2` and `P6 (s1, s2)` apply (auto simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(force simp add:ALM_trans_def fun_eq_iff P6_def ref_mapping_def)*)              proof -                {                  assume "s1' ≠ s1 & s2' ≠ s2"                     -- {*contradiction*}                  with in_invoke and `id1 ≠ 0` and `id1 < id2` and `P6 (s1', s2')` have ?thesis apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(auto simp add:ALM_trans_def P6_def) done                }                moreover                {                  assume "s1' = s1" and "s2' = s2"                  with in_invoke have pre_s1:"~(phase s1 c = Ready & request_snd r = c & r ∉ set (hist s1))"  and pre_s2:"~(phase s2 c = Ready & request_snd r = c & r ∉ set (hist s2))" apply (auto simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp_all add:ALM_trans_def) apply (drule_tac[!] arg_cong[where f = "phase"]) apply simp_all apply (metis phase.simps(8) fun_upd_idem_iff) apply (metis phase.simps(8) fun_upd_idem_iff) apply (metis phase.simps(8) fun_upd_idem_iff) apply (metis phase.simps(8) fun_upd_idem_iff) done (*TODO: how to deal with records automatically?*)                  hence  "~(phase ?t c = Ready & request_snd r = c & r ∉ set (hist ?t))" using `P14 (s1, s2)` by (auto simp add:ref_mapping_def P14_def)                  hence ?thesis using `id1 ≠ 0`  and `s1' = s1` and `s2' = s2` apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp_all add:ALM_trans_def) apply force done                 }                moreover                {                  assume "s1' ≠ s1" and "s2' = s2"                  with in_invoke have pre_s1:"phase s1 c = Ready & request_snd r = c & r ∉ set (hist s1)" and trans_s1: "s1' = s1(|pending :=  (pending s1)(c := r), phase := (phase s1)(c := Pending)|))," apply (simp_all add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp_all add:ALM_trans_def ref_mapping_def) done                  have pre_t: "phase ?t c = Ready & request_snd r = c & r ∉ set (hist ?t)"                  proof -                    from pre_s1 have "phase ?t c = Ready & request_snd r = c" by (auto simp add:ref_mapping_def)                    moreover have "r ∉ set (hist ?t)"                    proof (cases "hist s2 = []")                      assume "hist s2 = []"                      with pre_s1 show ?thesis by (auto simp add:ref_mapping_def)                    next                      assume "hist s2 ≠ []"                      show "r ∉ set (hist ?t)"                      proof auto                        assume "r ∈ set (hist ?t)"                        with `hist s2 ≠ []` have "r ∈ set (hist s2)" by (auto simp add:ref_mapping_def)                        moreover from pre_s1 and `P6 (s1, s2)` have "phase s2 (request_snd r) = Sleep" by (force simp add:P6_def)                        moreover note `P15 (s1, s2)`                        ultimately have "r ∈ set (hist s1) ∨ r ∈ pendingReqs s1" by (auto simp add:P15_def)                         with pre_s1 have "r ∈ pendingReqs s1" by auto                        with `P1a (s1, s2)` and pre_s1 show False by (auto simp add:pendingReqs_def P1a_def)                      qed                    qed                    ultimately show ?thesis by auto                  qed                  moreover from pre_s1 and trans_s1 and `s2' = s2` have trans_t:"?t' = ?t(|pending :=  (pending ?t)(c := r), phase := (phase ?t)(c := Pending)|))," by (auto simp add:ref_mapping_def  fun_eq_iff)                  ultimately have ?thesis apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp add:ALM_trans_def) done                 }                moreover                {                  assume "s1' = s1" and "s2' ≠ s2"                    (*CAN go automatically: with in_invoke and `id1 ≠ 0` and `P6 (s1, s2)` have ?thesis apply (auto simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(force simp add:ALM_trans_def fun_eq_iff P6_def ref_mapping_def)*)                  with in_invoke and `id1 ≠ 0` have pre_s2: "phase s2 c = Ready & request_snd r = c & r ∉ set (hist s2)" and trans_s2: "s2' = s2(|pending :=  (pending s2)(c := r), phase := (phase s2)(c := Pending)|))," apply (simp_all add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp_all add:ALM_trans_def ref_mapping_def) done                  from pre_s2 and `P6 (s1, s2)`  have aborted_s1_c:"phase s1 c = Aborted" by (auto simp add: P6_def)                   with pre_s2 and `P3 (s1, s2)` and `P14 (s1, s2)` have pre_t:"phase ?t c = Ready & request_snd r = c & r ∉ set (hist ?t)" apply (auto simp add: fun_eq_iff ref_mapping_def P3_def P14_def) done                  moreover have trans_t:"?t' = ?t(|pending :=  (pending ?t)(c := r), phase := (phase ?t)(c := Pending)|))," using aborted_s1_c and `s1' = s1` and trans_s2 apply(force simp add: fun_eq_iff ref_mapping_def) done                  ultimately have ?thesis apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp add:ALM_trans_def) done                 }                ultimately show ?thesis by auto              qed              ultimately show ?thesis by (auto intro: exI[where x="?ex"])            qed          next            fix c r h            assume in_switch:"(s1, s2) -Switch c 0 h r--composeALMs id1 id2-> (s1', s2')"              -- {*If we get a switch 0 input (nothing happens)*}            show "EX ex. is_exec_frag (ALM_ioa 0 id2) (?t, ex) & Finite ex & laststate (?t, ex) = ?t' & mk_trace (ALM_ioa 0 id2)\$ex = [Switch c 0 h r!]"            proof  -              let ?ex = "[(Switch c 0 h r, ?t')!]"                (*First a bunch of trivial things*)              have "Finite ?ex" by auto              moreover have "laststate (?t, ?ex) = ?t'" by (simp add: laststate_def)              moreover have "mk_trace (ALM_ioa 0 id2)\$(?ex) = [Switch c 0 h r!]" by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)                (*Proof that ?ex relates the mappings*)              moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)"              proof -                from in_switch and `id1 ≠ 0` and `id1 < id2` and `P5 (s1, s2)` have "s1' = s1" and "s2' = s2" and "!! c . phase s1 c ≠ Sleep" apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(simp_all add: ALM_trans_def P5_def) done                hence "?t = ?t'" and "!! c . phase ?t c ≠ Sleep" using `P6 (s1, s2)` by (auto simp add:ref_mapping_def P6_def)                thus ?thesis by (simp add:is_exec_frag_def  ALM_ioa_def trans_of_def ALM_trans_def)              qed              ultimately show ?thesis by (auto intro: exI[where x="?ex"])            qed          next            fix c h r            assume in_switch:"(s1, s2) -Switch c id2 h r--composeALMs id1 id2-> (s1', s2')"              -- {*The case when the system switches to a third, new, instance*}            show "EX ex. is_exec_frag (ALM_ioa 0 id2) (?t, ex) &              Finite ex & laststate (?t, ex) = ?t' & mk_trace (ALM_ioa 0 id2)\$ex = [Switch c id2 h r!]"            proof  -              let ?ex = "[(Switch c id2 h r, ?t')!]"              have "Finite ?ex" by auto              moreover have "laststate (?t, ?ex) = ?t'" by (simp add: laststate_def)              moreover have "mk_trace (ALM_ioa 0 id2)\$(?ex) = [Switch c id2 h r!]" by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)                (*Proof that ?ex relates the mappings*)              moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)"              proof -                from in_switch and `id1 < id2` have "s1' = s1" apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) done                from `id1 ≠ 0` and `id1 < id2` in_switch have pre_s2:"aborted s2 & phase s2 c = Pending & r = pending s2 c & (if initialized s2 then (h ∈ postfix_all (hist s2) (linearizations (pendingReqs s2))) else (h : postfix_all (l_c_p (initHists s2)) (linearizations (initValidReqs s2))))" and trans_s2: "s2' = s2(|phase := (phase s2)(c := Aborted)|))," apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def) done                from pre_s2 have s1_aborted:"phase s1 c = Aborted" using `P6 (s1, s2)` apply(auto simp add: P6_def) done                have pre_t:"aborted ?t & phase ?t c = Pending & initialized ?t & h : postfix_all (hist ?t) (linearizations (pendingReqs ?t)) & r = pending ?t c"                 proof -                  from s1_aborted and pre_s2 have "aborted ?t & pending ?t c = r" and "phase ?t c = Pending" and "initialized ?t" by (auto simp add: ref_mapping_def fun_eq_iff)                  moreover have "h : postfix_all (hist ?t) (linearizations (pendingReqs ?t))"                  proof -                    from pre_s2 have "(if initialized s2 then (h : postfix_all (hist s2) (linearizations (pendingReqs s2))) else (h : postfix_all (l_c_p (initHists s2)) (linearizations (initValidReqs s2))))" by auto                    thus ?thesis                    proof auto                      assume case1_1:"initialized s2" and case1_2:"h : postfix_all (hist s2) (linearizations (pendingReqs s2))"                      hence "suffixeq (hist s1) (hist s2)" using `P14 (s1, s2)` by (auto simp add:P14_def suffixeq_def)                      show "h ∈ postfix_all (hist ?t) (linearizations (pendingReqs ?t))"                      proof -                        have "hist ?t = hist s2"                        proof (cases "hist s2 = []")                          assume "hist s2 = []"                          show "hist ?t = hist s2"                          proof -                            from `hist s2 = []` and `suffixeq (hist s1) (hist s2)` have "hist s1 = []" by (auto simp add:suffixeq_def)                            with `hist s2 = []` show  "hist ?t = hist s2" by (auto simp add: ref_mapping_def)                          qed                        next                          assume "hist s2 ≠ []"                          thus "hist ?t = hist s2" by (simp add:ref_mapping_def)                        qed                        moreover have "pendingReqs s2 <= pendingReqs ?t"                        proof (simp add: pendingReqs_def, clarify)                           fix c                          assume "pending s2 c ∉ set (hist s2)" and "phase s2 c = Pending ∨ phase s2 c = Aborted"                          moreover with `P6 (s1, s2)` have "phase s1 c = Aborted" by (auto simp add:P6_def)                          moreover note `suffixeq (hist s1) (hist s2)`                          ultimately show "∃ca. pending s2 c = pending ?t ca ∧ pending s2 c ∉ set (hist ?t) ∧ (phase ?t ca = Pending ∨ phase ?t ca = Aborted)" apply (simp add:ref_mapping_def suffixeq_def) by (metis prefixeq_Nil prefixeq_def self_append_conv2)                        qed                        moreover note  case1_2                        ultimately show ?thesis by (auto simp add: linearizations_def postfix_all_def)                      qed                    next                      assume case2_1:"¬ initialized s2" and case2_2:"h : postfix_all (l_c_p (initHists s2)) (linearizations (initValidReqs s2))"                      from case2_1 and `P10 (s1, s2)` have "hist s2 = []" by (auto simp add:P10_def)                      have "h : postfix_all (hist s1) (linearizations (pendingReqs s1))"                      proof -                        from pre_s2 have "phase s2 c ≠ Sleep" by auto                        moreover note `P13 (s1, s2)` and case2_1 and case2_2                        ultimately  show ?thesis by (auto simp add:P13_def)                      qed                      moreover from `hist s2 = []` have "hist ?t = hist s1" by (auto simp add:P10_def ref_mapping_def)                      moreover have "pendingReqs ?t = pendingReqs s1"                      proof auto                        fix r                        assume "r ∈ pendingReqs ?t"                        with this obtain c' where "r = pending ?t c'" and "r ∉ set (hist ?t)" and "phase ?t c' ∈ {Pending, Aborted}" by (auto simp add:pendingReqs_def)                        show "r ∈ pendingReqs s1"                        proof (cases "phase s1 c' = Aborted")                          assume "phase s1 c' = Aborted"                          with `phase ?t c' ∈ {Pending, Aborted}` and `r = pending ?t c'` have "phase s2 c' ∈ {Pending, Aborted}" and "r = pending s2 c'" by (auto simp add:ref_mapping_def)                          with `P6 (s1, s2)` and case2_1 and `P7 (s1, s2)` and `hist ?t = hist s1` and `r ∉ set (hist ?t)` have "phase s1 c' = Aborted" and "r = pending s1 c'" and "r ∉ set (hist s1)" apply (auto simp add: P6_def P7_def) apply force apply force done                          thus ?thesis by (auto simp add:pendingReqs_def)                        next                          assume "phase s1 c' ≠ Aborted"                          with `r = pending ?t c'` and `r ∉ set (hist ?t)` and `phase ?t c' ∈ {Pending, Aborted}` and `hist ?t = hist s1` show ?thesis by (auto simp add:ref_mapping_def pendingReqs_def)                        qed                      next                        fix r                        assume "r ∈ pendingReqs s1"                        with this obtain c where "r = pending s1 c" and "phase s1 c ∈ {Pending, Aborted}" and "r ∉ set (hist s1)" by (auto simp add:pendingReqs_def)                        with `hist s2 = []` and `¬ initialized s2` and `P7 (s1, s2)` show "r ∈ pendingReqs ?t" by (auto simp add:ref_mapping_def pendingReqs_def P7_def)                      qed                      ultimately show ?thesis by (auto simp add: postfix_all_def linearizations_def)                    qed                  qed                  ultimately show ?thesis by auto                qed                moreover have trans_t:"?t' = ?t(|phase := (phase ?t)(c := Aborted)|))," using s1_aborted and `s1' = s1` and trans_s2 by (auto simp add:ref_mapping_def fun_eq_iff)                ultimately show ?thesis using `id1 < id2` apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp add:ALM_trans_def) done              qed              ultimately show ?thesis by (auto intro: exI[where x="?ex"])            qed          next            fix c h id'            assume in_commit:"(s1, s2) \<midarrow>Commit c id' h\<midarrow>composeALMs id1 id2--> (s1', s2')" and "id' <  id2"              -- {*Case when the composition commits a request*}            show "∃ex. is_exec_frag (ALM_ioa 0 id2) (?t, ex) ∧ Finite ex ∧ laststate (?t, ex) = ?t' ∧ mk_trace (ALM_ioa 0 id2)·ex = [Commit c id' h!]"            proof  -              let ?ex = "[(Commit c id' h, ?t')!]"                (*First a bunch of trivial things*)              have "Finite ?ex" by auto              moreover have "laststate (?t, ?ex) = ?t'" by (simp add: laststate_def)              moreover have "mk_trace (ALM_ioa 0 id2)\$(?ex) = [Commit c id' h!]" using `id' < id2` by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)                (*Proof that ?ex relates the mappings*)              moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)"              proof -                {                  assume "id' < id1"                  with in_commit have "s2' = s2" and pre_s1:"phase s1 c = Pending ∧ pending s1 c ∈ set (hist s1) ∧ h = dropWhile (λ r . r ≠ pending s1 c) (hist s1)" and trans_s1:"s1' = s1 (|phase := (phase s1)(c := Ready)|))," apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def) done                  from pre_s1 have s1_not_aborted_c:"phase s1 c ≠ Aborted" by auto                  have pre_t:"phase ?t c = Pending & pending ?t c ∈ set (hist ?t) ∧ h = dropWhile (λ r . r ≠ pending ?t c) (hist ?t)"                  proof (cases "hist s2 = []")                    assume "hist s2 = []"                    with pre_s1 and `phase s1 c ≠ Aborted` show ?thesis by (auto simp add: ref_mapping_def)                  next                    assume "hist s2 ≠ []"                    hence "initialized s2" using `P10 (s1, s2)` by (auto simp add:P10_def)                    from pre_s1 and `phase s1 c ≠ Aborted` have "phase ?t c = Pending" and "pending ?t c = pending s1 c" and "pending s1 c ∈ set (hist s1)" by (auto simp add:ref_mapping_def)                    moreover have "pending ?t c ∈ set (hist ?t)"                    proof -                      from `initialized s2` and `P14 (s1, s2)` obtain rs3 where "hist s2 = rs3 @ (hist s1)" by (auto simp add:P14_def)                      with `pending s1 c ∈ set (hist s1)` and `hist s2 = rs3 @ (hist s1)` and `pending ?t c = pending s1 c` show "pending ?t c ∈ set (hist ?t)" by (auto simp add:ref_mapping_def suffixeq_def)                    qed                    moreover have "h = dropWhile (λ r . r ≠ pending ?t c) (hist ?t)"                    proof -                      from `pending s1 c ∈ set (hist s1)` obtain rs1 rs2 where "hist s1 = rs2 @ rs1" and "hd rs1 = pending s1 c" and "rs1 ≠ []" and "pending s1 c ∉ set rs2"  by (metis hd.simps in_set_conv_decomp_first list.simps(3))                      with `pending ?t c = pending s1 c` and dropWhile_lemma[of "hist s1" rs1 "pending s1 c"] and pre_s1 have "h = rs1" by auto                      moreover have "dropWhile (λ r . r ≠ pending ?t c) (hist ?t) = rs1"                      proof -                        from `initialized s2` and `P14 (s1, s2)` obtain rs3 where "hist s2 = rs3 @ (hist s1)" and "set rs3 ∩ set (hist s1) = {}" by (auto simp add:P14_def)                        with `pending s1 c ∈ set (hist s1)` and `hist s1 = rs2 @ rs1` have "hist s2 = rs3 @ rs2 @ rs1" and "pending s1 c ∉ set rs3" by auto                        with `pending s1 c ∉ set rs2` obtain rs4 where "hist s2 = rs4 @ rs1" and "pending s1 c ∉ set rs4" by auto                        with `hd rs1 = pending s1 c` and `rs1 ≠ []` and dropWhile_lemma[of "hist s2" rs1 "pending s1 c"] have "dropWhile (λ r . r ≠ pending s1 c) (hist s2) = rs1" by auto                        thus ?thesis using `hist s2 ≠ []` and `pending ?t c = pending s1 c` by (auto simp add:ref_mapping_def)                      qed                      ultimately show ?thesis by auto                    qed                    ultimately show ?thesis by auto                  qed                  moreover from `s2' = s2` and s1_not_aborted_c and trans_s1 have trans_t:"?t' = ?t (|phase := (phase ?t)(c := Ready)|))," by (simp add:fun_eq_iff ref_mapping_def)                  ultimately have ?thesis using `id1 < id2` apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp add:ALM_trans_def) done                }                moreover                 {                  assume "id1 ≤ id'"                  with in_commit have "s1' = s1" and pre_s2:"phase s2 c = Pending ∧ pending s2 c ∈ set (hist s2) ∧ h = dropWhile (λ r . r ≠ pending s2 c) (hist s2)" and trans_s2:"s2' = s2 (|phase := (phase s2)(c := Ready)|))," apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def) done                  from pre_s2 and `P6 (s1, s2)` have facts:"aborted s1 & phase s1 c = Aborted & hist s2 ≠ []" by (force simp add:P6_def)                  with pre_s2 have pre_t:"phase ?t c = Pending ∧ pending ?t c ∈ set (hist ?t) ∧ h = dropWhile (λ r . r ≠ pending ?t c) (hist ?t)" by (auto simp add:ref_mapping_def)                  moreover from `s1' = s1` and facts and trans_s2 have trans_t:"?t' = ?t (|phase := (phase ?t)(c := Ready)|))," by (auto simp add:fun_eq_iff ref_mapping_def)                  ultimately have ?thesis using `id1 < id2` apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp add:ALM_trans_def) done                }                ultimately show ?thesis using `id' < id2` by force              qed              ultimately show ?thesis by (auto intro: exI[where x="?ex"])            qed          qed              -- {*We finished the case when the composition takes an action that is in the external signature of the spec*}        next          assume "act ∉ ext (ALM_ioa 0 id2)"            -- {*Now the case when the composition takes an action that is not in the external signature of the spec*}          with in_trans_comp and `id1 < id2` and `id1 ≠ 0` have "act : {act . act = Abort 0 | act = Abort id1 | (EX c r h . act = Linearize 0 h | act = Linearize id1 h | act = Switch c id1 h r | act = Initialize 0 h | act = Initialize id1 h)}" by  (auto simp add: composeALMs_def hide_def hide_asig_def ALM_ioa_def ALM_asig_def externals_def asig_inputs_def asig_outputs_def asig_internals_def asig_of_def trans_of_def par_def actions_def)          with in_trans_comp show "∃ex. is_exec_frag (ALM_ioa 0 id2) (?t, ex) ∧ Finite ex ∧ laststate (?t, ex) = ?t' ∧ mk_trace (ALM_ioa 0 id2)·ex = nil"           proof  auto             assume in_abort:"(s1, s2) \<midarrow>Abort 0\<midarrow>composeALMs id1 id2--> (s1', s2')"              -- {*The case where the first Abastract aborts*}            moreover  with `id1 ≠ 0` and `id1 < id2` and `P6 (s1, s2)` and `P2 (s1, s2)` have "∀ c . phase s1 c ≠ Aborted" and "hist s2 = []" and "∀ c . phase s2 c = Sleep" apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:fun_eq_iff ALM_trans_def ref_mapping_def P6_def P2_def) done            moreover  note `id1 ≠ 0`             ultimately  have "?t' = ?t"  apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:fun_eq_iff ALM_trans_def ref_mapping_def) done             thus ?thesis            proof  simp              let ?ex = "nil"              have "Finite ?ex" by auto              moreover have "laststate (?t, ?ex) = ?t" by (simp add: laststate_def)              moreover have "mk_trace (ALM_ioa 0 id2)·?ex = nil" using `id1 < id2` by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)              moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)" by (auto simp add:is_exec_frag_def)              ultimately show "∃ex. is_exec_frag (ALM_ioa 0 id2) (?t, ex) ∧ Finite ex ∧ laststate (?t, ex) = ?t ∧ mk_trace (ALM_ioa 0 id2)·ex = nil" by (auto intro: exI[where x="?ex"])            qed          next            assume in_abort:"(s1, s2) \<midarrow>Abort id1\<midarrow>composeALMs id1 id2--> (s1', s2')"              -- {*The case where the second ALM aborts*}            show ?thesis            proof  -              let ?ex = "[(Abort 0, ?t')!]"              have "Finite ?ex" by auto              moreover have "laststate (?t, ?ex) = ?t'" by (simp add: laststate_def)              moreover have "mk_trace (ALM_ioa 0 id2)·?ex = nil" by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)              moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)"              proof -                from in_abort and `id1 ≠ 0` have "s1' = s1" and pre_s2:"~ aborted s2 & (∃ c . phase s2 c ≠ Sleep)" and trans_s2:"s2' = s2(|aborted:= True|))," apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def) done                from pre_s2 and `P6 (s1, s2)` have pre_t:"~ aborted ?t  & (∃ c . phase ?t c ≠ Sleep)" apply (force simp add:ref_mapping_def P6_def) done                moreover from trans_s2 and `s1' = s1` have trans_t:"?t' = ?t(|aborted:= True|))," by (auto simp add: fun_eq_iff ref_mapping_def)                ultimately show ?thesis  apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(simp add:ALM_trans_def) done              qed              ultimately show ?thesis by (auto intro: exI[where x="?ex"])            qed          next            fix h            assume in_lin:"(s1, s2) \<midarrow>Linearize 0 h\<midarrow>composeALMs id1 id2--> (s1', s2')"              -- {*If the composition executes Linearize 0*}            show ?thesis            proof  -              let ?ex = "[(Linearize 0 h, ?t')!]"              have "Finite ?ex" by auto              moreover have "laststate (?t, ?ex) = ?t'" by (simp add: laststate_def)              moreover have "mk_trace (ALM_ioa 0 id2)·?ex = nil" by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)              moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)"              proof -                from in_lin and `id1 ≠ 0` have "s2' = s2" and pre_s1:"initialized s1 & ~ aborted s1 & h ∈ postfix_all (hist s1) (linearizations (pendingReqs s1))" and trans_s1:"s1' = s1(|hist := h, initialized := True|)),"  apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def) done                have pre_t:"initialized ?t & ~ aborted ?t & h ∈ postfix_all (hist ?t) (linearizations (pendingReqs ?t))"                proof -                  from  pre_s1 have "~ aborted s1" by auto                  with `P9 (s1, s2)` have "~ aborted ?t" and "initialized ?t" by (auto simp add:ref_mapping_def P9_def)                  moreover have "h ∈ postfix_all (hist ?t) (linearizations (pendingReqs ?t))"                  proof -                    from `¬ aborted s1` have "hist ?t = hist s1" using `P6 (s1, s2)` and `P2 (s1, s2)`  by (auto simp add:P6_def P2_def ref_mapping_def)                    moreover have "pendingReqs s1 ⊆ pendingReqs ?t"                     proof auto                      fix x                      assume "x ∈ pendingReqs s1"                      moreover note `¬ aborted s1` and `P6 (s1 ,s2)`                      ultimately obtain c where "x = pending s1 c" and "phase s1 c = Pending" and "pending s1 c ∉ set (hist s1)" by (auto simp add:pendingReqs_def P6_def)                      thus "x ∈ pendingReqs ?t" using `hist ?t = hist s1` by (force simp add:ref_mapping_def pendingReqs_def)                    qed                    moreover from pre_s1 have "h ∈ postfix_all (hist s1) (linearizations (pendingReqs s1))" by auto                    ultimately show ?thesis by (auto simp add: postfix_all_def linearizations_def)                  qed                  ultimately show ?thesis by auto                qed                moreover have trans_t: "?t' = ?t(|hist := h, initialized := True|)),"                proof -                  have "hist ?t' = hist s1'"                  proof -                    from pre_s1 have "~ aborted s1" by auto                    with  `P6 (s1, s2)` and `P2 (s1, s2)` have "hist s2 = []" by (auto simp add:P6_def P2_def)                    with `s2' = s2` show ?thesis by (auto simp add:ref_mapping_def)                  qed                  with trans_s1 have "hist ?t' = h" by auto                  thus ?thesis using `s2' = s2` and trans_s1 by (auto simp add:ref_mapping_def fun_eq_iff)                qed                ultimately show ?thesis  apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(auto simp add:ALM_trans_def) done              qed              ultimately show ?thesis by (auto intro: exI[where x="?ex"])            qed          next            fix h            assume in_lin:"(s1, s2) \<midarrow>Linearize id1 h\<midarrow>composeALMs id1 id2--> (s1', s2')"              -- {*If the composition executes Linearize id1*}            let ?ex = "[(Linearize id1 h, ?t')!]"            have "Finite ?ex" by auto            moreover have "laststate (?t, ?ex) = ?t'" by (simp add: laststate_def)            moreover have "mk_trace (ALM_ioa 0 id2)·?ex = nil" by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)            moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)"            proof -              from in_lin and `id1 ≠ 0` have "s1' = s1" and pre_s2: "initialized s2 ∧ ¬ aborted s2 ∧ h ∈ postfix_all (hist s2) (linearizations (pendingReqs s2))" and trans_s2: "s2' = s2(|hist := h|)),"  apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def) done              have pre_t:"initialized ?t ∧ ¬ aborted ?t ∧ h ∈ postfix_all (hist ?t) (linearizations (pendingReqs ?t))"              proof -                have  "¬ aborted ?t" and "initialized ?t" using pre_s2 by (auto simp add:ref_mapping_def)                moreover have "h ∈ postfix_all (hist ?t) (linearizations (pendingReqs ?t))"                proof -                  from pre_s2 have "initialized s2" by auto                  hence "suffixeq (hist s1) (hist s2)" using `P14 (s1, s2)` by (auto simp add:P14_def suffixeq_def)                  hence "hist ?t = hist s2"  by (auto simp add:ref_mapping_def)                  moreover have "pendingReqs s2 ⊆ pendingReqs ?t"                  proof auto                    fix x                    assume "x ∈ pendingReqs s2"                    from this obtain c where "x = pending s2 c" and "phase s2 c ∈ {Pending, Aborted}" and "pending s2 c ∉ set (hist s2)" by (auto simp add:pendingReqs_def)                    with `P6 (s1, s2)` and `hist ?t = hist s2` show "x ∈ pendingReqs ?t" by (force simp add:ref_mapping_def P6_def pendingReqs_def)                  qed                  moreover from pre_s2 have "h ∈ postfix_all (hist s2) (linearizations (pendingReqs s2))" by auto                  ultimately show ?thesis by (auto simp add:postfix_all_def linearizations_def)                qed                ultimately show ?thesis by auto              qed              moreover have trans_t: "?t' = ?t(|hist := h|)),"              proof -                from pre_s2 and trans_s2 have "initialized s2'" by auto                hence "suffixeq (hist s1') (hist s2')"  using `P14 (s1', s2')` by (auto simp add:P14_def suffixeq_def)                hence "hist ?t' = hist s2'" by (auto simp add:ref_mapping_def)                with trans_s2 and `s1' = s1` show ?thesis by (auto simp add:ref_mapping_def fun_eq_iff)              qed              ultimately show ?thesis  apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(auto simp add:ALM_trans_def) done            qed                        ultimately show ?thesis by  (auto intro: exI[where x="?ex"])          next            fix c r h            assume in_switch:"(s1, s2) \<midarrow>Switch c id1 h r\<midarrow>composeALMs id1 id2--> (s1', s2')"              -- {*If the composition switches internally*}            show ?thesis            proof -              let ?ex = "nil"              have "Finite ?ex" by auto              moreover have "laststate (?t, ?ex) = ?t" by (simp add: laststate_def)              moreover have "mk_trace (ALM_ioa 0 id2)·?ex = nil" by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)              moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)" by (auto simp add:is_exec_frag_def)              moreover have "?t' = ?t"              proof -                from in_switch and `id1 ≠ 0` have pre_s1:"aborted s1 ∧ phase s1 c = Pending ∧ r = pending s1 c ∧ (if initialized s1 then (h ∈ postfix_all (hist s1) (linearizations (pendingReqs s1))) else (h : postfix_all (l_c_p (initHists s1)) (linearizations (initValidReqs s1))))" and trans_s1: "s1' = s1(|phase := (phase s1)(c := Aborted)|))," apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def) done                 have pre_s2:"phase s2 c = Sleep" and trans_s2: "s2' = s2 (|initHists := {h} ∪ (initHists s2), phase := (phase s2)(c := Pending), pending := (pending s2)(c := r)|)),"                proof -                  from pre_s1 have "phase s1 c = Pending" by auto                  with `P6 (s1, s2)` have "phase s2 c = Sleep" apply (simp add:P6_def) by (metis phase.simps(10))                  with in_switch and `id1 ≠ 0` and `id1 < id2` show "phase s2 c = Sleep" and  "s2' = s2 (|initHists := {h} ∪ (initHists s2), phase := (phase s2)(c := Pending), pending := (pending s2)(c := r)|)),"  apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def P6_def) done                qed                from pre_s1 and pre_s2 and trans_s1 and trans_s2 and `P1a (s1, s2)` have "pending ?t c = pending ?t' c & initHists ?t = initHists ?t' & hist ?t = hist ?t' & aborted ?t = aborted ?t' ∧ phase ?t' c = phase ?t c" by (simp add:ref_mapping_def fun_eq_iff P1a_def)                moreover note pre_s1 and pre_s2 and trans_s1 and trans_s2                ultimately show ?thesis by (force simp add:ref_mapping_def fun_eq_iff)              qed              ultimately show ?thesis  by (auto intro: exI[where x="?ex"])            qed          next            fix h            assume in_initialize:"(s1, s2) \<midarrow>Initialize 0 h\<midarrow>composeALMs id1 id2--> (s1', s2')"            hence False  using `P10 (s1, s2)` apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def P10_def) done             thus ?thesis by  auto          next            fix h            assume in_initialize:"(s1, s2) \<midarrow>Initialize id1 h\<midarrow>composeALMs id1 id2--> (s1', s2')"            -- {*If the second ALM of the composition initializes*}            let ?ex = "[(Linearize id1 h, ?t')!]"            have "Finite ?ex" by auto            moreover have "laststate (?t, ?ex) = ?t'" by (simp add: laststate_def)            moreover have "mk_trace (ALM_ioa 0 id2)·?ex = nil" by (simp add: mk_trace_def externals_def asig_inputs_def asig_outputs_def asig_of_def ALM_ioa_def ALM_asig_def)            moreover have "is_exec_frag (ALM_ioa 0 id2) (?t, ?ex)"            proof -              from in_initialize and `id1 ≠ 0` have "s1' = s1" and pre_s2:"(∃ c . phase s2 c ≠ Sleep) ∧ ¬ aborted s2 ∧ ¬ initialized s2 ∧ h ∈ postfix_all (l_c_p (initHists s2)) (linearizations (initValidReqs s2))" and trans_s2:"s2' = s2(|hist := h, initialized := True|)),"  apply (simp_all add: composeALMs_def trans_of_def hide_def  par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def ALM_ioa_def ALM_asig_def) apply(auto simp add:ALM_trans_def) done              have pre_t:"initialized ?t ∧ ¬ aborted ?t ∧ h ∈ postfix_all (hist ?t) (linearizations (pendingReqs ?t))"              proof -                from pre_s2 have "initialized ?t ∧ ¬ aborted ?t" by (auto simp add:ref_mapping_def)                moreover have "h ∈ postfix_all (hist ?t) (linearizations (pendingReqs ?t))"                proof -                  from pre_s2 have "h ∈ postfix_all (l_c_p (initHists s2)) (linearizations (initValidReqs s2))" and "¬ initialized s2" and "∃ c . phase s2 c ≠ Sleep" by auto                  with `P13 (s1, s2)` have "h ∈ postfix_all (hist s1) (linearizations (pendingReqs s1))" by (auto simp add:P13_def)                  moreover from `¬ initialized s2` and `P10 (s1, s2)` have "hist ?t = hist s1" by (auto simp add:ref_mapping_def P10_def)                  moreover have "pendingReqs s1 ⊆ pendingReqs ?t"                  proof auto                    fix x                    assume "x ∈ pendingReqs s1"                    from this obtain c where "x = pending s1 c" and "phase s1 c ∈ {Pending, Aborted}" and "pending s1 c ∉ set (hist s1)" by (auto simp add:pendingReqs_def)                    show "x ∈ pendingReqs ?t"                    proof (cases "phase s1 c = Pending")                      assume "phase s1 c = Pending"                      with `x = pending s1 c` and `pending s1 c ∉ set (hist s1)` and `hist ?t = hist s1` show ?thesis by (force simp add:ref_mapping_def pendingReqs_def)                    next                      assume "phase s1 c ≠ Pending"                      with `phase s1 c ∈ {Pending, Aborted}` have "phase s1 c = Aborted" by auto                      with `¬ initialized s2` and `P6 (s1, s2)` and `P7 (s1, s2)` have "pending s2 c = pending s1 c" and "phase s2 c ∈ {Pending, Aborted}" by (auto simp add:P6_def P7_def)                      with `x = pending s1 c` and `pending s1 c ∉ set (hist s1)` and `hist ?t = hist s1` and `P6 (s1, s2)` show ?thesis by (auto simp add:ref_mapping_def pendingReqs_def P6_def)                     qed                  qed                  ultimately show ?thesis by (auto simp add:postfix_all_def linearizations_def)                qed                ultimately show ?thesis by auto              qed              moreover have trans_t:"?t' = ?t(|hist := h|)),"              proof -                from pre_s2 have "∃ c . phase s2 c ≠ Sleep" by auto                with trans_s2 have "initialized s2'" and "∃ c . phase s2' c ≠ Sleep" by auto                hence "suffixeq (hist s1') (hist s2')" using `P14 (s1', s2')` by (auto simp add:P14_def suffixeq_def)                hence "hist ?t' = hist s2'" by (auto simp add:ref_mapping_def)                with trans_s2 and `s1' = s1` show ?thesis by (auto simp add:ref_mapping_def fun_eq_iff)              qed              ultimately show ?thesis  apply (simp add: is_exec_frag_def composeALMs_def trans_of_def hide_def  ALM_ioa_def ALM_asig_def par_def actions_def asig_outputs_def asig_inputs_def asig_internals_def asig_of_def) apply(auto simp add:ALM_trans_def) done            qed            ultimately show ?thesis by (auto intro: exI[where x="?ex"])          qed         qed      qed    qed  qedqedend`