Quelle Safety.thy

Sprache: Isabelle

(*<*)
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 ⊨_w_f τ" 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 ⊨_w_f Δ"
  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,τ')#_\<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 ⊨_w_f Δ'" 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 ⊨_w_f Δ"
  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 ⊨_w_f s : b_of τ"  using check_s_wf[OF assms] by auto
  moreover have "Θ ; B ; GNil ⊨_w_f τ " using check_s_wf assms by auto
  moreover have "Θ ; B ; GNil ⊨_w_f 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 ‹ Θ ; {||} ⊨_w_f b' ›
  shows "check_funtyp Θ Φ {||} (AF_fun_typ x b[bv::=b']_b_b (c[bv::=b']_c_b) τ[bv::=b']_\<tau>_b s[bv::=b']_s_b)"
  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']_b_b (c'[bv::=b']_c_b) τ'[bv::=b']_\<tau>_b s'[bv::=b']_s_b)" proof
    show ‹atom x' ♯ (Θ, Φ, {||}::bv fset, b[bv::=b']_b_b)› 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']_s_b <== τ'[bv::=b']_\τ_b› proof(rule subst_b_check_s)
      show ‹ Θ ; {||} ⊨_w_f 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']_b_b, c'[bv::=b']_c_b) #_\Γ GNil ; []_\Δ ⊨ s'[bv::=b']_s_b <== τ'[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']_b_b (c[bv::=b']_c_b) τ[bv::=b']_\<tau>_b s[bv::=b']_s_b) = (AF_fun_typ x' b[bv::=b']_b_b (c'[bv::=b']_c_b) τ'[bv::=b']_\<tau>_b s'[bv::=b']_s_b)"
    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]_s_v <== τ[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]_c_v = 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]_c_v = c' ∧ s'[x'::=v]_s_v = s[x::=v]_s_v ∧ τ'[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]_c_v) #_\<Gamma> GNil)[x'::=v]_\<Gamma>_v ; []_\<Delta>[x'::=v]_\<Delta>_v ⊨ s'[x'::=v]_s_v <== τ'[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]_c_v) #_\Γ GNil ; []_\Δ ⊨ s' <== τ'› using check_funtypI eq2 by metis
    show ‹ (x', b, c''[x''::=[ x' ]^v]_c_v) #_\Γ GNil = GNil @ (x', b, c''[x''::=[ x' ]^v]_c_v) #_\Γ GNil› using append_g.simps by auto
  qed
  hence " Θ; Φ; {||}; GNil; []_\<Delta> ⊨ s'[x'::=v]_s_v <== τ'[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]_s_v <== 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]_s_v = s[x::=v]_s_v ∧ t[x::=v]_\<tau>_v = t'[x'::=v]_\<tau>_v"
    using funtyp_eq_iff_equalities by metis
  hence "Θ; Φ; {||}; GNil; []_\<Delta> ⊨ s'[x'::=v]_s_v <== 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']_b_b | c'[bv'::=b']_c_b } = { x : b[bv::=b']_b_b | c[bv::=b']_c_b } ∧
          s'[bv'::=b']_s_b[x'::=v]_s_v = s[bv::=b']_s_b[x::=v]_s_v ∧ 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']_b_b | c[bv::=b']_c_b }"   and
    "Θ ; {||} ⊨_w_f b'"
  shows "Θ; Φ; {||}; GNil; DNil ⊨ s[bv::=b']_s_b[x::=v]_s_v <== 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']_b_b | c'[bv'::=b']_c_b } = { x : b[bv::=b']_b_b | c[bv::=b']_c_b } ∧
          s'[bv'::=b']_s_b[x'::=v]_s_v = s[bv::=b']_s_b[x::=v]_s_v ∧ 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']_b_b (c'[bv'::=b']_c_b) (t'[bv'::=b']_\<tau>_b) s'[bv'::=b']_s_b)"
    using check_funtyp_subst_b[OF check_funtypq_polyI(5) check_funtypq_polyI(8)]  by metis
  moreover have "Θ ; {||} ; GNil ⊨ v <== { x' : b''[bv'::=b']_b_b | c'[bv'::=b']_c_b }" using ** check_funtypq_polyI by metis
  ultimately have "Θ; Φ; {||}; GNil; []_\<Delta> ⊨ s'[bv'::=b']_s_b[x'::=v]_s_v <== 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 ⊨_w_f Δ"
  shows "Θ; Φ; {||}; GNil; Δ ⊨ s[x::=v]_s_v <== 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']_b_b | c[bv::=b']_c_b }" and "Θ ; {||} ; GNil ⊨_w_f Δ" and  "Θ ; {||} ⊨_w_f b'"
  shows "Θ; Φ; {||}; GNil; Δ ⊨ s[bv::=b']_s_b[x::=v]_s_v <== 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]_s_v) 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 ⊨_w_f Δ ∧ Θ ⊨_w_f Φ ∧ 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]_c_v } ∧ 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]_s_v) s2 <== τ" proof
    show ‹atom x2 ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, τ3[x3::=v]_\τ_v, s3[x3::=v]_s_v, τ)›
      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]_s_v <== τ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 ⊨_w_f Δ › 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]_s_v) s2 = AS_let2 x (τ1'[x1::=v]_\<tau>_v) (s1'[x1::=v]_s_v) 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]_s_v = (s1'[x1::=v]_s_v)" 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 ==> Θ ; {||} ⊨_w_f b' ==>
               Θ; Φ; {||}; GNil; Δ ⊨ LET x : (τ1'[bv1::=b']_\<tau>_b[x1::=v]_\<tau>_v) = (s1'[bv1::=b']_s_b[x1::=v]_s_v) 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 ⊨_w_f Δ ∧ Θ ⊨_w_f Φ ∧ 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']_b_b | c3[bv3::=b']_c_b } ∧ atom x3 ♯ GNil ∧ τ3[bv3::=b']_\<tau>_b[x3::=v]_\<tau>_v = { z : b | c }
  ∧ Θ ; {||} ⊨_w_f 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]_c_v } ∧ atom z3 ♯ (x3, v,c3,x1,c1)" using obtain_fresh_z3 by metis

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

  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']_s_b[x3::=v]_s_v) s2 <== τ"
  proof
    show ‹atom x2 ♯ (Θ, Φ, {||}::bv fset, GNil, Δ, τ3[bv3::=b']_\τ_b[x3::=v]_\τ_v, s3[bv3::=b']_s_b[x3::=v]_s_v, τ)›
    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']_s_b[x3::=v]_s_v"
        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']_s_b[x3::=v]_s_v <== τ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']_b_b | c3[bv3::=b']_c_b }› using ** by metis
      show ‹ Θ ; {||} ; GNil ⊨_w_f Δ › using ** by metis
      show ‹ Θ ; {||} ⊨_w_f 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']_s_b[x3::=v]_s_v) s2 = AS_let2 x (τ1'[bv1::=b']_\<tau>_b[x1::=v]_\<tau>_v) (s1'[bv1::=b']_s_b[x1::=v]_s_v) 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']_s_b[x3::=v]_s_v = (s1'[bv1::=b']_s_b[x1::=v]_s_v)" 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)]^c^e) ([V_lit (L_num n2)]^c^e) }"
    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 ]^c^e == [ plus [ [ L_num n1 ]^v ]^c^e [ [ L_num n2 ]^v ]^c^e ]^c^e } ==> 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)]^c^e) ([V_lit (L_num n2)]^c^e) }"
    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)]^c^e) ([V_lit (n2)]^c^e) }"
    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 ]^c^e == [ eq [ [ n1 ]^v ]^c^e [ [ n2 ]^v ]^c^e ]^c^e } = 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 "Θ ; {||} ⊨_w_f 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 ‹Θ ; {||} ⊨_w_f 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]_s_v = sa[xa::=v]_s_v"
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]_s_v) <== τ" 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]_c_v) #_\<Gamma> Γ"
  have "Θ ; Φ ; B ; ?G[x1::=v]_\<Gamma>_v ; Δ[x1::=v]_\<Delta>_v ⊨ s1[x1::=v]_s_v <== τ[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]_c_v) #_\Γ Γ ; Δ ⊨ s1 <== τ› using check_letI subst_defs by auto
    show "(x1, b, c[z::=V_var x1]_c_v) #_\<Gamma> Γ = GNil @ (x1, b, c[z::=V_var x1]_c_v) #_\<Gamma> Γ" by auto
  qed

  hence "Θ ; Φ ; B ; Γ ; Δ ⊨ s1[x1::=v]_s_v <== τ"  using check_letI by auto
  moreover have " s1[x1::=v]_s_v = s[x::=v]_s_v"
    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]_s_v <== τ[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]_c_v) #_\<Gamma> Γ" using append_g.simps c_of_switch * fresh_prodN by metis
  qed

  hence "Θ ; Φ ; B ; Γ ; Δ ⊨ s2[x1::=v]_s_v <== τ"  using check_let2I by auto
  moreover have " s2[x1::=v]_s_v = s[x::=v]_s_v" 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]_s_v ⟩ <== τ ∧ Δ ⊑ Δ'"
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]_s_v <== τ"
  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 ; Γ ⊨_w_f { z : b_of t | c_of t z }" and "Θ ; B ; Γ ⊨_w_f { 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]_c_v) #_\<Gamma> Γ ⊨ (c IMP c_of t z )[z::=[ x ]^v]_c_v "
    unfolding subst_cv.simps
  proof(rule valid_eq_imp)

    have "Θ ; B ; (x, b_of t, (c_of t z)[z::=[ x ]^v]_v) #_\<Gamma> Γ ⊨_w_f (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]_c_v) #_\<Gamma> Γ ⊨_w_f c[z::=[ x ]^v]_c_v IMP (c_of t z)[z::=[ x ]^v]_c_v "
      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 ; Γ ⊨_w_f t" and "Θ ; B ; Γ ⊨_w_f { 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 ; Γ ⊨_w_f 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 ⊨_w_f τ ==> 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]_c_v = (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 ⊨_w_f ({ 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 ⊨_w_f τ" 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 ⊨_w_f { z : b | c1 }" and  "Θ ; B ; GNil ⊨_w_f { z : b | c2 }"
  shows  "Θ ; B ; GNil ⊨_w_f { 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 ⊨_w_f b › using wfT_elims assms by metis
  have "Θ ; B ; (z, b, TRUE) #_\<Gamma> GNil ⊨_w_f c1" using wfT_wfC fresh_GNil assms by auto
  moreover have "Θ ; B ; (z, b, TRUE) #_\<Gamma> GNil ⊨_w_f c2" using wfT_wfC fresh_GNil assms by auto
  ultimately show ‹ Θ ; B ; (z, b, TRUE) #_\Γ GNil ⊨_w_f 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 ⊨_w_f { 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 ⊨_w_f { 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 ⊨_w_f (x, b, c1 AND c2) #_\<Gamma> Γ"
  shows "Θ ; B ⊨_w_f (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]_s_v <== τ" 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]_s_v <== τ"
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 ]^c^e == [ V_cons tid cons [ x ]^v ]^c^e 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 ]^c^e == [ V_cons tid cons [ z ]^v ]^c^e 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 ]^c^e == [ V_cons tid cons [ z ]^v ]^c^e }"
    proof(rule check_v_top)

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

      proof(rule wfG_wfT)
        show ‹ Θ ; B ⊨_w_f (x, b_of const, ([ va ]^c^e == [ V_cons tid cons [ z ]^v ]^c^e )[z::=[ x ]^v]_c_v) #_\Γ GNil ›
        proof -
          have 1: "va[z::=[ x ]^v]_v_v = va" using  forget_subst_v subst_v_v_def  z fresh_prodN by metis
          moreover have 2: "Θ ; B ⊨_w_f (x, b_of const, [ va ]^c^e == [ V_cons tid cons [ x ]^v ]^c^e AND c_of const x ) #_\<Gamma> GNil "
            using    check_branch_s_branchI(17)[THEN check_s_wf] ‹Γ = GNil› by auto
          moreover hence "Θ ; B ⊨_w_f (x, b_of const, [ va ]^c^e == [ V_cons tid cons [ x ]^v ]^c^e ) #_\<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 ]^c^e == [ V_cons tid cons [ z ]^v ]^c^e )› 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 ]^c^e = [ V_cons tid cons [ z ]^v ]^c^e[z::=v]_c_e_v›
        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 ]^c^e ⊆ 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]_s_v <== τ[x::=v]_\<tau>_v"
  proof(rule subst_check_check_s)
    show ‹Θ ; B ; GNil ⊨ v <== { z : b_of const | [ va ]^c^e == [ V_cons tid cons [ z ]^v ]^c^e 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 ]^c^e == [ V_cons tid cons [ z ]^v ]^c^e AND c_of const z)[z::=[ x ]^v]_c_v) #_\Γ GNil›
    proof -
      have "va[z::=[ x ]^v]_v_v = va" using  forget_subst_v subst_v_v_def  z fresh_prodN by metis
      moreover have  "(c_of const z)[z::=[ x ]^v]_c_v = 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]_s_v = s'[x'::=v]_s_v"
    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 ⊨_w_f Δ"  and "Θ ⊨_w_f Φ"  and "Θ ; {||} ⊨_w_f G"
  shows ‹ Θ ; Φ ; {||} ; G ; Δ ⊨ [[ L_unit ]^v]^s <== τ'›
proof -
  have *:"Θ ; {||} ; GNil ⊨ [L_unit]^v ==> { z : B_unit | [ [ z ]^v ]^c^e == [ [ L_unit ]^v ]^c^e }"
    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 ]^c^e == [ [ L_unit ]^v ]^c^e } < τ'"
    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: "Θ ; {||} ⊨_w_f ?G" proof
      show "c_of { z' : B_bool | TRUE } x ∈ {TRUE, FALSE}" using subst_cv.simps cof by auto
      show "Θ ; {||} ⊨_w_f GNil " using wfG_nilI check_whileI wfX_wfY check_s_wf by metis
      show "atom x ♯ GNil" using fresh_GNil by auto
      show "Θ ; {||} ⊨_w_f b_of { z' : B_bool | TRUE } " using wfB_boolI wfX_wfY check_s_wf b_of.simps
        by (metis ‹Θ ; {||} ⊨_w_f 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]^c^e == [[ x ]^v]^c^e }›
          using infer_v_varI lookup.simps wfg b_of.simps by metis
        thus  ‹Θ ; {||} ; ?G ⊨ { zz : B_bool | [[ zz ]^v]^c^e == [[ x ]^v]^c^e } < { 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 ]^c^e == [ [ L_true ]^v ]^c^e 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 ]^c^e == [ [ L_true ]^v ]^c^e 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 ]^c^e == [ [ L_true ]^v ]^c^e IMP c_of τ' zz }›
          proof(rule subtype_eq_if_τ)
            show ‹ Θ ; {||} ; ?G ⊨_w_f τ' › using * check_s_wf by auto
            show ‹ Θ ; {||} ; ?G ⊨_w_f { zz : b_of τ' | [ [ x ]^v ]^c^e == [ [ L_true ]^v ]^c^e 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 ]^c^e == [ [ L_false ]^v ]^c^e 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 ]^c^e == [ [ L_false ]^v ]^c^e IMP c_of τ' zz }›
        proof(rule subtype_eq_if_τ)
          show ‹ Θ ; {||} ; ?G ⊨_w_f τ' › using * check_s_wf by metis
          show ‹ Θ ; {||} ; ?G ⊨_w_f { zz : b_of τ' | [ [ x ]^v ]^c^e == [ [ L_false ]^v ]^c^e 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]_c_v = 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]_s_v <== τ[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 ]^c^e == [ [ L_true ]^v ]^c^e , 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 ; Γ ⊨_w_f { z : B_bool | [ [ z ]^v ]^c^e == [ [ L_true ]^v ]^c^e } › using vt infer_v_wf by simp
      show ‹ Θ ; B ; Γ ⊨_w_f { z : B_bool | c[x::=[ z ]^v]_v } › proof(rule wfG_wfT)
        show ‹ Θ ; B ⊨_w_f (x, B_bool, c[x::=[ z ]^v]_v[z::=[ x ]^v]_c_v) #_\Γ Γ › 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 ⊨_w_f(x, B_bool, ([ [ z ]^v ]^c^e == [ [ L_true ]^v ]^c^e )[z::=[ x ]^v]_v) #_\<Gamma> Γ"
        using wfT_wfG vt infer_v_wf fresh_prodN assms by simp
      show  ‹Θ ; B ; (x, B_bool, ([ [ z ]^v ]^c^e == [ [ L_true ]^v ]^c^e )[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]_c_v) #_\Γ Γ› 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 ]^c^e == [ [ v1 , v2 ]^v ]^c^e }"
  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]_s_v) s <== τ"
    using preservation_app reduce_let_appI tt by auto

  hence "Θ; Φ; Δ ⊨ ⟨ δ , AS_let2 x (τ'[z::=v]_\<tau>_v) s'[z::=v]_s_v 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']_s_b[z::=v]_s_v) 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 ‹ Θ ; {||} ⊨_w_f 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']_s_b[z::=v]_s_v 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]_c_v) #_\<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]_c_v) #_\<Gamma> GNil ; Δ ⊨ sa <== τ" proof(rule ctx_subtype_s)
    show "Θ ; Φ ; {||} ; GNil @ (xa, ba, ca[za::=V_var xa]_c_v) #_\<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 ⊨_w_f ({ 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 ⊨_w_f ({ 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 ⊨_w_f Δ" 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 " Θ ⊨_w_f Φ" 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 ⊨_w_f Δ'" using * check_s_wf by auto
      moreover have "Θ ; {||} ⊨_w_f ((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) ⊨_w_f Δ'" 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 ⊨_w_f Δ"
    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 ⊨_w_f Δ'" 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]_s_v <== τ" 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 "Θ ; {||} ⊨_w_f 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)]^c^e) ([V_lit (L_bitvec v2)]^c^e))} ›
      (is "Θ; Φ; {||}; GNil; Δ ⊨ ?e1 ==> ?t1")
    proof
      show ‹ Θ ; {||} ; GNil ⊨_w_f Δ › using check_s_wf elim by auto
      show ‹ Θ ⊨_w_f Φ › 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  ‹Θ ; {||} ⊨_w_f 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  ‹Θ ; {||} ⊨_w_f 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  ‹Θ ; {||} ⊨_w_f 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)]^c^e) }" 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))]^c^e }" 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 *:"Θ ; {||} ⊨_w_f 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 ⊨_w_f Δ › using check_s_wf elim by auto
      show ‹ Θ ⊨_w_f Φ › 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  ‹Θ ; {||} ⊨_w_f GNil› fresh_GNil by auto
      show "Θ ; {||} ; GNil ⊨ ([ L_num
                           n ]^v) <== { z : B_int | (([ leq [ [ L_num 0 ]^v ]^c^e [ [ z ]^v ]^c^e ]^c^e) == ([ [ L_true ]^v ]^c^e)) AND [ leq [ [ z ]^v ]^c^e [| [ [ L_bitvec
                   v ]^v ]^c^e |]^c^e ]^c^e == [ [ L_true ]^v ]^c^e }" 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  ‹Θ ; {||} ⊨_w_f 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 ⊨_w_f c" using * check_s_wf by auto
    hence wfg:"Θ ; {||} ⊨_w_f (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 ⊨_w_f Δ' " 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

Messung V0.5 in Prozent

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.60Bemerkung: (vorverarbeitet am 2026-06-10) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.