Quellcode-Bibliothek Safety.thy

(*<*)
theory Safety
  imports Operational IVSubstTypingL BTVSubstTypingL 
begin
  (*>*)

method supp_calc = (metis (mono_tags, opaque_lifting) pure_supp  c.supp e.supp v.supp supp_l_empty opp.supp sup_bot.right_neutral supp_at_base)
declare infer_e.intros[simp]
declare infer_e.intros[intro]

chapter ‹Safety›

text ‹Lemmas about the operational semantics leading up to progress and preservation and then
 .›

section ‹Store Lemmas›

abbreviation delta_ext (‹ _ ⊑ _ ›) where  
  "delta_ext Δ Δ' ≡ (setD Δ ⊆ setD Δ')" 

nominal_function dc_of :: "branch_s ==> string" where
  "dc_of (AS_branch dc _ _) = dc"
  apply(auto,simp add: eqvt_def dc_of_graph_aux_def)
  using   s_branch_s_branch_list.exhaust by metis
nominal_termination (eqvt) by lexicographic_order

lemma delta_sim_fresh: 
  assumes "Θ ⊨ δ ∼ Δ" and "atom u ♯ δ"
  shows "atom u ♯ Δ"
  using assms proof(induct rule : delta_sim.inducts)
  case (delta_sim_nilI Θ)
  then show ?case using fresh_def supp_DNil by blast
next
  case (delta_sim_consI Θ δ Δ v τ u')
  hence  "Θ ; {||} ; GNil ⊨_wf τ" using check_v_wf  by meson
  hence  "supp τ = {}" using  wfT_supp by fastforce
  moreover have  "atom u ♯ u'" using delta_sim_consI fresh_Cons fresh_Pair by blast
  moreover have "atom u ♯ Δ" using delta_sim_consI fresh_Cons by blast
  ultimately show ?case using fresh_Pair fresh_DCons fresh_def by blast
qed

lemma delta_sim_v: 
  fixes Δ::Δ
  assumes "Θ ⊨ δ ∼ Δ " and "(u,v) ∈ set δ" and "(u,τ) ∈ setD Δ" and "Θ ; {||} ; GNil ⊨_wf Δ"
  shows "Θ ; {||} ; GNil ⊨ v <== τ"
  using assms proof(induct δ arbitrary: Δ)
  case Nil
  then show ?case by auto
next
  case (Cons uv δ)
  obtain u' and v' where uv : "uv=(u',v')" by fastforce
  show ?case proof(cases "u'=u")
    case True
    hence  *:"Θ ⊨ ((u,v')#δ) ∼ Δ" using uv Cons by blast
    then obtain τ' and Δ' where tt: "Θ ; {||} ; GNil ⊨ v' <== τ' ∧ u ∉ fst ` set δ ∧ Δ = (u,τ')#<sub>\</sub><Delta>Δ'" using delta_sim_elims(3)[OF *] by metis
    moreover hence "v'=v" using Cons True 
      by (metis Pair_inject fst_conv image_eqI set_ConsD uv)
    moreover have "τ=τ'" using wfD_unique tt Cons 
        setD.simps list.set_intros by blast
    ultimately show ?thesis by metis
  next
    case False
    hence  *:"Θ ⊨ ((u',v')#δ) ∼ Δ" using uv Cons by blast
    then obtain τ' and Δ' where tt: "Θ ⊨ δ ∼ Δ' ∧ Θ ; {||} ; GNil ⊨ v' <== τ' ∧ u' ∉ fst ` set δ ∧ Δ = (u',τ')#_\<Delta>Δ'" using delta_sim_elims(3)[OF *] by metis

    moreover hence "Θ ; {||} ; GNil ⊨_wf Δ'" using wfD_elims Cons delta_sim_elims by metis
    ultimately show ?thesis using Cons  
      using False by auto
  qed
qed

lemma delta_sim_delta_lookup:
  assumes "Θ ⊨ δ ∼ Δ " and "(u, { z : b | c }) ∈ setD Δ" 
  shows "∃v. (u,v) ∈ set δ"
  using assms by(induct rule: delta_sim.inducts,auto+)

lemma update_d_stable:
  "fst ` set δ = fst ` set (update_d δ u v)"
proof(induct δ)
  case Nil
  then show ?case by auto
next
  case (Cons a δ)
  then show ?case using update_d.simps
    by (metis (no_types, lifting) eq_fst_iff image_cong image_insert list.simps(15) prod.exhaust_sel)
qed

lemma update_d_sim:
  fixes Δ::Δ
  assumes "Θ ⊨ δ ∼ Δ" and "Θ ; {||} ; GNil ⊨ v <== τ" and "(u,τ) ∈ setD Δ" and "Θ ; {||} ; GNil ⊨_wf Δ"
  shows "Θ ⊨ (update_d δ u v) ∼ Δ"
  using assms proof(induct δ arbitrary: Δ)
  case Nil
  then show ?case using delta_sim_consI by simp
next
  case (Cons uv δ)
  obtain u' and v' where uv : "uv=(u',v')" by fastforce

  hence  *:"Θ ⊨ ((u',v')#δ) ∼ Δ" using uv Cons by blast
  then obtain τ' and Δ' where tt: "Θ ⊨ δ ∼ Δ' ∧ Θ ; {||} ; GNil ⊨ v' <== τ' ∧ u' ∉ fst ` set δ ∧ Δ = (u',τ')#_\<Delta>Δ'" using delta_sim_elims * by metis

  show ?case proof(cases "u=u'")
    case True
    then have "(u,τ') ∈ setD Δ" using tt by auto
    then have "τ = τ'" using Cons  wfD_unique by metis
    moreover  have "update_d ((u',v')#δ) u v = ((u',v)#δ)" using update_d.simps True by presburger
    ultimately show ?thesis using delta_sim_consI tt Cons True 
      by (simp add: tt uv)
  next
    case False
    have  "Θ ⊨ (u',v') # (update_d δ u v) ∼ (u',τ')#_\<Delta>Δ'" 
    proof(rule delta_sim_consI)
      show "Θ ⊨ update_d δ u v ∼ Δ' " using Cons using delta_sim_consI 
          delta_sim.simps update_d.simps Cons  delta_sim_elims uv  tt 
          False fst_conv set_ConsD wfG_elims wfD_elims  by (metis setD_ConsD)
      show "Θ ; {||} ; GNil ⊨ v' <== τ'" using tt by auto
      show "u' ∉ fst ` set (update_d δ u v)" using  update_d.simps Cons update_d_stable tt by auto
    qed
    thus  ?thesis using False update_d.simps uv 
      by (simp add: tt)
  qed
qed

section ‹Preservation›
text ‹Types are preserved under reduction step. Broken down into lemmas about different operations›

subsection ‹Function Application›

lemma check_s_x_fresh:
  fixes x::x and s::s
  assumes "Θ ; Φ ; B ; GNil ; D ⊨ s <== τ" 
  shows "atom x ♯ s ∧ atom x ♯ τ ∧ atom x ♯ D"
proof - 
  have "Θ ; Φ ; B ; GNil ; D ⊨_wf s : b_of τ"  using check_s_wf[OF assms] by auto 
  moreover have "Θ ; B ; GNil ⊨_wf τ " using check_s_wf assms by auto
  moreover have "Θ ; B ; GNil ⊨_wf D" using check_s_wf assms by auto
  ultimately show ?thesis using wf_supp x_fresh_u 
    by (meson fresh_GNil wfS_x_fresh wfT_x_fresh wfD_x_fresh)
qed

lemma check_funtyp_subst_b: 
  fixes b'::b
  assumes "check_funtyp Θ Φ {|bv|} (AF_fun_typ x b c τ s)" and ‹ Θ ; {||} ⊨_wf b' ›
  shows "check_funtyp Θ Φ {||} (AF_fun_typ x b[bv::=b']_bb (c[bv::=b']_cb) τ[bv::=b']_\<tau>_b s[bv::=b']_sb)"
  using assms proof (nominal_induct "{|bv|}" "AF_fun_typ x b c τ s" rule: check_funtyp.strong_induct)
  case (check_funtypI x' Θ Φ c' s' τ')
  have "check_funtyp Θ Φ {||} (AF_fun_typ x' b[bv::=b']_bb (c'[bv::=b']_cb) τ'[bv::=b']_\<tau>_b s'[bv::=b']_sb)" proof
    show ‹atom x' ♯ (Θ, Φ, {||}::bv fset, b[bv::=b']_bb)› using check_funtypI fresh_prodN x_fresh_b fresh_empty_fset by metis

    have  ‹ Θ ; Φ ; {||} ; ((x', b, c') #_\Γ GNil)[bv::=b']_\Γ_b ; []_\Δ[bv::=b']_\Δ_b ⊨ s'[bv::=b']_sb <== τ'[bv::=b']_\τ_b›  proof(rule subst_b_check_s)
      show ‹ Θ ; {||} ⊨_wf b' › using check_funtypI by metis
      show ‹{|bv|} = {|bv|}› by auto
      show ‹ Θ ; Φ ; {|bv|} ; (x', b, c') #_\Γ GNil ; []_\Δ ⊨ s' <== τ'› using check_funtypI by metis
    qed

    thus ‹ Θ ; Φ ; {||} ; (x', b[bv::=b']_bb, c'[bv::=b']_cb) #_\Γ GNil ; []_\Δ ⊨ s'[bv::=b']_sb <== τ'[bv::=b']_\τ_b›
      using subst_gb.simps subst_db.simps by simp
  qed

  moreover have "(AF_fun_typ x b c τ s) = (AF_fun_typ x' b c' τ' s')"  using fun_typ.eq_iff check_funtypI by metis
  moreover hence "(AF_fun_typ x b[bv::=b']_bb (c[bv::=b']_cb) τ[bv::=b']_\<tau>_b s[bv::=b']_sb) = (AF_fun_typ x' b[bv::=b']_bb (c'[bv::=b']_cb) τ'[bv::=b']_\<tau>_b s'[bv::=b']_sb)"
    using  subst_ft_b.simps by metis
  ultimately show  ?case by metis
qed

lemma funtyp_simple_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  
  assumes "check_funtyp Θ Φ ({||}::bv fset) (AF_fun_typ x b c τ s)" and
    "Θ ; {||} ; GNil ⊨ v <== { x : b | c }" 
  shows "Θ ; Φ ; {||} ; GNil ; DNil ⊨ s[x::=v]_sv <== τ[x::=v]_\<tau>_v"
  using assms proof(nominal_induct  " ({||}::bv fset)" "AF_fun_typ x b c τ s" avoiding: v x  rule: check_funtyp.strong_induct)
  case (check_funtypI x' Θ Φ c' s' τ')

  hence eq1: "{ x' : b | c' } = { x : b | c }" using funtyp_eq_iff_equalities by metis

  obtain x'' and c'' where xf:"{ x : b | c } = { x'' : b | c'' } ∧ atom x'' ♯ (x',v) ∧ atom x'' ♯ (x,c)" using obtain_fresh_z3 by metis 
  moreover have "atom x' ♯ c''" proof -
    have "supp { x'' : b | c'' } = {}" using eq1 check_funtypI xf check_v_wf wfT_nil_supp by metis 
    hence "supp c'' ⊆ { atom x'' }" using  τ.supp eq1 xf by (auto simp add: freshers)
    moreover have "atom x' ≠ atom x''" using xf fresh_Pair fresh_x_neq by metis
    ultimately show ?thesis using xf fresh_Pair fresh_x_neq fresh_def fresh_at_base by blast
  qed
  ultimately have eq2: "c''[x''::=[ x' ]^v]_cv = c'" using eq1  type_eq_subst_eq3(1)[of x' b c' x'' b  c''] by metis

  have "atom x' ♯ c" proof -
    have "supp { x : b | c } = {}" using eq1 check_funtypI xf check_v_wf wfT_nil_supp by metis 
    hence "supp c ⊆ { atom x }" using  τ.supp by auto
    moreover have "atom x ≠ atom x'" using check_funtypI fresh_Pair fresh_x_neq by metis
    ultimately show ?thesis using fresh_def by force
  qed
  hence eq: " c[x::=[ x' ]^v]_cv = c' ∧ s'[x'::=v]_sv = s[x::=v]_sv ∧ τ'[x'::=v]_\<tau>_v = τ[x::=v]_\<tau>_v" 
    using funtyp_eq_iff_equalities type_eq_subst_eq3 check_funtypI by metis

  have " Θ ; Φ ; {||} ; ((x', b, c''[x''::=[ x' ]^v]_cv) #_\<Gamma> GNil)[x'::=v]_\<Gamma>_v ; []_\<Delta>[x'::=v]_\<Delta>_v ⊨ s'[x'::=v]_sv <== τ'[x'::=v]_\<tau>_v" 
  proof(rule subst_check_check_s )
    show ‹Θ ; {||} ; GNil ⊨ v <== { x'' : b | c'' }› using check_funtypI eq1 xf by metis
    show ‹atom x'' ♯ (x', v)› using check_funtypI fresh_x_neq fresh_Pair xf by metis
    show ‹ Θ ; Φ ; {||} ; (x', b, c''[x''::=[ x' ]^v]_cv) #_\Γ GNil ; []_\Δ ⊨ s' <== τ'› using check_funtypI eq2 by metis
    show ‹ (x', b, c''[x''::=[ x' ]^v]_cv) #_\Γ GNil = GNil @ (x', b, c''[x''::=[ x' ]^v]_cv) #_\Γ GNil› using append_g.simps by auto
  qed
  hence " Θ; Φ; {||}; GNil; []_\<Delta> ⊨ s'[x'::=v]_sv <== τ'[x'::=v]_\<tau>_v" using subst_gv.simps subst_dv.simps by auto
  thus ?case using eq  by auto
qed

lemma funtypq_simple_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  
  assumes "check_funtypq Θ Φ (AF_fun_typ_none (AF_fun_typ x b c t s))" and
    "Θ ; {||} ; GNil ⊨ v <== { x : b | c }" 
  shows "Θ; Φ; {||}; GNil; DNil ⊨ s[x::=v]_sv <== t[x::=v]_\<tau>_v"
  using assms proof(nominal_induct  "(AF_fun_typ_none (AF_fun_typ x b c t s))" avoiding: v rule: check_funtypq.strong_induct)
  case (check_fundefq_simpleI Θ Φ x' c' t' s')
  hence eq: "{ x : b | c } = { x' : b | c' } ∧ s'[x'::=v]_sv = s[x::=v]_sv ∧ t[x::=v]_\<tau>_v = t'[x'::=v]_\<tau>_v" 
    using funtyp_eq_iff_equalities by metis
  hence "Θ; Φ; {||}; GNil; []_\<Delta> ⊨ s'[x'::=v]_sv <== t'[x'::=v]_\<tau>_v" 
    using funtyp_simple_check[OF check_fundefq_simpleI(1)] check_fundefq_simpleI by metis
  thus ?case  using eq by metis
qed

lemma funtyp_poly_eq_iff_equalities:
  assumes "[[atom bv']]lst. AF_fun_typ x' b'' c' t' s' = [[atom bv]]lst. AF_fun_typ x b c t s" 
  shows "{ x' : b''[bv'::=b']_bb | c'[bv'::=b']_cb } = { x : b[bv::=b']_bb | c[bv::=b']_cb } ∧
          s'[bv'::=b']_sb[x'::=v]_sv = s[bv::=b']_sb[x::=v]_sv ∧ t'[bv'::=b']_\<tau>_b[x'::=v]_\<tau>_v = t[bv::=b']_\<tau>_b[x::=v]_\<tau>_v" 
proof - 
  have "subst_ft_b (AF_fun_typ x' b'' c' t' s') bv' b' = subst_ft_b (AF_fun_typ x b c t s) bv b'"
    using subst_b_flip_eq_two subst_b_fun_typ_def assms by metis
  thus ?thesis using fun_typ.eq_iff subst_ft_b.simps funtyp_eq_iff_equalities subst_tb.simps 
    by (metis (full_types) assms fun_poly_arg_unique)

qed

lemma funtypq_poly_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  and b'::b
  assumes "check_funtypq Θ Φ (AF_fun_typ_some bv (AF_fun_typ x b c t s))" and
    "Θ ; {||} ; GNil ⊨ v <== { x : b[bv::=b']_bb | c[bv::=b']_cb }"   and
    "Θ ; {||} ⊨_wf b'" 
  shows "Θ; Φ; {||}; GNil; DNil ⊨ s[bv::=b']_sb[x::=v]_sv <== t[bv::=b']_\<tau>_b[x::=v]_\<tau>_v"
  using assms proof(nominal_induct  "(AF_fun_typ_some bv (AF_fun_typ x b c t s))" avoiding: v rule: check_funtypq.strong_induct)
  case (check_funtypq_polyI bv' Θ Φ  x' b'' c' t' s')

  hence **:"{ x' : b''[bv'::=b']_bb | c'[bv'::=b']_cb } = { x : b[bv::=b']_bb | c[bv::=b']_cb } ∧
          s'[bv'::=b']_sb[x'::=v]_sv = s[bv::=b']_sb[x::=v]_sv ∧ t'[bv'::=b']_\<tau>_b[x'::=v]_\<tau>_v = t[bv::=b']_\<tau>_b[x::=v]_\<tau>_v" 
    using funtyp_poly_eq_iff_equalities by metis

  have *:"check_funtyp Θ Φ {||} (AF_fun_typ x' b''[bv'::=b']_bb (c'[bv'::=b']_cb) (t'[bv'::=b']_\<tau>_b) s'[bv'::=b']_sb)"
    using check_funtyp_subst_b[OF check_funtypq_polyI(5) check_funtypq_polyI(8)]  by metis
  moreover have "Θ ; {||} ; GNil ⊨ v <== { x' : b''[bv'::=b']_bb | c'[bv'::=b']_cb }" using ** check_funtypq_polyI by metis
  ultimately have "Θ; Φ; {||}; GNil; []_\<Delta> ⊨ s'[bv'::=b']_sb[x'::=v]_sv <== t'[bv'::=b']_\<tau>_b[x'::=v]_\<tau>_v"
    using funtyp_simple_check[OF *] check_funtypq_polyI by metis
  thus ?case using ** by metis

qed

lemma fundef_simple_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  
  assumes "check_fundef Θ Φ (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c t s)))" and
    "Θ ; {||} ; GNil ⊨ v <== { x : b | c }" and "Θ ; {||} ; GNil ⊨_wf Δ"
  shows "Θ; Φ; {||}; GNil; Δ ⊨ s[x::=v]_sv <== t[x::=v]_\<tau>_v"
  using assms proof(nominal_induct  "(AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c t s)))" avoiding: v rule: check_fundef.strong_induct)
  case (check_fundefI Θ Φ)
  then show ?case using funtypq_simple_check[THEN check_s_d_weakening(1) ] setD.simps by auto
qed

lemma fundef_poly_check:
  fixes s::s  and Δ::Δ and τ::τ and v::v  and b'::b
  assumes "check_fundef Θ Φ (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c t s)))" and
    "Θ ; {||} ; GNil ⊨ v <== { x : b[bv::=b']_bb | c[bv::=b']_cb }" and "Θ ; {||} ; GNil ⊨_wf Δ" and  "Θ ; {||} ⊨_wf b'" 
  shows "Θ; Φ; {||}; GNil; Δ ⊨ s[bv::=b']_sb[x::=v]_sv <== t[bv::=b']_\<tau>_b[x::=v]_\<tau>_v" 
  using assms proof(nominal_induct  "(AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c t s)))" avoiding: v rule: check_fundef.strong_induct)
  case (check_fundefI Θ Φ)
  then show ?case using funtypq_poly_check[THEN check_s_d_weakening(1) ] setD.simps by auto
qed

lemma preservation_app:
  assumes
    "Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x1 b1 c1 τ1' s1'))) = lookup_fun Φ f" and  "(∀fd∈set Φ. check_fundef Θ Φ fd)"
  shows "Θ ; Φ ; B ; G ; Δ ⊨ ss <== τ ==> B = {||} ==> G = GNil ==> ss = LET x = (AE_app f v) IN s ==>
           Θ; Φ; {||}; GNil; Δ ⊨ LET x : (τ1'[x1::=v]_\<tau>_v) = (s1'[x1::=v]_sv) IN s <== τ" and
    "check_branch_s Θ Φ B GNil Δ tid dc const v cs τ ==> True" and 
    "check_branch_list Θ Φ B Γ Δ tid dclist v css τ ==> True"
  using assms proof(nominal_induct τ and τ and τ   avoiding: v rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_letI x2 Θ Φ B Γ Δ e τ z s2 b c)

  hence eq: "e = (AE_app f v)" by simp
  hence *:"Θ ; Φ ; {||} ;GNil ; Δ ⊨ (AE_app f v) ==> { z : b | c }" using check_letI by auto

  then obtain x3 b3 c3 τ3 s3 where
    **:"Θ ; {||} ; GNil ⊨_wf Δ ∧ Θ ⊨_wf Φ ∧ Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x3 b3 c3 τ3 s3))) = lookup_fun Φ f ∧
     Θ ; {||} ; GNil ⊨ v <== { x3 : b3 | c3 } ∧ atom x3 ♯ (Θ, Φ, ({||}::bv fset), GNil, Δ, v, { z : b | c }) ∧ τ3[x3::=v]_\<tau>_v = { z : b | c }"
    using infer_e_elims(6)[OF *] subst_defs by metis

  obtain z3 where z3:"{ x3 : b3 | c3 } = { z3 : b3 | c3[x3::=V_var z3]_cv } ∧ atom z3 ♯ (x3, v,c3,x1,c1)" using obtain_fresh_z3 by metis

  have seq:"[[atom x3]]lst. s3 = [[atom x1]]lst. s1'" using fun_def_eq check_letI ** option.inject by metis

  let ?ft = "AF_fun_typ x3 b3 c3 τ3 s3"


  have sup: "supp τ3 ⊆ { atom x3} ∧ supp s3 ⊆ { atom x3}"  using wfPhi_f_supp ** by metis

  have "Θ; Φ; {||}; GNil; Δ ⊨ AS_let2 x2 τ3[x3::=v]_\<tau>_v (s3[x3::=v]_sv) s2 <== τ" proof
    show ‹atom x2 ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, τ3[x3::=v]_\τ_v, s3[x3::=v]_sv, τ)›
      unfolding fresh_prodN using check_letI fresh_subst_v_if subst_v_τ_def sup
      by (metis all_not_in_conv fresh_def fresh_empty_fset fresh_subst_sv_if fresh_subst_tv_if singleton_iff subset_singleton_iff)

    show ‹ Θ; Φ; {||}; GNil; Δ ⊨ s3[x3::=v]_sv <== τ3[x3::=v]_\τ_v› proof(rule fundef_simple_check)
      show ‹check_fundef Θ Φ (AF_fundef f (AF_fun_typ_none (AF_fun_typ x3 b3 c3 τ3 s3)))› using ** check_letI lookup_fun_member by metis
      show ‹Θ ; {||} ; GNil ⊨ v <== { x3 : b3 | c3 }› using ** by auto
      show ‹ Θ ; {||} ; GNil ⊨_wf Δ › using ** by auto
    qed
    show ‹ Θ ; Φ ; {||} ; (x2, b_of τ3[x3::=v]_\τ_v, c_of τ3[x3::=v]_\τ_v x2) #_\Γ GNil ; Δ ⊨ s2 <== τ›  
      using check_letI ** b_of.simps c_of.simps subst_defs  by metis
  qed

  moreover have "AS_let2 x2 τ3[x3::=v]_\<tau>_v (s3[x3::=v]_sv) s2 = AS_let2 x (τ1'[x1::=v]_\<tau>_v) (s1'[x1::=v]_sv) s" proof -
    have *: "[[atom x2]]lst. s2 = [[atom x]]lst. s" using check_letI  s_branch_s_branch_list.eq_iff by auto
    moreover have " τ3[x3::=v]_\<tau>_v = τ1'[x1::=v]_\<tau>_v" using fun_ret_unique ** check_letI by metis
    moreover have "s3[x3::=v]_sv = (s1'[x1::=v]_sv)" using subst_v_flip_eq_two subst_v_s_def seq by metis
    ultimately show ?thesis using s_branch_s_branch_list.eq_iff by metis
  qed

  ultimately show ?case using check_letI by auto
qed(auto+)

lemma fresh_subst_v_subst_b:
  fixes x2::x and tm::"'a::{has_subst_v,has_subst_b}" and x::x
  assumes  "supp tm ⊆ { atom bv, atom x }" and "atom x2 ♯ v" 
  shows  "atom x2 ♯ tm[bv::=b]_b[x::=v]_v"  
  using assms proof(cases "x2=x")
  case True
  then show ?thesis using fresh_subst_v_if assms by blast
next
  case False
  hence "atom x2 ♯ tm" using assms fresh_def fresh_at_base by force
  hence "atom x2 ♯ tm[bv::=b]_b" using  assms fresh_subst_if x_fresh_b False by force
  then show ?thesis using fresh_subst_v_if assms by auto
qed

lemma preservation_poly_app:
  assumes
    "Some (AF_fundef f (AF_fun_typ_some bv1 (AF_fun_typ x1 b1 c1 τ1' s1'))) = lookup_fun Φ f" and  "(∀fd∈set Φ. check_fundef Θ Φ fd)"
  shows "Θ ; Φ ; B ; G ; Δ ⊨ ss <== τ ==> B = {||} ==> G = GNil ==> ss = LET x = (AE_appP f b' v) IN s ==> Θ ; {||} ⊨_wf b' ==>
               Θ; Φ; {||}; GNil; Δ ⊨ LET x : (τ1'[bv1::=b']_\<tau>_b[x1::=v]_\<tau>_v) = (s1'[bv1::=b']_sb[x1::=v]_sv) IN s <== τ" and
    "check_branch_s Θ Φ B GNil Δ tid dc const v cs τ ==> True" and 
    "check_branch_list Θ Φ B Γ Δ tid dclist v css τ ==> True"
  using assms proof(nominal_induct τ and τ and τ   avoiding: v x1 rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_letI x2 Θ Φ B Γ Δ e τ z s2 b c)

  hence eq: "e = (AE_appP f b' v)" by simp
  hence *:"Θ ; Φ ; {||} ;GNil ; Δ ⊨ (AE_appP f b' v) ==> { z : b | c }" using check_letI by auto

  then obtain x3 b3 c3 τ3 s3 bv3 where
    **:"Θ ; {||} ; GNil ⊨_wf Δ ∧ Θ ⊨_wf Φ ∧ Some (AF_fundef f (AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3))) = lookup_fun Φ f ∧
     Θ ; {||} ; GNil ⊨ v <== { x3 : b3[bv3::=b']_bb | c3[bv3::=b']_cb } ∧ atom x3 ♯ GNil ∧ τ3[bv3::=b']_\<tau>_b[x3::=v]_\<tau>_v = { z : b | c }
  ∧ Θ ; {||} ⊨_wf b'"
    using infer_e_elims(21)[OF *] subst_defs  by metis

  obtain z3 where z3:"{ x3 : b3 | c3 } = { z3 : b3 | c3[x3::=V_var z3]_cv } ∧ atom z3 ♯ (x3, v,c3,x1,c1)" using obtain_fresh_z3 by metis

  let ?ft = "(AF_fun_typ x3 (b3[bv3::=b']_bb) (c3[bv3::=b']_cb) (τ3[bv3::=b']_\<tau>_b) (s3[bv3::=b']_sb))"

  have *:"check_fundef Θ Φ (AF_fundef f (AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3)))" using ** check_letI lookup_fun_member by metis

  hence ftq:"check_funtypq Θ Φ (AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3))" using check_fundef_elims by auto

  let ?ft = "AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3)"

  have sup: "supp τ3 ⊆ { atom x3, atom bv3} ∧ supp s3 ⊆ { atom x3, atom bv3 }"  
    using  wfPhi_f_poly_supp_t wfPhi_f_poly_supp_s ** by metis

  have "Θ; Φ; {||}; GNil; Δ ⊨ AS_let2 x2 τ3[bv3::=b']_\<tau>_b[x3::=v]_\<tau>_v (s3[bv3::=b']_sb[x3::=v]_sv) s2 <== τ" 
  proof
    show ‹atom x2 ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, τ3[bv3::=b']_\τ_b[x3::=v]_\τ_v, s3[bv3::=b']_sb[x3::=v]_sv, τ)›
    proof -

      have "atom x2 ♯ τ3[bv3::=b']_\<tau>_b[x3::=v]_\<tau>_v" 
        using fresh_subst_v_subst_b subst_v_τ_def subst_b_τ_def ‹ atom x2 ♯ v› sup by fastforce      
      moreover have "atom x2 ♯ s3[bv3::=b']_sb[x3::=v]_sv" 
        using fresh_subst_v_subst_b subst_v_s_def subst_b_s_def ‹ atom x2 ♯ v› sup 
      proof -
        have "∀b. atom x2 = atom x3 ∨ atom x2 ♯ s3[bv3::=b]_b"
          by (metis (no_types) check_letI.hyps(1) fresh_subst_sv_if(1) fresh_subst_v_subst_b insert_commute subst_v_s_def sup) (* 140 ms *)
        then show ?thesis
          by (metis check_letI.hyps(1) fresh_subst_sb_if fresh_subst_sv_if(1) has_subst_b_class.subst_b_fresh_x x_fresh_b) (* 78 ms *)
      qed
      ultimately show ?thesis using fresh_prodN check_letI by metis
    qed

    show ‹ Θ; Φ; {||}; GNil; Δ ⊨ s3[bv3::=b']_sb[x3::=v]_sv <== τ3[bv3::=b']_\τ_b[x3::=v]_\τ_v› proof( rule fundef_poly_check)
      show ‹check_fundef Θ Φ (AF_fundef f (AF_fun_typ_some bv3 (AF_fun_typ x3 b3 c3 τ3 s3)))›   
        using **  lookup_fun_member check_letI by metis
      show ‹Θ ; {||} ; GNil ⊨ v <== { x3 : b3[bv3::=b']_bb | c3[bv3::=b']_cb }› using ** by metis
      show ‹ Θ ; {||} ; GNil ⊨_wf Δ › using ** by metis
      show ‹ Θ ; {||} ⊨_wf b' ›  using ** by metis
    qed
    show ‹ Θ ; Φ ; {||} ; (x2, b_of τ3[bv3::=b']_\τ_b[x3::=v]_\τ_v, c_of τ3[bv3::=b']_\τ_b[x3::=v]_\τ_v x2) #_\Γ GNil ; Δ ⊨ s2 <== τ›
      using check_letI ** b_of.simps c_of.simps subst_defs by metis
  qed

  moreover have "AS_let2 x2 τ3[bv3::=b']_\<tau>_b[x3::=v]_\<tau>_v (s3[bv3::=b']_sb[x3::=v]_sv) s2 = AS_let2 x (τ1'[bv1::=b']_\<tau>_b[x1::=v]_\<tau>_v) (s1'[bv1::=b']_sb[x1::=v]_sv) s" proof -
    have *: "[[atom x2]]lst. s2 = [[atom x]]lst. s" using check_letI  s_branch_s_branch_list.eq_iff by auto
    moreover have " τ3[bv3::=b']_\<tau>_b[x3::=v]_\<tau>_v = τ1'[bv1::=b']_\<tau>_b[x1::=v]_\<tau>_v" using fun_poly_ret_unique ** check_letI by metis
    moreover have "s3[bv3::=b']_sb[x3::=v]_sv = (s1'[bv1::=b']_sb[x1::=v]_sv)" using subst_v_flip_eq_two subst_v_s_def  fun_poly_body_unique ** check_letI by metis
    ultimately show ?thesis using s_branch_s_branch_list.eq_iff by metis
  qed

  ultimately show ?case using check_letI by auto
qed(auto+)

lemma check_s_plus:
  assumes "Θ; Φ; {||}; GNil; Δ ⊨ LET x = (AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2))) IN s' <== τ" 
  shows   "Θ; Φ; {||}; GNil; Δ ⊨ LET x = (AE_val (V_lit (L_num (n1+n2)))) IN s' <== τ"   
proof  -
  obtain t1 where 1: "Θ; Φ; {||}; GNil; Δ ⊨ AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2)) ==> t1"
    using assms check_s_elims by metis
  then obtain z1 where 2: "t1 = { z1 : B_int | CE_val (V_var z1) == CE_op Plus ([V_lit (L_num n1)]^ce) ([V_lit (L_num n2)]^ce) }"
    using infer_e_plus by metis

  obtain z2 where 3: ‹Θ ; Φ ; {||} ; GNil ; Δ ⊨ AE_val (V_lit (L_num (n1+n2))) ==> { z2 : B_int | CE_val (V_var z2) == CE_val (V_lit (L_num (n1+n2))) }›
    using infer_v_form infer_e_valI infer_v_litI   infer_l.intros infer_e_wf 1 
    by (simp add: fresh_GNil)

  let ?e = " (AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2)))"

  show ?thesis proof(rule  subtype_let)
    show "Θ ; Φ ; {||} ; GNil ; Δ ⊨ LET x = ?e IN s' <== τ" using assms by auto
    show "Θ ; Φ ; {||} ; GNil ; Δ ⊨ ?e ==> t1" using 1 by auto
    show "Θ ; Φ ; {||} ; GNil ; Δ ⊨ [ [ L_num (n1 + n2) ]^v ]^e ==> { z2 : B_int | CE_val (V_var z2) == CE_val (V_lit (L_num (n1+n2))) }" using 3 by auto
    show "Θ ; {||} ; GNil ⊨ { z2 : B_int | CE_val (V_var z2) == CE_val (V_lit (L_num (n1+n2))) } < t1" using subtype_bop_arith 
      by (metis "1" ‹∧thesis. (∧z1. t1 = { z1 : B_int | [ [ z1 ]^v ]^ce == [ plus [ [ L_num n1 ]^v ]^ce [ [ L_num n2 ]^v ]^ce ]^ce } ==> thesis) ==> thesis› infer_e_wf(2) opp.distinct(1) type_for_lit.simps(3))
  qed

qed

lemma check_s_leq:
  assumes "Θ ; Φ ; {||} ; GNil ; Δ ⊨ LET x = (AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2))) IN s' <== τ" 
  shows "Θ; Φ; {||}; GNil; Δ ⊨ LET x = (AE_val (V_lit (if (n1 ≤ n2) then L_true else L_false))) IN s' <== τ"   
proof -
  obtain t1 where 1: "Θ; Φ; {||}; GNil; Δ ⊨ AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2)) ==> t1"
    using assms check_s_elims by metis
  then obtain z1 where 2: "t1 = { z1 : B_bool | CE_val (V_var z1) == CE_op LEq ([V_lit (L_num n1)]^ce) ([V_lit (L_num n2)]^ce) }"
    using infer_e_leq by auto

  obtain z2 where 3: ‹Θ ; Φ ; {||} ; GNil ; Δ ⊨ AE_val (V_lit ((if (n1 ≤ n2) then L_true else L_false))) ==> { z2 : B_bool | CE_val (V_var z2) == CE_val (V_lit ((if (n1 ≤ n2) then L_true else L_false))) }›
    using infer_v_form infer_e_valI infer_v_litI   infer_l.intros infer_e_wf 1 
      fresh_GNil 
    by simp

  show ?thesis proof(rule subtype_let)
    show ‹ Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_op LEq [ L_num n1 ]^v [ L_num n2 ]^v) s' <== τ› using assms by auto
    show ‹Θ; Φ; {||}; GNil; Δ ⊨ AE_op LEq [ L_num n1 ]^v [ L_num n2 ]^v ==> t1› using 1 by auto
    show ‹Θ; Φ; {||}; GNil; Δ ⊨ [ [ if n1 ≤ n2 then L_true else L_false ]^v ]^e ==> { z2 : B_bool | CE_val (V_var z2) == CE_val (V_lit ((if (n1 ≤ n2) then L_true else L_false))) }› using 3 by auto
    show ‹Θ ; {||} ; GNil ⊨ { z2 : B_bool | CE_val (V_var z2) == CE_val (V_lit ((if (n1 ≤ n2) then L_true else L_false))) } < t1›
      using subtype_bop_arith[where opp=LEq] check_s_wf assms 2  
      by (metis opp.distinct(1) subtype_bop_arith type_l_eq)
  qed
qed

lemma check_s_eq:
  assumes "Θ ; Φ ; {||} ; GNil ; Δ ⊨ LET x = (AE_op Eq (V_lit (n1)) (V_lit ( n2))) IN s' <== τ" 
  shows "Θ; Φ; {||}; GNil; Δ ⊨ LET x = (AE_val (V_lit (if (n1 = n2) then L_true else L_false))) IN s' <== τ"   
proof -
  obtain t1 where 1: "Θ; Φ; {||}; GNil; Δ ⊨ AE_op Eq (V_lit (n1)) (V_lit (n2)) ==> t1"
    using assms check_s_elims by metis
  then obtain z1 where 2: "t1 = { z1 : B_bool | CE_val (V_var z1) == CE_op Eq ([V_lit (n1)]^ce) ([V_lit (n2)]^ce) }"
    using infer_e_leq by auto

  obtain z2 where 3: ‹Θ ; Φ ; {||} ; GNil ; Δ ⊨ AE_val (V_lit ((if (n1 = n2) then L_true else L_false))) ==> { z2 : B_bool | CE_val (V_var z2) == CE_val (V_lit ((if (n1 = n2) then L_true else L_false))) }›
    using infer_v_form infer_e_valI infer_v_litI   infer_l.intros infer_e_wf 1 
      fresh_GNil 
    by simp

  show ?thesis proof(rule subtype_let)
    show ‹ Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_op Eq [ n1 ]^v [ n2 ]^v) s' <== τ› using assms by auto
    show ‹Θ; Φ; {||}; GNil; Δ ⊨ AE_op Eq [ n1 ]^v [ n2 ]^v ==> t1› using 1 by auto
    show ‹Θ; Φ; {||}; GNil; Δ ⊨ [ [ if n1 = n2 then L_true else L_false ]^v ]^e ==> { z2 : B_bool | CE_val (V_var z2) == CE_val (V_lit ((if (n1 = n2) then L_true else L_false))) }› using 3 by auto
    show ‹Θ ; {||} ; GNil ⊨ { z2 : B_bool | CE_val (V_var z2) == CE_val (V_lit ((if (n1 = n2) then L_true else L_false))) } < t1›
    proof -
      have " { z2 : B_bool | [ [ z2 ]^v ]^ce == [ eq [ [ n1 ]^v ]^ce [ [ n2 ]^v ]^ce ]^ce } = t1" using 2 
        by (metis τ_fresh_c fresh_opp_all infer_l_form2 infer_l_fresh ms_fresh_all(31) ms_fresh_all(33) obtain_fresh_z type_e_eq type_l_eq)
      moreover have "Θ ; {||} ⊨_wf GNil" using assms wfX_wfY by fastforce
      moreover have "base_for_lit n1 = base_for_lit n2" using 1 infer_e_wf wfE_elims(12) wfV_elims 
        by metis
      ultimately show ?thesis using subtype_bop_eq[OF ‹Θ ; {||} ⊨_wf GNil›, of n1 n2 z2] by auto     
    qed
  qed
qed

subsection ‹Operators›

lemma preservation_plus:
  assumes "Θ; Φ; Δ ⊨ ⟨ δ , LET x = (AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2))) IN s' ⟩ <== τ"        
  shows "Θ; Φ; Δ ⊨ ⟨ δ , LET x = (AE_val (V_lit (L_num (n1+n2)))) IN s' ⟩ <== τ"
proof -

  have tt: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_op Plus (V_lit (L_num n1)) (V_lit (L_num n2))) s' <== τ" and dsim: "Θ ⊨ δ ∼ Δ" and fd:"(∀fd∈set Φ. check_fundef Θ Φ fd)"
    using assms config_type_elims by blast+

  hence "Θ; Φ; {||}; GNil; Δ ⊨AS_let x (AE_val (V_lit (L_num (n1+n2)))) s' <== τ" using check_s_plus assms by auto  

  hence "Θ; Φ; Δ ⊨ ⟨ δ , AS_let x (AE_val (V_lit ( (L_num (n1+n2))))) s' ⟩ <== τ" using dsim config_typeI fd by presburger
  then show ?thesis using dsim config_typeI 
    by (meson order_refl)
qed

lemma preservation_leq:
  assumes "Θ; Φ; Δ ⊨ ⟨ δ , AS_let x (AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2))) s' ⟩ <== τ"        
  shows "Θ; Φ; Δ ⊨ ⟨ δ , AS_let x (AE_val (V_lit (((if (n1 ≤ n2) then L_true else L_false))))) s' ⟩ <== τ"
proof -

  have tt: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_op LEq (V_lit (L_num n1)) (V_lit (L_num n2))) s' <== τ" and dsim: "Θ ⊨ δ ∼ Δ" and fd:"(∀fd∈set Φ. check_fundef Θ Φ fd)"
    using assms config_type_elims by blast+

  hence "Θ; Φ; {||}; GNil; Δ ⊨AS_let x (AE_val (V_lit ( ((if (n1 ≤ n2) then L_true else L_false))))) s' <== τ" using check_s_leq assms by auto  

  hence "Θ; Φ; Δ ⊨ ⟨ δ , AS_let x (AE_val (V_lit ( (((if (n1 ≤ n2) then L_true else L_false)))))) s' ⟩ <== τ" using dsim config_typeI fd by presburger
  then show ?thesis using dsim config_typeI 
    by (meson order_refl)
qed

lemma preservation_eq:
  assumes "Θ; Φ; Δ ⊨ ⟨ δ , AS_let x (AE_op Eq (V_lit (n1)) (V_lit (n2))) s' ⟩ <== τ"        
  shows "Θ; Φ; Δ ⊨ ⟨ δ , AS_let x (AE_val (V_lit (((if (n1 = n2) then L_true else L_false))))) s' ⟩ <== τ"
proof -

  have tt: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_op Eq (V_lit (n1)) (V_lit (n2))) s' <== τ" and dsim: "Θ ⊨ δ ∼ Δ" and fd:"(∀fd∈set Φ. check_fundef Θ Φ fd)"
    using assms config_type_elims by blast+

  hence "Θ; Φ; {||}; GNil; Δ ⊨AS_let x (AE_val (V_lit ( ((if (n1 = n2) then L_true else L_false))))) s' <== τ" using check_s_eq assms by auto  

  hence "Θ; Φ; Δ ⊨ ⟨ δ , AS_let x (AE_val (V_lit ( (((if (n1 = n2) then L_true else L_false)))))) s' ⟩ <== τ" using dsim config_typeI fd by presburger
  then show ?thesis using dsim config_typeI 
    by (meson order_refl)
qed

subsection ‹Let Statements›

lemma subst_s_abs_lst:
  fixes s::s and sa::s and v'::v
  assumes "[[atom x]]lst. s = [[atom xa]]lst. sa" and "atom xa ♯ v ∧ atom x ♯ v"
  shows "s[x::=v]_sv = sa[xa::=v]_sv"
proof -
  obtain c'::x where cdash: "atom c' ♯ (v, x, xa, s, sa)" using obtain_fresh by blast    
  moreover have " (x ↔ c') ∙ s = (xa ↔ c') ∙ sa" proof -
    have "atom c' ♯ (s, sa) ∧ atom c' ♯ (x, xa, s, sa)" using cdash by auto
    thus ?thesis using assms by auto
  qed
  ultimately show ?thesis using assms 
    using subst_sv_flip by auto 
qed

lemma check_let_val: 
  fixes v::v and s::s
  shows "Θ ; Φ ; B ; G ; Δ ⊨ ss <== τ ==> B = {||} ==> G = GNil ==>
        ss = AS_let x (AE_val v) s ∨ ss = AS_let2 x t (AS_val v) s ==> Θ; Φ; {||}; GNil; Δ ⊨ (s[x::=v]_sv) <== τ" and
    "check_branch_s Θ Φ B GNil Δ tid dc const v cs τ ==> True" and 
    "check_branch_list Θ Φ B Γ Δ tid dclist v css τ ==> True"
proof(nominal_induct τ and τ and τ  avoiding: v rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_letI x1 Θ Φ B Γ Δ e τ z s1 b c)
  hence *:"e = AE_val v" by auto
  let ?G = "(x1, b, c[z::=V_var x1]_cv) #_\<Gamma> Γ"
  have "Θ ; Φ ; B ; ?G[x1::=v]_\<Gamma>_v ; Δ[x1::=v]_\<Delta>_v ⊨ s1[x1::=v]_sv <== τ[x1::=v]_\<tau>_v" 
  proof(rule subst_infer_check_s(1))
    show **:‹ Θ ; B ; Γ ⊨ v ==> { z : b | c }› using infer_e_elims check_letI * by fast
    thus ‹Θ ; B ; Γ ⊨ { z : b | c } < { z : b | c }› using subtype_reflI  infer_v_wf by metis
    show ‹atom z ♯ (x1, v)› using check_letI fresh_Pair by auto
    show ‹Θ ; Φ ; B ; (x1, b, c[z::=V_var x1]_cv) #_\Γ Γ ; Δ ⊨ s1 <== τ› using check_letI subst_defs by auto
    show "(x1, b, c[z::=V_var x1]_cv) #_\<Gamma> Γ = GNil @ (x1, b, c[z::=V_var x1]_cv) #_\<Gamma> Γ" by auto
  qed

  hence "Θ ; Φ ; B ; Γ ; Δ ⊨ s1[x1::=v]_sv <== τ"  using check_letI by auto
  moreover have " s1[x1::=v]_sv = s[x::=v]_sv" 
    by (metis (full_types) check_letI fresh_GNil infer_e_elims(7) s_branch_s_branch_list.distinct s_branch_s_branch_list.eq_iff(2) 
        subst_s_abs_lst wfG_x_fresh_in_v_simple)

  ultimately show ?case using check_letI by simp
next
  case (check_let2I x1 Θ Φ B Γ Δ t s1 τ s2 )

  hence s1eq:"s1 = AS_val v" by auto
  let ?G = "(x1, b_of t, c_of t x1) #_\<Gamma> Γ"
  obtain z::x where *:"atom z ♯ (x1 , v,t)"  using obtain_fresh_z by metis
  hence teq:"t = { z : b_of t | c_of t z }" using b_of_c_of_eq by auto
  have "Θ ; Φ ; B ; ?G[x1::=v]_\<Gamma>_v ; Δ[x1::=v]_\<Delta>_v ⊨ s2[x1::=v]_sv <== τ[x1::=v]_\<tau>_v" 
  proof(rule subst_check_check_s(1))
    obtain t' where "Θ ; B ; Γ ⊨ v ==> t' ∧ Θ ; B ; Γ ⊨ t' < t" using  check_s_elims(1) check_let2I(10) s1eq by auto
    thus  **:‹ Θ ; B ; Γ ⊨ v <== { z : b_of t | c_of t z }› using  check_v.intros teq by auto
    show "atom z ♯ (x1, v)" using * by auto
    show ‹ Θ ; Φ ; B ; (x1, b_of t, c_of t x1) #_\Γ Γ ; Δ ⊨ s2 <== τ› using check_let2I by auto
    show "(x1, b_of t , c_of t x1) #_\<Gamma> Γ = GNil @ (x1, b_of t, (c_of t z)[z::=V_var x1]_cv) #_\<Gamma> Γ" using append_g.simps c_of_switch * fresh_prodN by metis
  qed

  hence "Θ ; Φ ; B ; Γ ; Δ ⊨ s2[x1::=v]_sv <== τ"  using check_let2I by auto
  moreover have " s2[x1::=v]_sv = s[x::=v]_sv" using
      check_let2I fresh_GNil check_s_elims s_branch_s_branch_list.distinct s_branch_s_branch_list.eq_iff
      subst_s_abs_lst wfG_x_fresh_in_v_simple
  proof -
    have "AS_let2 x t (AS_val v) s = AS_let2 x1 t s1 s2"
      by (metis check_let2I.prems(3) s_branch_s_branch_list.distinct s_branch_s_branch_list.eq_iff(3)) (* 62 ms *)
    then show ?thesis
      by (metis (no_types) check_let2I check_let2I.prems(2) check_s_elims(1) fresh_GNil s_branch_s_branch_list.eq_iff(3) subst_s_abs_lst wfG_x_fresh_in_v_simple) (* 375 ms *)
  qed

  ultimately show ?case using check_let2I by simp
qed(auto+)

lemma preservation_let_val:
  assumes "Θ; Φ; Δ ⊨ ⟨ δ , AS_let x (AE_val v) s ⟩ <== τ ∨ Θ; Φ; Δ ⊨ ⟨ δ , AS_let2 x t (AS_val v) s ⟩ <== τ" (is "?A ∨ ?B")
  shows " ∃Δ'. Θ; Φ; Δ' ⊨ ⟨ δ , s[x::=v]_sv ⟩ <== τ ∧ Δ ⊑ Δ'"
proof -
  have tt:  "Θ ⊨ δ ∼ Δ" and fd: "(∀fd∈set Φ. check_fundef Θ Φ fd)"
    using assms by blast+

  have  "?A ∨ ?B" using assms by auto
  then have "Θ; Φ; {||}; GNil; Δ ⊨ s[x::=v]_sv <== τ"
  proof
    assume "Θ; Φ; Δ ⊨ ⟨ δ , AS_let x (AE_val v) s ⟩ <== τ"
    hence * : " Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_val v) s <== τ" by blast
    thus ?thesis using check_let_val by simp
  next
    assume "Θ; Φ; Δ ⊨ ⟨ δ , AS_let2 x t (AS_val v) s ⟩ <== τ"
    hence * : "Θ; Φ; {||}; GNil; Δ ⊨ AS_let2 x t (AS_val v) s <== τ" by blast
    thus ?thesis using check_let_val by simp
  qed

  thus  ?thesis using tt config_typeI fd
      order_refl by metis
qed

lemma check_s_fst_snd:
  assumes "fst_snd = AE_fst ∧ v=v1 ∨ fst_snd = AE_snd ∧ v=v2" 
    and   "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (fst_snd (V_pair v1 v2)) s' <== τ"
  shows "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x ( AE_val v) s' <== τ"
proof -
  have  1: ‹ Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (fst_snd (V_pair v1 v2)) s' <== τ› using assms by auto

  then obtain t1 where 2:"Θ; Φ; {||}; GNil; Δ ⊨ (fst_snd (V_pair v1 v2)) ==> t1" using check_s_elims by auto

  show ?thesis using subtype_let 1 2 assms 
    by (meson infer_e_fst_pair infer_e_snd_pair)
qed

lemma preservation_fst_snd:
  assumes "Θ; Φ; Δ ⊨ ⟨ δ , LET x = (fst_snd (V_pair v1 v2)) IN s' ⟩ <== τ" and 
    "fst_snd = AE_fst ∧ v=v1 ∨ fst_snd = AE_snd ∧ v=v2"
  shows "∃Δ'. Θ; Φ; Δ ⊨ ⟨ δ , LET x = (AE_val v) IN s' ⟩ <== τ ∧ Δ ⊑ Δ'"
proof - 
  have  tt: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (fst_snd (V_pair v1 v2)) s' <== τ ∧ Θ ⊨ δ ∼ Δ" using assms by blast
  hence t2: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (fst_snd (V_pair v1 v2)) s' <== τ" by auto

  moreover have "∀fd∈set Φ. check_fundef Θ Φ fd" using assms config_type_elims by auto
  ultimately show ?thesis using config_typeI order_refl tt assms check_s_fst_snd by metis
qed

inductive_cases check_branch_s_elims2[elim!]:
  "Θ ; Φ ; B ; Γ ; Δ; tid ; cons ; const ; v ⊨ cs <== τ"

lemmas freshers = freshers atom_dom.simps toSet.simps fresh_def x_not_in_b_set
declare freshers [simp]

lemma subtype_eq_if:
  fixes t::τ and va::v
  assumes "Θ ; B ; Γ ⊨_wf { z : b_of t | c_of t z }" and "Θ ; B ; Γ ⊨_wf { z : b_of t | c IMP c_of t z } "
  shows   "Θ ; B ; Γ ⊨ { z : b_of t | c_of t z } < { z : b_of t | c IMP c_of t z } "
proof -
  obtain x::x where xf:"atom x ♯ ((Θ, B, Γ, z, c_of t z, z, c IMP c_of t z ),c)" using obtain_fresh by metis

  moreover have "Θ ; B ; (x, b_of t, (c_of t z)[z::=[ x ]^v]_cv) #_\<Gamma> Γ ⊨ (c IMP c_of t z )[z::=[ x ]^v]_cv " 
    unfolding subst_cv.simps 
  proof(rule valid_eq_imp)

    have "Θ ; B ; (x, b_of t, (c_of t z)[z::=[ x ]^v]_v) #_\<Gamma> Γ ⊨_wf (c IMP (c_of t z))[z::=[ x ]^v]_v " 
      apply(rule  wfT_wfC_cons)
      apply(simp add: assms, simp add: assms, unfold fresh_prodN )
      using  xf fresh_prodN by metis+     
    thus "Θ ; B ; (x, b_of t, (c_of t z)[z::=[ x ]^v]_cv) #_\<Gamma> Γ ⊨_wf c[z::=[ x ]^v]_cv IMP (c_of t z)[z::=[ x ]^v]_cv " 
      using subst_cv.simps subst_defs by auto
  qed

  ultimately show ?thesis using subtype_baseI assms fresh_Pair subst_defs by metis
qed

lemma subtype_eq_if_τ:
  fixes t::τ and va::v
  assumes "Θ ; B ; Γ ⊨_wf t" and "Θ ; B ; Γ ⊨_wf { z : b_of t | c IMP c_of t z } " and "atom z ♯ t"
  shows   "Θ ; B ; Γ ⊨ t < { z : b_of t | c IMP c_of t z } "
proof -
  have "t = { z : b_of t | c_of t z }" using b_of_c_of_eq assms by auto
  thus ?thesis  using subtype_eq_if assms  c_of.simps b_of.simps by metis
qed

lemma valid_conj:
  assumes  "Θ ; B ; Γ ⊨ c1" and "Θ ; B ; Γ ⊨ c2" 
  shows "Θ ; B ; Γ ⊨ c1 AND c2" 
proof
  show ‹ Θ ; B ; Γ ⊨_wf c1 AND c2 › using valid.simps wfC_conjI assms by auto
  show ‹∀i. Θ ; Γ ⊨ i ∧ i ⊨ Γ ⟶ i ⊨ c1 AND c2 ›
  proof(rule+)
    fix i
    assume *:"Θ ; Γ ⊨ i ∧ i ⊨ Γ " 
    thus "i [ c1 ] ~ True" using assms valid.simps 
      using is_satis.cases by blast
    show "i [ c2 ] ~ True" using assms valid.simps 
      using is_satis.cases * by blast  
  qed
qed

subsection ‹Other Statements›

lemma check_if:
  fixes s'::s and cs::branch_s and css::branch_list and v::v
  shows    "Θ; Φ; B; G; Δ ⊨ s' <== τ ==> s' = IF (V_lit ll) THEN s1 ELSE s2 ==>
        Θ ; {||} ; GNil ⊨_wf τ ==> G = GNil ==> B = {||} ==> ll = L_true ∧ s = s1 ∨ ll = L_false ∧ s = s2 ==>
        Θ; Φ; {||}; GNil; Δ ⊨ s <== τ" and
    "check_branch_s Θ Φ {||} GNil Δ tid dc const v cs τ ==> True" and 
    "check_branch_list Θ Φ {||} Γ Δ tid dclist v css τ ==> True"
proof(nominal_induct τ and τ and τ  rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_ifI z Θ Φ B Γ Δ v s1 s2 τ)
  obtain z' where teq: "τ = { z' : b_of τ | c_of τ z' } ∧ atom z' ♯ (z,τ)" using obtain_fresh_z_c_of by metis
  hence ceq: "(c_of τ z')[z'::=[ z ]^v]_cv = (c_of τ z)" using c_of_switch fresh_Pair by metis
  have zf: " atom z ♯ c_of τ z'"
    using c_of_fresh check_ifI teq fresh_Pair fresh_at_base by metis
  hence 1:"Θ; Φ; {||}; GNil; Δ ⊨ s <== { z : b_of τ | CE_val (V_lit ll) == CE_val (V_lit ll) IMP c_of τ z }" using check_ifI by auto
  moreover have 2:"Θ ; {||} ; GNil ⊨ ({ z : b_of τ | CE_val (V_lit ll) == CE_val (V_lit ll) IMP c_of τ z }) < τ" 
  proof - 
    have "Θ ; {||} ; GNil ⊨_wf ({ z : b_of τ | CE_val (V_lit ll ) == CE_val (V_lit ll) IMP c_of τ z })" using check_ifI check_s_wf by auto
    moreover have "Θ ; {||} ; GNil ⊨_wf τ" using  check_s_wf check_ifI by auto
    ultimately show ?thesis using subtype_if_simp[of Θ " {||}" z "b_of τ" ll "c_of τ z'" z'] using teq ceq zf subst_defs by metis
  qed
  ultimately show ?case  using check_s_supertype(1) check_ifI by metis
qed(auto+)

lemma preservation_if: 
  assumes  "Θ; Φ; Δ ⊨ ⟨ δ , IF (V_lit ll) THEN s1 ELSE s2 ⟩ <== τ" and 
    "ll = L_true ∧ s = s1 ∨ ll = L_false ∧ s = s2"
  shows "Θ; Φ; Δ ⊨ ⟨δ, s⟩ <== τ ∧ setD Δ ⊆ setD Δ"
proof -
  have *: "Θ; Φ; {||}; GNil; Δ ⊨ AS_if (V_lit ll) s1 s2 <== τ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using assms config_type_elims by metis
  hence "Θ; Φ; {||}; GNil; Δ ⊨ s <== τ" using check_s_wf check_if assms by metis
  hence "Θ; Φ; Δ ⊨ ⟨δ, s⟩ <== τ ∧ setD Δ ⊆ setD Δ" using config_typeI * 
    using assms(1) by blast
  thus ?thesis by blast
qed

lemma wfT_conj:
  assumes "Θ ; B ; GNil ⊨_wf { z : b | c1 }" and  "Θ ; B ; GNil ⊨_wf { z : b | c2 }"
  shows  "Θ ; B ; GNil ⊨_wf { z : b | c1 AND c2}"
proof
  show ‹atom z ♯ (Θ, B, GNil)›
    apply(unfold fresh_prodN, intro conjI) 
    using wfTh_fresh wfT_wf assms apply metis
    using fresh_GNil x_not_in_b_set fresh_def by metis+   
  show ‹ Θ ; B ⊨_wf b › using wfT_elims assms by metis
  have "Θ ; B ; (z, b, TRUE) #_\<Gamma> GNil ⊨_wf c1" using wfT_wfC fresh_GNil assms by auto
  moreover have "Θ ; B ; (z, b, TRUE) #_\<Gamma> GNil ⊨_wf c2" using wfT_wfC fresh_GNil assms by auto
  ultimately show ‹ Θ ; B ; (z, b, TRUE) #_\Γ GNil ⊨_wf c1 AND c2 › using wfC_conjI by auto
qed

lemma subtype_conj:
  assumes    "Θ ; B ; GNil ⊨ t < { z : b | c1 }" and   "Θ ; B ; GNil ⊨ t < { z : b | c2 }" 
  shows   "Θ ; B ; GNil ⊨ { z : b | c_of t z } < { z : b | c1 AND c2 }" 
proof -
  have beq: "b_of t = b" using subtype_eq_base2 b_of.simps assms by metis
  obtain x::x where x:‹atom x ♯ (Θ, B, GNil, z, c_of t z, z, c1 AND c2 )› using obtain_fresh by metis
  thus ?thesis proof
    have "atom z ♯ t" using subtype_wf wfT_supp fresh_def x_not_in_b_set atom_dom.simps toSet.simps assms dom.simps by fastforce
    hence t:"t = { z : b_of t | c_of t z }" using b_of_c_of_eq by auto
    thus  ‹ Θ ; B ; GNil ⊨_wf { z : b | c_of t z } › using subtype_wf beq assms by auto

    show ‹Θ ; B ; (x, b, (c_of t z)[z::=[ x ]^v]_v) #_\Γ GNil ⊨ (c1 AND c2 )[z::=[ x ]^v]_v ›      
    proof -
      have ‹Θ ; B ; (x, b, (c_of t z)[z::=[ x ]^v]_v) #_\Γ GNil ⊨ c1[z::=[ x ]^v]_v ›
      proof(rule subtype_valid)
        show ‹Θ ; B ; GNil ⊨ t < { z : b | c1 }› using assms by auto
        show ‹atom x ♯ GNil› using fresh_GNil by auto
        show ‹t = { z : b | c_of t z }› using t beq by auto
        show ‹{ z : b | c1 } = { z : b | c1 }› by auto
      qed
      moreover have ‹Θ ; B ; (x, b, (c_of t z)[z::=[ x ]^v]_v) #_\Γ GNil ⊨ c2[z::=[ x ]^v]_v ›
      proof(rule subtype_valid)
        show ‹Θ ; B ; GNil ⊨ t < { z : b | c2 }› using assms by auto
        show ‹atom x ♯ GNil› using fresh_GNil by auto
        show ‹t = { z : b | c_of t z }› using t beq by auto
        show ‹{ z : b | c2 } = { z : b | c2 }› by auto
      qed
      ultimately show ?thesis unfolding subst_cv.simps subst_v_c_def  using valid_conj by metis
    qed
    thus ‹ Θ ; B ; GNil ⊨_wf { z : b | c1 AND c2 } › using subtype_wf wfT_conj assms by auto
  qed
qed

lemma infer_v_conj:
  assumes "Θ ; B ; GNil ⊨ v <== { z : b | c1 }" and "Θ ; B ; GNil ⊨ v <== { z : b | c2 }"
  shows "Θ ; B ; GNil ⊨ v <== { z : b | c1 AND c2 }" 
proof -
  obtain t1 where t1: "Θ ; B ; GNil ⊨ v ==> t1 ∧ Θ ; B ; GNil ⊨ t1 < { z : b | c1 }" 
    using assms check_v_elims by metis
  obtain t2 where t2: "Θ ; B ; GNil ⊨ v ==> t2 ∧ Θ ; B ; GNil ⊨ t2 < { z : b | c2 }" 
    using assms check_v_elims by metis
  have teq: "t1 = { z : b | c_of t1 z }" using subtype_eq_base2 b_of.simps 
    by (metis (full_types) b_of_c_of_eq fresh_GNil infer_v_t_wf t1 wfT_x_fresh)
  have "t1 = t2" using infer_v_uniqueness t1 t2 by auto
  hence " Θ ; B ; GNil ⊨ { z : b | c_of t1 z } < { z : b | c1 AND c2 }" using subtype_conj t1 t2 by simp
  hence " Θ ; B ; GNil ⊨ t1 < { z : b | c1 AND c2 }" using teq by auto
  thus ?thesis using t1 using check_v.intros by auto
qed

lemma wfG_conj:
  fixes c1::c
  assumes  "Θ ; B ⊨_wf (x, b, c1 AND c2) #_\<Gamma> Γ"
  shows "Θ ; B ⊨_wf (x, b, c1) #_\<Gamma> Γ"
proof(cases "c1 ∈ {TRUE, FALSE}")
  case True
  then show ?thesis using assms wfG_cons2I  wfG_elims wfX_wfY by metis
next
  case False
  then show ?thesis using assms wfG_cons1I  wfG_elims wfX_wfY wfC_elims 
    by (metis wfG_elim2)
qed

lemma check_match:
  fixes s'::s and s::s and css::branch_list and cs::branch_s
  shows "Θ ; Φ ; B ; Γ ; Δ ⊨ s <== τ ==> True" and
    "Θ ; Φ ; B ; G ; Δ ; tid ; dc ; const ; vcons ⊨ cs <== τ ==>
             vcons = V_cons tid dc v ==> B = {||} ==> G = GNil ==> cs = (dc x' ==> s') ==>
             Θ ; {||} ; GNil ⊨ v <== const ==>
             Θ; Φ; {||}; GNil; Δ ⊨ s'[x'::=v]_sv <== τ" and
    "Θ ; Φ ; B ; G ; Δ ; tid ; dclist ; vcons ⊨ css <== τ ==> distinct (map fst dclist) ==>
             vcons = V_cons tid dc v ==> B = {||} ==> (dc, const) ∈ set dclist ==> G = GNil ==>
             Some (AS_branch dc x' s') = lookup_branch dc css ==> Θ ; {||} ; GNil ⊨ v <== const ==>
             Θ; Φ; {||}; GNil; Δ ⊨ s'[x'::=v]_sv <== τ"
proof(nominal_induct τ and τ and τ avoiding: x' v  rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_branch_list_consI Θ Φ B Γ Δ tid consa consta va cs τ dclist cssa)

  then obtain xa and sa where cseq:"cs = AS_branch consa xa sa" using check_branch_s_elims2[OF check_branch_list_consI(1)] by metis

  show ?case proof(cases "dc = consa")
    case True
    hence "cs = AS_branch consa x' s'" using check_branch_list_consI cseq 
      by (metis lookup_branch.simps(2) option.inject)
    moreover have "const = consta" using check_branch_list_consI distinct.simps 
      by (metis True dclist_distinct_unique list.set_intros(1))
    moreover have "va = V_cons tid consa v" using check_branch_list_consI True by auto
    ultimately  show ?thesis using check_branch_list_consI  by auto
  next
    case False
    hence "Some (AS_branch dc x' s') = lookup_branch dc cssa" using lookup_branch.simps(2) check_branch_list_consI(10) cseq by auto
    moreover have "(dc, const) ∈ set dclist" using check_branch_list_consI False by simp
    ultimately show ?thesis using check_branch_list_consI by auto
  qed

next
  case (check_branch_list_finalI Θ Φ B Γ Δ tid cons const va cs τ)
  hence " cs = AS_branch cons x' s'" using lookup.simps check_branch_list_finalI lookup_branch.simps option.inject 
    by (metis map_of.simps(1) map_of_Cons_code(2) option.distinct(1) s_branch_s_branch_list.exhaust(2) weak_map_of_SomeI)
  then show ?case using check_branch_list_finalI by auto
next
  case (check_branch_s_branchI Θ B Γ Δ τ const x Φ tid cons va s)

  text ‹Supporting facts here to make the main body of the proof concise›
  have xf:"atom x ♯ τ" proof -
    have "supp τ ⊆ supp B" using wf_supp(4) check_branch_s_branchI  atom_dom.simps toSet.simps dom.simps by fastforce
    thus ?thesis using fresh_def x_not_in_b_set by blast
  qed

  hence "τ[x::=v]_\<tau>_v = τ" using forget_subst_v subst_v_τ_def by auto
  have "Δ[x::=v]_\<Delta>_v = Δ" using forget_subst_dv  wfD_x_fresh fresh_GNil check_branch_s_branchI by metis

  have "supp v = {}" using check_branch_s_branchI check_v_wf wfV_supp_nil by metis
  hence "supp va = {}" using ‹ va = V_cons tid cons v› v.supp pure_supp by auto

  let ?G = "(x, b_of const, [ va ]^ce == [ V_cons tid cons [ x ]^v ]^ce AND c_of const x ) #_\<Gamma> Γ"
  obtain z::x where z: "const = { z : b_of const | c_of const z } ∧ atom z ♯ (x', v,x,const,va)" 
    using obtain_fresh_z_c_of by metis

  have  vt: ‹Θ ; B ; GNil ⊨ v <== { z : b_of const | [ va ]^ce == [ V_cons tid cons [ z ]^v ]^ce AND c_of const z }›
  proof(rule infer_v_conj)
    obtain t' where t: "Θ ; B ; GNil ⊨ v ==> t' ∧ Θ ; B ; GNil ⊨ t' < const" 
      using check_v_elims check_branch_s_branchI by metis
    show "Θ ; B ; GNil ⊨ v <== { z : b_of const | [ va ]^ce == [ V_cons tid cons [ z ]^v ]^ce }"        
    proof(rule check_v_top)

      show "Θ ; B ; GNil ⊨_wf { z : b_of const | [ va ]^ce == [ V_cons tid cons [ z ]^v ]^ce } "     

      proof(rule wfG_wfT)
        show ‹ Θ ; B ⊨_wf (x, b_of const, ([ va ]^ce == [ V_cons tid cons [ z ]^v ]^ce )[z::=[ x ]^v]_cv) #_\Γ GNil ›
        proof -
          have 1: "va[z::=[ x ]^v]_vv = va" using  forget_subst_v subst_v_v_def  z fresh_prodN by metis
          moreover have 2: "Θ ; B ⊨_wf (x, b_of const, [ va ]^ce == [ V_cons tid cons [ x ]^v ]^ce AND c_of const x ) #_\<Gamma> GNil "
            using    check_branch_s_branchI(17)[THEN check_s_wf] ‹Γ = GNil› by auto      
          moreover hence "Θ ; B ⊨_wf (x, b_of const, [ va ]^ce == [ V_cons tid cons [ x ]^v ]^ce ) #_\<Gamma> GNil" 
            using wfG_conj by metis
          ultimately show ?thesis
            unfolding subst_cv.simps subst_cev.simps subst_vv.simps by auto
        qed      
        show ‹atom x ♯ ([ va ]^ce == [ V_cons tid cons [ z ]^v ]^ce )› unfolding c.fresh ce.fresh v.fresh
          apply(intro conjI )        
          using  check_branch_s_branchI fresh_at_base z freshers apply simp
          using  check_branch_s_branchI fresh_at_base z freshers apply simp
          using pure_supp apply force
          using z fresh_x_neq fresh_prod5 by metis        
      qed
      show ‹[ va ]^ce = [ V_cons tid cons [ z ]^v ]^ce[z::=v]_cev›
        using ‹ va = V_cons tid cons v› subst_cev.simps subst_vv.simps by auto
      show ‹ Θ ; B ; GNil ⊨ v <== const › using check_branch_s_branchI by auto
      show "supp [ va ]^ce ⊆ supp B" using ‹supp va = {}› ce.supp by simp
    qed
    show "Θ ; B ; GNil ⊨ v <== { z : b_of const | c_of const z }" 
      using check_branch_s_branchI z by auto
  qed

  text ‹Main body of proof for this case›
  have "Θ ; Φ ; B ; (?G)[x::=v]_\<Gamma>_v ; Δ[x::=v]_\<Delta>_v ⊨ s[x::=v]_sv <== τ[x::=v]_\<tau>_v"
  proof(rule subst_check_check_s)
    show ‹Θ ; B ; GNil ⊨ v <== { z : b_of const | [ va ]^ce == [ V_cons tid cons [ z ]^v ]^ce AND c_of const z }› using vt by auto
    show ‹atom z ♯ (x, v)› using z fresh_prodN by auto
    show ‹ Θ ; Φ ; B ; ?G ; Δ ⊨ s <== τ›
      using check_branch_s_branchI by auto

    show ‹ ?G = GNil @ (x, b_of const, ([ va ]^ce == [ V_cons tid cons [ z ]^v ]^ce AND c_of const z)[z::=[ x ]^v]_cv) #_\Γ GNil›      
    proof -
      have "va[z::=[ x ]^v]_vv = va" using  forget_subst_v subst_v_v_def  z fresh_prodN by metis
      moreover have  "(c_of const z)[z::=[ x ]^v]_cv = c_of const x" 
        using  c_of_switch[of z const x]  z fresh_prodN by metis
      ultimately show ?thesis
        unfolding subst_cv.simps subst_cev.simps subst_vv.simps append_g.simps         
        using c_of_switch[of z const x]  z fresh_prodN z fresh_prodN  check_branch_s_branchI by argo
    qed
  qed
  moreover have "s[x::=v]_sv = s'[x'::=v]_sv" 
    using check_branch_s_branchI subst_v_flip_eq_two subst_v_s_def s_branch_s_branch_list.eq_iff by metis
  ultimately show  ?case using  check_branch_s_branchI ‹τ[x::=v]_\τ_v = τ› ‹Δ[x::=v]_\Δ_v = Δ› by auto
qed(auto+)

text ‹Lemmas for while reduction. Making these separate lemmas allows flexibility in wiring them into the main proof and robustness
  we change it›

lemma check_unit:
  fixes τ::τ and Φ::Φ and Δ::Δ and G::Γ
  assumes "Θ ; {||} ; GNil ⊨ { z : B_unit | TRUE } < τ'" and "Θ ; {||} ; GNil ⊨_wf Δ"  and "Θ ⊨_wf Φ"  and "Θ ; {||} ⊨_wf G"
  shows ‹ Θ ; Φ ; {||} ; G ; Δ ⊨ [[ L_unit ]^v]^s <== τ'›
proof - 
  have *:"Θ ; {||} ; GNil ⊨ [L_unit]^v ==> { z : B_unit | [ [ z ]^v ]^ce == [ [ L_unit ]^v ]^ce }" 
    using infer_l.intros(4) infer_v_litI fresh_GNil assms  wfX_wfY   by (meson subtype_g_wf)
  moreover have "Θ ; {||} ; GNil ⊨ { z : B_unit | [ [ z ]^v ]^ce == [ [ L_unit ]^v ]^ce } < τ'" 
    using subtype_top subtype_trans * infer_v_wf 
    by (meson assms(1))
  ultimately show ?thesis (*apply(rule check_valI, auto simp add: assms,rule * )*)
    using subtype_top subtype_trans fresh_GNil assms check_valI assms check_s_g_weakening assms toSet.simps 
    by (metis bot.extremum infer_v_g_weakening subtype_weakening wfD_wf)
qed

lemma preservation_var:
  shows "Θ; Φ; {||}; GNil; Δ ⊨ VAR u : τ' = v IN s <== τ ==> Θ ⊨ δ ∼ Δ ==> atom u ♯ δ ==> atom u ♯ Δ ==>
         Θ; Φ; {||}; GNil; (u,τ')#_\<Delta>Δ ⊨ s <== τ ∧ Θ ⊨ (u,v)#δ ∼ (u,τ')#_\<Delta>Δ"
    and
    "check_branch_s Θ Φ {||} GNil Δ tid dc const v cs τ ==> True" and 
    "check_branch_list Θ Φ {||} Γ Δ tid dclist v css τ ==> True"
proof(nominal_induct  "{||}::bv fset" GNil Δ "VAR u : τ' = v IN s" τ and τ and τ  rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_varI u' Θ Φ Δ τ s')
  hence "Θ; Φ; {||}; GNil; (u, τ') #_\<Delta> Δ ⊨ s <== τ" using check_s_abs_u check_v_wf by metis

  moreover have "Θ ⊨ ((u,v)#δ) ∼ ((u,τ')#_\<Delta>Δ)" proof
    show ‹Θ ⊨ δ ∼ Δ › using check_varI by auto
    show ‹Θ ; {||} ; GNil ⊨ v <== τ'› using check_varI by auto
    show ‹u ∉ fst ` set δ› using check_varI fresh_d_fst_d by auto
  qed

  ultimately show ?case by simp
qed(auto+)

lemma check_while:
  shows "Θ; Φ; {||}; GNil; Δ ⊨ WHILE s1 DO { s2 } <== τ ==> atom x ♯ (s1, s2) ==> atom z' ♯ x ==>
       Θ; Φ; {||}; GNil; Δ ⊨ LET x : ({ z' : B_bool | TRUE }) = s1 IN (IF (V_var x) THEN (s2 ;; (WHILE s1 DO {s2}))
            ELSE ([ V_lit L_unit]^s)) <== τ" and
    "check_branch_s Θ Φ {||} GNil Δ tid dc const v cs τ ==> True" and 
    "check_branch_list Θ Φ {||} Γ Δ tid dclist v css τ ==> True"
proof(nominal_induct  "{||}::bv fset" GNil Δ "AS_while s1 s2" τ and τ and τ  avoiding: s1 s2 x z' rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_whileI Θ Φ Δ s1 z s2 τ')
  have teq:"{ z' : B_bool | TRUE } = { z : B_bool | TRUE }" using τ.eq_iff by auto

  show ?case proof
    have " atom x ♯ τ' " using wfT_nil_supp fresh_def subtype_wfT check_whileI(5) by fast
    moreover have "atom x ♯ { z' : B_bool | TRUE } " using τ.fresh c.fresh b.fresh by metis  
    ultimately show ‹atom x ♯ (Θ, Φ, {||}, GNil, Δ, { z' : B_bool | TRUE }, s1, τ')›
      apply(unfold fresh_prodN)  
      using check_whileI  wb_x_fresh check_s_wf wfD_x_fresh fresh_empty_fset fresh_GNil fresh_Pair ‹atom x ♯ τ'›  by metis

    show ‹ Θ ; Φ ; {||} ; GNil ; Δ ⊨ s1 <== { z' : B_bool | TRUE }› using check_whileI  teq by metis

    let ?G =  "(x, b_of { z' : B_bool | TRUE }, c_of { z' : B_bool | TRUE } x) #_\<Gamma> GNil"

    have cof:"(c_of { z' : B_bool | TRUE } x) = C_true" using c_of.simps check_whileI subst_cv.simps by metis
    have  wfg: "Θ ; {||} ⊨_wf ?G" proof 
      show "c_of { z' : B_bool | TRUE } x ∈ {TRUE, FALSE}" using subst_cv.simps cof by auto
      show "Θ ; {||} ⊨_wf GNil " using wfG_nilI check_whileI wfX_wfY check_s_wf by metis
      show "atom x ♯ GNil" using fresh_GNil by auto
      show "Θ ; {||} ⊨_wf b_of { z' : B_bool | TRUE } " using wfB_boolI wfX_wfY check_s_wf b_of.simps 
        by (metis ‹Θ ; {||} ⊨_wf GNil›)
    qed

    obtain zz::x where zf:‹atom zz ♯ ((Θ, Φ, {||}::bv fset, ?G , Δ, [ x ]^v,
 AS_seq s2 (AS_while s1 s2), AS_val [ L_unit ]^v, τ'),x,?G)›
      using obtain_fresh by blast
    show ‹ Θ ; Φ ; {||} ; ?G ; Δ ⊨
 AS_if [ x ]^v (AS_seq s2 (AS_while s1 s2)) (AS_val [ L_unit ]^v) <== τ'›
    proof      
      show "atom zz ♯ (Θ, Φ, {||}::bv fset, ?G , Δ, [ x ]^v, AS_seq s2 (AS_while s1 s2), AS_val [ L_unit ]^v, τ')" using zf by auto
      show ‹Θ ; {||} ; ?G ⊨ [ x ]^v <== { zz : B_bool | TRUE }› proof
        have "atom zz ♯ x ∧ atom zz ♯ (Θ, {||}::bv fset, ?G)" using zf fresh_prodN by metis
        thus ‹ Θ ; {||} ; ?G ⊨ [ x ]^v ==>{ zz : B_bool | [[zz]^v]^ce == [[ x ]^v]^ce }›
          using infer_v_varI lookup.simps wfg b_of.simps by metis
        thus  ‹Θ ; {||} ; ?G ⊨ { zz : B_bool | [[ zz ]^v]^ce == [[ x ]^v]^ce } < { zz : B_bool | TRUE }›
          using subtype_top infer_v_wf by metis
      qed 
      show ‹ Θ ; Φ ; {||} ; ?G ; Δ ⊨ AS_seq s2 (AS_while s1 s2) <== { zz : b_of τ' | [ [ x ]^v ]^ce == [ [ L_true ]^v ]^ce IMP c_of τ' zz }›
      proof 
        have "{ zz : B_unit | TRUE } = { z : B_unit | TRUE }" using τ.eq_iff by auto 
        thus ‹ Θ ; Φ ; {||} ; ?G ; Δ ⊨ s2 <== { zz : B_unit | TRUE }› using check_s_g_weakening(1) [OF check_whileI(3) _ wfg] toSet.simps 
          by (simp add: ‹{ zz : B_unit | TRUE } = { z : B_unit | TRUE }›)

        show ‹ Θ ; Φ ; {||} ; ?G ; Δ ⊨ AS_while s1 s2 <== { zz : b_of τ' | [ [ x ]^v ]^ce == [ [ L_true ]^v ]^ce IMP c_of τ' zz }›
        proof(rule check_s_supertype(1))
          have ‹ Θ; Φ; {||}; GNil; Δ ⊨ AS_while s1 s2 <== τ'› using  check_whileI by auto
          thus *:‹ Θ ; Φ ; {||} ; ?G ; Δ ⊨ AS_while s1 s2 <== τ' › using  check_s_g_weakening(1)[OF _ _ wfg] toSet.simps by auto

          show ‹Θ ; {||} ; ?G ⊨ τ' < { zz : b_of τ' | [ [ x ]^v ]^ce == [ [ L_true ]^v ]^ce IMP c_of τ' zz }›
          proof(rule subtype_eq_if_τ)
            show ‹ Θ ; {||} ; ?G ⊨_wf τ' › using * check_s_wf by auto
            show ‹ Θ ; {||} ; ?G ⊨_wf { zz : b_of τ' | [ [ x ]^v ]^ce == [ [ L_true ]^v ]^ce IMP c_of τ' zz } ›
              apply(rule wfT_eq_imp, simp add: base_for_lit.simps)
              using subtype_wf check_whileI wfg zf fresh_prodN by metis+
            show ‹atom zz ♯ τ'› using  zf fresh_prodN by metis
          qed
        qed

      qed
      show ‹ Θ ; Φ ; {||} ; ?G ; Δ ⊨ AS_val [ L_unit ]^v <== { zz : b_of τ' | [ [ x ]^v ]^ce == [ [ L_false ]^v ]^ce IMP c_of τ' zz }›
      proof(rule check_s_supertype(1))

        show *:‹ Θ ; Φ ; {||} ; ?G ; Δ ⊨ AS_val [ L_unit ]^v <== τ'›
          using check_unit[OF check_whileI(5) _ _ wfg] using check_whileI wfg wfX_wfY check_s_wf by metis
        show ‹Θ ; {||} ; ?G ⊨ τ' < { zz : b_of τ' | [ [ x ]^v ]^ce == [ [ L_false ]^v ]^ce IMP c_of τ' zz }›
        proof(rule subtype_eq_if_τ)
          show ‹ Θ ; {||} ; ?G ⊨_wf τ' › using * check_s_wf by metis
          show ‹ Θ ; {||} ; ?G ⊨_wf { zz : b_of τ' | [ [ x ]^v ]^ce == [ [ L_false ]^v ]^ce IMP c_of τ' zz } ›                          
            apply(rule wfT_eq_imp, simp add: base_for_lit.simps)
            using subtype_wf check_whileI wfg zf fresh_prodN by metis+
          show ‹atom zz ♯ τ'› using  zf fresh_prodN by metis
        qed
      qed
    qed
  qed
qed(auto+)

lemma check_s_narrow:
  fixes s::s and x::x
  assumes "atom x ♯ (Θ, Φ, B, Γ, Δ, c, τ, s)" and "Θ ; Φ ; B ; (x, B_bool, c) #_\<Gamma> Γ ; Δ ⊨ s <== τ" and    
    "Θ ; B ; Γ ⊨ c "
  shows "Θ ; Φ ; B ; Γ ; Δ ⊨ s <== τ"
proof -
  let ?B = "({||}::bv fset)"
  let ?v = "V_lit L_true"

  obtain z::x where z: "atom z ♯ (x, [ L_true ]^v,c)" using obtain_fresh by metis

  have "atom z ♯ c" using z fresh_prodN by auto
  hence c:" c[x::=[ z ]^v]_v[z::=[ x ]^v]_cv = c" using  subst_v_c_def by simp

  have "Θ ; Φ ; B ; ((x,B_bool, c) #_\<Gamma> Γ)[x::=?v]_\<Gamma>_v ; Δ[x::=?v]_\<Delta>_v ⊨ s[x::=?v]_sv <== τ[x::=?v]_\<tau>_v" proof(rule  subst_infer_check_s(1) )
    show vt: ‹ Θ ; B ; Γ ⊨ [ L_true ]^v ==> { z : B_bool | (CE_val (V_var z)) == (CE_val (V_lit L_true )) } ›
      using infer_v_litI check_s_wf wfG_elims(2) infer_trueI assms by metis     
    show ‹Θ ; B ; Γ ⊨ { z : B_bool | (CE_val (V_var z)) == (CE_val (V_lit L_true )) } < { z : B_bool | c[x::=[ z ]^v]_v }› proof
      show ‹atom x ♯ (Θ, B, Γ, z, [ [ z ]^v ]^ce == [ [ L_true ]^v ]^ce , z, c[x::=[ z ]^v]_v)›
        apply(unfold fresh_prodN, intro conjI) 
        prefer 5
        using c.fresh ce.fresh v.fresh z fresh_prodN apply auto[1]
        prefer 6
        using fresh_subst_v_if[of "atom x" c x] assms fresh_prodN apply simp
        using z assms fresh_prodN apply metis
        using z  assms fresh_prodN apply metis
        using z assms  fresh_prodN apply metis
        using z fresh_prodN assms fresh_at_base by metis+
      show ‹ Θ ; B ; Γ ⊨_wf { z : B_bool | [ [ z ]^v ]^ce == [ [ L_true ]^v ]^ce } › using vt infer_v_wf by simp
      show ‹ Θ ; B ; Γ ⊨_wf { z : B_bool | c[x::=[ z ]^v]_v } › proof(rule wfG_wfT)    
        show ‹ Θ ; B ⊨_wf (x, B_bool, c[x::=[ z ]^v]_v[z::=[ x ]^v]_cv) #_\Γ Γ › using c check_s_wf assms by metis
        have " atom x ♯ [ z ]^v" using v.fresh z fresh_at_base by auto
        thus  ‹atom x ♯ c[x::=[ z ]^v]_v› using fresh_subst_v_if[of "atom x" c ] by auto
      qed
      have wfg: "Θ ; B ⊨_wf(x, B_bool, ([ [ z ]^v ]^ce == [ [ L_true ]^v ]^ce )[z::=[ x ]^v]_v) #_\<Gamma> Γ" 
        using wfT_wfG vt infer_v_wf fresh_prodN assms by simp
      show  ‹Θ ; B ; (x, B_bool, ([ [ z ]^v ]^ce == [ [ L_true ]^v ]^ce )[z::=[ x ]^v]_v) #_\Γ Γ ⊨ c[x::=[ z ]^v]_v[z::=[ x ]^v]_v ›
        using c valid_weakening[OF assms(3) _ wfg ] toSet.simps 
        using subst_v_c_def by auto
    qed
    show ‹atom z ♯ (x, [ L_true ]^v)› using z fresh_prodN by metis
    show ‹ Θ ; Φ ; B ; (x, B_bool, c) #_\Γ Γ ; Δ ⊨ s <== τ› using assms by auto

    thus ‹(x, B_bool, c) #_\Γ Γ = GNil @ (x, B_bool, c[x::=[ z ]^v]_v[z::=[ x ]^v]_cv) #_\Γ Γ› using append_g.simps c by auto
  qed

  moreover have "((x,B_bool, c) #_\<Gamma> Γ)[x::=?v]_\<Gamma>_v = Γ " using subst_gv.simps by auto
  ultimately show ?thesis using assms forget_subst_dv forget_subst_sv forget_subst_tv fresh_prodN  by metis
qed

lemma check_assert_s:
  fixes s::s and x::x
  assumes "Θ; Φ; {||}; GNil; Δ ⊨ AS_assert c s <== τ"
  shows "Θ; Φ; {||}; GNil; Δ ⊨ s <== τ ∧ Θ ; {||} ; GNil ⊨ c "
proof -
  let ?B = "({||}::bv fset)"
  let ?v = "V_lit L_true"

  obtain x where x: "Θ ; Φ ; ?B ; (x,B_bool, c) #_\<Gamma> GNil ; Δ ⊨ s <== τ ∧ atom x ♯ (Θ, Φ, ?B, GNil, Δ, c, τ, s ) ∧ Θ ; ?B ; GNil ⊨ c " 
    using check_s_elims(10)[OF ‹Θ ; Φ ; ?B ; GNil ; Δ ⊨ AS_assert c s <== τ›] valid.simps by metis

  show ?thesis using assms check_s_narrow x by metis
qed

lemma infer_v_pair2I:
  "atom z ♯ (v1, v2) ==>
   atom z ♯ (Θ, B, Γ) ==>
   Θ ; B ; Γ ⊨ v1 ==> t1 ==>
   Θ ; B ; Γ ⊨ v2 ==> t2 ==>
   b1 = b_of t1 ==> b2 = b_of t2 ==>
  Θ ; B ; Γ ⊨ [ v1 , v2 ]^v ==> { z : [ b1 , b2 ]^b | [ [ z ]^v ]^ce == [ [ v1 , v2 ]^v ]^ce }"
  using infer_v_pairI by simp

subsection ‹Main Lemma›

lemma preservation: 
  assumes "Φ ⊨ ⟨δ, s⟩ ⟶ ⟨δ', s'⟩" and "Θ; Φ; Δ ⊨ ⟨δ, s⟩ <== τ"
  shows "∃Δ'. Θ; Φ; Δ' ⊨ ⟨δ', s'⟩ <== τ ∧ Δ ⊑ Δ'" 
  using assms 
proof(induct arbitrary: τ rule: reduce_stmt.induct)
  case (reduce_let_plusI δ x n1 n2 s')
  then show ?case using preservation_plus
    by (metis order_refl)  
next
  case (reduce_let_leqI b n1 n2 δ x s) 
  then show ?case using preservation_leq  by (metis order_refl)  
next
  case (reduce_let_eqI b n1 n2 Φ δ x s)
  then show ?case using preservation_eq[OF reduce_let_eqI(2)] order_refl by metis
next
  case (reduce_let_appI f z b c τ' s' Φ δ x v s)
  hence tt: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_app f v) s <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" using config_type_elims[OF reduce_let_appI(2)] by metis 
  hence *:"Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_app f v) s <== τ" by auto

  hence  "Θ; Φ; {||}; GNil; Δ ⊨ AS_let2 x (τ'[z::=v]_\<tau>_v) (s'[z::=v]_sv) s <== τ" 
    using preservation_app reduce_let_appI tt by auto

  hence "Θ; Φ; Δ ⊨ ⟨ δ , AS_let2 x (τ'[z::=v]_\<tau>_v) s'[z::=v]_sv s ⟩ <== τ"  using  config_typeI tt by auto
  then show ?case using tt order_refl reduce_let_appI by metis

next
  case (reduce_let_appPI f bv z b c τ' s' Φ δ x b' v s)

  hence tt: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_appP f b' v) s <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" using config_type_elims[OF reduce_let_appPI(2)] by metis 
  hence *:"Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_appP f b' v) s <== τ" by auto

  have  "Θ; Φ; {||}; GNil; Δ ⊨ AS_let2 x (τ'[bv::=b']_\<tau>_b[z::=v]_\<tau>_v) (s'[bv::=b']_sb[z::=v]_sv) s <== τ" 
  proof(rule preservation_poly_app) 
    show ‹Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ z b c τ' s'))) = lookup_fun Φ f› using reduce_let_appPI by metis
    show ‹∀fd∈set Φ. check_fundef Θ Φ fd› using tt lookup_fun_member by metis
    show ‹ Θ ; Φ ;{||} ; GNil ; Δ ⊨ AS_let x (AE_appP f b' v) s <== τ› using * by auto
    show ‹ Θ ; {||} ⊨_wf b' › using check_s_elims infer_e_wf wfE_elims * by metis
  qed(auto+)

  hence "Θ; Φ; Δ ⊨ ⟨ δ , AS_let2 x (τ'[bv::=b']_\<tau>_b[z::=v]_\<tau>_v) s'[bv::=b']_sb[z::=v]_sv s ⟩ <== τ"  using  config_typeI tt by auto
  then show ?case using tt order_refl reduce_let_appI by metis

next
  case (reduce_if_trueI δ s1 s2) 
  then show ?case using preservation_if by metis
next
  case (reduce_if_falseI uw δ s1 s2)
  then show ?case using preservation_if by metis
next
  case (reduce_let_valI δ x v s)
  then show ?case using preservation_let_val by presburger
next
  case (reduce_let_mvar u v δ Φ  x s)
  hence *:"Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_mvar u) s <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by blast

  hence **: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_mvar u) s <== τ" by auto
  obtain xa::x and za::x and ca::c and ba::b and sa::s where
    sa1: "atom xa ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, AE_mvar u, τ) ∧ atom za ♯ (xa, Θ, Φ, {||}::bv fset, GNil, Δ, AE_mvar u, τ, sa) ∧
     Θ; Φ; {||}; GNil; Δ ⊨ AE_mvar u ==> { za : ba | ca } ∧
     Θ ; Φ ; {||} ; (xa, ba, ca[za::=V_var xa]_cv) #_\<Gamma> GNil ; Δ ⊨ sa <== τ ∧
       (∀c. atom c ♯ (s, sa) ⟶ atom c ♯ (x, xa, s, sa) ⟶ (x ↔ c) ∙ s = (xa ↔ c) ∙ sa)" 
    using check_s_elims(2)[OF **] subst_defs by metis

  have "Θ ; {||} ; GNil ⊨ v <== { za : ba | ca }" proof -
    have " (u , { za : ba | ca }) ∈ setD Δ" using infer_e_elims(11) sa1 by fast
    thus  ?thesis using delta_sim_v reduce_let_mvar config_type_elims check_s_wf  by metis
  qed

  then obtain τ' where  vst: "Θ ; {||} ; GNil ⊨ v ==> τ' ∧
        Θ ; {||} ; GNil ⊨ τ' < { za : ba | ca }" using check_v_elims by blast

  obtain za2 and ba2 and ca2 where  zbc: "τ' = ({ za2 : ba2 | ca2 }) ∧ atom za2 ♯ (xa, (xa, Θ, Φ, {||}::bv fset, GNil, Δ, AE_val v, τ, sa))"
    using obtain_fresh_z by blast
  have beq: "ba=ba2" using subtype_eq_base vst zbc by blast

  moreover have xaf: "atom xa ♯ (za, za2)" 
    apply(unfold fresh_prodN, intro conjI)
    using sa1 zbc fresh_prodN fresh_x_neq by metis+

  have sat2: " Θ ; Φ ; {||} ; GNil@(xa, ba, ca2[za2::=V_var xa]_cv) #_\<Gamma> GNil ; Δ ⊨ sa <== τ" proof(rule ctx_subtype_s)
    show "Θ ; Φ ; {||} ; GNil @ (xa, ba, ca[za::=V_var xa]_cv) #_\<Gamma> GNil ; Δ ⊨ sa <== τ" using sa1 by auto
    show "Θ ; {||} ; GNil ⊨ { za2 : ba | ca2 } < { za : ba | ca }" using beq zbc vst by fast
    show "atom xa ♯ (za, za2, ca, ca2)" proof -
      have *:"Θ ; {||} ; GNil ⊨_wf ({ za2 : ba2 | ca2 }) " using zbc vst subtype_wf by auto
      hence "supp ca2 ⊆ { atom za2 }" using wfT_supp_c[OF *] supp_GNil by simp
      moreover have "atom za2 ♯ xa" using zbc fresh_Pair fresh_x_neq by metis
      ultimately have  "atom xa ♯ ca2" using zbc supp_at_base fresh_def 
        by (metis empty_iff singleton_iff subset_singletonD)
      moreover have "atom xa ♯ ca" proof -
        have *:"Θ ; {||} ; GNil ⊨_wf ({ za : ba | ca }) " using zbc vst subtype_wf by auto
        hence "supp ca ⊆ { atom za }" using wfT_supp τ.supp by force
        moreover have "xa ≠ za"  using   fresh_def fresh_x_neq xaf fresh_Pair by metis
        ultimately show ?thesis using fresh_def by auto
      qed
      ultimately show ?thesis using xaf sa1 fresh_prod4 fresh_Pair by metis
    qed
  qed
  hence dwf: "Θ ; {||} ; GNil ⊨_wf Δ" using sa1 infer_e_wf by meson

  have "Θ; Φ; {||}; GNil; Δ ⊨ AS_let xa (AE_val v) sa <== τ" proof 
    have "atom xa ♯ (AE_val v)" using infer_v_wf(1) wfV_supp fresh_def e.fresh x_not_in_b_set vst by fastforce
    thus  "atom xa ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, AE_val v, τ)" using sa1 freshers by simp 
    have "atom za2 ♯ (AE_val v)" using infer_v_wf(1) wfV_supp fresh_def e.fresh x_not_in_b_set vst by fastforce
    thus "atom za2 ♯ (xa, Θ, Φ, {||}::bv fset, GNil, Δ, AE_val v, τ, sa)" using zbc freshers fresh_prodN by auto
    have " Θ ⊨_wf Φ" using sa1 infer_e_wf by auto
    thus  "Θ; Φ; {||}; GNil; Δ ⊨ AE_val v ==> { za2 : ba | ca2 }" 
      using zbc vst beq dwf infer_e_valI by blast
    show "Θ ; Φ ; {||} ; (xa, ba, ca2[za2::=V_var xa]_v) #_\<Gamma> GNil ; Δ ⊨ sa <== τ" using sat2 append_g.simps subst_defs by metis
  qed
  moreover have  "AS_let xa (AE_val v) sa = AS_let x (AE_val v) s" proof -
    have "[[atom x]]lst. s = [[atom xa]]lst. sa" 
      using sa1 Abs1_eq_iff_all(3)[where z=" (s, sa)"] by metis
    thus ?thesis using s_branch_s_branch_list.eq_iff(2) by metis
  qed
  ultimately have "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_val v) s <== τ"  by auto

  then show ?case using reduce_let_mvar * config_typeI
    by (meson order_refl)
next
  case (reduce_let2I Φ δ s1 δ' s1'  x t s2)
  hence **: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let2 x t s1 s2 <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" using config_type_elims[OF reduce_let2I(3)] by blast
  hence *:"Θ; Φ; {||}; GNil; Δ ⊨ AS_let2 x t s1 s2 <== τ" by auto

  obtain xa::x and  z::x and c and b and s2a::s where st: "atom xa ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, t, s1, τ) ∧
       Θ; Φ; {||}; GNil; Δ ⊨ s1 <== t ∧
       Θ ; Φ ; {||} ; (xa, b_of t, c_of t xa) #_\<Gamma> GNil ; Δ ⊨ s2a <== τ ∧ ([[atom x]]lst. s2 = [[atom xa]]lst. s2a) "
    using check_s_elims(4)[OF *] Abs1_eq_iff_all(3) by metis

  hence "Θ; Φ; Δ ⊨ ⟨ δ , s1 ⟩ <== t"  using config_typeI ** by auto
  then obtain Δ' where s1r: "Θ; Φ; Δ' ⊨ ⟨ δ' , s1' ⟩ <== t ∧ Δ ⊑ Δ'" using reduce_let2I by presburger

  have  "Θ; Φ; {||}; GNil; Δ' ⊨ AS_let2 xa t s1' s2a <== τ" 
  proof(rule check_let2I)
    show *:"Θ; Φ; {||}; GNil; Δ' ⊨ s1' <== t" using config_type_elims st s1r by metis
    show  "atom xa ♯ (Θ, Φ, {||}::bv fset, GNil, Δ',t, s1', τ)" proof -  
      have "atom xa ♯ s1'" using  check_s_x_fresh *  by auto
      moreover have "atom xa ♯ Δ'" using check_s_x_fresh * by auto
      ultimately show ?thesis  using st fresh_prodN by metis
    qed

    show "Θ ; Φ ; {||} ; (xa, b_of t, c_of t xa) #_\<Gamma> GNil ; Δ' ⊨ s2a <== τ"  proof -
      have "Θ ; {||} ; GNil ⊨_wf Δ'" using * check_s_wf by auto
      moreover have "Θ ; {||} ⊨_wf ((xa, b_of t, c_of t xa) #_\<Gamma> GNil)" using st check_s_wf by auto
      ultimately have "Θ ; {||} ; ((xa, b_of t , c_of t xa) #_\<Gamma> GNil) ⊨_wf Δ'" using wf_weakening by auto
      thus  ?thesis using check_s_d_weakening check_s_wf st  s1r by metis
    qed
  qed
  moreover have "AS_let2 xa t s1' s2a = AS_let2 x t s1' s2"  using st s_branch_s_branch_list.eq_iff by metis
  ultimately have "Θ; Φ; {||}; GNil; Δ' ⊨ AS_let2 x t s1' s2 <== τ" using st by argo
  moreover have "Θ ⊨ δ' ∼ Δ'" using config_type_elims s1r by fast
  ultimately show ?case using config_typeI **
    by (meson s1r)
next
  case (reduce_let2_valI vb δ x t v s)
  then show ?case using preservation_let_val by meson
next
  case (reduce_varI u δ Φ τ' v s)

  hence ** : "Θ; Φ; {||}; GNil; Δ ⊨ AS_var u τ' v s <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by meson
  have uf: "atom u ♯ Δ" using reduce_varI delta_sim_fresh by force  
  hence *: "Θ; Φ; {||}; GNil; Δ ⊨ AS_var u τ' v s <== τ" and " Θ ⊨ δ ∼ Δ" using **  by auto

  thus ?case using preservation_var reduce_varI config_typeI ** set_subset_Cons
      setD_ConsD subsetI  by (metis delta_sim_fresh)

next
  case (reduce_assignI Φ δ u v )
  hence *: "Θ; Φ; {||}; GNil; Δ ⊨ AS_assign u v <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by meson
  then obtain z and τ' where zt: "Θ ; {||} ; GNil ⊨ ({ z : B_unit | TRUE }) < τ ∧ (u,τ') ∈ setD Δ ∧ Θ ; {||} ; GNil ⊨ v <== τ' ∧ Θ ; {||} ; GNil ⊨_wf Δ" 
    using check_s_elims(8) by metis
  hence "Θ ⊨ update_d δ u v ∼ Δ" using update_d_sim  * by metis
  moreover have "Θ; Φ; {||}; GNil; Δ ⊨ AS_val (V_lit L_unit ) <== τ" using zt * check_s_v_unit check_s_wf
    by auto
  ultimately show ?case using config_typeI * by (meson order_refl)
next
  case (reduce_seq1I Φ δ s)
  hence "Θ ; Φ ; {||} ; GNil ; Δ ⊨ s <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using check_s_elims config_type_elims by force
  then show ?case  using config_typeI by blast
next
  case (reduce_seq2I s1 v Φ δ δ' s1' s2)
  hence tt: "Θ; Φ; {||}; GNil; Δ ⊨ AS_seq s1 s2 <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by blast
  then obtain z where zz: "Θ ; Φ ; {||} ; GNil; Δ ⊨ s1 <== ({ z : B_unit | TRUE }) ∧ Θ; Φ; {||}; GNil; Δ ⊨ s2 <== τ" 
    using check_s_elims by blast
  hence "Θ; Φ; Δ ⊨ ⟨ δ , s1 ⟩ <== ({ z : B_unit | TRUE })" 
    using tt config_typeI tt by simp 
  then obtain Δ' where *: "Θ; Φ; Δ' ⊨ ⟨ δ' , s1' ⟩ <== ({ z : B_unit | TRUE }) ∧ Δ ⊑ Δ'" 
    using reduce_seq2I by meson
  moreover hence  s't: "Θ; Φ; {||}; GNil; Δ' ⊨ s1' <== ({ z : B_unit | TRUE }) ∧ Θ ⊨ δ' ∼ Δ'" 
    using config_type_elims by force
  moreover hence "Θ ; {||} ; GNil ⊨_wf Δ'" using check_s_wf by meson
  moreover hence  "Θ; Φ; {||}; GNil; Δ' ⊨ s2 <== τ" 
    using calculation(1) zz check_s_d_weakening * by metis
  moreover hence  "Θ; Φ; {||}; GNil; Δ' ⊨ (AS_seq s1' s2) <== τ" 
    using check_seqI zz s't by meson 
  ultimately have  "Θ; Φ; Δ' ⊨ ⟨ δ' , AS_seq s1' s2 ⟩ <== τ ∧ Δ ⊑ Δ'"
    using zz config_typeI tt  by meson
  then show ?case by meson
next
  case (reduce_whileI x  s1 s2 z' Φ δ )

  hence *: "Θ; Φ; {||}; GNil; Δ ⊨ AS_while s1 s2 <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by meson

  hence  **:"Θ; Φ; {||}; GNil; Δ ⊨ AS_while s1 s2 <== τ" by auto
  hence "Θ; Φ; {||}; GNil; Δ ⊨ AS_let2 x ({ z' : B_bool | TRUE }) s1 (AS_if (V_var x) (AS_seq s2 (AS_while s1 s2)) (AS_val (V_lit L_unit)) ) <== τ"
    using check_while reduce_whileI by auto
  thus ?case  using config_typeI *   by (meson subset_refl)

next
  case (reduce_caseI dc x' s' css Φ δ tyid  v)

  hence **: "Θ; Φ; {||}; GNil; Δ ⊨ AS_match (V_cons tyid dc v) css <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)"
    using config_type_elims[OF reduce_caseI(2)] by metis
  hence ***: "Θ; Φ; {||}; GNil; Δ ⊨ AS_match (V_cons tyid dc v) css <== τ" by auto

  let ?vcons = "V_cons tyid dc v"

  obtain dclist tid  and z::x where cv:  "Θ; {||} ; GNil ⊨ (V_cons tyid dc v) <== ({ z : B_id tid | TRUE }) ∧
    Θ; Φ; {||}; GNil; Δ ; tid ; dclist ; (V_cons tyid dc v) ⊨ css <== τ ∧ AF_typedef tid dclist ∈ set Θ ∧
 Θ ; {||} ; GNil ⊨ V_cons tyid dc v <== { z : B_id tid | TRUE }"
    using check_s_elims(9)[OF ***] by metis

  hence vi:" Θ ; {||} ; GNil ⊨ V_cons tyid dc v <== { z : B_id tid | TRUE }" by auto
  obtain tcons where vi2:" Θ ; {||} ; GNil ⊨ V_cons tyid dc v ==> tcons ∧ Θ ; {||} ; GNil ⊨ tcons < { z : B_id tid | TRUE }" 
    using check_v_elims(1)[OF vi] by metis
  hence vi1: "Θ ; {||} ; GNil ⊨ V_cons tyid dc v ==> tcons" by auto

  show ?case proof(rule infer_v_elims(4)[OF vi1],goal_cases)
    case (1 dclist2 tc tv z2)
    have "tyid = tid" using τ.eq_iff using subtype_eq_base vi2 1 by fastforce 
    hence deq:"dclist = dclist2"  using check_v_wf wfX_wfY cv 1  wfTh_dclist_unique by metis
    have "Θ; Φ; {||}; GNil; Δ ⊨ s'[x'::=v]_sv <== τ" proof(rule check_match(3))     
      show ‹ Θ ; Φ ; {||} ; GNil ; Δ ; tyid ; dclist ; ?vcons ⊨ css <== τ› using ‹tyid = tid› cv by auto
      show "distinct (map fst dclist)" using wfTh_dclist_distinct check_v_wf wfX_wfY cv by metis
      show ‹?vcons = V_cons tyid dc v› by auto
      show ‹{||} = {||}› by auto
      show ‹(dc, tc) ∈ set dclist› using 1 deq by auto
      show ‹GNil = GNil› by auto
      show ‹Some (AS_branch dc x' s') = lookup_branch dc css› using reduce_caseI by auto
      show ‹Θ ; {||} ; GNil ⊨ v <== tc› using 1 check_v.intros by auto
    qed
    thus  ?case using config_typeI ** by blast
  qed

next
  case (reduce_let_fstI Φ δ x v1 v2 s)
  thus ?case using preservation_fst_snd order_refl by metis
next
  case (reduce_let_sndI  Φ δ x v1 v2 s)
  thus ?case using preservation_fst_snd order_refl by metis
next
  case (reduce_let_concatI Φ δ x v1 v2 s)
  hence elim: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))) s <== τ ∧
                  Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by metis

  obtain z::x where z: "atom z ♯ (AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2)), GNil, CE_val (V_lit (L_bitvec (v1 @ v2))))" 
    using obtain_fresh by metis

  have "Θ ; {||} ⊨_wf GNil" using check_s_wf elim by auto

  have "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_val (V_lit (L_bitvec (v1 @ v2)))) s <== τ" proof(rule subtype_let)
    show ‹ Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))) s <== τ› using elim by auto
    show ‹Θ; Φ; {||}; GNil; Δ ⊨ (AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))) ==> { z : B_bitvec | CE_val (V_var z) == (CE_concat ([V_lit (L_bitvec v1)]^ce) ([V_lit (L_bitvec v2)]^ce))} ›
      (is "Θ; Φ; {||}; GNil; Δ ⊨ ?e1 ==> ?t1")
    proof
      show ‹ Θ ; {||} ; GNil ⊨_wf Δ › using check_s_wf elim by auto
      show ‹ Θ ⊨_wf Φ › using check_s_wf elim by auto
      show ‹ Θ ; {||} ; GNil ⊨ V_lit (L_bitvec v1) ==> { z : B_bitvec | CE_val (V_var z) == CE_val (V_lit (L_bitvec v1)) }›
        using infer_v_litI infer_l.intros  ‹Θ ; {||} ⊨_wf GNil›  fresh_GNil by auto
      show ‹ Θ ; {||} ; GNil ⊨ V_lit (L_bitvec v2) ==> { z : B_bitvec | CE_val (V_var z) == CE_val (V_lit (L_bitvec v2)) }›
        using infer_v_litI infer_l.intros  ‹Θ ; {||} ⊨_wf GNil›  fresh_GNil by auto
      show ‹atom z ♯ AE_concat (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))› using z fresh_Pair by metis
      show ‹atom z ♯ GNil› using z fresh_Pair by auto
    qed
    show ‹Θ; Φ; {||}; GNil; Δ ⊨ AE_val (V_lit (L_bitvec (v1 @ v2))) ==> { z : B_bitvec | CE_val (V_var z) == CE_val (V_lit (L_bitvec (v1 @ v2))) } ›
      (is "Θ; Φ; {||}; GNil; Δ ⊨ ?e2 ==> ?t2")
      using infer_e_valI infer_v_litI infer_l.intros  ‹Θ ; {||} ⊨_wf GNil›  fresh_GNil check_s_wf elim by metis
    show ‹Θ ; {||} ; GNil ⊨ ?t2 < ?t1› using subtype_concat check_s_wf elim by auto
  qed

  thus ?case  using config_typeI elim by (meson order_refl)
next
  case (reduce_let_lenI Φ δ x v s)
  hence elim: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_len (V_lit (L_bitvec v))) s <== τ ∧ Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using check_s_elims config_type_elims by metis

  then obtain t where t: "Θ; Φ; {||}; GNil; Δ ⊨ AE_len (V_lit (L_bitvec v)) ==> t"   using check_s_elims by meson

  moreover then obtain z::x where  "t = { z : B_int | CE_val (V_var z) == CE_len ([V_lit (L_bitvec v)]^ce) }" using infer_e_elims by meson 

  moreover obtain z'::x where "atom z' ♯ v" using obtain_fresh by metis
  moreover have  "Θ; Φ; {||}; GNil; Δ ⊨ AE_val (V_lit (L_num (int (length v)))) ==> { z' : B_int | CE_val (V_var z') == CE_val (V_lit (L_num (int (length v)))) }" 
    using infer_e_valI infer_v_litI infer_l.intros(3)  t  check_s_wf elim 
    by (metis infer_l_form2 type_for_lit.simps(3))

  moreover have "Θ ; {||} ; GNil ⊨ { z' : B_int | CE_val (V_var z') == CE_val (V_lit (L_num (int (length v)))) } <
                           { z : B_int | CE_val (V_var z) == CE_len [(V_lit (L_bitvec v))]^ce }" using subtype_len check_s_wf elim by auto

  ultimately have "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_val (V_lit (L_num (int (length v))))) s <== τ" using subtype_let by (meson elim)
  thus ?case  using config_typeI elim by (meson order_refl)
next
  case (reduce_let_splitI n v v1 v2 Φ δ x s)
  hence elim: "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_split (V_lit (L_bitvec v)) (V_lit (L_num n))) s <== τ ∧
                  Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by metis

  obtain z::x where z: "atom z ♯ (AE_split (V_lit (L_bitvec v)) (V_lit (L_num n)), GNil, CE_val (V_lit (L_bitvec (v1 @ v2))),
([ L_bitvec v1 ]^v, [ L_bitvec v2 ]^v), Θ, {||}::bv fset)" 
    using obtain_fresh by metis

  have *:"Θ ; {||} ⊨_wf GNil" using check_s_wf elim by auto

  have "Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_val (V_pair (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2)))) s <== τ" proof(rule subtype_let)

    show ‹ Θ; Φ; {||}; GNil; Δ ⊨ AS_let x (AE_split (V_lit (L_bitvec v)) (V_lit (L_num n))) s <== τ› using elim by auto
    show ‹Θ; Φ; {||}; GNil; Δ ⊨ (AE_split (V_lit (L_bitvec v)) (V_lit (L_num n))) ==> { z : B_pair B_bitvec B_bitvec
 | ((CE_val (V_lit (L_bitvec v))) == (CE_concat (CE_fst (CE_val (V_var z))) (CE_snd (CE_val (V_var z)))))
 AND (((CE_len (CE_fst (CE_val (V_var z))))) == (CE_val (V_lit (L_num n)))) } ›
      (is "Θ; Φ; {||}; GNil; Δ ⊨ ?e1 ==> ?t1") 
    proof
      show ‹ Θ ; {||} ; GNil ⊨_wf Δ › using check_s_wf elim by auto
      show ‹ Θ ⊨_wf Φ › using check_s_wf elim by auto
      show ‹ Θ ; {||} ; GNil ⊨ V_lit (L_bitvec v) ==> { z : B_bitvec | CE_val (V_var z) == CE_val (V_lit (L_bitvec v)) }›
        using infer_v_litI infer_l.intros  ‹Θ ; {||} ⊨_wf GNil›  fresh_GNil by auto
      show "Θ ; {||} ; GNil ⊨ ([ L_num
                           n ]^v) <== { z : B_int | (([ leq [ [ L_num 0 ]^v ]^ce [ [ z ]^v ]^ce ]^ce) == ([ [ L_true ]^v ]^ce)) AND [ leq [ [ z ]^v ]^ce [| [ [ L_bitvec
                   v ]^v ]^ce |]^ce ]^ce == [ [ L_true ]^v ]^ce }" using split_n  reduce_let_splitI check_v_num_leq * wfX_wfY  by metis
      show ‹atom z ♯ AE_split [ L_bitvec v ]^v [ L_num n ]^v› using z fresh_Pair by auto
      show ‹atom z ♯ GNil› using z fresh_Pair by auto
      show ‹atom z ♯ AE_split [ L_bitvec v ]^v [ L_num n ]^v› using z fresh_Pair by auto
      show ‹atom z ♯ GNil› using z fresh_Pair by auto
      show ‹atom z ♯ AE_split [ L_bitvec v ]^v [ L_num n ]^v› using z fresh_Pair by auto
      show ‹atom z ♯ GNil› using z fresh_Pair by auto
    qed

    show ‹Θ; Φ; {||}; GNil; Δ ⊨ AE_val (V_pair (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2))) ==> { z : B_pair B_bitvec B_bitvec | CE_val (V_var z) == CE_val ((V_pair (V_lit (L_bitvec v1)) (V_lit (L_bitvec v2)))) } ›
      (is "Θ; Φ; {||}; GNil; Δ ⊨ ?e2 ==> ?t2")
      apply(rule infer_e_valI)
      using check_s_wf elim apply metis
      using check_s_wf elim apply metis      
      apply(rule infer_v_pair2I)
      using z fresh_prodN apply metis
      using z fresh_GNil fresh_prodN apply metis
      using  infer_v_litI infer_l.intros  ‹Θ ; {||} ⊨_wf GNil› b_of.simps  apply blast+
      using b_of.simps apply simp+
      done
    show ‹Θ ; {||} ; GNil ⊨ ?t2 < ?t1› using subtype_split check_s_wf elim reduce_let_splitI by auto
  qed

  thus ?case  using config_typeI elim by (meson order_refl)
next
  case (reduce_assert1I Φ δ c v)

  hence elim: "Θ; Φ; {||}; GNil; Δ ⊨ AS_assert c [v]^s <== τ ∧
                  Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims reduce_assert1I by metis
  hence *:"Θ; Φ; {||}; GNil; Δ ⊨ AS_assert c [v]^s <== τ" by auto

  have  "Θ; Φ; {||}; GNil; Δ ⊨ [v]^s <== τ" using  check_assert_s *  by metis
  thus  ?case using elim config_typeI  by blast
next
  case (reduce_assert2I Φ δ s δ' s' c)

  hence elim: "Θ; Φ; {||}; GNil; Δ ⊨ AS_assert c s <== τ ∧
                  Θ ⊨ δ ∼ Δ ∧ (∀fd∈set Φ. check_fundef Θ Φ fd)" 
    using config_type_elims by metis
  hence *:"Θ; Φ; {||}; GNil; Δ ⊨ AS_assert c s <== τ" by auto

  have  cv: "Θ; Φ; {||}; GNil; Δ ⊨ s <== τ ∧ Θ ; {||} ; GNil ⊨ c " using check_assert_s *  by metis

  hence "Θ; Φ; Δ ⊨ ⟨δ, s⟩ <== τ" using elim config_typeI by simp
  then obtain Δ' where D: "Θ; Φ; Δ' ⊨ ⟨ δ' , s' ⟩ <== τ ∧ Δ ⊑ Δ'" using reduce_assert2I by metis
  hence **:"Θ; Φ; {||}; GNil; Δ' ⊨ s' <== τ ∧ Θ ⊨ δ' ∼ Δ'" using config_type_elims by metis

  obtain x::x where x:"atom x ♯ (Θ, Φ, ({||}::bv fset), GNil, Δ', c, τ, s')" using obtain_fresh by metis

  have *:"Θ; Φ; {||}; GNil; Δ' ⊨ AS_assert c s' <== τ" proof
    show "atom x ♯ (Θ, Φ, {||}, GNil, Δ', c, τ, s')" using x by auto
    have "Θ ; {||} ; GNil ⊨_wf c" using * check_s_wf by auto
    hence wfg:"Θ ; {||} ⊨_wf (x, B_bool, c) #_\<Gamma> GNil" using wfC_wfG wfB_boolI check_s_wf *  fresh_GNil by auto
    moreover have cs: "Θ; Φ; {||}; GNil; Δ' ⊨ s' <== τ" using ** by auto
    ultimately show  "Θ ; Φ ; {||} ; (x, B_bool, c) #_\<Gamma> GNil ; Δ' ⊨ s' <== τ" using check_s_g_weakening(1)[OF cs _ wfg]   toSet.simps  by simp
    show "Θ ; {||} ; GNil ⊨ c " using cv by auto
    show "Θ ; {||} ; GNil ⊨_wf Δ' " using check_s_wf ** by auto
  qed

  thus  ?case using elim config_typeI D ** by metis
qed

lemma preservation_many: 
  assumes " Φ ⊨ ⟨δ, s⟩ ⟶^* ⟨ δ' , s' ⟩"
  shows "Θ; Φ; Δ ⊨ ⟨δ, s⟩ <== τ ==> ∃Δ'. Θ; Φ; Δ' ⊨ ⟨ δ' , s' ⟩ <== τ ∧ Δ ⊑ Δ'" 
  using assms proof(induct arbitrary: Δ rule: reduce_stmt_many.induct)
  case (reduce_stmt_many_oneI Φ δ s δ' s')
  then show ?case using preservation by simp
next
  case (reduce_stmt_many_manyI Φ δ s δ' s' δ'' s'')
  then show ?case using preservation subset_trans by metis
qed

section ‹Progress›
text ‹We prove that a well typed program is either a value or we can make a step›

lemma check_let_op_infer:
  assumes  "Θ; Φ; {||}; Γ; Δ ⊨ LET x = (AE_op opp v1 v2) IN s <== τ" and "supp ( LET x = (AE_op opp v1 v2) IN s) ⊆ atom`fst`setD Δ"
  shows  "∃ z b c. Θ; Φ; {||}; Γ; Δ ⊨ (AE_op opp v1 v2) ==> {z:b|c}"
proof - 
  have xx: "Θ; Φ; {||}; Γ; Δ ⊨ LET x = (AE_op opp v1 v2) IN s <== τ" using assms by simp
  then show ?thesis using check_s_elims(2)[OF xx] by meson
qed

lemma infer_pair:
  assumes "Θ ; B; Γ ⊨ v ==> { z : B_pair b1 b2 | c }" and "supp v = {}"
  obtains v1 and v2 where "v = V_pair v1 v2" 
  using assms proof(nominal_induct v rule: v.strong_induct)
  case (V_lit x)
  then show ?case by auto
next
  case (V_var x)
  then show ?case using v.supp supp_at_base by auto
next
  case (V_pair x1a x2a)
  then show ?case by auto
next
  case (V_cons x1a x2a x3)
  then show ?case by auto
next
  case (V_consp x1a x2a x3 x4)
  then show ?case by auto
qed

lemma progress_fst:
  assumes  "Θ; Φ; {||}; Γ; Δ ⊨ LET x = (AE_fst v) IN s <== τ" and  "Θ ⊨ δ ∼ Δ" and 
    "supp (LET x = (AE_fst v) IN s) ⊆ atom`fst`setD Δ"
  shows "∃δ' s'. Φ ⊨ ⟨ δ , LET x = (AE_fst v) IN s ⟩ ⟶ ⟨δ', s'⟩"
proof -
  have *:"supp v = {}" using assms s_branch_s_branch_list.supp by auto
  obtain z and b and c where "Θ; Φ; {||}; Γ; Δ ⊨ (AE_fst v ) ==> { z : b | c }" 
    using check_s_elims(2)  using assms by meson
  moreover obtain z' and b' and c' where "Θ ; {||} ; Γ ⊨ v ==> { z' : B_pair b b' | c' }" 
    using infer_e_elims(8)  using calculation by auto 
  moreover then obtain v1 and v2 where "V_pair v1 v2 = v" 
    using * infer_pair by metis
  ultimately show ?thesis using reduce_let_fstI assms  by metis
qed

lemma progress_let:
  assumes "Θ; Φ; {||}; Γ; Δ ⊨ LET x = e IN s <== τ" and "Θ ⊨ δ ∼ Δ" and 
    "supp (LET x = e IN s) ⊆ atom ` fst ` setD Δ" and "sble Θ Γ"
  shows "∃δ' s'. Φ ⊨ ⟨ δ , LET x = e IN s⟩ ⟶ ⟨ δ' , s'⟩"
proof -
  obtain z b c where *: "Θ; Φ; {||}; Γ; Δ ⊨ e ==> { z : b | c } " using check_s_elims(2)[OF assms(1)] by metis
  have **: "supp e ⊆ atom ` fst ` setD Δ" using assms s_branch_s_branch_list.supp by auto
  from * ** assms show ?thesis proof(nominal_induct "{ z : b | c }"  rule: infer_e.strong_induct)
    case (infer_e_valI Θ B Γ Δ Φ v)
    then show ?case using reduce_stmt_elims reduce_let_valI by metis
  next
    case (infer_e_plusI Θ B Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit (L_num n1) ∧ v2 = (V_lit (L_num n2))" using infer_int infer_e_plusI by metis
    then show ?case using reduce_let_plusI * by metis
  next
    case (infer_e_leqI Θ B Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit (L_num n1) ∧ v2 = (V_lit (L_num n2))" using infer_int infer_e_leqI by metis
    then show ?case using reduce_let_leqI * by metis
  next
    case (infer_e_eqI Θ B Γ Δ Φ v1 z1 bb c1 v2 z2 c2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit n1 ∧ v2 = (V_lit n2)" using infer_lit infer_e_eqI by metis
    then show ?case using reduce_let_eqI by blast
  next
    case (infer_e_appI Θ B Γ Δ Φ f x b c τ' s' v)
    then show ?case using reduce_let_appI by metis
  next
    case (infer_e_appPI Θ B Γ Δ Φ b' f bv x b c τ' s' v)
    then show ?case using reduce_let_appPI by metis
  next
    case (infer_e_fstI Θ B Γ Δ Φ v z' b2 c z)
    hence "supp v = {}" by force
    then obtain v1 and v2 where "v = V_pair v1 v2" using infer_e_fstI infer_pair by metis
    then show ?case using reduce_let_fstI * by metis
  next
    case (infer_e_sndI Θ B Γ Δ Φ v z' b1 c z)
    hence "supp v = {}" by force
    then obtain v1 and v2 where "v = V_pair v1 v2" using infer_e_sndI infer_pair by metis
    then show ?case using reduce_let_sndI * by metis
  next
    case (infer_e_lenI Θ B Γ Δ Φ v z' c za)
    hence "supp v = {}" by force
    then obtain bvec where "v = V_lit (L_bitvec bvec)" using infer_e_lenI infer_bitvec by metis
    then show ?case using reduce_let_lenI * by metis
  next
    case (infer_e_mvarI Θ B Γ Φ Δ u)
    hence "(u, { z : b | c }) ∈ setD Δ" using infer_e_elims(10) by meson
    then obtain v where "(u,v) ∈ set δ" using infer_e_mvarI delta_sim_delta_lookup by meson
    then show ?case using reduce_let_mvar by metis
  next
    case (infer_e_concatI Θ B Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit (L_bitvec n1) ∧ v2 = (V_lit (L_bitvec n2))" using infer_bitvec infer_e_concatI by metis
    then show ?case using reduce_let_concatI * by metis
  next
    case (infer_e_splitI Θ B Γ Δ Φ v1 z1 c1 v2 z2 z3)
    hence vf: "supp v1 = {} ∧ supp v2 = {}"  by force
    then obtain n1 and n2 where *: "v1 = V_lit (L_bitvec n1) ∧ v2 = (V_lit (L_num n2))" using infer_bitvec infer_e_splitI check_int by metis

    have "0 ≤ n2 ∧ n2 ≤ int (length n1)" using  check_v_range[OF _ * ]   infer_e_splitI by simp
    then obtain bv1 and bv2 where "split n2 n1 (bv1 , bv2)" using obtain_split by metis
    then show ?case using reduce_let_splitI * by metis
  qed
qed 

lemma check_css_lookup_branch_exist:
  fixes s::s and cs::branch_s and css::branch_list and v::v
  shows 
    "Θ; Φ; B; G; Δ ⊨ s <== τ ==> True" and 
    "check_branch_s Θ Φ {||} GNil Δ tid dc const v cs τ ==> True" and 
    "Θ; Φ; B; Γ; Δ; tid; dclist; v ⊨ css <== τ ==> (dc, t) ∈ set dclist ==>
              ∃x' s'. Some (AS_branch dc x' s') = lookup_branch dc css"
proof(nominal_induct τ and τ and τ  rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_branch_list_consI Θ Φ B Γ Δ tid cons const v cs τ dclist css)
  then show ?case  using lookup_branch.simps check_branch_list_finalI by force
next
  case (check_branch_list_finalI Θ Φ B Γ Δ tid cons const v cs τ)
  then show ?case  using lookup_branch.simps check_branch_list_finalI by force
qed(auto+)

lemma progress_aux:  
  shows    "Θ; Φ; B; Γ; Δ ⊨ s <== τ ==> B = {||} ==> sble Θ Γ ==> supp s ⊆ atom ` fst ` setD Δ ==> Θ ⊨ δ ∼ Δ ==>
               (∃v. s = [v]^s) ∨ (∃δ' s'. Φ ⊨ ⟨δ, s⟩ ⟶ ⟨δ', s'⟩)" and
    "Θ; Φ; {||}; Γ; Δ; tid; dc; const; v2 ⊨ cs <== τ ==> supp cs = {} ==> True " 
    "Θ; Φ; {||}; Γ; Δ; tid; dclist; v2 ⊨ css <== τ ==> supp css = {} ==> True " 
proof(induct  rule: check_s_check_branch_s_check_branch_list.inducts)
  case (check_valI Δ Θ Γ v τ' τ)
  then show ?case by auto
next
  case (check_letI x Θ Φ B Γ Δ e τ z s b c)
  hence "Θ; Φ; {||}; Γ; Δ ⊨ AS_let x e s <== τ" using Typing.check_letI by meson
  then show ?case using progress_let check_letI by metis
next
  case (check_branch_s_branchI Θ B Γ Δ τ const x Φ tid cons v s)
  then show ?case by auto
next
  case (check_branch_list_consI Θ Φ B Γ Δ tid dclist v cs τ css)
  then show ?case by auto
next
  case (check_branch_list_finalI Θ Φ B Γ Δ tid dclist v cs τ)
  then show ?case by auto
next
  case (check_ifI z Θ Φ B Γ Δ v s1 s2 τ)
  have "supp v = {}" using check_ifI s_branch_s_branch_list.supp by auto
  hence "v = V_lit L_true ∨ v = V_lit L_false" using  check_bool_options check_ifI by auto
  then show ?case using reduce_if_falseI reduce_if_trueI check_ifI by meson
next
  case (check_let2I x Θ Φ B G Δ t s1 τ s2 )
  then consider  " (∃v. s1 = AS_val v)" | "(∃δ' a. Φ ⊨ ⟨δ, s1⟩ ⟶ ⟨δ', a⟩)" by auto
  then show ?case proof(cases)
    case 1
    then show ?thesis using reduce_let2_valI by fast
  next
    case 2
    then show ?thesis using reduce_let2I check_let2I by meson
  qed
next
  case (check_varI u Θ Φ B Γ Δ τ' v τ s)

  obtain uu::u where uf: "atom uu ♯ (u,δ,s) " using obtain_fresh by blast
  obtain sa where " (uu ↔ u ) ∙ s = sa" by presburger
  moreover have "atom uu ♯ s" using uf fresh_prod3 by auto
  ultimately have "AS_var uu τ' v sa = AS_var u τ' v s" using s_branch_s_branch_list.eq_iff(7) Abs1_eq_iff(3)[of uu sa u s] by auto

  moreover have "atom uu ♯ δ" using uf fresh_prod3 by auto
  ultimately have "Φ ⊨ ⟨δ, AS_var u τ' v s⟩ ⟶ ⟨(uu, v) # δ, sa⟩"
    using reduce_varI uf by metis
  then show ?case by auto
next
  case (check_assignI Δ u τ P G v z τ')
  then show ?case using reduce_assignI by blast
next
  case (check_whileI Θ Φ B Γ Δ s1 z s2 τ')
  obtain x::x where "atom x ♯ (s1,s2)" using obtain_fresh by metis
  moreover obtain z::x where "atom z ♯ x" using obtain_fresh by metis
  ultimately show ?case using reduce_whileI by fast
next
  case (check_seqI P Φ B G Δ s1 z s2 τ)
  thus  ?case proof(cases "∃v. s1 = AS_val v")
    case True
    then obtain v where v: "s1 = AS_val v" by blast
    hence "supp v = {}" using check_seqI by auto
    have "∃z1 c1. P; B; G ⊨ v ==> ({ z1 : B_unit | c1 })" proof - 
      obtain t where t:"P; B; G ⊨ v ==> t ∧ P; B ; G ⊨ t < ({ z : B_unit | TRUE })"  
        using v check_seqI(1) check_s_elims(1) by blast
      obtain z1 and b1 and c1 where teq: "t = ({ z1 : b1 | c1 })" using obtain_fresh_z by meson
      hence "b1 = B_unit" using subtype_eq_base t by meson
      thus ?thesis using t teq by fast
    qed
    then obtain z1 and c1 where "P ; B ; G ⊨ v ==> ({ z1 : B_unit | c1 })" by auto
    hence "v = V_lit L_unit" using infer_v_unit_form ‹supp v = {}› by simp
    hence "s1 = AS_val (V_lit L_unit)" using v by auto
    then show ?thesis using check_seqI reduce_seq1I by meson
  next
    case False
    then show ?thesis using check_seqI reduce_seq2I 
      by (metis Un_subset_iff s_branch_s_branch_list.supp(9))
  qed

next
  case (check_caseI Θ Φ B Γ Δ tid dclist v cs τ  z)
  hence "supp v = {}" by auto

  then obtain v' and dc and t::τ where v: "v = V_cons tid dc v' ∧ (dc, t) ∈ set dclist" 
    using  check_v_tid_form check_caseI by metis
  obtain z and b and c where teq: "t = ({ z : b | c })" using obtain_fresh_z by meson

  moreover then obtain x' s' where  "Some (AS_branch dc x' s') = lookup_branch dc cs" using  v teq check_caseI check_css_lookup_branch_exist by metis
  ultimately show ?case using reduce_caseI v check_caseI dc_of.cases by metis
next
  case (check_assertI x Θ Φ B Γ Δ c τ s)
  hence sps: "supp s ⊆ atom ` fst ` setD Δ" by auto
  have "atom x ♯ c " using check_assertI by auto
  have "atom x ♯ Γ" using check_assertI check_s_wf wfG_elims by metis
  have "sble Θ ((x, B_bool, c) #_\<Gamma> Γ)" proof -
    obtain i' where i':" i' ⊨ Γ ∧ Θ; Γ ⊨ i'" using check_assertI sble_def by metis
    obtain i::valuation where i:"i = i' ( x ↦ SBool True)" by auto

    have "i ⊨ (x, B_bool, c) #_\<Gamma> Γ" proof -
      have "i' ⊨ c" using valid.simps i'  check_assertI by metis
      hence "i ⊨ c" using is_satis_weakening_x i ‹atom x ♯ c› by auto
      moreover have "i ⊨ Γ"  using is_satis_g_weakening_x i' i  check_assertI ‹atom x ♯ Γ› by metis
      ultimately show ?thesis   using is_satis_g.simps i by auto
    qed
    moreover have "Θ ; ((x, B_bool, c) #_\<Gamma> Γ) ⊨ i" proof(rule  wfI_cons)
      show ‹ i' ⊨ Γ › using i' by auto
      show ‹ Θ ; Γ ⊨ i'› using i' by auto
      show ‹i = i'(x ↦ SBool True)› using i by auto
      show ‹ Θ ⊨ SBool True: B_bool› using wfRCV_BBoolI by auto
      show ‹atom x ♯ Γ› using check_assertI check_s_wf wfG_elims by auto
    qed
    ultimately show  ?thesis using sble_def by auto
  qed
  then consider "(∃v. s = [v]^s)" | "(∃δ' a. Φ ⊨ ⟨δ, s⟩ ⟶ ⟨ δ', a⟩)" using check_assertI sps by metis
  hence "(∃δ' a. Φ ⊨ ⟨δ, ASSERT c IN s⟩ ⟶ ⟨δ', a⟩)" proof(cases)
    case 1
    then show ?thesis using reduce_assert1I by metis
  next
    case 2
    then show ?thesis using reduce_assert2I by metis
  qed  
  thus ?case by auto
qed

lemma progress:
  assumes "Θ; Φ; Δ ⊨ ⟨δ, s⟩ <== τ" 
  shows "(∃v. s = [v]^s) ∨ (∃δ' s'. Φ ⊨ ⟨δ, s⟩ ⟶ ⟨δ', s'⟩)"
proof -
  have "Θ; Φ; {||}; GNil; Δ ⊨ s <== τ" and "Θ ⊨ δ ∼ Δ"
    using config_type_elims[OF assms(1)] by auto+
  moreover hence "supp s ⊆ atom ` fst ` setD Δ" using check_s_wf wfS_supp by fastforce
  moreover have "sble Θ GNil" using sble_def wfI_def is_satis_g.simps by simp
  ultimately show  ?thesis using progress_aux by blast
qed

section ‹Safety›

lemma  safety_stmt:
  assumes "Φ ⊨ ⟨δ, s⟩ ⟶^* ⟨δ', s'⟩" and "Θ; Φ; Δ ⊨ ⟨δ, s⟩ <== τ"
  shows  "(∃v. s' = [v]^s) ∨ (∃δ'' s''. Φ ⊨ ⟨δ', s'⟩ ⟶ ⟨δ'', s''⟩)"  
  using preservation_many progress assms  by meson

lemma safety:
  assumes "⊨ ⟨PROG Θ Φ G s⟩ <== τ" and  "Φ ⊨ ⟨δ_of G, s⟩ ⟶^* ⟨δ', s'⟩"
  shows  "(∃v. s' = [v]^s) ∨ (∃δ'' s''. Φ ⊨ ⟨δ', s'⟩ ⟶ ⟨δ'', s''⟩)"   
  using assms config_type_prog_elims safety_stmt by metis

end