Theory BTVSubstTypingL

(*<*)
theory BTVSubstTypingL
  imports  "HOL-Eisbach.Eisbach_Tools" ContextSubtypingL SubstMethods
begin
  (*>*)

chapter ‹Basic Type Variable Substitution Lemmas›
text ‹Lemmas that show that types are preserved, in some way, 
under basic type variable substitution›

lemma subst_vv_subst_bb_commute:
  fixes bv::bv and b::b and x::x and v::v
  assumes "atom bv ♯ v"
  shows "(v'[x::=v]⇩v⇩v)[bv::=b]⇩v⇩b = (v'[bv::=b]⇩v⇩b)[x::=v]⇩v⇩v" 
  using assms proof(nominal_induct v'  rule: v.strong_induct)
  case (V_lit x)
  then show ?case using subst_vb.simps subst_vv.simps by simp
next
  case (V_var y)
  hence "v[bv::=b]⇩v⇩b=v" using forget_subst subst_b_v_def by metis
  then show ?case unfolding subst_vb.simps(2) subst_vv.simps(2) using V_var by auto
next
  case (V_pair x1a x2a)
  then show ?case using subst_vb.simps subst_vv.simps by simp
next
  case (V_cons x1a x2a x3)
  then show ?case using subst_vb.simps subst_vv.simps by simp
next
  case (V_consp x1a x2a x3 x4)
  then show ?case using subst_vb.simps subst_vv.simps by simp
qed

lemma subst_cev_subst_bb_commute:
  fixes bv::bv and b::b and x::x and v::v
  assumes "atom bv ♯ v"
  shows "(ce[x::=v]⇩v)[bv::=b]⇩c⇩e⇩b = (ce[bv::=b]⇩c⇩e⇩b)[x::=v]⇩v" 
  using assms apply (nominal_induct ce  rule: ce.strong_induct, (simp add: subst_vv_subst_bb_commute subst_ceb.simps subst_cv.simps))
  using assms subst_vv_subst_bb_commute subst_ceb.simps subst_cv.simps 
  by (simp add: subst_v_ce_def)+

lemma subst_cv_subst_bb_commute:
  fixes bv::bv and b::b and x::x and v::v
  assumes "atom bv ♯ v"
  shows "c[x::=v]⇩c⇩v[bv::=b]⇩c⇩b = (c[bv::=b]⇩c⇩b)[x::=v]⇩c⇩v" 
  using assms apply (nominal_induct c  rule: c.strong_induct )
  using assms subst_vv_subst_bb_commute subst_ceb.simps subst_cv.simps 
    subst_v_c_def subst_b_c_def   apply auto
  using subst_cev_subst_bb_commute subst_v_ce_def by auto+

lemma subst_b_c_of:
  "(c_of τ z)[bv::=b]⇩c⇩b =  c_of (τ[bv::=b]⇩τ⇩b) z"
proof(nominal_induct τ avoiding: z rule:τ.strong_induct)
  case (T_refined_type z' b' c')
  moreover have "atom bv ♯ [ z ]⇧v " using fresh_at_base v.fresh by auto
  ultimately show ?case using subst_cv_subst_bb_commute[of bv "V_var z" c' z' b]  c_of.simps subst_tb.simps by metis
qed

lemma subst_b_b_of:
  "(b_of τ)[bv::=b]⇩b⇩b =  b_of (τ[bv::=b]⇩τ⇩b)"
  by(nominal_induct τ rule:τ.strong_induct, simp add: b_of.simps subst_tb.simps )

lemma subst_b_if:
  "⦃ z : b_of τ[bv::=b]⇩τ⇩b  | CE_val (v[bv::=b]⇩v⇩b)  ==  CE_val (V_lit ll)   IMP  c_of τ[bv::=b]⇩τ⇩b z  ⦄ = ⦃ z : b_of τ | CE_val (v)  ==  CE_val (V_lit ll)   IMP  c_of τ z  ⦄[bv::=b]⇩τ⇩b "
  unfolding subst_tb.simps subst_cb.simps subst_ceb.simps subst_vb.simps using subst_b_b_of   subst_b_c_of by auto

lemma subst_b_top_eq:
  "⦃ z : B_unit  | TRUE ⦄[bv::=b]⇩τ⇩b = ⦃ z : B_unit  | TRUE ⦄" and "⦃ z : B_bool  | TRUE ⦄[bv::=b]⇩τ⇩b = ⦃ z : B_bool  | TRUE ⦄"  and "⦃ z : B_id tid | TRUE ⦄ = ⦃ z : B_id tid | TRUE ⦄[bv::=b]⇩τ⇩b"
  unfolding  subst_tb.simps subst_bb.simps subst_cb.simps by auto

lemmas subst_b_eq = subst_b_c_of subst_b_b_of subst_b_if subst_b_top_eq

lemma subst_cx_subst_bb_commute[simp]:
  fixes bv::bv and b::b and x::x and v'::c
  shows "(v'[x::=V_var y]⇩c⇩v)[bv::=b]⇩c⇩b = (v'[bv::=b]⇩c⇩b)[x::=V_var y]⇩c⇩v" 
  using subst_cv_subst_bb_commute fresh_at_base  v.fresh by auto

lemma subst_b_infer_b:
  fixes l::l and b::b
  assumes " ⊢ l ⇒ τ" and "Θ ; {||} ⊢⇩w⇩f b" and "B = {|bv|}"
  shows  "⊢ l ⇒ (τ[bv::=b]⇩τ⇩b)" 
  using assms infer_l_form3 infer_l_form4 wf_b_subst infer_l_wf subst_tb.simps base_for_lit.simps subst_tb.simps
    subst_b_base_for_lit subst_cb.simps(6) subst_ceb.simps(1) subst_vb.simps(1) subst_vb.simps(2) type_l_eq
  by metis

lemma subst_b_subtype:
  fixes s::s and b'::b
  assumes  "Θ ; {|bv|} ; Γ  ⊢ τ1 ≲ τ2" and "Θ ; {||} ⊢⇩w⇩f b'"  and "B = {|bv|}" 
  shows "Θ ; {||} ; Γ[bv::=b']⇩Γ⇩b  ⊢ τ1[bv::=b']⇩τ⇩b ≲ τ2[bv::=b']⇩τ⇩b"
  using assms proof(nominal_induct "{|bv|}"  Γ τ1 τ2 rule:subtype.strong_induct)
  case (subtype_baseI x Θ Γ z c z' c' b)

  hence **: "Θ ; {|bv|} ; (x, b, c[z::=V_var x]⇩c⇩v) #⇩Γ Γ  ⊨ c'[z'::=V_var x]⇩c⇩v " using validI subst_defs by metis

  have "Θ ; {||} ; Γ[bv::=b']⇩Γ⇩b  ⊢ ⦃ z : b[bv::=b']⇩b⇩b | c[bv::=b']⇩c⇩b ⦄  ≲ ⦃ z' : b[bv::=b']⇩b⇩b | c'[bv::=b']⇩c⇩b ⦄" proof(rule Typing.subtype_baseI)
    show "Θ ; {||} ; Γ[bv::=b']⇩Γ⇩b   ⊢⇩w⇩f ⦃ z : b[bv::=b']⇩b⇩b  | c[bv::=b']⇩c⇩b ⦄ " 
      using subtype_baseI assms wf_b_subst(4) subst_tb.simps subst_defs  by metis
    show "Θ ; {||} ; Γ[bv::=b']⇩Γ⇩b   ⊢⇩w⇩f ⦃ z' : b[bv::=b']⇩b⇩b  | c'[bv::=b']⇩c⇩b ⦄ " 
      using subtype_baseI assms wf_b_subst(4) subst_tb.simps by metis
    show "atom x ♯(Θ, {||}::bv fset, Γ[bv::=b']⇩Γ⇩b,  z , c[bv::=b']⇩c⇩b ,  z'  , c'[bv::=b']⇩c⇩b )" 
      apply(unfold fresh_prodN,auto simp add: * fresh_prodN fresh_empty_fset) 
      using subst_b_fresh_x * fresh_prodN  ‹atom x ♯ c› ‹atom x ♯ c'› subst_defs subtype_baseI by metis+
    have "Θ ; {||} ; (x, b[bv::=b']⇩b⇩b, c[z::=V_var x]⇩v[bv::=b']⇩c⇩b) #⇩Γ Γ[bv::=b']⇩Γ⇩b  ⊨ c'[z'::=V_var x]⇩v[bv::=b']⇩c⇩b" 
      using ** subst_b_valid subst_gb.simps assms  subtype_baseI  by metis
    thus "Θ ; {||} ; (x, b[bv::=b']⇩b⇩b, (c[bv::=b']⇩c⇩b)[z::=V_var x]⇩v) #⇩Γ Γ[bv::=b']⇩Γ⇩b  ⊨ (c'[bv::=b']⇩c⇩b)[z'::=V_var x]⇩v" 
      using subst_defs subst_cv_subst_bb_commute  by (metis subst_cx_subst_bb_commute)
  qed
  thus ?case using subtype_baseI subst_tb.simps subst_defs by metis
qed

lemma b_of_subst_bv:
  "(b_of τ)[x::=v]⇩b⇩b = b_of (τ[x::=v]⇩τ⇩b)"
proof -
  obtain z b c where *:"τ = ⦃ z : b | c ⦄ ∧ atom z ♯ (x,v)" using obtain_fresh_z by metis
  thus ?thesis  using subst_tv.simps * by auto 
qed

lemma subst_b_infer_v:
  fixes v::v and b::b
  assumes "Θ ; B ; G ⊢ v ⇒ τ" and "Θ ; {||} ⊢⇩w⇩f b" and "B = {|bv|}"
  shows  "Θ ; {||} ; G[bv::=b]⇩Γ⇩b ⊢ v[bv::=b]⇩v⇩b ⇒ (τ[bv::=b]⇩τ⇩b)" 
  using assms proof(nominal_induct avoiding: b bv rule: infer_v.strong_induct)
  case (infer_v_varI Θ ℬ Γ b' c x z)
  show ?case unfolding  subst_b_simps proof
    show "Θ ; {||}  ⊢⇩w⇩f Γ[bv::=b]⇩Γ⇩b " using infer_v_varI wf_b_subst by metis
    show "Some (b'[bv::=b]⇩b⇩b, c[bv::=b]⇩c⇩b) = lookup Γ[bv::=b]⇩Γ⇩b x" using subst_b_lookup infer_v_varI by metis
    show "atom z ♯ x" using infer_v_varI by auto
    show "atom z ♯  (Θ, {||}, Γ[bv::=b]⇩Γ⇩b) " by(fresh_mth add: infer_v_varI subst_b_fresh_x subst_b_Γ_def fresh_prodN fresh_empty_fset )
  qed
next
  case (infer_v_litI Θ ℬ Γ l τ)
  then show ?case using Typing.infer_v_litI subst_b_infer_b 
    using wf_b_subst1(3) by auto
next
  case (infer_v_pairI z v1 v2 Θ ℬ Γ t1 t2)
  show ?case unfolding   subst_b_simps b_of_subst_bv proof
    show "atom z ♯ (v1[bv::=b]⇩v⇩b, v2[bv::=b]⇩v⇩b)" by(fresh_mth add: infer_v_pairI subst_b_fresh_x)
    show "atom z ♯ (Θ, {||}, Γ[bv::=b]⇩Γ⇩b)" by(fresh_mth add: infer_v_pairI subst_b_fresh_x subst_b_Γ_def fresh_empty_fset)
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v1[bv::=b]⇩v⇩b ⇒ t1[bv::=b]⇩τ⇩b" using infer_v_pairI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v2[bv::=b]⇩v⇩b ⇒ t2[bv::=b]⇩τ⇩b" using infer_v_pairI by auto
  qed
next
  case (infer_v_consI s dclist Θ dc tc ℬ Γ v tv z)
  show ?case unfolding   subst_b_simps b_of_subst_bv proof
    show "AF_typedef s dclist ∈ set Θ" using infer_v_consI by auto
    show "(dc, tc) ∈ set dclist"  using infer_v_consI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v[bv::=b]⇩v⇩b ⇒ tv[bv::=b]⇩τ⇩b" using infer_v_consI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ tv[bv::=b]⇩τ⇩b ≲ tc" proof -
      have "atom bv ♯ tc" using wfTh_lookup_supp_empty fresh_def infer_v_consI infer_v_wf by fast
      moreover have  "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ tv[bv::=b]⇩τ⇩b ≲ tc[bv::=b]⇩τ⇩b"  
        using subst_b_subtype infer_v_consI by simp     
      ultimately show  ?thesis using forget_subst subst_b_τ_def by metis
    qed
    show "atom z ♯ v[bv::=b]⇩v⇩b"  using infer_v_consI using  subst_b_fresh_x subst_b_v_def by metis
    show "atom z ♯ (Θ, {||}, Γ[bv::=b]⇩Γ⇩b)"  by(fresh_mth add: infer_v_consI subst_b_fresh_x subst_b_Γ_def fresh_empty_fset)
  qed
next
  case (infer_v_conspI s bv2 dclist2 Θ dc tc ℬ Γ v tv ba z)

  have "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ V_consp s dc (ba[bv::=b]⇩b⇩b) (v[bv::=b]⇩v⇩b) ⇒ ⦃ z : B_app s (ba[bv::=b]⇩b⇩b)  | [ [ z ]⇧v ]⇧c⇧e  ==  [ V_consp s dc (ba[bv::=b]⇩b⇩b) (v[bv::=b]⇩v⇩b) ]⇧c⇧e  ⦄"
  proof(rule Typing.infer_v_conspI)
    show "AF_typedef_poly s bv2 dclist2 ∈ set Θ" using infer_v_conspI by auto
    show "(dc, tc) ∈ set dclist2"  using infer_v_conspI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v[bv::=b]⇩v⇩b ⇒ tv[bv::=b]⇩τ⇩b" 
      using infer_v_conspI subst_tb.simps by metis

    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ tv[bv::=b]⇩τ⇩b ≲ tc[bv2::=ba[bv::=b]⇩b⇩b]⇩τ⇩b" proof -
      have "supp tc ⊆ { atom bv2 }" using infer_v_conspI wfTh_poly_lookup_supp wfX_wfY by metis
      moreover have "bv2 ≠ bv"  using ‹atom bv2 ♯ ℬ› ‹ℬ = {|bv|} › fresh_at_base fresh_def 
        using fresh_finsert by fastforce
      ultimately have "atom bv ♯ tc" unfolding fresh_def by auto
      hence "tc[bv2::=ba[bv::=b]⇩b⇩b]⇩τ⇩b = tc[bv2::=ba]⇩τ⇩b[bv::=b]⇩τ⇩b" 
        using subst_tb_commute by metis
      moreover  have "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ tv[bv::=b]⇩τ⇩b ≲ tc[bv2::=ba]⇩τ⇩b[bv::=b]⇩τ⇩b" 
        using infer_v_conspI(7) subst_b_subtype infer_v_conspI by metis
      ultimately show ?thesis by auto
    qed    
    show "atom z ♯ (Θ, {||}, Γ[bv::=b]⇩Γ⇩b, v[bv::=b]⇩v⇩b, ba[bv::=b]⇩b⇩b)" 
      apply(unfold fresh_prodN, intro conjI, auto simp add: infer_v_conspI fresh_empty_fset)
      using ‹atom z ♯ Γ›  fresh_subst_if   subst_b_Γ_def x_fresh_b  apply metis
      using ‹atom z ♯ v›  fresh_subst_if   subst_b_v_def x_fresh_b  by metis
    show "atom bv2 ♯ (Θ, {||}, Γ[bv::=b]⇩Γ⇩b, v[bv::=b]⇩v⇩b, ba[bv::=b]⇩b⇩b)" 
      apply(unfold fresh_prodN, intro conjI, auto simp add: infer_v_conspI fresh_empty_fset)
      using ‹atom bv2 ♯ b›  ‹atom bv2 ♯ Γ› fresh_subst_if   subst_b_Γ_def apply metis
      using ‹atom bv2 ♯ b›  ‹atom bv2 ♯ v› fresh_subst_if   subst_b_v_def apply metis
      using ‹atom bv2 ♯ b›  ‹atom bv2 ♯ ba› fresh_subst_if   subst_b_b_def by metis
    show "Θ ; {||}  ⊢⇩w⇩f ba[bv::=b]⇩b⇩b " 
      using infer_v_conspI  wf_b_subst by metis
  qed
  thus ?case using subst_vb.simps subst_tb.simps subst_bb.simps by simp

qed

lemma subst_b_check_v:
  fixes v::v and b::b
  assumes "Θ ; B ; G ⊢ v ⇐ τ" and "Θ ; {||} ⊢⇩w⇩f b" and "B = {|bv|}"
  shows  "Θ ; {||} ; G[bv::=b]⇩Γ⇩b ⊢ v[bv::=b]⇩v⇩b ⇐ (τ[bv::=b]⇩τ⇩b)" 
proof -
  obtain τ' where "Θ ; B ; G ⊢ v ⇒ τ' ∧  Θ ; B ; G  ⊢ τ' ≲ τ" using check_v_elims[OF assms(1)] by metis
  thus ?thesis using subst_b_subtype subst_b_infer_v assms 
    by (metis (no_types)  check_v_subtypeI subst_b_infer_v subst_b_subtype)
qed

lemma subst_vv_subst_vb_switch:
  shows  "(v'[bv::=b']⇩v⇩b)[x::=v[bv::=b']⇩v⇩b]⇩v⇩v = v'[x::=v]⇩v⇩v[bv::=b']⇩v⇩b"
proof(nominal_induct v' rule:v.strong_induct)
  case (V_lit x)
  then show ?case using subst_vv.simps subst_vb.simps by auto
next
  case (V_var x)
  then show ?case using subst_vv.simps subst_vb.simps by auto
next
  case (V_pair x1a x2a)
  then show ?case using subst_vv.simps subst_vb.simps v.fresh by auto
next
  case (V_cons x1a x2a x3)
  then show ?case using subst_vv.simps subst_vb.simps v.fresh by auto
next
  case (V_consp x1a x2a x3 x4)
  then show ?case using subst_vv.simps subst_vb.simps v.fresh pure_fresh 
    by (metis forget_subst subst_b_b_def)
qed

lemma subst_cev_subst_vb_switch:
  shows  "(ce[bv::=b']⇩c⇩e⇩b)[x::=v[bv::=b']⇩v⇩b]⇩c⇩e⇩v = (ce[x::=v]⇩c⇩e⇩v)[bv::=b']⇩c⇩e⇩b"
  by(nominal_induct ce rule:ce.strong_induct, auto simp add: subst_vv_subst_vb_switch ce.fresh)

lemma subst_cv_subst_vb_switch:
  shows  "(c[bv::=b']⇩c⇩b)[x::=v[bv::=b']⇩v⇩b]⇩c⇩v = c[x::=v]⇩c⇩v[bv::=b']⇩c⇩b"
  by(nominal_induct c rule:c.strong_induct, auto simp add: subst_cev_subst_vb_switch c.fresh)

lemma subst_tv_subst_vb_switch:
  shows  "(τ[bv::=b']⇩τ⇩b)[x::=v[bv::=b']⇩v⇩b]⇩τ⇩v = τ[x::=v]⇩τ⇩v[bv::=b']⇩τ⇩b"
proof(nominal_induct τ avoiding: x v rule:τ.strong_induct)
  case (T_refined_type z b c )
  hence ceq: "(c[bv::=b']⇩c⇩b)[x::=v[bv::=b']⇩v⇩b]⇩c⇩v = c[x::=v]⇩c⇩v[bv::=b']⇩c⇩b" using subst_cv_subst_vb_switch by auto

  moreover have "atom z ♯ v[bv::=b']⇩v⇩b" using x_fresh_b fresh_subst_if subst_b_v_def T_refined_type by metis

  hence "⦃ z : b  | c ⦄[bv::=b']⇩τ⇩b[x::=v[bv::=b']⇩v⇩b]⇩τ⇩v = ⦃ z : b[bv::=b']⇩b⇩b  | (c[bv::=b']⇩c⇩b)[x::=v[bv::=b']⇩v⇩b]⇩c⇩v ⦄"
    using subst_tv.simps subst_tb.simps T_refined_type fresh_Pair by metis

  moreover have "⦃ z : b[bv::=b']⇩b⇩b  | (c[bv::=b']⇩c⇩b)[x::=v[bv::=b']⇩v⇩b]⇩c⇩v ⦄  =  ⦃ z : b  | c[x::=v]⇩c⇩v ⦄[bv::=b']⇩τ⇩b"
    using subst_tv.simps subst_tb.simps ceq τ.fresh forget_subst[of "bv" b b'] subst_b_b_def T_refined_type by metis

  ultimately show ?case using subst_tv.simps subst_tb.simps ceq T_refined_type by auto
qed

lemma subst_tb_triple:
  assumes "atom bv ♯ τ'" 
  shows  "τ'[bv'::=b'[bv::=b]⇩b⇩b]⇩τ⇩b[x'::=v'[bv::=b]⇩v⇩b]⇩τ⇩v = τ'[bv'::=b']⇩τ⇩b[x'::=v']⇩τ⇩v[bv::=b]⇩τ⇩b"  
proof -
  have "τ'[bv'::=b'[bv::=b]⇩b⇩b]⇩τ⇩b[x'::=v'[bv::=b]⇩v⇩b]⇩τ⇩v = τ'[bv'::=b']⇩τ⇩b[bv::=b]⇩τ⇩b [x'::=v'[bv::=b]⇩v⇩b]⇩τ⇩v"
    using subst_tb_commute ‹atom bv ♯ τ'› by auto
  also have "... = τ'[bv'::=b']⇩τ⇩b [x'::=v']⇩τ⇩v[bv::=b]⇩τ⇩b" 
    using subst_tv_subst_vb_switch by auto
  finally show ?thesis using fresh_subst_if forget_subst by auto
qed

lemma subst_b_infer_e:
  fixes s::s and b::b
  assumes "Θ ; Φ ; B ; G; D ⊢ e ⇒ τ" and "Θ ; {||} ⊢⇩w⇩f b"  and "B = {|bv|}" 
  shows  "Θ ; Φ ; {||} ; G[bv::=b]⇩Γ⇩b; D[bv::=b]⇩Δ⇩b ⊢ (e[bv::=b]⇩e⇩b) ⇒ (τ[bv::=b]⇩τ⇩b)" 
  using assms proof(nominal_induct avoiding: b rule: infer_e.strong_induct)
  case (infer_e_valI Θ ℬ Γ Δ Φ v τ)
  thus ?case using  subst_eb.simps infer_e.intros wf_b_subst subst_db.simps wf_b_subst infer_v_wf subst_b_infer_v 
    by (metis forget_subst ms_fresh_all(1) wfV_b_fresh)
next
  case (infer_e_plusI Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)

  show ?case unfolding subst_b_simps subst_eb.simps proof(rule Typing.infer_e_plusI)
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b " using wf_b_subst(10) subst_db.simps infer_e_plusI wfX_wfY 
      by (metis wf_b_subst(15))
    show "Θ  ⊢⇩w⇩f Φ " using infer_e_plusI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v1[bv::=b]⇩v⇩b ⇒ ⦃ z1 : B_int  | c1[bv::=b]⇩c⇩b ⦄" using subst_b_infer_v  infer_e_plusI subst_b_simps by force
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v2[bv::=b]⇩v⇩b ⇒ ⦃ z2 : B_int  | c2[bv::=b]⇩c⇩b ⦄" using subst_b_infer_v  infer_e_plusI subst_b_simps by force
    show "atom z3 ♯ AE_op Plus (v1[bv::=b]⇩v⇩b) (v2[bv::=b]⇩v⇩b)" using  subst_b_simps infer_e_plusI subst_b_fresh_x subst_b_e_def by metis
    show "atom z3 ♯ Γ[bv::=b]⇩Γ⇩b" using subst_g_b_x_fresh infer_e_plusI by auto
  qed
next
  case (infer_e_leqI Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
  show ?case unfolding subst_b_simps proof(rule Typing.infer_e_leqI)
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b  " using wf_b_subst(10) subst_db.simps infer_e_leqI wfX_wfY 
      by (metis wf_b_subst(15))
    show "Θ  ⊢⇩w⇩f Φ " using infer_e_leqI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v1[bv::=b]⇩v⇩b ⇒ ⦃ z1 : B_int  | c1[bv::=b]⇩c⇩b ⦄" using subst_b_infer_v  infer_e_leqI subst_b_simps by force
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v2[bv::=b]⇩v⇩b ⇒ ⦃ z2 : B_int  | c2[bv::=b]⇩c⇩b ⦄" using subst_b_infer_v  infer_e_leqI subst_b_simps by force
    show "atom z3 ♯ AE_op LEq (v1[bv::=b]⇩v⇩b) (v2[bv::=b]⇩v⇩b)" using  subst_b_simps infer_e_leqI subst_b_fresh_x subst_b_e_def by metis
    show "atom z3 ♯ Γ[bv::=b]⇩Γ⇩b" using subst_g_b_x_fresh infer_e_leqI by auto
  qed
next
  case (infer_e_eqI Θ ℬ Γ Δ Φ v1 z1 bb c1 v2 z2 c2 z3)
  show ?case unfolding subst_b_simps proof(rule Typing.infer_e_eqI)
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b  " using wf_b_subst(10) subst_db.simps infer_e_eqI wfX_wfY 
      by (metis wf_b_subst(15))
    show "Θ  ⊢⇩w⇩f Φ " using infer_e_eqI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v1[bv::=b]⇩v⇩b ⇒ ⦃ z1 : bb[bv::=b]⇩b⇩b  | c1[bv::=b]⇩c⇩b ⦄" using subst_b_infer_v  infer_e_eqI subst_b_simps by force
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v2[bv::=b]⇩v⇩b ⇒ ⦃ z2 : bb[bv::=b]⇩b⇩b  | c2[bv::=b]⇩c⇩b ⦄" using subst_b_infer_v  infer_e_eqI subst_b_simps by force
    show "atom z3 ♯ AE_op Eq (v1[bv::=b]⇩v⇩b) (v2[bv::=b]⇩v⇩b)" using  subst_b_simps infer_e_eqI subst_b_fresh_x subst_b_e_def by metis
    show "atom z3 ♯ Γ[bv::=b]⇩Γ⇩b" using subst_g_b_x_fresh infer_e_eqI by auto
    show "bb[bv::=b]⇩b⇩b  ∈ {B_bool, B_int, B_unit}" using infer_e_eqI by auto
  qed
next
  case (infer_e_appI Θ ℬ Γ Δ Φ f x b' c τ' s' v τ)
  show ?case proof(subst subst_eb.simps, rule Typing.infer_e_appI)
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b"  using wf_b_subst(10) subst_db.simps infer_e_appI wfX_wfY by (metis wf_b_subst(15))
    show "Θ  ⊢⇩w⇩f Φ " using infer_e_appI by auto
    show "Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b' c τ' s'))) = lookup_fun Φ f" using infer_e_appI by auto
        (*show  "Θ ; {||} ; (x, b', c) #⇩Γ GNil   ⊢⇩w⇩f τ'" using infer_e_appI sory*)
    have "atom bv ♯ b'"  using ‹Θ  ⊢⇩w⇩f Φ › infer_e_appI wfPhi_f_supp  fresh_def[of "atom bv" b'] by simp
    hence "b' = b'[bv::=b]⇩b⇩b" using subst_b_simps 
      using has_subst_b_class.forget_subst subst_b_b_def by force
    moreover have  ceq:"c = c[bv::=b]⇩c⇩b" using subst_b_simps proof -
      have "supp c ⊆ {atom x}" using infer_e_appI wfPhi_f_simple_supp_c[OF  _  ‹Θ  ⊢⇩w⇩f Φ ›]  by simp
      hence "atom bv ♯ c" using
          fresh_def[of "atom bv" c] 
        using fresh_def fresh_finsert insert_absorb 
          insert_subset ms_fresh_all supp_at_base x_not_in_b_set fresh_prodN by metis
      thus ?thesis 
        using forget_subst subst_b_c_def  fresh_def[of "atom bv" c] by metis    
    qed 
    show   "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ v[bv::=b]⇩v⇩b ⇐ ⦃ x : b'  | c ⦄"  
      using subst_b_check_v subst_tb.simps subst_vb.simps infer_e_appI 
    proof -
      have "Θ ; {|bv|} ; Γ ⊢ v ⇐ ⦃ x : b' | c ⦄"
        by (metis ‹ℬ = {|bv|}› ‹Θ ; ℬ ; Γ ⊢ v ⇐ ⦃ x : b' | c ⦄›) (* 0.0 ms *)
      then show ?thesis 
        by (metis (no_types) ‹Θ ; {||} ⊢⇩w⇩f b› ‹b' = b'[bv::=b]⇩b⇩b› subst_b_check_v subst_tb.simps ceq) 
    qed
    show "atom x ♯ (Θ, Φ, {||}::bv fset, Γ[bv::=b]⇩Γ⇩b, Δ[bv::=b]⇩Δ⇩b, v[bv::=b]⇩v⇩b, τ[bv::=b]⇩τ⇩b)"
      apply (fresh_mth add:  fresh_prodN subst_g_b_x_fresh infer_e_appI )
      using subst_b_fresh_x infer_e_appI apply metis+
      done            
    have "supp τ' ⊆ { atom x }" using wfPhi_f_simple_supp_t  infer_e_appI by auto
    hence "atom bv ♯ τ'" using fresh_def fresh_at_base by force
    then  show  "τ'[x::=v[bv::=b]⇩v⇩b]⇩v = τ[bv::=b]⇩τ⇩b" using infer_e_appI 
        forget_subst subst_b_τ_def subst_tv_subst_vb_switch subst_defs by metis
  qed
next
  case (infer_e_appPI Θ' ℬ Γ' Δ Φ' b' f' bv' x' b1 c τ' s' v' τ1)

  have beq: "b1[bv'::=b']⇩b⇩b[bv::=b]⇩b⇩b =  b1[bv'::=b'[bv::=b]⇩b⇩b]⇩b⇩b" 
  proof -
    have "supp b1 ⊆ { atom bv' }" using wfPhi_f_poly_supp_b infer_e_appPI 
      using supp_at_base by blast
    moreover have "bv ≠ bv'" using infer_e_appPI fresh_def supp_at_base 
      by (simp add: fresh_def supp_at_base)
    ultimately have "atom bv ♯ b1" using fresh_def fresh_at_base by force
    thus ?thesis by simp
  qed

  have ceq: "(c[bv'::=b']⇩c⇩b)[bv::=b]⇩c⇩b = c[bv'::=b'[bv::=b]⇩b⇩b]⇩c⇩b" proof -
    have "supp c ⊆ { atom bv', atom x' }" using wfPhi_f_poly_supp_c infer_e_appPI 
      using supp_at_base by blast
    moreover have "bv ≠ bv'" using infer_e_appPI fresh_def supp_at_base 
      by (simp add: fresh_def supp_at_base)
    moreover have "atom x' ≠ atom bv" by auto
    ultimately have "atom bv ♯ c" using fresh_def[of "atom bv" c] fresh_at_base by auto
    thus ?thesis by simp
  qed

  show ?case proof(subst subst_eb.simps, rule Typing.infer_e_appPI)
    show "Θ' ; {||} ; Γ'[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b " using wf_b_subst subst_db.simps infer_e_appPI wfX_wfY by metis
    show "Θ'  ⊢⇩w⇩f Φ' " using infer_e_appPI by auto
    show "Some (AF_fundef f' (AF_fun_typ_some bv' (AF_fun_typ x' b1 c τ' s'))) = lookup_fun Φ' f'" using infer_e_appPI by auto
    thus  "Θ' ; {||} ; Γ'[bv::=b]⇩Γ⇩b  ⊢ v'[bv::=b]⇩v⇩b ⇐ ⦃ x' : b1[bv'::=b'[bv::=b]⇩b⇩b]⇩b  | c[bv'::=b'[bv::=b]⇩b⇩b]⇩b ⦄"  
      using subst_b_check_v subst_tb.simps subst_b_simps infer_e_appPI 
    proof -
      have "Θ' ; {||} ; Γ'[bv::=b]⇩Γ⇩b  ⊢ v'[bv::=b]⇩v⇩b ⇐ ⦃ x' : b1[bv'::=b']⇩b[bv::=b]⇩b⇩b  | (c[bv'::=b']⇩b)[bv::=b]⇩c⇩b ⦄" 
        using  infer_e_appPI subst_b_check_v subst_tb.simps by metis
      thus  ?thesis using beq ceq  subst_defs by metis
    qed
    show "atom x' ♯ Γ'[bv::=b]⇩Γ⇩b" using subst_g_b_x_fresh infer_e_appPI by auto
    show  "τ'[bv'::=b'[bv::=b]⇩b⇩b]⇩b[x'::=v'[bv::=b]⇩v⇩b]⇩v = τ1[bv::=b]⇩τ⇩b" proof - (* τ'[bv'::=b']⇩τ⇩b[x'::=v']⇩τ⇩v = τ1 *)

      have "supp τ' ⊆ { atom x', atom bv' }" using wfPhi_f_poly_supp_t  infer_e_appPI by auto
      moreover hence "bv ≠ bv'" using infer_e_appPI fresh_def supp_at_base 
        by (simp add: fresh_def supp_at_base)
      ultimately have "atom bv ♯ τ'" using fresh_def by force
      hence "τ'[bv'::=b'[bv::=b]⇩b⇩b]⇩b[x'::=v'[bv::=b]⇩v⇩b]⇩v = τ'[bv'::=b']⇩b[x'::=v']⇩v[bv::=b]⇩τ⇩b"  using subst_tb_triple subst_defs by auto 
      thus ?thesis using infer_e_appPI by metis
    qed
    show "atom bv' ♯ (Θ', Φ', {||}, Γ'[bv::=b]⇩Γ⇩b, Δ[bv::=b]⇩Δ⇩b, b'[bv::=b]⇩b⇩b, v'[bv::=b]⇩v⇩b, τ1[bv::=b]⇩τ⇩b)" 
      unfolding fresh_prodN apply( auto simp add: infer_e_appPI fresh_empty_fset)
      using fresh_subst_if subst_b_Γ_def  subst_b_Δ_def  subst_b_b_def subst_b_v_def subst_b_τ_def infer_e_appPI by metis+
    show "Θ' ; {||}  ⊢⇩w⇩f b'[bv::=b]⇩b⇩b " using infer_e_appPI wf_b_subst by simp
  qed
next
  case (infer_e_fstI Θ ℬ Γ Δ Φ v z' b1 b2 c z)
  show ?case unfolding subst_b_simps proof(rule Typing.infer_e_fstI)
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b " using wf_b_subst(10) subst_db.simps infer_e_fstI wfX_wfY 
      by (metis wf_b_subst(15))
    show "Θ  ⊢⇩w⇩f Φ " using infer_e_fstI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v[bv::=b]⇩v⇩b ⇒ ⦃ z' : B_pair b1[bv::=b]⇩b⇩b b2[bv::=b]⇩b⇩b  | c[bv::=b]⇩c⇩b ⦄" 
      using subst_b_infer_v subst_tb.simps subst_b_simps infer_e_fstI by force
    show "atom z ♯ AE_fst (v[bv::=b]⇩v⇩b)" using infer_e_fstI subst_b_fresh_x subst_b_v_def e.fresh by metis
    show "atom z ♯ Γ[bv::=b]⇩Γ⇩b" using subst_g_b_x_fresh infer_e_fstI by auto
  qed
next
  case (infer_e_sndI Θ ℬ Γ Δ Φ v z' b1 b2 c z)
  show ?case unfolding subst_b_simps proof(rule Typing.infer_e_sndI)
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b  " using wf_b_subst(10) subst_db.simps infer_e_sndI wfX_wfY 
      by (metis wf_b_subst(15))
    show "Θ  ⊢⇩w⇩f Φ " using infer_e_sndI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v[bv::=b]⇩v⇩b ⇒ ⦃ z' : B_pair b1[bv::=b]⇩b⇩b b2[bv::=b]⇩b⇩b  | c[bv::=b]⇩c⇩b ⦄" 
      using subst_b_infer_v subst_tb.simps subst_b_simps infer_e_sndI by force
    show "atom z ♯ AE_snd (v[bv::=b]⇩v⇩b)" using infer_e_sndI subst_b_fresh_x subst_b_v_def e.fresh by metis
    show "atom z ♯ Γ[bv::=b]⇩Γ⇩b" using subst_g_b_x_fresh infer_e_sndI by auto
  qed
next
  case (infer_e_lenI Θ ℬ Γ Δ Φ v z' c z)
  show ?case unfolding subst_b_simps proof(rule Typing.infer_e_lenI)
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b  " using wf_b_subst(10) subst_db.simps infer_e_lenI wfX_wfY 
      by (metis wf_b_subst(15))
    show "Θ  ⊢⇩w⇩f Φ " using infer_e_lenI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v[bv::=b]⇩v⇩b ⇒ ⦃ z' : B_bitvec  | c[bv::=b]⇩c⇩b ⦄" 
      using subst_b_infer_v subst_tb.simps subst_b_simps infer_e_lenI by force
    show "atom z ♯ AE_len (v[bv::=b]⇩v⇩b)" using infer_e_lenI subst_b_fresh_x subst_b_v_def e.fresh by metis
    show "atom z ♯ Γ[bv::=b]⇩Γ⇩b" using subst_g_b_x_fresh infer_e_lenI by auto
  qed
next
  case (infer_e_mvarI Θ ℬ Γ Φ Δ u τ)
  show ?case proof(subst  subst subst_eb.simps, rule Typing.infer_e_mvarI)
    show "Θ ; {||}  ⊢⇩w⇩f Γ[bv::=b]⇩Γ⇩b " using infer_e_mvarI wf_b_subst by auto
    show "Θ  ⊢⇩w⇩f Φ "  using infer_e_mvarI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b "   using infer_e_mvarI  using wf_b_subst(10) subst_db.simps infer_e_sndI wfX_wfY 
      by (metis wf_b_subst(15))
    show "(u, τ[bv::=b]⇩τ⇩b) ∈ setD Δ[bv::=b]⇩Δ⇩b"  using infer_e_mvarI subst_db.simps set_insert 
        subst_d_b_member by simp
  qed
next
  case (infer_e_concatI Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 c2 z3)
  show ?case unfolding subst_b_simps proof(rule Typing.infer_e_concatI)
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b " using wf_b_subst(10) subst_db.simps infer_e_concatI wfX_wfY 
      by (metis wf_b_subst(15))
    show "Θ  ⊢⇩w⇩f Φ " using infer_e_concatI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v1[bv::=b]⇩v⇩b ⇒ ⦃ z1 : B_bitvec  | c1[bv::=b]⇩c⇩b ⦄" 
      using subst_b_infer_v subst_tb.simps subst_b_simps infer_e_concatI by force
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v2[bv::=b]⇩v⇩b ⇒ ⦃ z2 : B_bitvec  | c2[bv::=b]⇩c⇩b ⦄" 
      using subst_b_infer_v subst_tb.simps subst_b_simps infer_e_concatI by force
    show "atom z3 ♯ AE_concat (v1[bv::=b]⇩v⇩b) (v2[bv::=b]⇩v⇩b)" using infer_e_concatI subst_b_fresh_x subst_b_v_def e.fresh by metis
    show "atom z3 ♯ Γ[bv::=b]⇩Γ⇩b" using subst_g_b_x_fresh infer_e_concatI by auto
  qed
next
  case (infer_e_splitI Θ ℬ Γ Δ Φ v1 z1 c1 v2 z2 z3)
  show ?case unfolding subst_b_simps proof(rule Typing.infer_e_splitI)
    show ‹ Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b › using wf_b_subst(10) subst_db.simps infer_e_splitI wfX_wfY 
      by (metis wf_b_subst(15))
    show ‹ Θ  ⊢⇩w⇩f Φ ›  using infer_e_splitI by auto
    show ‹ Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v1[bv::=b]⇩v⇩b ⇒ ⦃ z1 : B_bitvec  | c1[bv::=b]⇩c⇩b ⦄›  
      using subst_b_infer_v subst_tb.simps subst_b_simps infer_e_splitI by force
    show ‹Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ v2[bv::=b]⇩v⇩b ⇐ ⦃ z2 : B_int  | [ leq [ [ L_num 0 ]⇧v ]⇧c⇧e [ [ z2 ]⇧v ]⇧c⇧e ]⇧c⇧e  ==  [ [ L_true ]⇧v ]⇧c⇧e   AND
                  [ leq [ [ z2 ]⇧v ]⇧c⇧e [| [ v1[bv::=b]⇩v⇩b ]⇧c⇧e |]⇧c⇧e ]⇧c⇧e  ==  [ [ L_true ]⇧v ]⇧c⇧e   ⦄›  
      using subst_b_check_v subst_tb.simps subst_b_simps infer_e_splitI 
    proof -
      have "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢ v2[bv::=b]⇩v⇩b ⇐ ⦃ z2 : B_int | [ leq [ [ L_num 0 ]⇧v ]⇧c⇧e [ [ z2 ]⇧v ]⇧c⇧e ]⇧c⇧e == [ [ L_true ]⇧v ]⇧c⇧e AND [ leq [ [ z2 ]⇧v ]⇧c⇧e [| [ v1 ]⇧c⇧e |]⇧c⇧e ]⇧c⇧e == [ [ L_true ]⇧v ]⇧c⇧e ⦄[bv::=b]⇩τ⇩b"
        using infer_e_splitI.hyps(7) infer_e_splitI.prems(1) infer_e_splitI.prems(2) subst_b_check_v by presburger (* 0.0 ms *)
      then show ?thesis
        by simp (* 0.0 ms *)
    qed
    show ‹atom z1 ♯ AE_split (v1[bv::=b]⇩v⇩b) (v2[bv::=b]⇩v⇩b)› using infer_e_splitI subst_b_fresh_x subst_b_v_def e.fresh by metis
    show ‹atom z1 ♯ Γ[bv::=b]⇩Γ⇩b› using subst_g_b_x_fresh infer_e_splitI by auto

    show ‹atom z2 ♯ AE_split (v1[bv::=b]⇩v⇩b) (v2[bv::=b]⇩v⇩b)›  using infer_e_splitI subst_b_fresh_x subst_b_v_def e.fresh by metis

    show ‹atom z2 ♯ Γ[bv::=b]⇩Γ⇩b› using subst_g_b_x_fresh infer_e_splitI by auto
    show ‹atom z3 ♯ AE_split (v1[bv::=b]⇩v⇩b) (v2[bv::=b]⇩v⇩b)›  using infer_e_splitI subst_b_fresh_x subst_b_v_def e.fresh by metis
    show ‹atom z3 ♯ Γ[bv::=b]⇩Γ⇩b› using subst_g_b_x_fresh infer_e_splitI by auto
  qed
qed

text ‹This is needed for preservation. When we apply a function "f [b] v" we need to 
substitute into the body of the function f replacing type-variable with b›

lemma subst_b_c_of_forget:
  assumes "atom bv ♯ const"
  shows "(c_of const x)[bv::=b]⇩c⇩b = c_of const x" 
  using assms proof(nominal_induct const avoiding: x rule:τ.strong_induct)
  case (T_refined_type x' b' c')
  hence "c_of ⦃ x' : b' | c' ⦄ x = c'[x'::=V_var x]⇩c⇩v" using c_of.simps by metis
  moreover have "atom bv ♯ c'[x'::=V_var x]⇩c⇩v" proof -
    have "atom bv ♯ c'" using T_refined_type τ.fresh by simp
    moreover have "atom bv ♯ V_var x" using v.fresh by simp
    ultimately show ?thesis   
      using T_refined_type τ.fresh subst_b_c_def fresh_subst_if
        τ_fresh_c fresh_subst_cv_if has_subst_b_class.subst_b_fresh_x ms_fresh_all(37) ms_fresh_all assms by metis
  qed
  ultimately show ?case using forget_subst subst_b_c_def by metis
qed

lemma subst_b_check_s:
  fixes s::s and b::b and cs::branch_s and css::branch_list and v::v and τ::τ
  assumes "Θ ; {||} ⊢⇩w⇩f b"  and "B = {|bv|}" (*and "D = []"*)
  shows  "Θ ; Φ ; B ; G; D ⊢ s ⇐ τ ⟹ Θ ; Φ ; {||} ; G[bv::=b]⇩Γ⇩b; D[bv::=b]⇩Δ⇩b ⊢ (s[bv::=b]⇩s⇩b) ⇐ (τ[bv::=b]⇩τ⇩b)" and
    "Θ ; Φ ; B ; G; D ; tid ; cons ; const ; v ⊢ cs ⇐ τ ⟹ Θ ; Φ ; {||} ; G[bv::=b]⇩Γ⇩b; D[bv::=b]⇩Δ⇩b ; tid ; cons ; const ; v[bv::=b]⇩v⇩b ⊢ (subst_branchb cs bv b) ⇐ (τ[bv::=b]⇩τ⇩b)" and
    "Θ ; Φ ; B ; G; D ; tid ; dclist ; v ⊢ css ⇐ τ ⟹ Θ ; Φ ; {||} ; G[bv::=b]⇩Γ⇩b; D[bv::=b]⇩Δ⇩b ; tid ; dclist ; v[bv::=b]⇩v⇩b ⊢ (subst_branchlb css bv b ) ⇐ (τ[bv::=b]⇩τ⇩b)" 
  using assms proof(induct  rule: check_s_check_branch_s_check_branch_list.inducts)
  note facts = wfD_emptyI wfX_wfY wf_b_subst subst_b_subtype subst_b_infer_v
  case (check_valI Θ ℬ Γ Δ Φ v τ' τ)
  show ?case 
    apply(subst subst_sb.simps, rule Typing.check_valI) 
    using facts check_valI apply metis
    using check_valI subst_b_infer_v wf_b_subst subst_b_subtype apply blast
    using check_valI subst_b_infer_v wf_b_subst subst_b_subtype apply blast  
    using check_valI subst_b_infer_v wf_b_subst subst_b_subtype by metis
next
  case (check_letI x Θ Φ ℬ Γ Δ e τ z s b' c)
  show ?case proof(subst subst_sb.simps, rule Typing.check_letI) 

    show "atom x ♯(Θ, Φ, {||}, Γ[bv::=b]⇩Γ⇩b, Δ[bv::=b]⇩Δ⇩b, e[bv::=b]⇩e⇩b, τ[bv::=b]⇩τ⇩b)" (*using check_letI  subst_b_τ_def subst_b_Γ_def subst_b_fresh_x fresh_prod4 subst_b_c_def sory*)
      apply(unfold fresh_prodN,auto)
      apply(simp add: check_letI fresh_empty_fset)+
      apply(metis *   subst_b_fresh_x check_letI fresh_prodN)+ done
    show "atom z ♯ (x, Θ, Φ, {||}, Γ[bv::=b]⇩Γ⇩b, Δ[bv::=b]⇩Δ⇩b, e[bv::=b]⇩e⇩b, τ[bv::=b]⇩τ⇩b, s[bv::=b]⇩s⇩b)"  
      apply(unfold fresh_prodN,auto)
      apply(simp add: check_letI fresh_empty_fset)+
      apply(metis *   subst_b_fresh_x check_letI fresh_prodN)+ done
    show "Θ ; Φ ; {||} ; Γ[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b  ⊢ e[bv::=b]⇩e⇩b ⇒ ⦃ z : b'[bv::=b]⇩b⇩b  | c[bv::=b]⇩c⇩b  ⦄" 
      using check_letI subst_b_infer_e subst_tb.simps by metis
    have "c[z::=[ x ]⇧v]⇩c⇩v[bv::=b]⇩c⇩b =  (c[bv::=b]⇩c⇩b)[z::=V_var x]⇩c⇩v" 
      using subst_cv_subst_bb_commute[of bv "V_var x" c z b] fresh_at_base by simp
    thus "Θ ; Φ ; {||} ; ((x, b'[bv::=b]⇩b⇩b , (c[bv::=b]⇩c⇩b)[z::=V_var x]⇩v) #⇩Γ Γ[bv::=b]⇩Γ⇩b) ; Δ[bv::=b]⇩Δ⇩b  ⊢ s[bv::=b]⇩s⇩b ⇐ τ[bv::=b]⇩τ⇩b" 
      using check_letI subst_gb.simps subst_defs by metis
  qed
next
  case (check_assertI x Θ Φ ℬ Γ Δ c τ s)
  show ?case proof(subst subst_sb.simps, rule Typing.check_assertI)
    show "atom x ♯ (Θ, Φ, {||}, Γ[bv::=b]⇩Γ⇩b, Δ[bv::=b]⇩Δ⇩b,  c[bv::=b]⇩c⇩b, τ[bv::=b]⇩τ⇩b, s[bv::=b]⇩s⇩b)"   
      apply(unfold fresh_prodN,auto)
      apply(simp add: check_assertI fresh_empty_fset)+
      apply(metis *   subst_b_fresh_x check_assertI fresh_prodN)+ done

    have "Θ ; Φ ; {||} ; ((x, B_bool, c) #⇩Γ Γ)[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b  ⊢ s[bv::=b]⇩s⇩b ⇐ τ[bv::=b]⇩τ⇩b" using  check_assertI
      by metis
    thus "Θ ; Φ ; {||} ; (x, B_bool, c[bv::=b]⇩c⇩b) #⇩Γ Γ[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b  ⊢ s[bv::=b]⇩s⇩b ⇐ τ[bv::=b]⇩τ⇩b" using  subst_gb.simps by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊨ c[bv::=b]⇩c⇩b " using subst_b_valid  check_assertI by simp
    show " Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b " using wf_b_subst2(6) check_assertI by simp
  qed
next
  case (check_branch_list_consI Θ Φ ℬ Γ Δ tid dclist v cs τ css)
  then show ?case unfolding subst_branchlb.simps using Typing.check_branch_list_consI by simp
next
  case (check_branch_list_finalI Θ Φ ℬ Γ Δ tid dclist v cs τ)
  then show ?case unfolding subst_branchlb.simps using Typing.check_branch_list_finalI by simp
next
  case (check_branch_s_branchI Θ ℬ Γ Δ τ const x Φ tid cons v s)

  show ?case unfolding subst_b_simps proof(rule Typing.check_branch_s_branchI) 
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b  "  using check_branch_s_branchI wf_b_subst subst_db.simps by metis
    show "⊢⇩w⇩f Θ " using check_branch_s_branchI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b   ⊢⇩w⇩f τ[bv::=b]⇩τ⇩b "   using check_branch_s_branchI wf_b_subst by metis

    show "atom x ♯(Θ, Φ, {||}, Γ[bv::=b]⇩Γ⇩b, Δ[bv::=b]⇩Δ⇩b, tid, cons , const, v[bv::=b]⇩v⇩b, τ[bv::=b]⇩τ⇩b)"       
      apply(unfold fresh_prodN,auto)
      apply(simp add: check_branch_s_branchI fresh_empty_fset)+
      apply(metis *   subst_b_fresh_x check_branch_s_branchI fresh_prodN)+
      done
    show wft:"Θ ; {||} ; GNil ⊢⇩w⇩f  const" using check_branch_s_branchI  by auto
    hence "(b_of const) = (b_of const)[bv::=b]⇩b⇩b" 
      using wfT_nil_supp   fresh_def[of "atom bv" ] forget_subst subst_b_b_def τ.supp
        bot.extremum_uniqueI ex_in_conv fresh_def supp_empty_fset 
      by (metis b_of_supp)
    moreover have "(c_of const x)[bv::=b]⇩c⇩b = c_of const x" 
      using wft   wfT_nil_supp   fresh_def[of "atom bv" ] forget_subst subst_b_c_def τ.supp
        bot.extremum_uniqueI ex_in_conv fresh_def supp_empty_fset  subst_b_c_of_forget by metis
    ultimately show  "Θ ; Φ ; {||} ; (x, b_of const, CE_val (v[bv::=b]⇩v⇩b)  ==  CE_val(V_cons tid cons (V_var x)) AND c_of const x) #⇩Γ Γ[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b   ⊢ s[bv::=b]⇩s⇩b ⇐ τ[bv::=b]⇩τ⇩b"  
      using check_branch_s_branchI subst_gb.simps by auto
  qed
next
  case (check_ifI z Θ Φ ℬ Γ Δ v s1 s2 τ)
  show ?case unfolding subst_b_simps proof(rule  Typing.check_ifI) 
    show ‹atom z ♯ (Θ, Φ, {||}, Γ[bv::=b]⇩Γ⇩b, Δ[bv::=b]⇩Δ⇩b, v[bv::=b]⇩v⇩b, s1[bv::=b]⇩s⇩b, s2[bv::=b]⇩s⇩b, τ[bv::=b]⇩τ⇩b)› 
      by(unfold fresh_prodN,auto, auto simp add: check_ifI fresh_empty_fset subst_b_fresh_x )
    have "⦃ z : B_bool  | TRUE ⦄[bv::=b]⇩τ⇩b  = ⦃ z : B_bool  | TRUE ⦄"  by auto
    thus ‹Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ v[bv::=b]⇩v⇩b ⇐ ⦃ z : B_bool  | TRUE ⦄› using check_ifI subst_b_check_v by metis
    show ‹ Θ ; Φ ; {||} ; Γ[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b  ⊢ s1[bv::=b]⇩s⇩b ⇐ ⦃ z : b_of τ[bv::=b]⇩τ⇩b  | CE_val (v[bv::=b]⇩v⇩b)  ==  CE_val (V_lit L_true)   IMP  c_of τ[bv::=b]⇩τ⇩b z  ⦄› 
      using subst_b_if check_ifI by metis
    show ‹ Θ ; Φ ; {||} ; Γ[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b  ⊢ s2[bv::=b]⇩s⇩b ⇐ ⦃ z : b_of τ[bv::=b]⇩τ⇩b  | CE_val (v[bv::=b]⇩v⇩b)  ==  CE_val (V_lit L_false)   IMP  c_of τ[bv::=b]⇩τ⇩b z  ⦄› 
      using subst_b_if check_ifI by metis
  qed
next
  case (check_let2I x Θ Φ ℬ G Δ t s1 τ s2 )
  show ?case unfolding subst_b_simps proof (rule Typing.check_let2I)
    have "atom x ♯ b" using x_fresh_b by auto
    show ‹atom x ♯ (Θ, Φ, {||}, G[bv::=b]⇩Γ⇩b, Δ[bv::=b]⇩Δ⇩b, t[bv::=b]⇩τ⇩b, s1[bv::=b]⇩s⇩b, τ[bv::=b]⇩τ⇩b)›      
      apply(unfold fresh_prodN, auto, auto simp add: check_let2I fresh_prodN fresh_empty_fset)
      apply(metis  subst_b_fresh_x check_let2I fresh_prodN)+
      done

    show ‹ Θ ; Φ ; {||} ; G[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b  ⊢ s1[bv::=b]⇩s⇩b ⇐ t[bv::=b]⇩τ⇩b › using check_let2I subst_tb.simps  by auto
    show ‹ Θ ; Φ ; {||} ; (x, b_of t[bv::=b]⇩τ⇩b, c_of t[bv::=b]⇩τ⇩b x) #⇩Γ G[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b  ⊢ s2[bv::=b]⇩s⇩b ⇐ τ[bv::=b]⇩τ⇩b› 
      using check_let2I subst_tb.simps  subst_gb.simps b_of.simps subst_b_c_of subst_b_b_of by auto
  qed
next
  case (check_varI u Θ Φ ℬ Γ Δ τ' v τ s)
  show ?case unfolding subst_b_simps proof(rule Typing.check_varI) 
    show "atom u ♯  (Θ, Φ, {||}, Γ[bv::=b]⇩Γ⇩b, Δ[bv::=b]⇩Δ⇩b, τ'[bv::=b]⇩τ⇩b, v[bv::=b]⇩v⇩b, τ[bv::=b]⇩τ⇩b) "
      by(unfold fresh_prodN,auto simp add: check_varI fresh_empty_fset subst_b_fresh_u )
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ v[bv::=b]⇩v⇩b ⇐ τ'[bv::=b]⇩τ⇩b" using check_varI subst_b_check_v by auto
    show "Θ ; Φ ; {||} ; (subst_gb  Γ bv b) ; (u, (τ'[bv::=b]⇩τ⇩b)) #⇩Δ (subst_db  Δ bv b)   ⊢ (s[bv::=b]⇩s⇩b) ⇐ (τ[bv::=b]⇩τ⇩b)" using check_varI by auto
  qed
next
  case (check_assignI Θ Φ ℬ Γ Δ u τ v z τ')
  show ?case unfolding subst_b_simps proof( rule Typing.check_assignI) 
    show "Θ  ⊢⇩w⇩f Φ " using check_assignI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f Δ[bv::=b]⇩Δ⇩b " using wf_b_subst check_assignI by auto
    show "(u, τ[bv::=b]⇩τ⇩b) ∈ setD Δ[bv::=b]⇩Δ⇩b" using check_assignI subst_d_b_member  by simp
    show " Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ v[bv::=b]⇩v⇩b ⇐ τ[bv::=b]⇩τ⇩b"  using check_assignI subst_b_check_v by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ ⦃ z : B_unit  | TRUE ⦄ ≲ τ'[bv::=b]⇩τ⇩b" using check_assignI subst_b_subtype subst_b_simps subst_tb.simps by fastforce
  qed
next
  case (check_whileI Θ Φ ℬ Γ Δ s1 z s2 τ')
  show ?case unfolding subst_b_simps proof(rule Typing.check_whileI) 
    show "Θ ; Φ ; {||} ; Γ[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b  ⊢ s1[bv::=b]⇩s⇩b ⇐ ⦃ z : B_bool  | TRUE ⦄" using check_whileI by auto
    show "Θ ; Φ ; {||} ; Γ[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b  ⊢ s2[bv::=b]⇩s⇩b ⇐ ⦃ z : B_unit  | TRUE ⦄" using check_whileI by auto
    show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ ⦃ z : B_unit  | TRUE ⦄ ≲ τ'[bv::=b]⇩τ⇩b"  using subst_b_subtype check_whileI by fastforce
  qed     
next
  case (check_seqI Θ Φ ℬ Γ Δ s1 z s2 τ)
  then show ?case unfolding subst_sb.simps using check_seqI Typing.check_seqI subst_b_eq by metis
next
  case (check_caseI Θ Φ ℬ  Γ Δ tid dclist v cs τ  z)
  show ?case unfolding subst_b_simps proof(rule Typing.check_caseI)
    show ‹ Θ ;  Φ ; {||} ; Γ[bv::=b]⇩Γ⇩b ; Δ[bv::=b]⇩Δ⇩b ; tid ; dclist ; v[bv::=b]⇩v⇩b ⊢ subst_branchlb cs bv b ⇐ τ[bv::=b]⇩τ⇩b› using check_caseI by auto
    show ‹AF_typedef tid dclist ∈ set Θ› using check_caseI by auto
    show ‹Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b  ⊢ v[bv::=b]⇩v⇩b ⇐ ⦃ z : B_id tid  | TRUE ⦄› using check_caseI subst_b_check_v subst_b_simps subst_tb.simps subst_b_simps       
    proof -
      have "⦃ z : B_id tid | TRUE ⦄ = ⦃ z : B_id tid | TRUE ⦄[bv::=b]⇩τ⇩b" using subst_b_eq by auto
      then show ?thesis
        by (metis (no_types) check_caseI.hyps(4) check_caseI.prems(1) check_caseI.prems(2) subst_b_check_v) (* 31 ms *)
    qed
    show ‹   ⊢⇩w⇩f Θ › using check_caseI by auto
  qed
qed

end