Theory Example_Swap_Add

(*
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)
*)
theory Example_Swap_Add
imports 
  "../TypeSystem" 
  TypeSystemTactics
begin

text ‹
  Use upper-case variable names to avoid clashing with one-letter free variables
›
datatype addr = X | control_X | Y | control_Y | Z | control_Z
type_synonym val = nat
type_synonym mem = "addr ⇒ val"

datatype aexp = Load "addr" | Const "val" | Add "addr" "addr" 

fun 
  ev⇩A :: "mem ⇒ aexp ⇒ val"
where
  "ev⇩A mem (Load x) = mem x" |
  "ev⇩A mem (Const c) = c" |
  "ev⇩A mem (Add x y) = mem x + mem y"
 
fun
  aexp_vars :: "aexp ⇒ addr set"
where
  "aexp_vars (Load x) = {x}" |
  "aexp_vars (Const c) = {}" |
  "aexp_vars (Add x y) = {x,y}"
  
datatype bexp = Same "addr" "aexp" |
                Eq "addr" "val" |
                Not bexp |
                Imp bexp bexp |
                And bexp bexp |
                Or bexp bexp | TT | FF

fun
  ev⇩B :: "mem ⇒ bexp ⇒ bool"
where
  "ev⇩B mem (Same x e) = ((mem x) = (ev⇩A mem e))" | 
  "ev⇩B mem (Eq x c) = ((mem x) = c)" | 
  "ev⇩B mem (Not e) = (¬ ev⇩B mem e)" |
  "ev⇩B mem (Imp e f) = (ev⇩B mem e ⟶ ev⇩B mem f)" |
  "ev⇩B mem (And e f) = (ev⇩B mem e ∧ ev⇩B mem f)" |
  "ev⇩B mem (Or e f) = (ev⇩B mem e ∨ ev⇩B mem f)" |
  "ev⇩B mem TT = True" |
  "ev⇩B mem FF = False"


fun
  bexp_vars :: "bexp ⇒ addr set"
where
  "bexp_vars (Eq x c) = {x}" |
  "bexp_vars (Same x e) = {x} ∪ aexp_vars e" |
  "bexp_vars (Not e) = bexp_vars e" |
  "bexp_vars (Imp e f) = bexp_vars e ∪ bexp_vars f" |
  "bexp_vars (And e f) = bexp_vars e ∪ bexp_vars f" |
  "bexp_vars (Or e f) = bexp_vars e ∪ bexp_vars f" |
  "bexp_vars _ = {}"

  
fun
  bexp_neg :: "bexp ⇒ bexp"
where
  "bexp_neg e = (Not e)"
  
fun
   bexp_assign :: "addr ⇒ aexp ⇒ bexp"
where
  "bexp_assign x e  = (Same x e)"

definition
  dma_control_var :: "val ⇒ Sec"
where
  "dma_control_var v ≡ if v = 0 then Low else High"

fun
  control_var_of :: "addr ⇒ addr"
where
  "control_var_of X = control_X" |
  "control_var_of Y = control_Y" |
  "control_var_of Z = control_Z"
  
definition
  dma :: "mem ⇒ addr ⇒ Sec"
where
  "dma m x ≡ if x ∈ {X,Y,Z} then dma_control_var (m (control_var_of x)) else Low"

definition
  𝒞_vars :: "addr ⇒ addr set"
where
  "𝒞_vars x ≡ if x ∈ {X,Y,Z} then {control_var_of x} else {}"

definition
  mds⇩s :: "Mode ⇒ 'Var set"
where 
  "mds⇩s ≡ λ_. {}"

locale sifum_example =
  sifum_lang_no_dma ev⇩A ev⇩B aexp_vars bexp_vars +
  assumes eval_det: "(lc, lc') ∈ sifum_lang_no_dma.eval⇩w ev⇩A ev⇩B ⟹ (lc, lc'') ∈ sifum_lang_no_dma.eval⇩w ev⇩A ev⇩B ⟹ lc' = lc''"

definition
  𝒞 :: "addr set"
where
  "𝒞 ≡ ⋃x. 𝒞_vars x"

fun
  dma_type :: "addr ⇒ bexp set"
where
  "dma_type X = {Eq control_X 0}" |
  "dma_type Z = {Eq control_Z 0}" |
  "dma_type Y = {Eq control_Y 0}" |
  "dma_type _ = {}"

sublocale sifum_example ⊆ sifum_types_assign ev⇩A ev⇩B aexp_vars bexp_vars dma 𝒞_vars 𝒞 bexp_neg dma_type FF bexp_assign
  apply(unfold_locales)
              apply(blast intro: eval_det)
             apply(rule Var_finite)
            apply(auto simp: 𝒞_vars_def dma_def 𝒞_def split: if_splits)[3]
         apply(rename_tac mem e, case_tac e, auto)[1]
        apply(case_tac x, auto simp: dma_def dma_control_var_def)[1]
       apply(case_tac x, auto simp: 𝒞_vars_def)[1]
      apply(simp+)[2]
    apply(case_tac e, auto)[1]
   apply(case_tac e, simp)
  apply(auto simp: 𝒞_def)
  done

context sifum_example begin
  
lemma if_type'': 
  "⟦type_bexpr Γ e t; pred_entailment P t;
    has_type  Γ 𝒮 (add_pred P 𝒮 e) c⇩1 Γ' 𝒮' P';
    has_type Γ 𝒮 (add_pred P 𝒮 (bexp_neg e)) c⇩2 Γ' 𝒮' P'';
    pred_entailment P' {e}; pred_entailment P'' {bexp_neg e};  
    P''' = restrict_preds_to_vars (((Imp e) ` (P' - {e})) ∪ ((Imp (bexp_neg e)) ` (P'' - {bexp_neg e}))) {v. stable 𝒮' v}⟧
⟹ has_type Γ 𝒮 P (Stmt.If e c⇩1 c⇩2) Γ' 𝒮' P'''"
  apply(erule (3) if_type,simp+)
     apply(auto simp: pred_entailment_def pred_def image_def restrict_preds_to_vars_def)[1]
    apply(auto simp: pred_entailment_def pred_def image_def restrict_preds_to_vars_def)[1]
   apply(clarsimp simp: tyenv_wellformed_def mds_consistent_def stable_def image_def restrict_preds_to_vars_def)
   apply fastforce
  apply(clarsimp simp: tyenv_wellformed_def mds_consistent_def stable_def image_def restrict_preds_to_vars_def)
  apply fastforce
  done
  

definition
  swap_vars :: "(addr, aexp, bexp) Stmt"
where
  "swap_vars ≡ 
     ModeDecl Skip (Acq control_X AsmNoWrite) ;; 
     ModeDecl Skip (Acq control_Y AsmNoWrite) ;;
     ModeDecl Skip (Acq control_Z AsmNoWrite) ;;
     ModeDecl Skip (Acq X AsmNoReadOrWrite) ;; 
     ModeDecl Skip (Acq Y AsmNoReadOrWrite) ;;
     ModeDecl Skip (Acq Z AsmNoReadOrWrite) ;;
     Assign Z (Load X) ;;
     Assign X (Load Y) ;;
     Assign Y (Load Z) ;;
     Assign control_Z (Load control_X) ;;
     Assign control_X (Load control_Y) ;;
     Assign control_Y (Load control_Z) ;;
     ModeDecl Skip (Rel X AsmNoReadOrWrite) ;;
     ModeDecl Skip (Rel Y AsmNoReadOrWrite) ;;
     ModeDecl Skip (Rel Z AsmNoReadOrWrite) ;;
     ModeDecl Skip (Rel control_X AsmNoWrite) ;; 
     ModeDecl Skip (Rel control_Y AsmNoWrite) ;;
     ModeDecl Skip (Rel control_Z AsmNoWrite) ;;
     Skip"

lemma 𝒞_simp[simp]:
  "𝒞 = {control_X, control_Y, control_Z}"
proof -
  have "𝒞 = control_var_of ` {x. x = X ∨ x = Y ∨ x = Z}"
    by (simp add: 𝒞_def 𝒞_vars_def UNION_singleton_eq_range)
  also have "{x. x = X ∨ x = Y ∨ x = Z} = {X, Y, Z}"
    by auto
  finally show ?thesis
    by simp
qed

lemma type_aexpr_Load:
  "v ∉ dom Γ ⟹ type_aexpr Γ (Load v) (dma_type v)"
  apply(insert type_aexpr[of Γ "Load v", simplified])
  apply(simp add: to_total_def)
  done

lemma type_aexpr_Load':
  "v ∈ dom Γ ⟹ t = (the (Γ v)) ⟹ type_aexpr Γ (Load v) t"
  apply(insert type_aexpr[of Γ "Load v", simplified])
  apply(simp add: to_total_def)
  done

lemma type_aexpr_Add:
  "x ∉ dom Γ ⟹ y ∉ dom Γ ⟹ 
   type_aexpr Γ (Add x y) (⋃ {dma_type x, dma_type y})"
  apply(insert type_aexpr[of Γ "Add x y", simplified])
  apply(simp add: to_total_def)
  done

lemma type_aexpr_Add':
  "x ∉ dom Γ ⟹ y ∈ dom Γ ⟹ t = (the (Γ y)) ⟹
   type_aexpr Γ (Add x y) (⋃ {dma_type x, t})"
  apply(insert type_aexpr[of Γ "Add x y", simplified])
  apply(simp add: to_total_def)
  done

lemma type_aexpr_Add'':
  "x ∈ dom Γ ⟹ y ∉ dom Γ ⟹ t = (the (Γ x)) ⟹
   type_aexpr Γ (Add x y) (⋃ {t, dma_type y})"
  apply(insert type_aexpr[of Γ "Add x y", simplified])
  apply(simp add: to_total_def)
  done

lemma type_aexpr_Add''':
  "x ∈ dom Γ ⟹ y ∈ dom Γ ⟹ t = (the (Γ x)) ⟹ t' = (the (Γ y)) ⟹
   type_aexpr Γ (Add x y) (⋃ {t, t'})"
  apply(insert type_aexpr[of Γ "Add x y", simplified])
  apply(simp add: to_total_def)
  done


lemma type_aexpr_Const[simp]:
  "type_aexpr Γ (Const c) {}"
  apply(insert type_aexpr[of Γ "Const c", simplified],simp)
  done


declare restrict_preds_to_vars_def [simp]
declare add_pred_def [simp]
declare stable_def [simp]
declare to_total_def [simp]
declare 𝒞_vars_def [simp]
declare anno_type_stable_def [simp]
declare anno_type_sec_def [simp]
declare assign_post_def [simp]


lemma control_vars_cases:
  "control_X ∈ 𝒞_vars v ⟹ v = X"
  "control_Y ∈ 𝒞_vars v ⟹ v = Y"
  "control_Z ∈ 𝒞_vars v ⟹ v = Z"
  by(case_tac v, auto)+

lemma mem_is_different[simp, intro]:
  "mem x = A ⟹ mem y ≠ A ⟹ ¬ ev⇩B  mem (Same y (Load x))"
  "mem x = A ⟹ mem y ≠ A ⟹ ¬ ev⇩B  mem (Same x (Load y))"
  by fastforce+

lemma restrict_preds_to_vars_empty[simp]:
  "restrict_preds_to_vars {} V = {}"
  apply(simp add: restrict_preds_to_vars_def)
  done

lemma restrict_preds_to_vars_idemp[simp]:
  "restrict_preds_to_vars (restrict_preds_to_vars P V) V = 
   restrict_preds_to_vars P V"
  apply(simp add: restrict_preds_to_vars_def)
  done

lemma restrict_preds_to_vars_insert1[simp]:
  "(∀x∈bexp_vars a. x ∈ V) ⟹ restrict_preds_to_vars (insert a P) V = (insert a (restrict_preds_to_vars P V))"
  apply(simp add: restrict_preds_to_vars_def)
  apply fastforce
  done

lemma restrict_preds_to_vars_insert2[simp]:
  "(∃x∈bexp_vars a. x ∉ V) ⟹ restrict_preds_to_vars (insert a P) V = ((restrict_preds_to_vars P V))"
  apply(simp add: restrict_preds_to_vars_def)
  apply fastforce
  done
  
declare restrict_preds_to_vars_def[simp del]

lemma [simp]: "pred_entailment P {}" by(simp add: pred_entailment_def pred_def)
lemma [simp]: "e ∈ P ⟹ pred_entailment P {e}" by(blast intro: subset_entailment)
lemma [simp]: "FF ∈ P ⟹ pred_entailment P Q" by(auto simp: pred_entailment_def pred_def)

lemma swap_vars_typed:
  "Γ = (λ_. None) ⟹ 𝒮 = ({},{}) ⟹ P = {} ⟹ 
  ∃Γ' 𝒮' P'. has_type Γ 𝒮 P swap_vars Γ' 𝒮' P'"
  apply(intro exI)
  apply(simp add: swap_vars_def)
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply(simp+)[4]
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply(simp+)[4]
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply(simp+)[4]
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
        apply clarsimp
       apply(rule skip_type)
      apply(simp+)[4]
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply(simp+)[4]
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply(simp+)[4]

  apply(rule seq_type)
   apply(rule assign⇩2[OF _ _ _ HOL.refl])
      apply simp
     apply(rule type_aexpr_Load')
     apply(simp+)[4]

  apply(rule seq_type)
   apply(rule assign⇩2[OF _ _ _ HOL.refl])
      apply simp
     apply(rule type_aexpr_Load')
     apply(simp+)[4]

  apply(rule seq_type)
   apply(rule assign⇩2[OF _ _ _ HOL.refl])
      apply simp
     apply(rule type_aexpr_Load')
     apply(simp+)[4]

  apply(rule seq_type)
   apply(rule assign⇩𝒞[OF _ _ _ _ HOL.refl])
      apply simp
     apply(rule type_aexpr_Load)
     apply (simp+)[4]
  apply simp
 
  apply(rule seq_type)
   apply(rule conc'[where x="Z" and t="dma_type Z", OF _ HOL.refl])
       apply(rule conc'[where x=Y and t="dma_type Z", OF _ HOL.refl])
           apply(rule assign⇩𝒞[OF _ _ _ _ HOL.refl])
                apply simp
               apply(rule type_aexpr_Load)
               apply simp+
         apply(clarsimp simp: type_equiv_def subtype_def pred_entailment_def pred_def)
        apply(fastforce simp: type_wellformed_def)
       apply simp
      apply simp
     apply(clarsimp simp: type_equiv_def subtype_def pred_entailment_def pred_def)
    apply(fastforce simp: type_wellformed_def)
   apply simp

  apply simp
  apply(rule seq_type)
   apply(rule conc'[where x=X and t="dma_type X" , OF _ HOL.refl])
       apply(rule assign⇩𝒞[OF _ _ _ _ HOL.refl])
           apply simp
          apply(rule type_aexpr_Load)
          apply simp+
     apply(clarsimp simp: type_equiv_def subtype_def pred_entailment_def pred_def)
    apply(clarsimp simp: type_wellformed_def)
   apply simp
  
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply(rule skip_type)
      apply simp
     apply(fastforce simp: add_anno_def subtype_def pred_entailment_def pred_def)
    apply simp
   apply simp

  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply simp
     apply(fastforce simp: add_anno_def subtype_def pred_entailment_def pred_def)
    apply simp
   apply simp
 
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply simp
     apply(fastforce simp: add_anno_def subtype_def pred_entailment_def pred_def)
    apply simp
   apply simp

  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply simp
     apply(fastforce simp: add_anno_def subtype_def)
     apply (simp add: add_anno_def) 
    apply simp 

  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply simp
     apply(fastforce simp: add_anno_def subtype_def)
     apply (simp add: add_anno_def) 
    apply simp 

  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply clarsimp
       apply(rule skip_type)
      apply simp
     apply(fastforce simp: add_anno_def subtype_def)
     apply (simp add: add_anno_def) 
    apply simp 

  apply(rule skip_type)
  done

lemma swap_vars_sifum_secure:
  "com_sifum_secure (swap_vars,(λ_. {}))"
  apply(insert swap_vars_typed[OF HOL.refl HOL.refl HOL.refl])
  apply clarify
  apply(rule typed_secure)
   apply(fastforce simp: Γ_of_mds_def 𝒮_of_mds_def)
  apply(auto simp: mds_yields_stable_types_def)
  done

definition
  add_vars :: "(addr, aexp, bexp) Stmt"
where
  "add_vars ≡ 
     ModeDecl Skip (Acq control_X AsmNoWrite) ;; 
     ModeDecl Skip (Acq control_Y AsmNoWrite) ;;
     ModeDecl Skip (Acq control_Z AsmNoWrite) ;;
     ModeDecl Skip (Acq Z AsmNoReadOrWrite) ;;
     Assign Z (Add X Y) ;;
     If (Eq control_X 0)
        (If (Eq control_Y 0)
            (Assign control_Z (Const 0))
            (Assign control_Z (Const 1)))
        (Assign control_Z (Const 1)) ;;
     ModeDecl Skip (Rel Z AsmNoReadOrWrite) ;;
     ModeDecl Skip (Rel control_X AsmNoWrite) ;; 
     ModeDecl Skip (Rel control_Y AsmNoWrite) ;;
     ModeDecl Skip (Rel control_Z AsmNoWrite) ;;
     Skip"

lemma pred_entailment_singleton_by_case_distinction:
  "Imp e f ∈ P ⟹ Imp (bexp.Not e) f ∈ P ⟹ pred_entailment P {f}"
  apply(clarsimp simp: pred_entailment_def pred_def)
  apply(case_tac "ev⇩B mem e")
   apply fastforce+
  done


lemma restrict_preds_to_vars_nest [simp]:
  "restrict_preds_to_vars (restrict_preds_to_vars P V) V' = restrict_preds_to_vars P (V ∩ V')"
  apply(auto simp: restrict_preds_to_vars_def)
  done

lemma restrict_preds_to_vars_imp_image1 [simp]:
  "¬ bexp_vars e ⊆ V ⟹ restrict_preds_to_vars (Imp e ` P) V = {}"
  apply(auto simp: restrict_preds_to_vars_def)
  done

lemma restrict_preds_to_vars_imp_image2 [simp]:
  "bexp_vars e ⊆ V ⟹ restrict_preds_to_vars (Imp e ` P) V = ((Imp e) ` (restrict_preds_to_vars P V))"
  apply(auto simp: restrict_preds_to_vars_def)
  done

  
lemma insert_minus1 [simp]:
  "x = y ⟹ (insert x A) - {y} = (A - {y})"
  by auto
  
lemma insert_minus2 [simp]:
  "x ≠ y ⟹ (insert x A) - {y} = insert x (A - {y})"
  by auto
  
lemma add_vars_typed:
  "Γ = (λ_. None) ⟹ 𝒮 = ({},{}) ⟹ P = {} ⟹ 
  ∃Γ' 𝒮' P'. has_type Γ 𝒮 P add_vars Γ' 𝒮' P'"
  apply(intro exI)
  apply(simp add: add_vars_def)
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply(rule skip_type)
      apply simp+
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply(rule skip_type)
      apply simp+
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply(rule skip_type)
      apply simp+
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply(rule skip_type)
      apply simp+

  apply(rule seq_type)
   apply(rule assign⇩2)
       apply simp
      apply (rule type_aexpr_Add type_aexpr_Add' type_aexpr_Add'' type_aexpr_Add'''; simp)
     apply(simp)
    apply(simp)
   apply simp
 
  apply(clarsimp)
  apply(rule seq_type)
   apply(rule if_type''[OF _ _ _ _ _ _ HOL.refl])
        apply(rule type_bexprI)
        apply(clarsimp)
        apply(rule HOL.refl)
       apply simp
      apply(rule if_type''[OF _ _ _ _ _ _ HOL.refl])
           apply(rule type_bexprI)
           apply(clarsimp simp: to_total_def)
           apply(rule HOL.refl)
          apply simp
         apply(rule assign⇩𝒞)
              apply simp
             apply(rule type_aexpr_Const)
            apply simp 
           apply (clarsimp, fast)
          apply(simp)
         apply simp
        apply(rule assign⇩𝒞)
             apply simp
            apply(rule type_aexpr_Const)
           apply simp 
          apply auto[1]
         apply(simp)
        apply clarsimp
       apply(clarsimp simp: subset_entailment)
      apply(clarsimp simp: subset_entailment)
             
     apply(rule assign⇩𝒞)
          apply simp
         apply(rule type_aexpr_Const)
        apply simp 
       apply clarsimp 
       apply fast
      apply(simp)
     apply simp
    apply(fastforce intro: pred_entailment_singleton_by_case_distinction simp: image_def)
   apply(fastforce intro: subset_entailment)
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply(rule skip_type)
      apply simp
     apply(clarsimp simp: subtype_def pred_def add_anno_def pred_entailment_def)
    apply simp+
 
 apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply(rule skip_type)
      apply simp
     apply(clarsimp simp: subtype_def pred_def add_anno_def)
    apply (simp add: add_anno_def)
   apply simp+
 
  apply(rule seq_type)
   apply(rule anno_type[OF HOL.refl HOL.refl HOL.refl])
       apply(rule skip_type)
      apply fastforce+
  done
  

method post_conc_tac 
  declares aexpr bexpr =
  ( simp,
   clarsimp simp: type_equiv_def subtype_def pred_entailment_def pred_def,
   clarsimp simp: type_wellformed_def,
   simp, 
   has_type_tac')

method conc_tac for x :: addr and y :: addr  =
  (rule conc'[where  x="x" and t="dma_type y", OF _ HOL.refl])


lemma swap_vars_typed':
  "Γ = (λ_. None) ⟹ 𝒮 = ({},{}) ⟹ P = {} ⟹ 
  ∃Γ' 𝒮' P'. has_type Γ 𝒮 P swap_vars Γ' 𝒮' P'"
  apply (has_type_tac prog: swap_vars_def aexpr: type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
   apply(conc_tac Z Z)
       apply(conc_tac Y Z)  
           apply (has_type_tac' aexpr:type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
          apply post_conc_tac
      apply post_conc_tac
   apply (has_type_tac' aexpr:type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
   apply(conc_tac X X)
       apply (has_type_tac' aexpr:type_aexpr_Load' type_aexpr_Load bexpr:type_bexprI)
      apply  (post_conc_tac)
  done



lemma add_vars_typed':
  "Γ = (λ_. None) ⟹ 𝒮 = ({},{}) ⟹ P = {} ⟹ 
  ∃Γ' 𝒮' P'. has_type Γ 𝒮 P add_vars Γ' 𝒮' P'"
  apply (has_type_no_if_tac
          prog: add_vars_def
          aexpr: type_aexpr_Load' type_aexpr_Load type_aexpr_Add 
           type_aexpr_Add' type_aexpr_Add''  type_aexpr_Const
          bexpr:type_bexprI) 
   apply(rule if_type''[OF _ _ _ _ _ _ HOL.refl])
        apply(rule type_bexprI)
        apply(clarsimp)
        apply(rule HOL.refl)
       apply simp
      apply(rule if_type''[OF _ _ _ _ _ _ HOL.refl])
           apply(rule type_bexprI)
           apply(clarsimp)
           apply(rule HOL.refl)
          apply simp
         apply (has_type_tac' aexpr: type_aexpr_Const)
        apply (has_type_tac' aexpr: type_aexpr_Const)
       apply(clarsimp simp: subset_entailment)
      apply(clarsimp simp: subset_entailment)     
     apply (has_type_tac' aexpr: type_aexpr_Const)
    apply simp
    apply(fastforce intro: pred_entailment_singleton_by_case_distinction simp: image_def)
   apply(fastforce intro: subset_entailment)
  apply (has_type_tac')
  done 

end

end