Theory TypeSystem

(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
section ‹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 ⇀ 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 ‹↝› 70)
  where
  "x ↝ y ≡ (x, y) ∈ evalw"

abbreviation low_indistinguishable_abv :: "'Var Mds ⇒ ('Var, 'AExp, 'BExp) Stmt ⇒ (_, _, _) Stmt ⇒ bool"
  (‹_ ∼ı _› [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" (‹_ ⊢a _ ∈ _› [120, 120, 120] 1000)
  where
  type_aexpr [intro!]: "Γ ⊢a e ∈ max_dom (image (λ x. to_total Γ x) (aexp_vars e))"

inductive_cases type_aexpr_elim [elim]: "Γ ⊢a e ∈ t"

inductive type_bexpr :: "'Var TyEnv ⇒ 'BExp ⇒ Type ⇒ bool" (‹_ ⊢b _ ∈ _ › [120, 120, 120] 1000)
  where
  type_bexpr [intro!]: "Γ ⊢b e ∈ max_dom (image (λ x. to_total Γ x) (bexp_vars e))"

inductive_cases type_bexpr_elim [elim]: "Γ ⊢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 ‹⊑c› 100)
  where
  "Γ ⊑c Γ' ≡ (dom Γ = dom Γ') ∧ (∀ x ∈ dom Γ. the (Γ x) ⊑ the (Γ' x))"

inductive has_type :: "'Var TyEnv ⇒ ('Var, 'AExp, 'BExp) Stmt ⇒ 'Var TyEnv ⇒ bool"
  (‹⊢ _ {_} _› [120, 120, 120] 1000)
  where
  stop_type [intro]: "⊢ Γ {Stop} Γ" |
  skip_type [intro] : "⊢ Γ {Skip} Γ" |
  assign1 : "⟦ x ∉ dom Γ ; Γ ⊢a e ∈ t; t ⊑ dma x ⟧ ⟹ ⊢ Γ {x ← e} Γ" |
  assign2 : "⟦ x ∈ dom Γ ; Γ ⊢a e ∈ t ⟧ ⟹ has_type Γ (x ← e) (Γ (x := Some t))" |
  if_type [intro]: "⟦ Γ ⊢b e ∈ High ⟶ 
    ((∀ mds. mds_consistent mds Γ ⟶ (low_indistinguishable mds c1 c2)) ∧
     (∀ x ∈ dom Γ'. Γ' x = Some High))
             ; ⊢ Γ { c1 } Γ'
             ; ⊢ Γ { c2 } Γ' ⟧ ⟹
             ⊢ Γ { If e c1 c2 } Γ'" |
  while_type [intro]: "⟦ Γ ⊢b e ∈ Low ; ⊢ Γ { c } Γ ⟧ ⟹ ⊢ Γ { While e c } Γ" |
  anno_type [intro]: "⟦ Γ' = Γ ⊕ upd ; ⊢ Γ' { c } Γ'' ; c ≠ Stop ;
                 ∀ x. to_total Γ x ⊑ to_total Γ' x ⟧ ⟹ ⊢ Γ { c@[upd] } Γ''" |
  seq_type [intro]: "⟦ ⊢ Γ { c1 } Γ' ; ⊢ Γ' { c2 } Γ'' ⟧ ⟹ ⊢ Γ { c1 ;; c2 } Γ''" |
  sub : "⟦ ⊢ Γ1 { c } Γ1' ; Γ2 ⊑c Γ1 ; Γ1' ⊑c Γ2' ⟧ ⟹ ⊢ Γ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: "⊢ Γ { c } Γ'"
inductive_cases has_type_stop_elim: "⊢ Γ { Stop } Γ'"

definition tyenv_eq :: "'Var TyEnv ⇒ ('Var, 'Val) Mem ⇒ ('Var, 'Val) Mem ⇒ bool"
  (infix ‹=ı› 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 ℛ1 :: "'Var TyEnv ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  and ℛ1_abv :: "'Var TyEnv ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  bool" (‹_ ℛ1ı _› [120, 120] 1000)
  for Γ' :: "'Var TyEnv"
  where
  "x ℛ1⇘Γ⇙ y ≡ (x, y) ∈ ℛ1 Γ" |
  intro [intro!] : "⟦ ⊢ Γ { c } Γ' ; mds_consistent mds Γ ; mem1 =⇘Γ⇙ mem2 ⟧ ⟹ ⟨c, mds, mem1⟩ ℛ1⇘Γ'⇙ ⟨c, mds, mem2⟩"

inductive_set ℛ2 :: "'Var TyEnv ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  and ℛ2_abv :: "'Var TyEnv ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  bool" (‹_ ℛ2ı _› [120, 120] 1000)
  for Γ' :: "'Var TyEnv"
  where
  "x ℛ2⇘Γ⇙ y ≡ (x, y) ∈ ℛ2 Γ" |
  intro [intro!] : "⟦ ⟨c1, mds, mem1⟩ ≈ ⟨c2, mds, mem2⟩ ;
                       ∀ x ∈ dom Γ'. Γ' x = Some High ;
                       ⊢ Γ1 { c1 } Γ' ; ⊢ Γ2 { c2 } Γ' ;
                       mds_consistent mds Γ1 ; mds_consistent mds Γ2 ⟧ ⟹
                     ⟨c1, mds, mem1⟩ ℛ2⇘Γ'⇙ ⟨c2, mds, mem2⟩"

inductive ℛ3_aux :: "'Var TyEnv ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
                 (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
                 bool" (‹_ ℛ3ı _› [120, 120] 1000)
  and ℛ3 :: "'Var TyEnv ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  where
  "ℛ3 Γ' ≡ {(lc1, lc2). ℛ3_aux Γ' lc1 lc2}" |
  intro1 [intro] : "⟦ ⟨c1, mds, mem1⟩ ℛ1⇘Γ⇙ ⟨c2, mds, mem2⟩; ⊢ Γ { c } Γ' ⟧ ⟹
                      ⟨Seq c1 c, mds, mem1⟩ ℛ3⇘Γ'⇙ ⟨Seq c2 c, mds, mem2⟩" |
  intro2 [intro] : "⟦ ⟨c1, mds, mem1⟩ ℛ2⇘Γ⇙ ⟨c2, mds, mem2⟩; ⊢ Γ { c } Γ' ⟧ ⟹
                      ⟨Seq c1 c, mds, mem1⟩ ℛ3⇘Γ'⇙ ⟨Seq c2 c, mds, mem2⟩" |
  intro3 [intro] : "⟦ ⟨c1, mds, mem1⟩ ℛ3⇘Γ⇙ ⟨c2, mds, mem2⟩; ⊢ Γ { c } Γ' ⟧ ⟹
                      ⟨Seq c1 c, mds, mem1⟩ ℛ3⇘Γ'⇙ ⟨Seq c2 c, mds, mem2⟩"

(* A weaker property than bisimulation to reason about the sub-relations of ℛ: *)
definition weak_bisim :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel ⇒
                        (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel ⇒ bool"
  where "weak_bisim 𝒯1 𝒯 ≡ ∀ c1 c2 mds mem1 mem2 c1' mds' mem1'.
  ((⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ 𝒯1 ∧
   (⟨c1, mds, mem1⟩ ↝ ⟨c1', mds', mem1'⟩)) ⟶
  (∃ c2' mem2'. ⟨c2, mds, mem2⟩ ↝ ⟨c2', mds', mem2'⟩ ∧ 
                (⟨c1', mds', mem1'⟩, ⟨c2', mds', mem2'⟩) ∈ 𝒯)"

inductive_set ℛ :: "'Var TyEnv ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  and ℛ_abv :: "'Var TyEnv ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  bool" (‹_ ℛuı _› [120, 120] 1000)
  for Γ :: "'Var TyEnv"
  where
  "x ℛu⇘Γ⇙ y ≡ (x, y) ∈ ℛ Γ" |
  intro1: "lc ℛ1⇘Γ⇙ lc' ⟹ (lc, lc') ∈ ℛ Γ" |
  intro2: "lc ℛ2⇘Γ⇙ lc' ⟹ (lc, lc') ∈ ℛ Γ" |
  intro3: "lc ℛ3⇘Γ⇙ lc' ⟹ (lc, lc') ∈ ℛ Γ"

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

inductive_cases ℛ_elim [elim]: "(⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ ℛ Γ"
inductive_cases ℛ_elim': "(⟨c1, mds, mem1⟩, ⟨c2, mds2, mem2⟩) ∈ ℛ Γ"
inductive_cases ℛ1_elim' : "⟨c1, mds, mem1⟩ ℛ1⇘Γ⇙ ⟨c2, mds2, mem2⟩"
inductive_cases ℛ2_elim' : "⟨c1, mds, mem1⟩ ℛ2⇘Γ⇙ ⟨c2, mds2, mem2⟩"
inductive_cases ℛ3_elim' : "⟨c1, mds, mem1⟩ ℛ3⇘Γ⇙ ⟨c2, mds2, mem2⟩"

(* To prove that ℛ is a bisimulation, we first show symmetry *)

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

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

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

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

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

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

lemma ℛ1_closed_glob_consistent: "closed_glob_consistent (ℛ1 Γ')"
  unfolding closed_glob_consistent_def
proof (clarify)
  fix c1 mds mem1 c2 mem2 x Γ'
  assume R1: "⟨c1, mds, mem1⟩ ℛ1⇘Γ'⇙ ⟨c2, mds, mem2⟩"
  hence [simp]: "c2 = c1" by blast
  from R1 obtain Γ where Γ_props: "⊢ Γ { c1 } Γ'" "mem1 =⇘Γ⇙ mem2" "mds_consistent mds Γ"
    by blast
  hence "⋀ v. ⟨c1, mds, mem1 (x := v)⟩ ℛ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)⟩ ℛ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)⟩ ℛ1⇘Γ'⇙ ⟨c2, mds, mem2(x := v2)⟩))
     ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite ⟶
      (∀v. ⟨c1, mds, mem1(x := v)⟩ ℛ1⇘Γ'⇙ ⟨c2, mds, mem2(x := v)⟩))"
    using intro1
    by auto
qed

lemma ℛ2_closed_glob_consistent: "closed_glob_consistent (ℛ2 Γ')"
  unfolding closed_glob_consistent_def
proof (clarify)
  fix c1 mds mem1 c2 mem2 x Γ'
  assume R2: "⟨c1, mds, mem1⟩ ℛ2⇘Γ'⇙ ⟨c2, mds, mem2⟩"
  then obtain Γ1 Γ2 where Γ_prop: "⊢ Γ1 { c1 } Γ'" "⊢ Γ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 ℛ' where ℛ'_prop: "(⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ ℛ' ∧ strong_low_bisim_mm ℛ'"
    apply (rule mm_equiv_elim)
    by (auto simp: strong_low_bisim_mm_def)
  from ℛ'_prop have ℛ'_cons: "closed_glob_consistent ℛ'"
    by (auto simp: strong_low_bisim_mm_def)
  moreover
  from Γ_prop and ℛ'_prop
  have "⋀mem1 mem2. (⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ ℛ' ⟹ ⟨c1, mds, mem1⟩ ℛ2⇘Γ'⇙ ⟨c2, mds, mem2⟩"
    using ℛ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)⟩ ℛ2⇘Γ'⇙ ⟨c2, mds, mem2(x := v2)⟩))
     ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite ⟶
      (∀v. ⟨c1, mds, mem1(x := v)⟩ ℛ2⇘Γ'⇙ ⟨c2, mds, mem2(x := v)⟩))"
    using ℛ'_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) ⟩) ∈ ℛ3 Γ')) ∧
         ((dma x = Low ∧ x ∉ mds AsmNoWrite) ⟶
           (∀ v. (⟨ c1, mds, mem1 (x := v) ⟩, ⟨ c2, mds, mem2 (x := v) ⟩) ∈ ℛ3 Γ')))"

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

lemma ℛ_closed_glob_consistent: "closed_glob_consistent (ℛ Γ')"
  unfolding closed_glob_consistent_def
proof (clarify, erule ℛ_elim, simp_all)
  fix c1 mds mem1 c2 mem2 x
  assume R1: "⟨c1, mds, mem1⟩ ℛ1⇘Γ'⇙ ⟨c2, mds, mem2⟩"
  with ℛ1_closed_glob_consistent show
    "(dma x = High ∧ x ∉ mds AsmNoWrite ⟶
        (∀v1 v2. (⟨c1, mds, mem1(x := v1)⟩, ⟨c2, mds, mem2(x := v2)⟩) ∈ ℛ Γ')) ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite ⟶
        (∀v. (⟨c1, mds, mem1(x := v)⟩, ⟨c2, mds, mem2(x := v)⟩) ∈ ℛ Γ'))"
    unfolding closed_glob_consistent_def
    using intro1
    apply clarify
    by metis
next
  fix c1 mds mem1 c2 mem2 x
  assume R2: "⟨c1, mds, mem1⟩ ℛ2⇘Γ'⇙ ⟨c2, mds, mem2⟩"
  with ℛ2_closed_glob_consistent show
    "(dma x = High ∧ x ∉ mds AsmNoWrite ⟶
      (∀v1 v2. (⟨c1, mds, mem1(x := v1)⟩, ⟨c2, mds, mem2(x := v2)⟩) ∈ ℛ Γ'))
     ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite ⟶
      (∀v. (⟨c1, mds, mem1(x := v)⟩, ⟨c2, mds, mem2(x := v)⟩) ∈ ℛ Γ'))"
    unfolding closed_glob_consistent_def
    using intro2
    apply clarify
    by metis
next
  fix c1 mds mem1 c2 mem2 x Γ'
  assume R3: "⟨c1, mds, mem1⟩ ℛ3⇘Γ'⇙ ⟨c2, mds, mem2⟩"
  thus
    "(dma x = High ∧ x ∉ mds AsmNoWrite ⟶
       (∀v1 v2. (⟨c1, mds, mem1(x := v1)⟩, ⟨c2, mds, mem2(x := v2)⟩) ∈ ℛ Γ'))
     ∧
     (dma x = Low ∧ x ∉ mds AsmNoWrite ⟶
       (∀v. (⟨c1, mds, mem1(x := v)⟩, ⟨c2, mds, mem2(x := v)⟩) ∈ ℛ Γ'))"
    using ℛ3_closed_glob_consistent
    apply auto
     apply (metis ℛ.intro3)
    by (metis (lifting) ℛ.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: "Γ ⊢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 : "Γ ⊢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: "⟦ Γ ⊑c Γ' ; Γ' ⊑c Γ'' ⟧ ⟹ Γ ⊑c Γ''"
  apply (auto simp: context_le_def)
  by (metis domI order_trans option.sel)

lemma context_le_refl [simp]: "Γ ⊑c Γ"
  by (metis context_le_def order_refl)

(* Strangely, using only ⊢ Γ { Stop } Γ' as assumption does not work *)
lemma stop_cxt :
  "⟦ ⊢ Γ { c } Γ' ; c = Stop ⟧ ⟹ Γ ⊑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: "⊢ Γ { c } Γ'"
  assumes eval: "⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
  shows "∃ Γ''. (⊢ Γ'' { 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⟩ ↝ ⟨c', mds', mem'⟩"
    by (metis upd_elim)
  with anno_type(3) obtain Γ''' where
    "⊢ Γ''' { 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 ↦ t)" in exI)
    apply (auto simp: mds_consistent_def)
         apply (metis Sec.exhaust)
        apply (metis (lifting, full_types) CollectD domI assign2(1))
       apply (metis (lifting, full_types) CollectD domI assign2(1))
      apply (metis (lifting) CollectE domI 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 while_type(1) 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 seq_type(1) seq_type(3) stop_cxt sub)
  next
    assume "c1 ≠ Stop"
    then obtain c1' where "⟨c1, mds, mem⟩ ↝ ⟨c1', mds', mem'⟩ ∧ c' = (c1' ;; c2)"
      by (metis seq_elim seq_type.prems)
    then obtain Γ''' where "⊢ Γ''' {c1'} Γ1 ∧
      (mds_consistent mds Γ ⟶ mds_consistent mds' Γ''')"
      using seq_type(2)
      by auto
    moreover
    from seq_type have "⊢ Γ1 { c2 } Γ2" by auto
    moreover
    ultimately show ?case
      apply (rule_tac x = Γ''' in exI)
      by (metis (lifting) ‹⟨c1, mds, mem⟩ ↝ ⟨c1', mds', mem'⟩ ∧ c' = c1' ;; c2› has_type.seq_type)
  qed
next
  case (sub Γ1 c Γ1' Γ2 Γ2' c' mds)
  then obtain Γ'' where "⊢ Γ'' { 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 sub(4) stop_cxt stop_type)
    apply (simp add: mds_consistent_def)
    by (metis context_le_def sub.hyps(3))
qed

lemma ℛ1_mem_eq: "⟨c1, mds, mem1⟩ ℛ1⇘Γ'⇙ ⟨c2, mds, mem2⟩ ⟹ mem1 =⇘mds⇙l mem2"
  apply (rule ℛ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 ℛ2_mem_eq: "⟨c1, mds, mem1⟩ ℛ2⇘Γ'⇙ ⟨c2, mds, mem2⟩ ⟹ mem1 =⇘mds⇙l mem2"
  apply (rule ℛ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 =⇘mds⇙l mem2"

lemma ℛ3_mem_eq: "⟨c1, mds, mem1⟩ ℛ3⇘Γ'⇙ ⟨c2, mds, mem2⟩ ⟹ mem1 =⇘mds⇙l mem2"
  apply (subgoal_tac "bisim_helper ⟨c1, mds, mem1⟩ ⟨c2, mds, mem2⟩")
   apply simp
  apply (induct rule: ℛ3_aux.induct)
  by (auto simp: ℛ1_mem_eq ℛ2_mem_eq)

(* ℛ2 is a full bisimulation so we can show the stronger step statement here: *)

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

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

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


(* Not actually needed, but an interesting "asymmetry" since
    ℛ1 and ℛ3 aren't bisimulations. *)
lemma ℛ2_bisim: "strong_low_bisim_mm (ℛ2 Γ')"
  unfolding strong_low_bisim_mm_def
  by (auto simp: ℛ2_sym ℛ2_closed_glob_consistent ℛ2_mem_eq ℛ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:
  "⟦ ⊢ Γ { 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⟩ ↝ ⟨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: "⊢ Γ { 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 ↝ ⟨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⟩ ↝ ⟨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 ℛ1_weak_bisim: *)

lemma ℛ_typed_step:
  "⟦ ⊢ Γ { c1 } Γ' ;
     mds_consistent mds Γ ;
     mem1 =⇘Γ⇙ mem2 ;
     ⟨c1, mds, mem1⟩ ↝ ⟨c1', mds', mem1'⟩ ⟧ ⟹
   (∃ c2' mem2'. ⟨c1, mds, mem2⟩ ↝ ⟨c2', mds', mem2'⟩ ∧
                 ⟨c1', mds', mem1'⟩ ℛ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 "Γ ⊑c Γ''"
      by (metis stop_cxt)
    hence "⊢ Γ { c2 } Γ'"
      by (metis context_le_refl seq_type(3) sub)
    have "⟨c2, mds, mem1⟩ ℛ1⇘Γ'⇙ ⟨c2, mds, mem2⟩"
      apply (rule ℛ1.intro [of Γ])
      by (auto simp: seq_type ‹⊢ Γ { c2 } Γ'›)
    thus ?case
      using ℛ.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⟩ ↝ ⟨c1', mds', mem1'⟩› obtain c1'' where c1''_props:
      "⟨c1, mds, mem1⟩ ↝ ⟨c1'', mds', mem1'⟩ ∧ c1' = c1'' ;; c2"
      by (metis seq_elim)
    with seq_type(2) obtain c2'' mem2' where c2''_props:
      "⟨c1, mds, mem2⟩ ↝ ⟨c2'', mds', mem2'⟩ ∧ ⟨c1'', mds', mem1'⟩ ℛu⇘Γ''⇙ ⟨c2'', mds', mem2'⟩"
      by (metis seq_type(5) seq_type(6))
    hence "⟨c1'' ;; c2, mds', mem1'⟩ ℛu⇘Γ'⇙ ⟨c2'' ;; c2, mds', mem2'⟩"
      apply (rule conjE)
      apply (erule ℛ_elim, auto)
        apply (metis ℛ.intro3 ℛ3_aux.intro1 seq_type(3))
       apply (metis ℛ.intro3 ℛ3_aux.intro2 seq_type(3))
      by (metis ℛ.intro3 ℛ3_aux.intro3 seq_type(3))
    moreover
    from c2''_props have "⟨c1 ;; c2, mds, mem2⟩ ↝ ⟨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 anno_type(5) anno_type(7) tyenv_eq_def)
  have "mds_consistent (update_modes upd mds) Γ'"
    by (metis (lifting) anno_type(1) anno_type(6) mode_update_add_anno)
  then obtain c2' mem2' where "(⟨c, update_modes upd mds, mem2⟩ ↝ ⟨c2', mds', mem2'⟩ ∧
    ⟨c1', mds', mem1'⟩ ℛu⇘Γ''⇙ ⟨c2', mds', mem2'⟩)"
    using anno_type
    apply auto
    by (metis ‹mem1 =⇘Γ'⇙ mem2› 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⟩ ℛ1⇘Γ⇙ ⟨Stop, mds, mem2⟩"
    by auto
  thus ?case
    using ℛ.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) assign1(5) tyenv_eq_def)
      by (metis assign1(5) tyenv_eq_def)
  qed
  hence "⟨x ← e, mds, mem2⟩ ↝ ⟨Stop, mds', mem2 (x := evA mem2 e)⟩"
    "⟨Stop, mds', mem1 (x := evA mem1 e)⟩ ℛu⇘Γ⇙ ⟨Stop, mds', mem2 (x := evA mem2 e)⟩"
    apply auto
     apply (metis cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.assign)
    by (rule ℛ.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 ↦ t)"
  have "⟨x ← e, mds, mem2⟩ ↝ ⟨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)⟩ ℛ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 assign2(1))
  next
    show "mem1 (x := evA mem1 e) =⇘?Γ'⇙ mem2 (x := evA mem2 e)"
      unfolding tyenv_eq_def
    proof (auto)
      assume "to_total (Γ(x ↦ t)) x = Low"
      with ‹Γ ⊢a e ∈ t› have "⋀ x. x ∈ aexp_vars e ⟹ to_total Γ x = Low"
        by (metis assign2.prems(1) domI fun_upd_same option.sel 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 ↦ 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 ← e, mds, mem2⟩ ↝ ⟨Stop, mds', mem2 (x := evA mem2 e)⟩"
    "⟨Stop, mds', mem1 (x := evA mem1 e)⟩ ℛu⇘Γ(x ↦ t)⇙ ⟨Stop, mds', mem2 (x := evA mem2 e)⟩"
    using ℛ.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⟩) ∈ ℛ Γ'"
    apply (rule intro1)
    apply clarify
    apply (rule ℛ1.intro [where Γ = Γ and Γ' = Γ'])
      apply (auto simp: if_type)
    by (metis (lifting) if_elim if_type(2) if_type(4) 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⟩ ↝ ⟨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 if_type(8))
       apply (metis if_elim if_type(8))
      apply (subgoal_tac "c1' = el")
       apply (metis (opaque_lifting, mono_tags) cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.if_false if_type(8))
      by (metis if_elim if_type(8))
    thus ?thesis
      by (metis ‹⟨c1', mds, mem1⟩ ℛu⇘Γ'⇙ ⟨c1', mds, mem2⟩› if_elim if_type(8))
  qed
  have "mem1 =⇘mds⇙l mem2"
    apply (auto simp: low_mds_eq_def mds_consistent_def)
    apply (subgoal_tac "x ∉ dom Γ")
     apply (metis if_type(7) to_total_def tyenv_eq_def)
    by (metis (lifting, mono_tags) CollectD Sec.simps(2) if_type(6) mds_consistent_def)
  obtain t where "Γ ⊢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 ‹Γ ⊢b e ∈ t›)
      from neq show ?thesis
      proof (cases "evB mem1 e")
        assume "evB mem1 e"
        hence "c1' = th"
          by (metis (lifting) if_elim if_type(8))
        hence "⟨If e th el, mds, mem2⟩ ↝ ⟨el, mds, mem2⟩"
          by (metis ‹evB mem1 e› cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.if_false if_type(8) neq)
        moreover
        with ‹mem1 =⇘mds⇙l 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 ‹Γ ⊢b e ∈ t›)
        have "⟨th, mds, mem1⟩ ℛ2⇘Γ'⇙ ⟨el, mds, mem2⟩"
          by (metis (lifting) ℛ2.intro ‹∀x∈dom Γ'. Γ' x = Some High› ‹⟨th, mds, mem1⟩ ≈ ⟨el, mds, mem2⟩› if_type(2) if_type(4) if_type(6))
        ultimately show ?thesis
          using ℛ.intro2
          apply clarify
          by (metis ‹c1' = th› if_elim 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⟩ ↝ ⟨th, mds, mem2⟩"
          by (metis (opaque_lifting, mono_tags) ‹¬ evB mem1 e› cxt_to_stmt.simps(1) evalw.unannotated evalw_simple.if_true if_type(8) neq)
        moreover
        from ‹th ∼⇘mds⇙ el› have "el ∼⇘mds⇙ th"
          by (metis low_indistinguishable_sym)
        with ‹mem1 =⇘mds⇙l 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 ‹Γ ⊢b e ∈ t›)
        have "⟨el, mds, mem1⟩ ℛ2⇘Γ'⇙ ⟨th, mds, mem2⟩"
          apply (rule ℛ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 ℛ.intro2
          apply clarify
          by (metis ‹c1' = el› if_elim 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 ‹Γ ⊢b e ∈ t› type_low_vars_low_b)
      by (metis (lifting) ‹Γ ⊢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⟩ ↝ ⟨c1', mds, mem2⟩"
    by (metis cxt_to_stmt.simps(1) evalw_simplep.while evalwp.unannotated evalwp_evalw_eq)
  moreover
  have "⟨c1', mds, mem1⟩ ℛ1⇘Γ⇙ ⟨c1', mds, mem2⟩"
    apply (rule ℛ1.intro [where Γ = Γ])
      apply (auto simp: while_type)
    apply (rule if_type)
      apply (metis (lifting) Sec.simps(1) while_type(1) type_bexpr_elim)
     apply (rule seq_type [where Γ' = Γ])
      by (auto simp: while_type)
  ultimately show ?case
    using ℛ.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 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⟩ ↝ ⟨c2', mds', mem2'⟩"
    "⟨c1', mds', mem1'⟩ ℛu⇘Γ1'⇙ ⟨c2', mds', mem2'⟩"
    using sub
    by blast
  moreover
  have "⋀ c1 mds mem1 c2 mem2. ⟨c1, mds, mem1⟩ ℛu⇘Γ1'⇙ ⟨c2, mds, mem2⟩ ⟹
    ⟨c1, mds, mem1⟩ ℛu⇘Γ'⇙ ⟨c2, mds, mem2⟩"
  proof -
    fix c1 mds mem1 c2 mem2
    let ?lc1 = "⟨c1, mds, mem1⟩" and ?lc2 = "⟨c2, mds, mem2⟩"
    assume asm: "?lc1 ℛu⇘Γ1'⇙ ?lc2"
    moreover
    have "?lc1 ℛ1⇘Γ1'⇙ ?lc2 ⟹ ?lc1 ℛ1⇘Γ'⇙ ?lc2"
      apply (erule ℛ1_elim)
      apply auto
      by (metis (lifting) has_type.sub sub(4) stop_cxt stop_type)
    moreover
    have "?lc1 ℛ2⇘Γ1'⇙ ?lc2 ⟹ ?lc1 ℛ2⇘Γ'⇙ ?lc2"
    proof -
      assume r2: "?lc1 ℛ2⇘Γ1'⇙ ?lc2"
      then obtain Λ1 Λ2 where "⊢ Λ1 { c1 }  Γ1'" "⊢ Λ2 { c2 } Γ1'" "mds_consistent mds Λ1"
        "mds_consistent mds Λ2"
        by (metis ℛ2_elim)
      hence "⊢ Λ1 { c1 } Γ'"
        using sub(4)
        by (metis context_le_refl has_type.sub sub(4))
      moreover
      have "⊢ Λ2 { c2 } Γ'"
        by (metis ‹⊢ Λ2 {c2} Γ1'› context_le_refl has_type.sub sub(4))
      moreover
      from r2 have "∀ x ∈ dom Γ1'. Γ1' x = Some High"
        apply (rule ℛ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 sub(4) rev_subsetD option.sel)
      ultimately show ?thesis
        by (metis (no_types) ℛ2.intro ℛ2_elim' ‹mds_consistent mds Λ1› ‹mds_consistent mds Λ2› r2)
    qed
    moreover
    have "?lc1 ℛ3⇘Γ1'⇙ ?lc2 ⟹ ?lc1 ℛ3⇘Γ'⇙ ?lc2"
      apply (erule ℛ3_elim)
      proof -
        fix Γ c1'' c2''' c
        assume [simp]: "c1 = c1'' ;; c" "c2 = c2''' ;; c"
        assume case1: "⊢ Γ {c} Γ1'" "⟨c1'', mds, mem1⟩ ℛ1⇘Γ⇙ ⟨c2''', mds, mem2⟩"
        hence "⊢ Γ {c} Γ'"
          using context_le_refl has_type.sub sub.hyps(4)
          by blast
        with case1 show "⟨c1, mds, mem1⟩ ℛ3⇘Γ'⇙ ⟨c2, mds, mem2⟩"
          using ℛ3_aux.intro1 by simp
      next
        fix Γ c1'' c2''' c''
        assume [simp]: "c1 = c1'' ;; c''" "c2 = c2''' ;; c''"
        assume "⟨c1'', mds, mem1⟩ ℛ2⇘Γ⇙ ⟨c2''', mds, mem2⟩" "⊢ Γ {c''} Γ1'"
        thus "⟨c1, mds, mem1⟩ ℛ3⇘Γ'⇙ ⟨c2, mds, mem2⟩"
          using ℛ3_aux.intro2
          apply simp
          apply (rule ℛ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⟩ ℛ3⇘Γ⇙ ⟨c2''', mds, mem2⟩" "⊢ Γ {c''} Γ1'"
        thus "⟨c1, mds, mem1⟩ ℛ3⇘Γ'⇙ ⟨c2, mds, mem2⟩"
          using ℛ3_aux.intro3
          apply auto
          by (metis (opaque_lifting, no_types) context_le_refl has_type.sub sub.hyps(4))
      qed
    ultimately show "?thesis c1 mds mem1 c2 mem2"
      by (auto simp: ℛ.intros)
  qed
  with c2'_props show ?case
    by blast
qed

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

lemma ℛ_to_ℛ3: "⟦ ⟨c1, mds, mem1⟩ ℛu⇘Γ⇙ ⟨c2, mds, mem2⟩ ; ⊢ Γ { c } Γ' ⟧ ⟹
  ⟨c1 ;; c, mds, mem1⟩ ℛ3⇘Γ'⇙ ⟨c2 ;; c, mds, mem2⟩"
  apply (erule ℛ_elim)
  by auto

lemma ℛ2_implies_typeable: "⟨c1, mds, mem1⟩ ℛ2⇘Γ'⇙ ⟨c2, mds, mem2⟩ ⟹ ∃ Γ1. ⊢ Γ1 { c2 } Γ'"
  apply (erule ℛ2_elim)
  by auto

lemma ℛ3_weak_bisim:
  "weak_bisim (ℛ3 Γ') (ℛ Γ')"
proof -
  {
    fix c1 mds mem1 c2 mem2 c1' mds' mem1'
    assume case3: "(⟨c1, mds, mem1⟩, ⟨c2, mds, mem2⟩) ∈ ℛ3 Γ'"
    assume eval: "⟨c1, mds, mem1⟩ ↝ ⟨c1', mds', mem1'⟩"
    have "∃ c2' mem2'. ⟨c2, mds, mem2⟩ ↝ ⟨c2', mds', mem2'⟩ ∧ ⟨c1', mds', mem1'⟩ ℛu⇘Γ'⇙ ⟨c2', mds', mem2'⟩"
      using case3 eval
      apply simp
      
    proof (induct arbitrary: c1' rule: ℛ3_aux.induct)
      case (intro1 Γ c1 mds mem1 c2 mem2 c Γ')
      hence [simp]: "c2 = c1"
        by (metis (lifting) ℛ1_elim)
      thus ?case
      proof (cases "c1 = Stop")
        assume [simp]: "c1 = Stop"
        from intro1(1) show ?thesis
          apply (rule ℛ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 ℛ.intro1, clarify)
          by (metis (no_types) ℛ1.intro ‹c1 = Stop› context_le_refl intro1.prems intro1(2) seq_stop_elim stop_cxt sub)
      next
        assume "c1 ≠ Stop"
        from intro1
        obtain c1'' where "⟨c1, mds, mem1⟩ ↝ ⟨c1'', mds', mem1'⟩ ∧ c1' = (c1'' ;; c)"
          by (metis ‹c1 ≠ Stop› intro1.prems seq_elim)
        with intro1
        obtain c2'' mem2' where "⟨c2, mds, mem2⟩ ↝ ⟨c2'', mds', mem2'⟩" "⟨c1'', mds', mem1'⟩ ℛu⇘Γ⇙ ⟨c2'', mds', mem2'⟩"
          using ℛ1_weak_bisim and weak_bisim_def
          by blast
        thus ?thesis
          using intro1(2) ℛ_to_ℛ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 ℛ.intro3)
          by (metis (opaque_lifting, no_types) ‹⟨c1, mds, mem1⟩ ↝ ⟨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) ℛ2_elim')
        from intro2 obtain Γ1 where "⊢ Γ1 { c2 } Γ"
          by (metis ℛ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⟩ ↝ ⟨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 ℛ2_elim)
          apply (simp add: mds_consistent_def)
          by (metis context_le_def stop_cxt)
        moreover
        from bisim have "mem1 =⇘mds⇙l mem2"
          by (auto simp: mm_equiv.simps strong_low_bisim_mm_def)
        have "∀ x ∈ dom Γ. Γ x = Some High"
          using intro2(1)
          by (metis ℛ2_elim')
        hence "mem1 =⇘Γ⇙ mem2"
          using ‹mds_consistent mds Γ› ‹mem1 =⇘mds⇙l 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 option.sel to_total_def)
        ultimately have "⟨cn, mds, mem1⟩ ℛ1⇘Γ'⇙ ⟨cn, mds, mem2⟩"
          by (metis (lifting) ℛ1.intro intro2(2))
        thus "?thesis"
          using ℛ.intro1
          apply auto
          by (metis ‹⟨c2 ;; cn, mds, mem2⟩ ↝ ⟨cn, mds', mem2⟩› ‹c2 = Stop› ‹mds' = mds›)
      next
        assume "c1 ≠ Stop"
        then obtain c1''' where "c1' = c1''' ;; cn" "⟨c1, mds, mem1⟩ ↝ ⟨c1''', mds', mem1'⟩"
          by (metis (no_types) intro2.prems seq_elim)
        then obtain c2''' mem2' where c2'''_props:
          "⟨c2, mds, mem2⟩ ↝ ⟨c2''', mds', mem2'⟩ ∧
          ⟨c1''', mds', mem1'⟩ ℛ2⇘Γ⇙ ⟨c2''', mds', mem2'⟩"
          using ℛ2_bisim_step intro2
          by blast
        let ?c2' = "c2''' ;; cn"
        from c2'''_props have "⟨c2 ;; cn, mds, mem2⟩ ↝ ⟨?c2', mds', mem2'⟩"
          by (metis (lifting) intro2 evalw.seq)
        moreover
        have "(⟨c1''' ;; cn, mds', mem1'⟩, ⟨?c2', mds', mem2'⟩) ∈ ℛ3 Γ'"
          by (metis (lifting) ℛ3_aux.intro2 c2'''_props intro2(2) mem_Collect_eq case_prodI)
        ultimately show ?thesis
          using ℛ.intro3
          by (metis (lifting) ℛ3_aux.intro2 ‹c1' = c1''' ;; cn› c2'''_props 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⟩ ↝ ⟨c1'', mds', mem1'⟩" "c1' = (c1'' ;; c)"
          by (metis intro3.prems seq_elim)
        then obtain c2'' mem2' where "⟨c2, mds, mem2⟩ ↝ ⟨c2'', mds', mem2'⟩" "⟨c1'', mds', mem1'⟩ ℛu⇘Γ⇙ ⟨c2'', mds', mem2'⟩"
          using intro3(2) mem_Collect_eq case_prodI
          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 ℛ_elim)
            apply simp_all
            apply (metis ℛ.intro3 ℛ_to_ℛ3 ‹⟨c1'', mds', mem1'⟩ ℛu⇘Γ⇙ ⟨c2'', mds', mem2'⟩› ‹c1' = c1'' ;; c› intro3(3))
           apply (metis (lifting) ℛ.intro3 ℛ_to_ℛ3 ‹⟨c1'', mds', mem1'⟩ ℛu⇘Γ⇙ ⟨c2'', mds', mem2'⟩› ‹c1' = c1'' ;; c› intro3(3))
          by (metis (lifting) ℛ.intro3 ℛ3_aux.intro3 ‹c1' = c1'' ;; c› intro3(3))
      qed
    qed
  }
  thus ?thesis
    unfolding weak_bisim_def
    by auto
qed

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

lemma Typed_in_ℛ:
  assumes typeable: "⊢ Γ { c } Γ'"
  assumes mds_cons: "mds_consistent mds Γ"
  assumes mem_eq: "∀ x. to_total Γ x = Low ⟶ mem1 x = mem2 x"
  shows "⟨c, mds, mem1⟩ ℛu⇘Γ'⇙ ⟨c, mds, mem2⟩"
  apply (rule ℛ.intro1 [of Γ'])
  apply clarify
  apply (rule ℛ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 ℛ1 *)
theorem type_soundness:
  assumes well_typed: "⊢ Γ { 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 ℛ_bisim Typed_in_ℛ
  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"
  (‹⊢ _› [120] 1000)
  where
  "⟦ list_all (λ c. ⊢ Γ0 { c } Γ0) cs ;
     ∀ mem. sound_mode_use (add_initial_modes cs, mem) ⟧ ⟹
    type_global cs"

inductive_cases type_global_elim: "⊢ cs"

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

lemma typed_secure:
  "⟦ ⊢ Γ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: "⊢ 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