Theory TypeSystem

(*
Title: Value-Dependent SIFUM-Type-Systems
Authors: Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
(Based on the SIFUM-Type-Systems AFP entry, whose authors
 are: Sylvia Grewe, Heiko Mantel, Daniel Schoepe)
*)
section ‹Type System for Ensuring SIFUM-Security of Commands›

theory TypeSystem
imports Compositionality Language
begin

subsection ‹Typing Rules›

text ‹
  Types now depend on memories. To see why, consider an assignment in which some variable
  @{term x} for which we have a @{term AsmNoReadOrWrite} assumption is assigned the value in 
  variable @{term input}, but where @{term input}'s classification depends on some control
  variable. Then the new type of @{term x} depends on memory. If we were to just take the 
  upper bound of @{term input}'s classification, this would likely give us @{term High} as
  @{term x}'s type, but that would prevent us from treating @{term x} as @{term Low}
  if we later learn @{term input}'s original classification. 
  
  Instead we need to make @{term x}'s type explicitly depend on memory so later on, once we
  learn @{term input}'s classification, we can resolve @{term x}'s type to a concrete
  security level.
  
  We choose to deeply embed types as sets of boolean expressions. If any expression in the
  set evaluates to @{term True}, the type is @{term High}; otherwise it is @{term Low}.
›
type_synonym 'BExp Type = "'BExp set"

text ‹
  We require @{term Γ} to track all stable (i.e. @{term AsmNoWrite} or @{term AsmNoReadOrWrite}), 
  non-@{term 𝒞} variables.
  
  This differs from Mantel a bit. Mantel would exclude from @{term Γ}, variables
  whose classification (according to @{term dma}) is @{term Low} for which we have only
  an @{term AsmNoWrite} assumption.
  
  We decouple the requirement for inclusion in @{term Γ} from a variable's classification
  so that we don't need to be updating @{term Γ} each time we alter a control variable.
  Even if we tried to keep @{term Γ} up-to-date in that case, we may not be able to 
  precisely compute the new classification of each variable after the modification anyway.
›
type_synonym ('Var,'BExp) TyEnv = "'Var ⇀ 'BExp Type"

text ‹
  This records which variables are \emph{stable} in that we have an assumption
  implying that their value won't change. It duplicates a bit of info in
  @{term Γ} above but I haven't yet thought of a way to remove that duplication
  cleanly.
  
  The first component of the pair records variables for which we have
  @{term AsmNoWrite}; the second component is for @{term AsmNoReadOrWrite}.
  
  The reason we want to distinguish the different kinds of assumptions is to know whether
  a variable should remain in @{term Γ} when we drop an assumption on it. If we drop
  e.g. @{term AsmNoWrite} but also have @{term AsmNoReadOrWrite} then if we didn't track
  stability info this way we wouldn't know whether we had to remove the variable from
  @{term Γ} or not.
›
type_synonym 'Var Stable = "('Var set × 'Var set)"

text ‹
  We track a set of predicates on memories as we execute. If we evaluate a boolean expression
  all of whose variables are stable, then we enrich this set predicate with that one.
  If we assign to a stable variable, then we enrich this predicate also.
  If we release an assumption making a variable unstable, we need to remove all predicates that
  pertain to it from this set.
  
  This needs to be deeply embedded (i.e. it cannot be stored as a predicate of type
  @{typ "('Var,'Val) Mem ⇒ bool"} or even @{typ "('Var,'Val) Mem set"}), because we need to be 
  able to identify each individual predicate and for each predicate identify all of the
  variables in it, so we can discard the right predicates each time a variable becomes unstable.
›
type_synonym 'bexp preds = "'bexp set"

context sifum_lang_no_dma begin

definition
  pred :: "'BExp preds ⇒ ('Var,'Val) Mem ⇒ bool"
where
  "pred P ≡ λmem. (∀p∈P. eval⇩B mem p)"

end

locale sifum_types =
  sifum_lang_no_dma ev⇩A ev⇩B aexp_vars bexp_vars + sifum_security dma 𝒞_vars 𝒞 eval⇩w undefined
  for ev⇩A :: "('Var, 'Val) Mem ⇒ 'AExp ⇒ 'Val"
  and ev⇩B :: "('Var, 'Val) Mem ⇒ 'BExp ⇒ bool"
  and aexp_vars :: "'AExp ⇒ 'Var set"
  and bexp_vars :: "'BExp ⇒ 'Var set"
  and dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
  and 𝒞_vars :: "'Var ⇒ 'Var set"
  and 𝒞 :: "'Var set" +
  (* we need to be able to negate predicates, when we explore the ELSE branch of an IF *)
  fixes bexp_neg :: "'BExp ⇒ 'BExp"
  assumes bexp_neg_negates: "⋀mem e. (ev⇩B mem (bexp_neg e)) = (¬ (ev⇩B mem e))" 
  (* we need to be able to compute a valid postcondition after an assignment *)
  fixes assign_post :: "'BExp preds ⇒ 'Var ⇒ 'AExp ⇒ 'BExp preds"
  assumes assign_post_valid: "⋀mem. pred P mem ⟹ pred (assign_post P x e) (mem(x := ev⇩A mem e))"
  fixes dma_type :: "'Var ⇒ 'BExp set"
  assumes dma_correct:
    "dma mem x = (if (∀e∈dma_type x. ev⇩B mem e) then Low else High)"
  assumes 𝒞_vars_correct:
    "𝒞_vars x = (⋃(bexp_vars ` dma_type x))"
  fixes pred_False :: 'BExp
  assumes pred_False_is_False: "¬ ev⇩B mem pred_False"
  assumes bexp_vars_pred_False: "bexp_vars pred_False = {}"
  

(* a more specialised form of the above locale useful for the examples that provides
   a brain-dead instantiation for the assignment postcondition transformer *)
locale sifum_types_assign =
  sifum_lang_no_dma ev⇩A ev⇩B aexp_vars bexp_vars + sifum_security dma 𝒞_vars 𝒞 eval⇩w undefined
  for ev⇩A :: "('Var, 'Val) Mem ⇒ 'AExp ⇒ 'Val"
  and ev⇩B :: "('Var, 'Val) Mem ⇒ 'BExp ⇒ bool"
  and aexp_vars :: "'AExp ⇒ 'Var set"
  and bexp_vars :: "'BExp ⇒ 'Var set"
  and dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
  and 𝒞_vars :: "'Var ⇒ 'Var set"
  and 𝒞 :: "'Var set" +
  (* we need to be able to negate predicates, when we explore the ELSE branch of an IF *)
  fixes bexp_neg :: "'BExp ⇒ 'BExp"
  assumes bexp_neg_negates: "⋀mem e. (ev⇩B mem (bexp_neg e)) = (¬ (ev⇩B mem e))" 
  fixes dma_type :: "'Var ⇒ 'BExp set"
  assumes dma_correct:
    "dma mem x = (if (∀e∈dma_type x. ev⇩B mem e) then Low else High)"
  assumes 𝒞_vars_correct:
    "𝒞_vars x = (⋃(bexp_vars ` dma_type x))"
  fixes pred_False :: 'BExp
  assumes pred_False_is_False: "¬ ev⇩B mem pred_False"
  assumes bexp_vars_pred_False: "bexp_vars pred_False = {}"
  (* we need to be able to say "variable x has value e" when we assign (the evaluation of e) to x *)
  fixes bexp_assign :: "'Var ⇒ 'AExp ⇒ 'BExp"
  assumes bexp_assign_eval: "⋀mem e x. (ev⇩B mem (bexp_assign x e)) = (mem x = (ev⇩A mem e))"
  assumes bexp_assign_vars: "⋀e x. (bexp_vars (bexp_assign x e)) = aexp_vars e ∪ {x}"

(* things needed by both sifum_types_assign and sifum_types, before we prove the former a sublocale *)
context sifum_lang_no_dma begin

definition
  stable :: "'Var Stable ⇒ 'Var ⇒ bool"
where
  "stable 𝒮 x ≡ x ∈ (fst 𝒮 ∪ snd 𝒮)"

definition
  add_pred :: "'BExp preds ⇒ 'Var Stable ⇒ 'BExp ⇒ 'BExp preds" ("_ +⇩_ _" [120, 120, 120] 1000)
where
  "P +⇩𝒮 e ≡ (if (∀x∈bexp_vars e. stable 𝒮 x) then P ∪ {e} else P)"

lemma add_pred_subset:
  "P ⊆ P +⇩𝒮 p"
  apply(clarsimp simp: add_pred_def)
  done


(* TODO: overloads the syntax for partial functions --- pick something else? *)
definition
  restrict_preds_to_vars :: "'BExp preds ⇒ 'Var set ⇒ 'BExp preds" ("_ |` _" [120, 120] 1000)
where
  "P |` V ≡ {e. e ∈ P ∧ bexp_vars e ⊆ V}"

end

context sifum_types_assign begin


text ‹
  the most simple assignment postcondition transformer
›
definition
  assign_post :: "'BExp preds ⇒ 'Var ⇒ 'AExp ⇒ 'BExp preds"
where
  "assign_post P x e ≡ 
           (if x ∈ (aexp_vars e) then 
              (restrict_preds_to_vars P  (-{x})) 
            else 
              (restrict_preds_to_vars P  (-{x})) ∪ {bexp_assign x e})"
 
end

sublocale sifum_types_assign ⊆ sifum_types _ _ _ _ _ _ _ _ assign_post
  apply(unfold_locales)
     using bexp_neg_negates apply blast
    apply(clarsimp simp: assign_post_def pred_def | safe)+
       using eval_vars_det⇩B
       unfolding restrict_preds_to_vars_def
       apply (metis (mono_tags, lifting) ComplD fun_upd_other mem_Collect_eq singletonI subset_eq)
      unfolding bexp_assign_eval
      using eval_vars_det⇩A
      apply fastforce
     using eval_vars_det⇩B
     apply (metis (mono_tags, lifting) ComplD fun_upd_other mem_Collect_eq singletonI subset_eq)
    using dma_correct apply blast
   using 𝒞_vars_correct pred_False_is_False bexp_vars_pred_False apply blast+
  done

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) ∈ eval⇩w"
  
abbreviation 
  eval_plus_abv :: "(_, 'Var, 'Val) LocalConf ⇒ (_, _, _) LocalConf ⇒ bool"
  (infixl "↝⇧+" 70)
where
  "x ↝⇧+ y ≡ (x, y) ∈ eval⇩w⇧+"
  
abbreviation 
  no_eval_abv :: "(_, 'Var, 'Val) LocalConf ⇒ bool" 
  ("_ ↝ ⊥")
where
  "x ↝ ⊥ ≡ ∀ y. (x, y) ∉ eval⇩w"

abbreviation 
  low_indistinguishable_abv :: "'Var Mds ⇒ ('Var, 'AExp, 'BExp) Stmt ⇒ (_, _, _) Stmt ⇒ bool"
  ("_ ∼ı _" [100, 100] 80)
where
  "c ∼⇘mds⇙ c' ≡ low_indistinguishable mds c c'"


abbreviation
  vars_of_type :: "'BExp Type ⇒ 'Var set"
where
  "vars_of_type t ≡ ⋃(bexp_vars ` t)"
  
definition
  type_wellformed :: "'BExp Type ⇒ bool"
where
  "type_wellformed t ≡ vars_of_type t ⊆ 𝒞"

lemma dma_type_wellformed [simp]:
  "type_wellformed (dma_type x)"
  apply(clarsimp simp: type_wellformed_def  𝒞_def | safe)+
  using 𝒞_vars_correct apply blast
  done
  
definition 
  to_total :: "('Var,'BExp) TyEnv ⇒ 'Var ⇒ 'BExp Type"
where 
  "to_total Γ ≡ λv. if v ∈ dom Γ then the (Γ v) else dma_type v"

definition
  types_wellformed :: "('Var,'BExp) TyEnv ⇒ bool"
where
  "types_wellformed Γ ≡ ∀x∈dom Γ. type_wellformed (the (Γ x))"
  
lemma to_total_type_wellformed:
  "types_wellformed Γ ⟹
  type_wellformed (to_total Γ x)"
  by(auto simp: to_total_def types_wellformed_def)
  
lemma Un_type_wellformed:
  "∀t∈ts. type_wellformed t ⟹ type_wellformed (⋃ ts)"
  apply(clarsimp simp: type_wellformed_def | safe)+
  by(fastforce simp: 𝒞_def elim!: subsetCE)

inductive 
  type_aexpr :: "('Var,'BExp) TyEnv ⇒ 'AExp ⇒ 'BExp Type ⇒ bool" ("_ ⊢⇩a _ ∈ _" [120, 120, 120] 1000)
where
  type_aexpr [intro!]: "Γ ⊢⇩a e ∈ ⋃ (image (λ x. to_total Γ x) (aexp_vars e))"

lemma type_aexprI:
  "t =  ⋃ (image (λ x. to_total Γ x) (aexp_vars e)) ⟹ Γ ⊢⇩a e ∈ t"
  apply(erule ssubst)
  apply(rule type_aexpr.intros)
  done

lemma type_aexpr_type_wellformed:
  "types_wellformed Γ ⟹ Γ ⊢⇩a e ∈ t ⟹ type_wellformed t"
  apply(erule type_aexpr.cases)
  apply(erule ssubst, rule Un_type_wellformed)
  apply clarsimp
  apply(blast intro: to_total_type_wellformed)
  done
  
inductive_cases type_aexpr_elim [elim]: "Γ ⊢⇩a e ∈ t"

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

lemma type_bexprI:
  "t =  ⋃ (image (λ x. to_total Γ x) (bexp_vars e)) ⟹ Γ ⊢⇩b e ∈ t"
  apply(erule ssubst)
  apply(rule type_bexpr.intros)
  done

lemma type_bexpr_type_wellformed:
  "types_wellformed Γ ⟹ Γ ⊢⇩b e ∈ t ⟹ type_wellformed t"
  apply(erule type_bexpr.cases)
  apply(erule ssubst, rule Un_type_wellformed)
  apply clarsimp
  apply(blast intro: to_total_type_wellformed)
  done
  
inductive_cases type_bexpr_elim [elim]: "Γ ⊢⇩b e ∈ t"


text ‹
  Define a sufficient condition for a type to be stable, assuming the type is wellformed.
  
  We need this because there is no point tracking the fact that e.g. variable @{term x}'s data has
  a classification that depends on some control variable @{term c} (where @{term c} might be
  the control variable for some other variable @{term y} whose value we've just assigned to
  @{term x}) if @{term c} can then go and be modified, since now the classification of
  the data in @{term x} no longer depends on the value of @{term c}, instead it depends on
  @{term c}'s \emph{old} value, which has now been lost.
  
  Therefore, if a type depends on @{term c}, then @{term c} had better be stable.
›
abbreviation
  pred_stable :: "'Var Stable ⇒ 'BExp ⇒ bool"
where
  "pred_stable 𝒮 p ≡ ∀x∈bexp_vars p. stable 𝒮 x"

abbreviation
  type_stable :: "'Var Stable ⇒ 'BExp Type ⇒ bool"
where
  "type_stable 𝒮 t ≡ (∀p∈t. pred_stable 𝒮 p)"
  
lemma type_stable_is_sufficient:
  "⟦type_stable 𝒮 t⟧ ⟹
  ∀mem mem'. (∀x. stable 𝒮 x ⟶ mem x = mem' x) ⟶ (ev⇩B mem) ` t = (ev⇩B mem') ` t"
  apply(clarsimp simp: type_wellformed_def image_def)
  apply safe
   using eval_vars_det⇩B apply blast+
  done
  
definition 
  mds_consistent :: "'Var Mds ⇒ ('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ bool"
where 
  "mds_consistent mds Γ 𝒮 P ≡
    (𝒮 = (mds AsmNoWrite, mds AsmNoReadOrWrite)) ∧
    (dom Γ = {x. x ∉ 𝒞 ∧ stable 𝒮 x}) ∧
    (∀p ∈ P. pred_stable 𝒮 p)"

fun 
  add_anno_dom :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'Var ModeUpd ⇒ 'Var set"
where
  "add_anno_dom Γ 𝒮 (Acq v AsmNoReadOrWrite) = (if v ∉ 𝒞 then dom Γ ∪ {v} else dom Γ)" |
  "add_anno_dom Γ 𝒮 (Acq v AsmNoWrite) = (if v ∉ 𝒞 then dom Γ ∪ {v} else dom Γ)" |
  "add_anno_dom Γ 𝒮 (Acq v _) = dom Γ" |
  "add_anno_dom Γ 𝒮 (Rel v AsmNoReadOrWrite) = (if v ∉ fst 𝒮 then dom Γ - {v} else dom Γ)" |
  "add_anno_dom Γ 𝒮 (Rel v AsmNoWrite) = (if v ∉ snd 𝒮 then dom Γ - {v} else dom Γ)" |
  "add_anno_dom Γ 𝒮 (Rel v _) = dom Γ"

definition 
  add_anno :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'Var ModeUpd ⇒ ('Var,'BExp) TyEnv" ("_ ⊕⇩_ _" [120, 120, 120] 1000)
where
  "Γ ⊕⇩𝒮 upd = restrict_map (λx. Some (to_total Γ x)) (add_anno_dom Γ 𝒮 upd)"

lemma add_anno_acq_AsmNoReadOrWrite_idemp [simp]:
  "v ∈ dom Γ ∨ v ∈ 𝒞 ⟹ Γ ⊕⇩𝒮 (Acq v AsmNoReadOrWrite) = Γ"
  apply(safe | clarsimp simp: add_anno_def to_total_def)+
    apply(rule ext)
    apply(clarsimp simp: restrict_map_def | safe)+
    apply(case_tac "Γ x", fastforce+)[5]
   apply(rule ext)
   apply(clarsimp simp: restrict_map_def | safe)+
   apply(case_tac "Γ x", fastforce+)
  apply(safe | clarsimp simp: add_anno_def to_total_def)+
  apply(rule ext)
  apply(clarsimp simp: restrict_map_def | safe)+
  apply(case_tac "Γ x", fastforce+)
  done

lemma add_anno_rel_AsmNoReadOrWrite_idemp [simp]:
  "⟦v ∉ dom Γ; v ∉ fst 𝒮⟧ ⟹ Γ ⊕⇩𝒮 (Rel v AsmNoReadOrWrite) = Γ"
  apply(subgoal_tac "v ∉ dom Γ")
   apply(safe | clarsimp simp: add_anno_def to_total_def)+
  apply(clarsimp simp: restrict_map_def | safe)+
  apply(erule_tac P="(λx. if x ∈ dom Γ ∧ x ≠ v
          then Some (if x ∈ dom Γ then the (Γ x) else dma_type x) else None) = Γ" in notE)
  apply(rule ext)
  apply(case_tac "Γ x", fastforce+)
  done

lemma add_anno_acq_AsmNoReadOrWrite [simp]:
  assumes notin [simp]: "v ∉ dom Γ"
  shows "v ∉ 𝒞 ⟹ Γ ⊕⇩𝒮 (Acq v AsmNoReadOrWrite) = (Γ(v ↦ dma_type v))"
  apply(safe | clarsimp simp: add_anno_def to_total_def)+
  apply(clarsimp simp: restrict_map_def | safe)+
  apply(rule ext)
  apply(auto intro: sym)
  done

lemma add_anno_rel_AsmNoReadOrWrite [simp]:
  assumes isin [simp]: "v ∈ dom Γ"
  shows "v ∉ fst 𝒮 ⟹ Γ ⊕⇩𝒮 (Rel v AsmNoReadOrWrite) = restrict_map Γ ((dom Γ) - {v})"
  apply(safe | clarsimp simp: add_anno_def to_total_def)+
  apply(clarsimp simp: restrict_map_def | safe)+
  apply(rule ext)
  apply(auto intro: sym)
  done

lemma add_anno_acq_AsmNoWrite_idemp [simp]:
  "v ∈ dom Γ ∨ v ∈ 𝒞 ⟹ Γ ⊕⇩𝒮 (Acq v AsmNoWrite) = Γ"
  apply(safe | clarsimp simp: add_anno_def to_total_def)+
    apply(rule ext)
    apply(clarsimp simp: restrict_map_def | safe)+
    apply(case_tac "Γ x", fastforce+)[5]
   apply(rule ext)
   apply(clarsimp simp: restrict_map_def | safe)+
   apply(case_tac "Γ x", fastforce+)
  apply(safe | clarsimp simp: add_anno_def to_total_def)+
  apply(rule ext)
  apply(clarsimp simp: restrict_map_def | safe)+
  apply(case_tac "Γ x", fastforce+)
  done

lemma add_anno_rel_AsmNoWrite_idemp [simp]:
  "⟦v ∉ dom Γ; v ∉ snd 𝒮⟧ ⟹ Γ ⊕⇩𝒮 (Rel v AsmNoWrite) = Γ"
  apply(subgoal_tac "v ∉ dom Γ")
   apply(safe | clarsimp simp: add_anno_def to_total_def)+
  apply(clarsimp simp: restrict_map_def | safe)+
  apply(erule_tac P="(λx. if x ∈ dom Γ ∧ x ≠ v
          then Some (if x ∈ dom Γ then the (Γ x) else dma_type x) else None) = Γ" in notE)
  apply(rule ext)
  apply(case_tac "Γ x", fastforce+)
  done

lemma add_anno_acq_AsmNoWrite [simp]:
  assumes notin [simp]: "v ∉ dom Γ"
  shows "v ∉ 𝒞 ⟹ Γ ⊕⇩𝒮 (Acq v AsmNoWrite) = (Γ(v ↦ dma_type v))"
  apply(safe | clarsimp simp: add_anno_def to_total_def)+
  apply(clarsimp simp: restrict_map_def | safe)+
  apply(rule ext)
  apply(auto intro: sym)
  done

lemma add_anno_rel_AsmNoWrite [simp]:
  assumes isin [simp]: "v ∈ dom Γ"
  shows "v ∉ snd 𝒮 ⟹ Γ ⊕⇩𝒮 (Rel v AsmNoWrite) = restrict_map Γ ((dom Γ) - {v})"
  apply(safe | clarsimp simp: add_anno_def to_total_def)+
  apply(clarsimp simp: restrict_map_def | safe)+
  apply(rule ext)
  apply(auto intro: sym)
  done
  
fun 
  add_anno_stable :: "'Var Stable ⇒ 'Var ModeUpd ⇒ 'Var Stable"
where
  "add_anno_stable 𝒮 (Acq v AsmNoReadOrWrite) = (fst 𝒮, snd 𝒮 ∪ {v})" |
  "add_anno_stable 𝒮 (Acq v AsmNoWrite) = (fst 𝒮 ∪ {v}, snd 𝒮)" |
  "add_anno_stable 𝒮 (Acq v _) = 𝒮" |
  "add_anno_stable 𝒮 (Rel v AsmNoReadOrWrite) = (fst 𝒮, snd 𝒮 - {v})" |
  "add_anno_stable 𝒮 (Rel v AsmNoWrite) = (fst 𝒮 - {v}, snd 𝒮)" |
  "add_anno_stable 𝒮 (Rel v _) = 𝒮"

definition
  pred_entailment :: "'BExp preds ⇒ 'BExp preds ⇒ bool" (infix "⊢" 70)
where
  "P ⊢ P' ≡ ∀mem. pred P mem ⟶ pred P' mem"

text ‹
  We give a predicate interpretation of subtype and then prove it has the correct
  semantic property.
›
definition
  subtype :: "'BExp Type ⇒ 'BExp preds ⇒ 'BExp Type ⇒ bool" ("_ ≤:⇩_ _" [120, 120, 120] 1000)
where
  "t ≤:⇩P t' ≡ (P ∪ t') ⊢ t"

definition
  type_max :: "'BExp Type ⇒ ('Var,'Val) Mem ⇒ Sec"
where
  "type_max t mem ≡ if (∀p∈t. ev⇩B mem p) then Low else High"

lemma type_stable_is_sufficient':
  "⟦type_stable 𝒮 t⟧ ⟹
  ∀mem mem'. (∀x. stable 𝒮 x ⟶ mem x = mem' x) ⟶ type_max t mem = type_max t mem'"
  using type_stable_is_sufficient
  unfolding type_max_def image_def
  by (metis (no_types, lifting) eval_vars_det⇩B)

lemma subtype_sound:
  "t ≤:⇩P t' ⟹ ∀mem. pred P mem ⟶ type_max t mem ≤ type_max t' mem"
  apply(fastforce simp: subtype_def pred_entailment_def pred_def type_max_def less_eq_Sec_def)
  done

lemma subtype_complete:
  assumes a: "⋀mem. pred P mem ⟹ type_max t mem ≤ type_max t' mem"
  shows "t ≤:⇩P t'"
unfolding subtype_def pred_entailment_def
proof (clarify)
  fix mem
  assume p: "pred (P ∪ t') mem"
  hence "pred P mem"
    unfolding pred_def by blast
  with a have tmax: "type_max t mem ≤ type_max t' mem" by blast
  from p have t': "pred t' mem"
    unfolding pred_def by blast
  from t' have "type_max t' mem = Low"
    unfolding type_max_def pred_def by force
  with tmax have "type_max t mem ≤ Low"
    by simp
  hence "type_max t mem = Low"
    unfolding less_eq_Sec_def by blast
  thus "pred t mem"
    unfolding type_max_def pred_def by (auto split: if_splits)
qed

lemma subtype_correct:
  "(t ≤:⇩P t')  = (∀mem. pred P mem ⟶ type_max t mem ≤ type_max t' mem)"
  apply(rule iffI)
   apply(simp add: subtype_sound)
  apply(simp add: subtype_complete)
  done

definition
  type_equiv :: "'BExp Type ⇒ 'BExp preds ⇒ 'BExp Type ⇒ bool" ("_ =:⇩_ _" [120, 120, 120] 1000)
where
  "t =:⇩P t' ≡ t ≤:⇩P t' ∧ t' ≤:⇩P t"
  

lemma subtype_refl [simp]:
  "t ≤:⇩P t"
  by(simp add: subtype_def pred_entailment_def pred_def)

lemma type_equiv_refl [simp]:
  "t =:⇩P t"
  by (simp add: type_equiv_def)
  
definition
  anno_type_stable :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'Var ModeUpd ⇒ bool"
where
  "anno_type_stable Γ 𝒮 upd ≡ (case upd of (Rel v m) ⇒
                                 (v ∈ 𝒞 ∧ v ∉ add_anno_dom Γ 𝒮 upd) ⟶
                                    (∀x∈dom Γ. v ∉ vars_of_type (the (Γ x)))
                                          | (Acq v m) ⇒ 
                                    (v ∉ 𝒞 ∧ v∈add_anno_dom Γ 𝒮 upd - dom Γ) ⟶
                                      (∀x∈𝒞_vars v. stable 𝒮 x))"

definition
  anno_type_sec :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒  'BExp preds ⇒ 'Var ModeUpd ⇒ bool"
where
  "anno_type_sec Γ 𝒮 P upd ≡ (case upd of (Rel v AsmNoReadOrWrite) ⇒
                                (v ∈ add_anno_dom Γ 𝒮 upd ⟶ (the (Γ v)) ≤:⇩P (dma_type v))
                                          |  _ ⇒ True)"

definition
  types_stable :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ bool"
where
  "types_stable Γ 𝒮 ≡ ∀x∈dom Γ. type_stable 𝒮 (the (Γ x))"
  
definition
  tyenv_wellformed :: "'Var Mds ⇒ ('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ bool"
where
  "tyenv_wellformed mds Γ 𝒮 P ≡ 
      mds_consistent mds Γ 𝒮 P ∧
      types_wellformed Γ ∧ types_stable Γ 𝒮"

lemma subset_entailment:
  "P' ⊆ P ⟹ P ⊢ P'"
  apply(auto simp: pred_entailment_def pred_def)
  done

lemma pred_entailment_refl [simp]:
  "P ⊢ P"
  by(simp add: pred_entailment_def)

lemma pred_entailment_mono:
  "P ⊢ P' ⟹ P ⊆ P'' ⟹ P'' ⊢ P'"
  by(auto simp: pred_entailment_def pred_def)
  
lemma type_equiv_subset:
  "type_equiv t P t' ⟹ P ⊆ P' ⟹ type_equiv t P' t'"
  apply(auto simp: type_equiv_def subtype_def intro: pred_entailment_mono)
  done
  
definition
  context_equiv :: "('Var,'BExp) TyEnv ⇒ 'BExp preds ⇒ ('Var,'BExp) TyEnv ⇒ bool" ("_ =:⇩_ _" [120, 120, 120] 1000)
where
  "Γ =:⇩P Γ' ≡ dom Γ = dom Γ' ∧
                           (∀x∈dom Γ'. type_equiv (the (Γ x)) P (the (Γ' x)))"

lemma context_equiv_refl[simp]:
  "context_equiv Γ P Γ"
  by(simp add: context_equiv_def)

lemma context_equiv_subset:
  "context_equiv Γ P Γ' ⟹ P ⊆ P' ⟹ context_equiv Γ P' Γ'"
  apply(auto simp: context_equiv_def intro: type_equiv_subset)
  done

lemma pred_entailment_trans:
  "P ⊢ P' ⟹ P' ⊢ P'' ⟹ P ⊢ P''"
  by(auto simp: pred_entailment_def)

lemma pred_un [simp]:
  "pred (P ∪ P') mem = (pred P mem ∧ pred P' mem)"
  apply(auto simp: pred_def)
  done
  
lemma pred_entailment_un:
  "P ⊢ P' ⟹ P ⊢ P'' ⟹ P ⊢ (P' ∪ P'')"
  apply(subst pred_entailment_def)
  apply clarsimp
  apply(fastforce simp: pred_entailment_def)
  done

lemma pred_entailment_mono_un:
  "P ⊢ P' ⟹ (P ∪ P'') ⊢ (P' ∪ P'')"
  apply(auto simp: pred_entailment_def pred_def)
  done
  
lemma subtype_trans:
  "t ≤:⇩P t' ⟹ t' ≤:⇩P' t'' ⟹ P ⊢ P' ⟹ t ≤:⇩P t''"
  "t ≤:⇩P' t' ⟹ t' ≤:⇩P t'' ⟹ P ⊢ P' ⟹ t ≤:⇩P t''"
   apply(clarsimp simp: subtype_def)
   apply(rule pred_entailment_trans)
    prefer 2
    apply assumption
   apply(rule pred_entailment_un)
    apply(blast intro: subset_entailment)
   apply(rule pred_entailment_trans)
    prefer 2
    apply assumption
   apply(blast intro: pred_entailment_mono_un)
  apply(clarsimp simp: subtype_def)
  apply(rule pred_entailment_trans)
   prefer 2
   apply assumption
  apply(rule pred_entailment_un)
   apply(blast intro: pred_entailment_mono)
  apply(blast intro: subset_entailment)
  done
  
lemma type_equiv_trans:
  "type_equiv t P t' ⟹ type_equiv t' P' t'' ⟹ P ⊢ P' ⟹ type_equiv t P t''"
  apply(auto simp: type_equiv_def intro: subtype_trans)
  done

lemma context_equiv_trans:
  "context_equiv Γ P Γ' ⟹ context_equiv Γ' P' Γ'' ⟹ P ⊢ P' ⟹ context_equiv Γ P Γ''"
  apply(force simp: context_equiv_def intro: type_equiv_trans)
  done

lemma un_pred_entailment_mono:
  "(P ∪ P') ⊢ P'' ⟹ P''' ⊢ P ⟹ (P''' ∪ P') ⊢ P''"
  unfolding pred_entailment_def pred_def
  apply blast
  done
  
lemma subtype_entailment:
  "t ≤:⇩P t' ⟹ P' ⊢ P ⟹ t ≤:⇩P' t'"
  apply(auto simp: subtype_def intro: un_pred_entailment_mono)
  done
  
lemma type_equiv_entailment:
  "type_equiv t P t' ⟹ P' ⊢ P ⟹ type_equiv t P' t'"
  apply(auto simp: type_equiv_def intro: subtype_entailment)  
  done
  
lemma context_equiv_entailment:
  "context_equiv Γ P Γ' ⟹ P' ⊢ P ⟹ context_equiv Γ P' Γ'"
  apply(auto simp: context_equiv_def intro: type_equiv_entailment)
  done


  
  
inductive 
  has_type :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ ('Var, 'AExp, 'BExp) Stmt ⇒ ('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ bool"
  ("⊢ _,_,_ {_} _,_,_" [120, 120, 120, 120, 120, 120, 120] 1000)
where
  stop_type [intro]: "⊢ Γ,𝒮,P {Stop} Γ,𝒮,P" |
  skip_type [intro] : "⊢ Γ,𝒮,P {Skip} Γ,𝒮,P" |
  assign⇩𝒞 : 
  "⟦x ∈ 𝒞; Γ ⊢⇩a e ∈ t; P ⊢ t; (∀v∈dom Γ. x ∉ vars_of_type (the (Γ v))); 
    P' = restrict_preds_to_vars (assign_post P x e) {v. stable 𝒮 v}; 
    ∀v. x ∈ 𝒞_vars v ∧ v ∉ snd 𝒮 ⟶ P ⊢ (to_total Γ v) ∧ 
                                      (to_total Γ v) ≤:⇩P' (dma_type v) ⟧ ⟹ 
   ⊢ Γ,𝒮,P {x ← e} Γ,𝒮,P'" | 
  assign⇩1 : 
  "⟦ x ∉ dom Γ ; x ∉ 𝒞; Γ ⊢⇩a e ∈ t; t ≤:⇩P (dma_type x); 
     P' = restrict_preds_to_vars (assign_post P x e)  {v. stable 𝒮 v} ⟧ ⟹ 
   ⊢ Γ,𝒮,P {x ← e} Γ,𝒮,P'" |
  assign⇩2 : 
  "⟦ x ∈ dom Γ ; Γ ⊢⇩a e ∈ t;  type_stable 𝒮 t; P' = restrict_preds_to_vars (assign_post P x e) {v. stable 𝒮 v}; 
     x ∉ snd 𝒮 ⟶ t ≤:⇩P' (dma_type x) ⟧ ⟹ 
   has_type Γ 𝒮 P (x ← e) (Γ (x := Some t)) 𝒮 P'" |
  if_type [intro]: 
  "⟦ Γ ⊢⇩b e ∈ t; P ⊢ t; 
     ⊢ Γ,𝒮,(P +⇩𝒮 e) { c⇩1 } Γ',𝒮',P'; ⊢ Γ,𝒮,(P +⇩𝒮 (bexp_neg e)) { c⇩2 } Γ'',𝒮',P''; 
     context_equiv Γ' P' Γ'''; context_equiv Γ'' P'' Γ'''; P' ⊢ P'''; P'' ⊢ P'''; 
     ∀mds. tyenv_wellformed mds Γ' 𝒮' P' ⟶ tyenv_wellformed mds Γ''' 𝒮' P'''; 
     ∀mds. tyenv_wellformed mds Γ'' 𝒮' P'' ⟶ tyenv_wellformed mds Γ''' 𝒮' P''' ⟧ ⟹ 
   ⊢ Γ,𝒮,P { If e c⇩1 c⇩2 } Γ''',𝒮',P'''" | 
  while_type [intro]: "⟦ Γ ⊢⇩b e ∈ t ; P ⊢ t; ⊢ Γ,𝒮,(P +⇩𝒮 e) { c } Γ,𝒮,P ⟧ ⟹ ⊢ Γ,𝒮,P { While e c } Γ,𝒮,P" |
  anno_type [intro]: "⟦ Γ' = Γ ⊕⇩𝒮 upd ; 𝒮' = add_anno_stable 𝒮 upd; P' = restrict_preds_to_vars P {v. stable 𝒮' v};
                 ⊢ Γ',𝒮',P' { c } Γ'',𝒮'',P'' ; c ≠ Stop ;
                 (⋀ x. (to_total Γ x) ≤:⇩P' (to_total Γ' x));
                 anno_type_stable Γ 𝒮 upd; anno_type_sec Γ 𝒮 P upd⟧ ⟹ ⊢ Γ,𝒮,P { c@[upd] } Γ'',𝒮'',P''" |
  seq_type [intro]: "⟦ ⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P' ; ⊢ Γ',𝒮',P' { c⇩2 } Γ'',𝒮'',P'' ⟧ ⟹ ⊢ Γ,𝒮,P { c⇩1 ;; c⇩2 } Γ'',𝒮'',P''" |
  sub : "⟦ ⊢ Γ⇩1,𝒮,P⇩1 { c } Γ⇩1',𝒮',P⇩1' ; context_equiv Γ⇩2 P⇩2 Γ⇩1 ; (∀mds. tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ⟶ tyenv_wellformed mds Γ⇩1 𝒮 P⇩1);
           (∀mds. tyenv_wellformed mds Γ⇩1' 𝒮' P⇩1' ⟶ tyenv_wellformed mds Γ⇩2' 𝒮' P⇩2'); context_equiv Γ⇩1' P⇩1' Γ⇩2'; P⇩2 ⊢ P⇩1; P⇩1' ⊢ P⇩2' ⟧ ⟹ ⊢ Γ⇩2,𝒮,P⇩2 { c } Γ⇩2',𝒮',P⇩2'" |
 await_type [intro]: 
  "⟦ Γ ⊢⇩b e ∈ t; P ⊢ t; 
     ⊢ Γ,𝒮,(P +⇩𝒮 e) { c } Γ',𝒮',P' ⟧ ⟹ 
   ⊢ Γ,𝒮,P { Await e c } Γ',𝒮',P'"

lemma sub':
  "⟦ context_equiv Γ⇩2 P⇩2 Γ⇩1 ;
    (∀mds. tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ⟶ tyenv_wellformed mds Γ⇩1 𝒮 P⇩1);
    (∀mds. tyenv_wellformed mds Γ⇩1' 𝒮' P⇩1' ⟶ tyenv_wellformed mds Γ⇩2' 𝒮' P⇩2');
    context_equiv Γ⇩1' P⇩1' Γ⇩2';
    P⇩2 ⊢ P⇩1;
    P⇩1' ⊢ P⇩2';
    ⊢ Γ⇩1,𝒮,P⇩1 { c } Γ⇩1',𝒮',P⇩1' ⟧ ⟹
  ⊢ Γ⇩2,𝒮,P⇩2 { c } Γ⇩2',𝒮',P⇩2'"
  by(rule sub)

lemma assign⇩2_helper:
  "⟦Γ x = Some t; has_type Γ 𝒮 P (x ← e) (Γ(x ↦ t)) 𝒮 P'⟧ ⟹ has_type Γ 𝒮 P (x ← e) Γ 𝒮 P'"
  by (simp add:map_upd_triv)

lemma conc':
  "⟦ ⊢ Γ⇩1,𝒮,P { c } Γ',𝒮',P'; 
    Γ⇩1 = (Γ⇩2(x ↦ t)); 
    x ∈ dom Γ⇩2; 
    type_equiv (the (Γ⇩2 x)) P t; 
    type_wellformed t; 
    type_stable 𝒮 t  ⟧ ⟹ 
  ⊢ Γ⇩2,𝒮,P { c } Γ',𝒮',P'"  
  apply(erule sub)
      apply(fastforce simp: context_equiv_def)
     apply(clarsimp simp: tyenv_wellformed_def mds_consistent_def)
     apply(rule conjI)
      apply fastforce
     apply(rule conjI)
      apply(fastforce simp: types_wellformed_def)
     apply(fastforce simp: types_stable_def)
     apply blast
    apply simp+
  done

lemma tyenv_wellformed_subset:
  "tyenv_wellformed mds Γ 𝒮 P ⟹ P' ⊆ P ⟹ tyenv_wellformed mds Γ 𝒮 P'"
  apply(auto simp: tyenv_wellformed_def mds_consistent_def)
  done

lemma if_type':
  "⟦ Γ ⊢⇩b e ∈ t; 
    P ⊢ t; 
    ⊢ Γ,𝒮,(P +⇩𝒮 e) { c⇩1 } Γ',𝒮',P'; 
    ⊢ Γ,𝒮,(P +⇩𝒮 (bexp_neg e)) { c⇩2 } Γ',𝒮',P''; 
    P''' ⊆ P' ∩ P'' ⟧ ⟹ 
  ⊢ Γ,𝒮,P { If e c⇩1 c⇩2 } Γ',𝒮',P'''"
  apply(erule (3) if_type)
       apply(rule context_equiv_refl)
      apply(rule context_equiv_refl)
     apply(blast intro: subset_entailment)+
   apply(blast intro: tyenv_wellformed_subset)+
  done

lemma skip_type':
  "⟦Γ = Γ'; 𝒮 = 𝒮'; P = P'⟧ ⟹ ⊢ Γ,𝒮,P {Skip} Γ',𝒮',P'"
  using skip_type by simp

text ‹
  Some helper lemmas to discharge the assumption of the @{thm anno_type} rule.
›
lemma anno_type_helpers [simp]:
  "(to_total Γ x) ≤:⇩P (to_total (add_anno Γ 𝒮 (buffer +=⇩m AsmNoWrite)) x)"
  "(to_total Γ x) ≤:⇩P (to_total (add_anno Γ 𝒮 (buffer +=⇩m AsmNoReadOrWrite)) x)"
  apply(auto simp: to_total_def add_anno_def subtype_def intro: subset_entailment)
  done

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.›


inductive_cases has_type_elim: "⊢ Γ,𝒮,P { c } Γ',𝒮',P'"
inductive_cases has_type_stop_elim: "⊢ Γ,𝒮,P { Stop } Γ',𝒮',P'"

definition tyenv_eq :: "('Var,'BExp) TyEnv ⇒ ('Var, 'Val) Mem ⇒ ('Var, 'Val) Mem ⇒ bool"
  (infix "=ı" 60)
  where "mem⇩1 =⇘Γ⇙ mem⇩2 ≡ ∀ x. (type_max (to_total Γ x) mem⇩1 = Low ⟶ mem⇩1 x = mem⇩2 x)"

lemma type_max_dma_type [simp]:
  "type_max (dma_type x) mem = dma mem x"
  using dma_correct unfolding type_max_def apply auto
  done

  
text ‹
  This result followed trivially for Mantel et al., but we need to know that the
  type environment is wellformed.
›
lemma tyenv_eq_sym': 
  "dom Γ ∩ 𝒞 = {} ⟹ types_wellformed Γ ⟹ mem⇩1 =⇘Γ⇙ mem⇩2 ⟹ mem⇩2 =⇘Γ⇙ mem⇩1"
proof(clarsimp simp: tyenv_eq_def)
  fix x
  assume a: "∀x. type_max (to_total Γ x) mem⇩1 = Low ⟶ mem⇩1 x = mem⇩2 x"
  assume b: "dom Γ ∩ 𝒞 = {}"
  from a b have eq_𝒞: "∀x∈𝒞. mem⇩1 x = mem⇩2 x"
    by (fastforce simp: to_total_def 𝒞_Low type_max_dma_type split: if_splits)
  hence "dma mem⇩1 = dma mem⇩2"
    by (rule dma_𝒞)
  hence dma_type_eq: "type_max (dma_type x) mem⇩1 = type_max (dma_type x) mem⇩2"
    by(simp)
  assume c: "types_wellformed Γ"
  
  assume d: "type_max (to_total Γ x) mem⇩2 = Low"
  show "mem⇩2 x = mem⇩1 x"
  proof(cases "x ∈ dom Γ")
    assume in_dom: "x ∈ dom Γ"
    from this obtain t where t: "Γ x = Some t" by blast
    from this in_dom c have "type_wellformed t" by (force simp: types_wellformed_def)
    hence "∀x∈vars_of_type t. mem⇩1 x = mem⇩2 x"
      using eq_𝒞 unfolding type_wellformed_def by blast
    hence t_eq: "type_max t mem⇩1 = type_max t mem⇩2" 
      unfolding type_max_def using eval_vars_det⇩B
      by fastforce
    with in_dom t have "to_total Γ x = t"
      by (auto simp: to_total_def)
    with t_eq have "type_max (to_total Γ x) mem⇩2 = type_max (to_total Γ x) mem⇩1" by simp
    with d have "type_max (to_total Γ x) mem⇩1 = Low" by simp
    with a show ?thesis by (metis sym)
  next
    assume "x ∉ dom Γ"
    hence "to_total Γ x = dma_type x"
      by (auto simp: to_total_def)
    with dma_type_eq have "type_max (to_total Γ x) mem⇩2 = type_max (to_total Γ x) mem⇩1" by simp
    with d have "type_max (to_total Γ x) mem⇩1 = Low" by simp
    with a show ?thesis by (metis sym)
  qed
qed

lemma tyenv_eq_sym:
  "tyenv_wellformed mds Γ 𝒮 P ⟹ mem⇩1 =⇘Γ⇙ mem⇩2 ⟹ mem⇩2 =⇘Γ⇙ mem⇩1"
  apply(rule tyenv_eq_sym')
    apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
   apply(simp add: tyenv_wellformed_def)
  by assumption
  
inductive_set ℛ⇩1 :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  and ℛ⇩1_abv :: "
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  ('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  bool" ("_ ℛ⇧1⇘_,_,_⇙ _" [120, 120, 120, 120, 120] 1000)
  for Γ' :: "('Var,'BExp) TyEnv"
  and 𝒮' :: "'Var Stable"
  and P' :: "'BExp preds"
where
  "x ℛ⇧1⇘Γ,𝒮,P⇙ y ≡ (x, y) ∈ ℛ⇩1 Γ 𝒮 P" |
  intro [intro!] : "⟦ ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ; tyenv_wellformed mds Γ 𝒮 P ; mem⇩1 =⇘Γ⇙ mem⇩2;
                      pred P mem⇩1; pred P mem⇩2; ∀x∈dom Γ. x∉mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem⇩1 ≤ dma mem⇩1 x⟧ ⟹ 
                    ⟨c, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c, mds, mem⇩2⟩"

inductive ℛ⇩3_aux :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
                 ('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
                 bool" ("_ ℛ⇧3⇘_,_,_⇙ _" [120, 120, 120, 120, 120] 1000)
  and ℛ⇩3 :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒ (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  where
  "ℛ⇩3 Γ' 𝒮' P' ≡ {(lc⇩1, lc⇩2). ℛ⇩3_aux lc⇩1 Γ' 𝒮' P' lc⇩2}" |
  intro⇩1 [intro] : "⟦ ⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩; ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ⟧ ⟹
                      ⟨Seq c⇩1 c, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨Seq c⇩2 c, mds, mem⇩2⟩" |
  intro⇩3 [intro] : "⟦ ⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩; ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ⟧ ⟹
                      ⟨Seq c⇩1 c, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨Seq c⇩2 c, mds, mem⇩2⟩"

(* 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 𝒯 ≡ ∀ c⇩1 c⇩2 mds mem⇩1 mem⇩2 c⇩1' mds' mem⇩1'.
  ((⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ 𝒯⇩1 ∧
   (⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩)) ⟶
  (∃ c⇩2' mem⇩2'. ⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧ 
                (⟨c⇩1', mds', mem⇩1'⟩, ⟨c⇩2', mds', mem⇩2'⟩) ∈ 𝒯)"

inductive_set ℛ :: "('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
  and ℛ_abv :: "
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  ('Var,'BExp) TyEnv ⇒ 'Var Stable ⇒ 'BExp preds ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  bool" ("_ ℛ⇧u⇘_,_,_⇙ _" [120, 120, 120, 120, 120] 1000)
  for Γ :: "('Var,'BExp) TyEnv"
  and 𝒮 :: "'Var Stable"
  and P :: "'BExp preds"
where
  "x ℛ⇧u⇘Γ,𝒮,P⇙ y ≡ (x, y) ∈ ℛ Γ 𝒮 P" |
  intro⇩1: "lc ℛ⇧1⇘Γ,𝒮,P⇙ lc' ⟹ (lc, lc') ∈ ℛ Γ 𝒮 P" |
  intro⇩3: "lc ℛ⇧3⇘Γ,𝒮,P⇙ lc' ⟹ (lc, lc') ∈ ℛ Γ 𝒮 P"

(* Some eliminators for the above relations *)
inductive_cases ℛ⇩1_elim [elim]: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩"
inductive_cases ℛ⇩3_elim [elim]: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩"

inductive_cases ℛ_elim [elim]: "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ ℛ Γ 𝒮 P"
inductive_cases ℛ_elim': "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds⇩2, mem⇩2⟩) ∈ ℛ Γ 𝒮 P"
inductive_cases ℛ⇩1_elim' : "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩2, mds⇩2, mem⇩2⟩"
inductive_cases ℛ⇩3_elim' : "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds⇩2, mem⇩2⟩"

lemma ℛ⇩1_mem_eq: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩ ⟹ mem⇩1 =⇘mds⇙⇧l mem⇩2"
proof (erule ℛ⇩1_elim)
  fix Γ 𝒮 P
  assume wf: "tyenv_wellformed mds Γ 𝒮 P"
  hence mds_consistent: "mds_consistent mds Γ 𝒮 P"
    unfolding tyenv_wellformed_def by blast
  assume tyenv_eq: "mem⇩1 =⇘Γ⇙ mem⇩2"
  assume leq: "∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem⇩1 ≤ dma mem⇩1 x"
  assume pred: "pred P mem⇩1"
  
  show "mem⇩1 =⇘mds⇙⇧l mem⇩2"
  unfolding low_mds_eq_def
  proof(clarify)
    fix x
    assume is_Low: "dma mem⇩1 x = Low"
    assume is_readable: "x ∈ 𝒞 ∨ x ∉ mds AsmNoReadOrWrite"
    show "mem⇩1 x = mem⇩2 x"
    proof(cases "x ∈ dom Γ")
      assume in_dom: "x ∈ dom Γ"
      with mds_consistent have "x ∉ 𝒞"
        unfolding mds_consistent_def by blast
      with is_readable have "x ∉ mds AsmNoReadOrWrite"
        by blast
       
      with in_dom leq  have "type_max (to_total Γ x) mem⇩1 ≤ dma mem⇩1 x"
        unfolding to_total_def
        by auto
      with is_Low have "type_max (to_total Γ x) mem⇩1 = Low"
        by(simp add: less_eq_Sec_def)
      with tyenv_eq show ?thesis
        unfolding tyenv_eq_def by blast
    next         
      assume nin_dom: "x ∉ dom Γ"
      with is_Low have "type_max (to_total Γ x) mem⇩1 = Low"
        unfolding to_total_def
        by simp
      with tyenv_eq show ?thesis
        unfolding tyenv_eq_def by blast
    qed
  qed
qed

lemma ℛ⇩1_dma_eq:
  "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩ ⟹ dma mem⇩1 = dma mem⇩2"
  apply(drule ℛ⇩1_mem_eq)
  apply(erule low_mds_eq_dma)
  done


(* ℛ meets the criteria of a "simple bisim"
   which can be used to simplify the establishment of a refinement relation *)
lemma bisim_simple_ℛ⇩1:
  "⟨c, mds, mem⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c', mds', mem'⟩ ⟹ c = c'"
  apply(cases rule: ℛ⇩1.cases, simp+)
  done

lemma bisim_simple_ℛ⇩3:
  "lc ℛ⇧3⇘Γ,𝒮,P⇙ lc' ⟹ (fst (fst lc)) = (fst (fst lc'))"
  apply(induct rule: ℛ⇩3_aux.induct)
  using bisim_simple_ℛ⇩1 apply clarsimp
  apply simp
  done

lemma bisim_simple_ℛ⇩u:
  "lc ℛ⇧u⇘Γ,𝒮,P⇙ lc' ⟹ (fst (fst lc)) = (fst (fst lc'))"
  apply(induct rule: ℛ.induct)
   apply clarsimp
   apply(cases rule: ℛ⇩1.cases, simp+)
  apply(cases rule: ℛ⇩3_aux.cases, simp+)
   apply blast
  using bisim_simple_ℛ⇩3 apply clarsimp
  done


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

lemma 𝒞_eq_type_max_eq:
  assumes wf: "type_wellformed t"
  assumes 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩2 x" 
  shows "type_max t mem⇩1 = type_max t mem⇩2"
proof -
  have "∀x∈vars_of_type t. mem⇩1 x = mem⇩2 x"
    using wf 𝒞_eq unfolding type_wellformed_def by blast
  thus ?thesis
    unfolding type_max_def using eval_vars_det⇩B by fastforce
qed

lemma vars_of_type_eq_type_max_eq:
  assumes mem_eq: "∀x∈vars_of_type t. mem⇩1 x = mem⇩2 x" 
  shows "type_max t mem⇩1 = type_max t mem⇩2"
proof -
  from assms show ?thesis
    unfolding type_max_def using eval_vars_det⇩B by fastforce
qed

lemma ℛ⇩1_sym: "sym (ℛ⇩1 Γ' 𝒮' P')"
unfolding sym_def
proof clarsimp
  fix c mds mem c' mds' mem'
  assume in_ℛ⇩1: "⟨c, mds, mem⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c', mds', mem'⟩"
  then obtain Γ 𝒮 P where
  stuff: "c' = c"  "mds' = mds"  "⊢ Γ,𝒮,P {c} Γ',𝒮',P'"  "tyenv_wellformed mds Γ 𝒮 P"
  "mem =⇘Γ⇙ mem'" "pred P mem" "pred P mem'"
  "∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem ≤ dma mem x"
    using ℛ⇩1_elim' by blast+
  from stuff have stuff': "mem' =⇘Γ⇙ mem"
    by (metis tyenv_eq_sym)
  
  have "∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem' ≤ dma mem' x"
  proof -
    from in_ℛ⇩1 have "dma mem = dma mem'"
      using ℛ⇩1_dma_eq stuff by metis
    moreover have "∀x∈dom Γ. type_max (the (Γ x)) mem = type_max (the (Γ x)) mem'"
    proof
      fix x
      assume "x ∈ dom Γ"
      hence "type_wellformed (the (Γ x))"
        using ‹tyenv_wellformed mds Γ 𝒮 P›
        by(auto simp: tyenv_wellformed_def types_wellformed_def)
      moreover have "∀x∈𝒞. mem x = mem' x"
        using in_ℛ⇩1 ℛ⇩1_mem_eq 𝒞_Low stuff
        unfolding low_mds_eq_def by auto
      ultimately
      show "type_max (the (Γ x)) mem = type_max (the (Γ x)) mem'"
        using 𝒞_eq_type_max_eq by blast
    qed
    ultimately show ?thesis
      using stuff(8) by fastforce
  qed
  with stuff stuff'
  show "⟨c', mds', mem'⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c, mds, mem⟩"
  by (metis (no_types) ℛ⇩1.intro)
qed

lemma ℛ⇩3_sym: "sym (ℛ⇩3 Γ 𝒮 P)"
  unfolding sym_def
proof (clarify)
  fix c⇩1 mds mem⇩1 c⇩2 mds' mem⇩2
  assume asm: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds', mem⇩2⟩"
  hence [simp]: "mds' = mds"
    using ℛ⇩3_elim' by blast
  from asm show "⟨c⇩2, mds', mem⇩2⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩1, mds, mem⇩1⟩"
    apply auto
    apply (induct rule: ℛ⇩3_aux.induct)
     apply (metis (lifting) ℛ⇩1_sym ℛ⇩3_aux.intro⇩1 symD)
    by (metis (lifting) ℛ⇩3_aux.intro⇩3)
qed

lemma ℛ_mds [simp]: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2, mds', mem⇩2⟩ ⟹ mds = mds'"
  apply (rule ℛ_elim')
     apply (auto)
   apply (metis ℛ⇩1_elim')
  apply (insert ℛ⇩3_elim')
  by blast

lemma ℛ_sym: "sym (ℛ Γ 𝒮 P)"
  unfolding sym_def
proof (clarify)
  fix c⇩1 mds mem⇩1 c⇩2 mds⇩2 mem⇩2
  assume asm: "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds⇩2, mem⇩2⟩) ∈ ℛ Γ 𝒮 P"
  with ℛ_mds have [simp]: "mds⇩2 = mds"
    by blast
  from asm show "(⟨c⇩2, mds⇩2, mem⇩2⟩, ⟨c⇩1, mds, mem⇩1⟩) ∈ ℛ Γ 𝒮 P"
    using ℛ.intro⇩1 [of Γ 𝒮 P] and ℛ.intro⇩3 [of _ Γ 𝒮 P]
    using ℛ⇩1_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 Γ' 𝒮' P')"
  unfolding closed_glob_consistent_def
proof (clarify)
  fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 A
  assume R1: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
  hence [simp]: "c⇩2 = c⇩1" by blast
  assume A_updates_vars: "∀x. case A x of None ⇒ True | Some (v, v') ⇒ mem⇩1 x ≠ v ∨ mem⇩2 x ≠ v' ⟶ ¬ var_asm_not_written mds x"
  assume A_updates_dma: "∀x. dma mem⇩1 [∥⇩1 A] x ≠ dma mem⇩1 x ⟶ ¬ var_asm_not_written mds x"
  assume A_updates_sec: "∀x. dma mem⇩1 [∥⇩1 A] x = Low ∧ (x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞) ⟶ mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"
  from R1 obtain Γ 𝒮 P where Γ_props: "⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P'" "mem⇩1 =⇘Γ⇙ mem⇩2" "tyenv_wellformed mds Γ 𝒮 P"
                                      "pred P mem⇩1" "pred P mem⇩2"
                                      "∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem⇩1 ≤ dma mem⇩1 x"
    by force

  from Γ_props(3) have stable_not_written: "∀x. stable 𝒮 x ⟶ var_asm_not_written mds x"
    by(auto simp: tyenv_wellformed_def mds_consistent_def stable_def var_asm_not_written_def)
  with A_updates_vars have stable_unchanged⇩1: "∀x. stable 𝒮 x ⟶ (mem⇩1 [∥⇩1 A]) x = mem⇩1 x" and
                           stable_unchanged⇩2: "∀x. stable 𝒮 x ⟶ (mem⇩2 [∥⇩2 A]) x = mem⇩2 x"
    by(auto simp: apply_adaptation_def split: option.splits)

  from stable_not_written A_updates_dma 
  have stable_unchanged_dma⇩1: "∀x. stable 𝒮 x ⟶ dma (mem⇩1 [∥⇩1 A]) x = dma mem⇩1 x"
    by(blast)

  have tyenv_eq': "mem⇩1 [∥⇩1 A] =⇘Γ⇙ mem⇩2 [∥⇩2 A]"
  proof(clarsimp simp: tyenv_eq_def)
    fix x
    assume a: "type_max (to_total Γ x) mem⇩1 [∥⇩1 A] = Low"
    show "mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"
    proof(cases "x ∈ dom Γ")
      assume in_dom: "x ∈ dom Γ"
      with Γ_props(3) have "var_asm_not_written mds x"
        by(auto simp: tyenv_wellformed_def mds_consistent_def var_asm_not_written_def stable_def)
      hence [simp]: "mem⇩1 [∥⇩1 A] x = mem⇩1 x" and [simp]: "mem⇩2 [∥⇩2 A] x = mem⇩2 x"
        using A_updates_vars by(auto simp: apply_adaptation_def split: option.splits)
      from in_dom a obtain t⇩x where Γ⇩x: "Γ x = Some t⇩x" and t⇩x_Low': "type_max t⇩x (mem⇩1 [∥⇩1 A]) = Low"
        by(auto simp: to_total_def)
      have t⇩x_unchanged: "type_max t⇩x (mem⇩1 [∥⇩1 A])  = type_max t⇩x mem⇩1"
      proof - 
        from Γ⇩x Γ_props(3) have t⇩x_stable: "type_stable 𝒮 t⇩x" and t⇩x_wellformed: "type_wellformed t⇩x"
          by(force simp: tyenv_wellformed_def types_stable_def types_wellformed_def)+
        from t⇩x_stable t⇩x_wellformed stable_unchanged⇩1 show ?thesis
          using type_stable_is_sufficient'
          by blast
      qed
      with t⇩x_Low' have t⇩x_Low: "type_max t⇩x mem⇩1 = Low" by simp
      with Γ⇩x Γ_props(2) have "mem⇩1 x = mem⇩2 x"
        by(force simp: tyenv_eq_def to_total_def split: if_splits)
      thus ?thesis by simp
    next
      assume nin_dom: "x ∉ dom Γ"
      with a have is_Low': "dma (mem⇩1[∥⇩1 A]) x = Low"
        by(simp add: to_total_def)
      show ?thesis
      proof(cases "x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞")
        assume "x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞"
        with is_Low' show ?thesis
          using A_updates_sec by blast
      next
        assume "¬ (x ∉ mds AsmNoReadOrWrite ∨ x ∈ 𝒞)"
        hence "x ∈ mds AsmNoReadOrWrite" and "x ∉ 𝒞"
          by auto
        with nin_dom Γ_props(3) have "False"
          by(auto simp: tyenv_wellformed_def mds_consistent_def stable_def)
        thus ?thesis by blast
      qed
    qed
  qed
  
  have sec': "∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) (mem⇩1 [∥⇩1 A]) ≤ dma (mem⇩1 [∥⇩1 A]) x"
  proof(intro ballI impI)
    fix x
    assume readable: "x ∉ mds AsmNoReadOrWrite"
    assume in_dom: "x ∈ dom Γ"
    with Γ_props(3) have "var_asm_not_written mds x"
      by(auto simp: tyenv_wellformed_def mds_consistent_def var_asm_not_written_def stable_def)
    hence [simp]: "dma mem⇩1 [∥⇩1 A] x = dma mem⇩1 x"
      using A_updates_dma by(auto simp: apply_adaptation_def split: option.splits)
    from in_dom obtain t⇩x where Γ⇩x: "Γ x = Some t⇩x"
      by(auto simp: to_total_def)
    have t⇩x_unchanged: "type_max t⇩x (mem⇩1 [∥⇩1 A])  = type_max t⇩x mem⇩1"
    proof - 
      from Γ⇩x Γ_props(3) have t⇩x_stable: "type_stable 𝒮 t⇩x" and t⇩x_wellformed: "type_wellformed t⇩x"
        by(force simp: tyenv_wellformed_def types_stable_def types_wellformed_def)+
      from t⇩x_stable t⇩x_wellformed stable_unchanged⇩1 show ?thesis
        using type_stable_is_sufficient'
        by blast
    qed
    with Γ⇩x have [simp]:"type_max (the (Γ x)) (mem⇩1 [∥⇩1 A]) = type_max (the (Γ x)) mem⇩1"
      by simp
    show "type_max (the (Γ x)) mem⇩1 [∥⇩1 A] ≤ dma mem⇩1 [∥⇩1 A] x "
      apply simp
      using in_dom readable Γ_props by metis
  qed
    
  from stable_unchanged⇩1 stable_unchanged⇩2 Γ_props(3) have "∀p∈P. ev⇩B (mem⇩1 [∥⇩1 A]) p = ev⇩B mem⇩1 p ∧ ev⇩B (mem⇩2 [∥⇩2 A]) p = ev⇩B mem⇩2 p"
    apply(intro ballI)
    apply(rule conjI)
    by(rule eval_vars_det⇩B,force simp: tyenv_wellformed_def mds_consistent_def stable_def)+
    
  hence "pred P (mem⇩1 [∥⇩1 A]) = pred P mem⇩1" and
        "pred P (mem⇩2 [∥⇩2 A]) = pred P mem⇩2"
    by(simp add: pred_def)+
  
  with Γ_props tyenv_eq' sec'
  show "⟨c⇩1, mds, mem⇩1 [∥⇩1 A]⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2 [∥⇩2 A]⟩"
    by auto
qed


lemma ℛ⇩3_closed_glob_consistent:
  "closed_glob_consistent (ℛ⇩3 Γ' 𝒮' P')"
unfolding closed_glob_consistent_def
proof(clarsimp)
  fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 A
  assume in_ℛ⇩3: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
  assume A_modifies_vars: "∀x. case A x of None ⇒ True | Some (v, v') ⇒ mem⇩1 x ≠ v ∨ mem⇩2 x ≠ v' ⟶ ¬ var_asm_not_written mds x"
  assume A_modifies_dma: "∀x. dma mem⇩1 [∥⇩1 A] x ≠ dma mem⇩1 x ⟶ ¬ var_asm_not_written mds x"
  assume A_modifies_sec: "∀x. dma mem⇩1 [∥⇩1 A] x = Low ∧ (x ∈ mds AsmNoReadOrWrite ⟶ x ∈ 𝒞) ⟶ mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"
  (* do a bit of massaging to get the goal state set-up nicely for the induction rule *)
  define lc⇩1 where "lc⇩1 ≡ ⟨c⇩1, mds, mem⇩1⟩"
  define lc⇩2 where "lc⇩2 ≡ ⟨c⇩2, mds, mem⇩2⟩"
  from lc⇩1_def lc⇩2_def in_ℛ⇩3 have "lc⇩1 ℛ⇧3⇘Γ',𝒮',P'⇙ lc⇩2" by simp
  from this lc⇩1_def lc⇩2_def A_modifies_vars A_modifies_dma A_modifies_sec
  show "⟨c⇩1, mds, mem⇩1 [∥⇩1 A]⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2 [∥⇩2 A]⟩"
  proof(induct arbitrary: c⇩1 mds mem⇩1 c⇩2 mds mem⇩2 rule: ℛ⇩3_aux.induct)
    case (intro⇩1 c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P')
    show ?case
      apply (rule ℛ⇩3_aux.intro⇩1[OF _ intro⇩1(2)])
      using ℛ⇩1_closed_glob_consistent intro⇩1
      unfolding closed_glob_consistent_def by blast
  next
    case (intro⇩3 c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P')
    show ?case
      apply(rule ℛ⇩3_aux.intro⇩3)
      apply(rule intro⇩3(2))
      using intro⇩3 apply simp+
      done
  qed
qed


lemma ℛ_closed_glob_consistent: "closed_glob_consistent (ℛ Γ' 𝒮' P')"
  unfolding closed_glob_consistent_def
proof (clarify, erule ℛ_elim, simp_all)
  fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 A
  assume R1: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
  and A_modifies_vars: "∀x. case A x of None ⇒ True | Some (v, v') ⇒ mem⇩1 x ≠ v ∨ mem⇩2 x ≠ v' ⟶ ¬ var_asm_not_written mds x"
  and A_modifies_dma: "∀x. dma (mem⇩1 [∥⇩1 A]) x ≠ dma mem⇩1 x ⟶ ¬ var_asm_not_written mds x"
  and A_modifies_sec: "∀x. dma mem⇩1 [∥⇩1 A] x = Low ∧ (x ∈ mds AsmNoReadOrWrite ⟶ x ∈ 𝒞) ⟶ mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"  
  show
    "⟨c⇩1, mds, mem⇩1 [∥⇩1 A]⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2 [∥⇩2 A]⟩"
    apply(rule intro⇩1)
    apply clarify
    using ℛ⇩1_closed_glob_consistent unfolding closed_glob_consistent_def
    using R1 A_modifies_vars A_modifies_dma A_modifies_sec
    by blast
next
  fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 x A
  assume R3: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
  and A_modifies_vars: "∀x. case A x of None ⇒ True | Some (v, v') ⇒ mem⇩1 x ≠ v ∨ mem⇩2 x ≠ v' ⟶ ¬ var_asm_not_written mds x"
  and A_modifies_dma: "∀x. dma (mem⇩1 [∥⇩1 A]) x ≠ dma mem⇩1 x ⟶ ¬ var_asm_not_written mds x"
  and A_modifies_sec: "∀x. dma mem⇩1 [∥⇩1 A] x = Low ∧ (x ∈ mds AsmNoReadOrWrite ⟶ x ∈ 𝒞) ⟶ mem⇩1 [∥⇩1 A] x = mem⇩2 [∥⇩2 A] x"
  show "⟨c⇩1, mds, mem⇩1 [∥⇩1 A]⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2 [∥⇩2 A]⟩ "
    apply(rule intro⇩3)
    using ℛ⇩3_closed_glob_consistent unfolding closed_glob_consistent_def
    using R3 A_modifies_vars A_modifies_dma A_modifies_sec
    by blast
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 mode_update_add_anno:
  "mds_consistent mds Γ 𝒮 P ⟹ 
   mds_consistent (update_modes upd mds) 
                  (Γ ⊕⇩𝒮 upd) 
                  (add_anno_stable 𝒮 upd) 
                  (P |` {v. stable (add_anno_stable 𝒮 upd) v})"
  apply(case_tac upd)
   apply(rename_tac v m)
   apply(case_tac m)
      apply((clarsimp simp: add_anno_def mds_consistent_def stable_def restrict_preds_to_vars_def | safe | fastforce)+)[4]
  apply(rename_tac v m)
  apply(case_tac m)
     apply((clarsimp simp: add_anno_def mds_consistent_def stable_def restrict_preds_to_vars_def | safe | fastforce)+)[4]
  done

lemma add_anno_acq_GuarNoReadOrWrite [simp]:
  "Γ ⊕⇩𝒮 (v +=⇩m GuarNoReadOrWrite) = Γ"
  apply(clarsimp simp: add_anno_def to_total_def restrict_map_def)
  apply(rule ext)
  apply(clarsimp | safe)+
  by (metis option.collapse prod.collapse)

lemma add_anno_rel_GuarNoReadOrWrite [simp]:
  "Γ ⊕⇩𝒮 (v -=⇩m GuarNoReadOrWrite) = Γ"
  apply(clarsimp simp: add_anno_def to_total_def restrict_map_def)
  apply(rule ext)
  apply(clarsimp | safe)+
  by (metis option.collapse)

lemma add_anno_acq_GuarNoWrite [simp]:
  "Γ ⊕⇩𝒮 (v +=⇩m GuarNoWrite) = Γ"
  apply(clarsimp simp: add_anno_def to_total_def restrict_map_def)
  apply(rule ext)
  apply(clarsimp | safe)+
  by (metis option.collapse prod.collapse)

lemma add_anno_rel_GuarNoWrite [simp]:
  "Γ ⊕⇩𝒮 (v -=⇩m GuarNoWrite) = Γ"
  apply(clarsimp simp: add_anno_def to_total_def restrict_map_def)
  apply(rule ext)
  apply(clarsimp | safe)+
  by (metis option.collapse)

lemma dom_add_anno_rel:
  "∀x∈dom (Γ ⊕⇩𝒮 (v -=⇩m m)). (Γ ⊕⇩𝒮 (v -=⇩m m)) x = Γ x"
  apply(clarsimp simp: add_anno_def to_total_def restrict_map_def split: if_splits)
  apply(case_tac m)
  apply(auto split: if_splits)
  done

lemma types_wellformed_mode_update:
  "types_wellformed Γ ⟹
   types_wellformed (Γ ⊕⇩𝒮 upd)"
  apply(clarsimp simp: types_wellformed_def)
  apply(case_tac upd)
   apply(rename_tac v t v' m)
   apply(case_tac m)
      apply clarsimp
      apply(case_tac "v' ∈ dom Γ ∨ v' ∈ 𝒞")
       apply(clarsimp, force)
      apply(simp split: if_splits)
       apply(drule sym, fastforce)
      apply(clarsimp | force )+
     apply(case_tac "v' ∈ dom Γ ∨ v' ∈ 𝒞")
      apply clarsimp
      apply force
     apply(simp split: if_splits)
      apply(drule sym, fastforce)
     apply(clarsimp | force)+
  using dom_add_anno_rel[THEN bspec, OF domI]
  apply (metis domI option.sel)
  done
  
(* TODO: consider putting this proof into Isar so we can explain the reasoning behind the
   anno_type_stable predicate *)
lemma types_stable_mode_update:
   "types_stable Γ 𝒮 ⟹ types_wellformed Γ ⟹ anno_type_stable Γ 𝒮 upd
    ⟹ types_stable (Γ ⊕⇩𝒮 upd) (add_anno_stable 𝒮 upd)"
  apply(clarsimp simp: types_stable_def)
  apply(rename_tac x c f C)
  apply(case_tac upd)
   apply(rename_tac v m)
   apply(case_tac m)
      apply clarsimp
      apply(case_tac "v ∈ dom Γ ∨ v ∈ 𝒞")
       apply clarsimp
       apply(force simp: stable_def)
      apply(simp split: if_splits)
       using 𝒞_vars_correct
       apply(fastforce simp:  anno_type_stable_def stable_def)
      apply(force simp: stable_def)
     apply clarsimp
     apply(case_tac "v ∈ dom Γ ∨ v ∈ 𝒞")
      apply clarsimp
      apply(force simp: stable_def)
     apply(simp split: if_splits)
      using 𝒞_vars_correct
      apply(fastforce simp: anno_type_stable_def stable_def)
     apply(force simp: stable_def)
    apply(force simp: stable_def)
   apply(force simp: stable_def)
  apply(rename_tac v m)
  apply(subgoal_tac "Γ x = Some (C)")
   prefer 2
   using dom_add_anno_rel
   apply (metis domI)
  apply(case_tac m)
     apply(clarsimp simp: anno_type_stable_def split: if_splits)
      apply(clarsimp simp: stable_def types_wellformed_def type_wellformed_def)
      using 𝒞_vars_correct
      apply (metis (mono_tags, lifting) UN_I contra_subsetD domI option.sel)
     apply(clarsimp simp: stable_def types_wellformed_def type_wellformed_def)
     using 𝒞_vars_correct
     apply (metis (mono_tags, lifting) UN_I contra_subsetD domI option.sel)
    apply(clarsimp simp: anno_type_stable_def split: if_splits)
     apply(clarsimp simp: stable_def types_wellformed_def type_wellformed_def)
     apply (metis (mono_tags, lifting) UN_I contra_subsetD domI option.sel)
    apply(clarsimp simp: stable_def)
    apply (metis (no_types, lifting) domI option.sel snd_conv subsetD type_wellformed_def types_wellformed_def)
   apply(clarsimp simp: anno_type_stable_def split: if_splits)
   apply(clarsimp simp: stable_def)
   apply (metis (no_types, lifting) domI option.sel snd_conv subsetD type_wellformed_def types_wellformed_def)
  apply(clarsimp simp: stable_def)
  apply (metis (no_types, lifting) domI option.sel snd_conv subsetD type_wellformed_def types_wellformed_def)
  done  
     
     
lemma tyenv_wellformed_mode_update:
  "tyenv_wellformed mds Γ 𝒮 P ⟹ anno_type_stable Γ 𝒮 upd ⟹
   tyenv_wellformed (update_modes upd mds) 
                  (Γ ⊕⇩𝒮 upd) 
                  (add_anno_stable 𝒮 upd) 
                  (P |` {v. stable (add_anno_stable 𝒮 upd) v})"
  apply(clarsimp simp: tyenv_wellformed_def)
  apply(rule conjI)
   apply(blast intro: mode_update_add_anno)
  apply(rule conjI)
   apply(blast intro: types_wellformed_mode_update)
  apply(blast intro: types_stable_mode_update)
  done


lemma stop_cxt :
  "⟦ ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ; c = Stop ⟧ ⟹ 
  context_equiv Γ P Γ' ∧ 𝒮' = 𝒮 ∧ P ⊢ P' ∧ (∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds Γ' 𝒮 P')"
  apply (induct rule: has_type.induct)
          apply (auto intro: context_equiv_trans context_equiv_entailment pred_entailment_trans)
  done

lemma tyenv_wellformed_preds_update:
  "P' = P'' |` {v. stable 𝒮 v} ⟹
  tyenv_wellformed mds Γ 𝒮 P ⟹ tyenv_wellformed mds Γ 𝒮 P'"
  apply(clarsimp simp: tyenv_wellformed_def)
  apply(clarsimp simp: mds_consistent_def)
  apply(auto simp: restrict_preds_to_vars_def add_pred_def split: if_splits)
  done


lemma mds_consistent_preds_tyenv_update:
  "P' = P'' |` {v. stable 𝒮 v} ⟹ v ∈ dom Γ ⟹
  mds_consistent mds Γ 𝒮 P ⟹ mds_consistent mds (Γ(v ↦ t)) 𝒮 P'"
  apply(clarsimp simp: mds_consistent_def)
  apply(auto simp: restrict_preds_to_vars_def add_pred_def split: if_splits)
  done


lemma pred_preds_update:
  assumes mem'_def: "mem' = mem (x := ev⇩A mem e)" 
  assumes P'_def: "P' = (assign_post P x e) |` {v. stable 𝒮 v}"
  assumes pred_P: "pred P mem" 
  shows "pred P' mem'"
proof -
  from P'_def have P'_def': "P' ⊆ assign_post P x e"
    by(auto simp: restrict_preds_to_vars_def add_pred_def split: if_splits)
  have "pred (assign_post P x e) mem'"
    using assign_post_valid pred_P mem'_def by blast
  with P'_def' show ?thesis
    unfolding pred_def by blast
qed

lemma types_wellformed_update:
  "types_wellformed Γ ⟹ type_wellformed t ⟹ types_wellformed (Γ(x ↦ t))"
  by(auto simp: types_wellformed_def)

lemma types_stable_update:
  "types_stable Γ 𝒮 ⟹ type_stable 𝒮 t ⟹ types_stable (Γ(x ↦ t)) 𝒮"
  by(auto simp: types_stable_def)
  
lemma tyenv_wellformed_sub:
  "⟦P⇩1 ⊆ P⇩2;
  Γ⇩2 = Γ⇩1; tyenv_wellformed mds Γ⇩2 𝒮 P⇩2⟧ ⟹
     tyenv_wellformed mds Γ⇩1 𝒮 P⇩1"
  apply(clarsimp simp: tyenv_wellformed_def | safe)+
  apply(fastforce simp: mds_consistent_def)
  done

abbreviation
  tyenv_sec :: "'Var Mds ⇒ ('Var,'BExp) TyEnv ⇒ ('Var,'Val) Mem ⇒ bool"
where
  "tyenv_sec mds Γ mem ≡ ∀x∈dom Γ. x∉mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem ≤ dma mem x"

lemma tyenv_sec_mode_update:
  "(∀x.  (to_total Γ x) ≤:⇩P''  (to_total Γ'' x)) ⟹ pred P'' mem ⟹ 𝒮 = (mds AsmNoWrite, mds AsmNoReadOrWrite) ⟹
    anno_type_sec Γ 𝒮 P upd ⟹ 𝒮'' = add_anno_stable 𝒮 upd ⟹ (∀p∈P. ∀v∈bexp_vars p. stable 𝒮 v) ⟹
  P'' = P |` {v. stable 𝒮'' v} ⟹
    Γ'' = Γ ⊕⇩𝒮 upd ⟹ tyenv_sec mds Γ mem ⟹ tyenv_sec (update_modes upd mds) Γ'' mem"
  apply(case_tac upd)
   apply(rename_tac v m)
   apply(case_tac m)
    apply(auto simp: add_anno_def to_total_def)[4]
  apply(rename_tac v m)
  apply(case_tac m)
    apply(subgoal_tac "v ∈ mds AsmNoWrite ⟶ P'' = P")
    by(auto simp: add_anno_def to_total_def dest: subtype_sound split: if_splits simp: anno_type_sec_def restrict_preds_to_vars_def stable_def)


lemma tyenv_sec_eq:
  "∀x∈𝒞. mem x = mem' x ⟹ types_wellformed Γ ⟹ tyenv_sec mds Γ mem = tyenv_sec mds Γ mem'"
  apply(rule ball_cong[OF HOL.refl])
  apply(rename_tac x)
  apply(rule imp_cong[OF HOL.refl])
  apply(subgoal_tac "type_max (the (Γ x)) mem = type_max (the (Γ x)) mem'")
   using dma_𝒞 apply fastforce
  apply(force intro: 𝒞_eq_type_max_eq simp: types_wellformed_def)
  done

lemma context_equiv_tyenv_sec:
  "context_equiv Γ⇩2 P⇩2 Γ⇩1 ⟹
    pred P⇩2 mem ⟹ tyenv_sec mds Γ⇩2 mem ⟹ tyenv_sec mds Γ⇩1 mem"
   apply(clarsimp simp: context_equiv_def type_equiv_def)
   apply(rename_tac x y)
   apply(rule_tac y="type_max (the (Γ⇩2 x)) mem" in order_trans)
    apply(rule subtype_sound[rule_format])
     apply force
    apply assumption
   apply force
   done

lemma add_pred_entailment:
  "P +⇩𝒮 p ⊢ P"
  apply(rule subset_entailment)
  apply(rule add_pred_subset)
  done


lemma preservation_no_await: 
  "⟦⊢ Γ,𝒮,P { c } Γ',𝒮',P';
    ⟨c, mds, mem⟩ ↝  ⟨c', mds', mem'⟩;
    no_await c⟧ ⟹ 
  ∃ Γ'' 𝒮'' P''. (⊢ Γ'',𝒮'',P'' { c' } Γ',𝒮',P') ∧ 
         (tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶ 
           tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧ 
           pred P'' mem' ∧ 
           tyenv_sec mds' Γ'' mem')"
proof (induct arbitrary: c' mds rule: has_type.induct)
  
  case (anno_type Γ'' Γ 𝒮 upd 𝒮'' P'' P c⇩1 Γ' 𝒮' P')
  hence step: "⟨c⇩1, update_modes upd mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
    by (metis upd_elim)
  from ‹no_await (c⇩1@[upd])› no_await.cases have "no_await c⇩1" by fast
  with step anno_type(5) obtain Γ''' 𝒮''' P''' where
    "⊢ Γ''',𝒮''',P''' { c' } Γ',𝒮',P' ∧ 
    (tyenv_wellformed (update_modes upd mds) Γ'' 𝒮'' P'' ∧ pred P'' mem ∧ tyenv_sec (update_modes upd mds) Γ'' mem ⟶
       tyenv_wellformed mds' Γ''' 𝒮''' P''' ∧ pred P''' mem' ∧ tyenv_sec mds' Γ''' mem')"
    by blast
  moreover
  have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed (update_modes upd mds) Γ'' 𝒮'' P''"
    using anno_type
    apply auto
    by (metis tyenv_wellformed_mode_update)
  moreover
  have pred: "pred P mem ⟶ pred P'' mem"
    using anno_type
    by (auto simp: pred_def restrict_preds_to_vars_def)
  moreover
  have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶ tyenv_sec (update_modes upd mds) Γ'' mem"
    apply(rule impI)
    apply(rule tyenv_sec_mode_update)
            using anno_type apply fastforce
           using anno_type pred apply fastforce
          using anno_type apply fastforce
         using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
        using anno_type apply fastforce
       apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
      apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
     using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
    by simp  
  ultimately show ?case
    by blast
next
  case stop_type
  with stop_no_eval show ?case by auto
next
  case skip_type
  hence "c' = Stop ∧ mds' = mds ∧ mem' = mem"
    by (metis skip_elim)
  thus ?case
    by (metis stop_type)
next
  case (assign⇩1 x Γ e t P P' 𝒮 c' mds)
  hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
    by (metis assign_elim)
  from assign⇩1(2) upd have 𝒞_eq: "∀x∈𝒞. mem x = mem' x"
    by auto
  from upd have " ⊢ Γ,𝒮,P' {c'} Γ,𝒮,P'"
    by (metis stop_type)
  moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
    using upd tyenv_wellformed_preds_update assign⇩1 by metis
  moreover have "pred P mem ⟶ pred P' mem'"
    using pred_preds_update assign⇩1 upd by metis
    
  moreover have "tyenv_wellformed mds Γ 𝒮 P  ∧ tyenv_sec mds Γ mem ⟶ tyenv_sec mds Γ mem'"
    using tyenv_sec_eq[OF 𝒞_eq, where Γ=Γ]
    unfolding tyenv_wellformed_def by blast
  ultimately show ?case
    by (metis upd)
next
  case (assign⇩2 x Γ e t 𝒮 P' P c' mds)
  hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
    by (metis assign_elim)
  let ?Γ' = "Γ (x ↦ t)"
  from upd have ty: " ⊢ ?Γ',𝒮,P' {c'} ?Γ',𝒮,P'"
    by (metis stop_type)
  have wf: "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' ?Γ' 𝒮 P'"
  proof
    assume tyenv_wf: "tyenv_wellformed mds Γ 𝒮 P"
    hence wf: "types_wellformed Γ"
      unfolding tyenv_wellformed_def by blast
    hence  "type_wellformed t"
      using assign⇩2(2) type_aexpr_type_wellformed
      by blast
    with wf have wf': "types_wellformed ?Γ'"
      using types_wellformed_update by metis
    from tyenv_wf have stable': "types_stable ?Γ' 𝒮"
      using types_stable_update
            assign⇩2(3)
      unfolding tyenv_wellformed_def by blast
    have m: "mds_consistent mds Γ 𝒮 P"
      using tyenv_wf unfolding tyenv_wellformed_def by blast
    from assign⇩2(4) assign⇩2(1)
    have "mds_consistent mds' (Γ(x ↦ t)) 𝒮 P'"
      apply(rule mds_consistent_preds_tyenv_update)
      using upd m by simp
    from wf' stable' this show "tyenv_wellformed mds' ?Γ' 𝒮 P'"
      unfolding tyenv_wellformed_def by blast
  qed
  have p: "pred P mem ⟶ pred P' mem'"
    using pred_preds_update assign⇩2 upd by metis
  have sec: "tyenv_wellformed mds Γ 𝒮 P ⟹ pred P mem ⟹ tyenv_sec mds Γ mem ⟹ tyenv_sec mds' ?Γ' mem'"
  proof(clarify)
    assume wf: "tyenv_wellformed mds Γ 𝒮 P"
    assume pred: "pred P mem"
    assume sec: "tyenv_sec mds Γ mem"
    from pred p have pred': "pred P' mem'" by blast
    fix v t'
    assume Γv: "(Γ(x ↦ t)) v = Some t'"
    assume "v ∉ mds' AsmNoReadOrWrite"
    show "type_max (the ((Γ(x ↦ t)) v)) mem' ≤ dma mem' v"
    proof(cases "v = x")
      assume [simp]: "v = x"
      hence [simp]: "(the ((Γ(x ↦ t)) v)) = t" and t_def: "t = t'"
        using Γv by auto
      from ‹v ∉ mds' AsmNoReadOrWrite› upd wf have readable: "v ∉ snd 𝒮"
        by(auto simp: tyenv_wellformed_def mds_consistent_def)
      with assign⇩2(5) have "t ≤:⇩P' (dma_type x)" by fastforce
      with pred' show ?thesis
        using type_max_dma_type subtype_correct
        by fastforce
    next
      assume neq: "v ≠ x"
      hence [simp]: "((Γ(x ↦ t)) v) = Γ v"
        by simp
      with Γv have Γv: "Γ v = Some t'" by simp
      with sec upd ‹v ∉ mds' AsmNoReadOrWrite› have f_leq: "type_max t' mem ≤ dma mem v"
        by auto
      have 𝒞_eq: "∀x∈𝒞. mem x = mem' x"
        using wf assign⇩2(1) upd by(auto simp: tyenv_wellformed_def mds_consistent_def)
      hence dma_eq: "dma mem = dma mem'"
        by(rule dma_𝒞)
      have f_eq: "type_max t' mem = type_max t' mem'"
        apply(rule 𝒞_eq_type_max_eq)
         using Γv wf apply(force simp: tyenv_wellformed_def types_wellformed_def)
        by(rule 𝒞_eq)     
      from neq Γv f_leq dma_eq f_eq show ?thesis
        by simp
    qed
  qed
  from ty wf p sec show ?case
    by blast
next
  case (assign⇩𝒞 x Γ e t P P' 𝒮 c' mds)
  (* this case follows from the same argument as assign⇩1 *)
  hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
    by (metis assign_elim)
  hence " ⊢ Γ,𝒮,P' {c'} Γ,𝒮,P'"
    by (metis stop_type)
  moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
    using upd tyenv_wellformed_preds_update assign⇩𝒞 by metis
  moreover have "pred P mem ⟶ pred P' mem'"
    using pred_preds_update assign⇩𝒞 upd by metis
  moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟹ tyenv_sec mds' Γ mem'"
  proof(clarify)
    fix v t'
    assume wf: "tyenv_wellformed mds Γ 𝒮 P"
    assume pred: "pred P mem"
    hence pred': "pred P' mem'" using ‹pred P mem ⟶ pred P' mem'› by blast
    assume sec: "tyenv_sec mds Γ mem"
    assume Γv: "Γ v = Some t'"
    assume readable': "v ∉ mds' AsmNoReadOrWrite"
    with upd have readable: "v ∉ mds AsmNoReadOrWrite" by simp
    with wf have "v ∉ snd 𝒮" by(auto simp: tyenv_wellformed_def mds_consistent_def)
    show "type_max (the (Γ v)) mem' ≤ dma mem' v"
    proof(cases "x ∈ 𝒞_vars v")
      assume "x ∈ 𝒞_vars v"
      with assign⇩𝒞(6) ‹v ∉ snd 𝒮› have "(to_total Γ v) ≤:⇩P' (dma_type v)" by blast
      from pred' Γv subtype_correct this show ?thesis
        using type_max_dma_type by(auto simp: to_total_def split: if_splits)
    next
      assume "x ∉ 𝒞_vars v"
      hence "∀v'∈𝒞_vars v. mem v' = mem' v'"
        using upd by auto
      hence dma_eq: "dma mem v = dma mem' v"
        by(rule dma_𝒞_vars)
      from Γv assign⇩𝒞(4) have "x ∉ vars_of_type t'" by force
      have "type_wellformed t'"
        using wf Γv by(force simp: tyenv_wellformed_def types_wellformed_def)
      with ‹x ∉ vars_of_type t'› upd have f_eq: "type_max t' mem = type_max t' mem'"
        using vars_of_type_eq_type_max_eq by fastforce
      from sec Γv readable have "type_max t' mem ≤ dma mem v"
        by auto
      with f_eq dma_eq Γv show ?thesis
        by simp
    qed
  qed
  ultimately show ?case
    by (metis)
next
  case (if_type Γ e t P 𝒮 th Γ' 𝒮' P' el Γ'' P'' Γ''' P''' c' mds)
  from if_type(13)
  show ?case
  proof(rule if_elim)
    assume [simp]: "ev⇩B mem e" and [simp]: "c' = th" and [simp]: "mem' = mem" and [simp]: "mds' = mds"
    from if_type(3) have " ⊢ Γ,𝒮,P +⇩𝒮 e {c'} Γ',𝒮',P'" by simp
    hence "⊢ Γ,𝒮,P +⇩𝒮 e {c'} Γ''',𝒮',P'''"
      apply(rule sub)
           apply simp+
         using if_type apply blast
        using if_type apply blast
       apply simp
      using if_type apply(blast intro: pred_entailment_trans)
      done
    moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 (P +⇩𝒮 e)"
      by(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)
    moreover have "pred P mem ⟶ pred (P +⇩𝒮 e) mem'"
      by(auto simp: pred_def add_pred_def)
    moreover have "tyenv_sec mds Γ mem ⟶ tyenv_sec mds' Γ mem'"
      by(simp)
    ultimately show ?case by blast
  next
    assume [simp]: "¬ ev⇩B mem e" and [simp]: "c' = el" and [simp]: "mem' = mem" and [simp]: "mds' = mds"
    from if_type(5) have " ⊢ Γ,𝒮,P +⇩𝒮 bexp_neg e {c'} Γ'',𝒮',P''" by simp
    hence "⊢ Γ,𝒮,P +⇩𝒮 bexp_neg e {c'} Γ''',𝒮',P'''"
      apply(rule sub)
           apply simp+
         using if_type apply blast
        using if_type apply blast
       apply simp
      using if_type apply(blast intro: pred_entailment_trans)
      done
    moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 (P +⇩𝒮 bexp_neg e)"
      by(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)
    moreover have "pred P mem ⟶ pred (P +⇩𝒮 bexp_neg e) mem'"
      by(auto simp: pred_def add_pred_def bexp_neg_negates)
    moreover have "tyenv_sec mds Γ mem ⟶ tyenv_sec mds' Γ mem'"
      by(simp)
    ultimately show ?case by blast
  qed
next
  case (while_type Γ e t P 𝒮 c c' mds)
  hence [simp]: "mds' = mds ∧ c' = If e (c ;; While e c) Stop ∧ mem' = mem"
    by (metis while_elim)
  have " ⊢ Γ,𝒮,P {c'} Γ,𝒮,P"
    apply simp
    apply(rule if_type)
             apply(rule while_type(1))
            apply(rule while_type(2))
           apply(rule seq_type)
            apply(rule while_type(3))
           apply(rule has_type.while_type)
             apply(rule while_type(1))
            apply(rule while_type(2))
           apply(rule while_type(3))
          apply(rule stop_type)
         apply simp
        apply simp
       apply simp
      apply(rule add_pred_entailment)
      apply simp+
    by(blast intro!: tyenv_wellformed_subset add_pred_subset)
  thus ?case
    by fastforce
next
  case (seq_type Γ 𝒮 P c⇩1 Γ⇩1 𝒮⇩1 P⇩1 c⇩2 Γ⇩2 𝒮⇩2 P⇩2 c' mds)
  thus ?case
  proof (cases "c⇩1 = Stop")
    assume [simp]: "c⇩1 = Stop"
    with seq_type have [simp]: "mds' = mds" and [simp]: "c' = c⇩2" and [simp]: "mem' = mem"
      by (metis seq_stop_elim)+
    have context_eq: "context_equiv Γ P Γ⇩1" and [simp]: "𝒮⇩1 = 𝒮" and entail: "P ⊢ P⇩1" and
             wf_imp: "∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds Γ⇩1 𝒮 P⇩1"
      using stop_cxt seq_type(1) by simp+
    have "⊢ Γ,𝒮,P {c⇩2} Γ⇩2,𝒮⇩2,P⇩2"
      apply(rule sub)
            using seq_type(3) apply simp
           apply(rule context_eq)
          apply(rule wf_imp)
         apply simp+
       apply(rule entail)
      apply(rule pred_entailment_refl)
      done
    thus ?case
      by fastforce
  next
    assume "c⇩1 ≠ Stop"
    then obtain c⇩1' where step: "⟨c⇩1, mds, mem⟩ ↝ ⟨c⇩1', mds', mem'⟩ ∧ c' = (c⇩1' ;; c⇩2)"
      by (metis seq_elim seq_type.prems)
    then have "no_await c⇩1" using ‹no_await (c⇩1 ;; c⇩2)› no_await.cases by blast
    then obtain Γ''' 𝒮''' P''' where "⊢ Γ''',𝒮''',P''' {c⇩1'} Γ⇩1,𝒮⇩1,P⇩1 ∧
      (tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶ 
       tyenv_wellformed mds' Γ''' 𝒮''' P''' ∧ pred P''' mem' ∧ tyenv_sec mds' Γ''' mem')"
      using step seq_type(2)
      by blast
    moreover
    from seq_type have "⊢ Γ⇩1,𝒮⇩1,P⇩1 {c⇩2} Γ⇩2,𝒮⇩2,P⇩2" by auto
    moreover
    ultimately show ?case
      apply (rule_tac x = Γ''' in exI)
      using ‹⟨c⇩1, mds, mem⟩ ↝ ⟨c⇩1', mds', mem'⟩ ∧ c' = c⇩1' ;; c⇩2› by blast
  qed
next
  case (sub Γ⇩1 𝒮 P⇩1 c Γ⇩1' 𝒮' P⇩1' Γ⇩2 P⇩2 Γ⇩2' P⇩2' c' mds)
  then obtain Γ'' 𝒮'' P'' where stuff: "⊢ Γ'',𝒮'',P'' { c' } Γ⇩1',𝒮',P⇩1' ∧
    (tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem ∧ tyenv_sec mds Γ⇩1 mem ⟶ 
     tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧ pred P'' mem' ∧ tyenv_sec mds' Γ'' mem')"
    by force

  have imp: "tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ∧ pred P⇩2 mem ∧ tyenv_sec mds Γ⇩2 mem ⟹ 
             tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem ∧ tyenv_sec mds Γ⇩1 mem"
    apply(rule conjI)
     using sub(5) sub(4) tyenv_wellformed_sub unfolding pred_def
     apply blast
    apply(rule conjI) 
     using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
    using sub(3) context_equiv_tyenv_sec unfolding pred_def by blast
  show ?case
    apply (rule_tac x = Γ'' in exI, rule_tac x = "𝒮''" in exI, rule_tac x="P''" in exI)  
    apply (rule conjI)
     apply(rule has_type.sub)
           apply(rule stuff[THEN conjunct1])
          apply simp+
        apply(rule sub(5))
       apply(rule sub(6))
      apply simp
     using sub apply blast
    using imp stuff apply blast
   done
next
  case (await_type Γ e t P 𝒮 c Γ' 𝒮' P' c' mds)
    show ?case using no_await_no_await await_type.prems by blast 
qed


lemma preservation_no_await_plus: 
  "⟦⟨c, mds, mem⟩ ↝⇧+ ⟨c', mds', mem'⟩;
    ⊢ Γ,𝒮,P { c } Γ',𝒮',P';
    no_await c⟧ ⟹ 
     no_await c' ∧ (∃ Γ'' 𝒮'' P''. (⊢ Γ'',𝒮'',P'' { c' } Γ',𝒮',P') ∧ 
     (tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶ 
     tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧ pred P'' mem' ∧ tyenv_sec mds' Γ'' mem'))"
  apply (induct arbitrary: Γ 𝒮 P rule: my_trancl_step_induct3)
   using preservation_no_await no_await_trans apply fast
  using preservation_no_await no_await_trans by metis 

(* First we show that (roughly) typeability is preserved by evaluation steps *)
lemma preservation:
  assumes typed: "⊢ Γ,𝒮,P { c } Γ',𝒮',P'"
  assumes eval: "⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
  shows "∃ Γ'' 𝒮'' P''. (⊢ Γ'',𝒮'',P'' { c' } Γ',𝒮',P') ∧ 
                    (tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶ 
                      tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧ pred P'' mem' ∧ tyenv_sec mds' Γ'' mem')"
  using typed eval
proof (induct arbitrary: c' mds rule: has_type.induct)

  case (anno_type Γ'' Γ 𝒮 upd 𝒮'' P'' P c⇩1 Γ' 𝒮' P')
  hence "⟨c⇩1, update_modes upd mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
    by (metis upd_elim)
  with anno_type(5) obtain Γ''' 𝒮''' P''' where
    "⊢ Γ''',𝒮''',P''' { c' } Γ',𝒮',P' ∧ 
    (tyenv_wellformed (update_modes upd mds) Γ'' 𝒮'' P'' ∧ pred P'' mem ∧ tyenv_sec (update_modes upd mds) Γ'' mem ⟶
       tyenv_wellformed mds' Γ''' 𝒮''' P''' ∧ pred P''' mem' ∧ tyenv_sec mds' Γ''' mem')"
    by blast

  moreover
  have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed (update_modes upd mds) Γ'' 𝒮'' P''"
    using anno_type
    apply auto
    by (metis tyenv_wellformed_mode_update)
  moreover
  have pred: "pred P mem ⟶ pred P'' mem"
    using anno_type
    by (auto simp: pred_def restrict_preds_to_vars_def)
  moreover
  have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶ tyenv_sec (update_modes upd mds) Γ'' mem"
    apply(rule impI)
    apply(rule tyenv_sec_mode_update)
            using anno_type apply fastforce
           using anno_type pred apply fastforce
          using anno_type apply fastforce
         using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
        using anno_type apply fastforce
       apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
      apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
     using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
    by simp  
  ultimately show ?case
    by blast
next
  case stop_type
  with stop_no_eval show ?case ..
next
  case skip_type
  hence "c' = Stop ∧ mds' = mds ∧ mem' = mem"
    by (metis skip_elim)
  thus ?case
    by (metis stop_type)
next
  case (assign⇩1 x Γ e t P P' 𝒮 c' mds)
  hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
    by (metis assign_elim)
  from assign⇩1(2) upd have 𝒞_eq: "∀x∈𝒞. mem x = mem' x"
    by auto
  from upd have " ⊢ Γ,𝒮,P' {c'} Γ,𝒮,P'"
    by (metis stop_type)
  moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
    using upd tyenv_wellformed_preds_update assign⇩1 by metis
  moreover have "pred P mem ⟶ pred P' mem'"
    using pred_preds_update assign⇩1 upd by metis
    
  moreover have "tyenv_wellformed mds Γ 𝒮 P  ∧ tyenv_sec mds Γ mem ⟶ tyenv_sec mds Γ mem'"
    using tyenv_sec_eq[OF 𝒞_eq, where Γ=Γ]
    unfolding tyenv_wellformed_def by blast
  ultimately show ?case
    by (metis upd)
next
  case (assign⇩2 x Γ e t 𝒮 P' P c' mds)
  hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
    by (metis assign_elim)
  let ?Γ' = "Γ (x ↦ t)"
  from upd have ty: " ⊢ ?Γ',𝒮,P' {c'} ?Γ',𝒮,P'"
    by (metis stop_type)
  have wf: "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' ?Γ' 𝒮 P'"
  proof
    assume tyenv_wf: "tyenv_wellformed mds Γ 𝒮 P"
    hence wf: "types_wellformed Γ"
      unfolding tyenv_wellformed_def by blast
    hence  "type_wellformed t"
      using assign⇩2(2) type_aexpr_type_wellformed
      by blast
    with wf have wf': "types_wellformed ?Γ'"
      using types_wellformed_update by metis
    from tyenv_wf have stable': "types_stable ?Γ' 𝒮"
      using types_stable_update
            assign⇩2(3)
      unfolding tyenv_wellformed_def by blast
    have m: "mds_consistent mds Γ 𝒮 P"
      using tyenv_wf unfolding tyenv_wellformed_def by blast
    from assign⇩2(4) assign⇩2(1)
    have "mds_consistent mds' (Γ(x ↦ t)) 𝒮 P'"
      apply(rule mds_consistent_preds_tyenv_update)
      using upd m by simp
    from wf' stable' this show "tyenv_wellformed mds' ?Γ' 𝒮 P'"
      unfolding tyenv_wellformed_def by blast
  qed
  have p: "pred P mem ⟶ pred P' mem'"
    using pred_preds_update assign⇩2 upd by metis
  have sec: "tyenv_wellformed mds Γ 𝒮 P ⟹ pred P mem ⟹ tyenv_sec mds Γ mem ⟹ tyenv_sec mds' ?Γ' mem'"
  proof(clarify)
    assume wf: "tyenv_wellformed mds Γ 𝒮 P"
    assume pred: "pred P mem"
    assume sec: "tyenv_sec mds Γ mem"
    from pred p have pred': "pred P' mem'" by blast
    fix v t'
    assume Γv: "(Γ(x ↦ t)) v = Some t'"
    assume "v ∉ mds' AsmNoReadOrWrite"
    show "type_max (the ((Γ(x ↦ t)) v)) mem' ≤ dma mem' v"
    proof(cases "v = x")
      assume [simp]: "v = x"
      hence [simp]: "(the ((Γ(x ↦ t)) v)) = t" and t_def: "t = t'"
        using Γv by auto
      from ‹v ∉ mds' AsmNoReadOrWrite› upd wf have readable: "v ∉ snd 𝒮"
        by(auto simp: tyenv_wellformed_def mds_consistent_def)
      with assign⇩2(5) have "t ≤:⇩P' (dma_type x)" by fastforce
      with pred' show ?thesis
        using type_max_dma_type subtype_correct
        by fastforce
    next
      assume neq: "v ≠ x"
      hence [simp]: "((Γ(x ↦ t)) v) = Γ v"
        by simp
      with Γv have Γv: "Γ v = Some t'" by simp
      with sec upd ‹v ∉ mds' AsmNoReadOrWrite› have f_leq: "type_max t' mem ≤ dma mem v"
        by auto
      have 𝒞_eq: "∀x∈𝒞. mem x = mem' x"
        using wf assign⇩2(1) upd by(auto simp: tyenv_wellformed_def mds_consistent_def)
      hence dma_eq: "dma mem = dma mem'"
        by(rule dma_𝒞)
      have f_eq: "type_max t' mem = type_max t' mem'"
        apply(rule 𝒞_eq_type_max_eq)
         using Γv wf apply(force simp: tyenv_wellformed_def types_wellformed_def)
        by(rule 𝒞_eq)     
      from neq Γv f_leq dma_eq f_eq show ?thesis
        by simp
    qed
  qed
  from ty wf p sec show ?case
    by blast
next
  case (assign⇩𝒞 x Γ e t P P' 𝒮 c' mds)
  (* this case follows from the same argument as assign⇩1 *)
  hence upd: "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)"
    by (metis assign_elim)
  hence " ⊢ Γ,𝒮,P' {c'} Γ,𝒮,P'"
    by (metis stop_type)
  moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
    using upd tyenv_wellformed_preds_update assign⇩𝒞 by metis
  moreover have "pred P mem ⟶ pred P' mem'"
    using pred_preds_update assign⇩𝒞 upd by metis
  moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟹ tyenv_sec mds' Γ mem'"
  proof(clarify)
    fix v t'
    assume wf: "tyenv_wellformed mds Γ 𝒮 P"
    assume pred: "pred P mem"
    hence pred': "pred P' mem'" using ‹pred P mem ⟶ pred P' mem'› by blast
    assume sec: "tyenv_sec mds Γ mem"
    assume Γv: "Γ v = Some t'"
    assume readable': "v ∉ mds' AsmNoReadOrWrite"
    with upd have readable: "v ∉ mds AsmNoReadOrWrite" by simp
    with wf have "v ∉ snd 𝒮" by(auto simp: tyenv_wellformed_def mds_consistent_def)
    show "type_max (the (Γ v)) mem' ≤ dma mem' v"
    proof(cases "x ∈ 𝒞_vars v")
      assume "x ∈ 𝒞_vars v"
      with assign⇩𝒞(6) ‹v ∉ snd 𝒮› have "(to_total Γ v) ≤:⇩P' (dma_type v)" by blast
      from pred' Γv subtype_sound[OF this] show ?thesis
        using type_max_dma_type by(auto simp: to_total_def split: if_splits)
    next
      assume "x ∉ 𝒞_vars v"
      hence "∀v'∈𝒞_vars v. mem v' = mem' v'"
        using upd by auto
      hence dma_eq: "dma mem v = dma mem' v"
        by(rule dma_𝒞_vars)
      from Γv assign⇩𝒞(4) have "x ∉ vars_of_type t'" by force
      have "type_wellformed t'"
        using wf Γv by(force simp: tyenv_wellformed_def types_wellformed_def)
      with ‹x ∉ vars_of_type t'› upd have f_eq: "type_max t' mem = type_max t' mem'"
        using vars_of_type_eq_type_max_eq by fastforce
      from sec Γv readable have "type_max t' mem ≤ dma mem v"
        by auto
      with f_eq dma_eq Γv show ?thesis
        by simp
    qed
  qed
  ultimately show ?case
    by (metis stop_type)
next
  case (if_type Γ e t P 𝒮 th Γ' 𝒮' P' el Γ'' P'' Γ''' P''' c' mds)
  from if_type(13)
  show ?case
  proof(rule if_elim)
    assume [simp]: "ev⇩B mem e" and [simp]: "c' = th" and [simp]: "mem' = mem" and [simp]: "mds' = mds"
    from if_type(3) have " ⊢ Γ,𝒮,P +⇩𝒮 e {c'} Γ',𝒮',P'" by simp
    hence "⊢ Γ,𝒮,P +⇩𝒮 e {c'} Γ''',𝒮',P'''"
      apply(rule sub)
           apply simp+
         using if_type apply blast
        using if_type apply blast
       apply simp
      using if_type apply(blast intro: pred_entailment_trans)
      done
    moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 (P +⇩𝒮 e)"
      by(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)
    moreover have "pred P mem ⟶ pred (P +⇩𝒮 e) mem'"
      by(auto simp: pred_def add_pred_def)
    moreover have "tyenv_sec mds Γ mem ⟶ tyenv_sec mds' Γ mem'"
      by(simp)
    ultimately show ?case by blast
  next
    assume [simp]: "¬ ev⇩B mem e" and [simp]: "c' = el" and [simp]: "mem' = mem" and [simp]: "mds' = mds"
    from if_type(5) have " ⊢ Γ,𝒮,P +⇩𝒮 bexp_neg e {c'} Γ'',𝒮',P''" by simp
    hence "⊢ Γ,𝒮,P +⇩𝒮 bexp_neg e {c'} Γ''',𝒮',P'''"
      apply(rule sub)
           apply simp+
         using if_type apply blast
        using if_type apply blast
       apply simp
      using if_type apply(blast intro: pred_entailment_trans)
      done
    moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 (P +⇩𝒮 bexp_neg e)"
      by(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)
    moreover have "pred P mem ⟶ pred (P +⇩𝒮 bexp_neg e) mem'"
      by(auto simp: pred_def add_pred_def bexp_neg_negates)
    moreover have "tyenv_sec mds Γ mem ⟶ tyenv_sec mds' Γ mem'"
      by(simp)
    ultimately show ?case by blast
  qed
next
  case (while_type Γ e t P 𝒮 c c' mds)
  hence [simp]: "mds' = mds ∧ c' = If e (c ;; While e c) Stop ∧ mem' = mem"
    by (metis while_elim)
  have " ⊢ Γ,𝒮,P {c'} Γ,𝒮,P"
    apply simp
    apply(rule if_type)
             apply(rule while_type(1))
            apply(rule while_type(2))
           apply(rule seq_type)
            apply(rule while_type(3))
           apply(rule has_type.while_type)
             apply(rule while_type(1))
            apply(rule while_type(2))
           apply(rule while_type(3))
          apply(rule stop_type)
         apply simp
        apply simp
       apply simp
      apply(rule add_pred_entailment)
      apply simp+
    by(blast intro!: tyenv_wellformed_subset add_pred_subset)
  thus ?case
    by fastforce
next
  case (seq_type Γ 𝒮 P c⇩1 Γ⇩1 𝒮⇩1 P⇩1 c⇩2 Γ⇩2 𝒮⇩2 P⇩2 c' mds)
  thus ?case
  proof (cases "c⇩1 = Stop")
    assume [simp]: "c⇩1 = Stop"
    with seq_type have [simp]: "mds' = mds" and [simp]: "c' = c⇩2" and [simp]: "mem' = mem"
      by (metis seq_stop_elim)+
    have context_eq: "context_equiv Γ P Γ⇩1" and [simp]: "𝒮⇩1 = 𝒮" and entail: "P ⊢ P⇩1" and
             wf_imp: "∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds Γ⇩1 𝒮 P⇩1"
      using stop_cxt seq_type(1) by simp+
    have "⊢ Γ,𝒮,P {c⇩2} Γ⇩2,𝒮⇩2,P⇩2"
      apply(rule sub)
            using seq_type(3) apply simp
           apply(rule context_eq)
          apply(rule wf_imp)
         apply simp+
       apply(rule entail)
      apply(rule pred_entailment_refl)
      done
    thus ?case
      by fastforce
  next
    assume "c⇩1 ≠ Stop"
    then obtain c⇩1' where "⟨c⇩1, mds, mem⟩ ↝ ⟨c⇩1', mds', mem'⟩ ∧ c' = (c⇩1' ;; c⇩2)"
      by (metis seq_elim seq_type.prems)
    then obtain Γ''' 𝒮''' P''' where "⊢ Γ''',𝒮''',P''' {c⇩1'} Γ⇩1,𝒮⇩1,P⇩1 ∧
      (tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem ∧ tyenv_sec mds Γ mem ⟶ 
       tyenv_wellformed mds' Γ''' 𝒮''' P''' ∧ pred P''' mem' ∧ tyenv_sec mds' Γ''' mem')"
      using seq_type(2)
      by force
    moreover
    from seq_type have "⊢ Γ⇩1,𝒮⇩1,P⇩1 {c⇩2} Γ⇩2,𝒮⇩2,P⇩2" by auto
    moreover
    ultimately show ?case
      apply (rule_tac x = Γ''' in exI)
      using ‹⟨c⇩1, mds, mem⟩ ↝ ⟨c⇩1', mds', mem'⟩ ∧ c' = c⇩1' ;; c⇩2› by blast
  qed
next
  case (sub Γ⇩1 𝒮 P⇩1 c Γ⇩1' 𝒮' P⇩1' Γ⇩2 P⇩2 Γ⇩2' P⇩2' c' mds)
  then obtain Γ'' 𝒮'' P'' where stuff: "⊢ Γ'',𝒮'',P'' { c' } Γ⇩1',𝒮',P⇩1' ∧
    (tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem ∧ tyenv_sec mds Γ⇩1 mem ⟶ 
     tyenv_wellformed mds' Γ'' 𝒮'' P'' ∧ pred P'' mem' ∧ tyenv_sec mds' Γ'' mem')"
    by force

  have imp: "tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ∧ pred P⇩2 mem ∧ tyenv_sec mds Γ⇩2 mem ⟹ 
             tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem ∧ tyenv_sec mds Γ⇩1 mem"
    apply(rule conjI)
     using sub(5) sub(4) tyenv_wellformed_sub unfolding pred_def
     apply blast
    apply(rule conjI) 
     using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
    using sub(3) context_equiv_tyenv_sec unfolding pred_def by blast
  show ?case
    apply (rule_tac x = Γ'' in exI, rule_tac x = "𝒮''" in exI, rule_tac x="P''" in exI)  
    apply (rule conjI)
     apply(rule has_type.sub)
           apply(rule stuff[THEN conjunct1])
          apply simp+
        apply(rule sub(5))
       apply(rule sub(6))
      apply simp
     using sub apply blast
    using imp stuff apply blast
   done
next
  case (await_type Γ e t P 𝒮 c Γ' 𝒮' P' c' mds)
  from this show ?case
    apply simp
    apply (drule await_elim, clarsimp)
    apply (drule preservation_no_await_plus[of c mds mem c' mds' mem' Γ 𝒮 "P +⇩𝒮 e" Γ' 𝒮' P'], assumption+)
    apply (subgoal_tac "⟦ tyenv_wellformed mds Γ 𝒮 P ⟧ ⟹ tyenv_wellformed mds Γ 𝒮 P +⇩𝒮 e") defer
      apply (unfold add_pred_def)[1]
      apply (case_tac "pred_stable 𝒮 e", clarsimp)
        apply (unfold tyenv_wellformed_def, clarsimp)[1]
        apply (unfold mds_consistent_def, clarsimp)[1]
      apply clarsimp
    apply (subgoal_tac "pred P mem ⟹ pred P +⇩𝒮 e mem") defer
      apply (unfold add_pred_def)[1]
      apply (case_tac "pred_stable 𝒮 e", clarsimp)
        apply (unfold pred_def, clarsimp)[1]
      apply clarsimp
    apply clarsimp
    using has_type.sub by (metis context_equiv_refl pred_entailment_refl)
qed

inductive_cases await_type_elim: "⊢ Γ,𝒮,P {Await b ca} Γ',𝒮',P'"


fun bisim_helper :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒ bool"
  where
  "bisim_helper ⟨c⇩1, mds, mem⇩1⟩ ⟨c⇩2, mds⇩2, mem⇩2⟩ = mem⇩1 =⇘mds⇙⇧l mem⇩2"

lemma ℛ⇩3_mem_eq: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩ ⟹ mem⇩1 =⇘mds⇙⇧l mem⇩2"
  apply (subgoal_tac "bisim_helper ⟨c⇩1, mds, mem⇩1⟩ ⟨c⇩2, mds, mem⇩2⟩")
   apply simp
  apply (induct rule: ℛ⇩3_aux.induct)
  by (auto simp: ℛ⇩1_mem_eq)


lemma ev⇩A_eq:
  assumes tyenv_eq: "mem⇩1 =⇘Γ⇙ mem⇩2"
  assumes pred: "pred P mem⇩1" 
  assumes e_type: "Γ ⊢⇩a e ∈ t"
  assumes subtype: "t ≤:⇩P (dma_type v)"
  assumes is_Low: "dma mem⇩1 v = Low"
  shows "ev⇩A mem⇩1 e = ev⇩A mem⇩2 e"
proof(rule eval_vars_det⇩A, clarify)
  fix x
  assume in_vars: "x ∈ aexp_vars e"
  have "type_max (to_total Γ x) mem⇩1 = Low"
  proof -
    from subtype_sound[OF subtype] pred have "type_max t mem⇩1 ≤ dma mem⇩1 v"
      by(auto)
    with is_Low have "type_max t mem⇩1 = Low" by(auto simp: less_eq_Sec_def)
    with e_type in_vars show ?thesis
      apply -
      apply(erule type_aexpr.cases)
      using Sec.exhaust by(auto simp: type_max_def split: if_splits)
  qed
  thus "mem⇩1 x = mem⇩2 x"
    using tyenv_eq unfolding tyenv_eq_def by blast
qed

lemma ev⇩A_eq':
  assumes tyenv_eq: "mem⇩1 =⇘Γ⇙ mem⇩2"
  assumes pred: "pred P mem⇩1" 
  assumes e_type: "Γ ⊢⇩a e ∈ t"
  assumes subtype: "P ⊢ t"
  shows "ev⇩A mem⇩1 e = ev⇩A mem⇩2 e"
proof(rule eval_vars_det⇩A, clarify)
  fix x
  assume in_vars: "x ∈ aexp_vars e"
  have "type_max (to_total Γ x) mem⇩1 = Low"
  proof -
    from subtype pred have "type_max t mem⇩1 ≤ Low"
      by(auto simp: type_max_def pred_entailment_def pred_def)
    hence "type_max t mem⇩1 = Low" by(auto simp: less_eq_Sec_def)
    with e_type in_vars show ?thesis
      apply -
      apply(erule type_aexpr.cases)
      using Sec.exhaust by(auto simp: type_max_def  split: if_splits)
  qed
  thus "mem⇩1 x = mem⇩2 x"
    using tyenv_eq unfolding tyenv_eq_def by blast
qed

lemma ev⇩B_eq':
  assumes tyenv_eq: "mem⇩1 =⇘Γ⇙ mem⇩2"
  assumes pred: "pred P mem⇩1" 
  assumes e_type: "Γ ⊢⇩b e ∈ t"
  assumes subtype: "P ⊢ t"
  shows "ev⇩B mem⇩1 e = ev⇩B mem⇩2 e"
proof(rule eval_vars_det⇩B, clarify)
  fix x
  assume in_vars: "x ∈ bexp_vars e"
  have "type_max (to_total Γ x) mem⇩1 = Low"
  proof -
    from subtype pred have "type_max t mem⇩1 ≤ Low"
      by(auto simp: type_max_def pred_entailment_def pred_def)
    hence "type_max t mem⇩1 = Low" by(auto simp: less_eq_Sec_def)
    with e_type in_vars show ?thesis
      apply -
      apply(erule type_bexpr.cases)
      using Sec.exhaust by(auto simp: type_max_def  split: if_splits)
  qed
  thus "mem⇩1 x = mem⇩2 x"
    using tyenv_eq unfolding tyenv_eq_def by blast
qed

lemma R1_equiv_entailment:
  "⟨c, mds, mem⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c', mds', mem'⟩ ⟹  
  context_equiv Γ' P' Γ'' ⟹ P' ⊢ P'' ⟹
  ∀mds. tyenv_wellformed mds Γ' 𝒮' P' ⟶ tyenv_wellformed mds Γ'' 𝒮' P'' ⟹
   ⟨c, mds, mem⟩ ℛ⇧1⇘Γ'',𝒮',P''⇙ ⟨c', mds', mem'⟩"
  apply(induct rule: ℛ⇩1.induct)
  apply(rule ℛ⇩1.intro)
       apply(blast intro: sub context_equiv_refl pred_entailment_refl)+
  done

lemma R3_equiv_entailment:
  "⟨c, mds, mem⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c', mds', mem'⟩ ⟹ 
    context_equiv Γ' P' Γ'' ⟹ P' ⊢ P'' ⟹ 
  ∀mds. tyenv_wellformed mds Γ' 𝒮' P' ⟶ tyenv_wellformed mds Γ'' 𝒮' P'' ⟹
  ⟨c, mds, mem⟩ ℛ⇧3⇘Γ'',𝒮',P''⇙ ⟨c', mds', mem'⟩"
  apply(induct rule: ℛ⇩3_aux.induct)
   apply(erule ℛ⇩3_aux.intro⇩1)
   apply(blast intro: sub context_equiv_refl tyenv_wellformed_subset subset_entailment)
  apply(erule ℛ⇩3_aux.intro⇩3)
  apply(blast intro: sub context_equiv_refl tyenv_wellformed_subset subset_entailment)
  done

lemma R_equiv_entailment:
  "lc⇩1 ℛ⇧u⇘Γ',𝒮',P'⇙ lc⇩2 ⟹ 
    context_equiv Γ' P' Γ'' ⟹ P' ⊢ P'' ⟹ 
  ∀mds. tyenv_wellformed mds Γ' 𝒮' P' ⟶ tyenv_wellformed mds Γ'' 𝒮' P'' ⟹
  lc⇩1 ℛ⇧u⇘Γ'',𝒮',P''⇙ lc⇩2"
  apply(induct rule: ℛ.induct)
   apply clarsimp
   apply(rule ℛ.intro⇩1)
   apply(fastforce intro: R1_equiv_entailment)
  apply(rule ℛ.intro⇩3)
  apply(fastforce intro: R3_equiv_entailment)
  done

lemma context_equiv_tyenv_eq:
  "tyenv_eq Γ mem mem' ⟹ context_equiv Γ P Γ' ⟹ pred P mem ⟹ tyenv_eq Γ' mem mem'"
  apply(clarsimp simp: tyenv_eq_def to_total_def context_equiv_def split: if_splits simp: type_equiv_def)
  using subtype_trans subtype_sound
  by (metis domI less_eq_Sec_def option.sel)


lemma ℛ_typed_step_no_await:
"⟦ ⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P' ;
  tyenv_wellformed mds Γ 𝒮 P; mem⇩1 =⇘Γ⇙ mem⇩2; pred P mem⇩1;
        pred P mem⇩2; tyenv_sec mds Γ mem⇩1;
     ⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩; no_await c⇩1 ⟧ ⟹
   (∃ c⇩2' mem⇩2'. ⟨c⇩1, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
                 ⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
proof (induct arbitrary: mds c⇩1' rule: has_type.induct)
  case (seq_type Γ 𝒮 P c⇩1 Γ'' 𝒮'' P'' c⇩2 Γ' 𝒮' P' mds)
  show ?case
  proof (cases "c⇩1 = Stop")
    assume "c⇩1 = Stop"
    hence [simp]: "c⇩1' = c⇩2" "mds' = mds" "mem⇩1' = mem⇩1"
      using seq_type
      by (auto simp: seq_stop_elim)
    from seq_type ‹c⇩1 = Stop› have "context_equiv Γ P Γ''" and "𝒮 = 𝒮''" and "P ⊢ P''" and
                                   "(∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed  mds Γ'' 𝒮 P'')"
      by (metis stop_cxt)+
    hence "⊢ Γ,𝒮,P { c⇩2 } Γ',𝒮',P'"
      apply -
      apply(rule sub)
          using seq_type(3) apply simp
         by auto
    have "⟨c⇩2, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
      apply (rule ℛ⇩1.intro [of Γ])
           apply(rule ‹⊢ Γ,𝒮,P { c⇩2 } Γ',𝒮',P'›)
          using seq_type by auto
    thus ?case
      using ℛ.intro⇩1
      apply clarify
      apply (rule_tac x = c⇩2 in exI)
      apply (rule_tac x = mem⇩2 in exI)
      by (auto simp: ‹c⇩1 = Stop› seq_stop_eval⇩w  ℛ.intro⇩1)
  next
    assume "c⇩1 ≠ Stop"
    with ‹⟨c⇩1 ;; c⇩2, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩› obtain c⇩1'' where c⇩1''_props:
      "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩ ∧ c⇩1' = c⇩1'' ;; c⇩2"
      by (metis seq_elim)
    with ‹no_await (c⇩1 ;; c⇩2)› have "no_await c⇩1" using no_await.cases by blast
    with seq_type(2) ‹no_await c⇩1› obtain c⇩2'' mem⇩2' where c⇩2''_props:
      "⟨c⇩1, mds, mem⇩2⟩ ↝ ⟨c⇩2'', mds', mem⇩2'⟩ ∧ ⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩2'', mds', mem⇩2'⟩"
      using seq_type.prems(1) seq_type.prems(2) seq_type.prems(3) seq_type.prems(4) seq_type.prems(5) c⇩1''_props
      by blast
    hence "⟨c⇩1'' ;; c⇩2, mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2'' ;; c⇩2, mds', mem⇩2'⟩"
      apply (rule conjE)
      apply (erule ℛ_elim, auto)
       apply (metis ℛ.intro⇩3 ℛ⇩3_aux.intro⇩1 seq_type(3))
      by (metis ℛ.intro⇩3 ℛ⇩3_aux.intro⇩3 seq_type(3))
    moreover
    from c⇩2''_props have "⟨c⇩1 ;; c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2'' ;; c⇩2, mds', mem⇩2'⟩"
      by (metis eval⇩w.seq)
    ultimately show ?case
      by (metis c⇩1''_props)
  qed
next
  case (anno_type Γ' Γ 𝒮 upd 𝒮' P' P c Γ'' 𝒮'' P'' mds)
  have "mem⇩1 =⇘Γ'⇙ mem⇩2"
  proof(clarsimp simp: tyenv_eq_def)
    fix x  
    assume a: "type_max (to_total Γ' x) mem⇩1 = Low"
    hence "type_max (to_total Γ x) mem⇩1 = Low"
    proof -
      from ‹pred P mem⇩1› have "pred P' mem⇩1"
        using anno_type.hyps(3)
        by(auto simp: restrict_preds_to_vars_def pred_def)
      with subtype_correct anno_type.hyps(7) a 
      show ?thesis
        using less_eq_Sec_def by metis
    qed
    thus " mem⇩1 x = mem⇩2 x"
      using anno_type.prems(2)
      unfolding tyenv_eq_def by blast
  qed
  
  have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed (update_modes upd mds) Γ' 𝒮' P'"
    using anno_type
    apply auto
    by (metis tyenv_wellformed_mode_update)
  moreover
  have pred: "pred P mem⇩1 ⟶ pred P' mem⇩1"
    using anno_type
    by (auto simp: pred_def restrict_preds_to_vars_def)
  moreover
  have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ tyenv_sec mds Γ mem⇩1 ⟶ 
        tyenv_sec (update_modes upd mds) Γ' mem⇩1"
    apply(rule impI)
    apply(rule tyenv_sec_mode_update)
            using anno_type apply fastforce
           using anno_type pred apply fastforce
          using anno_type apply fastforce
         using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
        using anno_type apply fastforce
       apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
      apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
     using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
    by simp
  from ‹no_await (c@[upd])› have "no_await c" using no_await.cases by blast
  ultimately obtain c⇩2' mem⇩2' where "(⟨c, update_modes upd mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
    ⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
    using anno_type
    apply auto    
    using ‹mem⇩1 =⇘Γ'⇙ mem⇩2› local.pred_def restrict_preds_to_vars_def upd_elim ‹no_await c›
      (* TODO: cleanup *)
      using ‹tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ (∀x∈dom Γ. x ∉ mds AsmNoReadOrWrite ⟶ type_max (the (Γ x)) mem⇩1 ≤ dma mem⇩1 x) ⟶ (∀x∈dom Γ'. x ∉ update_modes upd mds AsmNoReadOrWrite ⟶ type_max (the (Γ' x)) mem⇩1 ≤ dma mem⇩1 x)› mem_Collect_eq by fastforce try0
  thus ?case
    apply (rule_tac x = c⇩2' in exI)
    apply (rule_tac x = mem⇩2' in exI)
    apply auto
    by (metis cxt_to_stmt.simps(1) eval⇩w.decl)
next
  case stop_type
  with stop_no_eval show ?case by auto
next
  case (skip_type Γ 𝒮 P mds)
  moreover
  with skip_type have [simp]: "mds' = mds" "c⇩1' = Stop" "mem⇩1' = mem⇩1"
    using skip_elim
    by (metis, metis, metis)
  with skip_type have "⟨Stop, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨Stop, mds, mem⇩2⟩"
    by auto
  thus ?case
    using ℛ.intro⇩1 and unannotated [where c = Skip and E = "[]"]
    apply auto
    by (metis (mono_tags, lifting) ℛ.intro⇩1 old.prod.case skip_eval⇩w)
next (* assign⇩1 *)
  case (assign⇩1 x Γ e t P P' 𝒮 mds)
  hence upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
    using assign_elim
    by (auto, metis)
  from assign⇩1(2) upd have 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩1' x"
    by auto
  have dma_eq [simp]: "dma mem⇩1 = dma mem⇩1'"
    using dma_𝒞 assign⇩1(2) by simp
  have "mem⇩1 (x := ev⇩A mem⇩1 e) =⇘Γ⇙ mem⇩2 (x := ev⇩A mem⇩2 e)"
  unfolding tyenv_eq_def
  proof(clarify)
    fix v
    assume is_Low': "type_max (to_total Γ v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
    show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
    proof(cases "v ∈ dom Γ")
      assume [simp]: "v ∈ dom Γ"
      then obtain t' where [simp]: "Γ v = Some t'" by force
      hence [simp]: "(to_total Γ v) = t'"
        unfolding to_total_def by (auto split: if_splits)
      have "type_max t' mem⇩1 = type_max t' mem⇩1'"
        apply(rule 𝒞_eq_type_max_eq)
         using ‹Γ v = Some t'› assign⇩1(6) 
         unfolding tyenv_wellformed_def types_wellformed_def
         apply (metis ‹v ∈ dom Γ› option.sel)
                
        using assign⇩1(2) apply simp
        done
      with is_Low' have is_Low: "type_max (to_total Γ v) mem⇩1 = Low"
        by simp
      from assign⇩1(1) ‹v ∈ dom Γ› have "x ≠ v" by auto
      thus ?thesis
        apply simp
        using is_Low assign⇩1(7) unfolding tyenv_eq_def by auto
    next
      assume "v ∉ dom Γ"
      hence [simp]: "⋀mem. type_max (to_total Γ v) mem = dma mem v"
        unfolding to_total_def by simp
      with is_Low' have "dma mem⇩1' v = Low" by simp
      with dma_eq have dma_v_Low: "dma mem⇩1 v = Low" by simp
      hence is_Low: "type_max (to_total Γ v) mem⇩1 = Low" by simp
      show ?thesis
      proof(cases "x = v")
        assume "x ≠ v"
        thus ?thesis
          apply simp
          using is_Low assign⇩1(7) unfolding tyenv_eq_def by blast
      next
        assume "x = v"
        thus ?thesis
          apply simp
          apply(rule ev⇩A_eq)
              apply(rule assign⇩1(7))
             apply(rule assign⇩1(8))
            apply(rule assign⇩1(3))
           apply(rule assign⇩1(4))
          using dma_v_Low by simp
      qed
    qed
  qed

  moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
    using upd tyenv_wellformed_preds_update assign⇩1 by metis
  moreover have "pred P mem⇩1 ⟶ pred P' mem⇩1'"
    using pred_preds_update assign⇩1 upd by metis

  moreover have "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
    using pred_preds_update assign⇩1 upd by metis
    
  moreover have "tyenv_wellformed mds Γ 𝒮 P  ∧ tyenv_sec mds Γ mem⇩1 ⟶ tyenv_sec mds Γ mem⇩1'"
    using tyenv_sec_eq[OF 𝒞_eq, where Γ=Γ]
    unfolding tyenv_wellformed_def by blast

  ultimately have ℛ':
    "⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ,𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    apply -
    apply (rule ℛ.intro⇩1, auto simp: assign⇩1 simp del: dma_eq)
    done

  have a: "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
  by (auto, metis cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.assign)

  from ℛ' a show ?case
    using ‹c⇩1' = Stop› and ‹mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)›
    by blast
next (* assign⇩𝒞 *)
  case (assign⇩𝒞 x Γ e t P P' 𝒮 mds)
  hence upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
    using assign_elim
    by (auto, metis)
  have "mem⇩1 (x := ev⇩A mem⇩1 e) =⇘Γ⇙ mem⇩2 (x := ev⇩A mem⇩2 e)"
  unfolding tyenv_eq_def
  proof(clarify)
    fix v
    assume is_Low': "type_max (to_total Γ v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
    show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
    proof(cases "v ∈ dom Γ")
      assume in_dom [simp]: "v ∈ dom Γ"
      then obtain t' where Γv [simp]: "Γ v = Some t'" by force
      hence [simp]: "(to_total Γ v) = t'"
        unfolding to_total_def by (auto split: if_splits)
      from assign⇩𝒞(4) have x_nin_C: "x ∉ vars_of_type t'"
        using in_dom Γv 
        by (metis option.sel snd_conv)
      have Γv_wf: "type_wellformed t'"
        using in_dom Γv assign⇩𝒞(7) unfolding tyenv_wellformed_def types_wellformed_def
        by (metis option.sel)
        
      with x_nin_C have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
        using vars_of_type_eq_type_max_eq by simp
      with is_Low' have is_Low: "type_max (to_total Γ v) mem⇩1 = Low"
        by simp  
      from assign⇩𝒞(1) ‹v ∈ dom Γ› assign⇩𝒞(7) have "x ≠ v"
        by(auto simp: tyenv_wellformed_def mds_consistent_def)
      thus ?thesis
        apply simp
        using is_Low assign⇩𝒞(8) unfolding tyenv_eq_def by auto
    next
      assume nin_dom: "v ∉ dom Γ"
      hence [simp]: "⋀mem. type_max (to_total Γ v) mem = dma mem v"
        unfolding to_total_def  by simp
      with is_Low' have "dma mem⇩1' v = Low" by simp
      show ?thesis
      proof(cases "x = v")
        assume "x = v"
        thus ?thesis
          apply simp
          apply(rule ev⇩A_eq')
             apply(rule assign⇩𝒞(8))
            apply(rule assign⇩𝒞(9))
           apply(rule assign⇩𝒞(2))
          by(rule assign⇩𝒞(3))
      next
        assume [simp]: "x ≠ v"
        show ?thesis
        proof(cases "x ∈ 𝒞_vars v")
          assume in_𝒞_vars: "x ∈ 𝒞_vars v"
          hence "v ∉ 𝒞"
            using 𝒞_vars_𝒞 by auto
          with nin_dom have "v ∉ snd 𝒮"
            using assign⇩𝒞(7)
            by(auto simp: tyenv_wellformed_def mds_consistent_def stable_def)
          with in_𝒞_vars have "P ⊢ (to_total Γ v)"
            using assign⇩𝒞(6) by blast
          with assign⇩𝒞(9) have "type_max (to_total Γ v) mem⇩1 = Low"
            by(auto simp: type_max_def pred_def pred_entailment_def)
          thus ?thesis
            using not_sym[OF ‹x ≠ v›]
            apply simp
            using assign⇩𝒞(8)
            unfolding tyenv_eq_def by auto
        next
          assume "x ∉ 𝒞_vars v"
          with is_Low' have "dma mem⇩1 v = Low"
            using dma_𝒞_vars ‹⋀mem. type_max (to_total Γ v) mem = dma mem v›
            by (metis fun_upd_other)
          thus ?thesis
            using not_sym[OF ‹x ≠ v›]
            apply simp
            using assign⇩𝒞(8)
            unfolding tyenv_eq_def by auto            
        qed
      qed
    qed
  qed

  moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
    using upd tyenv_wellformed_preds_update assign⇩𝒞 by metis
  moreover have "pred P mem⇩1 ⟶ pred P' mem⇩1'"
    using pred_preds_update assign⇩𝒞 upd by metis
  moreover have "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
    using pred_preds_update assign⇩𝒞 upd by metis
  moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ tyenv_sec mds Γ mem⇩1 ⟹ tyenv_sec mds' Γ mem⇩1'"
  proof(clarify)
    fix v t'
    assume wf: "tyenv_wellformed mds Γ 𝒮 P"
    assume pred: "pred P mem⇩1"
    hence pred': "pred P' mem⇩1'" using ‹pred P mem⇩1 ⟶ pred P' mem⇩1'› by blast
    assume sec: "tyenv_sec mds Γ mem⇩1"
    assume Γv: "Γ v = Some t'"
    assume readable': "v ∉ mds' AsmNoReadOrWrite"
    with upd have readable: "v ∉ mds AsmNoReadOrWrite" by simp
    with wf have "v ∉ snd 𝒮" by(auto simp: tyenv_wellformed_def mds_consistent_def)
    show "type_max (the (Γ v)) mem⇩1' ≤ dma mem⇩1' v"
    proof(cases "x ∈ 𝒞_vars v")
      assume "x ∈ 𝒞_vars v"
      with assign⇩𝒞(6) ‹v ∉ snd 𝒮› have "(to_total Γ v) ≤:⇩P' (dma_type v)" by blast
      from pred' Γv subtype_correct this show ?thesis
        using type_max_dma_type by(auto simp: to_total_def split: if_splits)
    next
      assume "x ∉ 𝒞_vars v"
      hence "∀v'∈𝒞_vars v. mem⇩1 v' = mem⇩1' v'"
        using upd by auto
      hence dma_eq: "dma mem⇩1 v = dma mem⇩1' v"
        by(rule dma_𝒞_vars)
      from Γv assign⇩𝒞(4) have "x ∉ vars_of_type t'" by force
      have "type_wellformed t'"
        using wf Γv by(force simp: tyenv_wellformed_def types_wellformed_def)
      with ‹x ∉ vars_of_type t'› upd have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
        using vars_of_type_eq_type_max_eq by fastforce
      from sec Γv readable have "type_max t' mem⇩1 ≤ dma mem⇩1 v"
        by auto
      with f_eq dma_eq Γv show ?thesis
        by simp
    qed
  qed

  ultimately have ℛ':
    "⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ,𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    apply -
    apply (rule ℛ.intro⇩1, auto simp: assign⇩𝒞)
    done

  have a: "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
  by (auto, metis cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.assign)

  from ℛ' a show ?case
    using ‹c⇩1' = Stop› and ‹mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)›
    by blast
next (* assign⇩2 *)
  case (assign⇩2 x Γ e t 𝒮 P' P mds)
  have upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
    using assign_elim[OF assign⇩2(11)]
    by auto
  from ‹x ∈ dom Γ› ‹tyenv_wellformed mds Γ 𝒮 P›
  have x_nin_𝒞: "x ∉ 𝒞"
    by(auto simp: tyenv_wellformed_def mds_consistent_def)
  hence dma_eq [simp]: "dma mem⇩1' = dma mem⇩1"
    using dma_𝒞 assign⇩2
    by auto
    
  let ?Γ' = "Γ (x ↦ t)"
  have "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds, mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    using assign⇩2
    by (metis cxt_to_stmt.simps(1) eval⇩w_simplep.assign eval⇩wp.unannotated eval⇩wp_eval⇩w_eq)
    
  moreover
  have tyenv_eq': "mem⇩1(x := ev⇩A mem⇩1 e) =⇘Γ(x ↦ t)⇙ mem⇩2(x := ev⇩A mem⇩2 e)"
  unfolding tyenv_eq_def
  proof(clarify)
    fix v
    assume is_Low': "type_max (to_total (Γ(x ↦ t)) v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
    show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
    proof(cases "v = x")
      assume neq: "v ≠ x"
      hence "type_max (to_total Γ v) mem⇩1 = Low"
      proof(cases "v ∈ dom Γ")
        assume "v ∈ dom Γ"
        then obtain t' where [simp]: "Γ v = Some t'" by force
        hence [simp]: "(to_total Γ v) = t'"
          unfolding to_total_def by (auto split: if_splits)
        hence [simp]: "(to_total ?Γ' v) = t'"
          using neq by(auto simp: to_total_def)
        have "type_max t' mem⇩1 = type_max t' mem⇩1'"
          apply(rule 𝒞_eq_type_max_eq)
            using assign⇩2(6) 
            apply(clarsimp simp: tyenv_wellformed_def types_wellformed_def)
            using ‹v ∈ dom Γ› ‹Γ v = Some t'› apply(metis option.sel)
           using x_nin_𝒞 by simp
        from this is_Low' neq neq[THEN not_sym] show "type_max (to_total Γ v) mem⇩1 = Low"
          by auto
      next
        assume "v ∉ dom Γ"
        with is_Low' neq
        have "dma mem⇩1' v = Low"
          by(auto simp: to_total_def  split: if_splits)
        with dma_eq ‹v ∉ dom Γ› show ?thesis
          by(auto simp: to_total_def  split: if_splits)
      qed
      with neq assign⇩2(7) show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
        by(auto simp: tyenv_eq_def)
    next
      assume eq[simp]: "v = x"
      with is_Low' ‹x ∈ dom Γ› have t_Low': "type_max t mem⇩1' = Low"
        by(auto simp: to_total_def split: if_splits)
      have wf_t: "type_wellformed t"
        using type_aexpr_type_wellformed assign⇩2(2) assign⇩2(6)
        by(fastforce simp: tyenv_wellformed_def)
      with t_Low' ‹x ∉ 𝒞› have t_Low: "type_max t mem⇩1 = Low"
        using 𝒞_eq_type_max_eq
        by (metis (no_types, lifting) fun_upd_other upd(3))
      show ?thesis
      proof(simp, rule eval_vars_det⇩A, clarify)
        fix y
        assume in_vars: "y ∈ aexp_vars e"
        have "type_max (to_total Γ y) mem⇩1 = Low"
        proof -
          from t_Low in_vars assign⇩2(2) show ?thesis
            apply -
            apply(erule type_aexpr.cases)
            using Sec.exhaust by(auto simp: type_max_def  split: if_splits)
        qed
        thus "mem⇩1 y = mem⇩2 y"
          using assign⇩2 unfolding tyenv_eq_def by blast
      qed
    qed
  qed

  from upd have ty: " ⊢ ?Γ',𝒮,P' {c⇩1'} ?Γ',𝒮,P'"
    by (metis stop_type)
  have wf: "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' ?Γ' 𝒮 P'"
  proof
    assume tyenv_wf: "tyenv_wellformed mds Γ 𝒮 P"
    hence wf: "types_wellformed Γ"
      unfolding tyenv_wellformed_def by blast
    hence  "type_wellformed t"
      using assign⇩2(2) type_aexpr_type_wellformed
      by blast
    with wf have wf': "types_wellformed ?Γ'"
      using types_wellformed_update by metis
    from tyenv_wf have stable': "types_stable ?Γ' 𝒮"
      using types_stable_update
            assign⇩2(3)
      unfolding tyenv_wellformed_def by blast
    have m: "mds_consistent mds Γ 𝒮 P"
      using tyenv_wf unfolding tyenv_wellformed_def by blast
    from assign⇩2(4) assign⇩2(1)
    have "mds_consistent mds' (Γ(x ↦ t)) 𝒮 P'"
      apply(rule mds_consistent_preds_tyenv_update)
      using upd m by simp
    from wf' stable' this show "tyenv_wellformed mds' ?Γ' 𝒮 P'"
      unfolding tyenv_wellformed_def by blast
  qed
  have p: "pred P mem⇩1 ⟶ pred P' mem⇩1'"
    using pred_preds_update assign⇩2 upd by metis
  have p⇩2: "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
    using pred_preds_update assign⇩2 upd by metis
  have sec: "tyenv_wellformed mds Γ 𝒮 P ⟹ pred P mem⇩1 ⟹ tyenv_sec mds Γ mem⇩1 ⟹ tyenv_sec mds' ?Γ' mem⇩1'"
  proof(clarify)
    assume wf: "tyenv_wellformed mds Γ 𝒮 P"
    assume pred: "pred P mem⇩1"
    assume sec: "tyenv_sec mds Γ mem⇩1"
    from pred p have pred': "pred P' mem⇩1'" by blast
    fix v t'
    assume Γv: "(Γ(x ↦ t)) v = Some t'"
    assume "v ∉ mds' AsmNoReadOrWrite"
    show "type_max (the ((Γ(x ↦ t)) v)) mem⇩1' ≤ dma mem⇩1' v"
    proof(cases "v = x")
      assume [simp]: "v = x"
      hence [simp]: "(the ((Γ(x ↦ t)) v)) = t" and t_def: "t = t'"
        using Γv by auto
      from ‹v ∉ mds' AsmNoReadOrWrite› upd wf have readable: "v ∉ snd 𝒮"
        by(auto simp: tyenv_wellformed_def mds_consistent_def)
      with assign⇩2(5) have "t ≤:⇩P' (dma_type x)" by fastforce
      with pred' show ?thesis
        using type_max_dma_type subtype_correct
        by fastforce
    next
      assume neq: "v ≠ x"
      hence [simp]: "((Γ(x ↦ t)) v) = Γ v"
        by simp
      with Γv have Γv: "Γ v = Some t'" by simp
      with sec upd ‹v ∉ mds' AsmNoReadOrWrite› have f_leq: "type_max t' mem⇩1 ≤ dma mem⇩1 v"
        by auto
      have 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩1' x"
        using wf assign⇩2(1) upd by(auto simp: tyenv_wellformed_def mds_consistent_def)
      hence dma_eq: "dma mem⇩1 = dma mem⇩1'"
        by(rule dma_𝒞)
      have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
        apply(rule 𝒞_eq_type_max_eq)
         using Γv wf apply(force simp: tyenv_wellformed_def types_wellformed_def)
        by(rule 𝒞_eq)     
      from neq Γv f_leq dma_eq f_eq show ?thesis
        by simp
    qed
  qed

  have "⟨Stop, mds, mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧1⇘?Γ',𝒮,P'⇙ ⟨Stop, mds, mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    apply(rule ℛ⇩1.intro)
         apply blast
        using wf assign⇩2 apply fastforce
       apply(rule tyenv_eq')
      using p assign⇩2 apply fastforce
     using p⇩2 assign⇩2 apply fastforce
    using sec assign⇩2
    using upd(2) upd(3) by blast
    
  ultimately have "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    "⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ(x ↦ t),𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    using ℛ.intro⇩1
    by auto
  thus ?case
    using ‹mds' = mds› ‹c⇩1' = Stop› ‹mem⇩1' = mem⇩1(x := ev⇩A mem⇩1 e)›
    by blast
next (* if *)
  case (if_type Γ e t P 𝒮 th Γ' 𝒮' P' el Γ'' P'' Γ''' P''')
  let ?P = "if (ev⇩B mem⇩1 e) then P +⇩𝒮 e else P +⇩𝒮 (bexp_neg e)"
  from ‹⟨Stmt.If e th el, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩› have ty: "⊢ Γ,𝒮,?P {c⇩1'} Γ''',𝒮',P'''"
  proof (rule if_elim)
    assume "c⇩1' = th" "mem⇩1' = mem⇩1" "mds' = mds" "ev⇩B mem⇩1 e"
    with if_type(3)
    show ?thesis
      apply simp
      apply(erule sub)
         using if_type apply simp+
      done
  next
    assume "c⇩1' = el" "mem⇩1' = mem⇩1" "mds' = mds" "¬ ev⇩B mem⇩1 e"
    with if_type(5)
    show ?thesis
      apply simp
      apply(erule sub)
         using if_type apply simp+
      done
  qed
  have ev⇩B_eq [simp]: "ev⇩B mem⇩1 e = ev⇩B mem⇩2 e"
    apply(rule ev⇩B_eq')
       apply(rule ‹mem⇩1 =⇘Γ⇙ mem⇩2›)
      apply(rule ‹pred P mem⇩1›)
     apply(rule ‹Γ ⊢⇩b e ∈ t›)
    by(rule ‹ P ⊢ t›)
  have "(⟨c⇩1', mds, mem⇩1⟩, ⟨c⇩1', mds, mem⇩2⟩) ∈ ℛ Γ''' 𝒮' P'''"
    apply (rule intro⇩1)
    apply clarify
    apply (rule ℛ⇩1.intro [where Γ = Γ and Γ' = Γ''' and 𝒮 = 𝒮 and P = ?P])
         apply(rule ty)
        using ‹tyenv_wellformed mds Γ 𝒮 P›
        apply(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)[1]
       apply(rule ‹mem⇩1 =⇘Γ⇙ mem⇩2›)       
      using ‹pred P mem⇩1› apply(fastforce simp: pred_def add_pred_def bexp_neg_negates)
     using ‹pred P mem⇩2› apply(fastforce simp: pred_def add_pred_def bexp_neg_negates)
    by(rule ‹tyenv_sec mds Γ mem⇩1›)

  show ?case
  proof -
    from ev⇩B_eq if_type(13) have "(⟨If e th el, mds, mem⇩2⟩ ↝ ⟨c⇩1', mds, mem⇩2⟩)"
      apply (cases "ev⇩B mem⇩1 e")
       apply (subgoal_tac "c⇩1' = th")
        apply clarify
        apply (metis cxt_to_stmt.simps(1) eval⇩w_simplep.if_true eval⇩wp.unannotated eval⇩wp_eval⇩w_eq if_type(8))
       using if_type.prems(6) apply blast
      apply (subgoal_tac "c⇩1' = el")
       apply (metis (opaque_lifting, mono_tags) cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.if_false if_type(8))
      using if_type.prems(6) by blast
    with ‹⟨c⇩1', mds, mem⇩1⟩ ℛ⇧u⇘Γ''',𝒮',P'''⇙ ⟨c⇩1', mds, mem⇩2⟩› show ?thesis  
    by (metis if_elim if_type.prems(6))    
  qed
next (* while *)
  case (while_type Γ e t P 𝒮 c)
  hence [simp]: "c⇩1' = (If e (c ;; While e c) Stop)" and
    [simp]: "mds' = mds" and
    [simp]: "mem⇩1' = mem⇩1"
    by (auto simp: while_elim)

  with while_type have "⟨While e c, mds, mem⇩2⟩ ↝ ⟨c⇩1', mds, mem⇩2⟩"
    by (metis cxt_to_stmt.simps(1) eval⇩w_simplep.while eval⇩wp.unannotated eval⇩wp_eval⇩w_eq)
    
  moreover have ty: " ⊢ Γ,𝒮,P {c⇩1'} Γ,𝒮,P"
    apply simp
    apply(rule if_type)
              apply(rule while_type(1))
             apply(rule while_type(2))
            apply(rule seq_type)
             apply(rule while_type(3))
            apply(rule has_type.while_type)
              apply(rule while_type(1))
             apply(rule while_type(2))
            apply(rule while_type(3))
           apply(rule stop_type)
          apply simp+
      apply(rule add_pred_entailment)
     apply simp
    apply(blast intro!: add_pred_subset tyenv_wellformed_subset)
    done
  moreover
  have "⟨c⇩1', mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩1', mds, mem⇩2⟩"
    apply (rule ℛ⇩1.intro [where Γ = Γ])
         apply(rule ty)
        using while_type apply simp+
    done
  hence "⟨c⇩1', mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩1', mds, mem⇩2⟩"
    using ℛ.intro⇩1 by auto
  ultimately show ?case
    by fastforce
next
  case (sub Γ⇩1 𝒮 P⇩1 c Γ⇩1' 𝒮' P⇩1' Γ⇩2 P⇩2 Γ⇩2' P⇩2' mds c⇩1')
  have imp: "tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ∧ pred P⇩2 mem⇩1 ∧ pred P⇩2 mem⇩2 ∧ tyenv_sec mds Γ⇩2 mem⇩1 ⟹ 
             tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem⇩1 ∧ pred P⇩1 mem⇩2 ∧ tyenv_sec mds Γ⇩1 mem⇩1"
    apply(rule conjI)
     using sub(5) sub(4) tyenv_wellformed_sub unfolding pred_def
     apply blast
    apply(rule conjI)
     using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
    apply(rule conjI)
     using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
    using sub(3) context_equiv_tyenv_sec unfolding pred_def by blast

  have tyenv_eq: "mem⇩1 =⇘Γ⇩1⇙ mem⇩2"
    using context_equiv_tyenv_eq sub by blast
    
  from imp tyenv_eq obtain c⇩2' mem⇩2' where c⇩2'_props: "⟨c, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩"
    "⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ⇩1',𝒮',P⇩1'⇙ ⟨c⇩2', mds', mem⇩2'⟩"
    using sub by blast 
  with R_equiv_entailment ‹P⇩1' ⊢ P⇩2'› show ?case
    using sub.hyps(6) sub.hyps(5) by blast
next case (await_type Γ e t P 𝒮 c Γ' 𝒮' P' Γ'' P'')
  from this show ?case using no_await_no_await by blast
qed

lemma is_final_ℛ⇩u_is_final:
  "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩ ⟹ is_final c⇩1 ⟹ is_final c⇩2"
  by (fastforce dest: bisim_simple_ℛ⇩u)

lemma pred_plus_impl:
  "pred P mem ⟹ ev⇩B mem e ⟹ pred P +⇩S e mem"
  unfolding add_pred_def pred_def by simp

lemma my_ℛ⇩3_aux_induct [consumes 1, case_names intro⇩1 intro⇩3]: 
  "⟦⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩;
   ⋀c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P'. 
     ⟦⟨c⇩1, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩; 
      ⊢ Γ,𝒮,P {c} Γ',𝒮',P'⟧ ⟹ 
    Q (c⇩1 ;; c) mds mem⇩1 Γ' 𝒮' P' (c⇩2 ;; c) mds mem⇩2;
   ⋀c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P'. 
     ⟦⟨c⇩1, mds, mem⇩1⟩ ℛ⇧3⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩; 
      Q c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mds mem⇩2; 
      ⊢ Γ,𝒮,P {c} Γ',𝒮',P'⟧ ⟹ 
    Q (c⇩1 ;; c) mds mem⇩1 Γ' 𝒮' P' (c⇩2 ;; c) mds mem⇩2⟧ ⟹ 
  Q c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mds mem⇩2"
using ℛ⇩3_aux.induct[where 
    ?x1.0 = "⟨c⇩1, mds, mem⇩1⟩" and
    ?x2.0 = Γ and
    ?x3.0 = 𝒮 and
    ?x4.0 = P and
    ?x5.0 = "⟨c⇩2, mds, mem⇩2⟩" and
    ?P = "λctx⇩1 Γ 𝒮 P ctx⇩2. Q (fst (fst ctx⇩1)) (snd (fst ctx⇩1)) (snd ctx⇩1) Γ 𝒮 P (fst (fst ctx⇩2)) (snd (fst ctx⇩2)) (snd ctx⇩2)"]
by force

lemma ℛ_typed_step_plus: 
  "⟦⟨c⇩1, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1', mds', mem⇩1'⟩; 
    ⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P';
    no_await c⇩1;
    tyenv_wellformed mds Γ 𝒮 P; 
    mem⇩1 =⇘Γ⇙ mem⇩2; 
    pred P mem⇩1;
    pred P mem⇩2; 
    tyenv_sec mds Γ mem⇩1 ⟧ ⟹ 
   (∃ c⇩2' mem⇩2'. ⟨c⇩1, mds, mem⇩2⟩ ↝⇧+ ⟨c⇩2', mds', mem⇩2'⟩ ∧
                 ⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
proof (induct arbitrary: Γ 𝒮 P mem⇩2 rule: my_trancl_big_step_induct3)
  case (base c⇩1 mds mem⇩1 c⇩1' mds' mem⇩1')
  from this show ?case using ℛ_typed_step_no_await bisim_simple_ℛ⇩u by fast
next 
  case (step c⇩1 mds mem⇩1 c⇩1' mds' mem⇩1' c⇩1'' mds'' mem⇩1'') 
  from this obtain mem⇩2' where step⇩2': "⟨c⇩1, mds, mem⇩2⟩ ↝⇧+ ⟨c⇩1', mds', mem⇩2'⟩" and
      rel⇩2': "⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩1', mds', mem⇩2'⟩"
    using bisim_simple_ℛ⇩u by (metis fst_conv)
  from rel⇩2' show ?case
  proof(cases rule: ℛ.cases)
    case (intro⇩1) 
    from this obtain Γ'' 𝒮'' P'' where 
      "⊢ Γ'',𝒮'',P'' {c⇩1'} Γ',𝒮',P'" 
      "tyenv_wellformed mds' Γ'' 𝒮'' P''"
      "mem⇩1' =⇘Γ''⇙ mem⇩2'"
      "pred P'' mem⇩1'"
      "pred P'' mem⇩2'"
      "∀x∈dom Γ''. x ∉ mds' AsmNoReadOrWrite ⟶ type_max (the (Γ'' x)) mem⇩1' ≤ dma mem⇩1' x"
      using ℛ⇩1.cases by auto
    from step⇩2' ‹no_await c⇩1› step.hyps(1) step.hyps(4) this obtain mem⇩2'' where 
        step⇩2'': "⟨c⇩1', mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩" and 
        rel⇩2'': "⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩1'', mds'', mem⇩2''⟩"
      using no_await_trancl bisim_simple_ℛ⇩u by (metis fst_conv)
    from this step⇩2' show ?thesis using trancl_trans by fast
  next 
    case (intro⇩3)
    from intro⇩3 step.prems step.hyps(1) step.hyps(3) step.hyps(4) obtain mem⇩2'' where
        step'': "⟨c⇩1', mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩" and 
        rel'': "⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩1'', mds'', mem⇩2''⟩"
    proof (induct arbitrary: rule: my_ℛ⇩3_aux_induct)
      case (intro⇩1 c⇩1'1' mds' mem⇩1' Γ''' 𝒮''' P''' c⇩1'1 mem⇩2' c⇩1'2 Γ'' 𝒮'' P'')
      from intro⇩1(1) obtain Γv 𝒮v Pv where pre_props: 
        "⊢ Γv,𝒮v,Pv {c⇩1'1} Γ''',𝒮''',P'''" 
        "tyenv_wellformed mds' Γv 𝒮v Pv"
        "mem⇩1' =⇘Γv⇙ mem⇩2'"
        "pred Pv mem⇩1'"
        "pred Pv mem⇩2'"
        "c⇩1'1 = c⇩1'1'"
        "∀x∈dom Γv. x ∉ mds' AsmNoReadOrWrite ⟶ type_max (the (Γv x)) mem⇩1' ≤ dma mem⇩1' x"
        using ℛ⇩1.cases by blast
      from this intro⇩1 have typed: "⊢ Γv,𝒮v,Pv {c⇩1'1 ;; c⇩1'2} Γ'',𝒮'',P''"
        using has_type.seq_type by blast
      from this pre_props ‹no_await c⇩1› ‹⟨c⇩1, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩1'⟩› intro⇩1(13)
        obtain mem⇩2'' where 
               step: "⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩ ∧ 
                      ⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩1'', mds'', mem⇩2''⟩"
        using no_await_trancl bisim_simple_ℛ⇩u by (metis fst_conv)
      from this intro⇩1(3) show ?case using no_await_trancl bisim_simple_ℛ⇩u by blast
    next 
      case (intro⇩3 c⇩1'1' mds' mem⇩1' Γ''' 𝒮''' P''' c⇩1'1 mem⇩2' c⇩1'2 Γ'' 𝒮'' P'')
      from intro⇩3(1) obtain Γv 𝒮v Pv where pre_props: 
        "⊢ Γv,𝒮v,Pv {c⇩1'1} Γ''',𝒮''',P'''" 
        "tyenv_wellformed mds' Γv 𝒮v Pv"
        "mem⇩1' =⇘Γv⇙ mem⇩2'"
        "pred Pv mem⇩1'"
        "pred Pv mem⇩2'"
        "c⇩1'1 = c⇩1'1'"
        "∀x∈dom Γv. x ∉ mds' AsmNoReadOrWrite ⟶ type_max (the (Γv x)) mem⇩1' ≤ dma mem⇩1' x"
        by (induct arbitrary: rule: my_ℛ⇩3_aux_induct) 
           (blast elim: ℛ⇩1.cases, blast) 
      from this intro⇩1 have typed: "⊢ Γv,𝒮v,Pv {c⇩1'1 ;; c⇩1'2} Γ'',𝒮'',P''"
        using has_type.seq_type intro⇩3.hyps(3) by blast

      from this pre_props ‹no_await c⇩1› ‹⟨c⇩1, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩1'⟩› intro⇩3
        obtain mem⇩2'' where 
        step: "⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩ ∧ 
               ⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩1'', mds'', mem⇩2''⟩"   
      proof -
        assume a1: "⋀mem⇩2''. ⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩2'⟩ ↝⇧+ ⟨c⇩1'', mds'', mem⇩2''⟩ ∧ 
                               ⟨c⇩1'', mds'', mem⇩1''⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩1'', mds'', mem⇩2''⟩ ⟹ thesis"
        thus ?thesis using intro⇩3.prems(11)
          using a1 by (metis (no_types) pre_props(2-)
                       ‹⟨c⇩1, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1'1 ;; c⇩1'2, mds', mem⇩1'⟩›  ‹no_await c⇩1› 
                       bisim_simple_ℛ⇩u fst_conv no_await_trancl typed)
      qed
      from this intro⇩3 show ?case using no_await_trancl bisim_simple_ℛ⇩u by blast
    qed
    thus ?thesis 
      by (meson step⇩2' trancl_trans) 
  qed
qed

(* This is the main part of the proof and used in ℛ⇩1_weak_bisim: *)
lemma ℛ_typed_step:
  "⟦ ⊢ Γ,𝒮,P { c⇩1 } Γ',𝒮',P' ;
  tyenv_wellformed mds Γ 𝒮 P; mem⇩1 =⇘Γ⇙ mem⇩2; pred P mem⇩1;
        pred P mem⇩2; tyenv_sec mds Γ mem⇩1;
     ⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩ ⟧ ⟹
   (∃ c⇩2' mem⇩2'. ⟨c⇩1, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
                 ⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
proof (induct arbitrary: mds c⇩1' rule: has_type.induct)
  case (seq_type Γ 𝒮 P c⇩1 Γ'' 𝒮'' P'' c⇩2 Γ' 𝒮' P' mds)
  show ?case
  proof (cases "c⇩1 = Stop")
    assume "c⇩1 = Stop"
    hence [simp]: "c⇩1' = c⇩2" "mds' = mds" "mem⇩1' = mem⇩1"
      using seq_type
      by (auto simp: seq_stop_elim)
    from seq_type ‹c⇩1 = Stop› have "context_equiv Γ P Γ''" and "𝒮 = 𝒮''" and "P ⊢ P''" and
                                   "(∀mds. tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed  mds Γ'' 𝒮 P'')"
      by (metis stop_cxt)+
    hence "⊢ Γ,𝒮,P { c⇩2 } Γ',𝒮',P'"
      apply -
      apply(rule sub)
          using seq_type(3) apply simp
         by auto
    have "⟨c⇩2, mds, mem⇩1⟩ ℛ⇧1⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
      apply (rule ℛ⇩1.intro [of Γ])
           apply(rule ‹⊢ Γ,𝒮,P { c⇩2 } Γ',𝒮',P'›)
          using seq_type by auto
    thus ?case
      using ℛ.intro⇩1
      apply clarify
      apply (rule_tac x = c⇩2 in exI)
      apply (rule_tac x = mem⇩2 in exI)
      by (auto simp: ‹c⇩1 = Stop› seq_stop_eval⇩w  ℛ.intro⇩1)
  next
    assume "c⇩1 ≠ Stop"
    with ‹⟨c⇩1 ;; c⇩2, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩› obtain c⇩1'' where c⇩1''_props:
      "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩ ∧ c⇩1' = c⇩1'' ;; c⇩2"
      by (metis seq_elim)
    with seq_type(2) obtain c⇩2'' mem⇩2' where c⇩2''_props:
      "⟨c⇩1, mds, mem⇩2⟩ ↝ ⟨c⇩2'', mds', mem⇩2'⟩ ∧ ⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩2'', mds', mem⇩2'⟩"
      using seq_type.prems(1) seq_type.prems(2) seq_type.prems(3) seq_type.prems(4) seq_type.prems(5) by presburger
    hence "⟨c⇩1'' ;; c⇩2, mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2'' ;; c⇩2, mds', mem⇩2'⟩"
      apply (rule conjE)
      apply (erule ℛ_elim, auto)
       apply (metis ℛ.intro⇩3 ℛ⇩3_aux.intro⇩1 seq_type(3))
      by (metis ℛ.intro⇩3 ℛ⇩3_aux.intro⇩3 seq_type(3))
    moreover
    from c⇩2''_props have "⟨c⇩1 ;; c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2'' ;; c⇩2, mds', mem⇩2'⟩"
      by (metis eval⇩w.seq)
    ultimately show ?case
      by (metis c⇩1''_props)
  qed
next
  case (anno_type Γ' Γ 𝒮 upd 𝒮' P' P c Γ'' 𝒮'' P'' mds)
  have "mem⇩1 =⇘Γ'⇙ mem⇩2"
  proof(clarsimp simp: tyenv_eq_def)
    fix x  
    assume a: "type_max (to_total Γ' x) mem⇩1 = Low"
    hence "type_max (to_total Γ x) mem⇩1 = Low"
    proof -
      from ‹pred P mem⇩1› have "pred P' mem⇩1"
        using anno_type.hyps(3)
        by(auto simp: restrict_preds_to_vars_def pred_def)
      with subtype_sound[OF anno_type.hyps(7)] a 
      show ?thesis
        using less_eq_Sec_def by metis
    qed
    thus " mem⇩1 x = mem⇩2 x"
      using anno_type.prems(2)
      unfolding tyenv_eq_def by blast
  qed
  
  have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed (update_modes upd mds) Γ' 𝒮' P'"
    using anno_type
    apply auto
    by (metis tyenv_wellformed_mode_update)
  moreover
  have pred: "pred P mem⇩1 ⟶ pred P' mem⇩1"
    using anno_type
    by (auto simp: pred_def restrict_preds_to_vars_def)
  moreover
  have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ tyenv_sec mds Γ mem⇩1 ⟶ 
        tyenv_sec (update_modes upd mds) Γ' mem⇩1"
    apply(rule impI)
    apply(rule tyenv_sec_mode_update)
            using anno_type apply fastforce
           using anno_type pred apply fastforce
          using anno_type apply fastforce
         using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
        using anno_type apply fastforce
       apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
      apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
     using anno_type apply(fastforce simp: tyenv_wellformed_def mds_consistent_def)
    by simp  
  ultimately obtain c⇩2' mem⇩2' where "(⟨c, update_modes upd mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
    ⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ'',𝒮'',P''⇙ ⟨c⇩2', mds', mem⇩2'⟩)"
    using anno_type
    apply auto    
    using ‹mem⇩1 =⇘Γ'⇙ mem⇩2› local.pred_def restrict_preds_to_vars_def upd_elim by fastforce
  thus ?case
    apply (rule_tac x = c⇩2' in exI)
    apply (rule_tac x = mem⇩2' in exI)
    apply auto
    by (metis cxt_to_stmt.simps(1) eval⇩w.decl)
next
  case stop_type
  with stop_no_eval show ?case by auto
next
  case (skip_type Γ 𝒮 P mds)
  moreover
  with skip_type have [simp]: "mds' = mds" "c⇩1' = Stop" "mem⇩1' = mem⇩1"
    using skip_elim
    by (metis, metis, metis)
  with skip_type have "⟨Stop, mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨Stop, mds, mem⇩2⟩"
    by auto
  thus ?case
    using ℛ.intro⇩1 and unannotated [where c = Skip and E = "[]"]
    apply auto
    by (metis (mono_tags, lifting) ℛ.intro⇩1 old.prod.case skip_eval⇩w)
next (* assign⇩1 *)
  case (assign⇩1 x Γ e t P P' 𝒮 mds)
  hence upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
    using assign_elim
    by (auto, metis)
  from assign⇩1(2) upd have 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩1' x"
    by auto
  have dma_eq [simp]: "dma mem⇩1 = dma mem⇩1'"
    using dma_𝒞 assign⇩1(2) by simp
  have "mem⇩1 (x := ev⇩A mem⇩1 e) =⇘Γ⇙ mem⇩2 (x := ev⇩A mem⇩2 e)"
  unfolding tyenv_eq_def
  proof(clarify)
    fix v
    assume is_Low': "type_max (to_total Γ v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
    show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
    proof(cases "v ∈ dom Γ")
      assume [simp]: "v ∈ dom Γ"
      then obtain t' where [simp]: "Γ v = Some t'" by force
      hence [simp]: "(to_total Γ v) = t'"
        unfolding to_total_def by (auto split: if_splits)
      have "type_max t' mem⇩1 = type_max t' mem⇩1'"
        apply(rule 𝒞_eq_type_max_eq)
         using ‹Γ v = Some t'› assign⇩1(6) 
         unfolding tyenv_wellformed_def types_wellformed_def
         apply (metis ‹v ∈ dom Γ› option.sel)
                
        using assign⇩1(2) apply simp
        done
      with is_Low' have is_Low: "type_max (to_total Γ v) mem⇩1 = Low"
        by simp
      from assign⇩1(1) ‹v ∈ dom Γ› have "x ≠ v" by auto
      thus ?thesis
        apply simp
        using is_Low assign⇩1(7) unfolding tyenv_eq_def by auto
    next
      assume "v ∉ dom Γ"
      hence [simp]: "⋀mem. type_max (to_total Γ v) mem = dma mem v"
        unfolding to_total_def by simp
      with is_Low' have "dma mem⇩1' v = Low" by simp
      with dma_eq have dma_v_Low: "dma mem⇩1 v = Low" by simp
      hence is_Low: "type_max (to_total Γ v) mem⇩1 = Low" by simp
      show ?thesis
      proof(cases "x = v")
        assume "x ≠ v"
        thus ?thesis
          apply simp
          using is_Low assign⇩1(7) unfolding tyenv_eq_def by blast
      next
        assume "x = v"
        thus ?thesis
          apply simp
          apply(rule ev⇩A_eq)
              apply(rule assign⇩1(7))
             apply(rule assign⇩1(8))
            apply(rule assign⇩1(3))
           apply(rule assign⇩1(4))
          using dma_v_Low by simp
      qed
    qed
  qed

  moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
    using upd tyenv_wellformed_preds_update assign⇩1 by metis
  moreover have "pred P mem⇩1 ⟶ pred P' mem⇩1'"
    using pred_preds_update assign⇩1 upd by metis

  moreover have "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
    using pred_preds_update assign⇩1 upd by metis
    
  moreover have "tyenv_wellformed mds Γ 𝒮 P  ∧ tyenv_sec mds Γ mem⇩1 ⟶ tyenv_sec mds Γ mem⇩1'"
    using tyenv_sec_eq[OF 𝒞_eq, where Γ=Γ]
    unfolding tyenv_wellformed_def by blast

  ultimately have ℛ':
    "⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ,𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    apply -
    apply (rule ℛ.intro⇩1, auto simp: assign⇩1 simp del: dma_eq)
    done

  have a: "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
  by (auto, metis cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.assign)

  from ℛ' a show ?case
    using ‹c⇩1' = Stop› and ‹mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)›
    by blast
next (* assign⇩𝒞 *)
  case (assign⇩𝒞 x Γ e t P P' 𝒮 mds)
  hence upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
    using assign_elim
    by (auto, metis)
  have "mem⇩1 (x := ev⇩A mem⇩1 e) =⇘Γ⇙ mem⇩2 (x := ev⇩A mem⇩2 e)"
  unfolding tyenv_eq_def
  proof(clarify)
    fix v
    assume is_Low': "type_max (to_total Γ v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
    show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
    proof(cases "v ∈ dom Γ")
      assume in_dom [simp]: "v ∈ dom Γ"
      then obtain t' where Γv [simp]: "Γ v = Some t'" by force
      hence [simp]: "(to_total Γ v) = t'"
        unfolding to_total_def by (auto split: if_splits)
      from assign⇩𝒞(4) have x_nin_C: "x ∉ vars_of_type t'"
        using in_dom Γv 
        by (metis option.sel snd_conv)
      have Γv_wf: "type_wellformed t'"
        using in_dom Γv assign⇩𝒞(7) unfolding tyenv_wellformed_def types_wellformed_def
        by (metis option.sel)
        
      with x_nin_C have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
        using vars_of_type_eq_type_max_eq by simp
      with is_Low' have is_Low: "type_max (to_total Γ v) mem⇩1 = Low"
        by simp  
      from assign⇩𝒞(1) ‹v ∈ dom Γ› assign⇩𝒞(7) have "x ≠ v"
        by(auto simp: tyenv_wellformed_def mds_consistent_def)
      thus ?thesis
        apply simp
        using is_Low assign⇩𝒞(8) unfolding tyenv_eq_def by auto
    next
      assume nin_dom: "v ∉ dom Γ"
      hence [simp]: "⋀mem. type_max (to_total Γ v) mem = dma mem v"
        unfolding to_total_def  by simp
      with is_Low' have "dma mem⇩1' v = Low" by simp
      show ?thesis
      proof(cases "x = v")
        assume "x = v"
        thus ?thesis
          apply simp
          apply(rule ev⇩A_eq')
             apply(rule assign⇩𝒞(8))
            apply(rule assign⇩𝒞(9))
           apply(rule assign⇩𝒞(2))
          by(rule assign⇩𝒞(3))
      next
        assume [simp]: "x ≠ v"
        show ?thesis
        proof(cases "x ∈ 𝒞_vars v")
          assume in_𝒞_vars: "x ∈ 𝒞_vars v"
          hence "v ∉ 𝒞"
            using 𝒞_vars_𝒞 by auto
          with nin_dom have "v ∉ snd 𝒮"
            using assign⇩𝒞(7)
            by(auto simp: tyenv_wellformed_def mds_consistent_def stable_def)
          with in_𝒞_vars have "P ⊢ (to_total Γ v)"
            using assign⇩𝒞(6) by blast
          with assign⇩𝒞(9) have "type_max (to_total Γ v) mem⇩1 = Low"
            by(auto simp: type_max_def pred_def pred_entailment_def)
          thus ?thesis
            using not_sym[OF ‹x ≠ v›]
            apply simp
            using assign⇩𝒞(8)
            unfolding tyenv_eq_def by auto
        next
          assume "x ∉ 𝒞_vars v"
          with is_Low' have "dma mem⇩1 v = Low"
            using dma_𝒞_vars ‹⋀mem. type_max (to_total Γ v) mem = dma mem v›
            by (metis fun_upd_other)
          thus ?thesis
            using not_sym[OF ‹x ≠ v›]
            apply simp
            using assign⇩𝒞(8)
            unfolding tyenv_eq_def by auto            
        qed
      qed
    qed
  qed

  moreover have "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' Γ 𝒮 P'"
    using upd tyenv_wellformed_preds_update assign⇩𝒞 by metis
  moreover have "pred P mem⇩1 ⟶ pred P' mem⇩1'"
    using pred_preds_update assign⇩𝒞 upd by metis
  moreover have "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
    using pred_preds_update assign⇩𝒞 upd by metis
  moreover have "tyenv_wellformed mds Γ 𝒮 P ∧ pred P mem⇩1 ∧ tyenv_sec mds Γ mem⇩1 ⟹ tyenv_sec mds' Γ mem⇩1'"
  proof(clarify)
    fix v t'
    assume wf: "tyenv_wellformed mds Γ 𝒮 P"
    assume pred: "pred P mem⇩1"
    hence pred': "pred P' mem⇩1'" using ‹pred P mem⇩1 ⟶ pred P' mem⇩1'› by blast
    assume sec: "tyenv_sec mds Γ mem⇩1"
    assume Γv: "Γ v = Some t'"
    assume readable': "v ∉ mds' AsmNoReadOrWrite"
    with upd have readable: "v ∉ mds AsmNoReadOrWrite" by simp
    with wf have "v ∉ snd 𝒮" by(auto simp: tyenv_wellformed_def mds_consistent_def)
    show "type_max (the (Γ v)) mem⇩1' ≤ dma mem⇩1' v"
    proof(cases "x ∈ 𝒞_vars v")
      assume "x ∈ 𝒞_vars v"
      with assign⇩𝒞(6) ‹v ∉ snd 𝒮› have "(to_total Γ v) ≤:⇩P' (dma_type v)" by blast
      from pred' Γv subtype_sound[OF this] show ?thesis
        using type_max_dma_type by(auto simp: to_total_def split: if_splits)
    next
      assume "x ∉ 𝒞_vars v"
      hence "∀v'∈𝒞_vars v. mem⇩1 v' = mem⇩1' v'"
        using upd by auto
      hence dma_eq: "dma mem⇩1 v = dma mem⇩1' v"
        by(rule dma_𝒞_vars)
      from Γv assign⇩𝒞(4) have "x ∉ vars_of_type t'" by force
      have "type_wellformed t'"
        using wf Γv by(force simp: tyenv_wellformed_def types_wellformed_def)
      with ‹x ∉ vars_of_type t'› upd have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
        using vars_of_type_eq_type_max_eq by fastforce
      from sec Γv readable have "type_max t' mem⇩1 ≤ dma mem⇩1 v"
        by auto
      with f_eq dma_eq Γv show ?thesis
        by simp
    qed
  qed

  ultimately have ℛ':
    "⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ,𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    apply -
    apply (rule ℛ.intro⇩1, auto simp: assign⇩𝒞)
    done

  have a: "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
  by (auto, metis cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.assign)

  from ℛ' a show ?case
    using ‹c⇩1' = Stop› and ‹mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)›
    by blast
next (* assign⇩2 *)
  case (assign⇩2 x Γ e t 𝒮 P' P mds)
  have upd [simp]: "c⇩1' = Stop" "mds' = mds" "mem⇩1' = mem⇩1 (x := ev⇩A mem⇩1 e)"
    using assign_elim[OF assign⇩2(11)]
    by auto
  from ‹x ∈ dom Γ› ‹tyenv_wellformed mds Γ 𝒮 P›
  have x_nin_𝒞: "x ∉ 𝒞"
    by(auto simp: tyenv_wellformed_def mds_consistent_def)
  hence dma_eq [simp]: "dma mem⇩1' = dma mem⇩1"
    using dma_𝒞 assign⇩2
    by auto
    
  let ?Γ' = "Γ (x ↦ t)"
  have "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds, mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    using assign⇩2
    by (metis cxt_to_stmt.simps(1) eval⇩w_simplep.assign eval⇩wp.unannotated eval⇩wp_eval⇩w_eq)
    
  moreover
  have tyenv_eq': "mem⇩1(x := ev⇩A mem⇩1 e) =⇘Γ(x ↦ t)⇙ mem⇩2(x := ev⇩A mem⇩2 e)"
  unfolding tyenv_eq_def
  proof(clarify)
    fix v
    assume is_Low': "type_max (to_total (Γ(x ↦ t)) v) (mem⇩1(x := ev⇩A mem⇩1 e)) = Low"
    show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
    proof(cases "v = x")
      assume neq: "v ≠ x"
      hence "type_max (to_total Γ v) mem⇩1 = Low"
      proof(cases "v ∈ dom Γ")
        assume "v ∈ dom Γ"
        then obtain t' where [simp]: "Γ v = Some t'" by force
        hence [simp]: "(to_total Γ v) = t'"
          unfolding to_total_def by (auto split: if_splits)
        hence [simp]: "(to_total ?Γ' v) = t'"
          using neq by(auto simp: to_total_def)
        have "type_max t' mem⇩1 = type_max t' mem⇩1'"
          apply(rule 𝒞_eq_type_max_eq)
            using assign⇩2(6) 
            apply(clarsimp simp: tyenv_wellformed_def types_wellformed_def)
            using ‹v ∈ dom Γ› ‹Γ v = Some t'› apply(metis option.sel)
           using x_nin_𝒞 by simp
        from this is_Low' neq neq[THEN not_sym] show "type_max (to_total Γ v) mem⇩1 = Low"
          by auto
      next
        assume "v ∉ dom Γ"
        with is_Low' neq
        have "dma mem⇩1' v = Low"
          by(auto simp: to_total_def  split: if_splits)
        with dma_eq ‹v ∉ dom Γ› show ?thesis
          by(auto simp: to_total_def  split: if_splits)
      qed
      with neq assign⇩2(7) show "(mem⇩1(x := ev⇩A mem⇩1 e)) v = (mem⇩2(x := ev⇩A mem⇩2 e)) v"
        by(auto simp: tyenv_eq_def)
    next
      assume eq[simp]: "v = x"
      with is_Low' ‹x ∈ dom Γ› have t_Low': "type_max t mem⇩1' = Low"
        by(auto simp: to_total_def split: if_splits)
      have wf_t: "type_wellformed t"
        using type_aexpr_type_wellformed assign⇩2(2) assign⇩2(6)
        by(fastforce simp: tyenv_wellformed_def)
      with t_Low' ‹x ∉ 𝒞› have t_Low: "type_max t mem⇩1 = Low"
        using 𝒞_eq_type_max_eq
        by (metis (no_types, lifting) fun_upd_other upd(3))
      show ?thesis
      proof(simp, rule eval_vars_det⇩A, clarify)
        fix y
        assume in_vars: "y ∈ aexp_vars e"
        have "type_max (to_total Γ y) mem⇩1 = Low"
        proof -
          from t_Low in_vars assign⇩2(2) show ?thesis
            apply -
            apply(erule type_aexpr.cases)
            using Sec.exhaust by(auto simp: type_max_def  split: if_splits)
        qed
        thus "mem⇩1 y = mem⇩2 y"
          using assign⇩2 unfolding tyenv_eq_def by blast
      qed
    qed
  qed

  from upd have ty: " ⊢ ?Γ',𝒮,P' {c⇩1'} ?Γ',𝒮,P'"
    by (metis stop_type)
  have wf: "tyenv_wellformed mds Γ 𝒮 P ⟶ tyenv_wellformed mds' ?Γ' 𝒮 P'"
  proof
    assume tyenv_wf: "tyenv_wellformed mds Γ 𝒮 P"
    hence wf: "types_wellformed Γ"
      unfolding tyenv_wellformed_def by blast
    hence  "type_wellformed t"
      using assign⇩2(2) type_aexpr_type_wellformed
      by blast
    with wf have wf': "types_wellformed ?Γ'"
      using types_wellformed_update by metis
    from tyenv_wf have stable': "types_stable ?Γ' 𝒮"
      using types_stable_update
            assign⇩2(3)
      unfolding tyenv_wellformed_def by blast
    have m: "mds_consistent mds Γ 𝒮 P"
      using tyenv_wf unfolding tyenv_wellformed_def by blast
    from assign⇩2(4) assign⇩2(1)
    have "mds_consistent mds' (Γ(x ↦ t)) 𝒮 P'"
      apply(rule mds_consistent_preds_tyenv_update)
      using upd m by simp
    from wf' stable' this show "tyenv_wellformed mds' ?Γ' 𝒮 P'"
      unfolding tyenv_wellformed_def by blast
  qed
  have p: "pred P mem⇩1 ⟶ pred P' mem⇩1'"
    using pred_preds_update assign⇩2 upd by metis
  have p⇩2: "pred P mem⇩2 ⟶ pred P' (mem⇩2(x := ev⇩A mem⇩2 e))"
    using pred_preds_update assign⇩2 upd by metis
  have sec: "tyenv_wellformed mds Γ 𝒮 P ⟹ pred P mem⇩1 ⟹ tyenv_sec mds Γ mem⇩1 ⟹ tyenv_sec mds' ?Γ' mem⇩1'"
  proof(clarify)
    assume wf: "tyenv_wellformed mds Γ 𝒮 P"
    assume pred: "pred P mem⇩1"
    assume sec: "tyenv_sec mds Γ mem⇩1"
    from pred p have pred': "pred P' mem⇩1'" by blast
    fix v t'
    assume Γv: "(Γ(x ↦ t)) v = Some t'"
    assume "v ∉ mds' AsmNoReadOrWrite"
    show "type_max (the ((Γ(x ↦ t)) v)) mem⇩1' ≤ dma mem⇩1' v"
    proof(cases "v = x")
      assume [simp]: "v = x"
      hence [simp]: "(the ((Γ(x ↦ t)) v)) = t" and t_def: "t = t'"
        using Γv by auto
      from ‹v ∉ mds' AsmNoReadOrWrite› upd wf have readable: "v ∉ snd 𝒮"
        by(auto simp: tyenv_wellformed_def mds_consistent_def)
      with assign⇩2(5) have "t ≤:⇩P' (dma_type x)" by fastforce
      with pred' show ?thesis
        using type_max_dma_type subtype_sound
        by fastforce
    next
      assume neq: "v ≠ x"
      hence [simp]: "((Γ(x ↦ t)) v) = Γ v"
        by simp
      with Γv have Γv: "Γ v = Some t'" by simp
      with sec upd ‹v ∉ mds' AsmNoReadOrWrite› have f_leq: "type_max t' mem⇩1 ≤ dma mem⇩1 v"
        by auto
      have 𝒞_eq: "∀x∈𝒞. mem⇩1 x = mem⇩1' x"
        using wf assign⇩2(1) upd by(auto simp: tyenv_wellformed_def mds_consistent_def)
      hence dma_eq: "dma mem⇩1 = dma mem⇩1'"
        by(rule dma_𝒞)
      have f_eq: "type_max t' mem⇩1 = type_max t' mem⇩1'"
        apply(rule 𝒞_eq_type_max_eq)
         using Γv wf apply(force simp: tyenv_wellformed_def types_wellformed_def)
        by(rule 𝒞_eq)     
      from neq Γv f_leq dma_eq f_eq show ?thesis
        by simp
    qed
  qed

  have "⟨Stop, mds, mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧1⇘?Γ',𝒮,P'⇙ ⟨Stop, mds, mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    apply(rule ℛ⇩1.intro)
         apply blast
        using wf assign⇩2 apply fastforce
       apply(rule tyenv_eq')
      using p assign⇩2 apply fastforce
     using p⇩2 assign⇩2 apply fastforce
    using sec assign⇩2
    using upd(2) upd(3) by blast
    
  ultimately have "⟨x ← e, mds, mem⇩2⟩ ↝ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    "⟨Stop, mds', mem⇩1 (x := ev⇩A mem⇩1 e)⟩ ℛ⇧u⇘Γ(x ↦ t),𝒮,P'⇙ ⟨Stop, mds', mem⇩2 (x := ev⇩A mem⇩2 e)⟩"
    using ℛ.intro⇩1
    by auto
  thus ?case
    using ‹mds' = mds› ‹c⇩1' = Stop› ‹mem⇩1' = mem⇩1(x := ev⇩A mem⇩1 e)›
    by blast
next (* if *)
  case (if_type Γ e t P 𝒮 th Γ' 𝒮' P' el Γ'' P'' Γ''' P''')
  let ?P = "if (ev⇩B mem⇩1 e) then P +⇩𝒮 e else P +⇩𝒮 (bexp_neg e)"
  from ‹⟨Stmt.If e th el, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩› have ty: "⊢ Γ,𝒮,?P {c⇩1'} Γ''',𝒮',P'''"
  proof (rule if_elim)
    assume "c⇩1' = th" "mem⇩1' = mem⇩1" "mds' = mds" "ev⇩B mem⇩1 e"
    with if_type(3)
    show ?thesis
      apply simp
      apply(erule sub)
         using if_type apply simp+
      done
  next
    assume "c⇩1' = el" "mem⇩1' = mem⇩1" "mds' = mds" "¬ ev⇩B mem⇩1 e"
    with if_type(5)
    show ?thesis
      apply simp
      apply(erule sub)
         using if_type apply simp+
      done
  qed
  have ev⇩B_eq [simp]: "ev⇩B mem⇩1 e = ev⇩B mem⇩2 e"
    apply(rule ev⇩B_eq')
       apply(rule ‹mem⇩1 =⇘Γ⇙ mem⇩2›)
      apply(rule ‹pred P mem⇩1›)
     apply(rule ‹Γ ⊢⇩b e ∈ t›)
    by(rule ‹ P ⊢ t›)
  have "(⟨c⇩1', mds, mem⇩1⟩, ⟨c⇩1', mds, mem⇩2⟩) ∈ ℛ Γ''' 𝒮' P'''"
    apply (rule intro⇩1)
    apply clarify
    apply (rule ℛ⇩1.intro [where Γ = Γ and Γ' = Γ''' and 𝒮 = 𝒮 and P = ?P])
         apply(rule ty)
        using ‹tyenv_wellformed mds Γ 𝒮 P›
        apply(auto simp: tyenv_wellformed_def mds_consistent_def add_pred_def)[1]
       apply(rule ‹mem⇩1 =⇘Γ⇙ mem⇩2›)       
      using ‹pred P mem⇩1› apply(fastforce simp: pred_def add_pred_def bexp_neg_negates)
     using ‹pred P mem⇩2› apply(fastforce simp: pred_def add_pred_def bexp_neg_negates)
    by(rule ‹tyenv_sec mds Γ mem⇩1›)

  show ?case
  proof -
    from ev⇩B_eq if_type(13) have "(⟨If e th el, mds, mem⇩2⟩ ↝ ⟨c⇩1', mds, mem⇩2⟩)"
      apply (cases "ev⇩B mem⇩1 e")
       apply (subgoal_tac "c⇩1' = th")
        apply clarify
        apply (metis cxt_to_stmt.simps(1) eval⇩w_simplep.if_true eval⇩wp.unannotated eval⇩wp_eval⇩w_eq if_type(8))
       using if_type.prems(6) apply blast
      apply (subgoal_tac "c⇩1' = el")
       apply (metis (opaque_lifting, mono_tags) cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.if_false if_type(8))
      using if_type.prems(6) by blast
    with ‹⟨c⇩1', mds, mem⇩1⟩ ℛ⇧u⇘Γ''',𝒮',P'''⇙ ⟨c⇩1', mds, mem⇩2⟩› show ?thesis  
    by (metis if_elim if_type.prems(6))    
  qed
next (* while *)
  case (while_type Γ e t P 𝒮 c)
  hence [simp]: "c⇩1' = (If e (c ;; While e c) Stop)" and
    [simp]: "mds' = mds" and
    [simp]: "mem⇩1' = mem⇩1"
    by (auto simp: while_elim)

  with while_type have "⟨While e c, mds, mem⇩2⟩ ↝ ⟨c⇩1', mds, mem⇩2⟩"
    by (metis cxt_to_stmt.simps(1) eval⇩w_simplep.while eval⇩wp.unannotated eval⇩wp_eval⇩w_eq)
    
  moreover have ty: " ⊢ Γ,𝒮,P {c⇩1'} Γ,𝒮,P"
    apply simp
    apply(rule if_type)
              apply(rule while_type(1))
             apply(rule while_type(2))
            apply(rule seq_type)
             apply(rule while_type(3))
            apply(rule has_type.while_type)
              apply(rule while_type(1))
             apply(rule while_type(2))
            apply(rule while_type(3))
           apply(rule stop_type)
          apply simp+
      apply(rule add_pred_entailment)
     apply simp
    apply(blast intro!: add_pred_subset tyenv_wellformed_subset)
    done
  moreover
  have "⟨c⇩1', mds, mem⇩1⟩ ℛ⇧1⇘Γ,𝒮,P⇙ ⟨c⇩1', mds, mem⇩2⟩"
    apply (rule ℛ⇩1.intro [where Γ = Γ])
         apply(rule ty)
        using while_type apply simp+
    done
  hence "⟨c⇩1', mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩1', mds, mem⇩2⟩"
    using ℛ.intro⇩1 by auto
  ultimately show ?case
    by fastforce
next
  case (sub Γ⇩1 𝒮 P⇩1 c Γ⇩1' 𝒮' P⇩1' Γ⇩2 P⇩2 Γ⇩2' P⇩2' mds c⇩1')
  have imp: "tyenv_wellformed mds Γ⇩2 𝒮 P⇩2 ∧ pred P⇩2 mem⇩1 ∧ pred P⇩2 mem⇩2 ∧ tyenv_sec mds Γ⇩2 mem⇩1 ⟹ 
             tyenv_wellformed mds Γ⇩1 𝒮 P⇩1 ∧ pred P⇩1 mem⇩1 ∧ pred P⇩1 mem⇩2 ∧ tyenv_sec mds Γ⇩1 mem⇩1"
    apply(rule conjI)
     using sub(5) sub(4) tyenv_wellformed_sub unfolding pred_def
     apply blast
    apply(rule conjI)
     using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
    apply(rule conjI)
     using local.pred_def pred_entailment_def sub.hyps(7) apply auto[1]
    using sub(3) context_equiv_tyenv_sec unfolding pred_def by blast

  have tyenv_eq: "mem⇩1 =⇘Γ⇩1⇙ mem⇩2"
    using context_equiv_tyenv_eq sub by blast
    
  from imp tyenv_eq obtain c⇩2' mem⇩2' where c⇩2'_props: "⟨c, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩"
    "⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ⇩1',𝒮',P⇩1'⇙ ⟨c⇩2', mds', mem⇩2'⟩"
    using sub by blast 
  with R_equiv_entailment ‹P⇩1' ⊢ P⇩2'› show ?case
    using sub.hyps(6) sub.hyps(5) by blast
next case (await_type Γ e t P 𝒮 c Γ' 𝒮' P')
  from await_type.prems have "ev⇩B mem⇩1 e" "no_await c" "is_final c⇩1'" and step: "⟨c, mds, mem⇩1⟩ ↝⇧+ ⟨c⇩1', mds', mem⇩1'⟩"
    using await_elim by simp+
  from await_type.prems ‹Γ ⊢⇩b e ∈ t› ‹P ⊢ t› have "pred P +⇩𝒮 e mem⇩1" "pred P +⇩𝒮 e mem⇩2" "ev⇩B mem⇩2 e"
    using pred_plus_impl ‹ev⇩B mem⇩1 e› ‹pred P mem⇩1› ev⇩B_eq'
    by blast+
  from await_type.prems ‹Γ ⊢⇩b e ∈ t› ‹P ⊢ t› have wellformed: "tyenv_wellformed mds Γ 𝒮 P +⇩𝒮 e"
    apply (unfold add_pred_def)[1]
      apply (case_tac "pred_stable 𝒮 e", clarsimp)
        apply (unfold tyenv_wellformed_def, clarsimp)[1]
        apply (unfold mds_consistent_def, clarsimp)[1]
      by clarsimp
  from step ‹is_final c⇩1'› ‹no_await c› ‹tyenv_wellformed mds Γ 𝒮 P +⇩𝒮 e› await_type.prems ‹pred P +⇩𝒮 e mem⇩1› ‹pred P +⇩𝒮 e mem⇩2›
    obtain c⇩2' mem⇩2' where step: "⟨c, mds, mem⇩2⟩ ↝⇧+ ⟨c⇩2', mds', mem⇩2'⟩" and 
      rel: "⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩" "is_final c⇩2'"  
    using ℛ_typed_step_plus await_type.hyps(3) is_final_ℛ⇩u_is_final by meson
  from wellformed ‹is_final c⇩2'› ‹ev⇩B mem⇩2 e› ‹no_await c› ‹Γ ⊢⇩b e ∈ t› ‹P ⊢ t› ‹pred P +⇩𝒮 e mem⇩2› step rel show ?case 
    using eval⇩w.intros(4) by blast
qed

(* We can now show that ℛ⇩1 and ℛ⇩3 are weak bisimulations of ℛ,: *)
lemma ℛ⇩1_weak_bisim:
  "weak_bisim (ℛ⇩1 Γ' 𝒮' P') (ℛ Γ' 𝒮' P')"
  unfolding weak_bisim_def
  apply clarsimp
  apply(erule ℛ⇩1_elim)
  apply(blast intro: ℛ_typed_step)
  done


lemma ℛ_to_ℛ⇩3: "⟦ ⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2, mds, mem⇩2⟩ ; ⊢ Γ,𝒮,P { c } Γ',𝒮',P' ⟧ ⟹
  ⟨c⇩1 ;; c, mds, mem⇩1⟩ ℛ⇧3⇘Γ',𝒮',P'⇙ ⟨c⇩2 ;; c, mds, mem⇩2⟩"
  apply (erule ℛ_elim)
  by auto


lemma ℛ⇩3_weak_bisim:
  "weak_bisim (ℛ⇩3 Γ' 𝒮' P') (ℛ Γ' 𝒮' P')"
proof -
  {
    fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 c⇩1' mds' mem⇩1'
    assume case3: "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ ℛ⇩3 Γ' 𝒮' P'"
    assume eval: "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩"
    have "∃ c⇩2' mem⇩2'. ⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧ ⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩"
      using case3 eval
      apply simp
      
    proof (induct arbitrary: c⇩1' rule: ℛ⇩3_aux.induct)
      case (intro⇩1 c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P')
      hence [simp]: "c⇩2 = c⇩1"
        by (metis (lifting) ℛ⇩1_elim)
      thus ?case
      proof (cases "c⇩1 = Stop")
        assume [simp]: "c⇩1 = Stop"
        from intro⇩1(1) show ?thesis
          apply (rule ℛ⇩1_elim)
          apply simp
          apply (rule_tac x = c in exI)
          apply (rule_tac x = mem⇩2 in exI)
          apply (rule conjI)
           apply (metis ‹c⇩1 = Stop› cxt_to_stmt.simps(1) eval⇩w_simplep.seq_stop eval⇩wp.unannotated eval⇩wp_eval⇩w_eq intro⇩1.prems seq_stop_elim)
          apply (rule ℛ.intro⇩1, clarify)
          apply (subgoal_tac "c⇩1' = c")
           apply simp
           apply (rule ℛ⇩1.intro)
                apply(rule intro⇩1(2))
               apply (metis (no_types, lifting) ‹c⇩1 = Stop› intro⇩1.prems seq_stop_elim stop_cxt tyenv_wellformed_sub)
              using ‹c⇩1 = Stop› intro⇩1.prems seq_stop_elim stop_cxt context_equiv_tyenv_eq
              apply metis

             using ‹c⇩1 = Stop› intro⇩1.prems pred_entailment_def seq_stop_elim stop_cxt apply blast
            using pred_entailment_def stop_cxt apply blast
           
           apply (metis (no_types, lifting) ‹c⇩1 = Stop› context_equiv_def intro⇩1.prems less_eq_Sec_def seq_stop_elim stop_cxt subtype_sound type_equiv_def)
          using intro⇩1.prems seq_stop_elim by auto
      next
        assume "c⇩1 ≠ Stop"
        from intro⇩1
        obtain c⇩1'' where "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩ ∧ c⇩1' = (c⇩1'' ;; c)"
          by (metis ‹c⇩1 ≠ Stop› intro⇩1.prems seq_elim)
        with intro⇩1
        obtain c⇩2'' mem⇩2' where "⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2'', mds', mem⇩2'⟩" "⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2'', mds', mem⇩2'⟩"
          using ℛ⇩1_weak_bisim and weak_bisim_def
          by blast
        thus ?thesis
          using intro⇩1(2) ℛ_to_ℛ⇩3
          apply (rule_tac x = "c⇩2'' ;; c" in exI)
          apply (rule_tac x = mem⇩2' in exI)
          apply (rule conjI)
           apply (metis eval⇩w.seq)
          apply auto
          apply (rule ℛ.intro⇩3)
          
          by (simp add: ℛ_to_ℛ⇩3 ‹⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩ ∧ c⇩1' = c⇩1'' ;; c›)
      qed
    next
      case (intro⇩3 c⇩1 mds mem⇩1 Γ 𝒮 P c⇩2 mem⇩2 c Γ' 𝒮' P')
      thus ?case
        apply (cases "c⇩1 = Stop")
         apply blast
      proof -
        assume "c⇩1 ≠ Stop"
        then obtain c⇩1'' where "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1'', mds', mem⇩1'⟩" "c⇩1' = (c⇩1'' ;; c)"
          by (metis intro⇩3.prems seq_elim)
        then obtain c⇩2'' mem⇩2' where "⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2'', mds', mem⇩2'⟩" "⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2'', mds', mem⇩2'⟩"
          using intro⇩3(2) by metis
        thus ?thesis
          apply (rule_tac x = "c⇩2'' ;; c" in exI)
          apply (rule_tac x = mem⇩2' in exI)
          apply (rule conjI)
           apply (metis eval⇩w.seq)
          apply (erule ℛ_elim)
            apply simp_all
            apply (metis ℛ.intro⇩3 ℛ_to_ℛ⇩3 ‹⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2'', mds', mem⇩2'⟩› ‹c⇩1' = c⇩1'' ;; c› intro⇩3(3))
          apply (metis (lifting) ℛ.intro⇩3 ℛ_to_ℛ⇩3 ‹⟨c⇩1'', mds', mem⇩1'⟩ ℛ⇧u⇘Γ,𝒮,P⇙ ⟨c⇩2'', mds', mem⇩2'⟩› ‹c⇩1' = c⇩1'' ;; c› intro⇩3(3))
          done
      qed
    qed
  }
  thus ?thesis
    unfolding weak_bisim_def
    by auto
qed

(* Hence ℛ is a bisimulation: *)
lemma ℛ_bisim: "strong_low_bisim_mm (ℛ Γ' 𝒮' P')"
  unfolding strong_low_bisim_mm_def
proof (auto)
  from ℛ_sym show "sym (ℛ Γ' 𝒮' P')" .
next
  from ℛ_closed_glob_consistent show "closed_glob_consistent (ℛ Γ' 𝒮' P')" .
next
  fix c⇩1 mds mem⇩1 c⇩2 mem⇩2
  assume "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
  thus "mem⇩1 =⇘mds⇙⇧l mem⇩2"
    apply (rule ℛ_elim)
    by (auto simp: ℛ⇩1_mem_eq ℛ⇩3_mem_eq)
next
  fix c⇩1 mds mem⇩1 c⇩2 mem⇩2 c⇩1' mds' mem⇩1'
  assume eval: "⟨c⇩1, mds, mem⇩1⟩ ↝ ⟨c⇩1', mds', mem⇩1'⟩"
  assume R: "⟨c⇩1, mds, mem⇩1⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2, mds, mem⇩2⟩"
  from R show "∃ c⇩2' mem⇩2'. ⟨c⇩2, mds, mem⇩2⟩ ↝ ⟨c⇩2', mds', mem⇩2'⟩ ∧
                            ⟨c⇩1', mds', mem⇩1'⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c⇩2', mds', mem⇩2'⟩"
    apply (rule ℛ_elim)
      apply (insert ℛ⇩1_weak_bisim ℛ⇩3_weak_bisim eval weak_bisim_def)
      apply auto
    done
qed

lemma Typed_in_ℛ:
  assumes typeable: "⊢ Γ,𝒮,P { c } Γ',𝒮',P'"
  assumes wf: "tyenv_wellformed mds Γ 𝒮 P"
  assumes mem_eq: "∀ x. type_max (to_total Γ x) mem⇩1 = Low ⟶ mem⇩1 x = mem⇩2 x"
  assumes pred⇩1: "pred P mem⇩1"
  assumes pred⇩2: "pred P mem⇩2"
  assumes tyenv_sec: "tyenv_sec mds Γ mem⇩1"
  shows "⟨c, mds, mem⇩1⟩ ℛ⇧u⇘Γ',𝒮',P'⇙ ⟨c, mds, mem⇩2⟩"
  apply (rule ℛ.intro⇩1 [of Γ'])
  apply clarify
  apply (rule ℛ⇩1.intro [of Γ])
       apply(rule typeable)
      apply(rule wf)
     using mem_eq apply(fastforce simp: tyenv_eq_def)
    using assms by simp+

(* We then prove the main soundness theorem using the fact that typeable
    configurations can be related using ℛ⇩1 *)
theorem type_soundness:
  assumes well_typed: "⊢ Γ,𝒮,P { c } Γ',𝒮',P'"
  assumes wf: "tyenv_wellformed mds Γ 𝒮 P"
  assumes mem_eq: "∀ x. type_max (to_total Γ x) mem⇩1 = Low ⟶ mem⇩1 x = mem⇩2 x"
  assumes pred⇩1: "pred P mem⇩1"
  assumes pred⇩2: "pred P mem⇩2"
  assumes tyenv_sec: "tyenv_sec mds Γ mem⇩1"
  shows "⟨c, mds, mem⇩1⟩ ≈ ⟨c, mds, mem⇩2⟩"
  using ℛ_bisim Typed_in_ℛ
  by (metis assms mem_eq mm_equiv.simps well_typed)

definition
  Γ_of_mds :: "'Var Mds ⇒ ('Var,'BExp) TyEnv"
where
  "Γ_of_mds mds ≡ (λx. if x ∉ 𝒞 ∧ x ∈ mds AsmNoWrite ∪ mds AsmNoReadOrWrite then
                         if x ∈ mds AsmNoReadOrWrite then 
                           Some ({pred_False}) 
                         else
                           Some (dma_type x) 
                       else None)"

definition
  𝒮_of_mds :: "'Var Mds ⇒ 'Var Stable"
where
  "𝒮_of_mds mds ≡ (mds AsmNoWrite, mds AsmNoReadOrWrite)"

definition
  mds_yields_stable_types :: "'Var Mds ⇒ bool"
where
  "mds_yields_stable_types mds ≡ ∀x. x ∈ mds AsmNoWrite ∪ mds AsmNoReadOrWrite ⟶
                                     (∀v∈𝒞_vars x. v ∈ mds AsmNoWrite ∪ mds AsmNoReadOrWrite)"
  
(* The typing relation for lists of commands ("thread pools"). *)
inductive 
  type_global :: "(('Var, 'AExp, 'BExp) Stmt × 'Var Mds) list ⇒ bool"
  ("⊢ _" [120] 1000)
where
  "⟦ list_all (λ (c,m). (∃ Γ' 𝒮' P'. ⊢ (Γ_of_mds m),(𝒮_of_mds m),{} { c } Γ',𝒮',P') ∧ mds_yields_stable_types m) cs ;
       ∀ mem. sound_mode_use (cs, mem)
    ⟧ ⟹
    type_global cs"

                                     
inductive_cases type_global_elim: "⊢ cs"

lemma of_mds_tyenv_wellformed: "mds_yields_stable_types m ⟹ tyenv_wellformed m (Γ_of_mds m) (𝒮_of_mds m) {}"
  apply(auto simp: tyenv_wellformed_def Γ_of_mds_def 𝒮_of_mds_def mds_consistent_def stable_def
                   types_wellformed_def types_stable_def  mds_yields_stable_types_def 
                   type_wellformed_def dma_𝒞_vars 𝒞_def bexp_vars_pred_False 𝒞_vars_correct
             split: if_splits)
  done

lemma Γ_of_mds_tyenv_sec:
  "tyenv_sec m (Γ_of_mds m) mem⇩1"
  apply(auto simp: Γ_of_mds_def)
  done

lemma type_max_pred_False [simp]:
  "type_max {pred_False} mem = High"
  apply(simp add: type_max_def pred_False_is_False)
  done
  
lemma typed_secure:
  "⟦ ⊢ (Γ_of_mds m),(𝒮_of_mds m),{} { c } Γ',𝒮',P'; mds_yields_stable_types m ⟧ ⟹ com_sifum_secure (c,m)"
  apply (clarsimp simp: com_sifum_secure_def low_indistinguishable_def)
  apply (erule type_soundness)
      apply(erule of_mds_tyenv_wellformed)
     apply(auto simp: to_total_def split: if_split simp: Γ_of_mds_def low_mds_eq_def)[1]
    apply(fastforce simp: pred_def type_max_def)
   apply(fastforce simp: pred_def)
  by(rule Γ_of_mds_tyenv_sec)

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"
  shows "prog_sifum_secure_cont cs"
  using typeable
  apply (rule type_global_elim)
  apply (subgoal_tac "∀ c ∈ set cs. com_sifum_secure c")
   apply(rule sifum_compositionality_cont)
    using list_all_set apply fastforce
   apply fastforce
  apply(drule list_all_iff[THEN iffD1])
  apply clarsimp
  apply(rename_tac c m)
  apply(drule_tac x="(c,m)" in bspec)
   apply assumption
  apply clarsimp
  using typed_secure by blast

end
end