Theory Composing_Security

section ‹Binary compositionality theorem›

text ‹This theory provides the binary version of
the compositionality theorem for BD security.
It corresponds to Theorem 1 from \<^cite>‹"cosmedis-SandP2017"›
and to Theorem 5 (the System Compositionality Theorem) from
\<^cite>‹"BDsecurity-ITP2021"›.
›

theory Composing_Security
  imports Bounded_Deducibility_Security.BD_Security_TS
begin

(* Preliminaries *)


lemma list2_induct[case_names NilNil Cons1 Cons2]:
assumes NN: "P [] []"
and CN: "⋀x xs ys. P xs ys ⟹ P (x # xs) ys"
and NC: "⋀xs y ys. P xs ys ⟹ P xs (y # ys)"
shows "P xs ys"
proof (induction xs)
  case Nil show ?case using NN NC by (induction ys) auto next
  case (Cons x xs) then show ?case using CN by auto
qed

lemma list22_induct[case_names NilNil ConsNil NilCons ConsCons]:
assumes NN: "P [] []"
and CN: "⋀x xs. P xs [] ⟹ P (x # xs) []"
and NC: "⋀y ys. P [] ys ⟹ P [] (y # ys)"
and CC: "⋀x xs y ys.
   P xs ys ⟹
   (⋀ ys'. length ys' ≤ Suc (length ys) ⟹ P xs ys') ⟹
   (⋀ xs'. length xs' ≤ Suc (length xs) ⟹ P xs' ys) ⟹
   P (x # xs) (y # ys)"
shows "P xs ys"
proof (induction rule: measure_induct2[of "λxs ys. length xs + length ys", case_names IH])
  case (IH xs ys) with assms show ?case by (cases xs; cases ys) auto
qed


context BD_Security_TS begin

declare O_append[simp]
declare V_append[simp]
declare validFrom_Cons[simp]
declare validFrom_append[simp]

declare list_all_O_map[simp]
declare never_O_Nil[simp]
declare list_all_V_map[simp]
declare never_V_Nil[simp]

end (* BD_Security_NIO_Aut *)


locale Abstract_BD_Security_Comp =
  One: Abstract_BD_Security validSystemTraces1 V1 O1 B1 TT1 +
  Two: Abstract_BD_Security validSystemTraces2 V2 O2 B2 TT2 +
  Comp?: Abstract_BD_Security validSystemTraces V O B TT (* Note: the "Comp" prefix will be optional *)
for
   validSystemTraces1 :: "'traces1 ⇒ bool"
 and
   V1 :: "'traces1 ⇒ 'values1" and O1 :: "'traces1 ⇒ 'observations1"
 and
   TT1 :: "'traces1 ⇒ bool"
 and
   B1 :: "'values1 ⇒ 'values1 ⇒ bool"
 and
(*  *)
   validSystemTraces2 :: "'traces2 ⇒ bool"
 and
   V2 :: "'traces2 ⇒ 'values2" and O2 :: "'traces2 ⇒ 'observations2"
 and
   TT2 :: "'traces2 ⇒ bool"
 and
   B2 :: "'values2 ⇒ 'values2 ⇒ bool"
 and
 (*  *)
   validSystemTraces :: "'traces ⇒ bool"
 and
   V :: "'traces ⇒ 'values" and O :: "'traces ⇒ 'observations"
 and
   TT :: "'traces ⇒ bool"
 and
   B :: "'values ⇒ 'values ⇒ bool"
+
fixes
   comp :: "'traces1 ⇒ 'traces2 ⇒ 'traces ⇒ bool"
 and
   compO :: "'observations1 ⇒ 'observations2 ⇒ 'observations ⇒ bool"
 and
   compV :: "'values1 ⇒ 'values2 ⇒ 'values ⇒ bool"
assumes
validSystemTraces:
"⋀ tr. validSystemTraces tr ⟹
 (∃ tr1 tr2. validSystemTraces1 tr1 ∧ validSystemTraces2 tr2 ∧ comp tr1 tr2 tr)"
and
V_comp:
"⋀ tr1 tr2 tr.
   validSystemTraces1 tr1 ⟹ validSystemTraces2 tr2 ⟹ comp tr1 tr2 tr
   ⟹ compV (V1 tr1) (V2 tr2) (V tr)"
and
O_comp:
"⋀ tr1 tr2 tr.
   validSystemTraces1 tr1 ⟹ validSystemTraces2 tr2 ⟹ comp tr1 tr2 tr
   ⟹ compO (O1 tr1) (O2 tr2) (O tr)"
and
TT_comp:
"⋀ tr1 tr2 tr.
   validSystemTraces1 tr1 ⟹ validSystemTraces2 tr2 ⟹ comp tr1 tr2 tr
   ⟹ TT tr ⟹ TT1 tr1 ∧ TT2 tr2"
and
B_comp:
"⋀ vl1 vl2 vl vl'.
   compV vl1 vl2 vl ⟹ B vl vl'
   ⟹ ∃ vl1' vl2'. compV vl1' vl2' vl' ∧ B1 vl1 vl1' ∧ B2 vl2 vl2'"
and
O_V_comp:
"⋀ tr1 tr2 vl ol.
   validSystemTraces1 tr1 ⟹ validSystemTraces2 tr2 ⟹
   compV (V1 tr1) (V2 tr2) vl ⟹ compO (O1 tr1) (O2 tr2) ol
   ⟹ ∃ tr. validSystemTraces tr ∧ O tr = ol ∧ V tr = vl"
begin

abbreviation secure where "secure ≡ Comp.secure"
abbreviation secure1 where "secure1 ≡ One.secure"
abbreviation secure2 where "secure2 ≡ Two.secure"

theorem secure1_secure2_secure:
assumes s1: secure1 and s2: secure2
shows secure
unfolding secure_def proof clarify
  fix tr vl vl'
  assume v: "validSystemTraces tr" and T: "TT tr" and B: "B (V tr) vl'"
  then obtain tr1 tr2 where v1: "validSystemTraces1 tr1" and v2: "validSystemTraces2 tr2"
  and tr: "comp tr1 tr2 tr" using validSystemTraces by blast
  have T1: "TT1 tr1" and T2: "TT2 tr2" using TT_comp[OF v1 v2 tr T] by auto
  have Vtr: "compV (V1 tr1) (V2 tr2) (V tr)" using V_comp[OF v1 v2 tr] .
  have Otr: "compO (O1 tr1) (O2 tr2) (O tr)" using O_comp[OF v1 v2 tr] .
  obtain vl1' vl2' where vl': "compV vl1' vl2' vl'" and
  B1: "B1 (V1 tr1) vl1'" and B2: "B2 (V2 tr2) vl2'" using B_comp[OF Vtr B] by auto
  obtain tr1' where v1': "validSystemTraces1 tr1'" and O1: "O1 tr1 = O1 tr1'" and vl1': "vl1' = V1 tr1'"
  using s1 v1 T1 B1 unfolding One.secure_def by fastforce
  obtain tr2' where v2': "validSystemTraces2 tr2'" and O2: "O2 tr2 = O2 tr2'" and vl2': "vl2' = V2 tr2'"
  using s2 v2 T2 B2 unfolding Two.secure_def by fastforce
  obtain tr' where "validSystemTraces tr' ∧ O tr' = O tr ∧ V tr' = vl'"
  using O_V_comp[OF v1' v2' vl'[unfolded vl1' vl2'] Otr[unfolded O1 O2]] by auto
  thus "∃tr'. validSystemTraces tr' ∧ O tr' = O tr ∧ V tr' = vl'" by auto
qed

end (* context BD_Security_Comp *)


type_synonym ('state1,'state2) cstate = "'state1 × 'state2"
datatype ('state1,'trans1,'state2,'trans2) ctrans = Trans1 'state2 'trans1 | Trans2 'state1 'trans2 | CTrans 'trans1 'trans2
datatype ('obs1,'obs2) cobs = Obs1 'obs1 | Obs2 'obs2 | CObs 'obs1 'obs2
datatype ('value1,'value2) "cvalue" = isValue1: Value1 'value1 | isValue2: Value2 'value2 | isCValue: CValue 'value1 'value2


locale BD_Security_TS_Comp =
  One: BD_Security_TS istate1 validTrans1 srcOf1 tgtOf1 φ1 f1 γ1 g1 T1 B1 +
  Two: BD_Security_TS istate2 validTrans2 srcOf2 tgtOf2 φ2 f2 γ2 g2 T2 B2
for
   istate1 :: "'state1" and validTrans1 :: "'trans1 ⇒ bool"
 and
   srcOf1 :: "'trans1 ⇒ 'state1" and tgtOf1 :: "'trans1 ⇒ 'state1"
 and
   φ1 :: "'trans1 ⇒ bool" and f1 :: "'trans1 ⇒ 'value1"
 and
   γ1 :: "'trans1 ⇒ bool" and g1 :: "'trans1 ⇒ 'obs1"
 and
   T1 :: "'trans1 ⇒ bool" and B1 :: "'value1 list ⇒ 'value1 list ⇒ bool"
 and
 (*  *)
   istate2 :: "'state2" and validTrans2 :: "'trans2 ⇒ bool"
 and
   srcOf2 :: "'trans2 ⇒ 'state2" and tgtOf2 :: "'trans2 ⇒ 'state2"
 and
   φ2 :: "'trans2 ⇒ bool" and f2 :: "'trans2 ⇒ 'value2"
 and
   γ2 :: "'trans2 ⇒ bool" and g2 :: "'trans2 ⇒ 'obs2"
 and
   T2 :: "'trans2 ⇒ bool" and B2 :: "'value2 list ⇒ 'value2 list ⇒ bool"
+
fixes (* An identification of the communication transitions and of the synchronization predicate:  *)
  isCom1 :: "'trans1 ⇒ bool" and isCom2 :: "'trans2 ⇒ bool"
and
  sync :: "'trans1 ⇒ 'trans2 ⇒ bool"
and
  isComV1 :: "'value1 ⇒ bool" and isComV2 :: "'value2 ⇒ bool"
and
  syncV :: "'value1 ⇒ 'value2 ⇒ bool"
and
  isComO1 :: "'obs1 ⇒ bool" and isComO2 :: "'obs2 ⇒ bool"
and
  syncO :: "'obs1 ⇒ 'obs2 ⇒ bool"
(*  *)
assumes
  isCom1_isComV1: "⋀ trn1. validTrans1 trn1 ⟹ One.reach (srcOf1 trn1) ⟹ φ1 trn1 ⟹ isCom1 trn1 ⟷ isComV1 (f1 trn1)"
and
  isCom1_isComO1: "⋀ trn1. validTrans1 trn1 ⟹ One.reach (srcOf1 trn1) ⟹ γ1 trn1 ⟹ isCom1 trn1 ⟷ isComO1 (g1 trn1)"
and
  isCom2_isComV2: "⋀ trn2. validTrans2 trn2 ⟹ Two.reach (srcOf2 trn2) ⟹ φ2 trn2 ⟹ isCom2 trn2 ⟷ isComV2 (f2 trn2)"
and
  isCom2_isComO2: "⋀ trn2. validTrans2 trn2 ⟹ Two.reach (srcOf2 trn2) ⟹ γ2 trn2 ⟹ isCom2 trn2 ⟷ isComO2 (g2 trn2)"
and
  sync_syncV:
  "⋀ trn1 trn2.
       validTrans1 trn1 ⟹ One.reach (srcOf1 trn1) ⟹
       validTrans2 trn2 ⟹ Two.reach (srcOf2 trn2) ⟹
       isCom1 trn1 ⟹ isCom2 trn2 ⟹ φ1 trn1 ⟹ φ2 trn2 ⟹
       sync trn1 trn2 ⟹ syncV (f1 trn1) (f2 trn2)"
and
  sync_syncO:
  "⋀ trn1 trn2.
       validTrans1 trn1 ⟹ One.reach (srcOf1 trn1) ⟹
       validTrans2 trn2 ⟹ Two.reach (srcOf2 trn2) ⟹
       isCom1 trn1 ⟹ isCom2 trn2 ⟹ γ1 trn1 ⟹ γ2 trn2 ⟹
       sync trn1 trn2 ⟹ syncO (g1 trn1) (g2 trn2)"
and
  sync_φ1_φ2:
  "⋀ trn1 trn2.
       validTrans1 trn1 ⟹ One.reach (srcOf1 trn1) ⟹
       validTrans2 trn2 ⟹ Two.reach (srcOf2 trn2) ⟹
       isCom1 trn1 ⟹ isCom2 trn2 ⟹
       sync trn1 trn2 ⟹ φ1 trn1 ⟷ φ2 trn2"
and
  sync_φ_γ:
"⋀ trn1 trn2.
     validTrans1 trn1 ⟹ One.reach (srcOf1 trn1) ⟹
     validTrans2 trn2 ⟹ Two.reach (srcOf2 trn2) ⟹
     isCom1 trn1 ⟹ isCom2 trn2 ⟹
     γ1 trn1 ⟹ γ2 trn2 ⟹
     syncO (g1 trn1) (g2 trn2) ⟹
     (φ1 trn1 ⟹ φ2 trn2 ⟹ syncV (f1 trn1) (f2 trn2))
     ⟹
     sync trn1 trn2"
and  (* Every communication is observable (which does not mean that everything in
       a communication is observable!): *)
  isCom1_γ1: "⋀ trn1. validTrans1 trn1 ⟹ One.reach (srcOf1 trn1) ⟹ isCom1 trn1 ⟹ γ1 trn1"
and
  isCom2_γ2: "⋀ trn2. validTrans2 trn2 ⟹ Two.reach (srcOf2 trn2) ⟹ isCom2 trn2 ⟹ γ2 trn2"
and (* Lack of symmetry here: all the value-producing transitions of the second component
       need to be "communicating" (and hence proceed only synchronously) -- Technically, this tames shuffling...
       This restriction means that the only component that produces secrets is the first component -- the
       second component only receives secrets. *)
  isCom2_V2: "⋀ trn2. validTrans2 trn2 ⟹ Two.reach (srcOf2 trn2) ⟹ φ2 trn2 ⟹ isCom2 trn2"
and (* Added dummy assumption about the locale data not involved in any assumption: *)
  Dummy: "istate1 = istate1 ∧ srcOf1 = srcOf1 ∧ tgtOf1 = tgtOf1 ∧ T1 = T1 ∧ B1 = B1 ∧
          istate2 = istate2 ∧ srcOf2 = srcOf2 ∧ tgtOf2 = tgtOf2 ∧ T2 = T2 ∧ B2 = B2"
begin

lemma sync_γ1_γ2:
 "⋀ trn1 trn2.
      validTrans1 trn1 ⟹ One.reach (srcOf1 trn1) ⟹
      validTrans2 trn2 ⟹ Two.reach (srcOf2 trn2) ⟹
      isCom1 trn1 ⟹ isCom2 trn2 ⟹
      sync trn1 trn2 ⟹ γ1 trn1 ⟷ γ2 trn2"
using isCom1_γ1 isCom2_γ2
by auto


definition icstate where "icstate = (istate1,istate2)"

fun validTrans :: "('state1, 'trans1, 'state2, 'trans2) ctrans ⇒ bool" where
 "validTrans(Trans1 s2 trn1) = (validTrans1 trn1 ∧ ¬ isCom1 trn1)"
|"validTrans (Trans2 s1 trn2) = (validTrans2 trn2 ∧ ¬ isCom2 trn2)"
|"validTrans (CTrans trn1 trn2) =
   (validTrans1 trn1 ∧ validTrans2 trn2 ∧ isCom1 trn1 ∧ isCom2 trn2 ∧ sync trn1 trn2)"

fun srcOf :: "('state1, 'trans1, 'state2, 'trans2) ctrans ⇒ 'state1 × 'state2" where
 "srcOf (Trans1 s2 trn1) = (srcOf1 trn1, s2)"
|"srcOf (Trans2 s1 trn2) = (s1, srcOf2 trn2)"
|"srcOf (CTrans trn1 trn2) = (srcOf1 trn1, srcOf2 trn2)"

fun tgtOf :: "('state1, 'trans1, 'state2, 'trans2) ctrans ⇒ 'state1 × 'state2" where
 "tgtOf (Trans1 s2 trn1) = (tgtOf1 trn1, s2)"
|"tgtOf (Trans2 s1 trn2) = (s1, tgtOf2 trn2)"
|"tgtOf (CTrans trn1 trn2) = (tgtOf1 trn1, tgtOf2 trn2)"

fun φ :: "('state1, 'trans1, 'state2, 'trans2) ctrans ⇒ bool" where
 "φ (Trans1 s2 trn1) = φ1 trn1"
|"φ (Trans2 s1 trn2) = φ2 trn2"
|"φ (CTrans trn1 trn2) = (φ1 trn1 ∨ φ2 trn2)"

fun f :: "('state1, 'trans1, 'state2, 'trans2) ctrans ⇒ ('value1,'value2) cvalue" where
 "f (Trans1 s2 trn1) = Value1 (f1 trn1)"
|"f (Trans2 s1 trn2) = Value2 (f2 trn2)"
|"f (CTrans trn1 trn2) = CValue (f1 trn1) (f2 trn2)"

fun γ :: "('state1, 'trans1, 'state2, 'trans2) ctrans ⇒ bool" where
 "γ (Trans1 s2 trn1) = γ1 trn1"
|"γ (Trans2 s1 trn2) = γ2 trn2"
|"γ (CTrans trn1 trn2) = (γ1 trn1 ∨ γ2 trn2)"

fun g :: "('state1, 'trans1, 'state2, 'trans2) ctrans ⇒ ('obs1,'obs2) cobs" where
 "g (Trans1 s2 trn1) = Obs1 (g1 trn1)"
|"g (Trans2 s1 trn2) = Obs2 (g2 trn2)"
|"g (CTrans trn1 trn2) = CObs (g1 trn1) (g2 trn2)"

fun T :: "('state1, 'trans1, 'state2, 'trans2) ctrans ⇒ bool"
where
"T (Trans1 s2 trn1) = T1 trn1"
|
"T (Trans2 s1 trn2) = T2 trn2"
|
"T (CTrans trn1 trn2) = (T1 trn1 ∨ T2 trn2)"

inductive compV :: "'value1 list ⇒ 'value2 list ⇒ ('value1, 'value2) cvalue list ⇒ bool"
where
 Nil[intro!,simp]: "compV [] [] []"
|Step1[intro]:
"compV vl1 vl2 vl ⟹ ¬ isComV1 v1
 ⟹ compV (v1 # vl1) vl2 (Value1 v1 # vl)"
|Step2[intro]:
"compV vl1 vl2 vl ⟹ ¬ isComV2 v2
 ⟹ compV vl1 (v2 # vl2) (Value2 v2 # vl)"
|Com[intro]:
"compV vl1 vl2 vl ⟹ isComV1 v1 ⟹ isComV2 v2 ⟹ syncV v1 v2
 ⟹ compV (v1 # vl1) (v2 # vl2) (CValue v1 v2 # vl)"

lemma compV_cases_V[consumes 3, case_names Nil Step1 Com]:
assumes v: "Two.validFrom s2 tr2"
and c: "compV vl1 (Two.V tr2) vl"
and rs2: "Two.reach s2"
and Nil: "vl1 = [] ⟹ Two.V tr2 = [] ⟹ vl = [] ⟹ P"
and Step1:
"⋀vll1 vll2 vll v1.
    vl1 = v1 # vll1 ⟹
    Two.V tr2 = vll2 ⟹
    vl = Value1 v1 # vll ⟹
    compV vll1 vll2 vll ⟹ ¬ isComV1 v1 ⟹ P"
and Com:
"⋀vll1 vll2 vll v1 v2.
    vl1 = v1 # vll1 ⟹
    Two.V tr2 = v2 # vll2 ⟹
    vl = CValue v1 v2 # vll ⟹
    compV vll1 vll2 vll ⟹
    isComV1 v1 ⟹ isComV2 v2 ⟹ syncV v1 v2 ⟹ P"
shows P
using c proof cases
  case (Step2 vll2 vll1 v2)
  obtain tr2a trn2 tr2b where tr2: "tr2 = tr2a @ trn2 # tr2b" and
  φ2: "φ2 trn2" and f2: "f2 trn2 = v2"
  using ‹Two.V tr2 = v2 # vll2› by (metis Two.V_eq_Cons append_Cons)
  have v2: "validTrans2 trn2" using tr2 v
  by (metis Nil_is_append_conv Two.validFrom_def Two.valid_ConsE
          Two.valid_append list.distinct(2) self_append_conv2)
  have rs2': "Two.reach (srcOf2 trn2)" using v rs2 unfolding tr2
    by (induction tr2a arbitrary: s2) (auto intro: Two.reach.Step)
  then have False using isCom2_V2[OF v2 rs2' φ2] ‹¬ isComV2 v2›
  using φ2 f2 isCom2_isComV2 v2 by blast
  thus ?thesis by simp
qed (insert assms, auto)


inductive compO :: "'obs1 list ⇒ 'obs2 list ⇒ ('obs1, 'obs2) cobs list ⇒ bool"
where
 Nil[intro!,simp]: "compO [] [] []"
|Step1[intro]:
"compO ol1 ol2 ol ⟹ ¬ isComO1 o1
 ⟹ compO (o1 # ol1) ol2 (Obs1 o1 # ol)"
|Step2[intro]:
"compO ol1 ol2 ol ⟹ ¬ isComO2 o2
 ⟹ compO ol1 (o2 # ol2) (Obs2 o2 # ol)"
|Com[intro]:
"compO ol1 ol2 ol ⟹ isComO1 o1 ⟹ isComO2 o2 ⟹ syncO o1 o2
 ⟹ compO (o1 # ol1) (o2 # ol2) (CObs o1 o2 # ol)"

definition B :: "('value1,'value2) cvalue list ⇒ ('value1,'value2) cvalue list ⇒ bool" where
"B vl vl' ≡ ∀ vl1 vl2. compV vl1 vl2 vl ⟶
  (∃ vl1' vl2'. compV vl1' vl2' vl' ∧ B1 vl1 vl1' ∧ B2 vl2 vl2')"

inductive ccomp ::
"'state1 ⇒ 'state2 ⇒ 'trans1 trace ⇒ 'trans2 trace ⇒
 ('state1, 'trans1, 'state2, 'trans2) ctrans trace ⇒ bool"
where
Nil[simp,intro!]: "ccomp s1 s2 [] [] []"
|
Step1[intro]:
"ccomp (tgtOf1 trn1) s2 tr1 tr2 tr ⟹ ¬ isCom1 trn1 ⟹
 ccomp (srcOf1 trn1) s2 (trn1 # tr1) tr2 (Trans1 s2 trn1 # tr)"
|
Step2[intro]:
"ccomp s1 (tgtOf2 trn2) tr1 tr2 tr ⟹ ¬ isCom2 trn2 ⟹
 ccomp s1 (srcOf2 trn2) tr1 (trn2 # tr2) (Trans2 s1 trn2 # tr)"
|
Com[intro]:
"ccomp (tgtOf1 trn1) (tgtOf2 trn2) tr1 tr2 tr ⟹
 isCom1 trn1 ⟹ isCom2 trn2 ⟹ sync trn1 trn2 ⟹
 ccomp (srcOf1 trn1) s2 (trn1 # tr1) (trn2 # tr2) (CTrans trn1 trn2 # tr)"


definition comp where "comp ≡ ccomp istate1 istate2"

end (* context BD_Security_TS_Comp *)

sublocale BD_Security_TS_Comp ⊆ BD_Security_TS icstate validTrans srcOf tgtOf φ f γ g T B .

context BD_Security_TS_Comp
begin

lemma valid:
assumes "valid tr" and "srcOf (hd tr) = (s1,s2)"
shows
"∃tr1 tr2.
   One.validFrom s1 tr1 ∧ Two.validFrom s2 tr2 ∧
   ccomp s1 s2 tr1 tr2 tr"
using assms proof(induction arbitrary: s1 s2)
  case (Singl trn)
  show ?case proof(cases trn)
    case (Trans1 s22 trn1)
    show ?thesis using Singl unfolding Trans1
    by (intro exI[of _ "[trn1]"] exI[of _ "[]"]) auto
  next
    case (Trans2 s11 trn2)
    show ?thesis using Singl unfolding Trans2
    by (intro exI[of _ "[]::'trans1 trace"] exI[of _ "[trn2]"]) auto
  next
    case (CTrans trn1 trn2)
    show ?thesis using Singl unfolding CTrans
    by (intro exI[of _ "[trn1]"] exI[of _ "[trn2]"]) auto
  qed
next
  case (Cons trn tr)
  show ?case proof(cases trn)
    case (Trans1 s22 trn1)
    let ?s1 = "tgtOf1 trn1"
    have s22[simp]: "s22 = s2" using ‹srcOf (hd (trn # tr)) = (s1, s2)›
    unfolding Trans1 by simp
    hence "tgtOf trn = (?s1, s2)" unfolding Trans1 by simp
    hence "srcOf (hd tr) = (?s1, s2)" using Cons.hyps(2) by auto
    from Cons.IH[OF this] obtain tr1 tr2 where
    1: "One.validFrom ?s1 tr1 ∧ Two.validFrom s2 tr2 ∧
        ccomp ?s1 s2 tr1 tr2 tr" by auto
    show ?thesis using Cons.prems Cons.hyps 1 unfolding Trans1
    by (intro exI[of _ "trn1 # tr1"] exI[of _ "tr2"], cases tr2) auto
  next
    case (Trans2 s11 trn2)
    let ?s2 = "tgtOf2 trn2"
    have s11[simp]: "s11 = s1" using ‹srcOf (hd (trn # tr)) = (s1, s2)›
    unfolding Trans2 by simp
    hence "tgtOf trn = (s1, ?s2)" unfolding Trans2 by simp
    hence "srcOf (hd tr) = (s1, ?s2)" using Cons.hyps(2) by auto
    from Cons.IH[OF this] obtain tr1 tr2 where
    1: "One.validFrom s1 tr1 ∧ Two.validFrom ?s2 tr2 ∧
        ccomp s1 ?s2 tr1 tr2 tr" by auto
    show ?thesis using Cons.prems Cons.hyps 1 unfolding Trans2
    by (intro exI[of _ "tr1"] exI[of _ "trn2 # tr2"], cases tr1) auto
  next
    case (CTrans trn1 trn2)
    let ?s1 = "tgtOf1 trn1" let ?s2 = "tgtOf2 trn2"
    have "tgtOf trn = (?s1, ?s2)" unfolding CTrans by simp
    hence "srcOf (hd tr) = (?s1, ?s2)" using Cons.hyps(2) by auto
    from Cons.IH[OF this] obtain tr1 tr2 where
    1: "One.validFrom ?s1 tr1 ∧ Two.validFrom ?s2 tr2 ∧
        ccomp ?s1 ?s2 tr1 tr2 tr" by auto
    show ?thesis using Cons.prems Cons.hyps 1 unfolding CTrans
    by (intro exI[of _ "trn1 # tr1"] exI[of _ "trn2 # tr2"], cases tr2) auto
  qed
qed

lemma validFrom:
assumes "validFrom icstate tr"
shows "∃tr1 tr2. One.validFrom istate1 tr1 ∧ Two.validFrom istate2 tr2 ∧ comp tr1 tr2 tr"
using assms valid unfolding comp_def icstate_def validFrom_def by(cases tr) fastforce+

lemma reach_reach12:
assumes "reach s"
obtains "One.reach (fst s)" and "Two.reach (snd s)"
using assms proof (induction rule: reach.induct)
  case Istate
    then show thesis using One.reach.Istate Two.reach.Istate unfolding icstate_def by auto
next
  case (Step s trn s')
    then show thesis
      using One.reach.Step[of "fst s" _ "fst s'"] Two.reach.Step[of "snd s" _ "snd s'"]
      by (auto elim: validTrans.elims)
qed

lemma compV_ccomp:
assumes v: "One.validFrom s1 tr1" "Two.validFrom s2 tr2"
and c: "ccomp s1 s2 tr1 tr2 tr"
and rs1: "One.reach s1" and rs2: "Two.reach s2"
shows "compV (One.V tr1) (Two.V tr2) (V tr)"
using c v rs1 rs2 proof(induction)
  case (Step1 trn1 s2 tr1 tr2 tr)
  moreover then have "One.reach (tgtOf1 trn1)"
    using One.reach.Step[of "srcOf1 trn1" trn1 "tgtOf1 trn1"] by auto
  ultimately show ?case by (cases "φ1 trn1") (auto simp: isCom1_isComV1)
next
  case (Step2 s1 trn2 tr1 tr2 tr)
  moreover then have "Two.reach (tgtOf2 trn2)"
    using Two.reach.Step[of "srcOf2 trn2" trn2 "tgtOf2 trn2"] by auto
  ultimately show ?case by (cases "φ2 trn2") (auto simp: isCom2_isComV2)
next
  case (Com trn1 trn2 tr1 tr2 tr s2)
  moreover then have "One.reach (tgtOf1 trn1)" "Two.reach (tgtOf2 trn2)"
    using One.reach.Step[of "srcOf1 trn1" trn1 "tgtOf1 trn1"]
          Two.reach.Step[of "srcOf2 trn2" trn2 "tgtOf2 trn2"]
    by auto
  ultimately show ?case
    by (cases "φ1 trn1"; cases "φ2 trn2"; simp add: isCom1_isComV1 isCom2_isComV2)
       (use sync_φ1_φ2 sync_syncV Com in auto)
qed auto

lemma compV:
assumes "One.validFrom istate1 tr1" and "Two.validFrom istate2 tr2"
and "comp tr1 tr2 tr"
shows "compV (One.V tr1) (Two.V tr2) (V tr)"
using compV_ccomp assms One.reach.Istate Two.reach.Istate unfolding comp_def by auto

lemma compO_ccomp:
assumes v: "One.validFrom s1 tr1" "Two.validFrom s2 tr2"
and c: "ccomp s1 s2 tr1 tr2 tr"
and rs1: "One.reach s1" and rs2: "Two.reach s2"
shows "compO (One.O tr1) (Two.O tr2) (O tr)"
using c v rs1 rs2 proof(induction)
  case (Step1 trn1 s2 tr1 tr2 tr)
  moreover then have "One.reach (tgtOf1 trn1)"
    using One.reach.Step[of "srcOf1 trn1" trn1 "tgtOf1 trn1"] by auto
  ultimately show ?case by (cases "γ1 trn1") (auto simp: isCom1_isComO1)
next
  case (Step2 s1 trn2 tr1 tr2 tr)
  moreover then have "Two.reach (tgtOf2 trn2)"
    using Two.reach.Step[of "srcOf2 trn2" trn2 "tgtOf2 trn2"] by auto
  ultimately show ?case by (cases "γ2 trn2") (auto simp: isCom2_isComO2)
next
  case (Com trn1 trn2 tr1 tr2 tr s2)
  moreover then have "One.reach (tgtOf1 trn1)" "Two.reach (tgtOf2 trn2)"
    using One.reach.Step[of "srcOf1 trn1" trn1 "tgtOf1 trn1"]
          Two.reach.Step[of "srcOf2 trn2" trn2 "tgtOf2 trn2"]
    by auto
  ultimately show ?case
    by (cases "γ1 trn1"; cases "γ2 trn2"; simp add: isCom1_isComO1 isCom2_isComO2)
       (use sync_γ1_γ2 sync_syncO Com in auto)
qed auto

lemma compO:
assumes "One.validFrom istate1 tr1" and "Two.validFrom istate2 tr2"
and "comp tr1 tr2 tr"
shows "compO (One.O tr1) (Two.O tr2) (O tr)"
using compO_ccomp assms One.reach.Istate Two.reach.Istate unfolding comp_def by auto

lemma T_ccomp:
assumes v: "One.validFrom s1 tr1" "Two.validFrom s2 tr2"
and c: "ccomp s1 s2 tr1 tr2 tr" and n: "never T tr"
shows "never T1 tr1 ∧ never T2 tr2"
using c n v by (induction) auto

lemma T:
assumes "One.validFrom istate1 tr1" and "Two.validFrom istate2 tr2"
and "comp tr1 tr2 tr" and "never T tr"
shows "never T1 tr1 ∧ never T2 tr2"
using T_ccomp assms unfolding comp_def by auto

lemma B:
assumes "compV vl1 vl2 vl" and "B vl vl'"
shows "∃vl1' vl2'. compV vl1' vl2' vl' ∧ B1 vl1 vl1' ∧ B2 vl2 vl2'"
using assms unfolding B_def by auto

lemma pullback_O_V_aux:
assumes "One.validFrom s1 tr1" "Two.validFrom s2 tr2"
and "One.reach s1" "Two.reach s2"
and "compV (One.V tr1) (Two.V tr2) vl"
and "compO (One.O tr1) (Two.O tr2) obl"
shows "∃tr. validFrom (s1,s2) tr ∧ O tr = obl ∧ V tr = vl"
using assms proof(induction tr1 tr2 arbitrary: s1 s2 vl obl rule: list22_induct)
  case (NilNil s1 s2 vl obl)
  thus ?case by (intro exI[of _ "[]"]) (auto elim: compV.cases compO.cases)
next
  case (ConsNil trn1 tr1 s1 s2 vl obl)
  let ?s1 = "tgtOf1 trn1"
  have trn1: "validTrans1 trn1" and tr1: "One.validFrom ?s1 tr1"
  and s1: "srcOf1 trn1 = s1" "One.reach s1" and rs2: "Two.reach s2" using ConsNil.prems by auto
  then have rs1': "One.reach ?s1" by (intro One.reach.Step[of s1 trn1 ?s1]) auto
  show ?case proof(cases "isCom1 trn1")
    case True note com1 = True
    hence γ1: "γ1 trn1" using trn1 isCom1_γ1 s1 by auto
    hence "isComO1 (g1 trn1)" using γ1 com1 s1 isCom1_isComO1 trn1 by blast
    hence False using ‹compO (One.O (trn1 # tr1)) (Two.O []) obl›
    using γ1 by (auto elim: compO.cases)
    thus ?thesis by simp
  next
    case False note com1 = False
    show ?thesis proof(cases "φ1 trn1")
      case True note φ1 = True
      hence comv1: "¬ isComV1 (f1 trn1)" using φ1 com1 isCom1_isComV1 trn1 s1 by blast
      with ‹compV (One.V (trn1 # tr1)) (Two.V []) vl› φ1
      obtain vll where vl: "vl = Value1 (f1 trn1) # vll"
      and vll: "compV (One.V tr1) (Two.V []) vll" by (auto elim: compV.cases)
      show ?thesis proof(cases "γ1 trn1")
        case True note γ1 = True
        hence "¬ isComO1 (g1 trn1)" using γ1 com1 isCom1_isComO1 trn1 s1 by blast
        with ‹compO (One.O (trn1 # tr1)) (Two.O []) obl› γ1
        obtain obll where obl: "obl = Obs1 (g1 trn1) # obll"
        and obll: "compO (One.O tr1) (Two.O []) obll" by (auto elim: compO.cases)
        from ConsNil.IH[OF tr1 _ rs1' rs2 vll obll] obtain trr where
        "validFrom (?s1, s2) trr" and "O trr = obll ∧ V trr = vll" by auto
        thus ?thesis
        unfolding obl vl using trn1 com1 s1 φ1 γ1
        by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
      next
        case False note γ1 = False
        note obl = ‹compO (One.O (trn1 # tr1)) (Two.O []) obl›
        from ConsNil.IH[OF tr1 _ rs1' rs2 vll] obl γ1 obtain trr where
        "validFrom (?s1, s2) trr" and "O trr = obl ∧ V trr = vll" by auto
        thus ?thesis
        unfolding obl vl using trn1 com1 s1 φ1 γ1
        by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
      qed
    next
      case False note φ1 = False
      note vl = ‹compV (One.V (trn1 # tr1)) (Two.V []) vl›
      show ?thesis proof(cases "γ1 trn1")
        case True note γ1 = True
        hence "¬ isComO1 (g1 trn1)" using γ1 com1 isCom1_isComO1 trn1 s1 by blast
        with ‹compO (One.O (trn1 # tr1)) (Two.O []) obl› γ1
        obtain obll where obl: "obl = Obs1 (g1 trn1) # obll"
        and obll: "compO (One.O tr1) (Two.O []) obll" by (auto elim: compO.cases)
        from ConsNil.IH[OF tr1 _ rs1' rs2 _ obll] vl φ1 obtain trr where
        "validFrom (?s1, s2) trr" and "O trr = obll ∧ V trr = vl" by auto
        thus ?thesis
        unfolding obl vl using trn1 com1 s1 φ1 γ1
        by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
      next
        case False note γ1 = False
        note obl = ‹compO (One.O (trn1 # tr1)) (Two.O []) obl›
        from ConsNil.IH[OF tr1 _ rs1' rs2 _] vl φ1 obl γ1 obtain trr where
        "validFrom (?s1, s2) trr" and "O trr = obl ∧ V trr = vl" by fastforce
        thus ?thesis
        unfolding obl vl using trn1 com1 s1 φ1 γ1
        by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
      qed
    qed
  qed
next
  case (NilCons trn2 tr2 s1 s2 vl obl)
  let ?s2 = "tgtOf2 trn2"
  have trn2: "validTrans2 trn2" and tr2: "Two.validFrom ?s2 tr2"
  and s2: "srcOf2 trn2 = s2" "Two.reach s2" and rs1: "One.reach s1" using NilCons.prems by auto
  then have rs2': "Two.reach ?s2" by (intro Two.reach.Step[of s2 trn2 ?s2]) auto
  show ?case proof(cases "isCom2 trn2")
    case True note com2 = True
    hence γ2: "γ2 trn2" using trn2 isCom2_γ2 s2 by auto
    hence "isComO2 (g2 trn2)" using γ2 com2 isCom2_isComO2 trn2 s2 by blast
    hence False using ‹compO (One.O []) (Two.O (trn2 # tr2)) obl›
    using γ2 by (auto elim: compO.cases)
    thus ?thesis by simp
  next
    case False note com2 = False
    show ?thesis proof(cases "φ2 trn2")
      case True note φ2 = True
      hence comv1: "¬ isComV2 (f2 trn2)" using φ2 com2 isCom2_isComV2 trn2 s2 by blast
      with ‹compV (One.V []) (Two.V (trn2 # tr2)) vl› φ2
      obtain vll where vl: "vl = Value2 (f2 trn2) # vll"
      and vll: "compV (One.V []) (Two.V tr2) vll" by (auto elim: compV.cases)
      show ?thesis proof(cases "γ2 trn2")
        case True note γ2 = True
        hence "¬ isComO2 (g2 trn2)" using γ2 com2 isCom2_isComO2 trn2 s2 by blast
        with ‹compO (One.O []) (Two.O (trn2 # tr2)) obl› γ2
        obtain obll where obl: "obl = Obs2 (g2 trn2) # obll"
        and obll: "compO (One.O []) (Two.O tr2) obll" by (auto elim: compO.cases)
        from NilCons.IH[OF _ tr2 rs1 rs2' vll obll] obtain trr where
        "validFrom (s1, ?s2) trr" and "O trr = obll ∧ V trr = vll" by auto
        thus ?thesis
        unfolding obl vl using trn2 com2 s2 φ2 γ2
        by (intro exI[of _ "Trans2 s1 trn2 # trr"]) auto
      next
        case False note γ2 = False
        note obl = ‹compO (One.O []) (Two.O (trn2 # tr2)) obl›
        from NilCons.IH[OF _ tr2 rs1 rs2' vll] obl γ2 obtain trr where
        "validFrom (s1, ?s2) trr" and "O trr = obl ∧ V trr = vll" by auto
        thus ?thesis
        unfolding obl vl using trn2 com2 s2 φ2 γ2
        by (intro exI[of _ "Trans2 s1 trn2 # trr"]) auto
      qed
    next
      case False note φ2 = False
      note vl = ‹compV (One.V []) (Two.V (trn2 # tr2)) vl›
      show ?thesis proof(cases "γ2 trn2")
        case True note γ2 = True
        hence "¬ isComO2 (g2 trn2)" using γ2 com2 isCom2_isComO2 trn2 s2 by blast
        with ‹compO (One.O []) (Two.O (trn2 # tr2)) obl› γ2
        obtain obll where obl: "obl = Obs2 (g2 trn2) # obll"
        and obll: "compO (One.O []) (Two.O tr2) obll" by (auto elim: compO.cases)
        from NilCons.IH[OF _ tr2 rs1 rs2' _ obll] vl φ2 obtain trr where
        "validFrom (s1, ?s2) trr" and "O trr = obll ∧ V trr = vl" by auto
        thus ?thesis
        unfolding obl vl using trn2 com2 s2 φ2 γ2
        by (intro exI[of _ "Trans2 s1 trn2 # trr"]) auto
      next
        case False note γ2 = False
        note obl = ‹compO (One.O []) (Two.O (trn2 # tr2)) obl›
        from NilCons.IH[OF _ tr2 rs1 rs2' _] vl φ2 obl γ2 obtain trr where
        "validFrom (s1, ?s2) trr" and "O trr = obl ∧ V trr = vl" by fastforce
        thus ?thesis
        unfolding obl vl using trn2 com2 s2 φ2 γ2
        by (intro exI[of _ "Trans2 s1 trn2 # trr"]) auto
      qed
    qed
  qed
next
  case (ConsCons trn1 tr1 trn2 tr2 s1 s2 vl obl)
  let ?s1 = "tgtOf1 trn1"  let ?s2 = "tgtOf2 trn2"
  let ?tr1 = "trn1 # tr1" let ?tr2 = "trn2 # tr2"
  have trn1: "validTrans1 trn1" and tr1: "One.validFrom ?s1 tr1" and s1: "srcOf1 trn1 = s1" "One.reach s1"
  and trn2: "validTrans2 trn2" and tr2: "Two.validFrom ?s2 tr2" and s2: "srcOf2 trn2 = s2" "Two.reach s2"
  using ConsCons.prems by auto
  then have rs1': "One.reach ?s1" and rs2': "Two.reach ?s2"
    using One.reach.Step[of s1 trn1 ?s1] Two.reach.Step[of s2 trn2 ?s2] by auto
  note vl = ‹compV (One.V ?tr1) (Two.V ?tr2) vl›
  note obl = ‹compO (One.O ?tr1) (Two.O ?tr2) obl›
  note trr1 = ‹One.validFrom s1 ?tr1› note trr2 = ‹Two.validFrom s2 ?tr2›
  show ?case proof(cases "φ1 trn1 ∨ γ1 trn1")
    case False note φγ1 = False
    hence com1: "¬ isCom1 trn1" using isCom1_γ1 trn1 s1 by blast
    from ConsCons.IH(2)[of ?tr2, OF _ tr1 trr2 rs1' s2(2)] vl obl φγ1
    obtain trr where "validFrom (?s1, s2) trr" and "O trr = obl ∧ V trr = vl"
    by fastforce
    thus ?thesis
    unfolding obl vl using trn1 com1 s1 φγ1
    by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
  next
    case True note φγ1 = True
    show ?thesis proof(cases "φ2 trn2 ∨ γ2 trn2")
      case False note φγ2 = False
      hence com2: "¬ isCom2 trn2" using isCom2_γ2 trn2 s2 by blast
      from ConsCons.IH(3)[of ?tr1, OF _ trr1 tr2 s1(2) rs2'] vl obl φγ2
      obtain trr where "validFrom (s1, ?s2) trr" and "O trr = obl ∧ V trr = vl"
      by fastforce
      thus ?thesis
      unfolding obl vl using trn2 com2 s2 φγ2
      by (intro exI[of _ "Trans2 s1 trn2 # trr"]) auto
    next
      case True note φγ2 = True
      show ?thesis using obl ConsCons proof cases
        case Nil hence γ12: "¬ γ1 trn1 ∧ ¬ γ2 trn2" by auto
        hence obl: "compO (One.O tr1) (Two.O ?tr2) obl"
                   "compO (One.O tr1) (Two.O tr2) obl"
        using obl by auto
        have φ12: "φ1 trn1 ∧ φ2 trn2" using φγ1 φγ2 γ12 by auto
        show ?thesis using trr2 vl s2(2) proof(cases rule: compV_cases_V)
          case Nil hence False using φ12 by auto
          thus ?thesis by simp
        next
          case (Step1 vll1 vll2 vll v1)
          hence f1: "f1 trn1 = v1" and vll1: "One.V tr1 = vll1" using φ12 by auto
          hence vll: "compV (One.V tr1) (Two.V ?tr2) vll" using Step1 by auto
          from ConsCons.IH(2)[OF _ tr1 trr2 rs1' s2(2) vll obl(1)]
          obtain trr where "validFrom (?s1, s2) trr" and "O trr = obl ∧ V trr = vll"
          by auto
          thus ?thesis using trn1 Step1 f1 φ12 γ12 isCom2_V2 isCom2_γ2 trn2 s2
          by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
        next
          case (Com vll1 vll2 vll v1 v2)
          hence f1: "f1 trn1 = v1" and vll1: "One.V tr1 = vll1"
          and f2: "f2 trn2 = v2" and vll2: "Two.V tr2 = vll2"
          using φ12 by auto
          hence vll: "compV (One.V tr1) (Two.V tr2) vll" using Com by auto
          from ConsCons.IH(1)[OF tr1 tr2 rs1' rs2' vll obl(2)]
          obtain trr where "validFrom (?s1, ?s2) trr" and "O trr = obl ∧ V trr = vll"
          by auto
          thus ?thesis using trn1 Step1 f1 φ12 γ12 isCom2_V2 isCom2_γ2 trn2 s2
          by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
        qed
      next
        case (Step1 obll1 obll ob1) note Step1O = Step1
        show ?thesis proof(cases "γ1 trn1")
          case True note γ1 = True
          hence g1: "g1 trn1 = ob1" and "obll1 = One.O tr1" using Step1 by auto
          hence obll: "compO (One.O tr1) (Two.O ?tr2) obll" using Step1 by auto
          have com1: "¬ isCom1 trn1" using Step1O γ1 g1 isCom1_isComO1 trn1 s1 by blast
          show ?thesis using trr2 vl s2(2) proof(cases rule: compV_cases_V)
            case Nil
            hence φ12: "¬ φ1 trn1 ∧ ¬ φ2 trn2" by auto
            hence vl: "compV (One.V tr1) (Two.V ?tr2) vl" using vl by auto
            from ConsCons.IH(2)[OF _ tr1 trr2 rs1' s2(2) vl obll]
            obtain trr where "validFrom (?s1, s2) trr" and "O trr = obll ∧ V trr = vl"
            by auto
            thus ?thesis using trn1 Step1O g1 φ12 γ1 trn1 s1 isCom1_isComO1
            by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
          next
            case (Step1 vll1 vll2 vll v1) note Step1V = Step1
            show ?thesis proof(cases "φ1 trn1")
              case False note φ1 = False
              hence vl: "compV (One.V tr1) (Two.V ?tr2) vl" using vl by auto
              from ConsCons.IH(2)[OF _ tr1 trr2 rs1' s2(2) vl obll]
              obtain trr where "validFrom (?s1, s2) trr" and "O trr = obll ∧ V trr = vl"
              by auto
              thus ?thesis using trn1 Step1O g1 φ1 γ1 trn1 s1 isCom1_isComO1
              by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
            next
              case True note φ1 = True
              hence f1: "f1 trn1 = v1" and "vll1 = One.V tr1" using Step1V by auto
              hence vll: "compV (One.V tr1) (Two.V ?tr2) vll" using Step1V com1 by auto
              from ConsCons.IH(2)[OF _ tr1 trr2 rs1' s2(2) vll obll]
              obtain trr where "validFrom (?s1, s2) trr" and "O trr = obll ∧ V trr = vll"
              by auto
              thus ?thesis using trn1 Step1O Step1V f1 φ1 g1 φ1 γ1 trn1 s1 isCom1_isComO1
              by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
            qed
          next
            case (Com vll1 vll2 vll v1 v2)
            hence φ1: "¬ φ1 trn1" using com1 isCom1_isComV1[OF trn1] s1 by auto
            hence vl: "compV (One.V tr1) (Two.V ?tr2) vl" using vl by auto
            from ConsCons.IH(2)[OF _ tr1 trr2 rs1' s2(2) vl obll]
            obtain trr where "validFrom (?s1, s2) trr" and "O trr = obll ∧ V trr = vl"
            by auto
            thus ?thesis using trn1 Step1O g1 φ1 γ1 trn1 s1 isCom1_isComO1
            by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
          qed
        next
          case False note γ1 = False
          hence obl: "compO (One.O tr1) (Two.O ?tr2) obl" using obl by simp
          hence φ1: "φ1 trn1" and com1: "¬ isCom1 trn1" using φγ1 γ1 isCom1_γ1 trn1 s1 by auto
          show ?thesis using trr2 vl s2(2) proof(cases rule: compV_cases_V)
            case Nil hence False using φ1 by auto
            thus ?thesis by simp
          next
            case Com hence False using φ1 com1 trn1 using isCom1_isComV1 s1 by auto
            thus ?thesis by simp
          next
            case (Step1 vll1 vll2 vll v1) note Step1V = Step1
            hence f1: "f1 trn1 = v1" and "vll1 = One.V tr1" using φ1 by auto
            hence vll: "compV (One.V tr1) (Two.V ?tr2) vll" using Step1V com1 by auto
            from ConsCons.IH(2)[OF _ tr1 trr2 rs1' s2(2) vll obl]
            obtain trr where "validFrom (?s1, s2) trr" and "O trr = obl ∧ V trr = vll"
            by auto
            thus ?thesis using trn1 Step1O Step1V f1 φ1 φ1 γ1 trn1 s1 isCom1_isComV1
            by(intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
          qed
        qed
      next
        case (Step2 obl2 obll ob2) note Step2O = Step2
        hence com2: "¬ isCom2 trn2" using isCom2_γ2[OF trn2] isCom2_isComO2[OF trn2] s2 by auto
        hence φ2: "¬ φ2 trn2" using isCom2_V2[OF trn2] s2 by auto
        hence vl: "compV (One.V ?tr1) (Two.V tr2) vl" using vl by simp
        have γ2: "γ2 trn2" using φγ2 φ2 by simp
        hence g2: "g2 trn2 = ob2" and "obl2 = Two.O tr2" using Step2 by auto
        hence obll: "compO (One.O ?tr1) (Two.O tr2) obll" using Step2 by auto
        from ConsCons.IH(3)[OF _ trr1 tr2 s1(2) rs2' vl obll]
        obtain trr where "validFrom (s1, ?s2) trr" and "O trr = obll ∧ V trr = vl" by auto
        thus ?thesis using trn1 Step2O g2 φ2 γ2 trn2 s2 isCom2_isComO2
        by (intro exI[of _ "Trans2 s1 trn2 # trr"]) auto
      next
        case (Com obll1 obll2 obll ob1 ob2) note ComO = Com
        show ?thesis
        proof(cases "γ1 trn1")
          case True note γ1 = True
          hence com1: "isCom1 trn1" using isCom1_isComO1[OF trn1] s1 ComO by auto
          show ?thesis proof(cases "γ2 trn2")
            case True note γ2 = True
            hence com2: "isCom2 trn2" using isCom2_isComO2[OF trn2] s2 ComO by auto
            have obll: "compO (One.O tr1) (Two.O tr2) obll" using obl ComO γ1 γ2 by auto
            have g1: "g1 trn1 = ob1" and "obll1 = One.O tr1" and
                 g2: "g2 trn2 = ob2" and "obll2 = Two.O tr2"
            using γ1 γ2 ComO by auto
            have rs1: "One.reach (srcOf1 trn1)" and rs2: "Two.reach (srcOf2 trn2)"
              using s1 s2 by auto
            have sync: "sync trn1 trn2" proof(rule sync_φ_γ[OF trn1 rs1 trn2 rs2 com1 com2])
              show "syncO (g1 trn1) (g2 trn2)" using Com γ1 γ2 by auto
            next
              assume φ12: "φ1 trn1" "φ2 trn2"
              hence comV: "isComV1 (f1 trn1) ∧ isComV2 (f2 trn2)"
              using com1 com2 isCom1_isComV1 isCom2_isComV2 trn1 trn2 rs1 rs2 by blast
              show "syncV (f1 trn1) (f2 trn2)" using vl φ12 comV by cases auto
            qed(insert γ1 γ2, auto)
            show ?thesis
            proof(cases "φ1 trn1")
              case True
              hence φ12: "φ1 trn1 ∧ φ2 trn2" using sync_φ1_φ2[OF trn1 rs1 trn2 rs2 com1 com2 sync] by simp
              show ?thesis using trr2 vl s2(2) proof(cases rule: compV_cases_V)
                case Nil hence False using φ12 by auto
                thus ?thesis by simp
              next
                case Step1 hence False using φ12 com1 isCom1_isComV1[OF trn1] s1 by auto
                thus ?thesis by simp
              next
                case (Com vll1 vll2 vll v1 v2) note ComV = Com
                hence f1: "f1 trn1 = v1" and "vll1 = One.V tr1" and
                      f2: "f2 trn2 = v2" and "vll2 = Two.V tr2"
                using φ12 by auto
                hence vll: "compV (One.V tr1) (Two.V tr2) vll" using ComV com1 com2 φ12 by auto
                from ConsCons.IH(1)[OF tr1 tr2 rs1' rs2' vll obll]
                obtain trr where "validFrom (?s1, ?s2) trr" and "O trr = obll ∧ V trr = vll"
                by auto
                thus ?thesis using trn1 trn2 ComO ComV f1 f2 φ12 g1 g2 γ1 γ2 com1 com2 sync s1 s2
                by (intro exI[of _ "CTrans trn1 trn2 # trr"]) auto
              qed
            next
              case False
              hence φ12: "¬ φ1 trn1 ∧ ¬ φ2 trn2" using sync_φ1_φ2[OF trn1 rs1 trn2 rs2 com1 com2 sync] by simp
              hence vl: "compV (One.V tr1) (Two.V tr2) vl" using vl by simp
              from ConsCons.IH(1)[OF tr1 tr2 rs1' rs2' vl obll]
              obtain trr where "validFrom (?s1, ?s2) trr" and "O trr = obll ∧ V trr = vl" by auto
              thus ?thesis using trn1 trn2 ComO φ12 g1 g2 γ1 γ2 com1 com2 sync s1 s2
              by (intro exI[of _ "CTrans trn1 trn2 # trr"]) auto
            qed
          next
            case False
            hence φ2: "φ2 trn2" and com2: "¬ isCom2 trn2" using φγ2 isCom2_γ2 trn2 s2 by auto
            have False using trr2 vl s2(2) φ2 com2 isCom2_V2[OF trn2] s2 by (cases rule: compV_cases_V) auto
            thus ?thesis by simp
          qed
        next
          case False note γ1 = False
          hence obl: "compO (One.O tr1) (Two.O ?tr2) obl" using obl by simp
          have φ1: "φ1 trn1" and com1: "¬ isCom1 trn1" using γ1 φγ1 isCom1_γ1 trn1 s1 by auto
          show ?thesis using trr2 vl s2(2) proof(cases rule: compV_cases_V)
            case Nil hence False using φ1 by auto
            thus ?thesis by simp
          next
            case Com hence False using com1 φ1 isCom1_isComV1[OF trn1] s1 by auto
            thus ?thesis by simp
          next
            case (Step1 vll1 vll2 vll v1) note Step1V = Step1
            hence f1: "f1 trn1 = v1" and "vll1 = One.V tr1" using φ1 by auto
            hence vll: "compV (One.V tr1) (Two.V ?tr2) vll" using Step1V com1 by auto
            from ConsCons.IH(2)[OF _ tr1 trr2 rs1' s2(2) vll obl]
            obtain trr where "validFrom (?s1, s2) trr" and "O trr = obl ∧ V trr = vll"
            by auto
            thus ?thesis using trn1 Step1V f1 φ1 γ1 trn1 s1 isCom1_isComO1 com1
            by (intro exI[of _ "Trans1 s2 trn1 # trr"]) auto
          qed
        qed
      qed
    qed
  qed
qed




lemma pullback_O_V:
assumes "One.validFrom istate1 tr1" and "Two.validFrom istate2 tr2"
and "compV (One.V tr1) (Two.V tr2) vl"
and "compO (One.O tr1) (Two.O tr2) ol"
shows "∃tr. validFrom icstate tr ∧ O tr = ol ∧ V tr = vl"
using assms pullback_O_V_aux One.reach.Istate Two.reach.Istate unfolding icstate_def by auto

end (* context BD_Security_TS_Comp *)


sublocale BD_Security_TS_Comp ⊆ K? : Abstract_BD_Security_Comp where
  validSystemTraces1 = "One.validFrom istate1" and V1 = One.V and O1 = One.O
   and TT1 = "never T1" and B1 = B1 and
  validSystemTraces2 = "Two.validFrom istate2" and V2 = Two.V and O2 = Two.O
   and TT2 = "never T2" and B2 = B2 and
  validSystemTraces = "validFrom icstate" and V = V and O = O
   and TT = "never T" and B = B and
   comp = comp and compO = compO and compV = compV
  apply standard
  subgoal using validFrom by fastforce
  subgoal using compV by fastforce
  subgoal using compO by fastforce
  subgoal using T by fastforce
  subgoal using B by fastforce
  subgoal using pullback_O_V by fastforce
  done


context BD_Security_TS_Comp begin

(* Just contemplating the theorem provided as a
consequence of the sublocale inclusion: *)
theorem "secure1 ⟹ secure2 ⟹ secure"
using secure1_secure2_secure .

end (* context BD_Security_TS_Comp *)


end