Theory TypeSystem

theory TypeSystem
imports Language Compositionality
(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
header {* Type System for Ensuring SIFUM-Security of Commands *}

theory TypeSystem
imports Main Preliminaries Security Language Compositionality
begin

subsection {* Typing Rules *}

type_synonym Type = Sec

type_synonym 'Var TyEnv = "'Var \<rightharpoonup> Type"

(* We introduce a locale that instantiates the SIFUM-security property
  for the language from SIFUM_Lang.thy *)
locale sifum_types =
  sifum_lang evA evB + sifum_security dma Stop evalw
  for evA :: "('Var, 'Val) Mem => 'AExp => 'Val"
  and evB :: "('Var, 'Val) Mem => 'BExp => bool"

context sifum_types
begin

(* Redefined since Isabelle does not seem to be able to reuse the abbreviation from the old locale *)
abbreviation mm_equiv_abv2 :: "(_, _, _) LocalConf => (_, _, _) LocalConf => bool"
(infix "≈" 60)
  where "mm_equiv_abv2 c c' ≡ mm_equiv_abv c c'"

abbreviation eval_abv2 :: "(_, 'Var, 'Val) LocalConf => (_, _, _) LocalConf => bool"
  (infixl "\<leadsto>" 70)
  where
  "x \<leadsto> y ≡ (x, y) ∈ evalw"

abbreviation low_indistinguishable_abv :: "'Var Mds => ('Var, 'AExp, 'BExp) Stmt => (_, _, _) Stmt => bool"
  ("_ ∼\<index> _" [100, 100] 80)
  where
  "c ∼mds c' ≡ low_indistinguishable mds c c'"


definition to_total :: "'Var TyEnv => 'Var => Sec"
where "to_total Γ v ≡ if v ∈ dom Γ then the (Γ v) else dma v"

definition max_dom :: "Sec set => Sec"
  where "max_dom xs ≡ if High ∈ xs then High else Low"

inductive type_aexpr :: "'Var TyEnv => 'AExp => Type => bool" ("_ \<turnstile>a _ ∈ _" [120, 120, 120] 1000)
  where
  type_aexpr [intro!]: "Γ \<turnstile>a e ∈ max_dom (image (λ x. to_total Γ x) (aexp_vars e))"

inductive_cases type_aexpr_elim [elim]: "Γ \<turnstile>a e ∈ t"

inductive type_bexpr :: "'Var TyEnv => 'BExp => Type => bool" ("_ \<turnstile>b _ ∈ _ " [120, 120, 120] 1000)
  where
  type_bexpr [intro!]: "Γ \<turnstile>b e ∈ max_dom (image (λ x. to_total Γ x) (bexp_vars e))"

inductive_cases type_bexpr_elim [elim]: "Γ \<turnstile>b e ∈ t"

definition mds_consistent :: "'Var Mds => 'Var TyEnv => bool"
  where "mds_consistent mds Γ ≡
    dom Γ = {(x :: 'Var). (dma x = Low ∧ x ∈ mds AsmNoRead) ∨
                          (dma x = High ∧ x ∈ mds AsmNoWrite)}"

fun add_anno_dom :: "'Var TyEnv => 'Var ModeUpd => 'Var set"
  where
  "add_anno_dom Γ (Acq v AsmNoRead) = (if dma v = Low then dom Γ ∪ {v} else dom Γ)" |
  "add_anno_dom Γ (Acq v AsmNoWrite) = (if dma v = High then dom Γ ∪ {v} else dom Γ)" |
  "add_anno_dom Γ (Acq v _) = dom Γ" |
  "add_anno_dom Γ (Rel v AsmNoRead) = (if dma v = Low then dom Γ - {v} else dom Γ)" |
  "add_anno_dom Γ (Rel v AsmNoWrite) = (if dma v = High then dom Γ - {v} else dom Γ)" |
  "add_anno_dom Γ (Rel v _) = dom Γ"

definition add_anno :: "'Var TyEnv => 'Var ModeUpd => 'Var TyEnv" (infix "⊕" 60)
  where
  "Γ ⊕ upd = ((λx. Some (to_total Γ x)) |` add_anno_dom Γ upd)"

definition context_le :: "'Var TyEnv => 'Var TyEnv => bool" (infixr "\<sqsubseteq>c" 100)
  where
  "Γ \<sqsubseteq>c Γ' ≡ (dom Γ = dom Γ') ∧ (∀ x ∈ dom Γ. the (Γ x) \<sqsubseteq> the (Γ' x))"

inductive has_type :: "'Var TyEnv => ('Var, 'AExp, 'BExp) Stmt => 'Var TyEnv => bool"
  ("\<turnstile> _ {_} _" [120, 120, 120] 1000)
  where
  stop_type [intro]: "\<turnstile> Γ {Stop} Γ" |
  skip_type [intro] : "\<turnstile> Γ {Skip} Γ" |
  assign1 : "[| x ∉ dom Γ ; Γ \<turnstile>a e ∈ t; t \<sqsubseteq> dma x |] ==> \<turnstile> Γ {x \<leftarrow> e} Γ" |
  assign2 : "[| x ∈ dom Γ ; Γ \<turnstile>a e ∈ t |] ==> has_type Γ (x \<leftarrow> e) (Γ (x := Some t))" |
  if_type [intro]: "[| Γ \<turnstile>b e ∈ High --> 
    ((∀ mds. mds_consistent mds Γ --> (low_indistinguishable mds c1 c2)) ∧
     (∀ x ∈ dom Γ'. Γ' x = Some High))
             ; \<turnstile> Γ { c1 } Γ'
             ; \<turnstile> Γ { c2 } Γ' |] ==>
             \<turnstile> Γ { If e c1 c2 } Γ'" |
  while_type [intro]: "[| Γ \<turnstile>b e ∈ Low ; \<turnstile> Γ { c } Γ |] ==> \<turnstile> Γ { While e c } Γ" |
  anno_type [intro]: "[| Γ' = Γ ⊕ upd ; \<turnstile> Γ' { c } Γ'' ; c ≠ Stop ;
                 ∀ x. to_total Γ x \<sqsubseteq> to_total Γ' x |] ==> \<turnstile> Γ { c@[upd] } Γ''" |
  seq_type [intro]: "[| \<turnstile> Γ { c1 } Γ' ; \<turnstile> Γ' { c2 } Γ'' |] ==> \<turnstile> Γ { c1 ;; c2 } Γ''" |
  sub : "[| \<turnstile> Γ1 { c } Γ1' ; Γ2 \<sqsubseteq>c Γ1 ; Γ1' \<sqsubseteq>c Γ2' |] ==> \<turnstile> Γ2 { c } Γ2'"

subsection {* Typing Soundness *}

text {* The following predicate is needed to exclude some pathological
  cases, that abuse the @{term Stop} command which is not allowed to
  occur in actual programs. *}

fun has_annotated_stop :: "('Var, 'AExp, 'BExp) Stmt => bool"
  where
  "has_annotated_stop (c@[_]) = (if c = Stop then True else has_annotated_stop c)" |
  "has_annotated_stop (Seq p q) = (has_annotated_stop p ∨ has_annotated_stop q)" |
  "has_annotated_stop (If _ p q) = (has_annotated_stop p ∨ has_annotated_stop q)" |
  "has_annotated_stop (While _ p) = has_annotated_stop p" |
  "has_annotated_stop _ = False"

inductive_cases has_type_elim: "\<turnstile> Γ { c } Γ'"
inductive_cases has_type_stop_elim: "\<turnstile> Γ { Stop } Γ'"

definition tyenv_eq :: "'Var TyEnv => ('Var, 'Val) Mem => ('Var, 'Val) Mem => bool"
  (infix "=\<index>" 60)
  where "mem1 =Γ mem2 ≡ ∀ x. (to_total Γ x = Low --> mem1 x = mem2 x)"

lemma tyenv_eq_sym: "mem1 =Γ mem2 ==> mem2 =Γ mem1"
  by (auto simp: tyenv_eq_def)


(* Parametrized relations for type soundness proof *)
inductive_set \<R>1 :: "'Var TyEnv => (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  and \<R>1_abv :: "'Var TyEnv =>
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf =>
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf =>
  bool" ("_ \<R>1\<index> _" [120, 120] 1000)
  for Γ' :: "'Var TyEnv"
  where
  "x \<R>1Γ y ≡ (x, y) ∈ \<R>1 Γ" |
  intro [intro!] : "[| \<turnstile> Γ { c } Γ' ; mds_consistent mds Γ ; mem1 =Γ mem2 |] ==> ⟨c, mds, mem1⟩ \<R>1Γ' ⟨c, mds, mem2⟩"

inductive_set \<R>2 :: "'Var TyEnv => (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  and \<R>2_abv :: "'Var TyEnv =>
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf =>
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf =>
  bool" ("_ \<R>2\<index> _" [120, 120] 1000)
  for Γ' :: "'Var TyEnv"
  where
  "x \<R>2Γ y ≡ (x, y) ∈ \<R>2 Γ" |
  intro [intro!] : "[| ⟨c1, mds, mem1⟩ ≈ ⟨c2, mds, mem2⟩ ;
                       ∀ x ∈ dom Γ'. Γ' x = Some High ;
                       \<turnstile> Γ1 { c1 } Γ' ; \<turnstile> Γ2 { c2 } Γ' ;
                       mds_consistent mds Γ1 ; mds_consistent mds Γ2 |] ==>
                     ⟨c1, mds, mem1⟩ \<R>2Γ' ⟨c2, mds, mem2⟩"

inductive \<R>3_aux :: "'Var TyEnv => (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf =>
                 (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf =>
                 bool" ("_ \<R>3\<index> _" [120, 120] 1000)
  and \<R>3 :: "'Var TyEnv => (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  where
  "\<R>3 Γ' ≡ {(lc1, lc2). \<R>3_aux Γ' lc1 lc2}" |
  intro1 [intro] : "[| ⟨c1, mds, mem1⟩ \<R>1Γ ⟨c2, mds, mem2⟩; \<turnstile> Γ { c } Γ' |] ==>
                      ⟨Seq c1 c, mds, mem1⟩ \<R>3Γ' ⟨Seq c2 c, mds, mem2⟩" |
  intro2 [intro] : "[| ⟨c1, mds, mem1⟩ \<R>2Γ ⟨c2, mds, mem2⟩; \<turnstile> Γ { c } Γ' |] ==>
                      ⟨Seq c1 c, mds, mem1⟩ \<R>3Γ' ⟨Seq c2 c, mds, mem2⟩" |
  intro3 [intro] : "[| ⟨c1, mds, mem1⟩ \<R>3Γ ⟨c2, mds, mem2⟩; \<turnstile> Γ { c } Γ' |] ==>
                      ⟨Seq c1 c, mds, mem1⟩ \<R>3Γ' ⟨Seq c2 c, mds, mem2⟩"

(* A weaker property than bisimulation to reason about the sub-relations of \<R>: *)
definition weak_bisim :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel =>
                        (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel => bool"
  where "weak_bisim \<T>1 \<T> ≡ ∀ c1 c2 mds mem1 mem2 c1' mds' mem1'.
  ((⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ \<T>1 ∧
   (⟨c1, mds, mem1⟩ \<leadsto> ⟨c1', mds', mem1'⟩)) -->
  (∃ c2' mem2'. ⟨c2, mds, mem2⟩ \<leadsto> ⟨c2', mds', mem2'⟩ ∧ 
                (⟨c1', mds', mem1'⟩, ⟨c2', mds', mem2'⟩) ∈ \<T>)"

inductive_set \<R> :: "'Var TyEnv =>
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  and \<R>_abv :: "'Var TyEnv =>
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf =>
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf =>
  bool" ("_ \<R>u\<index> _" [120, 120] 1000)
  for Γ :: "'Var TyEnv"
  where
  "x \<R>uΓ y ≡ (x, y) ∈ \<R> Γ" |
  intro1: "lc \<R>1Γ lc' ==> (lc, lc') ∈ \<R> Γ" |
  intro2: "lc \<R>2Γ lc' ==> (lc, lc') ∈ \<R> Γ" |
  intro3: "lc \<R>3Γ lc' ==> (lc, lc') ∈ \<R> Γ"

(* Some eliminators for the above relations *)
inductive_cases \<R>1_elim [elim]: "⟨c1, mds, mem1⟩ \<R>1Γ ⟨c2, mds, mem2⟩"
inductive_cases \<R>2_elim [elim]: "⟨c1, mds, mem1⟩ \<R>2Γ ⟨c2, mds, mem2⟩"
inductive_cases \<R>3_elim [elim]: "⟨c1, mds, mem1⟩ \<R>3Γ ⟨c2, mds, mem2⟩"

inductive_cases \<R>_elim [elim]: "(⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ \<R> Γ"
inductive_cases \<R>_elim': "(⟨c1, mds, mem1⟩, ⟨c2, mds2, mem2⟩) ∈ \<R> Γ"
inductive_cases \<R>1_elim' : "⟨c1, mds, mem1⟩ \<R>1Γ ⟨c2, mds2, mem2⟩"
inductive_cases \<R>2_elim' : "⟨c1, mds, mem1⟩ \<R>2Γ ⟨c2, mds2, mem2⟩"
inductive_cases \<R>3_elim' : "⟨c1, mds, mem1⟩ \<R>3Γ ⟨c2, mds2, mem2⟩"

(* To prove that \<R> is a bisimulation, we first show symmetry *)

lemma \<R>1_sym: "sym (\<R>1 Γ)"
  unfolding sym_def
  apply auto
  by (metis (no_types) \<R>1.intro \<R>1_elim' tyenv_eq_sym)

lemma \<R>2_sym: "sym (\<R>2 Γ)"
  unfolding sym_def
  apply clarify
  by (metis (no_types) \<R>2.intro \<R>2_elim' mm_equiv_sym)

lemma \<R>3_sym: "sym (\<R>3 Γ)"
  unfolding sym_def
proof (clarify)
  fix c1 mds mem1 c2 mds' mem2
  assume asm: "⟨c1, mds, mem1⟩ \<R>3Γ ⟨c2, mds', mem2⟩"
  hence [simp]: "mds' = mds"
    using \<R>3_elim' by blast
  from asm show "⟨c2, mds', mem2⟩ \<R>3Γ ⟨c1, mds, mem1⟩"
    apply auto
    apply (induct rule: \<R>3_aux.induct)
      apply (metis (lifting) \<R>1_sym \<R>3_aux.intro1 symD)
     apply (metis (lifting) \<R>2_sym \<R>3_aux.intro2 symD)
    by (metis (lifting) \<R>3_aux.intro3)
qed

lemma \<R>_mds [simp]: "⟨c1, mds, mem1⟩ \<R>uΓ ⟨c2, mds', mem2⟩ ==> mds = mds'"
  apply (rule \<R>_elim')
     apply (auto)
    apply (metis \<R>1_elim')
   apply (metis \<R>2_elim')
  apply (insert \<R>3_elim')
  by blast

lemma \<R>_sym: "sym (\<R> Γ)"
  unfolding sym_def
proof (clarify)
  fix c1 mds mem1 c2 mds2 mem2
  assume asm: "(⟨c1, mds, mem1⟩, ⟨c2, mds2, mem2⟩) ∈ \<R> Γ"
  with \<R>_mds have [simp]: "mds2 = mds"
    by blast
  from asm show "(⟨c2, mds2, mem2⟩, ⟨c1, mds, mem1⟩) ∈ \<R> Γ"
    using \<R>.intro1 [of Γ] and \<R>.intro2 [of Γ] and \<R>.intro3 [of Γ]
    using \<R>1_sym [of Γ] and \<R>2_sym [of Γ] and \<R>3_sym [of Γ]
    apply simp
    apply (erule \<R>_elim)
      by (auto simp: sym_def)
qed

(* Next, we show that the relations are closed under globally consistent changes *)

lemma \<R>1_closed_glob_consistent: "closed_glob_consistent (\<R>1 Γ')"
  unfolding closed_glob_consistent_def
proof (clarify)
  fix c1 mds mem1 c2 mem2 x Γ'
  assume R1: "⟨c1, mds, mem1⟩ \<R>1Γ' ⟨c2, mds, mem2⟩"
  hence [simp]: "c2 = c1" by blast
  from R1 obtain Γ where Γ_props: "\<turnstile> Γ { c1 } Γ'" "mem1 =Γ mem2" "mds_consistent mds Γ"
    by blast
  hence "!! v. ⟨c1, mds, mem1 (x := v)⟩ \<R>1Γ' ⟨c2, mds, mem2 (x := v)⟩"
    by (auto simp: tyenv_eq_def mds_consistent_def)
  moreover
  from Γ_props have "!! v1 v2. [| dma x = High ; x ∉ mds AsmNoWrite |] ==>
    ⟨c1, mds, mem1(x := v1)⟩ \<R>1Γ' ⟨c2, mds, mem2(x := v2)⟩"
    apply (auto simp: mds_consistent_def tyenv_eq_def)
    by (metis (lifting, full_types) Sec.simps(2) mem_Collect_eq to_total_def)
  ultimately show
    "(dma x = High ∧ x ∉ mds AsmNoWrite -->
      (∀v1 v2. ⟨c1, mds, mem1(x := v1)⟩ \<R>1Γ' ⟨c2, mds, mem2(x := v2)⟩))
     ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite -->
      (∀v. ⟨c1, mds, mem1(x := v)⟩ \<R>1Γ' ⟨c2, mds, mem2(x := v)⟩))"
    using intro1
    by auto
qed

lemma \<R>2_closed_glob_consistent: "closed_glob_consistent (\<R>2 Γ')"
  unfolding closed_glob_consistent_def
proof (clarify)
  fix c1 mds mem1 c2 mem2 x Γ'
  assume R2: "⟨c1, mds, mem1⟩ \<R>2Γ' ⟨c2, mds, mem2⟩"
  then obtain Γ1 Γ2 where Γ_prop: "\<turnstile> Γ1 { c1 } Γ'" "\<turnstile> Γ2 { c2 } Γ'"
    "mds_consistent mds Γ1" "mds_consistent mds Γ2"
    by blast
  from R2 have bisim: "⟨c1, mds, mem1⟩ ≈ ⟨c2, mds, mem2⟩"
    by blast
  then obtain \<R>' where \<R>'_prop: "(⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ \<R>' ∧ strong_low_bisim_mm \<R>'"
    apply (rule mm_equiv_elim)
    by (auto simp: strong_low_bisim_mm_def)
  from \<R>'_prop have \<R>'_cons: "closed_glob_consistent \<R>'"
    by (auto simp: strong_low_bisim_mm_def)
  moreover
  from Γ_prop and \<R>'_prop
  have "!!mem1 mem2. (⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ \<R>' ==> ⟨c1, mds, mem1⟩ \<R>2Γ' ⟨c2, mds, mem2⟩"
    using \<R>2.intro [where Γ' = Γ' and Γ1 = Γ1 and Γ2 = Γ2]
    using mm_equiv_intro and R2
    by blast
  ultimately show
    "(dma x = High ∧ x ∉ mds AsmNoWrite -->
      (∀v1 v2. ⟨c1, mds, mem1(x := v1)⟩ \<R>2Γ' ⟨c2, mds, mem2(x := v2)⟩))
     ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite -->
      (∀v. ⟨c1, mds, mem1(x := v)⟩ \<R>2Γ' ⟨c2, mds, mem2(x := v)⟩))"
    using \<R>'_prop
    unfolding closed_glob_consistent_def
    by simp
qed

(* A predicate like this seems to be necessary to make induct generate
    the correct goal in the following lemma. Without it, it somehow does
    not "unify" the local configuration components in the goal and the assumptions. *)
fun closed_glob_helper :: "'Var TyEnv => (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf => (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf => bool"
  where
  "closed_glob_helper Γ' ⟨c1, mds, mem1⟩ ⟨c2, mds2, mem2⟩ =
  (∀ x. ((dma x = High ∧ x ∉ mds AsmNoWrite) -->
           (∀ v1 v2. (⟨ c1, mds, mem1 (x := v1) ⟩, ⟨ c2, mds, mem2 (x := v2) ⟩) ∈ \<R>3 Γ')) ∧
         ((dma x = Low ∧ x ∉ mds AsmNoWrite) -->
           (∀ v. (⟨ c1, mds, mem1 (x := v) ⟩, ⟨ c2, mds, mem2 (x := v) ⟩) ∈ \<R>3 Γ')))"

lemma \<R>3_closed_glob_consistent:
  assumes R3: "⟨c1, mds, mem1⟩ \<R>3Γ' ⟨c2, mds, mem2⟩"
  shows "∀ x.
    (dma x = High ∧ x ∉ mds AsmNoWrite -->
        (∀v1 v2. (⟨c1, mds, mem1(x := v1)⟩, ⟨c2, mds, mem2(x := v2)⟩) ∈ \<R>3 Γ')) ∧
       (dma x = Low ∧ x ∉ mds AsmNoWrite --> (∀v. (⟨c1, mds, mem1(x := v)⟩, ⟨c2, mds, mem2(x := v)⟩) ∈ \<R>3 Γ'))"
proof -
  from R3 have "closed_glob_helper Γ' ⟨c1, mds, mem1⟩ ⟨c2, mds, mem2⟩"
  proof (induct rule: \<R>3_aux.induct)
    case (intro1 Γ c1 mds mem1 c2 mem2 c Γ')
    thus ?case
      using \<R>1_closed_glob_consistent [of Γ] and \<R>3_aux.intro1
      unfolding closed_glob_consistent_def
      by (simp, blast)
  next
    case (intro2 Γ c1 mds mem1 c2 mem2 c Γ')
    thus ?case
      using \<R>2_closed_glob_consistent [of Γ] and \<R>3_aux.intro2
      unfolding closed_glob_consistent_def
      by (simp, blast)
  next
    case intro3
    thus ?case
      using \<R>3_aux.intro3
      by (simp, blast)
  qed
  thus ?thesis by simp
qed

lemma \<R>_closed_glob_consistent: "closed_glob_consistent (\<R> Γ')"
  unfolding closed_glob_consistent_def
proof (clarify, erule \<R>_elim, simp_all)
  fix c1 mds mem1 c2 mem2 x
  assume R1: "⟨c1, mds, mem1⟩ \<R>1Γ' ⟨c2, mds, mem2⟩"
  with \<R>1_closed_glob_consistent show
    "(dma x = High ∧ x ∉ mds AsmNoWrite -->
        (∀v1 v2. (⟨c1, mds, mem1(x := v1)⟩, ⟨c2, mds, mem2(x := v2)⟩) ∈ \<R> Γ')) ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite -->
        (∀v. (⟨c1, mds, mem1(x := v)⟩, ⟨c2, mds, mem2(x := v)⟩) ∈ \<R> Γ'))"
    unfolding closed_glob_consistent_def
    using intro1
    apply clarify
    by metis
next
  fix c1 mds mem1 c2 mem2 x
  assume R2: "⟨c1, mds, mem1⟩ \<R>2Γ' ⟨c2, mds, mem2⟩"
  with \<R>2_closed_glob_consistent show
    "(dma x = High ∧ x ∉ mds AsmNoWrite -->
      (∀v1 v2. (⟨c1, mds, mem1(x := v1)⟩, ⟨c2, mds, mem2(x := v2)⟩) ∈ \<R> Γ'))
     ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite -->
      (∀v. (⟨c1, mds, mem1(x := v)⟩, ⟨c2, mds, mem2(x := v)⟩) ∈ \<R> Γ'))"
    unfolding closed_glob_consistent_def
    using intro2
    apply clarify
    by metis
next
  fix c1 mds mem1 c2 mem2 x Γ'
  assume R3: "⟨c1, mds, mem1⟩ \<R>3Γ' ⟨c2, mds, mem2⟩"
  thus
    "(dma x = High ∧ x ∉ mds AsmNoWrite -->
       (∀v1 v2. (⟨c1, mds, mem1(x := v1)⟩, ⟨c2, mds, mem2(x := v2)⟩) ∈ \<R> Γ'))
     ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite -->
       (∀v. (⟨c1, mds, mem1(x := v)⟩, ⟨c2, mds, mem2(x := v)⟩) ∈ \<R> Γ'))"
    using \<R>3_closed_glob_consistent
    apply auto
     apply (metis \<R>.intro3)
    by (metis (lifting) \<R>.intro3)
qed

(* It now remains to show that steps of the first of two related configurations
    can be matched by the second: *)

(* Some technical lemmas: *)
lemma type_low_vars_low:
  assumes typed: "Γ \<turnstile>a e ∈ Low"
  assumes mds_cons: "mds_consistent mds Γ"
  assumes x_in_vars: "x ∈ aexp_vars e"
  shows "to_total Γ x = Low"
  using assms
  by (metis (full_types) Sec.exhaust imageI max_dom_def type_aexpr_elim)

lemma type_low_vars_low_b:
  assumes typed : "Γ \<turnstile>b e ∈ Low"
  assumes mds_cons: "mds_consistent mds Γ"
  assumes x_in_vars: "x ∈ bexp_vars e"
  shows "to_total Γ x = Low"
  using assms
  by (metis (full_types) Sec.exhaust imageI max_dom_def type_bexpr.simps)

lemma mode_update_add_anno:
  "mds_consistent mds Γ ==> mds_consistent (update_modes upd mds) (Γ ⊕ upd)"
  apply (induct arbitrary: Γ rule: add_anno_dom.induct)
  by (auto simp: add_anno_def mds_consistent_def)

lemma context_le_trans: "[| Γ \<sqsubseteq>c Γ' ; Γ' \<sqsubseteq>c Γ'' |] ==> Γ \<sqsubseteq>c Γ''"
  apply (auto simp: context_le_def)
  by (metis domI order_trans the.simps)

lemma context_le_refl [simp]: "Γ \<sqsubseteq>c Γ"
  by (metis context_le_def order_refl)

(* Strangely, using only \<turnstile> Γ { Stop } Γ' as assumption does not work *)
lemma stop_cxt :
  "[| \<turnstile> Γ { c } Γ' ; c = Stop |] ==> Γ \<sqsubseteq>c Γ'"
  apply (induct rule: has_type.induct)
          apply auto
  by (metis context_le_trans)

(* First we show that (roughly) typeability is preserved by evaluation steps *)
lemma preservation:
  assumes typed: "\<turnstile> Γ { c } Γ'"
  assumes eval: "⟨c, mds, mem⟩ \<leadsto> ⟨c', mds', mem'⟩"
  shows "∃ Γ''. (\<turnstile> Γ'' { c' } Γ') ∧ (mds_consistent mds Γ --> mds_consistent mds' Γ'')"
  using typed eval
proof (induct arbitrary: c' mds rule: has_type.induct)
  case (anno_type Γ'' Γ upd c1 Γ')
  hence "⟨c1, update_modes upd mds, mem⟩ \<leadsto> ⟨c', mds', mem'⟩"
    by (metis upd_elim)
  with anno_type(3) obtain Γ''' where
    "\<turnstile> Γ''' { c' } Γ' ∧ (mds_consistent (update_modes upd mds) Γ'' -->
                          mds_consistent mds' Γ''')"
    by auto
  moreover
  have "mds_consistent mds Γ --> mds_consistent (update_modes upd mds) Γ''"
    using anno_type
    apply auto
    by (metis mode_update_add_anno)
  ultimately show ?case
    by blast
next
  case stop_type
  with stop_no_eval show ?case ..
next
  case skip_type
  hence "c' = Stop ∧ mds' = mds"
    by (metis skip_elim)
  thus ?case
    by (metis stop_type)
next
  case (assign1 x Γ e t c' mds)
  hence "c' = Stop ∧ mds' = mds"
    by (metis assign_elim)
  thus ?case
    by (metis stop_type)
next
  case (assign2 x Γ e t c' mds)
  hence "c' = Stop ∧ mds' = mds"
    by (metis assign_elim)
  thus ?case
    apply (rule_tac x = "Γ (x \<mapsto> t)" in exI)
    apply (auto simp: mds_consistent_def)
         apply (metis Sec.exhaust)
        apply (metis (lifting, full_types) CollectD domI local.assign2(1))
       apply (metis (lifting, full_types) CollectD domI local.assign2(1))
      apply (metis (lifting) CollectE domI local.assign2(1))
     apply (metis (lifting, full_types) domD mem_Collect_eq)
    by (metis (lifting, full_types) domD mem_Collect_eq)
next
  case (if_type Γ e th el Γ' c' mds)
  thus ?case
    apply (rule_tac x = Γ in exI)
    by force
next
  case (while_type Γ e c c' mds)
  hence [simp]: "mds' = mds ∧ c' = If e (c ;; While e c) Stop"
    by (metis while_elim)
  thus ?case
    apply (rule_tac x = Γ in exI)
    apply auto
    by (metis Sec.simps(2) has_type.while_type if_type local.while_type(1) local.while_type(2) seq_type stop_type type_bexpr_elim)
next
  case (seq_type Γ c1 Γ1 c2 Γ2 c' mds)
  thus ?case
  proof (cases "c1 = Stop")
    assume [simp]: "c1 = Stop"
    with seq_type have [simp]: "mds' = mds ∧ c' = c2"
      by (metis seq_stop_elim)
    thus ?case
      apply auto
      by (metis (lifting) `c1 = Stop` context_le_refl local.seq_type(1) local.seq_type(3) stop_cxt sub)
  next
    assume "c1 ≠ Stop"
    then obtain c1' where "⟨c1, mds, mem⟩ \<leadsto> ⟨c1', mds', mem'⟩ ∧ c' = (c1' ;; c2)"
      by (metis seq_elim seq_type.prems)
    then obtain Γ''' where "\<turnstile> Γ''' {c1'} Γ1 ∧
      (mds_consistent mds Γ --> mds_consistent mds' Γ''')"
      using seq_type(2)
      by auto
    moreover
    from seq_type have "\<turnstile> Γ1 { c2 } Γ2" by auto
    moreover
    ultimately show ?case
      apply (rule_tac x = Γ''' in exI)
      by (metis (lifting) `⟨c1, mds, mem⟩ \<leadsto> ⟨c1', mds', mem'⟩ ∧ c' = c1' ;; c2` has_type.seq_type)
  qed
next
  case (sub Γ1 c Γ1' Γ2 Γ2' c' mds)
  then obtain Γ'' where "\<turnstile> Γ'' { c' } Γ1' ∧
    (mds_consistent mds Γ1 --> mds_consistent mds' Γ'')"
    by auto
  thus ?case
    apply (rule_tac x = Γ'' in exI)
    apply (rule conjI)
     apply (metis (lifting) has_type.sub local.sub(4) stop_cxt stop_type)
    apply (simp add: mds_consistent_def)
    by (metis context_le_def sub.hyps(3))
qed

lemma \<R>1_mem_eq: "⟨c1, mds, mem1⟩ \<R>1Γ' ⟨c2, mds, mem2⟩ ==> mem1 =mdsl mem2"
  apply (rule \<R>1_elim)
   apply (auto simp: tyenv_eq_def mds_consistent_def to_total_def)
  by (metis (lifting) Sec.simps(1) low_mds_eq_def)

lemma \<R>2_mem_eq: "⟨c1, mds, mem1⟩ \<R>2Γ' ⟨c2, mds, mem2⟩ ==> mem1 =mdsl mem2"
  apply (rule \<R>2_elim)
  by (auto simp: mm_equiv_elim strong_low_bisim_mm_def)

fun bisim_helper :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf =>
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf => bool"
  where
  "bisim_helper ⟨c1, mds, mem1⟩ ⟨c2, mds2, mem2⟩ = mem1 =mdsl mem2"

lemma \<R>3_mem_eq: "⟨c1, mds, mem1⟩ \<R>3Γ' ⟨c2, mds, mem2⟩ ==> mem1 =mdsl mem2"
  apply (subgoal_tac "bisim_helper ⟨c1, mds, mem1⟩ ⟨c2, mds, mem2⟩")
   apply simp
  apply (induct rule: \<R>3_aux.induct)
  by (auto simp: \<R>1_mem_eq \<R>2_mem_eq)

(* \<R>2 is a full bisimulation so we can show the stronger step statement here: *)

lemma \<R>2_bisim_step:
  assumes case2: "⟨c1, mds, mem1⟩ \<R>2Γ' ⟨c2, mds, mem2⟩"
  assumes eval: "⟨c1, mds, mem1⟩ \<leadsto> ⟨c1', mds', mem1'⟩"
  shows "∃ c2' mem2'. ⟨c2, mds, mem2⟩ \<leadsto> ⟨c2', mds', mem2'⟩ ∧ ⟨c1', mds', mem1'⟩ \<R>2Γ' ⟨c2', mds', mem2'⟩"
proof -
  from case2 have aux: "⟨c1, mds, mem1⟩ ≈ ⟨c2, mds, mem2⟩" "∀ x ∈ dom Γ'. Γ' x = Some High"
    by (rule \<R>2_elim, auto)
  with eval obtain c2' mem2' where c2'_props:
    "⟨c2, mds, mem2⟩ \<leadsto> ⟨c2', mds', mem2'⟩ ∧
     ⟨c1', mds', mem1'⟩ ≈ ⟨c2', mds', mem2'⟩"
    using mm_equiv_strong_low_bisim strong_low_bisim_mm_def
    by metis
  (* with aux(1) obtain \<R>' where \<R>'_props: "(⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ \<R>'" "strong_low_bisim_mm \<R>'" *)
    (* using mm_equiv_elim *)
    (* by auto *)
  from case2 obtain Γ1 Γ2 where "\<turnstile> Γ1 { c1 } Γ'" "\<turnstile> Γ2 { c2 } Γ'"
    "mds_consistent mds Γ1" "mds_consistent mds Γ2"
    by (metis \<R>2_elim')
  with preservation and c2'_props obtain Γ1' Γ2' where
    "\<turnstile> Γ1' {c1'} Γ'" "mds_consistent mds' Γ1'"
    "\<turnstile> Γ2' {c2'} Γ'" "mds_consistent mds' Γ2'"
    using eval
    by metis
  with c2'_props show ?thesis
    using \<R>2.intro aux(2) c2'_props
    by blast
qed

(* To achieve more "symmetry" later, we prove a property analogous to the ones
    for \<R>1 and \<R>3 which are not, by themselves, bisimulations. *)

lemma \<R>2_weak_bisim:
  "weak_bisim (\<R>2 Γ') (\<R> Γ')"
  unfolding weak_bisim_def
  using \<R>.intro2
  apply auto
  by (metis \<R>2_bisim_step)


(* Not actually needed, but an interesting "asymmetry" since
    \<R>1 and \<R>3 aren't bisimulations. *)
lemma \<R>2_bisim: "strong_low_bisim_mm (\<R>2 Γ')"
  unfolding strong_low_bisim_mm_def
  by (auto simp: \<R>2_sym \<R>2_closed_glob_consistent \<R>2_mem_eq \<R>2_bisim_step)

lemma annotated_no_stop: "[| ¬ has_annotated_stop (c@[upd]) |] ==> ¬ has_annotated_stop c"
  apply (cases c)
  by auto

lemma typed_no_annotated_stop:
  "[| \<turnstile> Γ { c } Γ' |] ==> ¬ has_annotated_stop c"
  by (induct rule: has_type.induct, auto)

lemma not_stop_eval:
  "[| c ≠ Stop ; ¬ has_annotated_stop c |] ==>
  ∀ mds mem. ∃ c' mds' mem'. ⟨c, mds, mem⟩ \<leadsto> ⟨c', mds', mem'⟩"
proof (induct)
  case (Assign x exp)
  thus ?case
    by (metis cxt_to_stmt.simps(1) evalw_simplep.assign evalwp.unannotated evalwp_evalw_eq)
next
  case Skip
  thus ?case
    by (metis cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.skip)
next
  case (ModeDecl c mu)
  hence "¬ has_annotated_stop c ∧ c ≠ Stop"
    by (metis has_annotated_stop.simps(1))
  with ModeDecl show ?case
    apply (clarify, rename_tac mds mem)
    apply simp
    apply (erule_tac x = "update_modes mu mds" in allE)
    apply (erule_tac x = mem in allE)
    apply (erule exE)+
    by (metis cxt_to_stmt.simps(1) evalw.decl)
next
  case (Seq c1 c2)
  thus ?case
  proof (cases "c1 = Stop")
    assume "c1 = Stop"
    thus ?case
      by (metis cxt_to_stmt.simps(1) evalw_simplep.seq_stop evalwp.unannotated evalwp_evalw_eq)
  next
    assume "c1 ≠ Stop"
    with Seq show ?case
      by (metis evalw.seq has_annotated_stop.simps(2))
  qed
next
  case (If bexp c1 c2)
  thus ?case
    apply (clarify, rename_tac mds mem)
    apply (case_tac "evB mem bexp")
     apply (metis cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.if_true)
    by (metis cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.if_false)
next
  case (While bexp c)
  thus ?case
    by (metis cxt_to_stmt.simps(1) evalw_simplep.while evalwp.unannotated evalwp_evalw_eq)
next
  case Stop
  thus ?case by blast
qed

lemma stop_bisim:
  assumes bisim: "⟨Stop, mds, mem1⟩ ≈ ⟨c, mds, mem2⟩"
  assumes typeable: "\<turnstile> Γ { c } Γ'"
  shows "c = Stop"
proof (rule ccontr)
  let ?lc1 = "⟨Stop, mds, mem1⟩" and
      ?lc2 = "⟨c, mds, mem2⟩"
  assume "c ≠ Stop"
  from typeable have "¬ has_annotated_stop c"
    by (metis typed_no_annotated_stop)
  with `c ≠ Stop` obtain c' mds' mem2' where "?lc2 \<leadsto> ⟨c', mds', mem2'⟩"
    using not_stop_eval
    by blast
  moreover
  from bisim have "?lc2 ≈ ?lc1"
    by (metis mm_equiv_sym)
  ultimately obtain c1' mds1' mem1'
    where "⟨Stop, mds, mem1⟩ \<leadsto> ⟨c1', mds1', mem1'⟩"
    using mm_equiv_strong_low_bisim
    unfolding strong_low_bisim_mm_def
    by blast
  thus False
    by (metis (lifting) stop_no_eval)
qed

(* This is the main part of the proof and used in \<R>1_weak_bisim: *)

lemma \<R>_typed_step:
  "[| \<turnstile> Γ { c1 } Γ' ;
     mds_consistent mds Γ ;
     mem1 =Γ mem2 ;
     ⟨c1, mds, mem1⟩ \<leadsto> ⟨c1', mds', mem1'⟩ |] ==>
   (∃ c2' mem2'. ⟨c1, mds, mem2⟩ \<leadsto> ⟨c2', mds', mem2'⟩ ∧
                 ⟨c1', mds', mem1'⟩ \<R>uΓ' ⟨c2', mds', mem2'⟩)"
proof (induct arbitrary: mds c1' rule: has_type.induct)
  case (seq_type Γ c1 Γ'' c2 Γ' mds)
  show ?case
  proof (cases "c1 = Stop")
    assume "c1 = Stop"
    hence [simp]: "c1' = c2" "mds' = mds" "mem1' = mem1"
      using seq_type
      by (auto simp: seq_stop_elim)
    from seq_type `c1 = Stop` have "Γ \<sqsubseteq>c Γ''"
      by (metis stop_cxt)
    hence "\<turnstile> Γ { c2 } Γ'"
      by (metis context_le_refl local.seq_type(3) sub)
    have "⟨c2, mds, mem1⟩ \<R>1Γ' ⟨c2, mds, mem2⟩"
      apply (rule \<R>1.intro [of Γ])
      by (auto simp: seq_type `\<turnstile> Γ { c2 } Γ'`)
    thus ?case
      using \<R>.intro1
      apply clarify
      apply (rule_tac x = c2 in exI)
      apply (rule_tac x = mem2 in exI)
      apply (auto simp: `c1 = Stop`)
      by (metis cxt_to_stmt.simps(1) evalw_simplep.seq_stop evalwp.unannotated evalwp_evalw_eq)
  next
    assume "c1 ≠ Stop"
    with `⟨c1 ;; c2, mds, mem1⟩ \<leadsto> ⟨c1', mds', mem1'⟩` obtain c1'' where c1''_props:
      "⟨c1, mds, mem1⟩ \<leadsto> ⟨c1'', mds', mem1'⟩ ∧ c1' = c1'' ;; c2"
      by (metis seq_elim)
    with seq_type(2) obtain c2'' mem2' where c2''_props:
      "⟨c1, mds, mem2⟩ \<leadsto> ⟨c2'', mds', mem2'⟩ ∧ ⟨c1'', mds', mem1'⟩ \<R>uΓ'' ⟨c2'', mds', mem2'⟩"
      by (metis local.seq_type(5) local.seq_type(6))
    hence "⟨c1'' ;; c2, mds', mem1'⟩ \<R>uΓ' ⟨c2'' ;; c2, mds', mem2'⟩"
      apply (rule conjE)
      apply (erule \<R>_elim, auto)
        apply (metis \<R>.intro3 \<R>3_aux.intro1 local.seq_type(3))
       apply (metis \<R>.intro3 \<R>3_aux.intro2 local.seq_type(3))
      by (metis \<R>.intro3 \<R>3_aux.intro3 local.seq_type(3))
    moreover
    from c2''_props have "⟨c1 ;; c2, mds, mem2⟩ \<leadsto> ⟨c2'' ;; c2, mds', mem2'⟩"
      by (metis evalw.seq)
    ultimately show ?case
      by (metis c1''_props)
  qed
next
  case (anno_type Γ' Γ upd c Γ'' mds)
  have "mem1 =Γ' mem2"
    by (metis less_eq_Sec_def local.anno_type(5) local.anno_type(7) tyenv_eq_def)
  have "mds_consistent (update_modes upd mds) Γ'"
    by (metis (lifting) local.anno_type(1) local.anno_type(6) mode_update_add_anno)
  then obtain c2' mem2' where "(⟨c, update_modes upd mds, mem2⟩ \<leadsto> ⟨c2', mds', mem2'⟩ ∧
    ⟨c1', mds', mem1'⟩ \<R>uΓ'' ⟨c2', mds', mem2'⟩)"
    using anno_type
    apply auto
    by (metis `mem1 =Γ' mem2` local.anno_type(1) upd_elim)
  thus ?case
    apply (rule_tac x = c2' in exI)
    apply (rule_tac x = mem2' in exI)
    apply auto
    by (metis cxt_to_stmt.simps(1) evalw.decl)
next
  case stop_type
  with stop_no_eval show ?case by auto
next
  case (skip_type Γ mds)
  moreover
  with skip_type have [simp]: "mds' = mds" "c1' = Stop" "mem1' = mem1"
    using skip_elim
    by (metis, metis, metis)
  with skip_type have "⟨Stop, mds, mem1⟩ \<R>1Γ ⟨Stop, mds, mem2⟩"
    by auto
  thus ?case
    using \<R>.intro1 and unannotated [where c = Skip and E = "[]"]
    apply auto
    by (metis evalw_simple.skip)
next (* assign1 *)
  case (assign1 x Γ e t mds)
  hence [simp]: "c1' = Stop" "mds' = mds" "mem1' = mem1 (x := evA mem1 e)"
    using assign_elim
    by (auto, metis)
  have "mem1 (x := evA mem1 e) =Γ mem2 (x := evA mem2 e)"
  proof (cases "to_total Γ x")
    assume "to_total Γ x = High"
    thus ?thesis
      using assign1 tyenv_eq_def
      by auto
  next
    assume "to_total Γ x = Low"
    with assign1 have [simp]: "t = Low"
      by (metis less_eq_Sec_def to_total_def)
    hence "dma x = Low"
      using assign1 `to_total Γ x = Low`
      by (metis to_total_def)
    with assign1 have "∀ v ∈ aexp_vars e. to_total Γ v = Low"
      using type_low_vars_low
      by auto
    thus ?thesis
      using eval_vars_detA
      apply (auto simp: tyenv_eq_def)
       apply (metis (no_types) local.assign1(5) tyenv_eq_def)
      by (metis local.assign1(5) tyenv_eq_def)
  qed
  hence "⟨x \<leftarrow> e, mds, mem2⟩ \<leadsto> ⟨Stop, mds', mem2 (x := evA mem2 e)⟩"
    "⟨Stop, mds', mem1 (x := evA mem1 e)⟩ \<R>uΓ ⟨Stop, mds', mem2 (x := evA mem2 e)⟩"
    apply auto
     apply (metis cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.assign)
    by (rule \<R>.intro1, auto simp: assign1)
  thus ?case
    using `c1' = Stop` and `mem1' = mem1 (x := evA mem1 e)`
    by blast
next (* assign2 *)
  case (assign2 x Γ e t mds)
  hence [simp]: "c1' = Stop" "mds' = mds" "mem1' = mem1 (x := evA mem1 e)"
    using assign_elim assign2
    by (auto, metis)
  let ?Γ' = "Γ (x \<mapsto> t)"
  have "⟨x \<leftarrow> e, mds, mem2⟩ \<leadsto> ⟨Stop, mds, mem2 (x := evA mem2 e)⟩"
    using assign2
    by (metis cxt_to_stmt.simps(1) evalw_simplep.assign evalwp.unannotated evalwp_evalw_eq)
  moreover
  have "⟨Stop, mds, mem1 (x := evA mem1 e)⟩ \<R>1?Γ' ⟨Stop, mds, mem2 (x := evA mem2 e)⟩"
  proof (auto)
    from assign2 show "mds_consistent mds ?Γ'"
      apply (simp add: mds_consistent_def)
      by (metis (lifting) insert_absorb local.assign2(1))
  next
    show "mem1 (x := evA mem1 e) =?Γ' mem2 (x := evA mem2 e)"
      unfolding tyenv_eq_def
    proof (auto)
      assume "to_total (Γ(x \<mapsto> t)) x = Low"
      with `Γ \<turnstile>a e ∈ t` have "!! x. x ∈ aexp_vars e ==> to_total Γ x = Low"
        by (metis assign2.prems(1) domI fun_upd_same the.simps to_total_def type_low_vars_low)
      thus "evA mem1 e = evA mem2 e"
        by (metis assign2.prems(2) eval_vars_detA tyenv_eq_def)
    next
      fix y
      assume "y ≠ x" and "to_total (Γ (x \<mapsto> t)) y = Low"
      thus "mem1 y = mem2 y"
        by (metis (full_types) assign2.prems(2) domD domI fun_upd_other to_total_def tyenv_eq_def)
    qed
  qed
  ultimately have "⟨x \<leftarrow> e, mds, mem2⟩ \<leadsto> ⟨Stop, mds', mem2 (x := evA mem2 e)⟩"
    "⟨Stop, mds', mem1 (x := evA mem1 e)⟩ \<R>uΓ(x \<mapsto> t) ⟨Stop, mds', mem2 (x := evA mem2 e)⟩"
    using \<R>.intro1
    by auto
  thus ?case
    using `mds' = mds` `c1' = Stop` `mem1' = mem1(x := evA mem1 e)`
    by blast
next (* if *)
  case (if_type Γ e th el Γ')
  have "(⟨c1', mds, mem1⟩, ⟨c1', mds, mem2⟩) ∈ \<R> Γ'"
    apply (rule intro1)
    apply clarify
    apply (rule \<R>1.intro [where Γ = Γ and Γ' = Γ'])
      apply (auto simp: if_type)
    by (metis (lifting) if_elim local.if_type(2) local.if_type(4) local.if_type(8))
  have eq_condition: "evB mem1 e = evB mem2 e ==> ?case"
  proof -
    assume "evB mem1 e = evB mem2 e"
    with if_type(8) have "(⟨If e th el, mds, mem2⟩ \<leadsto> ⟨c1', mds, mem2⟩)"
      apply (cases "evB mem1 e")
       apply (subgoal_tac "c1' = th")
        apply clarify
        apply (metis cxt_to_stmt.simps(1) evalw_simplep.if_true evalwp.unannotated evalwp_evalw_eq local.if_type(8))
       apply (metis if_elim local.if_type(8))
      apply (subgoal_tac "c1' = el")
       apply (metis (hide_lams, mono_tags) cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.if_false local.if_type(8))
      by (metis if_elim local.if_type(8))
    thus ?thesis
      by (metis `⟨c1', mds, mem1⟩ \<R>uΓ' ⟨c1', mds, mem2⟩` if_elim local.if_type(8))
  qed
  have "mem1 =mdsl mem2"
    apply (auto simp: low_mds_eq_def mds_consistent_def)
    apply (subgoal_tac "x ∉ dom Γ")
     apply (metis local.if_type(7) to_total_def tyenv_eq_def)
    by (metis (lifting, mono_tags) CollectD Sec.simps(2) local.if_type(6) mds_consistent_def)
  obtain t where "Γ \<turnstile>b e ∈ t"
    by (metis type_bexpr.intros)
  from if_type show ?case
  proof (cases t)
    assume "t = High"
    with if_type show ?thesis
    proof (cases "evB mem1 e = evB mem2 e")
      assume "evB mem1 e = evB mem2 e"
      with eq_condition show ?thesis by auto
    next
      assume neq: "evB mem1 e ≠ evB mem2 e"
      from if_type `t = High` have "th ∼mds el"
        by (metis `Γ \<turnstile>b e ∈ t`)
      from neq show ?thesis
      proof (cases "evB mem1 e")
        assume "evB mem1 e"
        hence "c1' = th"
          by (metis (lifting) if_elim local.if_type(8))
        hence "⟨If e th el, mds, mem2⟩ \<leadsto> ⟨el, mds, mem2⟩"
          by (metis `evB mem1 e` cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.if_false local.if_type(8) neq)
        moreover
        with `mem1 =mdsl mem2` have "⟨th, mds, mem1⟩ ≈ ⟨el, mds, mem2⟩"
          by (metis low_indistinguishable_def `th ∼mds el`)
        have "∀ x ∈ dom Γ'. Γ' x = Some High"
          using if_type `t = High`
          by (metis `Γ \<turnstile>b e ∈ t`)
        have "⟨th, mds, mem1⟩ \<R>2Γ' ⟨el, mds, mem2⟩"
          by (metis (lifting) \<R>2.intro `∀x∈dom Γ'. Γ' x = Some High` `⟨th, mds, mem1⟩ ≈ ⟨el, mds, mem2⟩` local.if_type(2) local.if_type(4) local.if_type(6))
        ultimately show ?thesis
          using \<R>.intro2
          apply clarify
          by (metis `c1' = th` if_elim local.if_type(8))
      next
        assume "¬ evB mem1 e"
        hence [simp]: "c1' = el"
          by (metis (lifting) if_type(8) if_elim)
        hence "⟨If e th el, mds, mem2⟩ \<leadsto> ⟨th, mds, mem2⟩"
          by (metis (hide_lams, mono_tags) `¬ evB mem1 e` cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.if_true local.if_type(8) neq)
        moreover
        from `th ∼mds el` have "el ∼mds th"
          by (metis low_indistinguishable_sym)
        with `mem1 =mdsl mem2` have "⟨el, mds, mem1⟩ ≈ ⟨th, mds, mem2⟩"
          by (metis low_indistinguishable_def)
        have "∀ x ∈ dom Γ'. Γ' x = Some High"
          using if_type `t = High`
          by (metis `Γ \<turnstile>b e ∈ t`)
        have "⟨el, mds, mem1⟩ \<R>2Γ' ⟨th, mds, mem2⟩"
          apply (rule \<R>2.intro [where Γ1 = Γ and Γ2 = Γ])
          by (auto simp: if_type `⟨el, mds, mem1⟩ ≈ ⟨th, mds, mem2⟩` `∀ x ∈ dom Γ'. Γ' x = Some High`)
        ultimately show ?thesis
          using \<R>.intro2
          apply clarify
          by (metis `c1' = el` if_elim local.if_type(8))
      qed
    qed
  next
    assume "t = Low"
    with if_type have "evB mem1 e = evB mem2 e"
      using eval_vars_detB
      apply (simp add: tyenv_eq_def `Γ \<turnstile>b e ∈ t` type_low_vars_low_b)
      by (metis (lifting) `Γ \<turnstile>b e ∈ t` type_low_vars_low_b)
    with eq_condition show ?thesis by auto
  qed
next (* while *)
  case (while_type Γ e c)
  hence [simp]: "c1' = (If e (c ;; While e c) Stop)" and
    [simp]: "mds' = mds" and
    [simp]: "mem1' = mem1"
    by (auto simp: while_elim)
  with while_type have "⟨While e c, mds, mem2⟩ \<leadsto> ⟨c1', mds, mem2⟩"
    by (metis cxt_to_stmt.simps(1) evalw_simplep.while evalwp.unannotated evalwp_evalw_eq)
  moreover
  have "⟨c1', mds, mem1⟩ \<R>1Γ ⟨c1', mds, mem2⟩"
    apply (rule \<R>1.intro [where Γ = Γ])
      apply (auto simp: while_type)
    apply (rule if_type)
      apply (metis (lifting) Sec.simps(1) local.while_type(1) type_bexpr_elim)
     apply (rule seq_type [where Γ' = Γ])
      by (auto simp: while_type)
  ultimately show ?case
    using \<R>.intro1 [of Γ]
    by (auto, blast)
next
  case (sub Γ1 c Γ1' Γ Γ' mds c1')
  hence "dom Γ1 ⊆ dom Γ" "dom Γ' ⊆ dom Γ1'"
    apply (metis (lifting) context_le_def equalityE)
    by (metis context_le_def local.sub(4) order_refl)
  hence "mds_consistent mds Γ1"
    using sub
    apply (auto simp: mds_consistent_def)
     apply (metis (lifting, full_types) context_le_def domD mem_Collect_eq)
    by (metis (lifting, full_types) context_le_def domD mem_Collect_eq)
  moreover have "mem1 =Γ1 mem2"
    unfolding tyenv_eq_def
    by (metis (lifting, no_types) context_le_def less_eq_Sec_def sub.hyps(3) sub.prems(2) to_total_def tyenv_eq_def)
  ultimately obtain c2' mem2' where c2'_props: "⟨c, mds, mem2⟩ \<leadsto> ⟨c2', mds', mem2'⟩"
    "⟨c1', mds', mem1'⟩ \<R>uΓ1' ⟨c2', mds', mem2'⟩"
    using sub
    by blast
  moreover
  have "!! c1 mds mem1 c2 mem2. ⟨c1, mds, mem1⟩ \<R>uΓ1' ⟨c2, mds, mem2⟩ ==>
    ⟨c1, mds, mem1⟩ \<R>uΓ' ⟨c2, mds, mem2⟩"
  proof -
    fix c1 mds mem1 c2 mem2
    let ?lc1 = "⟨c1, mds, mem1⟩" and ?lc2 = "⟨c2, mds, mem2⟩"
    assume asm: "?lc1 \<R>uΓ1' ?lc2"
    moreover
    have "?lc1 \<R>1Γ1' ?lc2 ==> ?lc1 \<R>1Γ' ?lc2"
      apply (erule \<R>1_elim)
      apply auto
      by (metis (lifting) has_type.sub local.sub(4) stop_cxt stop_type)
    moreover
    have "?lc1 \<R>2Γ1' ?lc2 ==> ?lc1 \<R>2Γ' ?lc2"
    proof -
      assume r2: "?lc1 \<R>2Γ1' ?lc2"
      then obtain Λ1 Λ2 where "\<turnstile> Λ1 { c1 }  Γ1'" "\<turnstile> Λ2 { c2 } Γ1'" "mds_consistent mds Λ1"
        "mds_consistent mds Λ2"
        by (metis \<R>2_elim)
      hence "\<turnstile> Λ1 { c1 } Γ'"
        using sub(4)
        by (metis context_le_refl has_type.sub local.sub(4))
      moreover
      have "\<turnstile> Λ2 { c2 } Γ'"
        by (metis `\<turnstile> Λ2 {c2} Γ1'` context_le_refl has_type.sub local.sub(4))
      moreover
      from r2 have "∀ x ∈ dom Γ1'. Γ1' x = Some High"
        apply (rule \<R>2_elim)
        by auto
      hence "∀ x ∈ dom Γ'. Γ' x = Some High"
        by (metis Sec.simps(2) `dom Γ' ⊆ dom Γ1'` context_le_def domD less_eq_Sec_def local.sub(4) set_rev_mp the.simps)
      ultimately show ?thesis
        by (metis (no_types) \<R>2.intro \<R>2_elim' `mds_consistent mds Λ1` `mds_consistent mds Λ2` r2)
    qed
    moreover
    have "?lc1 \<R>3Γ1' ?lc2 ==> ?lc1 \<R>3Γ' ?lc2"
      apply (erule \<R>3_elim)
      proof -
        fix Γ c1'' c2''' c
        assume [simp]: "c1 = c1'' ;; c" "c2 = c2''' ;; c"
        assume case1: "\<turnstile> Γ {c} Γ1'" "⟨c1'', mds, mem1⟩ \<R>1Γ ⟨c2''', mds, mem2⟩"
        hence "\<turnstile> Γ {c} Γ'"
          using context_le_refl has_type.sub sub.hyps(4)
          by blast
        with case1 show "⟨c1, mds, mem1⟩ \<R>3Γ' ⟨c2, mds, mem2⟩"
          using \<R>3_aux.intro1 by simp
      next
        fix Γ c1'' c2''' c''
        assume [simp]: "c1 = c1'' ;; c''" "c2 = c2''' ;; c''"
        assume "⟨c1'', mds, mem1⟩ \<R>2Γ ⟨c2''', mds, mem2⟩" "\<turnstile> Γ {c''} Γ1'"
        thus "⟨c1, mds, mem1⟩ \<R>3Γ' ⟨c2, mds, mem2⟩"
          using \<R>3_aux.intro2
          apply simp
          apply (rule \<R>3_aux.intro2 [where Γ = Γ])
           apply simp
          by (metis context_le_refl has_type.sub sub.hyps(4))
      next
        fix Γ c1'' c2''' c''
        assume [simp]: "c1 = c1'' ;; c''" "c2 = c2''' ;; c''"
        assume "⟨c1'', mds, mem1⟩ \<R>3Γ ⟨c2''', mds, mem2⟩" "\<turnstile> Γ {c''} Γ1'"
        thus "⟨c1, mds, mem1⟩ \<R>3Γ' ⟨c2, mds, mem2⟩"
          using \<R>3_aux.intro3
          apply auto
          by (metis (hide_lams, no_types) context_le_refl has_type.sub sub.hyps(4))
      qed
    ultimately show "?thesis c1 mds mem1 c2 mem2"
      by (auto simp: \<R>.intros)
  qed
  with c2'_props show ?case
    by blast
qed

(* We can now show that \<R>1 and \<R>3 are weak bisimulations of \<R>,: *)
lemma \<R>1_weak_bisim:
  "weak_bisim (\<R>1 Γ') (\<R> Γ')"
  unfolding weak_bisim_def
  using \<R>1_elim \<R>_typed_step
  by auto

lemma \<R>_to_\<R>3: "[| ⟨c1, mds, mem1⟩ \<R>uΓ ⟨c2, mds, mem2⟩ ; \<turnstile> Γ { c } Γ' |] ==>
  ⟨c1 ;; c, mds, mem1⟩ \<R>3Γ' ⟨c2 ;; c, mds, mem2⟩"
  apply (erule \<R>_elim)
  by auto

lemma \<R>2_implies_typeable: "⟨c1, mds, mem1⟩ \<R>2Γ' ⟨c2, mds, mem2⟩ ==> ∃ Γ1. \<turnstile> Γ1 { c2 } Γ'"
  apply (erule \<R>2_elim)
  by auto

lemma \<R>3_weak_bisim:
  "weak_bisim (\<R>3 Γ') (\<R> Γ')"
proof -
  {
    fix c1 mds mem1 c2 mem2 c1' mds' mem1'
    assume case3: "(⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ \<R>3 Γ'"
    assume eval: "⟨c1, mds, mem1⟩ \<leadsto> ⟨c1', mds', mem1'⟩"
    have "∃ c2' mem2'. ⟨c2, mds, mem2⟩ \<leadsto> ⟨c2', mds', mem2'⟩ ∧ ⟨c1', mds', mem1'⟩ \<R>uΓ' ⟨c2', mds', mem2'⟩"
      using case3 eval
      apply simp
      
    proof (induct arbitrary: c1' rule: \<R>3_aux.induct)
      case (intro1 Γ c1 mds mem1 c2 mem2 c Γ')
      hence [simp]: "c2 = c1"
        by (metis (lifting) \<R>1_elim)
      thus ?case
      proof (cases "c1 = Stop")
        assume [simp]: "c1 = Stop"
        from intro1(1) show ?thesis
          apply (rule \<R>1_elim)
          apply simp
          apply (rule_tac x = c in exI)
          apply (rule_tac x = mem2 in exI)
          apply (rule conjI)
           apply (metis `c1 = Stop` cxt_to_stmt.simps(1) evalw_simplep.seq_stop evalwp.unannotated evalwp_evalw_eq intro1.prems seq_stop_elim)
          apply (rule \<R>.intro1, clarify)
          by (metis (no_types) \<R>1.intro `c1 = Stop` context_le_refl intro1.prems local.intro1(2) seq_stop_elim stop_cxt sub)
      next
        assume "c1 ≠ Stop"
        from intro1
        obtain c1'' where "⟨c1, mds, mem1⟩ \<leadsto> ⟨c1'', mds', mem1'⟩ ∧ c1' = (c1'' ;; c)"
          by (metis `c1 ≠ Stop` intro1.prems seq_elim)
        with intro1
        obtain c2'' mem2' where "⟨c2, mds, mem2⟩ \<leadsto> ⟨c2'', mds', mem2'⟩" "⟨c1'', mds', mem1'⟩ \<R>uΓ ⟨c2'', mds', mem2'⟩"
          using \<R>1_weak_bisim and weak_bisim_def
          by blast
        thus ?thesis
          using intro1(2) \<R>_to_\<R>3
          apply (rule_tac x = "c2'' ;; c" in exI)
          apply (rule_tac x = mem2' in exI)
          apply (rule conjI)
           apply (metis evalw.seq)
          apply auto
          apply (rule \<R>.intro3)
          by (metis (hide_lams, no_types) `⟨c1, mds, mem1⟩ \<leadsto> ⟨c1'', mds', mem1'⟩ ∧ c1' = c1'' ;; c`)
      qed
    next
      case (intro2 Γ c1 mds mem1 c2 mem2 cn Γ')
      thus ?case
      proof (cases "c1 = Stop")
        assume [simp]: "c1 = Stop"
        hence [simp]: "c1' = cn" "mds' = mds" "mem1' = mem1"
          using eval intro2 seq_stop_elim 
          by auto
        from intro2 have bisim: "⟨c1, mds, mem1⟩ ≈ ⟨c2, mds, mem2⟩"
          by (metis (lifting) \<R>2_elim')
        from intro2 obtain Γ1 where "\<turnstile> Γ1 { c2 } Γ"
          by (metis \<R>2_implies_typeable)
        with bisim have [simp]: "c2 = Stop"
          apply auto
          apply (rule stop_bisim [of mds mem1 c2 mem2 Γ1 Γ])
          by simp_all
        have "⟨c2 ;; cn, mds, mem2⟩ \<leadsto> ⟨cn, mds', mem2⟩"
          apply (auto simp: intro2)
          by (metis cxt_to_stmt.simps(1) evalw_simplep.seq_stop evalwp.unannotated evalwp_evalw_eq)
        moreover
        from intro2(1) have "mds_consistent mds Γ"
          apply auto
          apply (erule \<R>2_elim)
          apply (simp add: mds_consistent_def)
          by (metis context_le_def stop_cxt)
        moreover
        from bisim have "mem1 =mdsl mem2"
          by (auto simp: mm_equiv.simps strong_low_bisim_mm_def)
        have "∀ x ∈ dom Γ. Γ x = Some High"
          using intro2(1)
          by (metis \<R>2_elim')
        hence "mem1 =Γ mem2"
          using `mds_consistent mds Γ` `mem1 =mdsl mem2`
          apply (auto simp: tyenv_eq_def low_mds_eq_def mds_consistent_def)
          by (metis Sec.simps(1) `∀x∈dom Γ. Γ x = Some High` `mds' = mds` domI the.simps to_total_def)
        ultimately have "⟨cn, mds, mem1⟩ \<R>1Γ' ⟨cn, mds, mem2⟩"
          by (metis (lifting) \<R>1.intro local.intro2(2))
        thus "?thesis"
          using \<R>.intro1
          apply auto
          by (metis `⟨c2 ;; cn, mds, mem2⟩ \<leadsto> ⟨cn, mds', mem2⟩` `c2 = Stop` `mds' = mds`)
      next
        assume "c1 ≠ Stop"
        then obtain c1''' where "c1' = c1''' ;; cn" "⟨c1, mds, mem1⟩ \<leadsto> ⟨c1''', mds', mem1'⟩"
          by (metis (no_types) intro2.prems seq_elim)
        then obtain c2''' mem2' where c2'''_props:
          "⟨c2, mds, mem2⟩ \<leadsto> ⟨c2''', mds', mem2'⟩ ∧
          ⟨c1''', mds', mem1'⟩ \<R>2Γ ⟨c2''', mds', mem2'⟩"
          using \<R>2_bisim_step intro2
          by blast
        let ?c2' = "c2''' ;; cn"
        from c2'''_props have "⟨c2 ;; cn, mds, mem2⟩ \<leadsto> ⟨?c2', mds', mem2'⟩"
          by (metis (lifting) intro2 evalw.seq)
        moreover
        have "(⟨c1''' ;; cn, mds', mem1'⟩, ⟨?c2', mds', mem2'⟩) ∈ \<R>3 Γ'"
          by (metis (lifting) \<R>3_aux.intro2 c2'''_props local.intro2(2) mem_Collect_eq splitI)
        ultimately show ?thesis
          using \<R>.intro3
          by (metis (lifting) \<R>3_aux.intro2 `c1' = c1''' ;; cn` c2'''_props local.intro2(2))
      qed
    next
      case (intro3 Γ c1 mds mem1 c2 mem2 c Γ')
      thus ?case
        apply (cases "c1 = Stop")
         apply blast
      proof -
        assume "c1 ≠ Stop"
        then obtain c1'' where "⟨c1, mds, mem1⟩ \<leadsto> ⟨c1'', mds', mem1'⟩" "c1' = (c1'' ;; c)"
          by (metis intro3.prems seq_elim)
        then obtain c2'' mem2' where "⟨c2, mds, mem2⟩ \<leadsto> ⟨c2'', mds', mem2'⟩" "⟨c1'', mds', mem1'⟩ \<R>uΓ ⟨c2'', mds', mem2'⟩"
          using local.intro3(2) mem_Collect_eq splitI
          by metis
        thus ?thesis
          apply (rule_tac x = "c2'' ;; c" in exI)
          apply (rule_tac x = mem2' in exI)
          apply (rule conjI)
           apply (metis evalw.seq)
          apply (erule \<R>_elim)
            apply simp_all
            apply (metis \<R>.intro3 \<R>_to_\<R>3 `⟨c1'', mds', mem1'⟩ \<R>uΓ ⟨c2'', mds', mem2'⟩` `c1' = c1'' ;; c` local.intro3(3))
           apply (metis (lifting) \<R>.intro3 \<R>_to_\<R>3 `⟨c1'', mds', mem1'⟩ \<R>uΓ ⟨c2'', mds', mem2'⟩` `c1' = c1'' ;; c` local.intro3(3))
          by (metis (lifting) \<R>.intro3 \<R>3_aux.intro3 `c1' = c1'' ;; c` local.intro3(3))
      qed
    qed
  }
  thus ?thesis
    unfolding weak_bisim_def
    by auto
qed

(* Hence \<R> is a bisimulation: *)
lemma \<R>_bisim: "strong_low_bisim_mm (\<R> Γ')"
  unfolding strong_low_bisim_mm_def
proof (auto)
  from \<R>_sym show "sym (\<R> Γ')" .
next
  from \<R>_closed_glob_consistent show "closed_glob_consistent (\<R> Γ')" .
next
  fix c1 mds mem1 c2 mem2
  assume "⟨c1, mds, mem1⟩ \<R>uΓ' ⟨c2, mds, mem2⟩"
  thus "mem1 =mdsl mem2"
    apply (rule \<R>_elim)
    by (auto simp: \<R>1_mem_eq \<R>2_mem_eq \<R>3_mem_eq)
next
  fix c1 mds mem1 c2 mem2 c1' mds' mem1'
  assume eval: "⟨c1, mds, mem1⟩ \<leadsto> ⟨c1', mds', mem1'⟩"
  assume R: "⟨c1, mds, mem1⟩ \<R>uΓ' ⟨c2, mds, mem2⟩"
  from R show "∃ c2' mem2'. ⟨c2, mds, mem2⟩ \<leadsto> ⟨c2', mds', mem2'⟩ ∧
                            ⟨c1', mds', mem1'⟩ \<R>uΓ' ⟨c2', mds', mem2'⟩"
    apply (rule \<R>_elim)
      apply (insert \<R>1_weak_bisim \<R>2_weak_bisim \<R>3_weak_bisim eval weak_bisim_def)
      apply (clarify, blast)+
    by (metis mem_Collect_eq prod_caseI)
qed

lemma Typed_in_\<R>:
  assumes typeable: "\<turnstile> Γ { c } Γ'"
  assumes mds_cons: "mds_consistent mds Γ"
  assumes mem_eq: "∀ x. to_total Γ x = Low --> mem1 x = mem2 x"
  shows "⟨c, mds, mem1⟩ \<R>uΓ' ⟨c, mds, mem2⟩"
  apply (rule \<R>.intro1 [of Γ'])
  apply clarify
  apply (rule \<R>1.intro [of Γ])
  by (auto simp: assms tyenv_eq_def) 

(* We then prove the main soundness theorem using the fact that typeable
    configurations can be related using \<R>1 *)
theorem type_soundness:
  assumes well_typed: "\<turnstile> Γ { c } Γ'"
  assumes mds_cons: "mds_consistent mds Γ"
  assumes mem_eq: "∀ x. to_total Γ x = Low --> mem1 x = mem2 x"
  shows "⟨c, mds, mem1⟩ ≈ ⟨c, mds, mem2⟩"
  using \<R>_bisim Typed_in_\<R>
  by (metis mds_cons mem_eq mm_equiv.simps well_typed)

definition "Γ0" :: "'Var TyEnv"
  where "Γ0 x = None"

(* The typing relation for lists of commands ("thread pools"). *)
inductive type_global :: "('Var, 'AExp, 'BExp) Stmt list => bool"
  ("\<turnstile> _" [120] 1000)
  where
  "[| list_all (λ c. \<turnstile> Γ0 { c } Γ0) cs ;
     ∀ mem. sound_mode_use (add_initial_modes cs, mem) |] ==>
    type_global cs"

inductive_cases type_global_elim: "\<turnstile> cs"

lemma mdss_consistent: "mds_consistent mdss Γ0"
  by (auto simp: mdss_def mds_consistent_def Γ0_def)

lemma typed_secure:
  "[| \<turnstile> Γ0 { c } Γ0 |] ==> com_sifum_secure c"
  apply (auto simp: com_sifum_secure_def low_indistinguishable_def mds_consistent_def type_soundness)
  apply (auto simp: low_mds_eq_def)
  apply (rule type_soundness [of Γ0 c Γ0])
    apply (auto simp: mdss_consistent to_total_def Γ0_def)
  by (metis empty_iff mdss_def)

lemma "[| mds_consistent mds Γ0 ; dma x = Low |] ==> x ∉ mds AsmNoRead"
  by (auto simp: mds_consistent_def Γ0_def)

lemma list_all_set: "∀ x ∈ set xs. P x ==> list_all P xs"
  by (metis (lifting) list_all_iff)

theorem type_soundness_global:
  assumes typeable: "\<turnstile> cs"
  assumes no_assms_term: "no_assumptions_on_termination cs"
  shows "prog_sifum_secure cs"
  using typeable
  apply (rule type_global_elim)
  apply (subgoal_tac "∀ c ∈ set cs. com_sifum_secure c")
   apply (metis list_all_set no_assms_term sifum_compositionality sound_mode_use.simps)
  by (metis (lifting) list_all_iff typed_secure)

end
end