(*<*)
theory TypingL
  imports Typing RCLogicL "HOL-Eisbach.Eisbach"
begin
  (*>*)

chapter  ‹Typing Lemmas›

section ‹Prelude›

text ‹Needed as the typing elimination rules give us facts for an alpha-equivalent version of a term
 and so need to be able to 'jump back' to a typing judgement for the orginal term›

lemma τ_fresh_c[simp]:
  assumes "atom x ♯ { z : b | c }" and "atom z ♯ x"
  shows "atom x ♯ c"
  using τ.fresh assms fresh_at_base 
  by (simp add: fresh_at_base(2))

lemmas subst_defs = subst_b_b_def subst_b_c_def subst_b_τ_def subst_v_v_def subst_v_c_def subst_v_τ_def

lemma wfT_wfT_if1:
  assumes "wfT Θ B Γ ({ z : b_of t | CE_val v == CE_val (V_lit L_false) IMP c_of t z })" and "atom z ♯ (Γ,t)"
  shows "wfT Θ B Γ t" 
  using assms proof(nominal_induct t avoiding: Γ z rule: τ.strong_induct)
  case (T_refined_type z' b' c')
  show ?case proof(rule wfT_wfT_if)
    show ‹ Θ; B; Γ ⊨_wf { z : b' | [ v ]^ce == [ [ L_false ]^v ]^ce IMP c'[z'::=[ z]^v]_cv } ›
      using T_refined_type b_of.simps c_of.simps subst_defs by metis
    show ‹atom z ♯ (c', Γ)› using T_refined_type fresh_prodN τ_fresh_c by metis
  qed
qed

lemma fresh_u_replace_true:
  fixes bv::bv and Γ::Γ
  assumes "atom bv ♯ Γ' @ (x, b, c) #_\<Gamma> Γ"
  shows "atom bv ♯ Γ' @ (x, b, TRUE) #_\<Gamma> Γ"
  using fresh_append_g fresh_GCons assms fresh_Pair c.fresh(1) by auto

lemma wf_replace_true1:
  fixes Γ::Γ and Φ::Φ and Θ::Θ and  Γ'::Γ and v::v and e::e and c::c and c''::c and c'::c and τ::τ and ts::"(string*τ) list" and Δ::Δ and b'::b and b::b and s::s  
    and ftq::fun_typ_q and ft::fun_typ and ce::ce and td::type_def and cs::branch_s and css::branch_list

shows  "Θ; B; G ⊨_wf v : b' ==> G = Γ' @ (x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf v : b'" and
  "Θ; B; G ⊨_wf c'' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf c''" and
  "Θ ; B ⊨_wf G ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ⊨_wf Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) " and
  "Θ; B; G ⊨_wf τ ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf τ" and
  "Θ; B; Γ ⊨_wf ts ==> True" and 
  "⊨_wf P ==> True" and
  "Θ ; B ⊨_wf b ==> True" and
  "Θ ; B ; G ⊨_wf ce : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf ce : b'" and
  "Θ ⊨_wf td ==> True"
proof(nominal_induct   
    b' and c'' and G and τ and ts and P and b and b' and td 
    arbitrary: Γ Γ'  and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ'
    rule:wfV_wfC_wfG_wfT_wfTs_wfTh_wfB_wfCE_wfTD.strong_induct)
  case (wfB_intI Θ B)
  then show ?case using wf_intros by metis
next
  case (wfB_boolI Θ B)
  then show ?case using wf_intros by metis
next
  case (wfB_unitI Θ B)
  then show ?case using wf_intros by metis
next
  case (wfB_bitvecI Θ B)
  then show ?case using wf_intros by metis
next
  case (wfB_pairI Θ B b1 b2)
  then show ?case using wf_intros by metis
next
  case (wfB_consI Θ s dclist B)
  then show ?case using wf_intros by metis
next
  case (wfB_appI Θ b s bv dclist B)
  then show ?case using wf_intros by metis
next
  case (wfV_varI Θ B Γ'' b' c x')
  hence wfg: ‹ Θ ; B ⊨_wf Γ' @ (x, b, TRUE) #_\Γ Γ › by auto
  show ?case proof(cases "x=x'")
    case True
    hence "Some (b, TRUE) = lookup (Γ' @ (x, b, TRUE) #_\<Gamma> Γ) x'" using lookup.simps lookup_inside_wf wfg by simp
    thus ?thesis using Wellformed.wfV_varI[OF wfg] 
      by (metis True lookup_inside_wf old.prod.inject option.inject wfV_varI.hyps(1) wfV_varI.hyps(3) wfV_varI.prems)        
  next
    case False
    hence "Some (b', c) = lookup (Γ' @ (x, b, TRUE) #_\<Gamma> Γ) x'" using  lookup_inside2  wfV_varI by metis
    then show ?thesis using Wellformed.wfV_varI[OF wfg]                                     
      by (metis wfG_elim2 wfG_suffix wfV_varI.hyps(1) wfV_varI.hyps(2) wfV_varI.hyps(3) 
          wfV_varI.prems Wellformed.wfV_varI wf_replace_inside(1))
  qed
next
  case (wfV_litI Θ B Γ l)
  then show ?case using wf_intros using wf_intros by metis
next
  case (wfV_pairI Θ B Γ v1 b1 v2 b2)
  then show ?case using wf_intros by metis
next
  case (wfV_consI s dclist Θ dc x b' c B Γ v)
  then show ?case using wf_intros by metis
next
  case (wfV_conspI s bv dclist Θ dc xc bc cc B b' Γ'' v)
  show ?case proof 
    show ‹AF_typedef_poly s bv dclist ∈ set Θ› using wfV_conspI by metis
    show ‹(dc, { xc : bc | cc }) ∈ set dclist›  using wfV_conspI by metis
    show ‹ Θ ;B ⊨_wf b' ›  using wfV_conspI by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf v : bc[bv::=b']_bb ›  using wfV_conspI by metis
    have "atom bv ♯ Γ' @ (x, b, TRUE) #_\<Gamma> Γ" using fresh_u_replace_true wfV_conspI by metis
    thus  ‹atom bv ♯ (Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, b', v)›  using wfV_conspI fresh_prodN by metis
  qed
next
  case (wfCE_valI Θ B Γ v b)
  then show ?case using wf_intros by metis
next
  case (wfCE_plusI Θ B Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_leqI Θ B Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_eqI Θ B Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_fstI Θ B Γ v1 b1 b2)
  then show ?case using wf_intros by metis
next
  case (wfCE_sndI Θ B Γ v1 b1 b2)
  then show ?case using wf_intros by metis
next
  case (wfCE_concatI Θ B Γ v1 v2)
  then show ?case using wf_intros by metis
next
  case (wfCE_lenI Θ B Γ v1)
  then show ?case using wf_intros by metis
next
  case (wfTI z Θ B Γ''  b' c')
  show ?case proof
    show ‹atom z ♯ (Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ)›  using wfTI fresh_append_g fresh_GCons fresh_prodN  by auto
    show ‹ Θ ; B ⊨_wf b' › using wfTI by metis
    show ‹ Θ; B; (z, b', TRUE) #_\Γ Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf c' ›  using wfTI append_g.simps by metis
  qed
next
  case (wfC_eqI Θ B Γ e1 b e2)
  then show ?case using wf_intros by metis
next
  case (wfC_trueI Θ B Γ)
  then show ?case using wf_intros by metis
next
  case (wfC_falseI Θ B Γ)
  then show ?case using wf_intros by metis
next
  case (wfC_conjI Θ B Γ c1 c2)
  then show ?case using wf_intros by metis
next
  case (wfC_disjI Θ B Γ c1 c2)
  then show ?case using wf_intros by metis
next
  case (wfC_notI Θ B Γ c1)
  then show ?case using wf_intros by metis
next
  case (wfC_impI Θ B Γ c1 c2)
  then show ?case using wf_intros by metis
next
  case (wfG_nilI Θ B)
  then show ?case  using GNil_append by blast
next
  case (wfG_cons1I c Θ B Γ'' x b)
  then show ?case using wf_intros wfG_cons_TRUE2 wfG_elims(2) wfG_replace_inside wfG_suffix
    by (metis (no_types, lifting))
next
  case (wfG_cons2I c Θ B Γ'' x' b)
  then show ?case using wf_intros 
    by (metis wfG_cons_TRUE2 wfG_elims(2) wfG_replace_inside wfG_suffix)
next
  case wfTh_emptyI
  then show ?case  using wf_intros by metis
next
  case (wfTh_consI tdef Θ)
  then show ?case  using wf_intros by metis
next
  case (wfTD_simpleI Θ lst s)
  then show ?case  using wf_intros by metis
next
  case (wfTD_poly Θ bv lst s)
  then show ?case  using wf_intros by metis
next
  case (wfTs_nil Θ B Γ)
  then show ?case  using wf_intros by metis
next
  case (wfTs_cons Θ B Γ τ dc ts)
  then show ?case  using wf_intros by metis
qed

lemma wf_replace_true2:
  fixes Γ::Γ and Φ::Φ and Θ::Θ and  Γ'::Γ and v::v and e::e and c::c and c''::c and c'::c and τ::τ and ts::"(string*τ) list" and Δ::Δ and b'::b and b::b and s::s  
    and ftq::fun_typ_q and ft::fun_typ and ce::ce and td::type_def and cs::branch_s and css::branch_list

shows   "Θ ; Φ ; B ; G ; D ⊨_wf e : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; Φ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ); D ⊨_wf e : b'" and
  "Θ ; Φ ; B ; G ; Δ ⊨_wf s : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; Φ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ; Δ ⊨_wf s : b'" and
  "Θ ; Φ ; B ; G ; Δ ; tid ; dc ; t ⊨_wf cs : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; Φ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ; Δ ; tid ; dc ; t ⊨_wf cs : b'" and
  "Θ ; Φ ; B ; G ; Δ ; tid ; dclist ⊨_wf css : b' ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; Φ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ; Δ ; tid ; dclist ⊨_wf css : b'" and

"Θ ⊨_wf Φ ==> True" and
"Θ; B; G ⊨_wf Δ ==> G = Γ' @(x, b, c) #_\<Gamma> Γ ==> Θ ; B ; Γ' @ ((x, b, TRUE) #_\<Gamma> Γ) ⊨_wf Δ" and

"Θ ; Φ ⊨_wf ftq ==> True" and
"Θ ; Φ ; B ⊨_wf ft ==> True"
proof(nominal_induct   
    b' and b' and b' and b' and Φ and Δ and ftq and ft 
    arbitrary: Γ Γ'  and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ' and Γ Γ'
    rule:wfE_wfS_wfCS_wfCSS_wfPhi_wfD_wfFTQ_wfFT.strong_induct)

  case (wfE_valI Θ Φ B Γ Δ v b)
  then show ?case using wf_intros using wf_intros wf_replace_true1 by metis
next
  case (wfE_plusI Θ Φ B Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_leqI Θ Φ B Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_eqI Θ Φ B Γ Δ v1 b v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_fstI Θ Φ B Γ Δ v1 b1 b2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_sndI Θ Φ B Γ Δ v1 b1 b2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_concatI Θ Φ B Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_splitI Θ Φ B Γ Δ v1 v2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_lenI Θ Φ B Γ Δ v1)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_appI Θ Φ B Γ Δ f x b c τ s v)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfE_appPI Θ Φ B Γ'' Δ b' bv v τ f x1 b1 c1 s)
  show ?case proof
    show ‹ Θ ⊨_wf Φ › using wfE_appPI wf_replace_true1 by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfE_appPI by metis
    show ‹ Θ ; B ⊨_wf b' › using wfE_appPI by metis
    have "atom bv ♯ Γ' @ (x, b, TRUE) #_\<Gamma> Γ" using fresh_u_replace_true wfE_appPI fresh_prodN by metis
    thus  ‹atom bv ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, b', v, (b_of τ)[bv::=b']_b)›
      using wfE_appPI fresh_prodN by auto
    show ‹Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x1 b1 c1 τ s))) = lookup_fun Φ f› using wfE_appPI by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf v : b1[bv::=b']_b › using wfE_appPI wf_replace_true1 by metis
  qed
next
  case (wfE_mvarI Θ Φ B Γ Δ u τ)
  then show ?case using wf_intros wf_replace_true1 by metis
next

  case (wfS_valI Θ Φ B Γ v b Δ)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_letI  Θ Φ B Γ'' Δ e b' x1 s b1)
  show ?case proof 
    show ‹ Θ ; Φ ; B ; Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf e : b' › using wfS_letI wf_replace_true1 by metis
    have  ‹ Θ ; Φ ; B ; ((x1, b', TRUE) #_\Γ Γ') @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b1 › apply(rule  wfS_letI(4))
      using wfS_letI  append_g.simps by simp
    thus  ‹ Θ ; Φ ; B ; (x1, b', TRUE) #_\Γ Γ'@ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b1 › using append_g.simps by auto
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfS_letI by metis
    show "atom x1 ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\<Gamma> Γ, Δ, e, b1)" using fresh_append_g fresh_GCons fresh_prodN wfS_letI by auto
  qed
next
  case (wfS_assertI Θ Φ B x' c Γ'' Δ s b')
  show ?case proof
    show ‹ Θ ; Φ ; B ; (x', B_bool, c) #_\Γ Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b' ›
      using wfS_assertI (2)[of "(x', B_bool, c) #_\<Gamma> Γ'" Γ] wfS_assertI by simp
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf c › using wfS_assertI wf_replace_true1 by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfS_assertI by metis    
    show  ‹atom x' ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, c, b', s)› using wfS_assertI fresh_prodN by simp
  qed
next
  case (wfS_let2I  Θ Φ B Γ'' Δ s1 τ  x' s2 ba')
  show ?case proof
    show ‹ Θ ; Φ ; B ; Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s1 : b_of τ › using wfS_let2I wf_replace_true1 by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf τ ›  using wfS_let2I wf_replace_true1 by metis
    have  ‹ Θ ; Φ ; B ; ((x', b_of τ, TRUE) #_\Γ Γ') @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s2 : ba' ›  
      apply(rule wfS_let2I(5))
      using wfS_let2I append_g.simps by auto
    thus ‹ Θ ; Φ ; B ; (x', b_of τ, TRUE) #_\Γ Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s2 : ba' ›  using wfS_let2I append_g.simps by auto
    show ‹atom x' ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, s1, ba', τ)›   using fresh_append_g fresh_GCons fresh_prodN wfS_let2I by auto
  qed
next
  case (wfS_ifI Θ B Γ v Φ Δ s1 b s2)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_varI Θ B Γ'' τ v u Φ Δ  b' s)
  show ?case proof
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf τ › using wfS_varI wf_replace_true1 by metis
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf v : b_of τ ›  using wfS_varI wf_replace_true1 by metis
    show ‹atom u ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, τ, v, b')›  using wfS_varI u_fresh_g fresh_prodN by auto
    show ‹ Θ ; Φ ; B ; Γ' @ (x, b, TRUE) #_\Γ Γ ; (u, τ) #_\Δ Δ ⊨_wf s : b' ›  using wfS_varI by metis
  qed

next
  case (wfS_assignI u τ Δ Θ B Γ Φ v)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_whileI Θ Φ B Γ Δ s1 s2 b)
  then show ?case using wf_intros wf_replace_true1 by metis
next
  case (wfS_seqI Θ Φ B Γ Δ s1 s2 b)
  then show ?case using wf_intros by metis
next
  case (wfS_matchI Θ B Γ'' v tid dclist Δ Φ cs b')
  show ?case proof
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf v : B_id tid › using wfS_matchI wf_replace_true1 by auto
    show ‹AF_typedef tid dclist ∈ set Θ› using wfS_matchI by auto
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfS_matchI by auto
    show ‹ Θ ⊨_wf Φ › using wfS_matchI by auto
    show ‹ Θ ; Φ ; B ; Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ; tid ; dclist ⊨_wf cs : b' › using wfS_matchI by auto
  qed
next
  case (wfS_branchI Θ Φ B x' τ Γ'' Δ s b' tid dc)
  show ?case proof
    have ‹ Θ ; Φ ; B ; ((x', b_of τ, TRUE) #_\Γ Γ') @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b' › using wfS_branchI append_g.simps by metis
    thus  ‹ Θ ; Φ ; B ; (x', b_of τ, TRUE) #_\Γ Γ' @ (x, b, TRUE) #_\Γ Γ ; Δ ⊨_wf s : b' › using wfS_branchI append_g.simps append_g.simps by metis
    show ‹atom x' ♯ (Φ, Θ, B, Γ' @ (x, b, TRUE) #_\Γ Γ, Δ, Γ' @ (x, b, TRUE) #_\Γ Γ, τ)› using wfS_branchI by auto
    show ‹ Θ; B; Γ' @ (x, b, TRUE) #_\Γ Γ ⊨_wf Δ › using wfS_branchI by auto
  qed
next
  case (wfS_finalI Θ Φ B Γ Δ tid dc t cs b)
  then show ?case using wf_intros by metis
next
  case (wfS_cons Θ Φ B Γ Δ tid dc t cs b dclist css)
  then show ?case using wf_intros by metis
next
  case (wfD_emptyI Θ B Γ)
  then show ?case  using wf_intros wf_replace_true1 by metis
next
  case (wfD_cons Θ B Γ Δ τ u)
  then show ?case  using wf_intros wf_replace_true1 by metis
next
  case (wfPhi_emptyI Θ)
  then show ?case  using wf_intros by metis
next
  case (wfPhi_consI f Θ Φ ft)
  then show ?case  using wf_intros by metis
next
  case (wfFTNone Θ Φ ft)
  then show ?case  using wf_intros by metis
next
  case (wfFTSome Θ Φ bv ft)
  then show ?case  using wf_intros by metis
next
  case (wfFTI Θ B b Φ x c s τ)
  then show ?case  using wf_intros by metis
qed

lemmas wf_replace_true = wf_replace_true1 wf_replace_true2

section ‹Subtyping›

lemma subtype_reflI2:
  fixes τ::τ
  assumes  "Θ; B; Γ ⊨_wf τ"
  shows "Θ; B; Γ ⊨ τ < τ"
proof -
  obtain z b c where *:"τ = { z : b | c } ∧ atom z ♯ (Θ,B,Γ) ∧ Θ; B; (z, b, TRUE) #_\<Gamma> Γ ⊨_wf c" 
    using  wfT_elims(1)[OF assms] by metis
  obtain x::x where **: "atom x ♯ (Θ, B, Γ, c, z ,c, z , c )" using obtain_fresh by metis
  have "Θ; B; Γ ⊨ { z : b | c } < { z : b | c }" proof
    show "Θ; B; Γ ⊨_wf { z : b | c }" using * assms by auto
    show "Θ; B; Γ ⊨_wf { z : b | c }" using * assms by auto
    show "atom x ♯ (Θ, B, Γ, z , c , z , c )" using fresh_prod6 fresh_prod5 ** by metis
    thus  "Θ; B; (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ ⊨ c[z::=V_var x]_v " using wfT_wfC_cons assms * ** subst_v_c_def  by simp
  qed
  thus ?thesis using * by auto
qed

lemma subtype_reflI:  
  assumes "{ z1 : b | c1 } = { z2 : b | c2 }" and wf1: "Θ; B;Γ ⊨_wf ({ z1 : b | c1 })"
  shows "Θ; B; Γ ⊨ ({ z1 : b | c1 }) < ({ z2 : b | c2 })"
  using assms subtype_reflI2 by metis

nominal_function base_eq :: "Γ → τ → τ → bool" where
  "base_eq _ { z1 : b1| c1 } { z2 : b2 | c2 } = (b1 = b2)" 
  apply(auto,simp add: eqvt_def base_eq_graph_aux_def )
  by (meson τ.exhaust)
nominal_termination (eqvt)  by lexicographic_order

lemma subtype_wfT:
  fixes t1::τ and t2::τ
  assumes "Θ; B; Γ ⊨ t1 < t2" 
  shows "Θ; B; Γ ⊨_wf t1 ∧ Θ; B; Γ ⊨_wf t2"
  using assms subtype_elims by metis

lemma  subtype_eq_base:
  assumes "Θ; B; Γ ⊨ ({ z1 : b1| c1 }) < ({ z2 : b2 | c2 })"
  shows "b1=b2"
  using subtype.simps  assms by auto

lemma subtype_eq_base2: 
  assumes "Θ; B; Γ ⊨ t1 < t2"
  shows "b_of t1 = b_of t2"
  using assms proof(rule  subtype.induct[of Θ  B Γ t1 t2],goal_cases)
  case (1 Θ  Γ z1 b c1 z2 c2 x)
  then show ?case using subtype_eq_base by auto
qed

lemma  subtype_wf: 
  fixes τ1::τ and τ2::τ
  assumes "Θ; B; Γ ⊨ τ1 < τ2" 
  shows "Θ; B; Γ ⊨_wf τ1 ∧Θ; B; Γ ⊨_wf τ2"
  using assms
proof(rule  subtype.induct[of Θ B Γ τ1 τ2],goal_cases)
  case (1 Θ  ΓG z1 b c1 z2 c2 x)
  then show ?case by blast
qed

lemma  subtype_g_wf: 
  fixes τ1::τ and τ2::τ and Γ::Γ
  assumes "Θ; B; Γ ⊨ τ1 < τ2" 
  shows "Θ ; B⊨_wf Γ"
  using assms
proof(rule  subtype.induct[of Θ B Γ τ1 τ2],goal_cases)
  case (1 Θ B Γ z1 b c1 z2 c2 x)
  then show ?case using wfX_wfY by auto
qed

text ‹ For when we have a particular y that satisfies the freshness conditions that we want the validity check to use ›

lemma valid_flip_simple: 
  assumes "Θ; B; (z, b, c) #_\<Gamma> Γ ⊨ c'" and  "atom z ♯ Γ" and "atom x ♯ (z, c, z, c', Γ)"
  shows "Θ; B; (x, b, (z ↔ x ) ∙ c) #_\<Gamma> Γ ⊨ (z ↔ x ) ∙ c'"
proof -
  have "(z ↔ x ) ∙ Θ; B; (z ↔ x ) ∙ ((z, b, c) #_\<Gamma> Γ) ⊨ (z ↔ x ) ∙ c'"
    using True_eqvt valid.eqvt assms beta_flip_eq wfX_wfY by metis
  moreover have " ⊨_wf Θ" using valid.simps wfC_wf wfG_wf assms by metis
  ultimately show ?thesis 
    using theta_flip_eq G_cons_flip_fresh3[of x Γ z b c]  assms fresh_Pair flip_commute by metis
qed

lemma valid_wf_all:
  assumes " Θ; B; (z0,b,c0)#_\<Gamma>G ⊨ c"   
  shows "wfG Θ B G" and "wfC Θ B ((z0,b,c0)#_\<Gamma>G) c" and "atom z0 ♯ G"
  using valid.simps wfC_wf wfG_cons assms by metis+

lemma valid_wfT: 
  fixes z::x
  assumes " Θ; B; (z0,b,c0[z::=V_var z0]_v)#_\<Gamma>G ⊨ c[z::=V_var z0]_v" and "atom z0 ♯ (Θ, B, G,c,c0)"
  shows "Θ; B; G ⊨_wf { z : b | c0 }"    and  "Θ; B; G ⊨_wf { z : b | c }"
proof -
  have "atom z0 ♯ c0" using assms fresh_Pair by auto
  moreover have *:" Θ ; B ⊨_wf (z0,b,c0[z::=V_var z0]_cv)#_\<Gamma>G" using valid_wf_all wfX_wfY assms subst_v_c_def by metis
  ultimately show wft: "Θ; B; G ⊨_wf { z : b | c0 }"  using wfG_wfT[OF *] by auto

  have "atom z0 ♯ c" using assms fresh_Pair by auto
  moreover have wfc: "Θ; B; (z0,b,c0[z::=V_var z0]_v)#_\<Gamma>G ⊨_wf c[z::=V_var z0]_v" using valid_wf_all assms by metis
  have  "Θ; B; G ⊨_wf { z0 : b | c[z::=V_var z0]_v }" proof
    show ‹atom z0 ♯ (Θ, B, G)› using assms fresh_prodN by simp
    show ‹ Θ ; B ⊨_wf b › using wft wfT_wfB by force
    show ‹ Θ; B; (z0, b, TRUE) #_\Γ G ⊨_wf c[z::=[ z0 ]^v]_v › using wfc wfC_replace_inside[OF wfc, of GNil z0 b "c0[z::=[ z0 ]^v]_v" G C_true] wfC_trueI 
        append_g.simps 
      by (metis "local.*" wfG_elim2 wf_trans(2))
  qed
  moreover have "{ z0 : b | c[z::=V_var z0]_v } = { z : b | c }" using ‹atom z0 ♯ c0› τ.eq_iff  Abs1_eq_iff(3) 
    using calculation(1) subst_v_c_def by auto
  ultimately show   "Θ; B; G ⊨_wf { z : b | c }" by auto
qed

lemma valid_flip: 
  fixes c::c and z::x and z0::x and xx2::x
  assumes " Θ; B; (xx2, b, c0[z0::=V_var xx2]_v) #_\<Gamma> Γ ⊨ c[z::=V_var xx2]_v" and 
    "atom xx2 ♯ (c0,Γ,c,z) " and "atom z0 ♯ (Γ,c,z)"
  shows " Θ; B; (z0, b, c0) #_\<Gamma> Γ ⊨ c[z::=V_var z0]_v"
proof -

  have " ⊨_wf Θ" using assms valid_wf_all wfX_wfY by metis
  hence " Θ ; B ; (xx2 ↔ z0 ) ∙ ((xx2, b, c0[z0::=V_var xx2]_v) #_\<Gamma> Γ) ⊨ ((xx2 ↔ z0 ) ∙ c[z::=V_var xx2]_v)"
    using valid.eqvt True_eqvt assms beta_flip_eq theta_flip_eq by metis
  hence " Θ; B; (((xx2 ↔ z0 ) ∙ xx2, b, (xx2 ↔ z0 ) ∙ c0[z0::=V_var xx2]_v) #_\<Gamma> (xx2 ↔ z0 ) ∙ Γ) ⊨ ((xx2 ↔ z0 ) ∙(c[z::=V_var xx2]_v))"
    using G_cons_flip[of xx2 z0 xx2 b "c0[z0::=V_var xx2]_v" Γ] by auto
  moreover have "(xx2 ↔ z0 ) ∙ xx2 = z0" by simp
  moreover have "(xx2 ↔ z0 ) ∙ c0[z0::=V_var xx2]_v = c0" 
    using assms subst_cv_v_flip[of xx2 c0 z0 "V_var z0"] assms fresh_prod4 by auto
  moreover have "(xx2 ↔ z0 ) ∙ Γ = Γ" proof -  
    have "atom xx2 ♯ Γ" using assms by auto
    moreover have "atom z0 ♯ Γ" using assms by auto
    ultimately show ?thesis using flip_fresh_fresh by auto
  qed
  moreover have "(xx2 ↔ z0 ) ∙ (c[z::=V_var xx2]_v) =c[z::=V_var z0]_v" 
    using subst_cv_v_flip3 assms by simp
  ultimately show ?thesis by auto
qed

lemma subtype_valid:
  assumes "Θ; B; Γ ⊨ t1 < t2" and "atom y ♯ Γ" and "t1 = { z1 : b | c1 }" and "t2 = { z2 : b | c2 }"
  shows  "Θ; B; ((y, b, c1[z1::=V_var y]_v) #_\<Gamma> Γ) ⊨ c2[z2::=V_var y]_v"
  using assms proof(nominal_induct t2 avoiding: y rule: subtype.strong_induct)
  case (subtype_baseI x Θ B Γ z c z' c' ba)

  hence "(x ↔ y) ∙ Θ ; (x ↔ y) ∙ B ; (x ↔ y) ∙ ((x, ba, c[z::=[ x ]^v]_v) #_\<Gamma> Γ) ⊨ (x ↔ y) ∙ c'[z'::=[ x ]^v]_v" using valid.eqvt 
    using permute_boolI by blast
  moreover have  " ⊨_wf Θ" using valid.simps wfC_wf wfG_wf subtype_baseI by metis
  ultimately have  "Θ; B; ((y, ba, (x ↔ y) ∙ c[z::=[ x ]^v]_v) #_\<Gamma> Γ) ⊨ (x ↔ y) ∙ c'[z'::=[ x ]^v]_v" 
    using subtype_baseI theta_flip_eq beta_flip_eq τ.eq_iff  G_cons_flip_fresh3[of y Γ x ba]  by (metis flip_commute)
  moreover have "(x ↔ y) ∙ c[z::=[ x ]^v]_v = c1[z1::=[ y ]^v]_v" 
    by (metis subtype_baseI permute_flip_cancel subst_cv_id subst_cv_v_flip3 subst_cv_var_flip type_eq_subst_eq wfT_fresh_c subst_v_c_def)
  moreover have  "(x ↔ y) ∙ c'[z'::=[ x ]^v]_v = c2[z2::=[ y ]^v]_v" 
    by (metis subtype_baseI permute_flip_cancel subst_cv_id subst_cv_v_flip3 subst_cv_var_flip type_eq_subst_eq wfT_fresh_c subst_v_c_def)

  ultimately show ?case using subtype_baseI τ.eq_iff by metis
qed

lemma subtype_valid_simple:
  assumes "Θ; B; Γ ⊨ t1 < t2" and "atom z ♯ Γ" and "t1 = { z : b | c1 }" and "t2 = { z : b | c2 }"
  shows  "Θ; B; ((z, b, c1) #_\<Gamma> Γ) ⊨ c2"
  using subst_v_c_def subst_v_id assms subtype_valid[OF assms] by simp

lemma obtain_for_t_with_fresh:
  assumes "atom x ♯ t"
  shows "∃b c. t = { x : b | c }"
proof -
  obtain z1 b1 c1 where *:" t = { z1 : b1 | c1 } ∧ atom z1 ♯ t" using obtain_fresh_z by metis
  then have "t = (x ↔ z1) ∙ t" using flip_fresh_fresh assms by metis
  also have "... = { (x ↔ z1) ∙ z1 : (x ↔ z1) ∙ b1 | (x ↔ z1) ∙ c1 }" using * assms by simp
  also have "... = { x : b1 | (x ↔ z1) ∙ c1 }" using * assms by auto
  finally show ?thesis by auto
qed

lemma subtype_trans: 
  assumes "Θ; B; Γ ⊨ τ1 < τ2" and "Θ; B; Γ ⊨ τ2 < τ3"
  shows "Θ; B; Γ ⊨ τ1 < τ3"
  using assms proof(nominal_induct  avoiding: τ3 rule: subtype.strong_induct)
  case (subtype_baseI x Θ B Γ z c z' c' b)
  hence "b_of τ3 = b" using  subtype_eq_base2 b_of.simps by metis
  then obtain z'' c'' where t3: "τ3 = { z'' : b | c''} ∧ atom z'' ♯ x" 
    using obtain_fresh_z2 by metis
  hence xf: "atom x ♯ (z'', c'')" using fresh_prodN subtype_baseI τ.fresh by auto
  have "Θ; B; Γ ⊨ { z : b | c } < { z'' : b | c''}" 
  proof(rule Typing.subtype_baseI)
    show ‹atom x ♯ (Θ, B, Γ, z, c, z'', c'')› using t3 fresh_prodN subtype_baseI xf by simp
    show ‹ Θ; B; Γ ⊨_wf { z : b | c } › using subtype_baseI by auto
    show ‹ Θ; B; Γ ⊨_wf { z'' : b | c'' } › using subtype_baseI t3 subtype_elims by metis
    have " Θ; B; (x, b, c'[z'::=[ x ]^v]_v) #_\<Gamma> Γ ⊨ c''[z''::=[ x ]^v]_v "
      using subtype_valid[OF ‹Θ; B; Γ ⊨ { z' : b | c' } < τ3› , of x z' b c' z'' c''] subtype_baseI 
        t3 by simp
    thus ‹Θ; B; (x, b, c[z::=[ x ]^v]_v) #_\Γ Γ ⊨ c''[z''::=[ x ]^v]_v ›
      using  valid_trans_full[of Θ B x b c z Γ c' z' c'' z'' ] subtype_baseI  t3 by simp
  qed
  thus ?case using t3 by simp
qed

lemma subtype_eq_e:
  assumes "∀i s1 s2 G. wfG P B G ∧ wfI P G i ∧ eval_e i e1 s1 ∧ eval_e i e2 s2 ⟶ s1 = s2"   and "atom z1 ♯ e1" and "atom z2 ♯ e2" and "atom z1 ♯ Γ" and "atom z2 ♯ Γ"
    and "wfCE P B Γ e1 b" and "wfCE P B Γ e2 b" 
  shows "P; B; Γ ⊨ { z1 : b | CE_val (V_var z1) == e1 } < ({ z2 : b | CE_val (V_var z2) == e2 })"
proof -

  have "wfCE P B Γ e1 b" and "wfCE P B Γ e2 b" using  assms by auto

  have wst1: "wfT P B Γ ({ z1 : b | CE_val (V_var z1) == e1 })" 
    using wfC_e_eq  wfTI assms wfX_wfB wfG_fresh_x 
    by (simp add: wfT_e_eq)

  moreover have wst2:"wfT P B Γ ({ z2 : b | CE_val (V_var z2) == e2 })" 
    using wfC_e_eq wfX_wfB wfTI assms wfG_fresh_x 
    by (simp add: wfT_e_eq)

  moreover obtain x::x where xf: "atom x ♯ (P, B , z1, CE_val (V_var z1) == e1 , z2, CE_val (V_var z2) == e2 , Γ)" using obtain_fresh by blast
  moreover have vld: "P; B ; (x, b, (CE_val (V_var z1) == e1 )[z1::=V_var x]_v) #_\<Gamma> Γ ⊨ (CE_val (V_var z2) == e2 )[z2::=V_var x]_v "  (is "P; B ; ?G ⊨ ?c")
  proof -

    have wbg: "P; B ⊨_wf ?G ∧ P ; B ⊨_wf Γ ∧ toSet Γ ⊆ toSet ?G"  proof -        
      have "P; B ⊨_wf ?G"  proof(rule wfG_consI) 
        show "P; B ⊨_wf Γ" using assms wfX_wfY by metis
        show "atom x ♯ Γ" using xf by auto
        show "P; B ⊨_wf b " using assms(6) wfX_wfB by auto
        show "P; B ; (x, b, TRUE) #_\<Gamma> Γ ⊨_wf (CE_val (V_var z1) == e1 )[z1::=V_var x]_v " 
          using wfC_e_eq[OF assms(6)] wf_subst(2)
          by (simp add: ‹atom x ♯ Γ› assms(2) subst_v_c_def)
      qed
      moreover hence  "P; B ⊨_wf Γ" using wfG_elims by metis
      ultimately show ?thesis using toSet.simps by auto 
    qed

    have wsc: "wfC P B ?G ?c" proof -
      have "wfCE P B ?G (CE_val (V_var x)) b" proof      
        show ‹ P; B ; (x, b, (CE_val (V_var z1) == e1 )[z1::=V_var x]_v) #_\Γ Γ ⊨_wf V_var x : b › using wfV_varI lookup.simps wbg by auto
      qed
      moreover have "wfCE P B ?G e2 b" using wf_weakening assms wbg by metis
      ultimately have "wfC P B ?G (CE_val (V_var x) == e2 )" using wfC_eqI by simp
      thus ?thesis using subst_cv.simps(6) ‹atom z2 ♯ e2› subst_v_c_def by simp
    qed

    moreover have "∀i. wfI P ?G i ∧ is_satis_g i ?G ⟶ is_satis i ?c" proof(rule allI , rule impI)
      fix i
      assume as: "wfI P ?G i ∧ is_satis_g i ?G" 
      hence "is_satis i ((CE_val (V_var z1) == e1 )[z1::=V_var x]_v)" 
        by (simp add: is_satis_g.simps(2))
      hence "is_satis i (CE_val (V_var x) == e1 )" using subst_cv.simps assms subst_v_c_def by auto
      then obtain s1 and s2 where *:"eval_e i (CE_val (V_var x)) s1 ∧ eval_e i e1 s2 ∧ s1=s2" using is_satis.simps eval_c_elims by metis
      moreover hence "eval_e i e2 s1" proof -
        have **:"wfI P ?G i" using as by auto
        moreover have "wfCE P B ?G e1 b ∧ wfCE P B ?G e2 b" using assms xf wf_weakening wbg by metis
        moreover then  obtain s2' where "eval_e i e2 s2'" using assms wfI_wfCE_eval_e ** by metis
        ultimately show ?thesis using * assms(1) wfX_wfY by metis
      qed
      ultimately have  "is_satis i (CE_val (V_var x) == e2 )" using is_satis.simps eval_c_eqI by force
      thus "is_satis i ((CE_val (V_var z2) == e2 )[z2::=V_var x]_v)"  using is_satis.simps eval_c_eqI assms subst_cv.simps subst_v_c_def by auto
    qed
    ultimately show ?thesis using valid.simps by simp
  qed
  moreover have "atom x ♯ (P, B, Γ, z1 , CE_val (V_var z1) == e1, z2, CE_val (V_var z2) == e2 ) " 
    unfolding fresh_prodN using  xf fresh_prod7 τ.fresh by fast
  ultimately show ?thesis using subtype_baseI[OF _ wst1 wst2  vld] xf by simp
qed

lemma subtype_eq_e_nil:
  assumes  "∀i s1 s2 G. wfG P B G ∧ wfI P G i ∧ eval_e i e1 s1 ∧ eval_e i e2 s2 ⟶ s1 = s2" and "supp e1 = {}" and "supp e2 = {}" and "wfTh P" 
    and "wfCE P B GNil e1 b" and "wfCE P B GNil e2 b"  and "atom z1 ♯ GNil" and "atom z2 ♯ GNil"
  shows "P; B ; GNil ⊨ { z1 : b | CE_val (V_var z1) == e1 } < ({ z2 : b | CE_val (V_var z2) == e2 })"
  apply(rule subtype_eq_e,auto simp add: assms e.fresh)
  using  assms fresh_def e.fresh  supp_GNil by metis+

lemma subtype_gnil_fst_aux:
  assumes "supp v₁ = {}" and "supp (V_pair v₁ v₂) = {}" and "wfTh P" and "wfCE P B GNil (CE_val v₁) b" and "wfCE P B GNil (CE_fst [V_pair v₁ v₂]^ce) b" and 
    "wfCE P B GNil (CE_val v₂) b2"  and "atom z1 ♯ GNil" and "atom z2 ♯ GNil"
  shows "P; B ; GNil ⊨ ({ z1 : b | CE_val (V_var z1) == CE_val v₁ }) < ({ z2 : b | CE_val (V_var z2) == CE_fst [V_pair v₁ v₂]^ce })"
proof - 
  have "∀i s1 s2 G . wfG P B G ∧ wfI P G i ∧ eval_e i ( CE_val v₁) s1 ∧ eval_e i (CE_fst [V_pair v₁ v₂]^ce) s2 ⟶ s1 = s2" proof(rule+) 
    fix i s1 s2 G
    assume as: "wfG P B G ∧ wfI P G i ∧ eval_e i (CE_val v₁) s1 ∧ eval_e i (CE_fst [V_pair v₁ v₂]^ce) s2"
    hence "wfCE P B G (CE_val v₂) b2" using assms wf_weakening 
      by (metis empty_subsetI toSet.simps(1))
    then obtain s3 where "eval_e i (CE_val v₂) s3" using wfI_wfCE_eval_e as by metis
    hence "eval_v i ((V_pair v₁ v₂)) (SPair s1 s3)"
      by (meson as eval_e_elims(1) eval_v_pairI)
    hence "eval_e i (CE_fst [V_pair v₁ v₂]^ce) s1" using eval_e_fstI eval_e_valI by metis
    show "s1 = s2" using as eval_e_uniqueness
      using ‹eval_e i (CE_fst [V_pair v₁ v₂]^ce) s1› by auto
  qed
  thus ?thesis using subtype_eq_e_nil  ce.supp assms by auto
qed

lemma subtype_gnil_snd_aux:
  assumes "supp v₂ = {}" and "supp (V_pair v₁ v₂) = {}" and "wfTh P" and "wfCE P B GNil (CE_val v₂) b" and 
    "wfCE P B GNil (CE_snd [(V_pair v₁ v₂)]^ce) b" and 
    "wfCE P B GNil (CE_val v₁) b2"  and "atom z1 ♯ GNil" and "atom z2 ♯ GNil"
  shows "P; B ; GNil ⊨ ({ z1 : b | CE_val (V_var z1) == CE_val v₂ }) < ({ z2 : b | CE_val (V_var z2) == CE_snd [(V_pair v₁ v₂)]^ce })"
proof - 
  have "∀i s1 s2 G. wfG P B G ∧ wfI P G i ∧ eval_e i ( CE_val v₂) s1 ∧ eval_e i (CE_snd [(V_pair v₁ v₂)]^ce) s2 ⟶ s1 = s2" proof(rule+) 
    fix i s1 s2 G
    assume as: " wfG P B G ∧ wfI P G i ∧ eval_e i (CE_val v₂) s1 ∧ eval_e i (CE_snd [(V_pair v₁ v₂)]^ce) s2"
    hence "wfCE P B G (CE_val v₁) b2" using assms wf_weakening 
      by (metis empty_subsetI toSet.simps(1))
    then obtain s3 where "eval_e i (CE_val v₁) s3" using wfI_wfCE_eval_e as by metis
    hence "eval_v i ((V_pair v₁ v₂)) (SPair s3 s1)"
      by (meson as eval_e_elims eval_v_pairI)
    hence "eval_e i (CE_snd [(V_pair v₁ v₂)]^ce) s1" using eval_e_sndI eval_e_valI by metis
    show "s1 = s2" using as eval_e_uniqueness
      using ‹eval_e i (CE_snd [V_pair v₁ v₂]^ce) s1› by auto
  qed
  thus ?thesis using assms subtype_eq_e_nil  by (simp add: ce.supp ce.supp)
qed

lemma subtype_gnil_fst:
  assumes "Θ ; {||} ; GNil ⊨_wf [#1[[v₁,v₂]^v]^ce]^ce : b" 
  shows "Θ ; {||} ; GNil ⊨ ({ z₁ : b | [[z₁]^v]^ce == [v₁]^ce }) <
        ({ z₂ : b | [[z₂]^v]^ce == [#1[[v₁, v₂]^v]^ce]^ce })"
proof  -
  obtain b2 where **:" Θ ; {||} ; GNil ⊨_wf V_pair v₁ v₂ : B_pair b b2" using wfCE_elims(4)[OF assms ] wfCE_elims by metis
  obtain b1' b2' where *:"B_pair b b2 = B_pair b1' b2' ∧ Θ ; {||} ; GNil ⊨_wf v₁ : b1' ∧ Θ ; {||} ; GNil ⊨_wf v₂ : b2'" 
    using wfV_elims(3)[OF **] by metis

  show ?thesis proof(rule subtype_gnil_fst_aux)
    show ‹supp v₁ = {}› using * wfV_supp_nil by auto
    show ‹supp (V_pair v₁ v₂) = {}› using ** wfV_supp_nil e.supp by metis
    show ‹⊨_wf Θ› using assms wfX_wfY   by metis
    show ‹Θ; {||}; GNil ⊨_wf CE_val v₁ : b › using  wfCE_valI  "*" by auto
    show ‹Θ; {||}; GNil ⊨_wf CE_fst [V_pair v₁ v₂]^ce : b › using assms by auto
    show ‹Θ; {||}; GNil ⊨_wf CE_val v₂ : b2 ›using  wfCE_valI  "*" by auto
    show ‹atom z₁ ♯ GNil› using fresh_GNil by metis
    show ‹atom z₂ ♯ GNil› using fresh_GNil by metis
  qed
qed

lemma subtype_gnil_snd:
  assumes "wfCE P {||} GNil (CE_snd ([V_pair v₁ v₂]^ce)) b" 
  shows "P ; {||} ; GNil ⊨ ({ z1 : b | CE_val (V_var z1) == CE_val v₂ }) < ({ z2 : b | CE_val (V_var z2) == CE_snd [(V_pair v₁ v₂)]^ce })"
proof  -
  obtain b1 where **:" P ; {||} ; GNil ⊨_wf V_pair v₁ v₂ : B_pair b1 b " using wfCE_elims assms by metis
  obtain b1' b2' where *:"B_pair b1 b = B_pair b1' b2' ∧ P ; {||} ; GNil ⊨_wf v₁ : b1' ∧ P ; {||} ; GNil ⊨_wf v₂ : b2'" using wfV_elims(3)[OF **] by metis

  show ?thesis proof(rule subtype_gnil_snd_aux)
    show ‹supp v₂ = {}› using * wfV_supp_nil by auto
    show ‹supp (V_pair v₁ v₂) = {}› using ** wfV_supp_nil e.supp by metis
    show ‹⊨_wf P› using assms wfX_wfY  by metis
    show ‹P; {||}; GNil ⊨_wf CE_val v₁ : b1 › using wfCE_valI   "*" by simp
    show ‹P; {||}; GNil ⊨_wf CE_snd [(V_pair v₁ v₂)]^ce : b › using assms by auto
    show ‹P; {||}; GNil ⊨_wf CE_val v₂ : b ›using  wfCE_valI  "*" by simp
    show ‹atom z1 ♯ GNil› using fresh_GNil by metis
    show ‹atom z2 ♯ GNil› using fresh_GNil by metis
  qed
qed

lemma subtype_fresh_tau:
  fixes x::x
  assumes "atom x ♯ t1" and "atom x ♯ Γ" and "P; B; Γ ⊨ t1 < t2"
  shows "atom x ♯ t2"
proof -
  have wfg: "P; B ⊨_wf Γ" using subtype_wf wfX_wfY  assms by metis
  have wft: "wfT P B Γ t2" using subtype_wf wfX_wfY assms by blast
  hence "supp t2 ⊆ atom_dom Γ ∪ supp B" using wf_supp 
    using atom_dom.simps by auto
  moreover have "atom x ∉ atom_dom Γ" using ‹atom x ♯ Γ› wfG_atoms_supp_eq wfg fresh_def by blast 
  ultimately show "atom x ♯ t2" using fresh_def
    by (metis Un_iff contra_subsetD x_not_in_b_set)
qed

lemma subtype_if_simp:
  assumes "wfT P B GNil ({ z1 : b | CE_val (V_lit l ) == CE_val (V_lit l) IMP c[z::=V_var z1]_v })" and
    "wfT P B GNil ({ z : b | c })" and "atom z1 ♯ c"
  shows  "P; B ; GNil ⊨ ({ z1 : b | CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v }) < ({ z : b | c })" 
proof -
  obtain x::x where xx: "atom x ♯ ( P , B , z1, CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z, c, GNil)" using obtain_fresh_z by blast
  hence xx2: " atom x ♯ (CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v , c, GNil)" using fresh_prod7 fresh_prod3 by fast
  have *:"P; B ; (x, b, (CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v )[z1::=V_var x]_v) #_\<Gamma> GNil ⊨ c[z::=V_var x]_v " (is "P; B ; ?G ⊨ ?c" ) proof -
    have "wfC P B ?G ?c"  using wfT_wfC_cons[OF assms(1) assms(2),of x] xx fresh_prod5 fresh_prod3 subst_v_c_def by metis
    moreover have "(∀i. wfI P ?G i ∧ is_satis_g i ?G ⟶ is_satis i ?c)" proof(rule allI, rule impI)
      fix i
      assume as1: "wfI P ?G i ∧ is_satis_g i ?G" 
      have "((CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v )[z1::=V_var x]_v) = ((CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var x]_v ))" 
        using assms subst_v_c_def by auto
      hence "is_satis i ((CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var x]_v ))" using is_satis_g.simps as1 by presburger
      moreover have "is_satis i ((CE_val (V_lit l) == CE_val (V_lit l)))" using is_satis.simps eval_c_eqI[of i "(CE_val (V_lit l))" "eval_l l"] eval_e_uniqueness 
          eval_e_valI eval_v_litI by metis
      ultimately show  "is_satis i ?c" using  is_satis_mp[of i] by metis
    qed
    ultimately show ?thesis using valid.simps by simp
  qed
  moreover have "atom x ♯ (P, B, GNil, z1 , CE_val (V_lit l) == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z, c )" 
    unfolding fresh_prod5 τ.fresh using xx fresh_prodN x_fresh_b by metis
  ultimately show ?thesis using subtype_baseI assms xx xx2  by metis
qed

lemma subtype_if:
  assumes "P; B; Γ ⊨ { z : b | c } < { z' : b | c' }" and 
    "wfT P B Γ ({ z1 : b | CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v })"  and
    "wfT P B Γ ({ z2 : b | CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v })" and 
    "atom z1 ♯ v" and  "atom z ♯ Γ" and "atom z1 ♯ c" and "atom z2 ♯ c'" and "atom z2 ♯ v"
  shows   "P; B ; Γ ⊨ { z1 : b | CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v } < { z2 : b | CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v }"
proof -
  obtain x::x where xx: "atom x ♯ (P,B,z,c,z', c', z1, CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z2, CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v , Γ)" 
    using obtain_fresh_z by blast
  hence xf: "atom x ♯ (z, c, z', c', Γ)" by simp
  have xf2: "atom x ♯ (z1, CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z2, CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v , Γ)" 
    using xx fresh_prod4 fresh_prodN by metis

  moreover have "P; B ; (x, b, (CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v )[z1::=V_var x]_v) #_\<Gamma> Γ ⊨ (CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v )[z2::=V_var x]_v" 
    (is "P; B ; ?G ⊨ ?c" )
  proof -
    have wbc: "wfC P B ?G ?c" using  assms xx fresh_prod4 fresh_prod2 wfT_wfC_cons assms subst_v_c_def by metis

    moreover have "∀i. wfI P ?G i ∧ is_satis_g i ?G ⟶ is_satis i ?c" proof(rule allI, rule impI)
      fix i
      assume a1: "wfI P ?G i ∧ is_satis_g i ?G"

      have *: " is_satis i ((CE_val v == CE_val (V_lit l))) ⟶ is_satis i ((c'[z'::=V_var z2]_v )[z2::=V_var x]_v)" 
      proof 
        assume a2: "is_satis i ((CE_val v == CE_val (V_lit l)))" 

        have "is_satis i ((CE_val v == CE_val (V_lit l) IMP (c[z::=V_var z1]_v ))[z1::=V_var x]_v)" 
          using a1 is_satis_g.simps  by simp
        moreover have "((CE_val v == CE_val (V_lit l) IMP (c[z::=V_var z1]_v ))[z1::=V_var x]_v) = (CE_val v == CE_val (V_lit l) IMP ((c[z::=V_var z1]_v )[z1::=V_var x]_v))" 
          using  assms subst_v_c_def by simp
        ultimately have "is_satis i (CE_val v == CE_val (V_lit l) IMP ((c[z::=V_var z1]_v )[z1::=V_var x]_v))" by argo

        hence  "is_satis i ((c[z::=V_var z1]_v )[z1::=V_var x]_v)" using a2 is_satis_mp by auto
        moreover have "((c[z::=V_var z1]_v )[z1::=V_var x]_v) = ((c[z::=V_var x]_v ))" using assms by auto
        ultimately have  "is_satis i ((c[z::=V_var x]_v ))"  using a2 is_satis.simps by auto

        hence "is_satis_g i ((x,b,(c[z::=V_var x]_v )) #_\<Gamma> Γ)" using a1 is_satis_g.simps by meson
        moreover have "wfI P ((x,b,(c[z::=V_var x]_v )) #_\<Gamma> Γ) i" proof -
          obtain s where "Some s = i x ∧ wfRCV P s b ∧ wfI P Γ i" using wfI_def a1 by auto
          thus ?thesis using wfI_def by auto
        qed
        ultimately have  "is_satis i ((c'[z'::=V_var x]_v))" using subtype_valid assms(1) xf valid.simps by simp

        moreover have "(c'[z'::=V_var x]_v) = ((c'[z'::=V_var z2]_v )[z2::=V_var x]_v)" using assms by auto
        ultimately show "is_satis i ((c'[z'::=V_var z2]_v )[z2::=V_var x]_v)" by auto
      qed

      moreover have "?c = ((CE_val v == CE_val (V_lit l)) IMP ((c'[z'::=V_var z2]_v )[z2::=V_var x]_v))" 
        using  assms subst_v_c_def by simp

      moreover have "∃b1 b2. eval_c i (CE_val v == CE_val (V_lit l) ) b1 ∧
                     eval_c i c'[z'::=V_var z2]_v[z2::=V_var x]_v b2" proof -

        have "wfC P B ?G (CE_val v == CE_val (V_lit l))"  using wbc wfC_elims(7) assms subst_cv.simps subst_v_c_def by fastforce

        moreover have "wfC P B ?G (c'[z'::=V_var z2]_v[z2::=V_var x]_v)" proof(rule wfT_wfC_cons)
          show ‹ P; B; Γ ⊨_wf { z1 : b | CE_val v == CE_val (V_lit l) IMP (c[z::=V_var z1]_v) } › using assms subst_v_c_def by auto
          have " { z2 : b | c'[z'::=V_var z2]_v } = { z' : b | c' }" using assms subst_v_c_def by auto
          thus  ‹ P; B; Γ ⊨_wf { z2 : b | c'[z'::=V_var z2]_v } › using assms subtype_elims by metis
          show ‹atom x ♯ (CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v , c'[z'::=V_var z2]_v, Γ)› using xx fresh_Pair c.fresh by metis
        qed

        ultimately show ?thesis using wfI_wfC_eval_c a1 subst_v_c_def by simp
      qed

      ultimately show "is_satis i ?c" using is_satis_imp[OF *] by auto
    qed
    ultimately show  ?thesis using valid.simps by simp
  qed
  moreover have "atom x ♯ (P, B, Γ, z1 , CE_val v == CE_val (V_lit l) IMP c[z::=V_var z1]_v , z2 , CE_val v == CE_val (V_lit l) IMP c'[z'::=V_var z2]_v )" 
    unfolding fresh_prod5 τ.fresh using xx xf2 fresh_prodN x_fresh_b by metis
  ultimately show ?thesis using subtype_baseI assms  xf2 by metis 
qed

lemma eval_e_concat_eq:
  assumes  "wfI Θ Γ i" 
  shows "∃s. eval_e i (CE_val (V_lit (L_bitvec (v1 @ v2))) ) s ∧ eval_e i (CE_concat [(V_lit (L_bitvec v1))]^ce [(V_lit (L_bitvec v2))]^ce) s"
  using eval_e_valI eval_e_concatI eval_v_litI eval_l.simps by metis

lemma is_satis_eval_e_eq_imp:
  assumes "wfI Θ Γ i" and "eval_e i e1 s" and "eval_e i e2 s"
    and  "is_satis i (CE_val (V_var x) == e1)"  (is "is_satis i ?c1")
  shows "is_satis i (CE_val (V_var x) == e2)"
proof -
  have *:"eval_c i ?c1 True" using assms is_satis.simps by blast
  hence "eval_e i (CE_val (V_var x)) s" using assms is_satis.simps eval_c_elims
    by (metis (full_types) eval_e_uniqueness)
  thus ?thesis using is_satis.simps eval_c.intros assms by fastforce
qed

lemma valid_eval_e_eq:
  fixes e1::ce and e2::ce
  assumes "∀Γ i. wfI Θ Γ i ⟶ (∃s. eval_e i e1 s ∧ eval_e i e2 s)" and "Θ; B; GNil ⊨_wf e1 : b " and  "Θ; B; GNil ⊨_wf e2 : b"
  shows    "Θ; B; (x, b, (CE_val (V_var x) == e1 )) #_\<Gamma> GNil ⊨ (CE_val (V_var x) == e2) "
proof(rule validI)
  show "Θ; B; (x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil ⊨_wf CE_val (V_var x) == e2" 
  proof
    have " Θ ; B ; (x, b, TRUE )#_\<Gamma>GNil ⊨_wf CE_val (V_var x) == e1" using assms wfC_eqI wfE_valI wfV_varI wfX_wfY 
      by (simp add: fresh_GNil wfC_e_eq)    
    hence "Θ ; B ⊨_wf (x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil" using wfG_consI fresh_GNil wfX_wfY assms wfX_wfB by metis
    thus "Θ; B; (x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil ⊨_wf CE_val (V_var x) : b " using  wfCE_valI wfV_varI wfX_wfY 
        lookup.simps  assms wfX_wfY by simp
    show "Θ; B; (x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil ⊨_wf e2 : b " using assms wf_weakening wfX_wfY 
      by (metis (full_types) ‹Θ; B; (x, b, CE_val (V_var x) == e1 ) #_\Γ GNil ⊨_wf CE_val (V_var x) : b› empty_iff subsetI toSet.simps(1))
  qed
  show " ∀i. wfI Θ ((x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil) i ∧ is_satis_g i ((x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil) ⟶ is_satis i (CE_val (V_var x) == e2 )"
  proof(rule,rule)
    fix i
    assume "wfI Θ ((x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil) i ∧ is_satis_g i ((x, b, CE_val (V_var x) == e1 ) #_\<Gamma> GNil)"
    moreover then obtain s where "eval_e i e1 s ∧ eval_e i e2 s" using assms by auto
    ultimately show "is_satis i (CE_val (V_var x) == e2 )" using assms  is_satis_eval_e_eq_imp is_satis_g.simps by meson
  qed
qed

lemma subtype_concat:
  assumes " ⊨_wf Θ"
  shows "Θ; B; GNil ⊨ { z : B_bitvec | CE_val (V_var z) == CE_val (V_lit (L_bitvec (v1 @ v2))) } <
            { z : B_bitvec | CE_val (V_var z) == CE_concat [(V_lit (L_bitvec v1))]^ce [(V_lit (L_bitvec v2))]^ce }" (is "Θ; B; GNil ⊨ ?t1 < ?t2")
proof -
  obtain x::x where x: "atom x ♯ (Θ, B, GNil, z , CE_val (V_var z) == CE_val (V_lit (L_bitvec (v1 @ v2))),
            z , CE_val (V_var z) == CE_concat [V_lit (L_bitvec v1)]^ce [V_lit (L_bitvec v2)]^ce )" 
    (is "?xfree" )
    using obtain_fresh by auto

  have wb1: "Θ; B; GNil ⊨_wf CE_val (V_lit (L_bitvec (v1 @ v2))) : B_bitvec" using wfX_wfY wfCE_valI wfV_litI assms base_for_lit.simps wfG_nilI by metis
  hence wb2: "Θ; B; GNil ⊨_wf CE_concat [(V_lit (L_bitvec v1))]^ce [(V_lit (L_bitvec v2))]^ce : B_bitvec" 
    using wfCE_concatI wfX_wfY wfV_litI base_for_lit.simps wfCE_valI by metis

  show ?thesis proof
    show " Θ; B; GNil ⊨_wf ?t1" using wfT_e_eq fresh_GNil wb1 wb2 by metis
    show " Θ; B; GNil ⊨_wf ?t2" using wfT_e_eq fresh_GNil wb1 wb2 by metis
    show ?xfree using x by auto
    show "Θ; B; (x, B_bitvec, (CE_val (V_var z) == CE_val (V_lit (L_bitvec (v1 @ v2))) )[z::=V_var x]_v) #_\<Gamma>
           GNil ⊨ (CE_val (V_var z) == CE_concat [(V_lit (L_bitvec v1))]^ce [(V_lit (L_bitvec v2))]^ce )[z::=V_var x]_v " 
      using valid_eval_e_eq eval_e_concat_eq wb1 wb2 subst_v_c_def by fastforce
  qed
qed

lemma subtype_len:
  assumes " ⊨_wf Θ"
  shows "Θ; B; GNil ⊨ { z' : B_int | CE_val (V_var z') == CE_val (V_lit (L_num (int (length v)))) } <
                           { z : B_int | CE_val (V_var z) == CE_len [(V_lit (L_bitvec v))]^ce }" (is "Θ; B; GNil ⊨ ?t1 < ?t2")
proof -

  have *: "Θ ⊨_wf [] ∧ Θ; B; GNil ⊨_wf []_\<Delta> " using assms wfG_nilI wfD_emptyI wfPhi_emptyI by auto
  obtain x::x where x: "atom x ♯ (Θ, B, GNil, z' , CE_val (V_var z') ==
          CE_val (V_lit (L_num (int (length v)))) , z, CE_val (V_var z) == CE_len [(V_lit (L_bitvec v))]^ce )"
    (is "atom x ♯ ?F")
    using obtain_fresh by metis
  then show ?thesis proof
    have "Θ ; B ; GNil ⊨_wf CE_val (V_lit (L_num (int (length v)))) : B_int" 
      using wfCE_valI * wfV_litI base_for_lit.simps 
      by (metis wfE_valI wfX_wfY)

    thus  "Θ; B; GNil ⊨_wf ?t1" using wfT_e_eq fresh_GNil by auto

    have "Θ ; B ; GNil ⊨_wf CE_len [(V_lit (L_bitvec v))]^ce : B_int"       
      using wfE_valI * wfV_litI base_for_lit.simps  wfE_valI wfX_wfY 
      by (metis wfCE_lenI wfCE_valI)

    thus "Θ; B; GNil ⊨_wf ?t2" using wfT_e_eq fresh_GNil  by auto

    show  "Θ; B; (x, B_int, (CE_val (V_var z') == CE_val (V_lit (L_num (int (length v)))) )[z'::=V_var x]_v) #_\<Gamma> GNil ⊨ (CE_val (V_var z) == CE_len [(V_lit (L_bitvec v))]^ce )[z::=V_var x]_v"
      (is "Θ; B; ?G ⊨ ?c" ) using valid_len assms subst_v_c_def by auto      
  qed
qed

lemma subtype_base_fresh:
  assumes "Θ; B; Γ ⊨_wf { z : b | c }" and "Θ; B; Γ ⊨_wf { z : b | c' } " and
    "atom z ♯ Γ" and "Θ; B; (z, b, c) #_\<Gamma> Γ ⊨ c'"
  shows "Θ; B; Γ ⊨ { z : b | c } < { z : b | c' }"
proof  -
  obtain x::x where *:"atom x ♯ ((Θ , B , z, c, z, c', Γ) , (Θ, B, Γ, { z : b | c }, { z : b | c' }))" using obtain_fresh by metis
  moreover hence "atom x ♯ Γ" using fresh_Pair by auto
  moreover hence "Θ; B; (x, b, c[z::=V_var x]_v) #_\<Gamma> Γ ⊨ c'[z::=V_var x]_v" using assms valid_flip_simple  * subst_v_c_def  by auto
  ultimately show ?thesis using subtype_baseI assms τ.fresh fresh_Pair by metis
qed

lemma subtype_bop_arith:
  assumes "wfG Θ B Γ" and "(opp = Plus ∧ ll = (L_num (n1+n2))) ∨ (opp = LEq ∧ ll = ( if n1≤n2 then L_true else L_false))"  
    and "(opp = Plus ⟶ b = B_int) ∧ (opp = LEq ⟶ b = B_bool)"
  shows "Θ; B; Γ ⊨ ({ z : b | C_eq (CE_val (V_var z)) (CE_val (V_lit (ll))) }) <
                           { z : b | C_eq (CE_val (V_var z)) (CE_op opp [(V_lit (L_num n1))]^ce [(V_lit (L_num n2))]^ce) }" (is "Θ; B; Γ ⊨ ?T1 < ?T2")   
proof -  
  obtain x::x where  xf: "atom x ♯ (z, CE_val (V_var z) == CE_val (V_lit (ll)) , z, CE_val (V_var z) == CE_op opp [(V_lit (L_num n1))]^ce [(V_lit (L_num n2))]^ce , Γ)" 
    using obtain_fresh by blast

  have "Θ; B; Γ ⊨ ({ x : b | C_eq (CE_val (V_var x)) (CE_val (V_lit (ll))) }) <
                           { x : b | C_eq (CE_val (V_var x)) (CE_op opp [(V_lit (L_num n1))]^ce [(V_lit (L_num n2))]^ce) }" (is "Θ; B; Γ ⊨ ?S1 < ?S2") 
  proof(rule  subtype_base_fresh)

    show "atom x ♯ Γ" using xf fresh_Pair by auto

    show  "wfT Θ B Γ ({ x : b | CE_val (V_var x) == CE_val (V_lit ll) })" (is "wfT Θ B ?A ?B") 
    proof(rule wfT_e_eq)
      have   " Θ; B; Γ ⊨_wf (V_lit ll) : b" using wfV_litI base_for_lit.simps assms by metis
      thus " Θ; B; Γ ⊨_wf CE_val (V_lit ll) : b" using wfCE_valI by auto
      show "atom x ♯ Γ" using xf fresh_Pair by auto
    qed

    consider "opp = Plus" | "opp = LEq" using opp.exhaust assms by blast
    then show  "wfT Θ B Γ ({ x : b | CE_val (V_var x) == CE_op opp [(V_lit (L_num n1))]^ce [(V_lit (L_num n2))]^ce })" (is "wfT Θ B ?A ?C")
    proof(cases)
      case 1
      then show "Θ ; B ; Γ ⊨_wf { x : b | [ [ x ]^v ]^ce == [ opp [ [ L_num n1 ]^v ]^ce [ [ L_num n2 ]^v ]^ce ]^ce }"   
        using wfCE_valI  wfCE_plusI  assms wfV_litI base_for_lit.simps assms 
        by (metis ‹atom x ♯ Γ› wfT_e_eq)
    next
      case 2
      then show "Θ ; B ; Γ ⊨_wf { x : b | [ [ x ]^v ]^ce == [ opp [ [ L_num n1 ]^v ]^ce [ [ L_num n2 ]^v ]^ce ]^ce } "  
        using wfCE_valI  wfCE_plusI  assms wfV_litI base_for_lit.simps assms 

        by (metis ‹atom x ♯ Γ› wfCE_leqI wfT_e_eq)
    qed    

    show   "Θ; B ; (x, b, (CE_val (V_var x) == CE_val (V_lit (ll)) )) #_\<Gamma> Γ
                          ⊨ (CE_val (V_var x) == CE_op opp [V_lit (L_num n1)]^ce [V_lit (L_num n2)]^ce)" (is "Θ; B; ?G ⊨ ?c")
      using valid_arith_bop assms xf by simp

  qed
  moreover have "?S1 = ?T1 " using type_l_eq by auto
  moreover have "?S2 = ?T2" using type_e_eq ce.fresh v.fresh supp_l_empty fresh_def empty_iff fresh_e_opp 
    by (metis ms_fresh_all(4))
  ultimately show ?thesis by auto 

qed

lemma subtype_bop_eq:
  assumes "wfG Θ B Γ" and "base_for_lit l1 = base_for_lit l2"
  shows "Θ; B; Γ ⊨ ({ z : B_bool | C_eq (CE_val (V_var z)) (CE_val (V_lit (if l1 = l2 then L_true else L_false))) }) <
                      { z : B_bool | C_eq (CE_val (V_var z)) (CE_op Eq [(V_lit l1)]^ce [(V_lit l2)]^ce) }" (is "Θ; B; Γ ⊨ ?T1 < ?T2")   
proof -
  let ?ll = "if l1 = l2 then L_true else L_false"
  obtain x::x where  xf: "atom x ♯ (z, CE_val (V_var z) == CE_val (V_lit (if l1 = l2 then L_true else L_false)) , z, CE_val (V_var z) == CE_op Eq [(V_lit l1)]^ce [(V_lit l2)]^ce , Γ, (Θ, B, Γ))" 
    using obtain_fresh by blast

  have "Θ; B; Γ ⊨ ({ x : B_bool | C_eq (CE_val (V_var x)) (CE_val (V_lit (?ll))) }) <
                           { x : B_bool | C_eq (CE_val (V_var x)) (CE_op Eq [(V_lit (l1))]^ce [(V_lit (l2))]^ce) }" (is "Θ; B; Γ ⊨ ?S1 < ?S2") 
  proof(rule  subtype_base_fresh)

    show "atom x ♯ Γ" using xf fresh_Pair by auto

    show  "wfT Θ B Γ ({ x : B_bool | CE_val (V_var x) == CE_val (V_lit ?ll) })" (is "wfT Θ B ?A ?B") 
    proof(rule wfT_e_eq)
      have   " Θ; B; Γ ⊨_wf (V_lit ?ll) : B_bool" using wfV_litI base_for_lit.simps assms by metis
      thus " Θ; B; Γ ⊨_wf CE_val (V_lit ?ll) : B_bool" using wfCE_valI by auto
      show "atom x ♯ Γ" using xf fresh_Pair by auto
    qed

    show " Θ ; B ; Γ ⊨_wf { x : B_bool | [ [ x ]^v ]^ce == [ eq [ [ l1 ]^v ]^ce [ [ l2 ]^v ]^ce ]^ce } "   
    proof(rule wfT_e_eq)
      show "Θ ; B ; Γ ⊨_wf [ eq [ [ l1 ]^v ]^ce [ [ l2 ]^v ]^ce ]^ce : B_bool" 
        apply(rule wfCE_eqI, rule wfCE_valI)
        apply(rule wfV_litI, simp add: assms)
        using wfV_litI assms wfCE_valI by auto   
      show "atom x ♯ Γ"  using xf fresh_Pair by auto
    qed

    show   "Θ; B ; (x, B_bool, (CE_val (V_var x) == CE_val (V_lit (?ll)) )) #_\<Gamma> Γ
                          ⊨ (CE_val (V_var x) == CE_op Eq [V_lit (l1)]^ce [V_lit (l2)]^ce)" (is "Θ; B; ?G ⊨ ?c")
      using valid_eq_bop assms xf by auto

  qed
  moreover have "?S1 = ?T1 " using type_l_eq by auto
  moreover have "?S2 = ?T2" using type_e_eq ce.fresh v.fresh supp_l_empty fresh_def empty_iff fresh_e_opp 
    by (metis ms_fresh_all(4))
  ultimately show ?thesis by auto 

qed

lemma subtype_top:
  assumes "wfT Θ B G ({ z : b | c })"
  shows  "Θ; B; G ⊨ ({ z : b | c }) < ({ z : b | TRUE })"
proof - 
  obtain x::x where *: "atom x ♯ (Θ, B, G, z , c, z , TRUE)" using obtain_fresh by blast
  then show ?thesis proof(rule subtype_baseI)
    show ‹ Θ; B; G ⊨_wf { z : b | c } › using assms by auto
    show ‹ Θ; B;G ⊨_wf { z : b | TRUE } › using wfT_TRUE assms wfX_wfY b_of.simps wfT_wf
      by (metis wfX_wfB(8))
    hence "Θ ; B ⊨_wf (x, b, c[z::=V_var x]_v) #_\<Gamma> G" using wfT_wf_cons3 assms fresh_Pair * subst_v_c_def by auto
    thus  ‹Θ; B; (x, b, c[z::=V_var x]_v) #_\Γ G ⊨ (TRUE)[z::=V_var x]_v › using valid_trueI subst_cv.simps subst_v_c_def by metis
  qed
qed

lemma if_simp:
  "(if x = x then e1 else e2) = e1"
  by auto

lemma subtype_split:
  assumes "split n v (v1,v2)" and "⊨_wf Θ"
  shows "Θ ; {||} ; GNil ⊨ { z : [ B_bitvec , B_bitvec ]^b | [ [ z ]^v ]^ce == [ [ [ L_bitvec
           v1 ]^v , [ L_bitvec
                       v2 ]^v ]^v ]^ce } < { z : [ B_bitvec , B_bitvec ]^b | [ [ L_bitvec
          v ]^v ]^ce == [ [#1[ [ z ]^v ]^ce]^ce @@ [#2[ [ z ]^v ]^ce]^ce ]^ce AND [| [#1[ [ z ]^v ]^ce]^ce |]^ce == [ [ L_num
                                                             n ]^v ]^ce }" 
    (is "Θ ;?B ; GNil ⊨ { z : [ B_bitvec , B_bitvec ]^b | ?c1 } < { z : [ B_bitvec , B_bitvec ]^b | ?c2 }")
proof -
  obtain x::x where xf:"atom x ♯ (Θ, ?B, GNil, z, ?c1,z, ?c2 )"  using obtain_fresh by auto
  then show ?thesis proof(rule subtype_baseI)
    show *: ‹Θ ; ?B ; (x, [ B_bitvec , B_bitvec ]^b, (?c1)[z::=[ x ]^v]_v) #_\Γ
 GNil ⊨ (?c2)[z::=[ x ]^v]_v ›
      unfolding subst_v_c_def subst_cv.simps subst_cev.simps subst_vv.simps if_simp      
      using valid_split[OF assms, of x] by simp
    show ‹ Θ ; ?B ; GNil ⊨_wf { z : [ B_bitvec , B_bitvec ]^b| ?c1 } › using valid_wfT[OF *] xf fresh_prodN by metis
    show ‹ Θ ; ?B ; GNil ⊨_wf { z : [ B_bitvec , B_bitvec ]^b| ?c2 } ›  using valid_wfT[OF *] xf fresh_prodN by metis
  qed
qed

lemma subtype_range:
  fixes n::int and Γ::Γ
  assumes "0 ≤ n ∧ n ≤ int (length v)" and "Θ ; {||} ⊨_wf Γ" 
  shows "Θ ; {||} ; Γ ⊨ { z : B_int | [ [ z ]^v ]^ce == [ [ L_num n ]^v ]^ce } <
                           { z : B_int | ([ leq [ [ L_num 0 ]^v ]^ce [ [ z ]^v ]^ce ]^ce == [ [ L_true ]^v ]^ce ) AND (
                                   [ leq [ [ z ]^v ]^ce [| [ [ L_bitvec v ]^v ]^ce |]^ce ]^ce == [ [ L_true ]^v ]^ce) }"
    (is  "Θ ; ?B ; Γ ⊨ { z : B_int | ?c1 } < { z : B_int | ?c2 AND ?c3 }")
proof -
  obtain x::x where *:‹atom x ♯ (Θ, ?B, Γ, z, ?c1 , z, ?c2 AND ?c3)› using obtain_fresh by auto
  moreover have **:‹Θ ; ?B ; (x, B_int, (?c1)[z::=[ x ]^v]_v) #_\Γ Γ ⊨ (?c2 AND ?c3)[z::=[ x ]^v]_v›
    unfolding subst_v_c_def subst_cv.simps subst_cev.simps subst_vv.simps if_simp using valid_range_length[OF assms(1)] assms fresh_prodN * by simp

  moreover hence ‹ Θ ; ?B ; Γ ⊨_wf { z : B_int | [ [ z ]^v ]^ce == [ [ L_num n ]^v ]^ce } › using 
      valid_wfT * fresh_prodN by metis
  moreover have ‹ Θ ; ?B ; Γ ⊨_wf { z : B_int | ?c2 AND ?c3 } ›
    using valid_wfT[OF **]  * fresh_prodN by metis
  ultimately show ?thesis using subtype_baseI by auto
qed

lemma check_num_range:
  assumes "0 ≤ n ∧ n ≤ int (length v)" and "⊨_wf Θ"
  shows "Θ ; {||} ; GNil ⊨ ([ L_num n ]^v) ← { z : B_int | ([ leq [ [ L_num 0 ]^v ]^ce [ [ z ]^v ]^ce ]^ce == [ [ L_true ]^v ]^ce) AND
      [ leq [ [ z ]^v ]^ce [| [ [ L_bitvec v ]^v ]^ce |]^ce ]^ce == [ [ L_true ]^v ]^ce }"
  using assms subtype_range check_v.intros infer_v_litI wfG_nilI 
  by (meson infer_natI)

section ‹Literals›

nominal_function type_for_lit :: "l → τ" where
  "type_for_lit (L_true) = ({ z : B_bool | [[z]^v]^ce == [V_lit L_true]^ce })"
| "type_for_lit (L_false) = ({ z : B_bool | [[z]^v]^ce == [V_lit L_false]^ce })"
| "type_for_lit (L_num n) = ({ z : B_int | [[z]^v]^ce == [V_lit (L_num n)]^ce })"
| "type_for_lit (L_unit) = ({ z : B_unit | [[z]^v]^ce == [V_lit (L_unit )]^ce })" (* could have done { z : unit | True } but want the uniformity *)
| "type_for_lit (L_bitvec v) = ({ z : B_bitvec | [[z]^v]^ce == [V_lit (L_bitvec v)]^ce })"
  by (auto simp: eqvt_def type_for_lit_graph_aux_def, metis l.strong_exhaust,(simp add: permute_int_def flip_bitvec0)+ )
nominal_termination (eqvt) by lexicographic_order


nominal_function type_for_var :: "Γ → τ → x → τ" where
  "type_for_var G τ x = (case lookup G x of
                       None → τ
                  | Some (b,c) → ({ x : b | c })) "  
  apply auto  unfolding eqvt_def apply(rule allI)  unfolding type_for_var_graph_aux_def eqvt_def by simp
nominal_termination (eqvt) by lexicographic_order

lemma infer_l_form:
  fixes l::l and tm::"'a::fs"
  assumes "⊨ l → τ" 
  shows "∃z b. τ = ({ z : b | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) }) ∧ atom z ♯ tm"
proof -
  obtain z' and b where t:"τ = ({ z' : b | C_eq (CE_val (V_var z')) (CE_val (V_lit l)) })" using infer_l_elims  assms  using infer_l.simps type_for_lit.simps 
      type_for_lit.cases by blast
  obtain z::x where zf: "atom z ♯ tm" using obtain_fresh by metis
  have "τ = { z : b | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) }" using type_e_eq ce.fresh v.fresh l.fresh 
    by (metis t type_l_eq)
  thus ?thesis using zf by auto
qed

lemma infer_l_form3:
  fixes l::l
  assumes "⊨ l → τ" 
  shows "∃z. τ = ({ z : base_for_lit l | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) })"
  using infer_l_elims using assms  using infer_l.simps type_for_lit.simps base_for_lit.simps by auto

lemma infer_l_form4[simp]:
  fixes Γ::Γ
  assumes "Θ ; B ⊨_wf Γ "   
  shows "∃z. ⊨ l → ({ z : base_for_lit l | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) })"
  using assms  infer_l_form2 infer_l_form3 by metis

lemma infer_v_unit_form:
  fixes v::v
  assumes "P ; B ; Γ ⊨ v → ({ z1 : B_unit | c1 })" and "supp v = {}"
  shows "v = V_lit L_unit"
  using assms proof(nominal_induct Γ v "{ z1 : B_unit | c1 }" rule: infer_v.strong_induct)
  case (infer_v_varI Θ B c x z)
  then show ?case using supp_at_base by auto
next
  case (infer_v_litI Θ B Γ l)
  from ‹⊨ l → { z1 : B_unit | c1 }›  show ?case by(nominal_induct "{ z1 : B_unit | c1 }" rule: infer_l.strong_induct,auto)
qed

lemma base_for_lit_wf:
  assumes "⊨_wf Θ"
  shows   "Θ ; B ⊨_wf base_for_lit l"
  using base_for_lit.simps using  wfV_elims wf_intros  assms l.exhaust by metis

lemma infer_l_t_wf:
  fixes Γ::Γ
  assumes "Θ ; B ⊨_wf Γ ∧ atom z ♯ Γ"
  shows  "Θ; B; Γ ⊨_wf { z : base_for_lit l | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) }"
proof 
  show "atom z ♯ (Θ, B, Γ)" using  wfG_fresh_x assms by auto
  show "Θ ; B ⊨_wf base_for_lit l" using base_for_lit_wf assms wfX_wfY by metis
  thus "Θ; B; (z, base_for_lit l, TRUE) #_\<Gamma> Γ ⊨_wf CE_val (V_var z) == CE_val (V_lit l)" using wfC_v_eq wfV_litI assms wfX_wfY by metis
qed

lemma infer_l_wf:
  fixes l::l and Γ::Γ and τ::τ and Θ::Θ
  assumes "⊨ l → τ" and "Θ ; B ⊨_wf Γ"
  shows "⊨_wf Θ" and  "Θ ; B ⊨_wf Γ" and "Θ; B; Γ ⊨_wf τ"
proof -
  show *:"Θ ; B ⊨_wf Γ" using assms infer_l_elims by auto
  thus  "⊨_wf Θ" using wfX_wfY by auto
  show *:"Θ ; B ; Γ ⊨_wf τ" using infer_l_t_wf assms infer_l_form3 * 
    by (metis ‹⊨_wf Θ› fresh_GNil wfG_nilI wfT_weakening_nil)
qed

lemma infer_l_uniqueness: 
  fixes l::l
  assumes "⊨ l → τ" and "⊨ l → τ'" 
  shows "τ = τ'"
  using assms
proof -
  obtain z and b where zt: "τ = ({ z : b | C_eq (CE_val (V_var z)) (CE_val (V_lit l)) })" using infer_l_form assms by blast
  obtain z' and b where z't: "τ' = ({ z' : b | C_eq (CE_val (V_var z')) (CE_val (V_lit l)) })" using infer_l_form assms   by blast
  thus ?thesis using type_l_eq zt z't   assms infer_l.simps infer_l_elims l.distinct    
    by (metis infer_l_form3)
qed

section ‹Values›

lemma type_v_eq:
  assumes "{ z1 : b1 | c1 } = { z : b | C_eq (CE_val (V_var z)) (CE_val (V_var x)) }" and "atom z ♯ x"
  shows "b = b1" and "c1 = C_eq (CE_val (V_var z1)) (CE_val (V_var x))"
  using assms  by (auto,metis Abs1_eq_iff τ.eq_iff assms c.fresh ce.fresh type_e_eq v.fresh)

lemma infer_var2 [elim]:
  assumes "P; B ; G ⊨ V_var x → τ"
  shows "∃b c. Some (b,c) = lookup G x"
  using assms infer_v_elims lookup_iff   by (metis (no_types, lifting))

lemma infer_var3 [elim]:
  assumes "Θ; B; Γ ⊨ V_var x → τ"
  shows "∃z b c. Some (b,c) = lookup Γ x ∧ τ = ({ z : b | C_eq (CE_val (V_var z)) (CE_val (V_var x)) }) ∧ atom z ♯ x ∧ atom z ♯ (Θ, B, Γ)"
  using infer_v_elims(1)[OF assms(1)] by metis

lemma infer_bool_options2:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v → { z : b | c }" and "supp v = {} ∧ b = B_bool"
  shows  "v = V_lit L_true ∨ (v = (V_lit L_false))"
  using assms
proof(nominal_induct "{ z : b | c }"  rule: infer_v.strong_induct)
  case (infer_v_varI Θ B Γ c x z)
  then show ?case using v.supp supp_at_base by auto
next
  case (infer_v_litI Θ B Γ l)
  from ‹ ⊨ l → { z : b | c }› show ?case proof(nominal_induct "{ z : b | c }"  rule: infer_l.strong_induct)
    case (infer_trueI z)
    then show ?case by auto
  next
    case (infer_falseI z)
    then show ?case by auto
  next
    case (infer_natI n z)
    then show ?case using infer_v_litI by simp
  next
    case (infer_unitI z)
    then show ?case using infer_v_litI by simp
  next
    case (infer_bitvecI bv z)
    then show ?case using infer_v_litI by simp
  qed
qed(auto+)

lemma infer_bool_options:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v → { z : B_bool | c }" and "supp v = {}"
  shows "v = V_lit L_true ∨ (v = (V_lit L_false))"
  using infer_bool_options2  assms by blast

lemma infer_int2:
  fixes v::v
  assumes "Θ; B; Γ ⊨ v → { z : b | c }"
  shows "supp v = {} ∧ b = B_int ⟶ (∃n. v = V_lit (L_num n))"
  using assms
proof(nominal_induct "{ z : b | c }"  rule: infer_v.strong_induct)
  case (infer_v_varI Θ B Γ c x z)
  then show ?case using v.supp supp_at_base by auto
next
  case (infer_v_litI Θ B Γ l)
  from ‹ ⊨ l → { z : b | c }› show ?case proof(nominal_induct "{ z : b | c }"  rule: infer_l.strong_induct)
    case (infer_trueI z)
    then show ?case by auto
  next
    case (infer_falseI z)
    then show ?case by auto
  next
    case (infer_natI n z)
    then show ?case using infer_v_litI by simp
  next
    case (infer_unitI z)
    then show ?case using infer_v_litI by simp
  next
    case (infer_bitvecI bv z)
    then show ?case using infer_v_litI by simp
  qed
qed(auto+)

lemma infer_bitvec:
  fixes \<Theta>::\<Theta> and v::v
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<lbrace> z' : B_bitvec | c' \<rbrace>" and "supp v = {}"
  shows "\<exists>bv. v = V_lit (L_bitvec bv)"
  using assms proof(nominal_induct v rule: v.strong_induct)
  case (V_lit l)
  then show ?case by(nominal_induct l rule: l.strong_induct,force+)
next
  case (V_consp s dc b v)
  then show ?case using  infer_v_elims(7)[OF V_consp(2)] \<tau>.eq_iff by auto
next
  case (V_var x)
  then show ?case using supp_at_base by auto
qed(force+)

lemma infer_int:
  assumes "infer_v \<Theta> \<B> \<Gamma> v  (\<lbrace> z : B_int | c \<rbrace>)" and "supp v= {}"
  shows "\<exists>n. V_lit (L_num n) = v"
  using assms infer_int2  by (metis (no_types, lifting))

lemma infer_lit:
  assumes "infer_v \<Theta> \<B> \<Gamma> v  (\<lbrace> z : b | c \<rbrace>)" and "supp v= {}" and "b \<in> { B_bool , B_int , B_unit }"
  shows "\<exists>l. V_lit l = v"
  using assms proof(nominal_induct v rule: v.strong_induct)
  case (V_lit x)
  then show ?case   by (simp add: supp_at_base)
next
  case (V_var x)
  then show ?case 
    by (simp add: supp_at_base)
next
  case (V_pair x1a x2a)
  then show ?case  using supp_at_base by auto
next
  case (V_cons x1a x2a x3)
  then show ?case   using supp_at_base by auto
next
  case (V_consp x1a x2a x3 x4)
  then show ?case    using supp_at_base by auto
qed

lemma infer_v_form[simp]:
  fixes v::v
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<tau>" 
  shows "\<exists>z b. \<tau> = (\<lbrace> z : b | C_eq (CE_val (V_var z)) (CE_val v)\<rbrace>) \<and> atom z \<sharp> v \<and> atom z \<sharp> (\<Theta>, \<B>, \<Gamma>)"
  using assms
proof(nominal_induct   rule: infer_v.strong_induct)
  case (infer_v_varI \<Theta> \<B> \<Gamma> b c x z)
  then show ?case by force
next
  case (infer_v_litI \<Theta> \<B> \<Gamma> l \<tau>)
  then obtain z and b where "\<tau> = \<lbrace> z : b  | CE_val (V_var z)  ==  CE_val (V_lit l)  \<rbrace> \<and>atom z \<sharp> (\<Theta>, \<B>, \<Gamma>) "
    using infer_l_form by metis
  moreover hence  "atom z \<sharp> (V_lit l)" using supp_l_empty v.fresh(1) fresh_prod2 fresh_def by blast
  ultimately show ?case by metis
next
  case (infer_v_pairI z v1 v2 \<Theta> \<B> \<Gamma> t1 t2)
  then show ?case by force
next
  case (infer_v_consI s dclist \<Theta> dc tc \<B> \<Gamma> v tv z)
  moreover hence "atom z \<sharp> (V_cons s dc v)" using
      Un_commute b.supp(3) fresh_def sup_bot.right_neutral supp_b_empty v.supp(4) pure_supp by metis
  ultimately show ?case using fresh_prodN by metis
next
  case (infer_v_conspI s bv dclist \<Theta> dc tc \<B> \<Gamma> v tv b z)
  moreover hence "atom z \<sharp> (V_consp s dc b v)" unfolding v.fresh using pure_fresh fresh_prodN * by metis
  ultimately show ?case using fresh_prodN by metis
qed

lemma infer_v_form2:
  fixes v::v
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> (\<lbrace> z : b | c \<rbrace>)" and "atom z \<sharp> v" 
  shows "c = C_eq (CE_val (V_var z)) (CE_val v)"
  using assms 
proof -
  obtain z' and b' where "(\<lbrace> z : b | c \<rbrace>)  = (\<lbrace> z' : b'  | CE_val (V_var z')  ==  CE_val v  \<rbrace>) \<and> atom z' \<sharp> v"
    using infer_v_form assms by meson
  thus ?thesis using Abs1_eq_iff(3) \<tau>.eq_iff  type_e_eq
    by (metis assms(2) ce.fresh(1))
qed

lemma infer_v_form3:
  fixes v::v
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<tau>"  and "atom z \<sharp> (v,\<Gamma>)"
  shows "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<lbrace> z : b_of \<tau> | C_eq (CE_val (V_var z)) (CE_val v)\<rbrace>"
proof -
  obtain z' and b' where "\<tau> = \<lbrace> z' : b' | C_eq (CE_val (V_var z')) (CE_val v)\<rbrace> \<and> atom z' \<sharp> v \<and> atom z' \<sharp> (\<Theta>, \<B>, \<Gamma>)" 
    using infer_v_form assms by metis
  moreover hence "\<lbrace> z' : b' | C_eq (CE_val (V_var z')) (CE_val v)\<rbrace> = \<lbrace> z : b' | C_eq (CE_val (V_var z)) (CE_val v)\<rbrace>" 
    using assms type_e_eq fresh_Pair ce.fresh by auto
  ultimately show  ?thesis using  b_of.simps assms by auto
qed

lemma infer_v_form4:
  fixes v::v
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<tau>"  and "atom z \<sharp> (v,\<Gamma>)" and "b = b_of \<tau>"
  shows "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<lbrace> z : b | C_eq (CE_val (V_var z)) (CE_val v)\<rbrace>"
  using assms infer_v_form3 by simp

lemma infer_v_v_wf:
  fixes v::v
  shows "\<Theta>; \<B> ; G \<turnstile> v \<Rightarrow> \<tau> \<Longrightarrow>  \<Theta>; \<B>; G \<turnstile>\<^sub>w\<^sub>f v : (b_of \<tau>)"
proof(induct rule: infer_v.induct)
  case (infer_v_varI \<Theta> \<B> \<Gamma> b c x z)
  then show ?case using  wfC_elims  wf_intros by auto
next
  case (infer_v_pairI z v1 v2 \<Theta> \<B> \<Gamma> t1 t2)
  then show ?case using  wfC_elims  wf_intros by auto
next
  case (infer_v_litI \<Theta> \<B> \<Gamma> l \<tau>)
  hence "b_of \<tau> = base_for_lit l" using infer_l_form3 b_of.simps by metis
  then show ?case using wfV_litI infer_l_wf infer_v_litI wfG_b_weakening
    by (metis fempty_fsubsetI)
next
  case (infer_v_consI s dclist \<Theta> dc tc \<B> \<Gamma> v tv z)
  then show ?case using  wfC_elims  wf_intros 
    by (metis (no_types, lifting) b_of.simps has_fresh_z2 subtype_eq_base2)
next
  case (infer_v_conspI s bv dclist \<Theta> dc tc \<B> \<Gamma> v tv b z)
  obtain z1 b1 c1 where t:"tc = \<lbrace> z1 : b1 | c1 \<rbrace>" using obtain_fresh_z by metis
  show ?case unfolding b_of.simps proof(rule wfV_conspI)
    show \<open>AF_typedef_poly s bv dclist \<in> set \<Theta>\<close> using infer_v_conspI by auto
    show \<open>(dc,  \<lbrace> z1 : b1 | c1 \<rbrace> ) \<in> set dclist\<close> using infer_v_conspI t by auto
    show \<open> \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f b \<close> using infer_v_conspI by auto
    show \<open>atom bv \<sharp> (\<Theta>, \<B>, \<Gamma>, b, v)\<close> using infer_v_conspI by auto
    have " b1[bv::=b]\<^sub>b\<^sub>b = b_of tv" using subtype_eq_base2[OF infer_v_conspI(5)] b_of.simps t subst_tb.simps by auto
    thus \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b1[bv::=b]\<^sub>b\<^sub>b \<close> using infer_v_conspI by auto
  qed
qed

lemma infer_v_t_form_wf:
  assumes " wfB \<Theta> \<B> b" and "wfV  \<Theta> \<B> \<Gamma> v b" and "atom z \<sharp> \<Gamma>"
  shows "wfT \<Theta> \<B> \<Gamma> \<lbrace> z : b | C_eq (CE_val (V_var z)) (CE_val v)\<rbrace>"
  using wfT_v_eq assms by auto

lemma infer_v_t_wf:
  fixes v::v
  assumes "\<Theta>; \<B>; G \<turnstile> v \<Rightarrow> \<tau>"
  shows "wfT \<Theta> \<B> G \<tau> \<and>  wfB  \<Theta> \<B> (b_of \<tau>) "
proof -
  obtain z and b where "\<tau> = \<lbrace> z : b  | CE_val (V_var z)  ==  CE_val v  \<rbrace> \<and> atom z \<sharp> v \<and> atom z \<sharp> (\<Theta>, \<B>, G)" using infer_v_form assms by metis
  moreover have  "wfB  \<Theta> \<B> b" using infer_v_v_wf b_of.simps wfX_wfB(1) assms 
    using calculation by fastforce
  ultimately show "wfT \<Theta> \<B> G \<tau> \<and>   wfB  \<Theta> \<B> (b_of \<tau>)" using infer_v_v_wf  infer_v_t_form_wf assms by fastforce
qed

lemma infer_v_wf: 
  fixes  v::v
  assumes "\<Theta>; \<B>; G \<turnstile> v \<Rightarrow> \<tau>"
  shows  "\<Theta>; \<B>; G \<turnstile>\<^sub>w\<^sub>f v : (b_of \<tau>)" and "wfT \<Theta> \<B> G \<tau>"  and "wfTh \<Theta>" and "wfG \<Theta> \<B> G"
proof -
  show "\<Theta>; \<B>; G \<turnstile>\<^sub>w\<^sub>f v : b_of \<tau> " using infer_v_v_wf assms by auto
  show "\<Theta>; \<B>; G   \<turnstile>\<^sub>w\<^sub>f \<tau>" using infer_v_t_wf assms by auto
  thus  "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f G" using wfX_wfY by auto
  thus  "\<turnstile>\<^sub>w\<^sub>f \<Theta>" using  wfX_wfY by auto
qed

lemma check_bool_options:
  assumes "\<Theta>; \<B>; \<Gamma>  \<turnstile> v \<Leftarrow> \<lbrace> z : B_bool  | TRUE \<rbrace>" and "supp v = {}"
  shows "v = V_lit L_true \<or> v = V_lit L_false"
proof -
  obtain t1 where  " \<Theta>; \<B>; \<Gamma>  \<turnstile> t1 \<lesssim>  \<lbrace> z : B_bool  | TRUE \<rbrace> \<and> \<Theta>; \<B>; \<Gamma>  \<turnstile> v \<Rightarrow> t1" using check_v_elims 
    using assms by blast
  thus ?thesis using infer_bool_options assms
    by (metis \<tau>.exhaust b_of.simps subtype_eq_base2)
qed

lemma check_v_wf:
  fixes v::v and \<Gamma>::\<Gamma> and \<tau>::\<tau>
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Leftarrow> \<tau>"
  shows " \<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f \<Gamma>" and "\<Theta>; \<B>;\<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b_of \<tau>" and "\<Theta>; \<B>;\<Gamma> \<turnstile>\<^sub>w\<^sub>f \<tau>"
proof -
  obtain \<tau>' where *: "\<Theta>; \<B>; \<Gamma> \<turnstile> \<tau>' \<lesssim> \<tau> \<and> \<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<tau>'" using check_v_elims assms by auto
  thus "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma> " and "\<Theta>; \<B>;\<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b_of \<tau>" and "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<tau>"  
    using infer_v_wf infer_v_v_wf  subtype_eq_base2   *  subtype_wf  by metis+
qed

lemma infer_v_form_fresh:
  fixes v::v and t::"'a::fs" 
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<tau>" 
  shows "\<exists>z b. \<tau> = \<lbrace> z : b | C_eq (CE_val (V_var z)) (CE_val v)\<rbrace> \<and> atom z \<sharp> (t,v)"
proof -
  obtain z' and b' where "\<tau> = \<lbrace> z' : b' | C_eq (CE_val (V_var z')) (CE_val v)\<rbrace>" using infer_v_form assms by blast
  moreover then obtain z and b and c where "\<tau> = \<lbrace> z : b | c \<rbrace> \<and> atom z \<sharp> (t,v)" using obtain_fresh_z by metis
  ultimately have "\<tau> = \<lbrace> z : b | C_eq (CE_val (V_var z)) (CE_val v)\<rbrace> \<and>  atom z \<sharp> (t,v) "
    using assms infer_v_form2  by auto
  thus ?thesis by blast
qed

text \<open> More generally, if support of a term is empty then any G will do \<close>

lemma infer_v_form_consp:
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> V_consp s dc b v \<Rightarrow> \<tau>"
  shows "b_of \<tau> = B_app s b"
  using assms proof(nominal_induct "V_consp s dc b v" \<tau>   rule: infer_v.strong_induct)
  case (infer_v_conspI bv dclist \<Theta> tc \<B> \<Gamma> tv z)
  then show ?case using b_of.simps by metis
qed

lemma lookup_in_rig_b:
  assumes "Some (b2, c2) = lookup (\<Gamma>[x\<longmapsto>c']) x'" and
    "Some (b1, c1) = lookup \<Gamma> x'"
  shows "b1 = b2"
  using assms lookup_in_rig[OF assms(2)] 
  by (metis option.inject prod.inject)

lemma infer_v_uniqueness_rig:
  fixes x::x and c::c
  assumes "infer_v P B G v \<tau>" and "infer_v P B (replace_in_g G x c') v \<tau>'"
  shows "\<tau> = \<tau>'"
  using assms
proof(nominal_induct "v"  arbitrary: \<tau>' \<tau> rule: v.strong_induct)
  case (V_lit l)
  hence "infer_l l \<tau>" and "infer_l l \<tau>'" using assms(1) infer_v_elims(2) by auto
  then show ?case using infer_l_uniqueness  by presburger
next
  case (V_var y)

  obtain b and c where bc: "Some (b,c) = lookup G y"  
    using assms(1) infer_v_elims(2)  using V_var.prems(1) lookup_iff by force
  then obtain  c'' where bc':"Some (b,c'') = lookup  (replace_in_g G x c') y" 
    using lookup_in_rig by blast

  obtain z  where "\<tau> = (\<lbrace> z : b |  C_eq (CE_val (V_var z)) (CE_val (V_var y)) \<rbrace>)" using infer_v_elims(1)[of P B G y \<tau>] V_var
      bc option.inject prod.inject lookup_in_g by metis
  moreover obtain z' where "\<tau>' = (\<lbrace> z' : b |  C_eq (CE_val (V_var z')) (CE_val (V_var y)) \<rbrace>)" using infer_v_elims(1)[of P B _ y \<tau>']  V_var
      option.inject prod.inject  lookup_in_rig  by (metis bc')
  ultimately show ?case using type_e_eq 
    by (metis V_var.prems(1) V_var.prems(2) \<tau>.eq_iff ce.fresh(1) finite.emptyI fresh_atom_at_base 
        fresh_finite_insert infer_v_elims(1) v.fresh(2))
next 
  case (V_pair v1 v2)
  obtain  z and z1 and z2 and t1 and t2 and c1 and c2 where
    t1: "\<tau> = (\<lbrace> z :  [ b_of t1 , b_of t2 ]\<^sup>b   | CE_val (V_var z)  ==  CE_val (V_pair v1 v2)  \<rbrace>) \<and> 
           atom z \<sharp> (v1, v2) \<and>  P ; B ; G  \<turnstile> v1 \<Rightarrow> t1 \<and>  P ; B ; G  \<turnstile> v2 \<Rightarrow> t2"
    using infer_v_elims(3)[OF V_pair(3)] by metis
  moreover obtain  z' and z1' and z2' and t1' and t2' and c1' and c2' where
    t2: "\<tau>' = (\<lbrace> z' :  [ b_of t1' , b_of t2' ]\<^sup>b  | CE_val (V_var z')  ==  CE_val (V_pair v1 v2)  \<rbrace>) \<and> 
             atom z' \<sharp> (v1, v2) \<and>  P ;  B ; (replace_in_g G x c')  \<turnstile> v1 \<Rightarrow> t1' \<and>  
             P ;  B ; (replace_in_g G x c')  \<turnstile> v2 \<Rightarrow> t2'"
    using infer_v_elims(3)[OF V_pair(4)] by metis
  ultimately have "t1 = t1' \<and> t2 = t2'" using V_pair.hyps(1) V_pair.hyps(2) \<tau>.eq_iff by blast
  then show ?case using t1 t2 by simp
next
  case (V_cons s dc v)
  obtain x and z and tc and dclist where  t1: "\<tau> = (\<lbrace> z : B_id s  | CE_val (V_var z)  ==  CE_val (V_cons s dc v) \<rbrace>) \<and>  
          AF_typedef s dclist \<in> set P \<and>
        (dc, tc) \<in> set dclist \<and> atom z \<sharp> v" 
    using infer_v_elims(4)[OF V_cons(2)] by metis
  moreover obtain x' and z' and tc' and dclist' where  t2: "\<tau>' = (\<lbrace> z' : B_id s  | CE_val (V_var z')  ==  CE_val (V_cons s dc v) \<rbrace>)
  \<and>  AF_typedef s dclist' \<in> set P \<and> (dc, tc') \<in> set dclist' \<and> atom z' \<sharp> v" 
    using infer_v_elims(4)[OF V_cons(3)] by metis
  moreover have a: "AF_typedef s dclist' \<in> set P" and b:"(dc,tc') \<in> set dclist'" and c:"AF_typedef s dclist \<in> set P" and
    d:"(dc, tc) \<in> set dclist" using t1 t2 by auto
  ultimately have "tc =  tc'" using wfTh_dc_t_unique2   infer_v_wf(3)[OF V_cons(2)] by metis

  moreover have "atom z \<sharp> CE_val (V_cons s dc v) \<and> atom z' \<sharp> CE_val (V_cons s dc v)" 
    using e.fresh(1)  v.fresh(4) t1 t2 pure_fresh by auto
  ultimately have "(\<lbrace> z : B_id s  | CE_val (V_var z)  ==  CE_val (V_cons s dc v) \<rbrace>) = (\<lbrace> z' : B_id s  | CE_val (V_var z')  ==  CE_val (V_cons s dc v) \<rbrace>)" 
    using type_e_eq by metis
  thus ?case using t1 t2 by simp
next
  case (V_consp s dc b v)
  from V_consp(2) V_consp show ?case proof(nominal_induct  "V_consp s dc b v" \<tau> arbitrary: v rule:infer_v.strong_induct)

    case (infer_v_conspI bv dclist \<Theta> tc \<B> \<Gamma> v tv z)

    obtain z3 and b3 where *:"\<tau>' = \<lbrace> z3 : b3 | [ [ z3 ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ V_consp s dc b v ]\<^sup>c\<^sup>e  \<rbrace> \<and> atom z3 \<sharp>  V_consp s dc b v"
      using infer_v_form[OF \<open>\<Theta>; \<B>; \<Gamma>[x\<longmapsto>c'] \<turnstile> V_consp s dc b v \<Rightarrow> \<tau>'\<close> ] by metis
    moreover then have "b3 = B_app s b" using  infer_v_form_consp b_of.simps * infer_v_conspI by metis

    moreover have "\<lbrace> z3 : B_app s b  | [ [ z3 ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ V_consp s dc b v ]\<^sup>c\<^sup>e  \<rbrace> =  \<lbrace> z : B_app s b  | [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ V_consp s dc b v ]\<^sup>c\<^sup>e  \<rbrace>"
    proof - 
      have "atom z3 \<sharp> [V_consp s dc b v]\<^sup>c\<^sup>e" using * ce.fresh by auto
      moreover have "atom z \<sharp> [V_consp s dc b v]\<^sup>c\<^sup>e" using * infer_v_conspI ce.fresh v.fresh pure_fresh by metis
      ultimately show ?thesis  using type_e_eq  infer_v_conspI v.fresh ce.fresh by metis
    qed
    ultimately  show ?case using * by auto
  qed
qed

lemma infer_v_uniqueness: 
  assumes "infer_v P B G v \<tau>" and "infer_v P B G v \<tau>'"
  shows "\<tau> = \<tau>'"
proof - 
  obtain x::x where "atom x \<sharp> G" using obtain_fresh by metis
  hence "G [ x \<longmapsto> C_true ] = G" using replace_in_g_forget assms infer_v_wf by fast
  thus ?thesis using infer_v_uniqueness_rig assms by metis
qed

lemma infer_v_tid_form:
  fixes v::v
  assumes "\<Theta> ; B ; \<Gamma>  \<turnstile> v \<Rightarrow> \<lbrace> z : B_id tid  | c \<rbrace>" and  "AF_typedef tid dclist \<in> set \<Theta>" and "supp v = {}"
  shows "\<exists>dc v' t. v = V_cons tid dc v' \<and> (dc , t ) \<in> set dclist"
  using assms proof(nominal_induct  v "\<lbrace> z : B_id tid  | c \<rbrace>" rule: infer_v.strong_induct)
  case (infer_v_varI \<Theta> \<B> c x z)
  then show ?case using v.supp supp_at_base  by auto
next
  case (infer_v_litI \<Theta> \<B> l)
  then show ?case by auto
next
  case (infer_v_consI dclist1 \<Theta> dc tc \<B> \<Gamma> v tv z)
  hence "supp v = {}" using v.supp by simp
  then obtain dca and v' where *:"V_cons tid dc v = V_cons tid dca v'" using infer_v_consI by auto
  hence "dca = dc" using v.eq_iff(4)  by auto
  hence  "V_cons tid dc v = V_cons tid dca v' \<and>  (dca, tc) \<in> set dclist1" using infer_v_consI * by auto
  moreover have "dclist = dclist1" using wfTh_dclist_unique infer_v_consI wfX_wfY \<open>dca=dc\<close> 
  proof -
    show ?thesis
      by (meson \<open>AF_typedef tid dclist1 \<in> set \<Theta>\<close> \<open>\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> tv\<close> infer_v_consI.prems infer_v_wf(4) wfTh_dclist_unique wfX_wfY) 
  qed
  ultimately show ?case by auto
qed

lemma check_v_tid_form:  
  assumes "\<Theta> ; B ; \<Gamma>  \<turnstile> v \<Leftarrow> \<lbrace> z : B_id tid  | TRUE \<rbrace>"  and "AF_typedef tid dclist \<in> set \<Theta>"  and "supp v = {}"
  shows "\<exists>dc v' t. v = V_cons tid dc v' \<and> (dc , t ) \<in> set dclist"
  using assms proof(nominal_induct  v "\<lbrace> z : B_id tid  | TRUE \<rbrace>" rule: check_v.strong_induct)
  case (check_v_subtypeI \<Theta> \<B> \<Gamma> \<tau>1 v)
  then obtain z and c where "\<tau>1 = \<lbrace> z : B_id tid | c \<rbrace>" using subtype_eq_base2 b_of.simps 
    by (metis obtain_fresh_z2)
  then show ?case  using infer_v_tid_form check_v_subtypeI by simp
qed

lemma check_v_num_leq:
  fixes n::int and \<Gamma>::\<Gamma>
  assumes "0 \<le> n \<and> n \<le> int (length v)" and " \<turnstile>\<^sub>w\<^sub>f \<Theta> " and "\<Theta> ; {||} \<turnstile>\<^sub>w\<^sub>f \<Gamma>"
  shows "\<Theta> ; {||} ; \<Gamma>  \<turnstile> [ L_num n ]\<^sup>v \<Leftarrow> \<lbrace> z : B_int  | ([ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e)   
       AND  ([ leq [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec  v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e )  \<rbrace>" 
proof - 
  have "\<Theta> ; {||} ; \<Gamma>  \<turnstile> [ L_num n ]\<^sup>v \<Rightarrow>  \<lbrace> z : B_int  | [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e  \<rbrace>" 
    using infer_v_litI infer_natI wfG_nilI assms by auto
  thus ?thesis using subtype_range[OF assms(1) ] assms check_v_subtypeI by metis
qed

lemma check_int:
  assumes "check_v \<Theta> \<B> \<Gamma> v  (\<lbrace> z : B_int | c \<rbrace>)" and "supp v = {}"
  shows "\<exists>n. V_lit (L_num n) = v"
  using assms infer_int check_v_elims  by (metis b_of.simps infer_v_form subtype_eq_base2)

definition sble :: "\<Theta> \<Rightarrow> \<Gamma> \<Rightarrow> bool" where
  "sble \<Theta> \<Gamma> = (\<exists>i. i \<Turnstile> \<Gamma> \<and> \<Theta> ; \<Gamma> \<turnstile> i)"

lemma check_v_range:
  assumes "\<Theta> ; B ; \<Gamma> \<turnstile> v2 \<Leftarrow> \<lbrace> z : B_int  | [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   AND  
            [ leq [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e [| [ v1 ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   \<rbrace>  "
    (is "\<Theta> ; ?B ; \<Gamma> \<turnstile> v2 \<Leftarrow> \<lbrace> z : B_int | ?c1 \<rbrace>") 
    and "v1 = V_lit (L_bitvec bv) \<and> v2 = V_lit (L_num n) " and "atom z \<sharp> \<Gamma>" and "sble \<Theta> \<Gamma>"
  shows "0 \<le> n \<and> n \<le> int (length bv)"
proof - 
  have  "\<Theta> ; ?B ; \<Gamma> \<turnstile>  \<lbrace>   z : B_int  |  [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e == [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrace> \<lesssim> \<lbrace> z : B_int | ?c1 \<rbrace>" 
    using check_v_elims assms 
    by (metis infer_l_uniqueness infer_natI infer_v_elims(2))
  moreover have "atom z \<sharp> \<Gamma>" using fresh_GNil assms by simp
  ultimately have  "\<Theta> ; ?B ; ((z, B_int, [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> \<Gamma>)  \<Turnstile> ?c1" 
    using subtype_valid_simple by auto
  thus ?thesis using assms valid_range_length_inv check_v_wf wfX_wfY sble_def by metis
qed

section \<open>Expressions\<close>

lemma infer_e_plus[elim]:
  fixes v1::v and v2::v
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> AE_op Plus v1 v2 \<Rightarrow> \<tau>"
  shows "\<exists>z . (\<lbrace> z : B_int |  C_eq (CE_val (V_var z)) (CE_op Plus [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e) \<rbrace> = \<tau>)"
  using infer_e_elims assms by metis

lemma infer_e_leq[elim]:
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> AE_op LEq v1 v2 \<Rightarrow> \<tau>"
  shows "\<exists>z . (\<lbrace> z : B_bool |  C_eq (CE_val (V_var z)) (CE_op LEq [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e) \<rbrace> = \<tau>)"
  using infer_e_elims assms by metis

lemma infer_e_eq[elim]:
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> AE_op Eq v1 v2 \<Rightarrow> \<tau>"
  shows "\<exists>z . (\<lbrace> z : B_bool |  C_eq (CE_val (V_var z)) (CE_op Eq [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e) \<rbrace> = \<tau>)"
  using infer_e_elims(25)[OF assms] by metis

lemma infer_e_e_wf: 
  fixes e::e
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> e \<Rightarrow> \<tau>" 
  shows "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f e : b_of \<tau>" 
  using assms proof(nominal_induct \<tau> avoiding: \<tau> rule: infer_e.strong_induct)
  case (infer_e_valI \<Theta> \<B> \<Gamma> \<Delta>' \<Phi> v \<tau>)
  then show ?case using  infer_v_v_wf wf_intros by metis
next
  case (infer_e_plusI \<Theta> \<B> \<Gamma> \<Delta>' \<Phi> v1 z1 c1 v2 z2 c2 z3)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_leqI \<Theta> \<B> \<Gamma> \<Delta>' v1 z1 c1 v2 z2 c2 z3)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_eqI \<Theta> \<B> \<Gamma> \<Delta>' v1 z1 c1 v2 z2 c2 z3)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_appI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> f x b c \<tau>' s' v \<tau>'')
  have "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f AE_app f v : b_of \<tau>' " proof 
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using infer_e_appI by auto
    show \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using infer_e_appI by auto
    show \<open>Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c \<tau>' s'))) = lookup_fun \<Phi> f\<close> using infer_e_appI by auto
    show "\<Theta>; \<B>;\<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b" using infer_e_appI check_v_wf b_of.simps by metis
  qed
  moreover have "b_of \<tau>' = b_of (\<tau>'[x::=v]\<^sub>v)" using subst_tbase_eq subst_v_\<tau>_def by auto
  ultimately show ?case using infer_e_appI subst_v_c_def subst_b_\<tau>_def by auto
next
  case (infer_e_appPI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> b' f bv x b c \<tau>'' s' v \<tau>')

  have "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f AE_appP f b' v : (b_of \<tau>'')[bv::=b']\<^sub>b " proof
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using infer_e_appPI by auto
    show \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using infer_e_appPI by auto
    show \<open>Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c \<tau>'' s'))) = lookup_fun \<Phi> f\<close> using * infer_e_appPI by metis
    show "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f b'" using infer_e_appPI by auto
    show "\<Theta>; \<B>;\<Gamma> \<turnstile>\<^sub>w\<^sub>f v : (b[bv::=b']\<^sub>b)" using infer_e_appPI check_v_wf b_of.simps subst_b_b_def by metis
    have "atom bv \<sharp> (b_of \<tau>'')[bv::=b']\<^sub>b\<^sub>b" using fresh_subst_if subst_b_b_def infer_e_appPI by metis
    thus  "atom bv \<sharp> (\<Phi>, \<Theta>, \<B>, \<Gamma>, \<Delta>, b', v, (b_of \<tau>'')[bv::=b']\<^sub>b)" using infer_e_appPI fresh_prodN subst_b_b_def by metis
  qed
  moreover have "b_of \<tau>' = (b_of \<tau>'')[bv::=b']\<^sub>b" 
    using \<open>\<tau>''[bv::=b']\<^sub>b[x::=v]\<^sub>v = \<tau>'\<close> b_of_subst_bb_commute subst_tbase_eq  subst_b_b_def subst_v_\<tau>_def subst_b_\<tau>_def by auto
  ultimately show ?case using infer_e_appI by auto
next
  case (infer_e_fstI \<Theta> \<B> \<Gamma> \<Delta>' \<Phi> v z' b1 b2 c z)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_sndI \<Theta> \<B> \<Gamma> \<Delta>' \<Phi> v z' b1 b2 c z)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_lenI \<Theta> \<B> \<Gamma> \<Delta>' \<Phi> v z' c z)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_mvarI \<Theta> \<Gamma> \<Phi> \<Delta> u \<tau>)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_concatI \<Theta> \<B> \<Gamma> \<Delta>' \<Phi> v1 z1 c1 v2 z2 c2 z3)
  then show ?case using  b_of.simps infer_v_v_wf wf_intros by metis
next
  case (infer_e_splitI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v1 z1 c1 v2 z2 z3)
  have " \<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f AE_split v1 v2  : B_pair B_bitvec B_bitvec"
  proof
    show "\<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi>" using infer_e_splitI by auto
    show "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta>" using infer_e_splitI by auto 
    show "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v1 : B_bitvec" using infer_e_splitI b_of.simps infer_v_wf by metis
    show "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v2 : B_int" using infer_e_splitI b_of.simps check_v_wf by metis
  qed  
  then show ?case using  b_of.simps by auto
qed

lemma infer_e_t_wf:
  fixes e::e and \<Gamma>::\<Gamma> and \<tau>::\<tau> and \<Delta>::\<Delta> and \<Phi>::\<Phi>
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> e \<Rightarrow> \<tau>"
  shows "\<Theta>; \<B>;\<Gamma> \<turnstile>\<^sub>w\<^sub>f \<tau> \<and> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi>" 
  using assms proof(induct  rule: infer_e.induct)
  case (infer_e_valI \<Theta> \<B> \<Gamma> \<Delta>' \<Phi> v \<tau>)
  then show ?case using infer_v_t_wf by auto
next
  case (infer_e_plusI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v1 z1 c1 v2 z2 c2 z3)
  hence "\<Theta>; \<B>; \<Gamma>  \<turnstile>\<^sub>w\<^sub>f CE_op Plus [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e : B_int" using wfCE_plusI wfD_emptyI wfPhi_emptyI infer_v_v_wf  wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_plusI by auto
next
  case (infer_e_leqI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v1 z1 c1 v2 z2 c2 z3)
  hence " \<Theta>; \<B>; \<Gamma>  \<turnstile>\<^sub>w\<^sub>f CE_op LEq [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e : B_bool" using wfCE_leqI wfD_emptyI wfPhi_emptyI infer_v_v_wf wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_leqI by auto
next
  case (infer_e_eqI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v1 z1 b c1 v2 z2 c2 z3)
  hence " \<Theta>; \<B>; \<Gamma>  \<turnstile>\<^sub>w\<^sub>f CE_op Eq [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e : B_bool" using wfCE_eqI wfD_emptyI wfPhi_emptyI infer_v_v_wf wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_eqI by auto
next
  case (infer_e_appI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> f x b c \<tau> s' v \<tau>')
  show ?case proof
    show "\<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi>" using infer_e_appI by auto
    show "\<Theta>; \<B>; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau>'" proof -
      have *:" \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b " using infer_e_appI check_v_wf(2) b_of.simps by metis
      moreover have *:"\<Theta>; \<B>; (x, b, c) #\<^sub>\<Gamma> \<Gamma>  \<turnstile>\<^sub>w\<^sub>f \<tau>" proof(rule  wf_weakening1(4))
        show \<open> \<Theta>; \<B>; (x,b,c)#\<^sub>\<Gamma>GNil  \<turnstile>\<^sub>w\<^sub>f \<tau> \<close> using  wfPhi_f_simple_wfT wfD_wf infer_e_appI wb_b_weakening by fastforce
        have "\<Theta> ;  \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<lbrace> x : b | c \<rbrace>" using infer_e_appI check_v_wf(3) by auto
        thus  \<open> \<Theta> ;  \<B> \<turnstile>\<^sub>w\<^sub>f (x, b, c) #\<^sub>\<Gamma> \<Gamma> \<close> using infer_e_appI 
            wfT_wfC[THEN wfG_consI[rotated 3] ]  *  wfT_wf_cons fresh_prodN by simp
        show \<open>toSet ((x,b,c)#\<^sub>\<Gamma>GNil) \<subseteq> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)\<close> using toSet.simps by auto
      qed
      moreover have "((x, b, c) #\<^sub>\<Gamma> \<Gamma>)[x::=v]\<^sub>\<Gamma>\<^sub>v = \<Gamma>" using subst_gv.simps by auto

      ultimately show ?thesis using infer_e_appI wf_subst1(4)[OF *, of GNil x b c \<Gamma> v] subst_v_\<tau>_def by auto
    qed
  qed
next
  case (infer_e_appPI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> b' f bv x b c \<tau>' s' v \<tau>)

  have "\<Theta>; \<B>; ((x, b[bv::=b']\<^sub>b\<^sub>b, c[bv::=b']\<^sub>c\<^sub>b) #\<^sub>\<Gamma> \<Gamma>)[x::=v]\<^sub>\<Gamma>\<^sub>v \<turnstile>\<^sub>w\<^sub>f (\<tau>'[bv::=b']\<^sub>b)[x::=v]\<^sub>\<tau>\<^sub>v" 
  proof(rule wf_subst(4))
    show \<open> \<Theta>; \<B>; (x, b[bv::=b']\<^sub>b\<^sub>b, c[bv::=b']\<^sub>c\<^sub>b) #\<^sub>\<Gamma> \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau>'[bv::=b']\<^sub>b \<close>  
    proof(rule  wf_weakening1(4))
      have  \<open> \<Theta> ; {|bv|} ; (x,b,c)#\<^sub>\<Gamma>GNil  \<turnstile>\<^sub>w\<^sub>f \<tau>' \<close> using  wfPhi_f_poly_wfT  infer_e_appI infer_e_appPI by simp
      thus  \<open> \<Theta>; \<B>; (x,b[bv::=b']\<^sub>b\<^sub>b,c[bv::=b']\<^sub>c\<^sub>b)#\<^sub>\<Gamma>GNil  \<turnstile>\<^sub>w\<^sub>f \<tau>'[bv::=b']\<^sub>b \<close> 
        using wfT_subst_wfT infer_e_appPI wb_b_weakening subst_b_\<tau>_def subst_v_\<tau>_def by presburger
      have "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<lbrace> x :  b[bv::=b']\<^sub>b\<^sub>b | c[bv::=b']\<^sub>c\<^sub>b \<rbrace>" 
        using infer_e_appPI check_v_wf(3) subst_b_b_def subst_b_c_def by metis
      thus  \<open> \<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f (x, b[bv::=b']\<^sub>b\<^sub>b, c[bv::=b']\<^sub>c\<^sub>b) #\<^sub>\<Gamma> \<Gamma> \<close> 
        using infer_e_appPI wfT_wfC[THEN wfG_consI[rotated 3] ]  * wfX_wfY wfT_wf_cons wb_b_weakening by metis
      show \<open>toSet ((x,b[bv::=b']\<^sub>b\<^sub>b,c[bv::=b']\<^sub>c\<^sub>b)#\<^sub>\<Gamma>GNil) \<subseteq> toSet ((x, b[bv::=b']\<^sub>b\<^sub>b, c[bv::=b']\<^sub>c\<^sub>b) #\<^sub>\<Gamma> \<Gamma>)\<close> using toSet.simps by auto
    qed
    show \<open>(x, b[bv::=b']\<^sub>b\<^sub>b, c[bv::=b']\<^sub>c\<^sub>b) #\<^sub>\<Gamma> \<Gamma> = GNil @ (x, b[bv::=b']\<^sub>b\<^sub>b, c[bv::=b']\<^sub>c\<^sub>b) #\<^sub>\<Gamma> \<Gamma>\<close> using append_g.simps by auto
    show \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v :b[bv::=b']\<^sub>b\<^sub>b  \<close> using infer_e_appPI check_v_wf(2) b_of.simps subst_b_b_def by metis
  qed
  moreover have "((x, b[bv::=b']\<^sub>b\<^sub>b, c[bv::=b']\<^sub>c\<^sub>b) #\<^sub>\<Gamma> \<Gamma>)[x::=v]\<^sub>\<Gamma>\<^sub>v = \<Gamma>" using subst_gv.simps by auto
  ultimately show ?case using infer_e_appPI subst_v_\<tau>_def by simp
next
  case (infer_e_fstI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v z' b1 b2 c z)
  hence "\<Theta>; \<B>; \<Gamma>  \<turnstile>\<^sub>w\<^sub>f CE_fst [v]\<^sup>c\<^sup>e: b1" using wfCE_fstI wfD_emptyI wfPhi_emptyI infer_v_v_wf 
      b_of.simps  using wfCE_valI by fastforce
  then show ?case  using wfT_e_eq infer_e_fstI by auto
next
  case (infer_e_sndI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v z' b1 b2 c z)
  hence "\<Theta>; \<B>; \<Gamma>  \<turnstile>\<^sub>w\<^sub>f CE_snd  [v]\<^sup>c\<^sup>e: b2" using wfCE_sndI wfD_emptyI wfPhi_emptyI infer_v_v_wf wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_sndI by auto
next
  case (infer_e_lenI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v z' c z)
  hence "\<Theta>; \<B>; \<Gamma>  \<turnstile>\<^sub>w\<^sub>f CE_len [v]\<^sup>c\<^sup>e: B_int" using wfCE_lenI wfD_emptyI wfPhi_emptyI infer_v_v_wf wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_lenI by auto
next
  case (infer_e_mvarI \<Theta> \<Gamma> \<Phi> \<Delta> u \<tau>)
  then show ?case using wfD_wfT by blast
next
  case (infer_e_concatI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v1 z1 c1 v2 z2 c2 z3)
  hence "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f CE_concat [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e: B_bitvec" using wfCE_concatI wfD_emptyI wfPhi_emptyI infer_v_v_wf  wfCE_valI
    by (metis b_of.simps infer_v_wf)
  then show ?case  using wfT_e_eq infer_e_concatI by auto
next
  case (infer_e_splitI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v1 z1 c1 v2 z2 z3)

  hence wfg: " \<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f (z3, [ B_bitvec , B_bitvec ]\<^sup>b, TRUE) #\<^sub>\<Gamma> \<Gamma>" 
    using infer_v_wf wfG_cons2I wfB_pairI wfB_bitvecI by simp
  have wfz: "\<Theta>; \<B>; (z3, [ B_bitvec , B_bitvec ]\<^sup>b, TRUE) #\<^sub>\<Gamma> \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ [ z3 ]\<^sup>v ]\<^sup>c\<^sup>e : [ B_bitvec , B_bitvec ]\<^sup>b "
    apply(rule wfCE_valI , rule wfV_varI)
    using wfg  apply simp
    using lookup.simps(2)[of z3 "[ B_bitvec , B_bitvec ]\<^sup>b" TRUE \<Gamma> z3] by simp
  have 1: "\<Theta>; \<B>; (z3, [ B_bitvec , B_bitvec ]\<^sup>b, TRUE) #\<^sub>\<Gamma> \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v2 ]\<^sup>c\<^sup>e : B_int " 
    using check_v_wf[OF infer_e_splitI(4)]  wf_weakening(1)[OF _ wfg] b_of.simps   toSet.simps wfCE_valI by fastforce
  have 2: "\<Theta>; \<B>; (z3, [ B_bitvec , B_bitvec ]\<^sup>b, TRUE) #\<^sub>\<Gamma> \<Gamma> \<turnstile>\<^sub>w\<^sub>f [ v1 ]\<^sup>c\<^sup>e : B_bitvec" 
    using infer_v_wf[OF infer_e_splitI(3)]  wf_weakening(1)[OF _ wfg] b_of.simps   toSet.simps wfCE_valI by fastforce

  have "\<Theta>; \<B>; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<lbrace> z3 : [ B_bitvec , B_bitvec ]\<^sup>b  | [ v1 ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z3 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z3 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z3 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ v2 ]\<^sup>c\<^sup>e   \<rbrace>"
  proof
    show "atom z3 \<sharp> (\<Theta>, \<B>, \<Gamma>)" using infer_e_splitI wfTh_x_fresh wfX_wfY fresh_prod3 wfG_fresh_x by metis
    show "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f [ B_bitvec , B_bitvec ]\<^sup>b " using wfB_pairI wfB_bitvecI infer_e_splitI wfX_wfY by metis
    show "\<Theta>; \<B>; (z3, [ B_bitvec , B_bitvec ]\<^sup>b, TRUE) #\<^sub>\<Gamma>
              \<Gamma>   \<turnstile>\<^sub>w\<^sub>f [ v1 ]\<^sup>c\<^sup>e  ==  [ [#1[ [ z3 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z3 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e   AND  [| [#1[ [ z3 ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e  ==  [ v2 ]\<^sup>c\<^sup>e" 
      using wfg wfz 1 2 wf_intros by meson
  qed
  thus ?case using infer_e_splitI by auto
qed

lemma infer_e_wf:
  fixes e::e and \<Gamma>::\<Gamma> and \<tau>::\<tau> and \<Delta>::\<Delta> and \<Phi>::\<Phi>
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> e \<Rightarrow> \<tau>"
  shows "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<tau>" and "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>" and "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta>" and "\<Theta> \<turnstile>\<^sub>w\<^sub>f \<Phi>" and "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f e : (b_of \<tau>)"
  using infer_e_t_wf infer_e_e_wf wfE_wf  assms by metis+

lemma infer_e_fresh:
  fixes x::x
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> e \<Rightarrow> \<tau>" and "atom x \<sharp> \<Gamma>"
  shows "atom x \<sharp> (e,\<tau>)"
proof - 
  have "atom x \<sharp> e" using infer_e_e_wf[THEN wfE_x_fresh,OF assms(1)] assms(2) by auto
  moreover have "atom x \<sharp> \<tau>" using assms infer_e_wf  wfT_x_fresh by metis
  ultimately show ?thesis using fresh_Pair by auto
qed

inductive check_e :: "\<Theta> \<Rightarrow> \<Phi> \<Rightarrow> \<B> \<Rightarrow> \<Gamma> \<Rightarrow> \<Delta> \<Rightarrow> e \<Rightarrow> \<tau> \<Rightarrow> bool"  (\<open> _ ; _ ; _ ; _ ; _  \<turnstile> _ \<Leftarrow> _\<close> [50, 50, 50] 50) where
  check_e_subtypeI: "\<lbrakk> infer_e T P B G D e \<tau>' ; subtype T B G \<tau>' \<tau> \<rbrakk> \<Longrightarrow> check_e T P B G D e \<tau>"
equivariance check_e
nominal_inductive check_e  .

inductive_cases check_e_elims[elim!]:
  "check_e F D B G \<Theta> (AE_val v) \<tau>"
  "check_e F D B G \<Theta> e \<tau>"

lemma infer_e_fst_pair:
  fixes v1::v
  assumes "\<Theta> ; \<Phi> ; {||} ; GNil ; \<Delta>  \<turnstile> [#1[ v1 , v2 ]\<^sup>v]\<^sup>e \<Rightarrow> \<tau>"
  shows "\<exists>\<tau>'. \<Theta> ; \<Phi> ; {||} ; GNil ; \<Delta>  \<turnstile> [v1]\<^sup>e \<Rightarrow> \<tau>' \<and> 
        \<Theta> ; {||} ; GNil \<turnstile> \<tau>' \<lesssim> \<tau>"
proof -
  obtain z' and b1 and b2 and c and z where ** : "\<tau> = (\<lbrace> z : b1  | C_eq (CE_val (V_var z))  (CE_fst [(V_pair v1 v2)]\<^sup>c\<^sup>e)  \<rbrace>) \<and> 
          wfD \<Theta> {||} GNil \<Delta> \<and> wfPhi \<Theta> \<Phi> \<and>
              (\<Theta> ; {||} ; GNil  \<turnstile> V_pair v1 v2 \<Rightarrow> \<lbrace> z' : B_pair b1 b2  | c \<rbrace>) \<and> atom z \<sharp> V_pair v1 v2 "
    using infer_e_elims assms  by metis
  hence *:" \<Theta> ; {||} ; GNil  \<turnstile> V_pair v1 v2 \<Rightarrow> \<lbrace> z' : B_pair b1 b2  | c \<rbrace>" by auto

  obtain  t1a  and t2a  where
    *: "\<Theta> ; {||} ; GNil  \<turnstile> v1 \<Rightarrow> t1a \<and>   \<Theta> ; {||} ; GNil  \<turnstile> v2 \<Rightarrow> t2a \<and>  B_pair b1 b2 = B_pair (b_of t1a) (b_of t2a)"
    using infer_v_elims(5)[OF *] by metis

  hence  suppv: "supp v1 = {}  \<and> supp v2 = {} \<and> supp (V_pair v1 v2) = {}" using ** infer_v_v_wf wfV_supp atom_dom.simps toSet.simps supp_GNil  
    by (meson wfV_supp_nil)

  obtain z1 and b1' where "t1a = \<lbrace> z1 : b1'  | [ [ z1 ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v1 ]\<^sup>c\<^sup>e  \<rbrace> " 
    using infer_v_form[of \<Theta> "{||}" GNil v1 t1a] * by auto
  moreover hence "b1' = b1" using * b_of.simps by simp
  ultimately have  "\<Theta> ; {||} ; GNil  \<turnstile> v1 \<Rightarrow> \<lbrace> z1 : b1  | CE_val (V_var z1)  ==  CE_val v1 \<rbrace>" using * by auto
  moreover have "\<Theta> ; {||} ; GNil  \<turnstile>\<^sub>w\<^sub>f CE_fst [V_pair v1 v2]\<^sup>c\<^sup>e : b1" using wfCE_fstI infer_v_wf(1) ** b_of.simps wfCE_valI by metis
  moreover hence st: "\<Theta> ; {||} ; GNil  \<turnstile> \<lbrace> z1 : b1  | CE_val (V_var z1)  ==  CE_val v1 \<rbrace> \<lesssim> (\<lbrace> z : b1  | CE_val (V_var z)  ==  CE_fst [V_pair v1 v2]\<^sup>c\<^sup>e  \<rbrace>)" 
    using subtype_gnil_fst infer_v_v_wf by auto
  moreover have "wfD \<Theta> {||} GNil \<Delta> \<and>  wfPhi \<Theta> \<Phi>" using **  by auto
  ultimately show ?thesis  using wfX_wfY  ** infer_e_valI by metis
qed

lemma infer_e_snd_pair:
  assumes  "\<Theta> ; \<Phi> ;  {||} ; GNil ; \<Delta>  \<turnstile> AE_snd (V_pair v1 v2) \<Rightarrow> \<tau>"
  shows  "\<exists>\<tau>'. \<Theta> ; \<Phi> ; {||} ; GNil ; \<Delta>  \<turnstile> AE_val v2 \<Rightarrow> \<tau>' \<and> \<Theta> ; {||} ; GNil \<turnstile> \<tau>' \<lesssim> \<tau>"
proof -
  obtain z' and b1 and b2 and c and z where ** : "(\<tau> = (\<lbrace> z : b2  | C_eq (CE_val (V_var z)) (CE_snd [(V_pair v1 v2)]\<^sup>c\<^sup>e)  \<rbrace>)) \<and> 
           (wfD \<Theta> {||} GNil \<Delta>) \<and> (wfPhi \<Theta> \<Phi>) \<and>
              \<Theta> ; {||} ; GNil  \<turnstile> V_pair v1 v2 \<Rightarrow> \<lbrace> z' : B_pair b1 b2  | c \<rbrace> \<and> atom z \<sharp> V_pair v1 v2 "
    using infer_e_elims(9)[OF assms(1)]  by metis
  hence *:" \<Theta> ; {||} ; GNil  \<turnstile> V_pair v1 v2 \<Rightarrow> \<lbrace> z' : B_pair b1 b2  | c \<rbrace>" by auto

  obtain  t1a  and t2a  where
    *: "\<Theta> ; {||} ; GNil  \<turnstile> v1 \<Rightarrow> t1a \<and>   \<Theta> ; {||} ; GNil  \<turnstile> v2 \<Rightarrow> t2a \<and>  B_pair b1 b2 = B_pair (b_of t1a) (b_of t2a)"
    using infer_v_elims(5)[OF *] by metis

  hence  suppv: "supp v1 = {} \<and> supp v2 = {} \<and> supp (V_pair v1 v2) = {}" using infer_v_v_wf wfV.simps v.supp  by (meson "**" wfV_supp_nil)

  obtain z2 and b2' where "t2a = \<lbrace> z2 : b2'  | [ [ z2 ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v2 ]\<^sup>c\<^sup>e  \<rbrace> " 
    using infer_v_form[of \<Theta> "{||}" GNil v2 t2a] * by auto
  moreover hence "b2' = b2" using * b_of.simps by simp

  ultimately have  "\<Theta> ; {||} ; GNil  \<turnstile> v2 \<Rightarrow> \<lbrace> z2 : b2  | CE_val (V_var z2)  ==  CE_val v2 \<rbrace>" using * by auto
  moreover have "\<Theta> ; {||} ; GNil  \<turnstile>\<^sub>w\<^sub>f CE_snd [V_pair v1 v2]\<^sup>c\<^sup>e : b2" using wfCE_sndI infer_v_wf(1) ** b_of.simps wfCE_valI by metis
  moreover hence st: "\<Theta> ; {||} ; GNil  \<turnstile> \<lbrace> z2 : b2  | CE_val (V_var z2)  ==  CE_val v2 \<rbrace> \<lesssim> (\<lbrace> z : b2  | CE_val (V_var z)  ==  CE_snd [V_pair v1 v2]\<^sup>c\<^sup>e  \<rbrace>)" 
    using subtype_gnil_snd infer_v_v_wf by auto
  moreover have "wfD \<Theta> {||} GNil \<Delta> \<and>  wfPhi \<Theta> \<Phi>" using ** by metis
  ultimately show ?thesis  using wfX_wfY  ** infer_e_valI by metis
qed

section \<open>Statements\<close>

lemma check_s_v_unit:
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> (\<lbrace> z : B_unit | TRUE \<rbrace>) \<lesssim> \<tau>"  and "wfD \<Theta> \<B> \<Gamma> \<Delta>" and "wfPhi \<Theta> \<Phi>"
  shows  "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> AS_val (V_lit L_unit ) \<Leftarrow> \<tau>" 
proof - 
  have "wfG \<Theta> \<B> \<Gamma>" using assms subtype_g_wf by meson
  moreover hence "wfTh \<Theta>" using wfG_wf by simp
  moreover obtain z'::x where "atom z' \<sharp> \<Gamma>" using obtain_fresh by auto
  ultimately have *:"\<Theta>; \<B>; \<Gamma> \<turnstile> V_lit L_unit \<Rightarrow> \<lbrace> z' : B_unit | CE_val (V_var z')  ==  CE_val (V_lit L_unit)  \<rbrace>" 
    using infer_v_litI infer_unitI by simp
  moreover have "wfT \<Theta> \<B> \<Gamma> (\<lbrace> z' : B_unit | CE_val (V_var z')  ==  CE_val (V_lit L_unit)  \<rbrace>)" using infer_v_t_wf
    by (meson calculation)
  moreover then have  "\<Theta>; \<B>; \<Gamma> \<turnstile> (\<lbrace> z' : B_unit | CE_val (V_var z')  ==  CE_val (V_lit L_unit)  \<rbrace>)  \<lesssim> \<tau>" using subtype_trans subtype_top assms 
      type_for_lit.simps(4) wfX_wfY by metis
  ultimately show  ?thesis using  check_valI assms * by auto
qed

lemma check_s_check_branch_s_wf:
  fixes s::s and cs::branch_s and \<Theta>::\<Theta> and \<Phi>::\<Phi> and \<Gamma>::\<Gamma> and \<Delta>::\<Delta> and v::v and \<tau>::\<tau> and css::branch_list
  shows "\<Theta> ; \<Phi> ; B ; \<Gamma> ; \<Delta> \<turnstile> s \<Leftarrow> \<tau>        \<Longrightarrow> \<Theta> ; B \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<and>  wfTh \<Theta> \<and> wfD \<Theta> B \<Gamma> \<Delta> \<and> wfT \<Theta> B \<Gamma> \<tau> \<and> wfPhi \<Theta> \<Phi> " and 
    "check_branch_s \<Theta> \<Phi> B \<Gamma> \<Delta>  tid cons const v cs  \<tau> \<Longrightarrow> \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<and>  wfTh \<Theta> \<and> wfD \<Theta> B \<Gamma> \<Delta> \<and> wfT \<Theta> B \<Gamma> \<tau> \<and> wfPhi \<Theta> \<Phi> "
    "check_branch_list \<Theta> \<Phi> B \<Gamma> \<Delta>  tid dclist v css  \<tau> \<Longrightarrow> \<Theta> ; B  \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<and>  wfTh \<Theta> \<and> wfD \<Theta> B \<Gamma> \<Delta> \<and> wfT \<Theta> B \<Gamma> \<tau> \<and> wfPhi \<Theta> \<Phi> " 
proof(induct rule: check_s_check_branch_s_check_branch_list.inducts)
  case (check_valI \<Theta> B \<Gamma> \<Delta> \<Phi> v \<tau>' \<tau>)
  then show ?case using infer_v_wf  infer_v_wf subtype_wf wfX_wfY wfS_valI 
    by (metis subtype_eq_base2)
next
  case (check_letI x \<Theta> \<Phi> \<B> \<Gamma> \<Delta> e \<tau> z s b c)
  then have *:"wfT \<Theta> \<B> ((x, b , c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>) \<tau>" by force
  moreover have "atom x \<sharp> \<tau>" using check_letI fresh_prodN by force
  ultimately have "\<Theta>; \<B>;\<Gamma> \<turnstile>\<^sub>w\<^sub>f \<tau>" using wfT_restrict2 by force
  then show ?case  using check_letI  infer_e_wf wfS_letI wfX_wfY wfG_elims by metis
next
  case (check_assertI x \<Theta> \<Phi> \<B> \<Gamma> \<Delta> c \<tau> s)
  then have *:"wfT \<Theta> \<B> ((x, B_bool , c) #\<^sub>\<Gamma> \<Gamma>) \<tau>" by force
  moreover have "atom x \<sharp> \<tau>" using check_assertI fresh_prodN by force
  ultimately have "\<Theta>; \<B>;\<Gamma> \<turnstile>\<^sub>w\<^sub>f \<tau>" using wfT_restrict2 by force
  then show ?case  using check_assertI   wfS_assertI wfX_wfY wfG_elims by metis
next
  case (check_branch_s_branchI \<Theta> \<B> \<Gamma> \<Delta> \<tau> cons const x v \<Phi> s tid)
  then show ?case using wfX_wfY by metis
next
  case (check_branch_list_consI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid dclist' v cs \<tau> css )
  then show ?case using wfX_wfY by metis
next
  case (check_branch_list_finalI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid dclist' v cs \<tau> )
  then show ?case using wfX_wfY by metis
next
  case (check_ifI z \<Theta> \<Phi> \<B> \<Gamma> \<Delta> v s1 s2 \<tau>)
  hence *:"wfT \<Theta>  \<B> \<Gamma> (\<lbrace> z : b_of \<tau>  | CE_val v  ==  CE_val (V_lit L_false) IMP  c_of \<tau> z  \<rbrace>)" (is "wfT \<Theta>  \<B> \<Gamma> ?tau") by auto
  hence "wfT \<Theta> \<B> \<Gamma> \<tau>" using wfT_wfT_if1 check_ifI  fresh_prodN by metis
  hence " \<Theta>; \<B>; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau> " using check_ifI b_of_c_of_eq fresh_prodN by auto
  thus ?case using check_ifI by metis
next
  case (check_let2I x \<Theta> \<Phi> \<B> G \<Delta> t s1 \<tau> s2)
  then have "wfT \<Theta> \<B> ((x, b_of t, (c_of t x)) #\<^sub>\<Gamma> G) \<tau>" by fastforce
  moreover have "atom x \<sharp> \<tau>" using check_let2I by force
  ultimately have "wfT \<Theta> \<B>  G \<tau>" using wfT_restrict2 by metis
  then show ?case using check_let2I by argo
next
  case (check_varI u \<Delta> P G v \<tau>' \<Phi> s \<tau>)
  then show ?case using wfG_elims wfD_elims 
      list.distinct list.inject by metis
next
  case (check_assignI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> u \<tau> v z \<tau>')
  obtain z'::x where *:"atom z' \<sharp> \<Gamma>" using obtain_fresh by metis
  moreover have "\<lbrace> z : B_unit | TRUE \<rbrace> = \<lbrace> z' : B_unit | TRUE \<rbrace>" by auto
  moreover hence "wfT \<Theta> \<B> \<Gamma> \<lbrace> z' : B_unit |TRUE \<rbrace>" using wfT_TRUE check_assignI check_v_wf * wfB_unitI wfG_wf by metis
  ultimately show ?case  using check_v.cases infer_v_wf  subtype_wf check_assignI wfT_wf check_v_wf wfG_wf
    by (meson subtype_wf)
next
  case (check_whileI \<Phi> \<Delta> G P s1 z s2 \<tau>')
  then show ?case using subtype_wf subtype_wf by auto
next
  case (check_seqI \<Delta> G P s1 z s2 \<tau>)
  then show ?case by fast
next
  case (check_caseI \<Theta> \<Phi> \<B> \<Gamma> \<Delta>  dclist cs \<tau> tid v z)
  then show ?case by fast
qed

lemma check_s_check_branch_s_wfS:
  fixes s::s and cs::branch_s and \<Theta>::\<Theta> and \<Phi>::\<Phi> and \<Gamma>::\<Gamma> and \<Delta>::\<Delta> and v::v and \<tau>::\<tau> and css::branch_list
  shows "\<Theta> ; \<Phi> ; B ; \<Gamma> ; \<Delta> \<turnstile> s \<Leftarrow> \<tau>        \<Longrightarrow>   \<Theta> ; \<Phi> ; B ; \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f s : b_of \<tau>  " and 
    "check_branch_s \<Theta> \<Phi> B \<Gamma> \<Delta>  tid cons const v cs  \<tau> \<Longrightarrow>  wfCS \<Theta> \<Phi> B \<Gamma> \<Delta> tid cons const cs (b_of \<tau>)"
    "check_branch_list \<Theta> \<Phi> B \<Gamma> \<Delta>  tid dclist v css  \<tau> \<Longrightarrow>  wfCSS \<Theta> \<Phi> B \<Gamma> \<Delta> tid dclist css (b_of \<tau>)" 
proof(induct rule: check_s_check_branch_s_check_branch_list.inducts)
  case (check_valI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v \<tau>' \<tau>)
  then show ?case using infer_v_wf  infer_v_wf subtype_wf wfX_wfY wfS_valI 
    by (metis subtype_eq_base2)
next
  case (check_letI x \<Theta> \<Phi> \<B> \<Gamma> \<Delta> e \<tau> z s b c)
  show ?case proof
    show \<open> \<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f e : b \<close> using infer_e_wf check_letI b_of.simps by metis
    show \<open> \<Theta> ; \<Phi> ; \<B> ; (x, b, TRUE) #\<^sub>\<Gamma> \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f s : b_of \<tau> \<close>  
      using check_letI b_of.simps wf_replace_true2(2)[OF check_letI(5)]   append_g.simps by metis
    show \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close>  using infer_e_wf check_letI b_of.simps by metis
    show \<open>atom x \<sharp> (\<Phi>, \<Theta>, \<B>, \<Gamma>, \<Delta>, e, b_of \<tau>)\<close> 
      apply(simp add: fresh_prodN, intro conjI)
      using  check_letI(1) fresh_prod7 by simp+ 
  qed
next
  case (check_assertI x \<Theta> \<Phi> \<B> \<Gamma> \<Delta> c \<tau> s)
  show ?case proof

    show \<open> \<Theta> ; \<Phi> ; \<B> ; (x, B_bool, c) #\<^sub>\<Gamma> \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f s : b_of \<tau> \<close> using check_assertI by auto
  next
    show \<open> \<Theta>; \<B>; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f c \<close> using check_assertI by auto
  next
    show \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using check_assertI by auto
  next
    show \<open>atom x \<sharp> (\<Phi>, \<Theta>, \<B>, \<Gamma>, \<Delta>, c, b_of \<tau>, s)\<close> using check_assertI by auto
  qed
next
  case (check_branch_s_branchI \<Theta> \<B> \<Gamma> \<Delta> \<tau> const x \<Phi> tid cons v s)
  show ?case proof
    show \<open> \<Theta> ; \<Phi> ; \<B> ; (x, b_of const, TRUE) #\<^sub>\<Gamma> \<Gamma> ; \<Delta> \<turnstile>\<^sub>w\<^sub>f s : b_of \<tau> \<close> 
      using wf_replace_true append_g.simps check_branch_s_branchI by metis
    show \<open>atom x \<sharp> (\<Phi>, \<Theta>, \<B>, \<Gamma>, \<Delta>, \<Gamma>, const)\<close> 
      using wf_replace_true append_g.simps check_branch_s_branchI fresh_prodN by metis
    show \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using wf_replace_true append_g.simps check_branch_s_branchI by metis
  qed
next
  case (check_branch_list_consI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid cons const v cs \<tau> dclist css)
  then show ?case using wf_intros by metis
next
  case (check_branch_list_finalI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid cons const v cs \<tau>)
  then show ?case using wf_intros by metis
next
  case (check_ifI z \<Theta> \<Phi> \<B> \<Gamma> \<Delta> v s1 s2 \<tau>)
  show ?case using wfS_ifI check_v_wf check_ifI b_of.simps by metis
next
  case (check_let2I x \<Theta> \<Phi> \<B> G \<Delta> t s1 \<tau> s2)
  show ?case proof
    show \<open> \<Theta> ; \<Phi> ; \<B> ; G ; \<Delta> \<turnstile>\<^sub>w\<^sub>f s1 : b_of t \<close>  using check_let2I  b_of.simps by metis 
    show \<open> \<Theta>; \<B>; G   \<turnstile>\<^sub>w\<^sub>f t \<close>  using  check_let2I check_s_check_branch_s_wf  by metis
    show \<open> \<Theta> ; \<Phi> ; \<B> ; (x, b_of t, TRUE) #\<^sub>\<Gamma> G ; \<Delta> \<turnstile>\<^sub>w\<^sub>f s2 : b_of \<tau> \<close>  
      using check_let2I(5) wf_replace_true2(2) append_g.simps check_let2I by metis 
    show \<open>atom x \<sharp> (\<Phi>, \<Theta>, \<B>, G, \<Delta>, s1, b_of \<tau>, t)\<close>  
      apply(simp add: fresh_prodN, intro conjI)
      using  check_let2I(1) fresh_prod7 by simp+ 
  qed
next
  case (check_varI u \<Theta> \<Phi> \<B> \<Gamma> \<Delta> \<tau>' v \<tau> s)
  show ?case proof
    show \<open> \<Theta>; \<B>; \<Gamma>   \<turnstile>\<^sub>w\<^sub>f \<tau>' \<close> using check_v_wf check_varI by metis
    show \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b_of \<tau>' \<close>  using check_v_wf check_varI by metis
    show \<open>atom u \<sharp> (\<Phi>, \<Theta>, \<B>, \<Gamma>, \<Delta>, \<tau>', v, b_of \<tau>)\<close>  using check_varI fresh_prodN u_fresh_b by metis
    show \<open> \<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; (u, \<tau>') #\<^sub>\<Delta>\<Delta> \<turnstile>\<^sub>w\<^sub>f s : b_of \<tau> \<close>  using check_varI by metis
  qed   
next
  case (check_assignI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> u \<tau> v z \<tau>')
  then show ?case using wf_intros check_v_wf subtype_eq_base2 b_of.simps by metis
next
  case (check_whileI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> s1 z s2 \<tau>')
  thus ?case using wf_intros  b_of.simps  check_v_wf subtype_eq_base2 b_of.simps by metis
next
  case (check_seqI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> s1 z s2 \<tau>)
  thus ?case using wf_intros  b_of.simps  by metis
next
  case (check_caseI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid dclist v cs \<tau> z)
  show  ?case proof
    show \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : B_id tid \<close> using check_caseI check_v_wf b_of.simps  by metis
    show \<open>AF_typedef tid dclist \<in> set \<Theta>\<close>  using check_caseI by metis
    show \<open> \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close>  using check_caseI check_s_check_branch_s_wf by metis
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close>  using check_caseI check_s_check_branch_s_wf  by metis
    show \<open> \<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> ; tid ; dclist \<turnstile>\<^sub>w\<^sub>f cs : b_of \<tau> \<close>  using check_caseI by metis
  qed
qed

lemma check_s_wf:
  fixes s::s
  assumes "\<Theta> ; \<Phi> ; B ; \<Gamma> ; \<Delta> \<turnstile> s \<Leftarrow> \<tau>"
  shows "\<Theta> ; B \<turnstile>\<^sub>w\<^sub>f \<Gamma> \<and> wfT \<Theta> B \<Gamma> \<tau> \<and> wfPhi \<Theta> \<Phi> \<and> wfTh \<Theta> \<and> wfD \<Theta> B \<Gamma> \<Delta> \<and> wfS  \<Theta> \<Phi> B \<Gamma> \<Delta> s (b_of \<tau>)"  
  using check_s_check_branch_s_wf check_s_check_branch_s_wfS assms  by meson

lemma check_s_flip_u1:
  fixes s::s and u::u and u'::u
  assumes  "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> s \<Leftarrow> \<tau>"
  shows "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; ( u \<leftrightarrow> u') \<bullet> \<Delta>  \<turnstile> (u \<leftrightarrow> u') \<bullet> s \<Leftarrow>  \<tau>" 
proof - 
  have  "(u \<leftrightarrow> u') \<bullet> \<Theta> ; (u \<leftrightarrow> u') \<bullet> \<Phi> ;  (u \<leftrightarrow> u') \<bullet>  \<B> ; (u \<leftrightarrow> u') \<bullet>  \<Gamma> ;  (u \<leftrightarrow> u') \<bullet> \<Delta>    \<turnstile> (u \<leftrightarrow> u') \<bullet> s \<Leftarrow> (u \<leftrightarrow> u') \<bullet> \<tau>" 
    using check_s.eqvt assms  by blast
  thus  ?thesis using check_s_wf[OF assms] flip_u_eq phi_flip_eq  by metis
qed

lemma check_s_flip_u2: 
  fixes s::s and u::u and u'::u
  assumes "\<Theta> ; \<Phi> ;  B ; \<Gamma> ; ( u \<leftrightarrow> u') \<bullet> \<Delta>   \<turnstile> (u \<leftrightarrow> u') \<bullet> s \<Leftarrow>  \<tau>" 
  shows "\<Theta> ; \<Phi> ;  B ; \<Gamma> ; \<Delta>  \<turnstile> s \<Leftarrow> \<tau>"
proof - 
  have "\<Theta> ; \<Phi> ; B ; \<Gamma> ; ( u \<leftrightarrow> u') \<bullet> ( u \<leftrightarrow> u') \<bullet> \<Delta>   \<turnstile> ( u \<leftrightarrow> u') \<bullet> (u \<leftrightarrow> u') \<bullet> s \<Leftarrow>  \<tau>" 
    using check_s_flip_u1 assms by blast
  thus ?thesis using  permute_flip_cancel by force
qed

lemma check_s_flip_u:
  fixes s::s and u::u and u'::u
  shows "\<Theta> ; \<Phi> ; B ; \<Gamma> ; ( u \<leftrightarrow> u') \<bullet> \<Delta>  \<turnstile> (u \<leftrightarrow> u') \<bullet> s \<Leftarrow>  \<tau> = (\<Theta> ; \<Phi> ; B ; \<Gamma> ; \<Delta> \<turnstile> s \<Leftarrow> \<tau>)"
  using check_s_flip_u1  check_s_flip_u2 by metis

lemma check_s_abs_u:
  fixes s::s and s'::s and u::u and u'::u and \<tau>'::\<tau>
  assumes "[[atom u]]lst. s = [[atom u']]lst. s'" and "atom u \<sharp> \<Delta>" and "atom u' \<sharp> \<Delta>"
    and "\<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<tau>'" 
    and "\<Theta> ; \<Phi> ; B ; \<Gamma> ; ( u , \<tau>') #\<^sub>\<Delta>\<Delta>  \<turnstile> s \<Leftarrow>  \<tau>"
  shows "\<Theta> ; \<Phi> ; B ; \<Gamma> ; ( u', \<tau>' ) #\<^sub>\<Delta>\<Delta> \<turnstile> s' \<Leftarrow> \<tau>"
proof -
  have "\<Theta> ; \<Phi> ; B ; \<Gamma> ; ( u' \<leftrightarrow> u) \<bullet> (( u , \<tau>') #\<^sub>\<Delta>\<Delta>)  \<turnstile> ( u' \<leftrightarrow> u) \<bullet> s \<Leftarrow>  \<tau>"
    using assms check_s_flip_u by metis
  moreover have " ( u' \<leftrightarrow> u) \<bullet> (( u , \<tau>') #\<^sub>\<Delta> \<Delta>) = ( u' , \<tau>') #\<^sub>\<Delta>\<Delta>" proof -
    have " ( u' \<leftrightarrow> u) \<bullet> (( u , \<tau>') #\<^sub>\<Delta> \<Delta>) = ((u' \<leftrightarrow> u) \<bullet> u, (u' \<leftrightarrow> u) \<bullet> \<tau>') #\<^sub>\<Delta> (u' \<leftrightarrow> u) \<bullet> \<Delta>"  
      using  DCons_eqvt  Pair_eqvt by auto
    also have "... = ( u' , (u' \<leftrightarrow> u) \<bullet> \<tau>') #\<^sub>\<Delta> \<Delta>" 
      using assms flip_fresh_fresh by auto
    also have "... = ( u' , \<tau>') #\<^sub>\<Delta> \<Delta>" using
        u_not_in_t fresh_def flip_fresh_fresh assms by metis
    finally show ?thesis by auto
  qed
  moreover have "( u' \<leftrightarrow> u) \<bullet> s = s'" using assms Abs1_eq_iff(3)[of u' s' u s] by auto
  ultimately show ?thesis by auto
qed

section \<open>Additional Elimination and Intros\<close>

subsection  \<open>Values\<close> 

nominal_function b_for :: "opp \<Rightarrow> b" where
  "b_for Plus = B_int"
| "b_for LEq = B_bool" | "b_for Eq = B_bool"
  apply(auto,simp add: eqvt_def b_for_graph_aux_def )
  by (meson opp.exhaust)
nominal_termination (eqvt)  by lexicographic_order


lemma infer_v_pair2I:
  fixes  v\<^sub>1::v and  v\<^sub>2::v
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v\<^sub>1 \<Rightarrow> \<tau>\<^sub>1" and "\<Theta>; \<B>; \<Gamma> \<turnstile> v\<^sub>2 \<Rightarrow> \<tau>\<^sub>2"
  shows "\<exists>\<tau>. \<Theta>; \<B>; \<Gamma> \<turnstile> V_pair v\<^sub>1 v\<^sub>2 \<Rightarrow> \<tau> \<and> b_of \<tau> = B_pair (b_of \<tau>\<^sub>1) (b_of \<tau>\<^sub>2)"
proof - 
  obtain z1 and b1 and c1 and z2 and b2 and c2 where zbc: "\<tau>\<^sub>1 = (\<lbrace> z1 : b1 | c1 \<rbrace>) \<and> \<tau>\<^sub>2 = (\<lbrace> z2 : b2 | c2 \<rbrace>)"
    using \<tau>.exhaust by meson
  obtain z::x where "atom z \<sharp> ( v\<^sub>1, v\<^sub>2,\<Theta>, \<B>,\<Gamma>)" using obtain_fresh
    by blast
  hence "atom z \<sharp> ( v\<^sub>1, v\<^sub>2) \<and> atom z \<sharp> (\<Theta>, \<B>,\<Gamma>)" using fresh_prodN by metis
  hence " \<Theta>; \<B>; \<Gamma> \<turnstile> V_pair v\<^sub>1 v\<^sub>2 \<Rightarrow> \<lbrace> z : [ b_of \<tau>\<^sub>1 , b_of \<tau>\<^sub>2 ]\<^sup>b  | CE_val (V_var z)  ==  CE_val (V_pair v\<^sub>1 v\<^sub>2)  \<rbrace>"  
    using assms infer_v_pairI zbc by metis
  moreover obtain \<tau> where "\<tau> = (\<lbrace> z : B_pair b1 b2  | CE_val (V_var z)  ==  CE_val (V_pair v\<^sub>1 v\<^sub>2)  \<rbrace>)" by blast
  moreover hence "b_of \<tau> = B_pair (b_of \<tau>\<^sub>1) (b_of \<tau>\<^sub>2)" using b_of.simps zbc by presburger
  ultimately show ?thesis using b_of.simps by metis
qed

lemma infer_v_pair2I_zbc:
  fixes  v\<^sub>1::v and  v\<^sub>2::v
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v\<^sub>1 \<Rightarrow> \<tau>\<^sub>1" and "\<Theta>; \<B>; \<Gamma> \<turnstile> v\<^sub>2 \<Rightarrow> \<tau>\<^sub>2"
  shows "\<exists>z \<tau>. \<Theta>; \<B>; \<Gamma> \<turnstile> V_pair v\<^sub>1 v\<^sub>2 \<Rightarrow> \<tau> \<and> \<tau> = (\<lbrace> z : B_pair (b_of \<tau>\<^sub>1) (b_of \<tau>\<^sub>2) | C_eq (CE_val (V_var z)) (CE_val (V_pair v\<^sub>1 v\<^sub>2)) \<rbrace>) \<and> atom z \<sharp> (v\<^sub>1,v\<^sub>2) \<and> atom z \<sharp> \<Gamma>"
proof - 
  obtain z1 and b1 and c1 and z2 and b2 and c2 where zbc: "\<tau>\<^sub>1 = (\<lbrace> z1 : b1 | c1 \<rbrace>) \<and> \<tau>\<^sub>2 = (\<lbrace> z2 : b2 | c2 \<rbrace>)"
    using \<tau>.exhaust by meson
  obtain z::x where * : "atom z \<sharp> ( v\<^sub>1, v\<^sub>2,\<Gamma>,\<Theta> , \<B> )"  using obtain_fresh
    by blast
  hence vinf: " \<Theta>; \<B>; \<Gamma> \<turnstile> V_pair v\<^sub>1 v\<^sub>2 \<Rightarrow> \<lbrace> z :[ b_of \<tau>\<^sub>1 , b_of \<tau>\<^sub>2 ]\<^sup>b  | CE_val (V_var z)  ==  CE_val (V_pair v\<^sub>1 v\<^sub>2)  \<rbrace>"  
    using assms infer_v_pairI by simp
  moreover obtain \<tau> where "\<tau> = (\<lbrace> z : B_pair b1 b2  | CE_val (V_var z)  ==  CE_val (V_pair v\<^sub>1 v\<^sub>2)  \<rbrace>)" by blast
  moreover have "b_of \<tau>\<^sub>1 = b1 \<and> b_of \<tau>\<^sub>2 = b2" using zbc b_of.simps by auto
  ultimately have "\<Theta>; \<B>; \<Gamma> \<turnstile> V_pair v\<^sub>1 v\<^sub>2 \<Rightarrow> \<tau> \<and> \<tau> = (\<lbrace> z : B_pair (b_of \<tau>\<^sub>1) (b_of \<tau>\<^sub>2) | CE_val (V_var z)  ==  CE_val (V_pair v\<^sub>1 v\<^sub>2)  \<rbrace>)" by auto
  thus ?thesis using * fresh_prod2 fresh_prod3 by metis
qed

lemma infer_v_pair2E:
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> V_pair v\<^sub>1 v\<^sub>2 \<Rightarrow> \<tau>"
  shows "\<exists>\<tau>\<^sub>1 \<tau>\<^sub>2 z . \<Theta>; \<B>; \<Gamma> \<turnstile> v\<^sub>1 \<Rightarrow> \<tau>\<^sub>1 \<and> \<Theta>; \<B>; \<Gamma> \<turnstile> v\<^sub>2 \<Rightarrow> \<tau>\<^sub>2 \<and> 
           \<tau> = (\<lbrace> z : B_pair (b_of \<tau>\<^sub>1) (b_of \<tau>\<^sub>2) | C_eq (CE_val (V_var z)) (CE_val (V_pair v\<^sub>1 v\<^sub>2)) \<rbrace>) \<and> atom z \<sharp>  (v\<^sub>1, v\<^sub>2)" 
proof - 
  obtain z and t1 and t2 where 
    "\<tau> = (\<lbrace> z : B_pair (b_of t1) (b_of t2)  | CE_val (V_var z)  ==  CE_val (V_pair v\<^sub>1 v\<^sub>2)  \<rbrace>) \<and>
        atom z \<sharp> (v\<^sub>1, v\<^sub>2) \<and>  \<Theta>; \<B>; \<Gamma> \<turnstile> v\<^sub>1 \<Rightarrow> t1 \<and>  \<Theta>; \<B>; \<Gamma> \<turnstile> v\<^sub>2 \<Rightarrow> t2 " using infer_v_elims(3)[OF assms ] by metis 
  thus ?thesis using b_of.simps  by metis
qed

subsection  \<open>Expressions\<close>

lemma infer_e_app2E:
  fixes \<Phi>::\<Phi> and \<Theta>::\<Theta>
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> AE_app f v \<Rightarrow> \<tau>"
  shows "\<exists>x b c s' \<tau>'.  wfD  \<Theta> \<B> \<Gamma> \<Delta> \<and> Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c \<tau>' s'))) = lookup_fun \<Phi> f \<and>  \<Theta> \<turnstile>\<^sub>w\<^sub>f \<Phi> \<and>
       \<Theta>; \<B>; \<Gamma> \<turnstile> v \<Leftarrow> \<lbrace> x : b  | c \<rbrace> \<and> \<tau> = \<tau>'[x::=v]\<^sub>\<tau>\<^sub>v \<and> atom x \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>, \<Delta>, v, \<tau>)"
  using infer_e_elims(6)[OF assms] b_of.simps subst_defs by metis

lemma infer_e_appP2E:
  fixes \<Phi>::\<Phi> and \<Theta>::\<Theta>
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> AE_appP f b v \<Rightarrow> \<tau>"
  shows "\<exists>bv x ba c s' \<tau>'.  wfD  \<Theta> \<B> \<Gamma> \<Delta> \<and> Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x ba c \<tau>' s'))) = lookup_fun \<Phi> f \<and>  \<Theta> \<turnstile>\<^sub>w\<^sub>f \<Phi> \<and>  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f b   \<and>
      (\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Leftarrow> \<lbrace> x : ba[bv::=b]\<^sub>b\<^sub>b  | c[bv::=b]\<^sub>c\<^sub>b \<rbrace>) \<and> (\<tau> = \<tau>'[bv::=b]\<^sub>\<tau>\<^sub>b[x::=v]\<^sub>\<tau>\<^sub>v) \<and> atom x \<sharp> \<Gamma> \<and> atom bv \<sharp> v"
proof -
  obtain bv x ba c s' \<tau>' where *:"wfD  \<Theta> \<B> \<Gamma> \<Delta> \<and> Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x ba c \<tau>' s'))) = lookup_fun \<Phi> f \<and>  \<Theta> \<turnstile>\<^sub>w\<^sub>f \<Phi> \<and>  \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f b   \<and>
      (\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Leftarrow> \<lbrace> x : ba[bv::=b]\<^sub>b\<^sub>b  | c[bv::=b]\<^sub>c\<^sub>b \<rbrace>) \<and> (\<tau> = \<tau>'[bv::=b]\<^sub>\<tau>\<^sub>b[x::=v]\<^sub>\<tau>\<^sub>v) \<and> atom x \<sharp> \<Gamma> \<and> atom bv \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>, \<Delta>, b, v, \<tau>)" 
    using infer_e_elims(21)[OF assms] subst_defs by metis
  moreover then have "atom bv \<sharp> v" using fresh_prodN by metis
  ultimately show ?thesis by metis
qed

section \<open>Weakening\<close>

text \<open> Lemmas showing that typing judgements hold when a context is extended \<close>

lemma subtype_weakening:
  fixes \<Gamma>'::\<Gamma>
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> \<tau>1 \<lesssim> \<tau>2" and  "toSet \<Gamma> \<subseteq> toSet \<Gamma>'" and "\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f \<Gamma>'" 
  shows  "\<Theta>; \<B>; \<Gamma>' \<turnstile> \<tau>1 \<lesssim> \<tau>2"
  using assms proof(nominal_induct \<tau>2 avoiding: \<Gamma>' rule: subtype.strong_induct)

  case (subtype_baseI x \<Theta> \<B> \<Gamma> z c z' c' b)
  show ?case proof
    show *:"\<Theta>; \<B>; \<Gamma>'   \<turnstile>\<^sub>w\<^sub>f \<lbrace> z : b  | c \<rbrace>" using wfT_weakening subtype_baseI by metis
    show "\<Theta>; \<B>; \<Gamma>'   \<turnstile>\<^sub>w\<^sub>f \<lbrace> z' : b  | c' \<rbrace>" using wfT_weakening subtype_baseI by metis
    show "atom x \<sharp> (\<Theta>, \<B>, \<Gamma>',  z ,  c ,  z' ,  c' )" using subtype_baseI fresh_Pair by metis
    have "toSet ((x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>) \<subseteq>  toSet ((x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>')" using subtype_baseI toSet.simps by blast
    moreover have "\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f (x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>'" using wfT_wf_cons3[OF *, of x] subtype_baseI fresh_Pair subst_defs by metis
    ultimately show "\<Theta>; \<B>; (x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>'  \<Turnstile> c'[z'::=V_var x]\<^sub>v" using valid_weakening subtype_baseI by metis
  qed
qed

method many_rules uses add = ( (rule+),((simp add: add)+)?)

lemma infer_v_g_weakening:
  fixes e::e and \<Gamma>'::\<Gamma> and v::v
  assumes "\<Theta>;  \<B> ; \<Gamma> \<turnstile> v \<Rightarrow> \<tau>" and "toSet \<Gamma> \<subseteq> toSet \<Gamma>'" and "\<Theta>  ; \<B> \<turnstile>\<^sub>w\<^sub>f \<Gamma>'"
  shows   "\<Theta>;  \<B> ; \<Gamma>' \<turnstile> v \<Rightarrow> \<tau>"
  using assms proof(nominal_induct   avoiding: \<Gamma>'  rule: infer_v.strong_induct)
  case (infer_v_varI \<Theta> \<B> \<Gamma> b c x' z)  
  show ?case proof
    show \<open> \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<close> using infer_v_varI by auto
    show \<open>Some (b, c) = lookup \<Gamma>' x'\<close> using infer_v_varI lookup_weakening by metis
    show \<open>atom z \<sharp> x'\<close> using infer_v_varI by auto
    show \<open>atom z \<sharp> (\<Theta>, \<B>, \<Gamma>')\<close> using infer_v_varI by auto
  qed
next
  case (infer_v_litI \<Theta> \<B> \<Gamma> l \<tau>)
  then show ?case using infer_v.intros by simp
next
  case (infer_v_pairI z v1 v2 \<Theta> \<B> \<Gamma> t1 t2)
  then show ?case using infer_v.intros by simp
next
  case (infer_v_consI s dclist \<Theta> dc tc \<B> \<Gamma> v tv z)
  show ?case proof 
    show \<open>AF_typedef s dclist \<in> set \<Theta>\<close> using infer_v_consI by auto
    show \<open>(dc, tc) \<in> set dclist\<close> using infer_v_consI by auto
    show \<open> \<Theta>; \<B>; \<Gamma>' \<turnstile> v \<Rightarrow> tv\<close> using infer_v_consI by auto
    show \<open>\<Theta>; \<B>; \<Gamma>'  \<turnstile> tv \<lesssim> tc\<close> using infer_v_consI subtype_weakening by auto
    show \<open>atom z \<sharp> v\<close> using infer_v_consI by auto
    show \<open>atom z \<sharp> (\<Theta>, \<B>, \<Gamma>')\<close> using infer_v_consI by auto
  qed
next
  case (infer_v_conspI s bv dclist \<Theta> dc tc \<B> \<Gamma> v tv b z)
  show ?case proof
    show \<open>AF_typedef_poly s bv dclist \<in> set \<Theta>\<close> using infer_v_conspI by auto
    show \<open>(dc, tc) \<in> set dclist\<close> using infer_v_conspI by auto 
    show \<open> \<Theta>; \<B>; \<Gamma>' \<turnstile> v \<Rightarrow> tv\<close> using infer_v_conspI by auto
    show \<open>\<Theta>; \<B>; \<Gamma>'  \<turnstile> tv \<lesssim> tc[bv::=b]\<^sub>\<tau>\<^sub>b\<close> using infer_v_conspI subtype_weakening by auto
    show \<open>atom z \<sharp> (\<Theta>, \<B>, \<Gamma>', v, b)\<close> using infer_v_conspI by auto
    show \<open>atom bv \<sharp> (\<Theta>, \<B>, \<Gamma>', v, b)\<close> using infer_v_conspI by auto
    show \<open> \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f b \<close> using infer_v_conspI by auto
  qed
qed

lemma check_v_g_weakening:
  fixes e::e and \<Gamma>'::\<Gamma>
  assumes "\<Theta>;  \<B> ; \<Gamma> \<turnstile> v \<Leftarrow> \<tau>" and "toSet \<Gamma> \<subseteq> toSet \<Gamma>'" and "\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f \<Gamma>'" 
  shows   "\<Theta>;  \<B> ; \<Gamma>' \<turnstile> v \<Leftarrow> \<tau>"
  using subtype_weakening infer_v_g_weakening check_v_elims  check_v_subtypeI assms by metis

lemma infer_e_g_weakening:
  fixes e::e and \<Gamma>'::\<Gamma>
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> e \<Rightarrow> \<tau>" and "toSet \<Gamma> \<subseteq> toSet \<Gamma>'" and "\<Theta> ;  \<B>  \<turnstile>\<^sub>w\<^sub>f \<Gamma>'"
  shows   "\<Theta> ; \<Phi> ;  \<B> ; \<Gamma>'; \<Delta> \<turnstile> e \<Rightarrow> \<tau>"
  using assms proof(nominal_induct \<tau> avoiding: \<Gamma>'  rule: infer_e.strong_induct)
  case (infer_e_valI \<Theta> \<B> \<Gamma> \<Delta>' \<Phi> v \<tau>)
  then show ?case using infer_v_g_weakening wf_weakening infer_e.intros by metis
next
  case (infer_e_plusI \<Theta>  \<B> \<Gamma> \<Delta> \<Phi> v1 z1 c1 v2 z2 c2 z3)

  obtain z'::x where z': "atom z' \<sharp> v1 \<and> atom z' \<sharp> v2 \<and> atom z' \<sharp> \<Gamma>'" using obtain_fresh fresh_prod3 by metis
  moreover hence  *:"\<lbrace> z3 : B_int  | CE_val (V_var z3)  ==  CE_op Plus [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace> = (\<lbrace> z' : B_int  | CE_val (V_var z')  ==  CE_op Plus [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace>)" 
    using infer_e_plusI type_e_eq ce.fresh fresh_e_opp by auto

  have "\<Theta> ; \<Phi> ;  \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> AE_op Plus v1 v2 \<Rightarrow> \<lbrace> z' : B_int  | CE_val (V_var z')  ==  CE_op Plus  [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace>" proof
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using wf_weakening infer_e_plusI by auto
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using infer_e_plusI by auto
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile> v1 \<Rightarrow> \<lbrace> z1 : B_int  | c1 \<rbrace>\<close> using infer_v_g_weakening infer_e_plusI by auto
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile> v2 \<Rightarrow> \<lbrace> z2 : B_int  | c2 \<rbrace>\<close> using infer_v_g_weakening infer_e_plusI by auto
    show \<open>atom z' \<sharp> AE_op Plus v1 v2\<close> using z'  by auto
    show \<open>atom z' \<sharp> \<Gamma>'\<close> using z' by auto
  qed
  thus ?case using * by metis

next
  case (infer_e_leqI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v1 z1 c1 v2 z2 c2 z3)
  obtain z'::x where z': "atom z' \<sharp> v1 \<and> atom z' \<sharp> v2 \<and> atom z' \<sharp> \<Gamma>'" using obtain_fresh fresh_prod3 by metis

  moreover hence  *:"\<lbrace> z3 : B_bool  | CE_val (V_var z3)  ==  CE_op LEq  [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace> = (\<lbrace> z' : B_bool  | CE_val (V_var z')  ==  CE_op LEq  [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace>)" 
    using infer_e_leqI type_e_eq ce.fresh fresh_e_opp by auto

  have "\<Theta> ; \<Phi> ;  \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> AE_op LEq v1 v2 \<Rightarrow> \<lbrace> z' : B_bool  | CE_val (V_var z')  ==  CE_op LEq  [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace>" proof
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using wf_weakening infer_e_leqI by auto
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using infer_e_leqI by auto
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile> v1 \<Rightarrow> \<lbrace> z1 : B_int  | c1 \<rbrace>\<close> using infer_v_g_weakening infer_e_leqI by auto
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile> v2 \<Rightarrow> \<lbrace> z2 : B_int  | c2 \<rbrace>\<close> using infer_v_g_weakening infer_e_leqI by auto
    show \<open>atom z' \<sharp> AE_op LEq v1 v2\<close> using z'  by auto
    show \<open>atom z' \<sharp> \<Gamma>'\<close> using z' by auto
  qed
  thus ?case using * by metis
next
  case (infer_e_eqI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v1 z1 bb c1 v2 z2 c2 z3)
  obtain z'::x where z': "atom z' \<sharp> v1 \<and> atom z' \<sharp> v2 \<and> atom z' \<sharp> \<Gamma>'" using obtain_fresh fresh_prod3 by metis

  moreover hence  *:"\<lbrace> z3 : B_bool  | CE_val (V_var z3)  ==  CE_op Eq  [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace> = (\<lbrace> z' : B_bool  | CE_val (V_var z')  ==  CE_op Eq  [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace>)" 
    using infer_e_eqI type_e_eq ce.fresh fresh_e_opp by auto

  have "\<Theta> ; \<Phi> ;  \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> AE_op Eq v1 v2 \<Rightarrow> \<lbrace> z' : B_bool  | CE_val (V_var z')  ==  CE_op Eq  [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace>" proof
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using wf_weakening infer_e_eqI by auto
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using infer_e_eqI by auto
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile> v1 \<Rightarrow> \<lbrace> z1 : bb  | c1 \<rbrace>\<close> using infer_v_g_weakening infer_e_eqI by auto
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile> v2 \<Rightarrow> \<lbrace> z2 : bb  | c2 \<rbrace>\<close> using infer_v_g_weakening infer_e_eqI by auto
    show \<open>atom z' \<sharp> AE_op Eq v1 v2\<close> using z'  by auto
    show \<open>atom z' \<sharp> \<Gamma>'\<close> using z' by auto
    show "bb \<in> {B_bool, B_int, B_unit}" using infer_e_eqI by auto
  qed
  thus ?case using * by metis
next
  case (infer_e_appI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> f x b c \<tau>' s' v \<tau>)
  show ?case proof 
    show "\<Theta>; \<B>; \<Gamma>' \<turnstile>\<^sub>w\<^sub>f \<Delta> "  using wf_weakening infer_e_appI by auto
    show "\<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi>"   using wf_weakening infer_e_appI by auto
    show "Some (AF_fundef f (AF_fun_typ_none (AF_fun_typ x b c \<tau>' s'))) = lookup_fun \<Phi> f"  using wf_weakening infer_e_appI by auto
    show "\<Theta>; \<B>; \<Gamma>'  \<turnstile> v \<Leftarrow> \<lbrace> x : b  | c \<rbrace>"  using wf_weakening infer_e_appI check_v_g_weakening by auto
    show "atom x \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>', \<Delta>, v, \<tau>)"  using wf_weakening infer_e_appI by auto
    show "\<tau>'[x::=v]\<^sub>v = \<tau>"  using wf_weakening infer_e_appI by auto
  qed

next
  case (infer_e_appPI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> b' f bv x b c \<tau>' s' v \<tau>)

  hence *:"\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> AE_appP f b' v \<Rightarrow> \<tau>" using Typing.infer_e_appPI by auto

  obtain x'::x where x':"atom x' \<sharp> (s', c, \<tau>', (\<Gamma>',v,\<tau>)) \<and> (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x b c \<tau>' s'))) =  (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x' b ((x' \<leftrightarrow> x) \<bullet> c) ((x' \<leftrightarrow> x) \<bullet> \<tau>') ((x' \<leftrightarrow> x) \<bullet> s'))))" 
    using obtain_fresh_fun_def[of s' c \<tau>' "(\<Gamma>',v,\<tau>)" f x b]
    by (metis fun_def.eq_iff fun_typ_q.eq_iff(2))

  hence **: " \<lbrace> x : b  | c \<rbrace> = \<lbrace> x' : b  | (x' \<leftrightarrow> x) \<bullet> c \<rbrace>" 
    using fresh_PairD(1) fresh_PairD(2) type_eq_flip by blast
  have "atom x' \<sharp> \<Gamma>" using x' infer_e_appPI fresh_weakening fresh_Pair by metis

  show ?case proof(rule Typing.infer_e_appPI[where x=x' and bv=bv and b=b and c="(x' \<leftrightarrow> x) \<bullet> c" and \<tau>'="(x' \<leftrightarrow> x) \<bullet> \<tau>'"and s'="((x' \<leftrightarrow> x) \<bullet> s')"])
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using wf_weakening infer_e_appPI by auto
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using wf_weakening infer_e_appPI by auto
    show "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f b'" using infer_e_appPI by auto
    show "Some (AF_fundef f (AF_fun_typ_some bv (AF_fun_typ x' b ((x' \<leftrightarrow> x) \<bullet> c) ((x' \<leftrightarrow> x) \<bullet> \<tau>') ((x' \<leftrightarrow> x) \<bullet> s')))) = lookup_fun \<Phi> f" using x' infer_e_appPI by argo
    show "\<Theta>; \<B>; \<Gamma>'  \<turnstile> v \<Leftarrow> \<lbrace> x' : b[bv::=b']\<^sub>b  | ((x' \<leftrightarrow> x) \<bullet> c)[bv::=b']\<^sub>b \<rbrace>" using **
        \<tau>.eq_iff check_v_g_weakening infer_e_appPI.hyps infer_e_appPI.prems(1) infer_e_appPI.prems subst_defs
        subst_tb.simps by metis
    show "atom x' \<sharp> \<Gamma>'" using x' fresh_prodN by metis

    have "atom x \<sharp> (v, \<tau>) \<and> atom x' \<sharp> (v, \<tau>)" using x' infer_e_fresh[OF *] e.fresh(2) fresh_Pair infer_e_appPI \<open>atom x' \<sharp> \<Gamma>\<close> e.fresh by metis
    moreover then have "((x' \<leftrightarrow> x) \<bullet> \<tau>')[bv::=b']\<^sub>\<tau>\<^sub>b = (x' \<leftrightarrow> x) \<bullet> (\<tau>'[bv::=b']\<^sub>\<tau>\<^sub>b)" using  subst_b_x_flip 
      by (metis subst_b_\<tau>_def)
    ultimately show "((x' \<leftrightarrow> x) \<bullet> \<tau>')[bv::=b']\<^sub>b[x'::=v]\<^sub>v = \<tau>" 
      using infer_e_appPI subst_tv_flip subst_defs by metis

    show "atom bv \<sharp>  (\<Theta>, \<Phi>, \<B>, \<Gamma>', \<Delta>, b', v, \<tau>)" using infer_e_appPI fresh_prodN by metis
  qed

next
  case (infer_e_fstI \<Theta>  \<B> \<Gamma> \<Delta> \<Phi> v z'' b1 b2 c z)

  obtain z'::x where  *: "atom z' \<sharp> \<Gamma>' \<and> atom z' \<sharp> v \<and> atom z' \<sharp> c" using obtain_fresh_z fresh_Pair by metis 
  hence **:"\<lbrace> z : b1  | CE_val (V_var z)  ==  CE_fst [v]\<^sup>c\<^sup>e  \<rbrace> =  \<lbrace> z' : b1  | CE_val (V_var z')  ==  CE_fst [v]\<^sup>c\<^sup>e  \<rbrace>"
    using  type_e_eq infer_e_fstI v.fresh e.fresh ce.fresh obtain_fresh_z fresh_Pair by metis

  have "\<Theta> ; \<Phi> ;  \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> AE_fst v \<Rightarrow> \<lbrace> z' : b1  | CE_val (V_var z')  ==  CE_fst [v]\<^sup>c\<^sup>e  \<rbrace>" proof
    show \<open> \<Theta> ;  \<B> ; \<Gamma>'  \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using wf_weakening infer_e_fstI by auto
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using wf_weakening infer_e_fstI by auto
    show "\<Theta> ;  \<B> ; \<Gamma>'  \<turnstile> v \<Rightarrow> \<lbrace> z'' : B_pair b1 b2  |  c \<rbrace>" using infer_v_g_weakening infer_e_fstI  by metis
    show "atom z' \<sharp> AE_fst v" using * ** e.supp by auto
    show "atom z' \<sharp> \<Gamma>'" using * by auto
  qed
  thus ?case using * ** by metis
next
  case (infer_e_sndI \<Theta>  \<B> \<Gamma> \<Delta> \<Phi> v z'' b1 b2 c z)

  obtain z'::x where  *: "atom z' \<sharp> \<Gamma>' \<and> atom z' \<sharp> v \<and> atom z' \<sharp> c"  using obtain_fresh_z fresh_Pair by metis 
  hence **:"\<lbrace> z : b2  | CE_val (V_var z)  ==  CE_snd [v]\<^sup>c\<^sup>e  \<rbrace> =  \<lbrace> z' : b2  | CE_val (V_var z')  ==  CE_snd [v]\<^sup>c\<^sup>e  \<rbrace>"
    using  type_e_eq infer_e_sndI e.fresh ce.fresh obtain_fresh_z fresh_Pair by metis

  have "\<Theta> ; \<Phi> ;  \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> AE_snd v \<Rightarrow> \<lbrace> z' : b2  | CE_val (V_var z')  ==  CE_snd [v]\<^sup>c\<^sup>e  \<rbrace>" proof
    show \<open> \<Theta> ;  \<B> ;\<Gamma>'  \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using wf_weakening infer_e_sndI by auto
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using wf_weakening infer_e_sndI by auto
    show "\<Theta> ;  \<B> ; \<Gamma>'  \<turnstile> v \<Rightarrow> \<lbrace> z'' : B_pair b1 b2  |  c \<rbrace>" using infer_v_g_weakening infer_e_sndI    by metis
    show "atom z' \<sharp> AE_snd v" using * e.supp by auto
    show "atom z' \<sharp> \<Gamma>'" using * by auto
  qed
  thus ?case using ** by metis
next
  case (infer_e_lenI \<Theta>  \<B> \<Gamma> \<Delta> \<Phi> v z'' c z)

  obtain z'::x where  *: "atom z' \<sharp> \<Gamma>' \<and> atom z' \<sharp> v \<and> atom z' \<sharp> c"  using obtain_fresh_z fresh_Pair by metis 
  hence **:"\<lbrace> z : B_int  | CE_val (V_var z)  ==  CE_len [v]\<^sup>c\<^sup>e  \<rbrace> =  \<lbrace> z' : B_int  | CE_val (V_var z')  ==  CE_len [v]\<^sup>c\<^sup>e  \<rbrace>"
    using  type_e_eq infer_e_lenI e.fresh ce.fresh obtain_fresh_z fresh_Pair by metis

  have "\<Theta> ; \<Phi> ; \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> AE_len v \<Rightarrow> \<lbrace> z' : B_int  | CE_val (V_var z')  ==  CE_len [v]\<^sup>c\<^sup>e  \<rbrace>" proof
    show \<open> \<Theta>; \<B>; \<Gamma>' \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using wf_weakening infer_e_lenI by auto
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using wf_weakening infer_e_lenI by auto
    show "\<Theta> ;  \<B> ; \<Gamma>' \<turnstile> v \<Rightarrow> \<lbrace> z'' : B_bitvec  | c \<rbrace>" using infer_v_g_weakening infer_e_lenI    by metis
    show "atom z' \<sharp> AE_len v" using * e.supp by auto
    show "atom z' \<sharp> \<Gamma>'" using * by auto
  qed
  thus ?case using * ** by metis
next
  case (infer_e_mvarI \<Theta> \<Gamma> \<Phi> \<Delta> u \<tau>)
  then show ?case using  wf_weakening infer_e.intros by metis
next
  case (infer_e_concatI \<Theta>  \<B> \<Gamma> \<Delta> \<Phi> v1 z1 c1 v2 z2 c2 z3)

  obtain z'::x where  *: "atom z' \<sharp> \<Gamma>' \<and> atom z' \<sharp> v1 \<and> atom z' \<sharp> v2" using obtain_fresh_z fresh_Pair by metis 
  hence **:"\<lbrace> z3 : B_bitvec  | CE_val (V_var z3)  ==  CE_concat [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e \<rbrace> =  \<lbrace> z' : B_bitvec  | CE_val (V_var z')  ==  CE_concat [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e \<rbrace>"
    using  type_e_eq infer_e_concatI e.fresh ce.fresh obtain_fresh_z fresh_Pair by metis

  have "\<Theta> ; \<Phi> ;  \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> AE_concat v1 v2 \<Rightarrow> \<lbrace> z' : B_bitvec  | CE_val (V_var z')  ==  CE_concat [v1]\<^sup>c\<^sup>e [v2]\<^sup>c\<^sup>e  \<rbrace>" proof
    show \<open> \<Theta>; \<B>; \<Gamma>' \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using wf_weakening infer_e_concatI by auto
    show \<open> \<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using wf_weakening infer_e_concatI by auto
    show "\<Theta> ;  \<B> ; \<Gamma>' \<turnstile> v1 \<Rightarrow> \<lbrace> z1 : B_bitvec  |  c1 \<rbrace>" using infer_v_g_weakening infer_e_concatI    by metis
    show "\<Theta> ;  \<B> ; \<Gamma>' \<turnstile> v2 \<Rightarrow> \<lbrace> z2 : B_bitvec  |  c2 \<rbrace>" using infer_v_g_weakening infer_e_concatI    by metis
    show "atom z' \<sharp> AE_concat v1 v2" using * e.supp by auto
    show "atom z' \<sharp> \<Gamma>'" using * by auto
  qed
  thus ?case using * ** by metis
next
  case (infer_e_splitI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v1 z1 c1 v2 z2 z3)
  show ?case proof
    show "\<Theta>; \<B>; \<Gamma>' \<turnstile>\<^sub>w\<^sub>f \<Delta>" using infer_e_splitI wf_weakening by auto
    show "\<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> " using infer_e_splitI wf_weakening by auto
    show "\<Theta>; \<B>; \<Gamma>' \<turnstile> v1 \<Rightarrow> \<lbrace> z1 : B_bitvec  | c1 \<rbrace>" using infer_v_g_weakening infer_e_splitI by metis
    show "\<Theta>; \<B>; \<Gamma>'  \<turnstile> v2 \<Leftarrow> \<lbrace> z2 : B_int  | [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ z2 ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e 
                  AND  [ leq [ [ z2 ]\<^sup>v ]\<^sup>c\<^sup>e [| [ v1 ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e ]\<^sup>c\<^sup>e  ==  [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e   \<rbrace>" 
      using check_v_g_weakening infer_e_splitI by metis
    show "atom z1 \<sharp> AE_split v1 v2" using infer_e_splitI by auto
    show "atom z1 \<sharp> \<Gamma>'" using infer_e_splitI by auto
    show "atom z2 \<sharp> AE_split v1 v2" using infer_e_splitI by auto
    show "atom z2 \<sharp> \<Gamma>'" using infer_e_splitI by auto
    show "atom z3 \<sharp> AE_split v1 v2" using infer_e_splitI by auto
    show "atom z3 \<sharp> \<Gamma>'" using infer_e_splitI by auto
  qed
qed

text \<open> Special cases proved explicitly, other cases at the end with method + \<close>

lemma infer_e_d_weakening:
  fixes e::e
  assumes "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> e \<Rightarrow> \<tau>" and "setD \<Delta> \<subseteq> setD \<Delta>'" and "wfD \<Theta>  \<B> \<Gamma> \<Delta>'" 
  shows   "\<Theta>; \<Phi> ;  \<B> ; \<Gamma> ; \<Delta>' \<turnstile> e \<Rightarrow> \<tau>"
  using assms by(nominal_induct \<tau> avoiding: \<Delta>' rule: infer_e.strong_induct,auto simp add:infer_e.intros)

lemma  wfG_x_fresh_in_v_simple:
  fixes x::x and v :: v
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<tau>" and "atom x \<sharp> \<Gamma>" 
  shows "atom x \<sharp> v"
  using wfV_x_fresh infer_v_wf assms by metis

lemma check_s_g_weakening:
  fixes v::v and s::s and cs::branch_s and x::x and c::c and b::b and \<Gamma>'::\<Gamma> and \<Theta>::\<Theta> and css::branch_list
  shows  "check_s \<Theta> \<Phi> \<B> \<Gamma> \<Delta> s  t \<Longrightarrow> toSet \<Gamma> \<subseteq> toSet \<Gamma>' \<Longrightarrow>  \<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f \<Gamma>' \<Longrightarrow> check_s \<Theta> \<Phi> \<B> \<Gamma>' \<Delta>  s   t"  and 
    "check_branch_s \<Theta> \<Phi> \<B> \<Gamma> \<Delta>  tid cons const v cs t \<Longrightarrow>  toSet \<Gamma> \<subseteq> toSet \<Gamma>' \<Longrightarrow>  \<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f \<Gamma>'  \<Longrightarrow> check_branch_s \<Theta> \<Phi> \<B> \<Gamma>' \<Delta> tid cons const v cs t" and
    "check_branch_list \<Theta> \<Phi> \<B> \<Gamma> \<Delta>  tid dclist v css t \<Longrightarrow>  toSet \<Gamma> \<subseteq> toSet \<Gamma>' \<Longrightarrow>  \<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f \<Gamma>'  \<Longrightarrow> check_branch_list \<Theta> \<Phi> \<B> \<Gamma>' \<Delta> tid dclist v css t"
proof(nominal_induct t and t and t avoiding: \<Gamma>'   rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_valI \<Theta> \<B> \<Gamma> \<Delta>' \<Phi> v \<tau>' \<tau>)
  then show ?case using Typing.check_valI infer_v_g_weakening wf_weakening subtype_weakening  by metis
next
  case (check_letI x \<Theta> \<Phi> \<B> \<Gamma> \<Delta> e \<tau> z s b c)
  hence xf:"atom x \<sharp> \<Gamma>'"  by metis
  show ?case proof
    show "atom x \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>', \<Delta>, e, \<tau>)" using check_letI using fresh_prod4 xf by metis
    show "\<Theta> ; \<Phi> ; \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> e \<Rightarrow> \<lbrace> z : b  | c \<rbrace>" using infer_e_g_weakening check_letI by metis
    show "atom z \<sharp> (x, \<Theta>, \<Phi>, \<B>, \<Gamma>', \<Delta>, e, \<tau>, s)" 
      by(unfold fresh_prodN,auto simp add: check_letI fresh_prodN) 
    have "toSet ((x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>) \<subseteq> toSet ((x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>')" using check_letI toSet.simps 
      by (metis Un_commute Un_empty_right Un_insert_right insert_mono)
    moreover hence "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>')" using check_letI wfG_cons_weakening check_s_wf by metis
    ultimately show "\<Theta> ; \<Phi> ; \<B> ; (x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>' ; \<Delta>  \<turnstile> s \<Leftarrow> \<tau>" using check_letI by metis
  qed
next
  case (check_let2I x \<Theta> \<Phi> \<B> G \<Delta> t s1 \<tau> s2)
  show ?case proof
    show "atom x \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>', \<Delta>, t, s1, \<tau>)" using check_let2I using fresh_prod4 by auto
    show "\<Theta> ; \<Phi> ; \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> s1 \<Leftarrow> t" using check_let2I by metis
    have "toSet ((x, b_of t, c_of t x) #\<^sub>\<Gamma> G) \<subseteq> toSet ((x, b_of t, c_of t x ) #\<^sub>\<Gamma> \<Gamma>')" using check_let2I by auto
    moreover hence "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x, b_of t, c_of t x) #\<^sub>\<Gamma> \<Gamma>')" using check_let2I wfG_cons_weakening check_s_wf by metis
    ultimately show "\<Theta> ; \<Phi> ; \<B> ; (x, b_of t, c_of t x) #\<^sub>\<Gamma> \<Gamma>' ; \<Delta>  \<turnstile> s2 \<Leftarrow> \<tau>" using check_let2I by metis
  qed
next
  case (check_branch_list_consI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid dclist' v cs \<tau> css dclist)
  thus ?case using Typing.check_branch_list_consI by metis
next
  case (check_branch_list_finalI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid dclist' v cs \<tau> dclist)
  thus ?case using Typing.check_branch_list_finalI by metis
next
  case (check_branch_s_branchI \<Theta> \<B> \<Gamma> \<Delta> \<tau> const x \<Phi> tid cons v  s)
  show ?case proof
    show "\<Theta>; \<B>; \<Gamma>' \<turnstile>\<^sub>w\<^sub>f \<Delta> " using  wf_weakening2(6) check_branch_s_branchI by metis
    show "\<turnstile>\<^sub>w\<^sub>f \<Theta>" using check_branch_s_branchI by auto
    show "\<Theta>; \<B>; \<Gamma>'   \<turnstile>\<^sub>w\<^sub>f \<tau> "  using check_branch_s_branchI wfT_weakening \<open>wfG  \<Theta> \<B> \<Gamma>'\<close> by presburger

    show "\<Theta> ; {||} ; GNil \<turnstile>\<^sub>w\<^sub>f const " using check_branch_s_branchI by auto
    show "atom x \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>', \<Delta>, tid, cons, const, v, \<tau>)" using check_branch_s_branchI by auto
    have "toSet ((x, b_of const, CE_val v  ==  CE_val(V_cons tid cons (V_var x))   AND  c_of const x) #\<^sub>\<Gamma> \<Gamma>) \<subseteq> toSet ((x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x)) AND  c_of const x) #\<^sub>\<Gamma> \<Gamma>')" 
      using check_branch_s_branchI by auto
    moreover hence "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f ((x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))   AND  c_of const x ) #\<^sub>\<Gamma> \<Gamma>')" 
      using check_branch_s_branchI wfG_cons_weakening check_s_wf by metis
    ultimately show "\<Theta> ; \<Phi> ; \<B> ; (x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))   AND  c_of const x ) #\<^sub>\<Gamma> \<Gamma>' ; \<Delta>  \<turnstile> s \<Leftarrow> \<tau>" 
      using check_branch_s_branchI  using fresh_dom_free by auto
  qed
next
  case (check_ifI z \<Theta> \<Phi> \<B> \<Gamma> \<Delta> v s1 s2 \<tau>)
  show ?case proof
    show \<open>atom z \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>', \<Delta>, v, s1, s2, \<tau>)\<close> using fresh_prodN check_ifI by auto
    show \<open>\<Theta>; \<B>; \<Gamma>'  \<turnstile> v \<Leftarrow> \<lbrace> z : B_bool  | TRUE \<rbrace>\<close> using check_v_g_weakening check_ifI by auto
    show \<open> \<Theta> ; \<Phi> ; \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> s1 \<Leftarrow> \<lbrace> z : b_of \<tau>  | CE_val v  ==  CE_val (V_lit L_true)   IMP  c_of \<tau> z  \<rbrace>\<close> using  check_ifI by auto
    show \<open> \<Theta> ; \<Phi> ; \<B> ; \<Gamma>' ; \<Delta>  \<turnstile> s2 \<Leftarrow> \<lbrace> z : b_of \<tau>  | CE_val v  ==  CE_val (V_lit L_false)   IMP  c_of \<tau> z  \<rbrace>\<close> using  check_ifI by auto
  qed
next 
  case (check_whileI \<Delta> G P s1 z s2 \<tau>')
  then show ?case using check_s_check_branch_s_check_branch_list.intros check_v_g_weakening subtype_weakening wf_weakening  
    by (meson infer_v_g_weakening)
next
  case (check_seqI \<Delta> G P s1 z s2 \<tau>)
  then show ?case using check_s_check_branch_s_check_branch_list.intros check_v_g_weakening subtype_weakening wf_weakening 
    by (meson infer_v_g_weakening)
next
  case (check_varI u \<Theta> \<Phi> \<B> \<Gamma> \<Delta> \<tau>' v \<tau> s)
  thus ?case  using check_v_g_weakening check_s_check_branch_s_check_branch_list.intros by auto
next
  case (check_assignI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> u \<tau> v z \<tau>')
  show ?case proof 
    show \<open>\<Theta>  \<turnstile>\<^sub>w\<^sub>f \<Phi> \<close> using check_assignI by auto
    show \<open>\<Theta>; \<B>;  \<Gamma>' \<turnstile>\<^sub>w\<^sub>f \<Delta>\<close> using check_assignI  wf_weakening by auto
    show \<open>(u, \<tau>) \<in> setD \<Delta>\<close> using check_assignI by auto
    show \<open>\<Theta>; \<B>; \<Gamma>'  \<turnstile> v \<Leftarrow> \<tau>\<close> using check_assignI  check_v_g_weakening by auto
    show \<open>\<Theta>; \<B>; \<Gamma>'  \<turnstile> \<lbrace> z : B_unit  | TRUE \<rbrace> \<lesssim> \<tau>'\<close> using  subtype_weakening check_assignI by auto
  qed
next
  case (check_caseI \<Delta> \<Gamma> \<Theta> dclist cs \<tau> tid v z)

  then show ?case using check_s_check_branch_s_check_branch_list.intros check_v_g_weakening subtype_weakening wf_weakening
    by (meson infer_v_g_weakening)
next
  case (check_assertI x \<Theta> \<Phi> \<B> \<Gamma> \<Delta> c \<tau> s)
  show ?case proof
    show \<open>atom x \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>', \<Delta>, c, \<tau>, s)\<close> using check_assertI by auto

    have " \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f  (x, B_bool, c) #\<^sub>\<Gamma> \<Gamma>" using check_assertI check_s_wf by metis
    hence *:" \<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f  (x, B_bool, c) #\<^sub>\<Gamma> \<Gamma>'"   using wfG_cons_weakening check_assertI by metis
    moreover have "toSet ((x, B_bool, c) #\<^sub>\<Gamma> \<Gamma>) \<subseteq> toSet ((x, B_bool, c) #\<^sub>\<Gamma> \<Gamma>')" using check_assertI by auto
    thus  \<open> \<Theta> ; \<Phi> ; \<B> ; (x, B_bool, c) #\<^sub>\<Gamma> \<Gamma>' ; \<Delta>  \<turnstile> s \<Leftarrow> \<tau>\<close> using check_assertI(11) [OF _ *] by auto

    show \<open>\<Theta>; \<B>; \<Gamma>'  \<Turnstile> c \<close> using check_assertI valid_weakening by metis
    show \<open> \<Theta>; \<B>; \<Gamma>' \<turnstile>\<^sub>w\<^sub>f \<Delta> \<close> using check_assertI wf_weakening by metis
  qed
qed

lemma  wfG_xa_fresh_in_v:
  fixes c::c and \<Gamma>::\<Gamma> and G::\<Gamma> and v::v and xa::x
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<tau>" and "G=( \<Gamma>'@ (x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>)" and "atom xa \<sharp> G" and "\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f G"
  shows "atom xa \<sharp> v"
proof -
  have "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : b_of \<tau>"  using infer_v_wf assms by metis
  hence "supp v \<subseteq> atom_dom \<Gamma>  \<union> supp \<B>" using wfV_supp by simp
  moreover have  "atom xa \<notin> atom_dom G"  
    using assms wfG_atoms_supp_eq[OF assms(4)] fresh_def by metis
  ultimately show ?thesis using fresh_def
    using assms infer_v_wf wfG_atoms_supp_eq
      fresh_GCons  fresh_append_g subsetCE
    by (metis wfG_x_fresh_in_v_simple)
qed

lemma fresh_z_subst_g:
  fixes G::\<Gamma>
  assumes "atom z' \<sharp> (x,v)" and \<open>atom z' \<sharp> G\<close>
  shows "atom z' \<sharp> G[x::=v]\<^sub>\<Gamma>\<^sub>v"
proof - 
  have "atom z' \<sharp> v" using assms fresh_prod2 by auto
  thus ?thesis  using fresh_subst_gv assms by metis
qed

lemma  wfG_xa_fresh_in_subst_v:
  fixes c::c and v::v and x::x  and \<Gamma>::\<Gamma> and G::\<Gamma> and xa::x
  assumes "\<Theta>; \<B>; \<Gamma> \<turnstile> v \<Rightarrow> \<tau>" and "G=( \<Gamma>'@ (x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>)" and "atom xa \<sharp> G" and "\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f G"
  shows "atom xa \<sharp> (subst_gv G x v)"
proof -
  have "atom xa \<sharp> v" using wfG_xa_fresh_in_v assms by metis
  thus ?thesis using fresh_subst_gv assms by metis
qed

subsection \<open>Weakening Immutable Variable Context\<close>

declare check_s_check_branch_s_check_branch_list.intros[simp]
declare check_s_check_branch_s_check_branch_list.intros[intro]

lemma check_s_d_weakening:
  fixes s::s and v::v and cs::branch_s and css::branch_list
  shows  " \<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta> \<turnstile> s \<Leftarrow> \<tau> \<Longrightarrow>  setD \<Delta> \<subseteq> setD \<Delta>' \<Longrightarrow>  wfD  \<Theta> \<B> \<Gamma> \<Delta>' \<Longrightarrow> \<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta>' \<turnstile> s \<Leftarrow> \<tau>" and 
    "check_branch_s \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid cons const v cs \<tau> \<Longrightarrow>  setD \<Delta> \<subseteq> setD \<Delta>' \<Longrightarrow>  wfD  \<Theta> \<B> \<Gamma> \<Delta>' \<Longrightarrow> check_branch_s \<Theta> \<Phi> \<B> \<Gamma> \<Delta>' tid cons const v cs \<tau>" and 
    "check_branch_list \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid dclist v css \<tau> \<Longrightarrow>  setD \<Delta> \<subseteq> setD \<Delta>' \<Longrightarrow>  wfD  \<Theta> \<B> \<Gamma> \<Delta>' \<Longrightarrow> check_branch_list \<Theta> \<Phi> \<B> \<Gamma> \<Delta>' tid dclist v css \<tau>"
proof(nominal_induct \<tau> and \<tau> and \<tau> avoiding: \<Delta>'   arbitrary: v rule: check_s_check_branch_s_check_branch_list.strong_induct)
  case (check_valI \<Theta> \<B> \<Gamma> \<Delta> \<Phi> v \<tau>' \<tau>)
  then show ?case using check_s_check_branch_s_check_branch_list.intros by blast
next
  case (check_letI x \<Theta> \<Phi> \<B> \<Gamma> \<Delta> e \<tau> z s b c)
  show ?case proof
    show "atom x \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>, \<Delta>', e, \<tau>)"  using check_letI by auto
    show "atom z \<sharp> (x, \<Theta>, \<Phi>, \<B>, \<Gamma>, \<Delta>', e, \<tau>, s)" using check_letI by auto
    show "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta>'  \<turnstile> e \<Rightarrow> \<lbrace> z : b  | c \<rbrace>"  using check_letI infer_e_d_weakening by auto
    have "\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f (x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma>" using check_letI check_s_wf by metis
    moreover have "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta>'" using check_letI check_s_wf by metis
    ultimately have "\<Theta>; \<B>; (x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta>'"  using wf_weakening2(6)  toSet.simps by fast
    thus  "\<Theta> ; \<Phi> ; \<B> ; (x, b, c[z::=V_var x]\<^sub>v) #\<^sub>\<Gamma> \<Gamma> ; \<Delta>'  \<turnstile> s \<Leftarrow> \<tau>"   using check_letI by simp
  qed
next
  case (check_branch_s_branchI \<Theta> \<B> \<Gamma> \<Delta> \<tau> const x \<Phi> tid cons v  s)
  moreover have "\<Theta> ;\<B> \<turnstile>\<^sub>w\<^sub>f (x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))   AND  c_of const x ) #\<^sub>\<Gamma> \<Gamma>" 
    using check_s_wf[OF check_branch_s_branchI(16) ] by metis
  moreover hence " \<Theta> ;\<B> ; (x, b_of const, CE_val v  ==  CE_val (V_cons tid cons (V_var x))   AND  c_of const x ) #\<^sub>\<Gamma> \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta>'" 
    using wf_weakening2(6) check_branch_s_branchI by fastforce
  ultimately show ?case 
    using  check_s_check_branch_s_check_branch_list.intros by simp
next
  case (check_branch_list_consI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid dclist v cs \<tau> css)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_branch_list_finalI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid dclist v cs \<tau>)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_ifI z \<Theta> \<Phi> \<B> \<Gamma> \<Delta> v s1 s2 \<tau>)
  show ?case proof
    show \<open>atom z \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>, \<Delta>', v, s1, s2, \<tau>)\<close> using fresh_prodN check_ifI by auto
    show \<open>\<Theta>; \<B>; \<Gamma>  \<turnstile> v \<Leftarrow> \<lbrace> z : B_bool  | TRUE \<rbrace>\<close> using  check_ifI by auto
    show \<open> \<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta>'  \<turnstile> s1 \<Leftarrow> \<lbrace> z : b_of \<tau>  | CE_val v  ==  CE_val (V_lit L_true)   IMP  c_of \<tau> z  \<rbrace>\<close> using  check_ifI by auto
    show \<open> \<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; \<Delta>'  \<turnstile> s2 \<Leftarrow> \<lbrace> z : b_of \<tau>  | CE_val v  ==  CE_val (V_lit L_false)   IMP  c_of \<tau> z  \<rbrace>\<close> using  check_ifI by auto
  qed
next
  case (check_assertI x \<Theta> \<Phi> \<B> \<Gamma> \<Delta> c \<tau> s)
  show ?case proof
    show "atom x \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>, \<Delta>', c, \<tau>,s)" using fresh_prodN check_assertI by auto
    show *:" \<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta>' " using check_assertI by auto
    hence  "\<Theta>; \<B>; (x, B_bool, c) #\<^sub>\<Gamma> \<Gamma> \<turnstile>\<^sub>w\<^sub>f \<Delta>' " using wf_weakening2(6)[OF *, of " (x, B_bool, c) #\<^sub>\<Gamma> \<Gamma>"] check_assertI check_s_wf toSet.simps by auto
    thus  "\<Theta> ; \<Phi> ; \<B> ; (x, B_bool, c) #\<^sub>\<Gamma> \<Gamma> ; \<Delta>'  \<turnstile> s \<Leftarrow> \<tau>" 
      using check_assertI(11)[OF \<open>setD \<Delta> \<subseteq> setD \<Delta>'\<close>] by simp
        (* wf_weakening2(6) check_s_wf check_assertI *)
    show "\<Theta>; \<B>; \<Gamma>  \<Turnstile> c " using fresh_prodN check_assertI by auto

  qed
next
  case (check_let2I x \<Theta> \<Phi> \<B> G \<Delta> t s1 \<tau> s2)
  show ?case proof
    show "atom x \<sharp> (\<Theta>, \<Phi>, \<B>, G, \<Delta>', t , s1, \<tau>)"  using check_let2I by auto

    show "\<Theta> ; \<Phi> ; \<B> ; G ; \<Delta>'  \<turnstile> s1 \<Leftarrow> t"  using check_let2I infer_e_d_weakening by auto
    have "\<Theta>; \<B>; (x, b_of t, c_of t x ) #\<^sub>\<Gamma> G \<turnstile>\<^sub>w\<^sub>f \<Delta>'"  using check_let2I wf_weakening2(6) check_s_wf by fastforce 
    thus  "\<Theta> ; \<Phi> ; \<B> ; (x, b_of t, c_of t x) #\<^sub>\<Gamma> G ; \<Delta>'  \<turnstile> s2 \<Leftarrow> \<tau>"   using check_let2I by simp
  qed
next
  case (check_varI u \<Theta> \<Phi> \<B> \<Gamma> \<Delta> \<tau>' v \<tau> s)
  show ?case proof
    show "atom u \<sharp> (\<Theta>, \<Phi>, \<B>, \<Gamma>, \<Delta>', \<tau>', v, \<tau>)" using check_varI by auto
    show "\<Theta>; \<B>; \<Gamma>  \<turnstile> v \<Leftarrow> \<tau>'" using check_varI by auto
    have "setD ((u, \<tau>') #\<^sub>\<Delta>\<Delta>) \<subseteq> setD ((u, \<tau>') #\<^sub>\<Delta>\<Delta>')" using setD.simps check_varI by auto
    moreover have "u \<notin> fst ` setD \<Delta>'" using check_varI(1) setD.simps fresh_DCons   by (simp add: fresh_d_not_in)
    moreover hence "\<Theta>; \<B>; \<Gamma> \<turnstile>\<^sub>w\<^sub>f (u, \<tau>') #\<^sub>\<Delta>\<Delta>' " using wfD_cons  fresh_DCons setD.simps check_varI check_v_wf  by metis
    ultimately show   "\<Theta> ; \<Phi> ; \<B> ; \<Gamma> ; (u, \<tau>') #\<^sub>\<Delta>\<Delta>'  \<turnstile> s \<Leftarrow> \<tau>" using check_varI by auto
  qed
next
  case (check_assignI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> u \<tau> v z \<tau>')
  moreover hence "(u, \<tau>) \<in> setD \<Delta>'" by auto
  ultimately show ?case using Typing.check_assignI by simp
next
  case (check_whileI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> s1 z s2 \<tau>')
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_seqI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> s1 z s2 \<tau>)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson
next
  case (check_caseI \<Theta> \<Phi> \<B> \<Gamma> \<Delta> tid dclist v cs \<tau> z)
  then show ?case using check_s_check_branch_s_check_branch_list.intros  by meson

qed

lemma valid_ce_eq:
  fixes v::v and ce2::ce
  assumes "ce1 = ce2[x::=v]\<^sub>c\<^sub>e\<^sub>v" and "wfV \<Theta>  \<B> GNil v b" and  "wfCE \<Theta>  \<B>  ((x, b, TRUE) #\<^sub>\<Gamma> GNil) ce2 b'" and "wfCE \<Theta>  \<B> GNil ce1 b'"
  shows \<open>\<Theta>; \<B>; (x, b, ([[x ]\<^sup>v]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e )) #\<^sub>\<Gamma> GNil  \<Turnstile> ce1  ==  ce2 \<close>
  unfolding valid.simps proof
  have wfg: "\<Theta> ; \<B>  \<turnstile>\<^sub>w\<^sub>f  (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil" 
    using wfG_cons1I wfG_nilI wfX_wfY assms wf_intros 
    by (meson fresh_GNil wfC_e_eq wfG_intros2)

  show wf: \<open>\<Theta>; \<B>; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f ce1  ==  ce2  \<close> 
    apply(rule wfC_eqI[where b=b'])
    using wfg toSet.simps assms wfCE_weakening apply simp

    using wfg assms wf_replace_inside1(8) assms 
    using wfC_trueI wf_trans(8)  by auto

  show \<open>\<forall>i. ((\<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i) \<and>  (i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil)  \<longrightarrow>
             (i \<Turnstile> (ce1  ==  ce2 )))\<close> proof(rule+,goal_cases)
    fix i
    assume as:"\<Theta> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and>  i \<Turnstile> (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil"
    have 1:"wfV \<Theta>  \<B> ((x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil) v b" 
      using wf_weakening assms append_g.simps toSet.simps wf wfX_wfY 
      by (metis empty_subsetI)
    hence "\<exists>s. i \<lbrakk> v \<rbrakk> ~ s"  using eval_v_exist[OF _ 1] as by auto
    then obtain s where iv:"i\<lbrakk> v \<rbrakk> ~ s" ..

    hence ix:"i x = Some s" proof -
      have "i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e" using is_satis_g.simps as by auto
      hence "i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e \<rbrakk> ~ True" using is_satis.simps by auto
      hence "i \<lbrakk>  [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s"  using  
          iv eval_e_elims
        by (metis eval_c_elims(7) eval_e_uniqueness eval_e_valI) 
      thus ?thesis using eval_v_elims(2) eval_e_elims(1) by metis
    qed

    have 1:"wfCE \<Theta>  \<B> ((x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e ) #\<^sub>\<Gamma> GNil) ce1 b'" 
      using wfCE_weakening assms append_g.simps toSet.simps wf wfX_wfY 
      by (metis empty_subsetI)
    hence "\<exists>s1. i \<lbrakk> ce1 \<rbrakk> ~ s1"  using eval_e_exist assms as by auto
    then obtain s1 where s1: "i\<lbrakk>ce1\<rbrakk> ~ s1" ..

    moreover have "i\<lbrakk> ce2 \<rbrakk> ~ s1" proof -
      have "i\<lbrakk> ce2[x::=v]\<^sub>c\<^sub>e\<^sub>v \<rbrakk> ~ s1" using assms s1 by auto
      moreover have "ce1 = ce2[x::=v]\<^sub>c\<^sub>e\<^sub>v" using subst_v_ce_def assms subst_v_simple_commute by auto
      ultimately have "i(x \<mapsto> s) \<lbrakk> ce2 \<rbrakk> ~ s1" 
        using ix subst_e_eval_v[of i ce1 s1 "ce2[z::=[ x ]\<^sup>v]\<^sub>v" x v s] iv s1 by auto
      moreover have "i(x \<mapsto> s) = i" using ix by auto
      ultimately show ?thesis by auto
    qed
    ultimately show "i \<lbrakk> ce1  ==  ce2 \<rbrakk> ~ True " using eval_c_eqI by metis
  qed
qed


lemma check_v_top:
  fixes v::v
  assumes  "\<Theta>; \<B>; GNil  \<turnstile> v \<Leftarrow> \<tau>" and "ce1 = ce2[z::=v]\<^sub>c\<^sub>e\<^sub>v" and  "\<Theta>; \<B>; GNil  \<turnstile>\<^sub>w\<^sub>f  \<lbrace> z : b_of \<tau>  | ce1 == ce2  \<rbrace>"    
    and "supp ce1 \<subseteq> supp  \<B>"
  shows "\<Theta>; \<B>; GNil  \<turnstile> v \<Leftarrow> \<lbrace> z : b_of \<tau>  | ce1 == ce2  \<rbrace>"      
proof -
  obtain t where t: "\<Theta>; \<B>; GNil  \<turnstile> v \<Rightarrow> t \<and> \<Theta>; \<B>; GNil  \<turnstile> t \<lesssim> \<tau>" 
    using assms check_v_elims by metis

  then obtain z' and b' where *:"t = \<lbrace> z' : b'  | [ [ z' ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e  \<rbrace> \<and> atom z' \<sharp> v \<and> atom z' \<sharp> (\<Theta>, \<B>,GNil)"
    using assms  infer_v_form by metis
  have beq: "b_of t = b_of \<tau>" using subtype_eq_base2 b_of.simps t by auto 
  obtain x::x where xf: \<open>atom x \<sharp> (\<Theta>, \<B>, GNil, z', [ [ z' ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e , z, ce1  ==  ce2 )\<close> 
    using obtain_fresh by metis

  have "\<Theta>; \<B>; (x, b_of \<tau>, TRUE) #\<^sub>\<Gamma> GNil   \<turnstile>\<^sub>w\<^sub>f (ce1[z::=[ x ]\<^sup>v]\<^sub>v  ==  ce2[z::=[ x ]\<^sup>v]\<^sub>v )"
    using wfT_wfC2[OF assms(3), of x] subst_cv.simps(6) subst_v_c_def subst_v_ce_def fresh_GNil by simp

  then obtain b2 where b2: "\<Theta>; \<B>; (x, b_of t, TRUE) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f ce1[z::=[ x ]\<^sup>v]\<^sub>v : b2 \<and> 
            \<Theta>; \<B>; (x, b_of t, TRUE) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f ce2[z::=[ x ]\<^sup>v]\<^sub>v : b2" using wfC_elims(3)
    beq by metis

  from xf have "\<Theta>; \<B>; GNil  \<turnstile> \<lbrace> z' : b_of t  | [ [ z' ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e  \<rbrace> \<lesssim>  \<lbrace> z : b_of t  | ce1 == ce2  \<rbrace>" 
  proof  
    show \<open> \<Theta>; \<B>; GNil   \<turnstile>\<^sub>w\<^sub>f \<lbrace> z' : b_of t  | [ [ z' ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e  \<rbrace> \<close> using b_of.simps assms infer_v_wf t * by auto
    show \<open> \<Theta>; \<B>; GNil   \<turnstile>\<^sub>w\<^sub>f \<lbrace> z : b_of t  | ce1  ==  ce2  \<rbrace> \<close> using beq assms by auto
    have \<open>\<Theta>; \<B>; (x, b_of t, ([ [ x ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e )) #\<^sub>\<Gamma> GNil  \<Turnstile> (ce1[z::=[ x ]\<^sup>v]\<^sub>v  ==  ce2[z::=[ x ]\<^sup>v]\<^sub>v ) \<close>  
    proof(rule valid_ce_eq)
      show \<open>ce1[z::=[ x ]\<^sup>v]\<^sub>v = ce2[z::=[ x ]\<^sup>v]\<^sub>v[x::=v]\<^sub>c\<^sub>e\<^sub>v\<close> proof -
        have "atom z \<sharp> ce1" using assms fresh_def x_not_in_b_set by fast 
        hence "ce1[z::=[ x ]\<^sup>v]\<^sub>v = ce1" 
          using forget_subst_v by auto
        also have "... = ce2[z::=v]\<^sub>c\<^sub>e\<^sub>v" using assms by auto
        also have "... = ce2[z::=[ x ]\<^sup>v]\<^sub>v[x::=v]\<^sub>c\<^sub>e\<^sub>v" proof -
          have "atom x \<sharp> ce2" using  xf fresh_prodN c.fresh by metis
          thus ?thesis using subst_v_simple_commute subst_v_ce_def by simp
        qed
        finally show ?thesis by auto
      qed
      show \<open> \<Theta>; \<B>; GNil \<turnstile>\<^sub>w\<^sub>f v : b_of t \<close> using infer_v_wf t by simp
      show  \<open>  \<Theta>; \<B>; (x, b_of t, TRUE) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f ce2[z::=[ x ]\<^sup>v]\<^sub>v : b2 \<close>  using b2 by auto

      have " \<Theta>; \<B>; (x, b_of t, TRUE) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\<^sub>f ce1[z::=[ x ]\<^sup>v]\<^sub>v : b2" using b2 by auto
      moreover have "atom x \<sharp> ce1[z::=[ x ]\<^sup>v]\<^sub>v" 
        using fresh_subst_v_if assms fresh_def 
        using \<open>\<Theta>; \<B>; GNil \<turnstile>\<^sub>w\<^sub>f v : b_of t\<close> \<open>ce1[z::=[ x ]\<^sup>v]\<^sub>v = ce2[z::=[ x ]\<^sup>v]\<^sub>v[x::=v]\<^sub>c\<^sub>e\<^sub>v\<close> 
          fresh_GNil subst_v_ce_def wfV_x_fresh by auto
      ultimately show  \<open>  \<Theta>; \<B>; GNil \<turnstile>\<^sub>w\<^sub>f ce1[z::=[ x ]\<^sup>v]\<^sub>v : b2 \<close> using
          wf_restrict(8) by force
    qed
    moreover have v: "v[z'::=[ x ]\<^sup>v]\<^sub>v\<^sub>v  = v" 
      using forget_subst assms infer_v_wf wfV_supp x_not_in_b_set 
      by (simp add: "local.*")
    ultimately show "\<Theta>; \<B>; (x, b_of t, ([ [ z' ]\<^sup>v ]\<^sup>c\<^sup>e  ==  [ v ]\<^sup>c\<^sup>e )[z'::=[ x ]\<^sup>v]\<^sub>v) #\<^sub>\<Gamma> GNil  \<Turnstile> (ce1  ==  ce2 )[z::=[ x ]\<^sup>v]\<^sub>v" 
      unfolding subst_cv.simps subst_v_c_def subst_cev.simps subst_vv.simps
      using subst_v_ce_def by simp
  qed
  thus ?thesis using b_of.simps assms * check_v_subtypeI t b_of.simps subtype_eq_base2 by metis
qed

end