Quelle  RCLogicL.thy

(*<*)
theory RCLogicL
  imports RCLogic WellformedL
begin
  (*>*)

hide_const Syntax.dom

chapter ‹Refinement Constraint Logic Lemmas›

section ‹Lemmas›

lemma wfI_domi:
  assumes "Θ ; Γ ⊨ i"
  shows "fst ` toSet Γ ⊆ dom i"
  using wfI_def toSet.simps assms by fastforce

lemma wfI_lookup:
  fixes G::Γ and b::b
  assumes "Some (b,c) = lookup G x" and "P ; G ⊨ i" and "Some s = i x" and "P ; B ⊨_wf G"
  shows "P ⊨ s : b"
proof -
  have "(x,b,c) ∈ toSet G" using lookup.simps assms
    using lookup_in_g by blast
  then obtain s' where *:"Some s' = i x ∧ wfRCV P s' b" using wfI_def assms by auto
  hence "s' = s" using assms  by (metis option.inject)
  thus ?thesis using * by auto
qed

lemma wfI_restrict_weakening:
  assumes "wfI Θ Γ' i'" and "i = restrict_map i' (fst `toSet Γ)" and "toSet Γ ⊆ toSet Γ'"
  shows  "Θ ; Γ ⊨ i"
proof -
  { fix x
    assume "x ∈ toSet Γ"
    have "case x of (x, b, c) ==> ∃s. Some s = i x ∧ Θ ⊨ s : b" using assms wfI_def
    proof -
      have "case x of (x, b, c) ==> ∃s. Some s = i' x ∧ Θ ⊨ s : b"
        using ‹x ∈ toSet Γ›  assms wfI_def by auto
      then have "∃s. Some s = i (fst x) ∧ wfRCV Θ s (fst (snd x))"
        by (simp add: ‹x ∈ toSet Γ› assms(2) case_prod_unfold)
      then show ?thesis
        by (simp add: case_prod_unfold)
    qed
  }
  thus ?thesis using wfI_def assms by auto
qed

lemma wfI_suffix:
  fixes G::Γ
  assumes "wfI P (G'@G) i" and "P ; B ⊨_wf G"
  shows "P ; G ⊨ i"
  using wfI_def append_g.simps assms toSet.simps by simp

lemma wfI_replace_inside:
  assumes "wfI Θ (Γ' @ (x, b, c) #_\<Gamma> Γ) i"
  shows  "wfI Θ (Γ' @ (x, b, c') #_\<Gamma> Γ) i"
  using wfI_def toSet_splitP assms by simp

section ‹Existence of evaluation›

lemma eval_l_base:
  "Θ ⊨ [ l ] : (base_for_lit l)"
  apply(nominal_induct l rule:l.strong_induct)
  using wfRCV.intros eval_l.simps  base_for_lit.simps by auto+

lemma obtain_fresh_bv_dclist:
  fixes tm::"'a::fs"
  assumes "(dc, { x : b | c }) ∈ set dclist" 
  obtains bv1::bv and dclist1 x1 b1 c1 where "AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1
      ∧ (dc, { x1 : b1 | c1 }) ∈ set dclist1 ∧ atom bv1 ♯ tm" 
proof - 
  obtain bv1 dclist1 where "AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 ∧ atom bv1 ♯ tm" 
    using obtain_fresh_bv by metis
  moreover hence "[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1" using type_def.eq_iff by metis
  moreover then obtain x1 b1 c1 where "(dc, { x1 : b1 | c1 }) ∈ set dclist1" using td_lookup_eq_iff assms by metis
  ultimately show ?thesis  using that by blast
qed

lemma obtain_fresh_bv_dclist_b_iff:
  fixes tm::"'a::fs"
  assumes "(dc, { x : b | c }) ∈ set dclist" and "AF_typedef_poly tyid bv dclist ∈ set P" and "⊨_wf P"
  obtains bv1::bv and dclist1 x1 b1 c1 where "AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1
      ∧ (dc, { x1 : b1 | c1 }) ∈ set dclist1 ∧ atom bv1 ♯ tm ∧ b[bv::=b']_bb=b1[bv1::=b']_bb" 
proof - 
  obtain bv1 dclist1 x1 b1 c1 where *:"AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1 ∧ atom bv1 ♯ tm
    ∧ (dc, { x1 : b1 | c1 }) ∈ set dclist1" using obtain_fresh_bv_dclist assms by metis

  hence "AF_typedef_poly tyid bv1 dclist1 ∈ set P" using assms by metis

  hence "b[bv::=b']_bb = b1[bv1::=b']_bb" 
    using  wfTh_typedef_poly_b_eq_iff[OF assms(2) assms(1) _ _ assms(3),of bv1 dclist1 x1 b1 c1 b']  * by metis

  from this that show ?thesis using * by metis  
qed

lemma eval_v_exist:
  fixes Γ::Γ and v::v and b::b
  assumes "P ; Γ ⊨ i" and "P ; B ; Γ ⊨_wf v : b"
  shows "∃s. i [ v ] ~ s ∧ P ⊨ s : b "
  using assms proof(nominal_induct v  arbitrary: b rule:v.strong_induct)
  case (V_lit x)
  then show ?case using eval_l_base eval_v.intros eval_l.simps wfV_elims rcl_val.supp pure_supp by metis
next
  case (V_var x)
  then obtain c where  *:"Some (b,c) = lookup Γ x" using wfV_elims by metis
  hence "x ∈ fst ` toSet Γ"  using lookup_x by blast
  hence "x ∈ dom i" using wfI_domi using assms by blast
  then obtain s where "i x = Some s" by auto
  moreover hence "P ⊨ s : b" using wfRCV.intros wfI_lookup * V_var
    by (metis wfV_wf)

  ultimately show ?case using eval_v.intros rcl_val.supp b.supp  by metis
next
  case (V_pair v1 v2)
  then  obtain b1 and b2 where *:"P ; B ; Γ ⊨_wf v1 : b1 ∧ P ; B ; Γ ⊨_wf v2 : b2 ∧ b = B_pair b1 b2" using wfV_elims by metis
  then obtain s1 and s2 where "eval_v i v1 s1 ∧ wfRCV P s1 b1 ∧ eval_v i v2 s2 ∧ wfRCV P s2 b2" using V_pair by metis
  thus   ?case using eval_v.intros wfRCV.intros * by metis
next
  case (V_cons tyid dc v)
  then obtain  s and  b'::b and dclist and x::x and c::c where "(wfV P B Γ v b') ∧ i [ v ] ~ s ∧ P ⊨ s : b' ∧ b = B_id tyid ∧
                 AF_typedef tyid dclist ∈ set P ∧ (dc, { x : b' | c }) ∈ set dclist" using  wfV_elims(4) by metis
  then show ?case using eval_v.intros(4) wfRCV.intros(5) V_cons by metis
next
  case (V_consp tyid dc b' v)

  obtain  b'a::b and bv and dclist and x::x and c::c where *:"(wfV P B Γ v b'a[bv::=b']_bb) ∧ b = B_app tyid b' ∧
                 AF_typedef_poly tyid bv dclist ∈ set P ∧ (dc, { x : b'a | c }) ∈ set dclist ∧
           atom bv ♯ (P, B_app tyid b',B) " using  wf_strong_elim(1)[OF V_consp(3)] by metis

  then obtain s where **:"i [ v ] ~ s ∧ P ⊨ s : b'a[bv::=b']_bb" using V_consp by auto

  have " ⊨_wf P" using wfX_wfY V_consp  by metis
  then obtain bv1::bv and dclist1 x1 b1 c1 where 3:"AF_typedef_poly tyid bv dclist = AF_typedef_poly tyid bv1 dclist1
      ∧ (dc, { x1 : b1 | c1 }) ∈ set dclist1 ∧ atom bv1 ♯ (P, SConsp tyid dc b' s, B_app tyid b')
          ∧ b'a[bv::=b']_bb = b1[bv1::=b']_bb" 
    using  *  obtain_fresh_bv_dclist_b_iff by blast

  have " i [ V_consp tyid dc b' v ] ~ SConsp tyid dc b' s" using  eval_v.intros  by (simp add: "**")

  moreover have " P ⊨ SConsp tyid dc b' s : B_app tyid b'" proof
    show ‹AF_typedef_poly tyid bv1 dclist1 ∈ set P› using 3 * by metis
    show ‹(dc, { x1 : b1 | c1 }) ∈ set dclist1› using 3 by auto 
    thus ‹atom bv1 ♯ (P, SConsp tyid dc b' s, B_app tyid b')› using * 3 fresh_prodN by metis
    show ‹ P ⊨ s : b1[bv1::=b']_bb› using  3 ** by auto
  qed

  ultimately show ?case using eval_v.intros wfRCV.intros V_consp * by auto
qed

lemma eval_v_uniqueness:
  fixes v::v
  assumes "i [ v ] ~ s" and "i [ v ] ~ s'"
  shows "s=s'"
  using assms proof(nominal_induct v arbitrary: s s' rule:v.strong_induct)
  case (V_lit x)
  then show ?case using eval_v_elims eval_l.simps by metis
next
  case (V_var x)
  then show ?case using eval_v_elims   by (metis option.inject)
next
  case (V_pair v1 v2)
  obtain s1 and s2 where s:"i [ v1 ] ~ s1 ∧ i [ v2 ] ~ s2 ∧ s = SPair s1 s2" using eval_v_elims V_pair by metis
  obtain s1' and s2' where s':"i [ v1 ] ~ s1' ∧ i [ v2 ] ~ s2' ∧ s' = SPair s1' s2'"  using eval_v_elims V_pair by metis
  then show ?case using eval_v_elims  using V_pair s s' by auto
next
  case (V_cons tyid dc v1)
  obtain sv1 where 1:"i [ v1 ] ~ sv1 ∧ s = SCons tyid dc sv1" using eval_v_elims V_cons by metis
  moreover obtain sv2 where 2:"i [ v1 ] ~ sv2 ∧ s' = SCons tyid dc sv2" using eval_v_elims V_cons by metis
  ultimately have "sv1 = sv2" using V_cons by auto
  then show ?case  using 1 2 by auto 
next
  case (V_consp tyid dc b v1)
  then show ?case using eval_v_elims  by metis

qed

lemma eval_v_base:
  fixes Γ::Γ and v::v and b::b
  assumes "P ; Γ ⊨ i" and "P ; B ; Γ ⊨_wf v : b" and "i [ v ] ~ s"
  shows "P ⊨ s : b"
  using eval_v_exist eval_v_uniqueness assms by metis

lemma eval_e_uniqueness:
  fixes e::ce
  assumes "i [ e ] ~ s" and "i [ e ] ~ s'"
  shows "s=s'"
  using assms proof(nominal_induct e arbitrary: s s' rule:ce.strong_induct)
  case (CE_val x)
  then show ?case using eval_v_uniqueness eval_e_elims by metis
next
  case (CE_op opp x1 x2)
  consider "opp = Plus" | "opp = LEq" | "opp = Eq" using opp.exhaust by metis
  thus  ?case proof(cases)
    case 1
    hence a1:"eval_e i (CE_op Plus x1 x2) s" and a2:"eval_e i (CE_op Plus x1 x2) s'" using CE_op by auto
    then show ?thesis using   eval_e_elims(2)[OF a1] eval_e_elims(2)[OF a2]
        CE_op eval_e_plusI 
      by (metis rcl_val.eq_iff(2))
  next
    case 2
    hence a1:"eval_e i (CE_op LEq x1 x2) s" and a2:"eval_e i (CE_op LEq x1 x2) s'" using CE_op by auto
    then show ?thesis using eval_v_uniqueness  eval_e_elims(3)[OF a1] eval_e_elims(3)[OF a2]
        CE_op eval_e_plusI 
      by (metis rcl_val.eq_iff(2))
  next
    case 3
    hence a1:"eval_e i (CE_op Eq x1 x2) s" and a2:"eval_e i (CE_op Eq x1 x2) s'" using CE_op by auto
    then show ?thesis using eval_v_uniqueness  eval_e_elims(4)[OF a1] eval_e_elims(4)[OF a2]
        CE_op eval_e_plusI 
      by (metis rcl_val.eq_iff(2))
  qed
next
  case (CE_concat x1 x2)
  hence a1:"eval_e i (CE_concat x1 x2) s" and a2:"eval_e i (CE_concat x1 x2) s'" using CE_concat by auto
  show ?case using  eval_e_elims(7)[OF a1] eval_e_elims(7)[OF a2] CE_concat eval_e_concatI rcl_val.eq_iff 
  proof -
    assume "∧P. (∧bv1 bv2. [s' = SBitvec (bv1 @ bv2); i [ x1 ] ~ SBitvec bv1 ; i [ x2 ] ~ SBitvec bv2 ] ==> P) ==> P"
    obtain bbs :: "bit list" and bbsa :: "bit list" where
      "i [ x2 ] ~ SBitvec bbs ∧ i [ x1 ] ~ SBitvec bbsa ∧ SBitvec (bbsa @ bbs) = s'"
      by (metis ‹∧P. (∧bv1 bv2. [s' = SBitvec (bv1 @ bv2); i [ x1 ] ~ SBitvec bv1 ; i [ x2 ] ~ SBitvec bv2 ] ==> P) ==> P›) (* 93 ms *)
    then have "s' = s"
      by (metis (no_types) ‹∧P. (∧bv1 bv2. [s = SBitvec (bv1 @ bv2); i [ x1 ] ~ SBitvec bv1 ; i [ x2 ] ~ SBitvec bv2 ] ==> P) ==> P› ‹∧s' s. [i [ x1 ] ~ s ; i [ x1 ] ~ s' ] ==> s = s'› ‹∧s' s. [i [ x2 ] ~ s ; i [ x2 ] ~ s' ] ==> s = s'› rcl_val.eq_iff(1)) (* 125 ms *)
    then show ?thesis
      by metis (* 0.0 ms *)
  qed
next
  case (CE_fst x)
  then show ?case using eval_v_uniqueness by (meson eval_e_elims rcl_val.eq_iff)
next
  case (CE_snd x)
  then show ?case using eval_v_uniqueness by (meson eval_e_elims rcl_val.eq_iff)
next
  case (CE_len x)
  then show ?case using eval_e_elims rcl_val.eq_iff
  proof -
    obtain bbs :: "rcl_val ==> ce ==> (x ==> rcl_val option) ==> bit list" where
      "∀x0 x1 x2. (∃v3. x0 = SNum (int (length v3)) ∧ x2 [ x1 ] ~ SBitvec v3 ) = (x0 = SNum (int (length (bbs x0 x1 x2))) ∧ x2 [ x1 ] ~ SBitvec (bbs x0 x1 x2) )"
      by moura (* 0.0 ms *)
    then have "∀f c r. ¬ f [ [| c |]^ce ] ~ r ∨ r = SNum (int (length (bbs r c f))) ∧ f [ c ] ~ SBitvec (bbs r c f)"
      by (meson eval_e_elims(8)) (* 46 ms *)
    then show ?thesis
      by (metis (no_types) CE_len.hyps CE_len.prems(1) CE_len.prems(2) rcl_val.eq_iff(1)) (* 31 ms *)
  qed

qed

lemma wfV_eval_bitvec:
  fixes v::v
  assumes "P ;  B ; Γ ⊨_wf v : B_bitvec" and "P ; Γ  ⊨ i"
  shows "∃bv. eval_v i v (SBitvec bv)"
proof -
  obtain s where "i [ v ] ~  s ∧ wfRCV P s B_bitvec" using eval_v_exist assms by metis
  moreover then obtain bv where "s = SBitvec bv" using wfRCV_elims(1)[of P s] by metis
  ultimately show ?thesis by metis
qed

lemma wfV_eval_pair:
  fixes v::v
  assumes "P ;  B ; Γ ⊨_wf v : B_pair b1 b2" and "P ; Γ  ⊨ i"
  shows "∃s1 s2. eval_v i v (SPair s1 s2)"
proof -
  obtain s where "i [ v ] ~  s ∧ wfRCV P s (B_pair b1 b2)" using eval_v_exist assms by metis
  moreover then obtain s1 and s2 where "s = SPair s1 s2" using wfRCV_elims(2)[of P s] by metis
  ultimately show ?thesis by metis
qed

lemma wfV_eval_int:
  fixes v::v
  assumes "P ;  B ; Γ ⊨_wf v : B_int" and "P ; Γ  ⊨ i"
  shows "∃n. eval_v i v (SNum n)"
proof -
  obtain s where "i [ v ] ~  s ∧ wfRCV P s (B_int)" using eval_v_exist assms by metis
  moreover then obtain n where "s = SNum n" using wfRCV_elims(3)[of P s] by metis
  ultimately show ?thesis by metis
qed

text ‹Well sorted value with a well sorted valuation evaluates›
lemma wfI_wfV_eval_v:
  fixes v::v and b::b
  assumes "Θ ;  B ; Γ ⊨_wf v : b" and "wfI Θ  Γ i"
  shows "∃s. i [ v ] ~  s ∧ Θ ⊨ s : b"
  using eval_v_exist assms by auto

lemma wfI_wfCE_eval_e:
  fixes e::ce and b::b
  assumes "wfCE P B G e b" and "P ; G ⊨ i"
  shows "∃s. i [ e ] ~ s ∧ P ⊨ s : b"
  using assms proof(nominal_induct e arbitrary: b rule: ce.strong_induct)
  case (CE_val v)
  obtain s where "i [ v ] ~ s ∧ P ⊨ s : b" using wfI_wfV_eval_v[of P B G v b i] assms wfCE_elims(1) [of P B G v b] CE_val by auto
  then show ?case using CE_val eval_e.intros(1)[of i v s ] by auto
next
  case (CE_op opp v1 v2)

  consider "opp =Plus" | "opp=LEq" | "opp=Eq" using opp.exhaust by auto

  thus ?case proof(cases)
    case 1
    hence "wfCE P  B G v1 B_int ∧ wfCE P  B G v2 B_int" using wfCE_elims(2) CE_op

      by blast
    then obtain s1 and s2 where *: "eval_e i v1 s1 ∧ wfRCV P s1 B_int ∧ eval_e i v2 s2 ∧ wfRCV P s2 B_int"
      using wfI_wfV_eval_v CE_op by metis
    then obtain n1 and n2 where **:"s2=SNum n2 ∧ s1 = SNum n1" using wfRCV_elims by meson
    hence "eval_e i (CE_op Plus v1 v2) (SNum (n1+n2))" using eval_e_plusI * ** by simp
    moreover have "wfRCV P (SNum (n1+n2)) B_int" using wfRCV.intros by auto
    ultimately show ?thesis using 1
      using CE_op.prems(1) wfCE_elims(2) by blast
  next
    case 2
    hence "wfCE P  B G v1 B_int ∧ wfCE P  B G v2 B_int" using wfCE_elims(3) CE_op
      by blast
    then obtain s1 and s2 where *: "eval_e i v1 s1 ∧ wfRCV P s1 B_int ∧ eval_e i v2 s2 ∧ wfRCV P s2 B_int"
      using wfI_wfV_eval_v CE_op by metis
    then obtain n1 and n2 where **:"s2=SNum n2 ∧ s1 = SNum n1" using wfRCV_elims by meson
    hence "eval_e i (CE_op LEq v1 v2) (SBool (n1 ≤ n2))" using eval_e_leqI * ** by simp
    moreover have "wfRCV P (SBool (n1≤n2)) B_bool" using wfRCV.intros by auto
    ultimately show ?thesis using 2
      using CE_op.prems wfCE_elims by metis
  next
    case 3
    then obtain b2 where "wfCE P  B G v1 b2 ∧ wfCE P  B G v2 b2" using wfCE_elims(9) CE_op
      by blast
    then obtain s1 and s2 where *: "eval_e i v1 s1 ∧ wfRCV P s1 b2 ∧ eval_e i v2 s2 ∧ wfRCV P s2 b2"
      using wfI_wfV_eval_v CE_op by metis
    hence "eval_e i (CE_op Eq v1 v2) (SBool (s1 = s2))" using eval_e_leqI *
      by (simp add: eval_e_eqI)
    moreover have "wfRCV P (SBool (s1 = s2)) B_bool" using wfRCV.intros by auto
    ultimately show ?thesis using 3
      using CE_op.prems wfCE_elims by metis
  qed
next
  case (CE_concat v1 v2)
  then obtain s1 and s2 where *:"b = B_bitvec ∧ eval_e i v1 s1 ∧ eval_e i v2 s2 ∧
      wfRCV P s1 B_bitvec ∧ wfRCV P s2 B_bitvec" using
    CE_concat
    by (meson wfCE_elims(6))
  thus ?case using eval_e_concatI wfRCV.intros(1) wfRCV_elims
  proof -
    obtain bbs :: "type_def list ==> rcl_val ==> bit list" where
      "∀ts s. ¬ ts ⊨ s : B_bitvec ∨ s = SBitvec (bbs ts s)"
      using wfRCV_elims(1) by moura (* 156 ms *)
    then show ?thesis
      by (metis (no_types) "local.*" wfRCV_BBitvecI eval_e_concatI) (* 78 ms *)
  qed
next
  case (CE_fst v1)
  thus ?case using eval_e_fstI wfRCV.intros wfCE_elims wfI_wfV_eval_v
    by (metis wfRCV_elims(2) rcl_val.eq_iff(4))
next
  case (CE_snd v1)
  thus ?case using eval_e_sndI wfRCV.intros wfCE_elims wfI_wfV_eval_v
    by (metis wfRCV_elims(2) rcl_val.eq_iff(4))
next
  case (CE_len x)
  thus ?case using eval_e_lenI wfRCV.intros wfCE_elims wfI_wfV_eval_v wfV_eval_bitvec
    by (metis wfRCV_elims(1))
qed

lemma eval_e_exist:
  fixes Γ::Γ and e::ce
  assumes "P ; Γ  ⊨ i" and "P ;  B ; Γ  ⊨_wf e : b"
  shows "∃s. i [ e ] ~ s"
  using assms proof(nominal_induct e arbitrary: b rule:ce.strong_induct)
  case (CE_val v)
  then show ?case using eval_v_exist wfCE_elims eval_e.intros by metis
next
  case (CE_op op v1 v2)

  show ?case proof(rule opp.exhaust)
    assume ‹op = Plus›
    hence "P ;  B ; Γ ⊨_wf v1 : B_int ∧ P ;  B ; Γ ⊨_wf v2 : B_int ∧ b = B_int" using wfCE_elims CE_op by metis
    then obtain n1 and n2 where "eval_e i v1 (SNum n1) ∧ eval_e i v2 (SNum n2)" using CE_op eval_v_exist wfV_eval_int
      by (metis wfI_wfCE_eval_e wfRCV_elims(3))
    then show ‹∃a. eval_e i (CE_op op v1 v2) a› using eval_e_plusI[of i v1 _ v2] ‹op=Plus› by auto
  next
    assume ‹op = LEq›
    hence "P ;  B ; Γ ⊨_wf v1 : B_int ∧ P ;  B ; Γ ⊨_wf v2 : B_int ∧ b = B_bool" using wfCE_elims CE_op by metis
    then obtain n1 and n2 where "eval_e i v1 (SNum n1) ∧ eval_e i v2 (SNum n2)" using CE_op eval_v_exist wfV_eval_int
      by (metis wfI_wfCE_eval_e wfRCV_elims(3))
    then show ‹∃a. eval_e i (CE_op op v1 v2) a› using eval_e_leqI[of i v1 _ v2] eval_v_exist ‹op=LEq› CE_op by auto
  next
    assume ‹op = Eq›
    then obtain b1 where "P ;  B ; Γ ⊨_wf v1 : b1 ∧ P ;  B ; Γ ⊨_wf v2 : b1 ∧ b = B_bool" using wfCE_elims CE_op by metis
    then obtain s1 and s2 where "eval_e i v1 s1 ∧ eval_e i v2 s2" using CE_op eval_v_exist wfV_eval_int
      by (metis wfI_wfCE_eval_e wfRCV_elims(3))
    then show ‹∃a. eval_e i (CE_op op v1 v2) a› using eval_e_eqI[of i v1 _ v2] eval_v_exist ‹op=Eq› CE_op by auto
  qed
next
  case (CE_concat v1 v2)
  then obtain bv1 and bv2 where "eval_e i v1 (SBitvec bv1) ∧ eval_e i v2 (SBitvec bv2)"
    using wfV_eval_bitvec wfCE_elims(6)
    by (meson eval_e_elims(7) wfI_wfCE_eval_e)
  then show ?case using eval_e.intros by metis
next
  case (CE_fst ce)
  then obtain b2 where b:"P ; B ; Γ ⊨_wf ce : B_pair b b2" using wfCE_elims by metis
  then obtain s where s:"i [ ce ] ~ s" using CE_fst by auto
  then obtain s1 and s2 where "s = (SPair s1 s2)" using eval_e_elims(4) CE_fst wfI_wfCE_eval_e[of P B Γ ce "B_pair b b2" i,OF b] wfRCV_elims(2)[of P s b b2]
    by (metis eval_e_uniqueness)
  then show ?case using s eval_e.intros by metis
next
  case (CE_snd ce)
  then obtain b1 where b:"P ; B ; Γ ⊨_wf ce : B_pair b1 b" using wfCE_elims by metis
  then obtain s where s:"i [ ce ] ~ s" using CE_snd by auto
  then obtain s1 and s2 where "s = (SPair s1 s2)"
    using eval_e_elims(5) CE_snd wfI_wfCE_eval_e[of P B Γ ce "B_pair b1 b" i,OF b] wfRCV_elims(2)[of P s b b1]
      eval_e_uniqueness
    by (metis wfRCV_elims(2))
  then show ?case using s eval_e.intros by metis
next
  case (CE_len v1)
  then obtain bv1 where "eval_e i v1 (SBitvec bv1)"
    using wfV_eval_bitvec CE_len wfCE_elims eval_e_uniqueness
    by (metis eval_e_elims(7) wfCE_concatI wfI_wfCE_eval_e)
  then show ?case using eval_e.intros by metis
qed

lemma eval_c_exist:
  fixes Γ::Γ and c::c
  assumes "P ; Γ  ⊨ i" and "P ; B ; Γ ⊨_wf c"
  shows "∃s. i [ c ] ~ s"
  using assms proof(nominal_induct c rule: c.strong_induct)
  case C_true
  then show ?case using eval_c.intros wfC_elims by metis
next
  case C_false
  then show ?case using eval_c.intros wfC_elims by metis
next
  case (C_conj c1 c2)
  then show ?case using eval_c.intros wfC_elims by metis
next
  case (C_disj x1 x2)
  then show ?case using eval_c.intros wfC_elims by metis
next
  case (C_not x)
  then show ?case using eval_c.intros wfC_elims by metis
next
  case (C_imp x1 x2)
  then show ?case using eval_c.intros eval_e_exist wfC_elims by metis
next
  case (C_eq x1 x2)
  then show ?case using eval_c.intros eval_e_exist wfC_elims by metis
qed

lemma eval_c_uniqueness:
  fixes c::c
  assumes "i [ c ] ~ s" and "i [ c ] ~ s'"
  shows "s=s'"
  using assms proof(nominal_induct c arbitrary: s s' rule:c.strong_induct)
  case C_true
  then show ?case using eval_c_elims by metis
next
  case C_false
  then show ?case using eval_c_elims by metis
next
  case (C_conj x1 x2)
  then show ?case using eval_c_elims(3) by (metis (full_types))
next
  case (C_disj x1 x2)
  then show ?case using eval_c_elims(4) by (metis (full_types))
next
  case (C_not x)
  then show ?case using eval_c_elims(6) by (metis (full_types))
next
  case (C_imp x1 x2)
  then show ?case using eval_c_elims(5) by (metis (full_types))
next
  case (C_eq x1 x2)
  then show ?case using eval_e_uniqueness eval_c_elims(7) by metis
qed

lemma wfI_wfC_eval_c:
  fixes c::c
  assumes "wfC P B G c" and "P ; G ⊨ i"
  shows "∃s. i [ c ] ~ s"
  using assms proof(nominal_induct c rule: c.strong_induct)
qed(metis wfC_elims wfI_wfCE_eval_e eval_c.intros)+

section ‹Satisfiability›

lemma satis_reflI:
  fixes c::c
  assumes "i ⊨ ((x, b, c) #_\<Gamma> G)"
  shows "i ⊨ c"
  using assms by auto

lemma is_satis_mp:
  fixes c1::c and c2::c
  assumes "i ⊨ (c1 IMP c2)" and "i ⊨ c1"
  shows "i ⊨ c2"
  using assms proof -
  have "eval_c i (c1 IMP c2) True" using is_satis.simps using assms by blast
  then obtain b1 and b2 where "True = (b1 ⟶ b2) ∧ eval_c i c1 b1 ∧ eval_c i c2 b2"
    using eval_c_elims(5) by metis
  moreover have "eval_c i c1 True" using is_satis.simps using assms by blast
  moreover have "b1 = True" using calculation eval_c_uniqueness by blast
  ultimately have "eval_c i c2 True" by auto
  thus ?thesis using is_satis.intros by auto
qed

lemma is_satis_imp:
  fixes c1::c and c2::c
  assumes "i ⊨ c1 ⟶ i ⊨ c2" and "i [ c1 ] ~ b1" and "i [ c2 ] ~ b2"
  shows "i ⊨ (c1 IMP c2)"
proof(cases b1)
  case True
  hence "i ⊨ c2" using assms is_satis.simps by simp
  hence "b2 = True" using is_satis.simps assms
    using eval_c_uniqueness by blast
  then show ?thesis using eval_c_impI is_satis.simps assms by force
next
  case False
  then show ?thesis using assms eval_c_impI is_satis.simps by metis
qed

lemma is_satis_iff:
  "i ⊨ G  = (∀x b c. (x,b,c) ∈ toSet G ⟶ i ⊨ c)"
  by(induct G,auto)

lemma is_satis_g_append:
  "i ⊨ (G1@G2) = (i ⊨  G1 ∧ i ⊨  G2)"
  using is_satis_g.simps is_satis_iff by auto

section ‹Substitution for Evaluation›

lemma eval_v_i_upd:
  fixes v::v
  assumes "atom x ♯ v" and "i [ v ] ~  s'"
  shows "eval_v ((i ( x ↦s))) v s' "
  using assms proof(nominal_induct v arbitrary: s' rule:v.strong_induct)
  case (V_lit x)
  then show ?case by (metis eval_v_elims(1) eval_v_litI)
next
  case (V_var y)
  then obtain s where *: "Some s = i y ∧ s=s'" using eval_v_elims by metis
  moreover have "x ≠ y" using ‹atom x ♯ V_var y› v.supp by simp
  ultimately have "(i ( x ↦s)) y = Some s"
    by (simp add: ‹Some s = i y ∧ s = s'›)
  then show ?case using eval_v_varI * ‹x ≠ y›
    by (simp add: eval_v.eval_v_varI)
next
  case (V_pair v1 v2)
  hence "atom x ♯ v1 ∧ atom x ♯ v2" using v.supp by simp
  moreover obtain s1 and s2 where *: "eval_v i v1 s1 ∧ eval_v i v2 s2 ∧ s' = SPair s1 s2" using eval_v_elims V_pair by metis
  ultimately have "eval_v ((i ( x ↦s))) v1 s1 ∧ eval_v ((i ( x ↦s))) v2 s2" using V_pair by blast
  thus ?case using eval_v_pairI * by meson
next
  case (V_cons tyid dc v1)
  hence "atom x ♯ v1" using v.supp by simp
  moreover obtain s1 where *: "eval_v i v1 s1 ∧ s' = SCons tyid dc s1" using eval_v_elims V_cons by metis
  ultimately have "eval_v ((i ( x ↦s))) v1 s1" using V_cons by blast
  thus ?case using eval_v_consI * by meson
next
  case (V_consp tyid dc b1 v1)

  hence "atom x ♯ v1" using v.supp by simp
  moreover obtain s1 where *: "eval_v i v1 s1 ∧ s' = SConsp tyid dc b1 s1" using eval_v_elims V_consp by metis
  ultimately have "eval_v ((i ( x ↦s))) v1 s1" using V_consp by blast
  thus ?case using eval_v_conspI * by meson
qed

lemma eval_e_i_upd:
  fixes e::ce
  assumes "i [ e ] ~ s'" and "atom x ♯ e"
  shows " (i ( x ↦s)) [ e ] ~ s'"
  using assms apply(induct rule: eval_e.induct) using eval_v_i_upd eval_e_elims
  by (meson ce.fresh eval_e.intros)+

lemma eval_c_i_upd:
  fixes c::c
  assumes "i [ c ] ~ s'" and "atom x ♯ c"
  shows "((i ( x ↦s))) [ c ] ~ s' "
  using assms proof(induct rule:eval_c.induct)
  case (eval_c_eqI i e1 sv1 e2 sv2)
  then show ?case using RCLogic.eval_c_eqI eval_e_i_upd c.fresh by metis
qed(simp add: eval_c.intros)+

lemma subst_v_eval_v[simp]:
  fixes v::v and v'::v
  assumes "i [ v ] ~  s" and "i [ (v'[x::=v]_vv) ] ~ s'"
  shows "(i ( x ↦ s )) [ v' ] ~ s'"
  using assms proof(nominal_induct v' arbitrary: s' rule:v.strong_induct)
  case (V_lit x)
  then show ?case using subst_vv.simps
    by (metis eval_v_elims(1) eval_v_litI)
next
  case (V_var x')
  then show ?case proof(cases "x=x'")
    case True
    hence "(V_var x')[x::=v]_vv = v" using subst_vv.simps by auto
    then show ?thesis using V_var eval_v_elims eval_v_varI eval_v_uniqueness True
      by (simp add: eval_v.eval_v_varI)
  next
    case False
    hence "atom x ♯ (V_var x')" by simp
    then show ?thesis using eval_v_i_upd False V_var by fastforce
  qed
next
  case (V_pair v1 v2)
  then obtain s1 and s2 where *:"eval_v i (v1[x::=v]_vv) s1 ∧ eval_v i (v2[x::=v]_vv) s2 ∧ s' = SPair s1 s2" using V_pair eval_v_elims subst_vv.simps by metis
  hence "(i ( x ↦ s )) [ v1 ] ~ s1 ∧ (i ( x ↦ s )) [ v2 ] ~ s2" using V_pair by metis
  thus ?case using eval_v_pairI subst_vv.simps * V_pair by metis
next
  case (V_cons tyid dc v1)
  then obtain s1 where "eval_v i (v1[x::=v]_vv) s1" using eval_v_elims subst_vv.simps by metis
  thus ?case using eval_v_consI V_cons
    by (metis eval_v_elims subst_vv.simps)
next
  case (V_consp tyid dc b1 v1)

  then obtain s1 where *:"eval_v i (v1[x::=v]_vv) s1 ∧ s' = SConsp tyid dc b1 s1" using eval_v_elims subst_vv.simps by metis
  hence "i ( x ↦ s ) [ v1 ] ~ s1" using V_consp by metis
  thus ?case using * eval_v_conspI by metis
qed

lemma subst_e_eval_v[simp]:
  fixes y::x and e::ce and v::v and e'::ce
  assumes "i [ e' ] ~  s'" and "e'=(e[y::=v]_cev)" and "i [ v ] ~  s"
  shows "(i ( y ↦ s )) [ e ] ~ s'"
  using assms proof(induct arbitrary: e rule: eval_e.induct)
  case (eval_e_valI i v1 sv)
  then obtain v1' where *:"e = CE_val v1' ∧ v1 = v1'[y::=v]_vv"
    using assms by(nominal_induct e rule:ce.strong_induct,simp+)
  hence "eval_v i (v1'[y::=v]_vv) sv" using eval_e_valI by simp
  hence "eval_v (i ( y ↦ s )) v1' sv" using subst_v_eval_v eval_e_valI by simp
  then show ?case using RCLogic.eval_e_valI * by meson
next
  case (eval_e_plusI i v1 n1 v2 n2)
  then obtain v1' and v2' where *:"e = CE_op Plus v1' v2' ∧ v1 = v1'[y::=v]_cev ∧ v2 = v2'[y::=v]_cev"
    using assms by(nominal_induct e rule:ce.strong_induct,simp+)
  hence "eval_e i (v1'[y::=v]_cev) (SNum n1) ∧ eval_e i (v2'[y::=v]_cev) (SNum n2)" using eval_e_plusI by simp
  hence "eval_e (i ( y ↦ s )) v1' (SNum n1) ∧  eval_e (i ( y ↦ s )) v2' (SNum n2)" using subst_v_eval_v eval_e_plusI
    using "local.*" by blast
  then show ?case using RCLogic.eval_e_plusI * by meson
next
  case (eval_e_leqI i v1 n1 v2 n2)
  then obtain v1' and v2' where *:"e = CE_op LEq v1' v2' ∧ v1 = v1'[y::=v]_cev ∧ v2 = v2'[y::=v]_cev"
    using assms by(nominal_induct e rule:ce.strong_induct,simp+)
  hence "eval_e i (v1'[y::=v]_cev) (SNum n1) ∧ eval_e i (v2'[y::=v]_cev) (SNum n2)" using eval_e_leqI by simp
  hence "eval_e (i ( y ↦ s )) v1' (SNum n1) ∧  eval_e (i ( y ↦ s )) v2' (SNum n2)" using subst_v_eval_v eval_e_leqI
    using * by blast
  then show ?case using RCLogic.eval_e_leqI * by meson
next
  case (eval_e_eqI i v1 n1 v2 n2)
  then obtain v1' and v2' where *:"e = CE_op Eq v1' v2' ∧ v1 = v1'[y::=v]_cev ∧ v2 = v2'[y::=v]_cev"
    using assms by(nominal_induct e rule:ce.strong_induct,simp+)
  hence "eval_e i (v1'[y::=v]_cev) n1 ∧ eval_e i (v2'[y::=v]_cev) n2" using eval_e_eqI by simp
  hence "eval_e (i ( y ↦ s )) v1' n1 ∧  eval_e (i ( y ↦ s )) v2' n2" using subst_v_eval_v eval_e_eqI
    using * by blast
  then show ?case using RCLogic.eval_e_eqI * by meson
next
  case (eval_e_fstI i v1 s1 s2)
  then obtain v1' and v2' where *:"e = CE_fst v1' ∧ v1 = v1'[y::=v]_cev"
    using assms by(nominal_induct e rule:ce.strong_induct,simp+)
  hence "eval_e i (v1'[y::=v]_cev) (SPair s1 s2)" using eval_e_fstI by simp
  hence "eval_e (i ( y ↦ s )) v1' (SPair s1 s2)" using eval_e_fstI * by metis
  then show ?case using RCLogic.eval_e_fstI * by meson
next
  case (eval_e_sndI i v1 s1 s2)
  then obtain v1' and v2' where *:"e = CE_snd v1' ∧ v1 = v1'[y::=v]_cev"
    using assms by(nominal_induct e rule:ce.strong_induct,simp+)
  hence "eval_e i (v1'[y::=v]_cev) (SPair s1 s2)" using eval_e_sndI by simp
  hence "eval_e (i ( y ↦ s )) v1' (SPair s1 s2)" using subst_v_eval_v eval_e_sndI * by blast
  then show ?case using RCLogic.eval_e_sndI * by meson
next
  case (eval_e_concatI i v1 bv1 v2 bv2)
  then obtain v1' and v2' where *:"e = CE_concat v1' v2' ∧ v1 = v1'[y::=v]_cev ∧ v2 = v2'[y::=v]_cev"
    using assms by(nominal_induct e rule:ce.strong_induct,simp+)
  hence "eval_e i (v1'[y::=v]_cev) (SBitvec bv1) ∧ eval_e i (v2'[y::=v]_cev) (SBitvec bv2)" using eval_e_concatI by simp
  moreover hence "eval_e (i ( y ↦ s )) v1' (SBitvec bv1) ∧  eval_e (i ( y ↦ s )) v2' (SBitvec bv2)"
    using subst_v_eval_v eval_e_concatI * by blast
  ultimately show ?case using RCLogic.eval_e_concatI * eval_v_uniqueness by (metis eval_e_concatI.hyps(1))
next
  case (eval_e_lenI i v1 bv)
  then obtain v1' where *:"e = CE_len v1' ∧ v1 = v1'[y::=v]_cev"
    using assms by(nominal_induct e rule:ce.strong_induct,simp+)
  hence "eval_e i (v1'[y::=v]_cev) (SBitvec bv)" using eval_e_lenI by simp
  hence "eval_e (i ( y ↦ s )) v1' (SBitvec bv)" using subst_v_eval_v eval_e_lenI * by blast
  then show ?case using RCLogic.eval_e_lenI * by meson
qed

lemma subst_c_eval_v[simp]:
  fixes v::v and c :: c
  assumes "i [ v ] ~  s" and "i [ c[x::=v]_cv ] ~ s1" and
    "(i ( x ↦ s)) [ c ] ~ s2"
  shows "s1 = s2"
  using assms proof(nominal_induct c arbitrary: s1 s2 rule: c.strong_induct)
  case C_true
  hence "s1 = True ∧ s2 = True" using eval_c_elims subst_cv.simps by auto
  then show ?case by auto
next
  case C_false
  hence "s1 = False ∧ s2 = False" using eval_c_elims subst_cv.simps by metis
  then show ?case by auto
next
  case (C_conj c1 c2)
  hence *:"eval_c i (c1[x::=v]_cv AND c2[x::=v]_cv) s1" using subst_cv.simps by auto
  then obtain s11 and s12 where "(s1 = (s11 ∧ s12)) ∧ eval_c i c1[x::=v]_cv s11 ∧ eval_c i c2[x::=v]_cv s12" using
      eval_c_elims(3) by metis
  moreover obtain s21 and s22 where "eval_c  (i ( x ↦ s)) c1 s21 ∧ eval_c  (i ( x ↦ s)) c2 s22 ∧ (s2 = (s21 ∧ s22))" using
      eval_c_elims(3) C_conj by metis
  ultimately show ?case using C_conj by (meson eval_c_elims)
next
  case (C_disj c1 c2)
  hence *:"eval_c i (c1[x::=v]_cv OR c2[x::=v]_cv) s1" using subst_cv.simps by auto
  then obtain s11 and s12 where "(s1 = (s11 ∨ s12)) ∧ eval_c i c1[x::=v]_cv s11 ∧ eval_c i c2[x::=v]_cv s12" using
      eval_c_elims(4) by metis
  moreover obtain s21 and s22 where "eval_c  (i ( x ↦ s)) c1 s21 ∧ eval_c  (i ( x ↦ s)) c2 s22 ∧ (s2 = (s21 ∨ s22))" using
      eval_c_elims(4) C_disj by metis
  ultimately show ?case using C_disj by (meson eval_c_elims)
next
  case (C_not c1)
  then obtain s11 where "(s1 = (¬ s11)) ∧ eval_c i c1[x::=v]_cv s11" using
      eval_c_elims(6) by (metis subst_cv.simps(7))
  moreover obtain s21 where "eval_c  (i ( x ↦ s)) c1 s21 ∧ (s2 = (¬s21))" using
      eval_c_elims(6) C_not by metis
  ultimately show ?case using C_not by (meson eval_c_elims)
next
  case (C_imp c1 c2)
  hence *:"eval_c i (c1[x::=v]_cv IMP c2[x::=v]_cv) s1" using subst_cv.simps by auto
  then obtain s11 and s12 where "(s1 = (s11 ⟶ s12)) ∧ eval_c i c1[x::=v]_cv s11 ∧ eval_c i c2[x::=v]_cv s12" using
      eval_c_elims(5) by metis
  moreover obtain s21 and s22 where "eval_c  (i ( x ↦ s)) c1 s21 ∧ eval_c  (i ( x ↦ s)) c2 s22 ∧ (s2 = (s21 ⟶ s22))" using
      eval_c_elims(5) C_imp by metis
  ultimately show ?case using C_imp by (meson eval_c_elims)
next
  case (C_eq e1 e2)
  hence *:"eval_c i (e1[x::=v]_cev == e2[x::=v]_cev) s1" using subst_cv.simps by auto
  then obtain s11 and s12 where "(s1 = (s11 = s12)) ∧ eval_e i (e1[x::=v]_cev) s11 ∧ eval_e i (e2[x::=v]_cev) s12" using
      eval_c_elims(7) by metis
  moreover obtain s21 and s22 where "eval_e  (i ( x ↦ s)) e1 s21 ∧ eval_e  (i ( x ↦ s)) e2 s22 ∧ (s2 = (s21 = s22))" using
      eval_c_elims(7) C_eq by metis
  ultimately show ?case using C_eq subst_e_eval_v by (metis eval_e_uniqueness)
qed

lemma wfI_upd:
  assumes "wfI Θ Γ i" and "wfRCV Θ s b" and "wfG Θ B ((x, b, c) #_\<Gamma> Γ)"
  shows "wfI Θ ((x, b, c) #_\<Gamma> Γ) (i(x ↦ s))"
proof(subst wfI_def,rule)
  fix xa
  assume as:"xa ∈ toSet ((x, b, c) #_\<Gamma> Γ)"

  then obtain x1::x and b1::b and c1::c where xa: "xa = (x1,b1,c1)" using toSet.simps
    using prod_cases3 by blast

  have "∃sa. Some sa = (i(x ↦ s)) x1 ∧ wfRCV Θ sa b1" proof(cases "x=x1")
    case True
    hence "b=b1" using as xa wfG_unique assms by metis
    hence "Some s = (i(x ↦ s)) x1 ∧ wfRCV Θ s b1" using assms True by simp
    then show ?thesis by auto
  next
    case False
    hence "(x1,b1,c1) ∈ toSet Γ" using xa as by auto
    then obtain sa where "Some sa = i x1 ∧ wfRCV Θ sa b1" using assms wfI_def as xa by auto
    hence "Some sa = (i(x ↦ s)) x1 ∧ wfRCV Θ sa b1" using False by auto
    then show ?thesis by auto
  qed

  thus "case xa of (xa, ba, ca) ==> ∃sa. Some sa = (i(x ↦ s)) xa ∧ wfRCV Θ sa ba" using xa by auto
qed

lemma wfI_upd_full:
  fixes v::v
  assumes "wfI Θ G i" and "G =  ((Γ'[x::=v]_\<Gamma>_v)@Γ)" and "wfRCV Θ s b" and "wfG Θ B  (Γ'@((x,b,c)#_\<Gamma>Γ))" and "Θ ; B  ; Γ ⊨_wf v : b"
  shows "wfI Θ  (Γ'@((x,b,c)#_\<Gamma>Γ)) (i(x ↦ s))"
proof(subst wfI_def,rule)
  fix xa
  assume as:"xa ∈ toSet (Γ'@((x,b,c)#_\<Gamma>Γ))"

  then obtain x1::x and b1::b and c1::c where xa: "xa = (x1,b1,c1)" using toSet.simps
    using prod_cases3 by blast

  have "∃sa. Some sa = (i(x ↦ s)) x1 ∧ wfRCV Θ sa b1"
  proof(cases "x=x1")
    case True
    hence "b=b1" using as xa wfG_unique_full assms by metis
    hence "Some s = (i(x ↦ s)) x1 ∧ wfRCV Θ s b1" using assms True by simp
    then show ?thesis by auto
  next
    case False
    hence "(x1,b1,c1) ∈ toSet (Γ'@Γ)" using as xa by auto
    then obtain c1' where "(x1,b1,c1') ∈ toSet (Γ'[x::=v]_\<Gamma>_v@Γ)" using xa as wfG_member_subst assms False by metis
    then obtain sa where "Some sa = i x1 ∧ wfRCV Θ sa b1" using assms wfI_def as xa by blast
    hence "Some sa = (i(x ↦ s)) x1 ∧ wfRCV Θ sa b1" using False by auto
    then show ?thesis by auto
  qed

  thus "case xa of (xa, ba, ca) ==> ∃sa. Some sa = (i(x ↦ s)) xa ∧ wfRCV Θ sa ba" using xa by auto
qed

lemma subst_c_satis[simp]:
  fixes v::v
  assumes "i [ v ] ~  s" and "wfC Θ B ((x,b,c')#_\<Gamma>Γ) c" and "wfI Θ Γ i" and "Θ ; B  ; Γ ⊨_wf v : b"
  shows "i ⊨ (c[x::=v]_cv) ⟷ (i ( x ↦ s)) ⊨ c"
proof -
  have "wfI Θ ((x, b, c') #_\<Gamma> Γ) (i(x ↦ s))" using wfI_upd assms wfC_wf eval_v_base by blast
  then obtain s1 where s1:"eval_c (i(x ↦ s)) c s1" using eval_c_exist[of Θ "((x,b,c')#_\<Gamma>Γ)" "(i ( x ↦ s))" B c ] assms by auto

  have "Θ ; B  ; Γ  ⊨_wf c[x::=v]_cv" using wf_subst1(2)[OF assms(2) _ assms(4) , of GNil x ] subst_gv.simps by simp
  then obtain s2 where s2:"eval_c i c[x::=v]_cv s2" using eval_c_exist[of Θ "Γ" "i" B "c[x::=v]_cv" ] assms by auto

  show ?thesis using s1 s2 subst_c_eval_v[OF assms(1) s2 s1] is_satis.cases
    using eval_c_uniqueness is_satis.simps by auto
qed

text ‹ Key theorem telling us we can replace a substitution with an update to the valuation ›
lemma subst_c_satis_full:
  fixes v::v and Γ'::Γ
  assumes "i [ v ] ~  s" and "wfC Θ B  (Γ'@((x,b,c')#_\<Gamma>Γ)) c" and "wfI Θ  ((Γ'[x::=v]_\<Gamma>_v)@Γ) i" and "Θ ; B  ; Γ ⊨_wf v : b"
  shows "i ⊨ (c[x::=v]_cv) ⟷ (i ( x ↦ s)) ⊨ c"
proof -
  have "wfI Θ (Γ'@((x, b, c')) #_\<Gamma> Γ) (i(x ↦ s))" using wfI_upd_full assms wfC_wf eval_v_base wfI_suffix wfI_def wfV_wf by fast
  then obtain s1 where s1:"eval_c (i(x ↦ s)) c s1" using eval_c_exist[of Θ "(Γ'@(x,b,c')#_\<Gamma>Γ)" "(i ( x ↦ s))" B c ] assms by auto

  have "Θ ; B ; ((Γ'[x::=v]_\<Gamma>_v)@Γ) ⊨_wf c[x::=v]_cv" using wbc_subst assms by auto

  then obtain s2 where s2:"eval_c i c[x::=v]_cv s2" using eval_c_exist[of Θ "((Γ'[x::=v]_\<Gamma>_v)@Γ)" "i" B "c[x::=v]_cv" ] assms by auto

  show ?thesis using s1 s2 subst_c_eval_v[OF assms(1) s2 s1] is_satis.cases
    using eval_c_uniqueness is_satis.simps by auto
qed

section ‹Validity›

lemma validI[intro]:
  fixes c::c
  assumes "wfC P B G c" and "∀i. P ; G ⊨ i ∧ i ⊨ G ⟶ i ⊨ c"
  shows "P ; B ; G ⊨ c"
  using assms valid.simps by presburger

lemma valid_g_wf:
  fixes c::c and G::Γ
  assumes "P ; B ; G ⊨ c"
  shows "P ; B ⊨_wf G"
  using assms wfC_wf valid.simps by blast

lemma valid_reflI [intro]:
  fixes b::b
  assumes "P ; B ; ((x,b,c1)#_\<Gamma>G) ⊨_wf c1" and "c1 = c2"
java.lang.NullPointerException
  using satis_reflI assms by simp

subsection‹

text ‹

lemma eval_v_weakening:
  fixes c::v and B::"bv fset"
  assumes "i = i'|` d" and "supp c ⊆ atom ` d ∪}Normal
  showsem Mod Modal Simplific (based on pure eventual, pure universal, orpure univer, or sususpe formulas)
  using assms proof(nominal_induct c arbitrary:s rule: vparts o LTL\\.thy (CAVA, LTL\\TO\_G). FuFurthesome rrul were taken from
  case (V_lit x)
  then show ?case using eval_v_elims eval_v_litI by metis
next
  case (V_var x)
  have "atom x ∈ atom ` d" using x_not_in_b_set[of x B] assms v.supp(2) supp_at_base
  proof -
    show ?thesis
      by (metis UnE V_var.prems(2) ‹atom x ∉ supp B› singletonI subset_iff supp_at_base v.supp(2)) (* 46 ms *)  cite
  qed
  moreover have "Some s = i x" using assms eval_v_elims(2)
    using V_var.prems(3) by blast
  hence "Some s= i' x" using assms insert_subset restrict_in
  proof -
    show ?thesis
      by (metis (no_types) ‹i = i' |` d› ‹Some s = i x› atom_eq_iff calculation imageE restrict_in) (* 31 ms *)
  qed
   ?cas usineval_v.eval_v_varI

next
  case (V_pair v1 v2)
  then show ?case using eval_v_elims(3) eval_v_pairI v.supp
    by (metis assms le_sup_iff)
next
  case (V_cons dc v1)
  then show ?case using eval_v_elims(4) eval_v_consI v.supp
    by (metis assms le_sup_iff)
next
   (V_onsp tyid dc b1 v1))

  then obtain sv1 where *:"i [ v1 ] ~ sv1 ∧ s = SConsp tyid dc b1 sv1" using eval_v_elims by metis
  hence "i' [ v1 ] ~ sv1" using V_consp by auto
  then show ?case using * eval_v_conspI v.supp eval_v.simps assms le_sup_iff by metis
qed

lemma eval_v_restrict:
  fixes c::v and B::"bv fset"
  assumes "i = i' |` d" and "supp c ⊆ atom ` d ∪ supp B " and "i' [ c ] ~ s"
  shows "i [ c ] ~ s"
  using assms proof(nominal_induct c arbitrary:s rule: v.strong_induct)
  case (V_lit x)
  then show ?case using eval_v_elims eval_v_litI by metis
next
  case (V_var x)
  have "atom x ∈ atom ` d" using x_not_in_b_set[of x B] assms v.supp(2) supp_at_base
  proof -
    
      by (metis UnE V_var.prems(2) ‹atom x ∉ supp B› singletonI subset_iff supp_at_base v.supp(2)) (* 46 ms *)
  qed
  moreover have "Some s = i' x" using assms eval_v_elims(2)
    using V_var.prems(3) by blast
  hence "Some s= i x" using assms insert_subset restrict_in
  proof -
    show ?thesis
      by (metis (no_types) ‹i = i' |` d› ‹Some s = i' x› atom_eq_iff calculation imageE restrict_in) (* 31 ms *)
  qed
  thus ?case using eval_v.eval_v_varI by simp
next
  case (V_pair v1 v2)
  then show ?case using eval_v_elims(3) eval_v_pairI v.supp
    by (metis assms le_sup_iff)
next
  case (V_cons dc v1)
  then show ?case using eval_v_elims(4) eval_v_consI v.supp
    by (metis assms le_sup_iff)
next
  case (V_consp tyid dc b1 v1)
  then obtain sv1 where *:"i \lbrakk v1 \<  
  hence "i [ v1 ] ~ sv1" using V_consp by auto
  then show ?case using * eval_v_conspI v.supp eval_v.simps assms le_sup_iff by metis
qed

lemma eval_e_weakening:
  fixes e::ce and B::"bv fset"
  assumes "i [ e ] ~ s" and "i = i' |` d" and "supp e ⊆ atom ` d ∪ supp B "
  shows "i' [ e ] ~ s"
  using assm prorule:: eval_e..induct)
  case (eval_e_valI i v sv)
  then show ?case using ce.supp eval_e.intros
    using eval_v_weakening by auto
next
  case (eval_e_plusI i v1 n1 v2 n2)
  then show ?case using ce.supp eval_e.intros
    using eval_v_weakening by auto
next
   (eval_e_ i v1 n1 v2 n2))
  then show ?case using ce.supp eval_e.intros
    using eval_v_weakening by auto
next
  case (eval_e_eqI i v1 n1 v2 n2)
  then show ?case using ce.supp eval_e.intros
    using eval_v_weakening by auto
next
  case (eval_e_fstI i v v1 v2)
  then show ?case using ce.supp eval_e.intros
    using eval_v_weakening by metis
next
  case (eval_e_sndI i v v1 v2)
  then show ?case using ce.supp eval_e.intros
    using eval_v_weakening by metis
wher
  case (eval_e_concatI i v1 bv2 v2 bv1)
  then show ?case using ce.supp eval_e.intros
    using eval_v_weakening by auto
next
  case (eval_e_lenI i v bv)
  then show ?case using ce.supp eval_e.intros
    using eval_v_weakening by auto
qed

lemma eval_e_restrict :
  fixes e::ce and B::"bv fset"
  assumes "i' [>n \Rightarrowtrue\^>n | false_^>n y)"
  shows "i [ e ] ~ s"
  using assms proof(induct rule: eval_e.induct)
  case (eval_e_valI i v sv)
  then show ?case using ce.supp eval_e.intros
    using eval_v_restrict by auto
next
  case (eval_e_plusI i v1 n1 v2 n2)
  then show ?case using ce.supp eval_e.intros
    using eval_v_restrict by auto
next
  case (eval_e_leqI i v1 n1 v2 n2)
  then show ?case using ce.supp eval_e.intros
    using eval_v_restrict by auto
next
  case (eval_e_eak_until
  then show ?case using ce.supp eval_e.intros
    using eval_v_restrict by auto
next
  case (eval_e_fstI i v v1 v2)
  then show ?case using ce.supp eval_e.intros
    using eval_v_restrict by metis
next
  case (eval_e_sndI i v v1 v2)| _ <> (case xx of true\^>n ==>y | 🚫
  then show ?case using ce.supp eval_e.intros
    using eval_v_restrict by metis
next
  case (eval_e_concatI i v1 bv2 v2 bv1)
  then show mk_strong_release x y ≡
    using eval_v_restrict by auto
next
  case (eval_e_lenI i v bv)
  then show ?case using ce.supp eval_e.intros
    using eval_v_restrict by auto
qed

lemma eval_c_i_weakening:
  fixes c::c and B::"bv fset"
  assumes "i [ c ] ~ s" and "i = i' |` d" and "supp c ⊆ atom ` d ∪ supp B"
  shows "i' [ c ] ~ s"
  using assms proof(induct rule:eval_c.induct)
  case (eval_c_eqI i e1 sv1 e2 sv2)
  then show ?case using eval_c.intros eval_e_weakening by auto
qed(auto simp add: eval_c.intros)+

lemma eval_c_i_restrict:
  fixes c::c and B::"bv fset"
  assumes "i' [ c ] ~ s" and "i = i' |` d" and "supp c ⊆ atom ` d ∪ supp B"
  shows "i [
  using assproof(induct rule:eval_c.induct)
  case (eval_c_eqI i e1 sv1 e2 sv2)
  then show ?casede mk_next_pow (\open\<^>'
qed(auto simp add: eval_c.intros)+

lemma is_satis_i_weakening:
  fixes c::c and B::"bv fset"
  assumes "i = i' |` d" and "supp c ⊆ atom ` d ∪ supp B " and "i ⊨ c"
  shows "i' ⊨ c"
  using is_satis.simps eval_c_i_weakening[OF _ assms(1) assms(2) ]
  using assms(3) by auto

lemma is_satis_i_restrict:
  fixes c::c and B::"bv fset"
  assumes "i = i' |` d" and "supp c ⊆ atom ` d ∪ supp B" and "i' ⊨ c"
  shows "i ⊨ c"
  using is_satis.simps eval_c_i_restrict[OF _ assms(1) assms(2) ]
  using assms(3) by auto

lemma is_satis_g_restrict1:
  fixes Γ'::\<  "
  assumes "toSet Γ ⊆ toSet Γ'" and "i ⊨ Γ'"
  shows "i ⊨ Γ"
  using assms proof(induct Γ rule: Γ.induct)
  case GNil
  then show ?case by auto
next
  case (GCons xbc G)
  obtain x and b and c::c where xbc: "xbc=(x,b,c)"
    using prod_cases3 by blast
  hence "i ⊨ G" using GCons by auto
  moreover have "i ⊨ c" using GCons
      is_satis_iff toSet.simps subs
    using xbc by blast
  ultimately show ?case using is_satis_g.simps GCons
    by (simp add: xbc)
qed

lemma is_satis_g_restrict2:
  fixes Γ'::Γ and Γ::Γ
  assumes "i ⊨ Γ"by
  shows "i' ⊨
  using proof(induct \Gamma: Γ
  case GNil
  then show ?case by auto
next
  case (GCons x b c G)

  hence "i' ⊨ G" proof -
    have "i ⊨ G" using GCons by simp
    moreover have "atom_dom G ⊆ atom ` d" using GCons by simp
    ultimately show ?thesis using GCons wfG_cons2 by blast
  qed

  moreover have "i' ⊨ c" proof -
    have "i ⊨ c" using GCons by auto
    moreover have "Θ ; B ; (x, b, TRUE) #_\<Gamma> G ⊨_wf c" using wfG_wfC GCons by simp
    moreover hence "supp c ⊆ atom ` d ∪ supp B" using wfC_supp GCons atom_dom_eq by blast
    ultimately show ?thesis using is_satis_i_restrict[of i' i d c] GCons by simp
  qed

  ultimately show ?case by auto
qed

lemma is_satis_g_restrict:
  fixes Γ
java.lang.NullPointerException
  shows "i ⊨ Γ"
  using assms is_satis_g_restrict1[OF assms(1) assms(2)] is_satis_g_restrict2[OF _ assms(3)] by simp

subsection ‹mk_globally_def semantics_ltln.simps(8,) removsimps split: ltln.splits)

lemma is_satis_c_i_upd:
  fixes c::c
  assumes "atom x ♯ c" and "i ⊨ c"
  shows "((i ( x ↦
  using assms eval_c_i_upd is_satis.simps by simp

lemma is_satis_g_i_upd:
  fixes G::Γ
  assumes "atom x ♯ G" and "i ⊨ G"
  shows "((i ( x ↦s))) ⊨ G"
  using assms proof(induct G rule: Γ_induct)
  case GNil
  then show ?case by auto
next
  case (GC

  hence *:"atom x ♯ G' ∧ fsi mk)+
    using fresh_def fresh_GCons GCons by force
  moreoverhenc "is_sati(i ( x \<>s
    using is_satis_c_i_upd GCons is_satis_g.simps by auto
  moreover have " is_satis_g (i(x ↦ s)) G'" using GCons * by fastforce
  ultimately show ?case
    using GCons is_satis_g.simps(2) by metis
qed

lemma valid_weakening:
>B \Gamma\Turnstilec an "to <> \subseteq t" "wfG \Theta B \Gamma>'"
  shows "Θ ; B ; Γ' ⊨ c"
proof -
  have "wfC Θ B Γ c" using assms valid.simps by auto
java.lang.StringIndexOutOfBoundsException: Index 4 out of bounds for length 4
    using atom_dom.simps dom.simps wf_supp(2) by metis
  have wfg: "wfG Θ B Γ" using assms valid.simps wfC_wf by auto

  moreover have a1: "(∀i. wfI Θ
     F mk
    assume as: "wfI Θ Γ' i ∧
    hence as1: "fst ` toSet Γsimp mk_we
    obtain i' where idash: "i' = restrict_map i (fst `toSet Γ)" by blast
    hence as2: "dom i' = (fst `toSet Γ<> w \Turnstile^u>nx M\<^> 

    have id2: "Θ ; Γ ⊨ i' ∧ i' ⊨
      have "wfI Θ
        usingt ?t
      moreover have "i' ⊨ s iidash by au
      ultimately show ?thesis using idash by auto
    qed
    hence "i' ⊨ c" using assms valid.simps by auto
    thus "i ⊨ c" using assms valid.simps is_satis_i_weakening idash sp by ed (cases x;; : mk_strong_rel+
qed
  moreover have "wfC Θ B Γ' c" using wf_weakening assms valid.simps
    by (meson wfg)
  ultimately show ?thesis using assms valid.simps by auto
qed

lemma is_satis_g_suffix:
  fixes G::Γ
  assumes "i ⊨ (G'@G)"
  shows "i ⊨
  using assms proof(induct G' rule:Γ.induct)
  case GNil
  then show ?case by auto
next
  case (GCons xbc x2)
  obtain x and b and c::c where xbc: "xbcfun is_constant :: "'a lt ==>
    using prod_cases3 by blast
  hence " i ⊨ (xbc #_\"i _ == Fa
  then show ?case using is_sati :
qed

lemma wfG_inside_valid2:
  fixes x::x and Γ::Γ and c0::c and c0'::c
  assumes "wfG Θ B (Γ>\<>is_constant
    "Θ ; B ; Γ'@(x,b0,c0)#_\<Gamma>Γ ⊨ c0'"
  shows "wfG Θ B (Γ x \Longrightarrow y \Longrightarrow (mk_x yy)"
proof -
  have "wfG Θ B (Γ'@(x,b0,c0)#_\<Gamma>Γ)" using valid.simps wfC_wf assms by auto
thus ?thesis u wfG_rplac assms by au
qed

lemma valid_trans:
  assumes " Θ ; B ; Γ ⊨ c0[z::=v]_v" and " Θ ; B ; (z,b,c0)#_\<Gamma>Γ ⊨
  shows " Θ ; B ; Γ ⊨ c1[z::=v]_v"
proof -
  have *:"wfC Θ B ((z,b,c0)#_\<Gamma>Γ) c1" using valid.simps assms by auto
   "wfC Θ\<^>)

  moreover have "∀i. wfI Θ Γ i ∧ is_satis_g i Γ ⟶ is_satis i (c1[z::=v]_v)"
  proof(rule,rule)
    fix i
    assume as: "wfI Θ Γ i ∧ is_satis_g i Γ"
    then obtain sv where sv: "eval_v i v sv ∧"isconsx \Longrightarrow (mk_ y)
    hence "is_satis i (c0[z::=v]_<>is (m y x)"
    hence "is_satis (i(z ↦ sv)) c0" using subst_c_satis sv as assms valid.simps wfC_wf wfG_elim2 subst_v_c_def by metis
    moreover have "is_satis_g (i(z ↦ sv)) Γ"
      using is_satis_g_i_upd assms by (simp add: as)
    ultimately have "is_satis_g (i(z ↦ sv)) ((z,b,c0)#_\<Gamma>Γ)"
      using is_satis_g.simps by simp
    moreover have "wfI Θ ((z,b,c0)#_\<Gamma>Γ) (i(z ↦ sv))" using as wfI_upd sv assms valid.simps wfC_wf by metis
    ultimately have "is_satis (i(z ↦ sv)) c1" using assms valid.simps by auto
    thus "is_satis i (c1[z::=v]_v)" using subst_c_satis sv as assms valid.simps wfC_wf wfG_elim2 subst_v_c_def by metis
  qed

  ultimately show ?thesis using valid.simps by auto
qed

lemma valid_trans_full:
  assumes "Θ ; B ; "is_con x ==>
    "Θ ; B ; ((x, b, c2[z2::=V_var x]_v) #_\<Gamma> Γ) ⊨ c3[z3::=V_var x]_v"
  shows "Θ ; B ; ((x,; cases y; simp add: m mk_or_def mk mk_g mk_unti mk mk_weak_unti mk_s mk_nex mk_)+
  unfolding valid.simps proof
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0

  show "∀i. ( wfI Θ ((x, b, c1[z1::=V_var x]_v) #_\<Gamma> Γ) i ∧ (is_satis_g i ((x, b, c1[z1::=V_var x]_v) #_\<Gamma> Γ)) ⟶ (is_satis i (c3[z3::=V_var x]_v)) ) "
  proofn n) (cas x; si ad mk_n+
    fix i
    assume as: "Θ\longleftrightarrow<sub>n <nd> y == true\<> 
    have "i ⊨ c2[z2::=V_var x]_v" using is_satis_g.simps as assms by simp
    moreover have "i ⊨ Γ" using is_satis_g.simps as by simp
    ultimately show "i ⊨ c3[z3::=V_var x]_v " using assms is_satis_g.simps valid.simps
      by (metis append_g.simps(1) as wfI_replace_inside)
  qed
qed

lemma eval_v_weakening_x:
  fixes c::v
  assumes i' \lbrakkc]i = i' (x↦
  shows "i [ c ] ~ s"
  using assms proof(induct rule: eval_v.induct)
  case (eval_v_litI i l)
  then show ?case using eval_v.intros by auto
next
  case (eval_v_varI sv i1 x1)
  hence "x ≠ x1" using v.fresh fresh_at_base by auto
  hence "i x1 = Some sv" using eval_v_varI by simp
  then show ?case using eval_v.intros by auto
next
   evai v1 s1 v s2)
  then show ?case using eval_v.intros by auto
next
  case (eval_v_consI i v s tyid dc)
  then show ?case using eval_v.intros by auto
next
  case (eval_v_conspI i v s tyid dc b)
  then sho ?ca us eval_vintro by aauto
qed

lemma eval_e_weakening_x:
  fixes c::ce
  assumes "i' [ c ] ~ s" and "atom x ♯ c" and "i = i' (x ↦ s')"
  shows "i [ c ] ~ s"
  using assms proof(induct rule: eval_e.induct)
  case (eval_e_valI i v sv)
  then show ?case using eval_v_weakening_x eval_e.intros ce.fresh by metis
next
  case (eval_e_plusI i v1 n1 v2 n2)
  then show ?case using eval_v_weakening_x eval_e.intros ce.fresh by metis
next
caseeval_e_leqIi vv2 n)
  then show ?case using eval_v_weakening_x eval_e.intros ce.fresh by metis
next
  case (eval_e_eqI i v1 n1 v2 n2)
  then show ?case using eval_v_weakening_x eval_e.intros ce.fresh by metis
next
  case (eval_e_fstI i v v1 v2)
  then show ?case using eval_v_weakening_x eval_e.intros ce.fresh by metis
next
  case (eval_e_sndI i v v1 v2)
  then show ?case using eval_v_weakening_x eval_e.intros ce.fresh by metis
next
  case (eval_e_concatI i v1 bv1 v2 bv2)
  then show ?case using eval_v_weakening_x eval_e.intros ce.fresh by metis
next
  case (eval_e_lenI i v bv)
  then show ?case using eval_v_weakening_x eval_e.intros ce.fresh by metis
qed

lemma eval_c_weakening_x:
  fixes c::c
  assumes "i' [ c ] ~ s" and "atom x ♯ c" and "i = i' (x ↦ s')"
  shows "i [ c ] ~ s"
  using assms proof(induct rule: eval_c.induct)
  case (eval_c_trueI i)
  then show ?case using eval_c.intros by auto
java.lang.StringIndexOutOfBoundsException: Index 4 out of bounds for length 4
case eval_c_falseI i))
  then show ?case using eval_c.intros by auto
next
  case (eval_c_conjI i c1 b1 c2 b2)
  then show ?case using eval_c.intros by auto
next
  case (eval_c_disjI i c1 b1 c2 b2)
  then show ?case using eval_c.intros by auto
next
  case (eval_c_impI i c1 b1 c2 b2)
  then show ?case using eval_c.intros by auto
next
  case (eval_c_notI i c b)
  then show ?case using eval_c.intros by auto
next
  case (eval_c_eqI i e1 sv1 e2 sv2)
  then show ?case using eval_e_weakening_x c.fresh eval_c.intros by metis
qed

lemma is_satis_weakening_x:
  fixes c::c
  assumes "i' ⊨ c" and "atom x ♯ c" and "i = i' (x ↦ s)"
  shows "i ⊨ c"
  using eval_c_weakening_x assms is_satis.simps by simp

lemma is_satis_g_weakening_x:
  fixes G::Γ
  assumes "i' ⊨ G" and "atom x ♯ G" and "i = i' (x ↦ s)"
  shows "i ⊨ G"
  using assms proof(induct G rule: Γ_induct)
  case GNil
  then show ?case by auto
next
  case (GCons x' b' c' Γ')
  hence "atom x ♯ c'" usin (i + jj) φ>)
  moreover hence "i ⊨ c'" using is_satis_weakening_x is_satis_g.simps(2) GCons by metis
  then show ?case using by (ca si) (cas \phi si add:: mk funpow_; simadd:: fun)
qed

section ‹i ) φ) U 🚫

text ‹The idea of boxing is to take an smt val and its base type and at nodes in the smt val that correspond to type variables we
wrap them in an SUt smt val node. Another way of looking at it is that s' where the node for the base type variable is an 'any node'.
It is needed to prove subst\_b\_valid - the base-type variable substitution lemma for validity.

The first @{text "rcl_val"} is the expanded form (has type with base-variables replaced with base-type terms)
 ; the second is its corresponding form

We only have one variable so we need to ensure that in all of the @{text "bs_boxed_BVarI"} cases, the s has the same
  base type.

For example is an SMT value is (SPair (SInt 1) (SBool true)) and it has sort (BPair (BVar x) BBool)[x::=BInt] then
the boxed version is SPair (SUt (SInt 1)) (SBool true) and is has sort (BPair (BVar x) BBool). We need to do this
so that we can obtain from a valuation i, that gives values like the first smt value, to a valuation i' that gives values like
the second.
\close

inductive boxed_b :: "Θ ==> rcl_val ==> b ==> bv ==> b ==> rcl_val ==> bool" ( ‹
  boxed_b_BVar1I: "[
| boxed_b_BVar2I: "[ bv ≠ bv'; wfRCV P s (B_var bv') ] ==> boxed_b P s (B_var bv') bv b s"
| boxed_b_BIntI:"wfRCV P s B_int ==> boxed_b P s B_int _ _ s"
boxed_b_BBoolI P s B_bo\Longrightarrowboxed_b P s B_bool _ _ "
| boxed_b_BUnitI:"wfRCV P s B_unit ==> boxed_b P s B_unit _ _ s"
| boxed_b_BPairI:"[ boxed_b P s1 b1 bv b s1' ; boxed_b P s2 b2 bv b s2' ] ==> boxed_b P (SPair s1 s2) (B_pair b1 b2) bv b (SPair s1' s2')"

| boxed_b_BConsI:"[ as far as possible. po›
      AF_typedef tyid dclist ∈
      (dc, { x : b | c }
      boxed_b P s1 b bv b' s1'
      ] ==>
     boxed_b P (SCons tyid dc s1) (B_id tyid) bv b' (SCons tyid dc s1')"

| boxed_b_BConspI:"[ AF_typedef_poly tyid bva dclist ∈ set P;
      atom bva ♯ (b1,bv,b',s1,s1');
\in>set d dcli ;
      boxed_b P s1 (b[bva::=b1]_bb) bv b' s1'
      ] ==>
      boxed_b P (SConsp tyid dc b1[bv::=b']_bb s1) (B_app tyid b1) bv b' (SConsp tyid dc b1 s1')"

| boxed_b_Bbitvec: "wfRCV P s B_bitvec ==>mk_n (the_nat_0 (j - i)) ψ

equivariance boxed_b
nominal_inductive boxed_b .

inductive_cases boxed_b_elims:
  "boxed_b P s (B_var bv) bv' b s'"
  "boxed_b P s B_int bv b s'"
  "boxed_b P s B_bool bv b s'"
  "boxed_b P s B_unit bv b s'"
  "boxed_b P s (B_pair b1 b2) bv b s'"
  "boxed_b P s (B_id dc) bv b s'"
  "boxed_b P s B_bitvec bv b s'"
  "boxed_b P s (B_app dc b') bv b s'"

lemma boxed_b_wfRCV:
  assumes "boxed_b P s b bv b' s'" (*and "supp s = {}"*) and "⊨_wf P"
  shows "wfRCV P s b[bv::=b']_bb ∧ wfRCV P s' b"
  using assms proof(induct rule: boxed_b.inducts)
  case (boxed_b_BVar1I bv bv' P s b )
  then show ?case using wfRCV.intros by auto
next
  case (boxed_b_BVar2I bv bv' P s )
  then show ?case using wfRCV.intros by auto
next
  case (boxed_b_BPairI P s1 b1 bv b s1' s2 b2 s2')
  then show ?case using wfRCV.intros rcl_val.supp by simp
next
  case (boxed_b_BConsI tyid dclist P dc x b c s1 bv b' s1')
  hence "supp b = {}" using wfTh_supp_b by metis
  hence "b [ bv ::= b' ]_bb = b" using fresh_def subst_b_b_def forget_subst[of "bv" b b'] by auto
  hence " P ⊨
  moreover have "P ⊨ SCons tyid dc s1' : B_id tyid" using boxed_b_BConsI
    using wfRCV.intros rcl_val.supp subst_bb.simps boxed_b_BConsI by metis
  ultimately show ?case using subst_bb.simps by whe
next
  case (boxed_b_BConspI tyid bva dclist P b1 bv b' s1 s1' dc x b c)

  obtain bva2 and dclist2 where *:"AF_typedef_poly tyid bva dclist = AF_typedef_poly tyid bva2 dclist2 ∧
             atom bva2 ♯ (bv,(P, SConsp tyid dc b1[bv::=b']_bb s1, B_app tyid b1[bv::=b']_b "ewf\<(false
    using obtain_fresh_bv by metis

  then obtai x2 b2 and c2 where **:\c2 wh**:🚫
    using boxed_b_BConspI td_lookup_eq_iff type_def.eq_iff by metis

  have "P ⊨ SConsp tyid dc b1[bv::=b']_bb s1 : (B_app tyid b1[bv::=b']_bb)" proof
    show 1: ‹AF_typedef_poly tyid bva2 dclist2 ∈ set P› using boxed_b_BConspI * by auto
    show 2: ‹

    hence "atom bv ♯ b2" proof -
      have "supp b2 ⊆ { atom bva2 }" using wfTh_poly_supp_b 1 2 boxed_b_BConspI by auto
      moreover have "bv \noteq bva2" using * " using * fresh_P fresh_at_base by met
      ultimately show ?thesis using fresh_def by force
    qed
    moreover "b[bva::=b1]\>^sub>>b = b2[bva2::=b]\<^\^
    ultimately show ‹ P ⊨ s1 : b2[bva2::=b1[bv::=b']_bb]_bb› using boxed_b_BConspI subst_b_b_def subst_bb_commute by auto
    show "atom bva2 ♯ (P, SConsp tyid dc b1[bv::=b']_bb s1, B_app tyid b1[bv::=b']_bb)" using * fresh_Pair by metis
java.lang.StringIndexOutOfBoundsException: Index 5 out of bounds for length 5

  moreover have "P ⊨ SConsp tyid dc b1 s1' : B_app tyid b1" proof
    show ‹AF_typedef_poly
    show ‹
    show ‹
    have "atom bva ♯ P" using boxed_b_BConspI wfTh_fresh assumes "j = <> \longleftrightarrow>is_constant y"
    thus "atom bva ♯ (P, SConsp t shows "combine mk_and (x, i) (y, j) =(z,k)\Longrightarrow (k = \= ∞
  qed

  ultimately show ?case using subst_bb.simps by simp
qed(auto)+

lemma subst_b_var:
  assumes "B_var bv2 = b[bv::=b']_bb"
  shows "(b = B_var bv ∧ b' = B_var bv2) ∨ (b=B_var bv2 ∧ bv ≠and "combine mk_unt (x i) (y,= (z, k) ==> is_constant z)"
  using assms by(nominal_induct b rule: b.strong_induct,auto+)

text ‹mk_release (x, ) (y, j) = (z, k) ==> isz)"
The next lemma for a clearer explanation of what this is. i produces values of sort b[bv::=b'] and i' produces values of sort b›

inductive boxed_i :: "Θ ==> Γ ==> b ==> bv ==> valuation ==> valuation ==> bool" ( ‹ _ ; _ ; _ , _ ⊨ _ ≈ _› [50,50] 50) where
  boxed_i_GNilI: "Θ ; GNil ; b , bv ⊨ i ≈ i"
| boxed_i_GConsI: "[,i) (y, j = z, z, k) \Longrightarrow (k = <i \<longleftrightarrow 
equivariance boxed_i
nominal_inductive boxed_i .

inductive_cases boxed_i_elims:
  "Θ ;GNil ; b , bv ⊨ i ≈ i'"
  "Θ ; ((x,b,c)#_\<Gamma>Γ:

lemma wfRCV_poly_elims:
  fixes tm::"'a::fs" and b::b
  assumes "T ⊨ SConsp typid dc bdc s : b"
  obtains bva dclist x1 b1 c1 where "b = B_app typid bdc ∧
    AF_typedef_poly typid bva dclist ∈ set T ∧ "w ⊨> i) (\psi>, j)) ⟷w \<Turnstile\<sub> to_ (<psi, j)"
  using assms proof(nominal_induct "SConsp typid dc bdc s" b avoiding: tm rule:wfRCV.strong_induct)
  case (wfRCV_BConsPI bv dclist Θ x b c)
  then show ?case by simp
qed

lemma boxed_b_e
  assumes "wfRCV T s b[bv::=b']_bb" and "wfTh T"
  shows "∃ is_constant_ons assms),
  using assms proof(nominal_induct s arbitrary: b rule: rcl_val.strong_induct)
  case (SBitvec x)
  have *:"b[bv::=b']_bb = B_bitvec" using wfRCV_elims(9)[OF SBitvec(1)] by metis
  show ?case proof (cases "b = B_var bv")
    case True
    moreover have "T ⊨ SBitvec x : B_bitvec" using wfRCV.intros by simp
    moreover hence "b' = B_bitvec" using True SBitvec subst_bb.simps * by simp
    ultimately show ?thesis using boxed_b.intros wfRCV.intros by metis
  next
    case False
    hence "b = B_bitvec" using subst_bb_inject * by metis
    then show ?thesis using * SBitvec boxed_b.intros by metis
  qed
next
  case (SNum x)
  have *:"b[bv::=b']_i \infinity \\<ongleftrightarrow> is_ \<phi"
  show ?case proof (cases "b = B_var bv")
    case True
    moreover have "T ⊨ SNum x : B_int" using wfRCV.intros by simp
    moreover hence "b' = B_int" using True SNum subst_bb.simps(1) * by simp
    
  next
    case False
    hence "b = B_int" using subst_bb_inject(1) * by metis
    then show ?thesis using * SNum boxed_b_BIntI by metis
  qed
next
  case (SBool x)
  have *:"b[bv::=b']_bb = B_bool" using wfRCV_elims(11)[OF SBool(1)] by metis
  show ?case proof (cases "b = B_var bv")
    case True
    moreover have "T ⊨ SBool x : B_bool" using wfRCV.intros by simp
    moreover hence "b' = B_bool" using True SBool subst_bb.simps * by simp
    ultimately show ?thesis using boxed_b.intros wfRCV.intros by metis
xt
    case False
    hence "b = B_bool" using subst_bb_inject * by metis
    then show ?thesis using * SBool boxed_b.intros by metis
  qed
next
  case (SPair s1 s2)
  then obtain b1 and b2 where *:"b[bv::=b']_bb = B_pair b1 b2 ∧ wfRCV T(case \psi; simp add: assms,
  show ?case proof (cases "b = B_var bv")
    case True
    moreover have "T ⊨ SPair s1 s2 : B_pair b1 b2" using wfRCV.intros * by simp
    moreover hence "
    ultimately show ?thesis using boxed_b_BVar1I by metis
  next
    case False
    then obtain b1' and b2' where "  = B_pair b1' b2' ∧b b2=b2'[bv::=b']_b" using subst_bb_inject(5)[OF _ False ] * by metis
 then show ?thesis using * SPair boxed_b_BPairI by blast
 qed
 
 case (SCons tyid dc s1)
 have *:"b[bv::=b']_bb = B_id tyid" using wfRCV_elims(13)[OF SCons(2)] by metis
 how ?case proo (cases "b = Bb = B_var bv")
 case True
 moreover have "T ⊨ tyid" using wfRCV.intros
 using "local.*" SCons.prems by auto
 moreover hence "b' = B_id tyid" using True SCons subst_bb.simps(1) * by simp
 ultimately show ?thesis using boxed_b_BVar1I wfRCV.intros by metis
 next
 case False
 then obtain b1' where beq: "b = B_id tyid" using subst_bb_inject * by metis
 then obtain b2 dclist x c where **:"AF_typedef tyid dclist ∈ set T ∧ (dc, {snd(rritXenat φ) = ∞e_X_enaa \>))"
 then have "atom bv ♯
 then have "b2 = b c (A_ltln \> ψ
 then obtain s1' where s1: thus ?casejava.lang.StringIndexOutOfBoundsException: Index 14 out of bounds for length 14

 have "T ⊨ SCons tyid dc s1 ~ (B_id tyid) [ bv ::= b' ] ∖ SCons tyid dc s1'" proof(rule boxed_b_BConsI)
 show "AF_typedef tyid dclist ∈ set T" using ** by auto
 show "(dc, { x : b2 | c }) ∈ setlisusing ** by auto
 show "T ⊨

 qed
 thus ?thesis using beq by metis
 qed
 
 case (SConsp typid dc bdc s)

 obtain bva dclist x1 b1 c1 where **:"b[bv::=b'] ψ
 AF_typedef_poly typid bva dclist ∈
 using wfRCV_poly_elims[OF SConsp(2)] by metis

 then have *:"B_app typid bdc = b[bv::=b']_bb" using wfRCV_elims(1
 show ?case proof (cases "b = B_var bv")
 case True
 moreover have "T ⊨ SConsp typid dc bdc s : B_app typid bdc" using wfRCV.intros
 using "local.*" SConsp.prems(1) by auto
 moreover hence "b' = B_app typid bdc" using True SConsp s.simps * by simp
 ultimately show ?thesis using boxed_b.intros wfRCV.intros by metis
 next
 case False
 then obtain bdc' where bdc: "b = B_app typid bdc' ∧ bdc = bdc'[bv::=b'] \<> 
        (*hence beq:"b = B_app typid bdc" using subst_bb_inject *  sory (* going to be like the above as bdc is closed *)*)
    have "atom bv ♯ b1" proof -
      have "supp b1 ⊆)
      moreover have "bv ?case
      ultimatelysimp:split_def eSuc_infinity)
    qed      
    have java.lang.NullPointerException
    moreover have " "b1[bva::=bdc']_b[bv::=b'] b1[ba::=bdc]\\<^sub>b_atom bv ♯ b1› by auto
    ultimately obtain s' where s':"T  ⊨ sjava.lang.NullPointerException
      using SConsp(1)[of "b1[bva::=bdc']_bcase (And_ltln ψ
    have    thus
    proof - 

      obtain bva3 and dclist3 where 3:"AF_typedef_poly typid bva3 dclist3 = AF_typedef_poly typid bva dclist ∧)
            atom bva3 ♯ (bdc', bv, b', s, s')" using obtain_fresh_bv  by metis
      then obtain x3 b3
        ged_b_BConspIdef_
        by (metis "**")

      show ?thesis proof
        show>AF_typedef_poly typid bva3 dclist3 ∈ t T using 3 ** by metis 
        show ‹
        show 4:\<open>(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in> set dclist3\<close> using 4 by auto
        have "b3[bva3::=bdc']\<^sub>b\<^sub>b = b1[bva::=bdc']\<^sub>b\<^sub>b" proof(rule wfTh_typedef_poly_b_eq_iff)
          show \<open>AF_typedef_poly typid bva3 dclist3 \<in> set T\<close> using 3 ** by metis
          show \<open>(dc, \<lbrace> x3 : b3  | c3 \<rbrace>) \<in>   (Next_ltln \<phi>java.lang.StringIndexOutOfBoundsException: Index 25 out of bounds for length 25
          show \<open>AF_typedef_poly      by (simp : split_def; cases "snd (rewrite_X_enat \phi) <> <nfinity)
          show \<open>(dc, \<lbrace x1 : b1  |  \<rbrace>) \<> set dclist\<close> using ** by auto
        qed(simp add: ** SConsp(7) by blast
        thus  \<open> T  \<turnstile> s ~ b3[bva3::=bdc']\<^sub>b\<^sub>b [ bv ::= b' ] \<setminus> s' \<close> using s' by auto
      qed
    qed
    then show ?thesis using bdc by auto

  qed
next 
  case SUnit
  have *:"b[bv::=b']\<^sub>b\<^sub>b = B_unit" using wfRCV_elims SUnit by metis
  show ?case proof (cases "b = B_var bv")
    case True
    moreover have "T  \<turnstile> SUnit : B_unit" using wfRCV.intros by simp
    moreover hence "b' = B_unit" using True SUnit subst_bb.simps * by simp
    ultimately show ?thesis using boxed_b.intros  wfRCV.intros by metis
  next
    case False
    hence "b = B_unit" using subst_bb_inject *  by metis  
    then show ?thesis using * SUnit boxed_b.intros by metis
  qed
next
  case (SUt x) 
  then obtain bv' where *:"b[bv::=b']\<^subure_universalrueue^> = True"
  howaseeproof cases B_varrv
    case e
    then show ?thesis using  "pure_universalnu>U\<^sub>n \<nu>') =pure_universalniversalsal<> and> pure_universal \<nu>')"
      localfRCV_BVarIastforceorce
  next
    case False
    then show ?thesis using boxed_b_BVar1I  boxed_b_BVar2I
      using "local.*" wfRCV_BVarI    by (metis subst_b_var)
  qed
qed

lemma boxed_i_ex:
  assumes <ammabv::=b]\<^sub>\<Gamma>\<^sub>b i" and "wfTh T"
  shows  <>i'. T ; \<Gamma> ; b , bv \<turnstile> i \approxi'"
  using assms proof(induct <>arbitrary: i rule:\<Gamma>_induct)
  case GNil
  then show ?case using boxed_i_GNilI by metis
next
  case (GCons x' b' c' \<Gamma>')
  then obtain s where 1me  x\and wfRCV T s b'[bv::=b]\<^sub>b\<subb" usinggwfI_def_fubst_gb y auto
  then obtain lemma pure_eventual_left_append
  then obtain i' where 3: "boxed_i T \<Gamma>' b bv i  i'singonsfI_defbst_gbt_gbbsimps yforcee
  have "boxed_i T ((x', b', c') #\<^sub>\<Gamma> \<Gamma>') b bv i  (i'(x' \<mapsto> s'))" proof
    show "Some s = i x'" using 1 by auto
    show "boxed_b T s b'by simp(metisuffix_conc_lengthnc_lengthix_suffix
show "; \<Gamma' ; b , bv \<turnstile> i \<pproxsing""yo
  qed
  thus ?case by auto
qed

_eq:
  assumes "boxed_b \<Theta> s1 b bv b' s1'" and "\<turnstile>\<^sub>w\<^sub>f \<Theta>"
  shows "wfTh \<Theta> \<Longrightarrow> boxed_b \<Theta> s2 b bv b' s2' \<Longrightarrow> ( s1 = s2 ) = ( s1' = s2' )"
  using assms proof(induct : 2s2 e boxed_b_nducts)
  case (boxed_b_BVar1I bv bv'  P s b )  
  then
    using boxed_b_elims(1) rcl_val.eq_iff by is
next
  case (boxed_b_BVar2I bv bv' P s b)
  then show ?case using boxed_b_elims(1) by metis
next
  case (boxed_b_BIntI P s uu uv)
  hence "s2 = s2'" using boxed_b_elims by metis
  then show ?case byuto
next
  boxed_b_BBoolIux)
ce singelimsy
  then show ?case by auto
next
  case (boxed_b_BUnitI P s uy uz)
  encece"2=s2"  xed_b_elimstis
  then show ?case by auto
next

  then show ?case
    by (metis boxed_b_elims(5) rcl_val.eq_iff(4))
next
  case (boxed_b_BConsIclist P b s1  bs1java.lang.StringIndexOutOfBoundsException: Index 59 out of bounds for length 59
  obtain s22 and s22' dclist2 dc2 x2 b2 c2 where *:"s2 = SCons tyid dc2 s22 \<and> s2' = SCons tyid dc2 s22' \<and> boxed_b P s22 b2 bvthus ase
       AF_typedef tyid dclist2 \<in> set P \<and> (2, lbrace x2 : b2  | c2 \<rbrace>) \<in> set dclist2 using ed_b_elimselims[Fxed_b_BConsIbymetis
  show ?case proof(cases "dc = dc2")
    case True
    hence "b = b2"  using wfTh_ctor_unique \<tau>.eq_iff wfTh_dclist_unique wf boxed_b_BConsI * by metis
    then show ?thesis using boxed_b_BConsI True * by auto
  next
    case False
    then show ?thesis using *boxed_b_BConsIbymp
  qed      
next
  case (boxed_b_Bbitvec P s bv b)
  hence "s2 = s2'" using boxed_b_elims by metis
  then show ?case by auto
next
  case (boxed_b_BConspI tyid bva dclist P
  obtain bva2 s22  s22' dclist2 dc2 x2 b2 c2 where *:"

     s2' = SConsp tyid dc2 b1 s22' \<and> 
     boxed_b P s22 b2[bva2
     AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc2, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2" using boxed_b_elims(8)[OF boxed_b_BConspI(7)] by metis
  show ?case proof(cases "dc = dc2")
    case True
    hence "AF_typedef_poly tyid bva2 dclist2 \<in> set P \<and> (dc, \<lbrace> x2 : b2  | c2 \<rbrace>) \<in> set dclist2" using * bye
    hence "b[bva::=b1]\<^sub>b\<^sub>b = b2[bva2::=b1]\<^sub>b\<^sub>b"  using wfTh_typedef_poly_b_eq_iff[OF boxed_b_BConspI(1) boxed_b_BConspI(3)] * boxed_b_BConspI by metis
    then show ?thesis using boxed_b_BConspI True * by auto
  next
    case False
    then show ?thesis using * boxed_b_BConspI by simp
  qed    
qed

lemmahence"<xi>' = rue^subn" and "pure_universal \<xi>"
  java.lang.StringIndexOutOfBoundsException: Index 20 out of bounds for length 20
  shows "Some (b,c) = lookup \<Gamma> x \<Longrightarrow> Some s = i x \<Longrightarrow> Some s' = i' x \<Longrightarrow> boxed_b \<Theta> s b bv b' s'"
  using assms proof(induct rule: boxed_i.inducts)
  case (boxed_i_GNilI T i)
  then show ?case using lookup.simps by auto
next
  case (boxed_i_GConsI s i x1 \<Theta> b1 bv b' s'  \<Gamma> i' c)
  show ?case proof (cases "x=x1
    case True
    then show ?thesis using boxed_i_GConsI
        fun_upd_same lookup.simps(2) option.inject prod.inject by metis
  next
    case False
    then show ?thesis using boxed_i_GConsI
        fun_upd_same lookup.simps option.inject prod.inject by auto
  qed
qed

lemma eval_l_boxed_b:
  es<lbrakk> l <brakk> = s"
  shows   "boxed_b \<Theta> s (base_for_lit l) bv b' s"
  using assms proof(nominal_induct l arbitrary: s  rule:l.strong_induct)
qed(auto simp add:  boxed_b.intros wfRCV.intros )+

lemma boxed_i_eval_v_boxed_b:
  fixes v::v
  assumessumesmess"boxed_i \<Theta>\<Gamma> b' bv i i'" and "i \<> vbv::=b']\<^sub>v\<^sub>b \rbrakk   s nd   i\<lbrakk v \<rbrakk> ~s ndV<>  \Gamma v b"  and "wfI \<Theta>  \<Gamma> i'"
  shows "boxed_b \<Theta> s b   s
  using assms proofnominal_inductl_inductuctarbitraryitraryrarys'rulevrong_induct
  asetl
  hence "\<lbrakk> l \<rbrakk> = s \<and> \<lbrakk> l \<rbrakk> = s'" using eval_v_elims by auto
  moreover have "b = base_for_lit l" using wfV_elims(2) V_lit  by metis
  ultimately show ?case using V_lit using  eval_l_boxed_b subst_b_base_for_lit by metis
next
  case (V_var x)   (* look at defn of bs_boxed *)
  hence Some
  moreover_n ψ
  ultimately show ?case using bs_boxed_var V_var by metis

next
  case (V_pair v1 v2)
  then obtain b1 and b2 where b:"b=B_pair b1 b2" using wfV_elims subst_vb.simps  by metisbyforce
  obtain s1 and s2 where s: java.lang.NullPointerException
  obtain s1' and s2' where s': "eval_v i' v1 \and eval_v i' v2 s2' ∧
  have  "boxed_b Θv b' (SPair s1s') "ofirI
    show"xed_b\Theta s1 b1 b1 bv b' s1'" using V_pair eval_v_elims wfV_elims b s s' b.eq_iff by metis
 owbTheta s2 b2usingimsss'eq_iff
  qed
  then show ?case using s s' b by autoite_modal> R_>∨ then rewrite_modal <psielseite_modalphiR_n rewrite_modal ψ))"
next
  case (V_cs tyi dv1)

  obtain dclist x b1 c where *: "b = B_id tyid
ing
btain 2\>i [v ingps metis
  obtain s2' where s2e
  have sp: "supp { x : b1 | c } = {}" using wfTh_lookup_supp_empty * wfX_wfYuntil_simp] suspendable_formula_simp])

  have "boxed_b Θ (SCons tyid dc s2) (B_id tyid) bv b' (SCons tyid dc s2')"
  proof(rule boxed_b_BConsI)
    show 1:"AF_typedef tyid dclist ∈v< ∨ suspendable ψ")
    show 2:"(dc, { x : b1 | c } set dclist" using * by auto
    have bvf:"atom bv ♯
    show "Θ  ⊨ s2 ~ b1 [ bv :case ψ
  qed
  then show ?case using * s2 s2' by simp
next
  case (V_consp tyid dc b1 v1)

  obtain bv2 dclist x2 b2 c2 where *: "b = B_app tyid b1 ∧
java.lang.NullPointerException
    using wf_strong_elim(1)[OF V_consp (5)] by metis

  obtain s2 where s2: "s = SConsp tyidapplyjava.lang.StringIndexOutOfBoundsException: Index 22 out of bounds for length 22
    using eval_v_elims V_consp subst_vb.simps by metis

  obtain s2' where s2': "s' = SConsp tyid dc b1 s2' ∧ i' [ v1 ] ~ s2'" 
    using

  have "⊨Syntactical Implication Based Simplification›
  then obtain bv3::bv and dclist3 x3 b3 c3 where **:" AF_typedef_poly tyid bv2 dclistv3
        (dc, { x3 : b3  | c3 }) ∈   "<>\^>s true_n"
    using * obtain_fresh_bv_dclist_b_iff1,s2

  have "boxed_b Θ (SConsp tyid dc b1[bv::=b'] ⊨s χ (φn ψ) \<urnstile<
  proof(rule boxdbBCospI[of[off tyid b3dcisst3 3\Theta, where x=x3 and b=b3 and c=c3])
    show 1:"AF_typedef_poly tyid bv3 dclist3 ∈_\<^sub>s (\psior_n χ)"
    show 2:"(c\>x3 : b3  | c3 }) ∈ set dclist3" using ** by auto
    show amb3\>(b1, bv, b', s2, s2')" using ** by auto  
    show " Θ ⊨ ⊨s χ φ_n χ
  qed
  then show ?case using * s2 s2' by simp
qed

lemma boxe__e_q
  assumes "boxed_b Θ ⊨s <\<)"
    "s' = SBool (n1 "φ<turnstile> ==> ⊨s ν (φn ψ_n ν)"
  shows  "s=s'" 
  using boxed_b_eq assms by auto

lemma boxed_i_eval_ce_boxed_b:
  fixesjava.lang.StringIndexOutOfBoundsException: Index 13 out of bounds for length 13
  assumes "i' [_\<^sub>n φ ==> w ⊨n ψ"
  shows "boxed_b Θ s b bv b' s'"
  using assms proof(nominal_induct e arbitrary: s s' b b' rule: ce.strong_induct)
  case (CE_val
  then showrewrite_syn_imp
next
  case (CE_op opp v1 v2)

  show ?case proof(rule opp.exhaust)
    assume ‹n
    have 1:"wfCE \<Theta> B \<Gamma> v1 (B_int)" using wfCE_elims CE_op  \<open>opp = Plus\<close>  by metis
    have 2:"wfCE \<Theta> B \<Gamma> v2 (B_int)" using wfCE_elims CE_op  \<open>opp = Plus\<close> by metis
    have *:"b = B_int" using CE_op wfCE_elims 
 (metis \<open>opp = plus\<close>)

    obtain n1 and n2 where n:"s = SNum (n1 + n2) \<and> i \<lbrakk> v1[mk_orwrite_syn_impphi) (rewrite_syn_imp \<psi>))"
    obtain n1' and n2' where n:"'um1' '\< i' \<lbrakk> v1 \<rbrakk> ~ SNum n1' \<and> i' \<lbrakk> v2<rbrakk> ~ Num' singval_e_elimsop\openopp = plus\<close> by metis

    have "boxed_b \<Theta> (SNum n1) B_int bv b' (SNum n1')" using boxed_i_eval_v_boxed_b 1 2 n n' CE_op \<open>opp = plus\<close> by metis
    moreover have "boxed_b \<Theta> (SNum n2) B_int bv b' (SNum n2')" using boxed_i_eval_v_boxed_b 1 2 n n' CE_op by metis
    ultimately have "s=s'" using n' n boxed_b_elims(2)
      by (metis rcl_val.eq_iff(2))
    thus ?thesis using  * n n' boxed_b_BIntI CE_op wfRCV.intros Plus by simp
  next
    assume \<open>opp = LEq\<close>
    have 1:"wfCE \<Theta> B \<Gamma> v1 (B_int)" using wfCE_elims CE_op  \<open>opp = LEq\<close>  by metis
    have 2"wfCETheta B \<Gamma> v2 (B_int)"glimsopopenopp = LEq\<close> by metis
    hence *:"b = B_bool" using CE_op wfCE_elims \<open>opp = LEq\<close>   by metis
    obtain n1 and n2 where n:"s = SBool (n1 \<le> n2) \<and> i \<lbrakk> v1[bv::=b']\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ SNum n1 \<moreover
    obtain n1' and n2' where n':"s' = SBool (n1' \<le> n2') \<and> i

    have "boxed_b \<Theta> (SNum n1) B_int bv b' (SNum n1')" using boxed_i_eval_v_boxed_b 1 2 n n' CE_op by metis
    moreover have "boxed_b \<Theta> (SNum n2) B_int bv b' (SNum n2')" using boxed_i_eval_v_boxed_b 1 2 n n' CE_op by metis
    ultimately have "s=s'" using n' n boxed_b_elims(2)
      by (metis rcl_val.eq_iff(2))
    thus ?thesis using  * n n' boxed_b_BBoolI CE_op wfRCV
  next
    assume \<open>opp = Eq\<close>
    obtain b1 where b1:"wfCE \<Theta> B \<Gamma> v1 b1 \<and> wfCE \<Theta> B \<Gamma> v2 b1" using wfCE_elims CE_op  \<open>opp = Eq\<close>  by metis

     B_boolE_opE_elimsims<>p\>   by metis
    obtain n1 and n2 where n:"s = SBool (n1 = n2) \<and> i \<lbrakk> v1[bv::=b']\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ n1 \<and> i \<lbrakk> v2[bv::=b']\<^sub>c\<^sub>e\<^sub>b \<define whereere <equivsuffix i w \<Turnstile>\<^sub psi"
    obtain n1' and n2' where n':"s' = SBool (n1' = n2') \<and> i' \<lbrakk> v1 \<rbrakk> ~ n1' \<and> i' \<lbrakk> v2 \<rbrakk> ~ n2'" using eval_e_elims CE_op \<open>opp = Eq\<close>  by metis

    have "boxed_b \<Theta> n1 b1 bv b' n1'" using boxed_i_eval_v_boxed_b b1  n n' CE_op by metis
    moreover haveed_b<Theta> n2 b1 bv b' n2'" using boxed_i_eval_v_boxed_b1  CE_opetis
    moreover have "\<turnstile>\<^sub>w\<^sub>f \<Theta>" using b1 wfX_wfY  ewrite_iter_slow<> equiv>iterate (rewrite_syn_imp o rewrite_modal o rewrite_X) \<phi> (size \<phi>)"
    ultimately have "s=s'" using n' n boxed_b_elims
        boxed_b_eq_eq
    thus ?thesis using  * n n' boxed_b_BBoolI CE_op wfRCV.intros \<open>opp = Eq\<close> by simp
  qed

next
  case (CE_concat v1 v2)

  obtain bv1 and bv2 where s :    st
    using eval_e_elims(7) subst_ceb.simps CE_concat.prems(2) eval_e_elims(6) subst_ceb.simps(6) by metis
  obtain bv1' and bv2' where s' : "s' = SBitvec (bv1' @ bv2') \<and> i' \<lbrakk> v1 \<rbrakk> ~ SBitvec bv1'  \<and> usingiterate_soundsyn_impp ewrite_modal_]
    using eval_e_elims<hi>) \<subseteq> atoms_ltln \<phi>"

  then show ?case ingged_i_eval_v_boxed_b_ims'E_concatcat
    toms_ltln<phi>  <subseteq> atoms_ltln \<phi>"
next
  case (CE_fst ce)
  obtain  s2 where 1:"i \<lbrakk> ce[bv::=b']\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ SPair s s2" using CE_fst eval_e_elims subst_ceb.simps byduction\>to
  obtain  s2' where 2:"i' \<lbrakk> ce \<rbrakk> ~ SPair s' s2'" using CE_fst eval_e_elims by metis
  obtain b2 where 3:"lemma move_strong_ops_atoms

  have "boxed_b \<Theta> (SPair s s2)
    using 1 tln(emove_weak_ops<>)\>atoms_ltln \<phi>"
  thus ?case using boxed_b_elims(5) by force
next
  case (CE_snd v)
  obtain s1  where 1:"i \<lbrakk> v[bv::=b']\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ SPair s1 s" using CE_snd eval_e_elims subst_cebsubseteq atoms_ltln \<phi>"
  obtain s1' where 2:"i' lemma mk_release_atoms
  obtain b1 where 3:"wfCE \<Theta> B \<Gamma> v (B_pair b1 b )" using wfCE_elims(5) CE_snd by metis

  have "boxed_b \<Theta> (SPair s1 s ) (B_pair b1 b ) bv b' (SPair s1' s')" using 1 2 3 CE_snd boxed_i_eval_v_boxed_b by simp
  thus ?case using boxed_b_elims(5) by force
next
  case (CE_len v)
  obtains1e s:\lbrakk v[bv::=b']\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ SBitvec s1singE_leneval_e_elimselimsbst_cebebmpss is
  obtain s1'assumes

  have "\<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : B_bitvec \<and> b = B_int"  using wfCE_elims CE_len by metis
  then show ?case using boxed_i_eval_v_boxed_b s s' CE_len combine_atomsOFmk_until_atomsl_atomsmsjava.lang.StringIndexOutOfBoundsException: Index 34 out of bounds for length 34
    by (metis boxed_b_BIntI boxed_b_elims rewrite_X_enat_atoms:
qed

lemma eval_c_eq_bs_boxed:
  fixes c::c
  assumes<c[bv::=b]\<^sub>^> \<rbrakk> ~ s" and "i' \<lbrakk> c \<rbrakk> ~ s'" and "wfC   c" "fI \<Gammaand<>; \<Gamma>[bv::=b<sub>\<Gamma>\<^sub>b  \<turnstile> i "
    and "boxed_i \<Theta> \<Gamma> b bv i i'"
  shows "s = s'"
  using assms proof(nominal_induct c arbitrary: s s'  rule:c.strong_induct)
lemma rewrite_iter_fast_atoms
  then show ?case using eval_c_elims subst_cb.simps by metis
next
  case C_false
  then show ?case using eval_c_elims  subst_cb.simps by metis
next
  case(_onj 1c2
  obtain s1 and s2 where 1: "eval_c i (c1[bv::=b]\<^sub>c\<^subhave1<And>\<phi>. atoms_ltln (rewrite_syn_imp (rewrite_modal (rewrite_X \<phi>))) \<subseteq> atoms_ltln"
  obtain s1' and s2' where 2:"eval_c i' c1 s1' \<and> eval_c i' c2 s2' \<and> s' = (s1'<>s2')" using_j_lims etis
  then show ?case using 1 2 wfC_elims C_conj by metis
next
  case (C_disj c1 c2)

  obtain s1 and s2 where 1: "eval_c i (c1[bv::=b]\<^sub>c\<^sub>b) s1 \<and> eval_c i (c2[bv::=b]\"\Turnstile\<^sub>n simplify m \<phi> \<longleftrightarrow> w \<^n \<phi>"
  obtain s1' and s2' where 2:"eval_c i' c1 s1' \<and> eval_c i' c2 s2' \<and> s' = (s1'\<or>s2')" using C_disj eval_c_elims(4) by metis
  then show ?case using 1 2 wfC_elims C_disj by metis
next
  case (C_not c)
  obtain s1::bool  where 1: "(i \<lbrakk> c[bv::]<subc\<^sub>b \<rbrakk> ~ s1) \<and> (s = (\<not> s1))" using  C_not eval_c_elims(6subst_cbt_cbbsimps)bytis
  obtain s1'::bool where 2: "(i' \<lbrakk> c \<rbrakk> ~ s1') \<and> (s' = (\<not> s1'))" using C_not eval_c_elims(6) by metis
  then show ?case using 1 2 wfC_elims C_not by metis
next
  case (C_imp c1 c2)
  obtain s1 and s2 where 1: "eval_c i (c1[bv::=b]\<^sub>c\<^sub>b) s1 \<and> eval_c i (c2[bv::=b]\<^sub>c\<^sub>b) s2 \<and> s = (s1 \<longrightarrow> s2)" using C_imp eval_c_elims(5) subst_cb.simps(5) by metis
  obtain s1' and s2' where 2:"eval_c i' c1 s1' \<and> eval_c i' c2 s2' \<and> s' = (s1' \<longrightarrow> s2')" using C_imp eval_c_elims(5) by metis
  then show ?case using 1 2 wfC_elims C_imp by metis
next
  case (C_eq e1 e2)
  obtain be where be: "wfCE \<Theta> B \<Gamma> e1 be \<and> wfCE \<Theta> B \<Gamma> e2 be" using C_eq wfC_elims by metis
  obtain s1 and s2 where 1: "eval_e i (e1[bv::=b]\<^sub>c\<^sub>e\<^sub>b) s1 \<and> eval_e i (e2[bv::=b]\<^sub>c\<^sub>e\<^sub>b) s2 \<and> s = (s1 = s2)" using C_eq eval_c_elims(7) subst_cb.simps(6) by metis
  obtain s1' and s2' where 2:"eval_e i' e1 s1' \<and> eval_e i' e2 s2' \<and> s' = (s1' = s2' )" using C_eq eval_c_elims(7) by metis
  have "\<turnstile>\<^sub>w\<^sub>f \<Theta>" using C_eq wfX_wfY by metis
  moreover have "\<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b  \<turnstile> i " using C_eq by auto
  ultimately show ?case using boxed_b_eq[of \<Theta> s1 be bv b s1' s2 s2'] 1 2 boxed_i_eval_ce_boxed_b  C_eq wfC_elims subst_cb.simps 1 2 be by auto
qed

lemma is_satis_bs_boxed:
  fixes c::c
  assumes  "boxed_i \<Theta> \<Gamma> b bv i i'" and "wfC \<Theta> B \<Gamma> c" and "wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "\<Theta> ; \<Gamma> \<turnstile> i'"
    and  "(i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b)"
  shows "(i' \<Turnstile> c)"
proof -
  have "eval_c i (c[bv::=b]\<^sub>c\<^sub>b) True" using is_satis.simps assms by auto
  moreover obtain s where "i' \<lbrakk> c \<rbrakk> ~ s" using eval_c_exist assms by metis
  ultimately show ?thesis using eval_c_eq_bs_boxed assms is_satis.simps by metis
qed

lemma is_satis_bs_boxed_rev:
  fixes c::c
  assumes  "boxed_i \<Theta> \<Gamma> b bv i i'" and "wfC \<Theta> B \<Gamma> c" and "wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "\<Theta> ; \<Gamma> \<turnstile> i'" and  "wfC \<Theta> {||} \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b (c[bv::=b]\<^sub>c\<^sub>b)"
    and  "(i' \<Turnstile> c)"
  shows "(i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b)"
proof -
  have "eval_c i' c True" using is_satis.simps assms by auto
  moreover obtain s where "i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s" using eval_c_exist assms by metis
  ultimately show ?thesis using eval_c_eq_bs_boxed assms is_satis.simps by metis
qed

lemma bs_boxed_wfi_aux:
  fixes b::b and bv::bv and \<Theta>::\<Theta> and B::\<B>
  assumes   "boxed_i \<Theta> \<Gamma> b bv i i'" and "wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "\<turnstile>\<^sub>w\<^sub>f \<Theta>" and "wfG \<Theta> B  \<Gamma>"
  shows "\<Theta> ; \<Gamma> \<turnstile> i'"
  using assms proof(induct rule: boxed_i.inducts)
  case (boxed_i_GNilI T i)
  then show ?case using wfI_def by auto
next
  case (boxed_i_GConsI s i x1 T b1 bv b s' G i' c1)
  {
    fix x2 b2 c2
    assume as : "(x2,b2,c2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)"

    then consider (hd) "(x2,b2,c2) = (x1, b1, c1)" | (tail) "(x2,b2,c2) \<in> toSet G" using toSet.simps by auto
    hence "\<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and> wfRCV T s b2" proof(cases)
      case hd
      hence "b1=b2" by auto
      moreover have "(x2,b2[bv::=b]\<^sub>b\<^sub>b,c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)[bv::=b]\<^sub>\<Gamma>\<^sub>b"  using hd subst_gb.simps by simp
      moreover hence "wfRCV T s b2[bv::=b]\<^sub>b\<^sub>b" using wfI_def boxed_i_GConsI hd
      proof -
        obtain ss :: "b \<Rightarrow> x \<Rightarrow> (x \<Rightarrow> rcl_val option) \<Rightarrow> type_def list \<Rightarrow> rcl_val" where
          "\<forall>x1a x2a x3 x4. (\<exists>v5. Some v5 = x3 x2a \<and> wfRCV x4 v5 x1a) = (Some (ss x1a x2a x3 x4) = x3 x2a \<and> wfRCV x4 (ss x1a x2a x3 x4) x1a)"
          by moura (* 0.0 ms *)
        then have f1: "Some (ss b2[bv::=b]_bb x1 i T) = i x1 ∧ wfRCV T (ss b2[bv::=b]_bb x1 i T) b2[bv::=b]_bb"
          using boxed_i_GConsI.prems(1) hd wfI_def by auto (* 31 ms *)
        then have "ss b2[bv::=b]_bb x1 i T = s"
          by (metis (no_types) boxed_i_GConsI.hyps(1) option.inject) (* 0.0 ms *)
        then show ?thesis
          using f1 by blast (* 0.0 ms *)
      qed
      ultimately have "wfRCV T s' b2" using boxed_i_GConsI boxed_b_wfRCV by metis

      then show ?thesis using hd by simp
    next
      case tail
      hence "wfI T G i'" using boxed_i_GConsI wfI_suffix wfG_suffix subst_gb.simps
        by (metis (no_types, lifting) Un_iff toSet.simps(2) wfG_cons2 wfI_def)
      then show ?thesis using wfI_def[of T G i'] tail
        using boxed_i_GConsI.prems(3) split_G wfG_cons_fresh2 by fastforce
    qed
  }
  thus ?case using wfI_def by fast

qed

lemma is_satis_g_bs_boxed_aux:
  fixes G::Γ
  assumes  "boxed_i Θ G1 b bv i i'" and "wfI Θ G1[bv::=b]_\<Gamma>_b i" and "wfI Θ G1 i'"  and "G1 = (G2@G)" and  "wfG Θ B G1"
    and "(i ⊨ G[bv::=b]_\<Gamma>_b) "
  shows  "(i' ⊨ G)"
  using assms proof(induct G arbitrary: G2 rule: Γ_induct)
  case GNil
  then show ?case by auto
next
  case (GCons x' b' c' Γ' G2)
  show ?case proof(subst is_satis_g.simps,rule)
    have *:"wfC Θ B G1 c'" using GCons wfG_wfC_inside by force
    show "i' ⊨ c'" using is_satis_bs_boxed[OF assms(1) * ] GCons by auto
    obtain G3 where "G1 = G3 @ Γ'" using GCons append_g.simps
      by (metis append_g_assoc)
    then show "i' ⊨ Γ'" using GCons append_g.simps by simp
  qed
qed

lemma is_satis_g_bs_boxed:
  fixes G::Γ
  assumes  "boxed_i Θ G b bv i i'" and "wfI Θ G[bv::=b]_\<Gamma>_b i" and "wfI Θ G i'"  and "wfG Θ B G"
    and "(i ⊨ G[bv::=b]_\<Gamma>_b) "
  shows  "(i' ⊨ G)"
  using is_satis_g_bs_boxed_aux assms
  by (metis (full_types) append_g.simps(1))

lemma subst_b_valid:
  fixes s::s and b::b
  assumes "Θ ; {||} ⊨_wf b"  and "B = {|bv|}" and "Θ ; {|bv|} ;Γ ⊨ c"
  shows "Θ ; {||} ; Γ[bv::=b]_\<Gamma>_b ⊨ c[bv::=b]_cb "
proof(rule validI)

  show **:"Θ ; {||} ; Γ[bv::=b]_\<Gamma>_b ⊨_wf c[bv::=b]_cb " using assms valid.simps wf_b_subst subst_gb.simps by metis
  show "∀i. (wfI Θ Γ[bv::=b]_\<Gamma>_b i ∧ i ⊨ Γ[bv::=b]_\<Gamma>_b) ⟶ i ⊨ c[bv::=b]_cb "
  proof(rule,rule)
    fix i
    assume *:"wfI Θ Γ[bv::=b]_\<Gamma>_b i ∧ i ⊨ Γ[bv::=b]_\<Gamma>_b"

    obtain i' where idash: "boxed_i Θ Γ b bv i i'" using boxed_i_ex wfX_wfY assms * by fastforce

    have wfc: "Θ ; {|bv|} ; Γ ⊨_wf c" using valid.simps assms by simp
    have wfg: "Θ ; {|bv|} ⊨_wf Γ" using valid.simps wfX_wfY assms by metis
    hence wfi: "wfI Θ Γ i'" using idash * bs_boxed_wfi_aux subst_gb.simps wfX_wfY by metis
    moreover have "i' ⊨ Γ" proof (rule is_satis_g_bs_boxed[OF idash ] wfX_wfY(2)[OF wfc])
      show "wfI Θ Γ[bv::=b]_\<Gamma>_b i" using subst_gb.simps * by simp
      show "wfI Θ Γ i'" using wfi by auto
      show "Θ ; B ⊨_wf Γ " using wfg assms by auto
      show "i ⊨ Γ[bv::=b]_\<Gamma>_b" using subst_gb.simps * by simp
    qed
    ultimately have ic:"i' ⊨ c" using assms valid_def   using valid.simps by blast

    show  "i ⊨ c[bv::=b]_cb" proof(rule is_satis_bs_boxed_rev)
      show "Θ ; Γ ; b , bv ⊨ i ≈ i'" using idash by auto
      show "Θ ; B ; Γ ⊨_wf c " using wfc assms by auto
      show "Θ ; Γ[bv::=b]_\<Gamma>_b ⊨ i" using subst_gb.simps * by simp
      show "Θ ; Γ ⊨ i'" using wfi by auto
      show "Θ ; {||} ; Γ[bv::=b]_\<Gamma>_b ⊨_wf c[bv::=b]_cb " using ** by auto
      show "i' ⊨ c" using ic by auto
    qed

  qed
qed

section ‹Expression Operator Lemmas›

lemma is_satis_len_imp:
  assumes "i ⊨ (CE_val (V_var x) == CE_val (V_lit (L_num (int (length v)))) )" (is "is_satis i ?c1")
  shows "i ⊨ (CE_val (V_var x) == CE_len [V_lit (L_bitvec v)]^ce)"
proof -
  have *:"eval_c i ?c1 True" using assms is_satis.simps by blast
  then have  "eval_e i (CE_val (V_lit (L_num (int (length v))))) (SNum (int (length v)))"
    using eval_e_elims(1) eval_v_elims eval_l.simps  by (metis eval_e.intros(1) eval_v_litI)
  hence "eval_e i (CE_val (V_var x)) (SNum (int (length v)))" using eval_c_elims(7)[OF *]
    by (metis eval_e_elims(1) eval_v_elims(1))
  moreover have "eval_e i (CE_len [V_lit (L_bitvec v)]^ce) (SNum (int (length v)))"
    using eval_e_elims(7) eval_v_elims eval_l.simps  by (metis eval_e.intros eval_v_litI)
  ultimately show ?thesis using eval_c.intros is_satis.simps by fastforce
qed

lemma is_satis_plus_imp:
  assumes "i ⊨ (CE_val (V_var x) == CE_val (V_lit (L_num (n1+n2))))" (is "is_satis i ?c1")
  shows   "i ⊨ (CE_val (V_var x) == CE_op Plus ([V_lit (L_num n1)]^ce) ([V_lit (L_num n2)]^ce))"
proof -
  have *:"eval_c i ?c1 True" using assms is_satis.simps by blast
  then have  "eval_e i (CE_val (V_lit (L_num (n1+n2)))) (SNum (n1+n2))"
    using eval_e_elims(1) eval_v_elims eval_l.simps  by (metis eval_e.intros(1) eval_v_litI)
  hence "eval_e i (CE_val (V_var x)) (SNum (n1+n2))" using eval_c_elims(7)[OF *]
    by (metis eval_e_elims(1) eval_v_elims(1))
  moreover have "eval_e i (CE_op Plus ([V_lit (L_num n1)]^ce) ([V_lit (L_num n2)]^ce)) (SNum (n1+n2))"
    using eval_e_elims(7) eval_v_elims eval_l.simps  by (metis eval_e.intros eval_v_litI)
  ultimately show ?thesis using eval_c.intros is_satis.simps by fastforce
qed

lemma is_satis_leq_imp:
  assumes "i ⊨ (CE_val (V_var x) == CE_val (V_lit (if (n1 ≤ n2) then L_true else L_false)))" (is "is_satis i ?c1")
  shows   "i ⊨ (CE_val (V_var x) == CE_op LEq [(V_lit (L_num n1))]^ce [(V_lit (L_num n2))]^ce)"
proof -
  have *:"eval_c i ?c1 True" using assms is_satis.simps by blast
  then have  "eval_e i (CE_val (V_lit ((if (n1 ≤ n2) then L_true else L_false)))) (SBool (n1≤n2))"
    using eval_e_elims(1) eval_v_elims eval_l.simps
    by (metis (full_types) eval_e.intros(1) eval_v_litI)
  hence "eval_e i (CE_val (V_var x)) (SBool (n1≤n2))" using eval_c_elims(7)[OF *]
    by (metis eval_e_elims(1) eval_v_elims(1))
  moreover have "eval_e i (CE_op LEq [(V_lit (L_num n1))]^ce [(V_lit (L_num n2) )]^ce) (SBool (n1≤n2))"
    using eval_e_elims(3) eval_v_elims eval_l.simps  by (metis eval_e.intros eval_v_litI)
  ultimately show ?thesis using eval_c.intros is_satis.simps by fastforce
qed

lemma eval_lit_inj:
  fixes n1::l and n2::l
  assumes "[ n1 ] = s" and "[ n2 ] = s" 
  shows "n1=n2" 
  using assms proof(nominal_induct s rule: rcl_val.strong_induct)
  case (SBitvec x)
  then show ?case using eval_l.simps 
    by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
next
  case (SNum x)
  then show ?case using eval_l.simps 
    by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
next
  case (SBool x)
  then show ?case using eval_l.simps 
    by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
next
  case (SPair x1a x2a)
  then show ?case using eval_l.simps 
    by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
next
  case (SCons x1a x2a x3a)
  then show ?case using eval_l.simps 
    by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
next
  case (SConsp x1a x2a x3a x4)
  then show ?case using eval_l.simps 
    by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
next
  case SUnit
  then show ?case using eval_l.simps 
    by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
next
  case (SUt x)
  then show ?case using eval_l.simps 
    by (metis l.strong_exhaust rcl_val.distinct rcl_val.eq_iff)
qed

lemma eval_e_lit_inj:
  fixes n1::l and n2::l
  assumes "i [ [ [ n1 ]^v ]^ce ] ~ s" and "i [ [ [ n2 ]^v ]^ce ] ~ s" 
  shows "n1=n2" 
  using eval_lit_inj assms eval_e_elims eval_v_elims by metis

lemma is_satis_eq_imp:
  assumes "i ⊨ (CE_val (V_var x) == CE_val (V_lit (if (n1 = n2) then L_true else L_false)))" (is "is_satis i ?c1")
  shows   "i ⊨ (CE_val (V_var x) == CE_op Eq [(V_lit (n1))]^ce [(V_lit (n2))]^ce)"
proof -
  have *:"eval_c i ?c1 True" using assms is_satis.simps by blast
  then have  "eval_e i (CE_val (V_lit ((if (n1=n2) then L_true else L_false)))) (SBool (n1=n2))"
    using eval_e_elims(1) eval_v_elims eval_l.simps
    by (metis (full_types) eval_e.intros(1) eval_v_litI)
  hence "eval_e i (CE_val (V_var x)) (SBool (n1=n2))" using eval_c_elims(7)[OF *]
    by (metis eval_e_elims(1) eval_v_elims(1))
  moreover have "eval_e i (CE_op Eq [(V_lit (n1))]^ce [(V_lit (n2) )]^ce) (SBool (n1=n2))"
  proof -
    obtain s1 and s2 where *:"i [ [ [ n1 ]^v ]^ce ] ~ s1 ∧ i [ [ [ n2 ]^v ]^ce ] ~ s2" using eval_l.simps eval_e.intros eval_v_litI by metis
    moreover have " SBool (n1 = n2) = SBool (s1 = s2)" proof(cases "n1=n2")
      case True
      then show ?thesis using * 
        by (simp add: calculation eval_e_uniqueness)
    next
      case False
      then show ?thesis using *  eval_e_lit_inj by auto
    qed
    ultimately show ?thesis using eval_e_eqI[of i "[(V_lit (n1))]^ce"  s1 "[(V_lit (n2))]^ce" s2 ] by auto
  qed
  ultimately show ?thesis using eval_c.intros is_satis.simps by fastforce
qed

lemma valid_eq_e:
  assumes "∀i s1 s2. wfG P B GNil ∧ wfI P GNil i ∧ eval_e i e1 s1 ∧ eval_e i e2 s2 ⟶ s1 = s2"   
    and "wfCE P B GNil e1 b" and "wfCE P B GNil e2 b" 
  shows "P ; B ; (x, b , CE_val (V_var x) == e1 )#_\<Gamma> GNil ⊨ CE_val (V_var x) == e2"
  unfolding valid.simps
proof(intro conjI)
  show ‹ P ; B ; (x, b, [ [ x ]^v ]^ce == e1 ) #_\Γ GNil ⊨_wf [ [ x ]^v ]^ce == e2 ›
    using assms wf_intros wfX_wfY  b.eq_iff fresh_GNil wfC_e_eq2 wfV_elims  by meson
  show ‹∀i. ((P ; (x, b, [ [ x ]^v ]^ce == e1 ) #_\Γ GNil ⊨ i) ∧ (i ⊨ (x, b, [ [ x ]^v ]^ce == e1 ) #_\Γ GNil) ⟶
 (i ⊨ [ [ x ]^v ]^ce == e2)) › proof(rule+)
    fix i
    assume as:"P ; (x, b, [ [ x ]^v ]^ce == e1 ) #_\<Gamma> GNil ⊨ i ∧ i ⊨ (x, b, [ [ x ]^v ]^ce == e1 ) #_\<Gamma> GNil"

    have *: "P ; GNil ⊨ i " using wfI_def by auto

    then obtain s1 where s1:"eval_e i e1 s1" using assms eval_e_exist  by metis
    obtain s2 where s2:"eval_e i e2 s2" using assms eval_e_exist  * by metis
    moreover have "i x = Some s1" proof -
      have "i ⊨ [ [ x ]^v ]^ce == e1" using as is_satis_g.simps by auto
      thus ?thesis using s1 
        by (metis eval_c_elims(7) eval_e_elims(1) eval_e_uniqueness eval_v_elims(2) is_satis.cases)
    qed
    moreover have "s1 = s2" using s1 s2 * assms wfG_nilI wfX_wfY by metis

    ultimately show "i [ [ [ x ]^v ]^ce == e2 ] ~ True" 
      using eval_c.intros eval_e.intros eval_v.intros 
    proof -
      have "i [ e2 ] ~ s1"
        by (metis ‹s1 = s2› s2) (* 0.0 ms *)
      then show ?thesis
        by (metis (full_types) ‹i x = Some s1› eval_c_eqI eval_e_valI eval_v_varI) (* 31 ms *)
    qed
  qed
qed

lemma valid_len:
  assumes " ⊨_wf Θ" 
  shows  "Θ ; B ; (x, B_int, [[x]^v]^ce == [[ L_num (int (length v)) ]^v]^ce) #_\<Gamma> GNil ⊨ [[x]^v]^ce == CE_len [[ L_bitvec v ]^v]^ce"  (is "Θ ; B ; ?G ⊨ ?c" )
proof - 
  have *:"Θ ⊨_wf ([]::Φ) ∧ Θ ; B ; GNil ⊨_wf []_\<Delta> " using assms wfG_nilI wfD_emptyI wfPhi_emptyI by auto

  moreover  hence "Θ ; 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)

  moreover 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 wfCE_valI
    by (metis wfCE_lenI)
  moreover have "atom x ♯ GNil" by auto
  ultimately have "Θ ; B ; ?G ⊨_wf ?c" using wfC_e_eq2 assms by simp
  moreover have "(∀i. wfI Θ ?G i ∧ is_satis_g i ?G ⟶ is_satis i ?c)" using is_satis_len_imp by auto
  ultimately show ?thesis using valid.simps by auto
qed

lemma valid_arith_bop:
  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)" and
    "atom x ♯ Γ" 
  shows   "Θ; 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")
proof -
  have "wfC Θ B ?G ?c" proof(rule wfC_e_eq2)
    show "Θ ; B ; Γ ⊨_wf CE_val (V_lit ll) : b" using wfCE_valI wfV_litI assms base_for_lit.simps by metis
    show "Θ ; B ; Γ ⊨_wf CE_op opp ([V_lit (L_num n1)]^ce) ([V_lit (L_num n2)]^ce) : b " 
      using wfCE_plusI wfCE_leqI   wfCE_eqI wfV_litI wfCE_valI base_for_lit.simps assms  by metis
    show "⊨_wf Θ" using assms wfX_wfY by auto 
    show "atom x ♯ Γ" using assms by auto
  qed

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

    hence "is_satis i ((CE_val (V_var x) == CE_val (V_lit (ll)) ))"   by auto
    thus  "is_satis i ((CE_val (V_var x) == CE_op opp ([V_lit (L_num n1)]^ce) ([V_lit (L_num n2)]^ce)))" 
      using is_satis_plus_imp assms opp.exhaust is_satis_leq_imp by auto
  qed
  ultimately show ?thesis using valid.simps by metis
qed

lemma valid_eq_bop:
  assumes "wfG Θ B Γ" and  "atom x ♯ Γ"  and  "base_for_lit l1 = base_for_lit l2"
  shows   "Θ; B ; (x, B_bool, (CE_val (V_var x) == CE_val (V_lit (if l1 = l2 then L_true else L_false)) )) #_\<Gamma> Γ
                          ⊨ (CE_val (V_var x) == CE_op Eq ([V_lit (l1)]^ce) ([V_lit (l2)]^ce ))" (is "Θ ; B ; ?G ⊨ ?c")
proof -
  let ?ll = "(if l1 = l2 then L_true else L_false)"
  have "wfC Θ B ?G ?c" proof(rule wfC_e_eq2)
    show "Θ ; B ; Γ ⊨_wf CE_val (V_lit ?ll) : B_bool" using wfCE_valI wfV_litI assms base_for_lit.simps by metis
    show "Θ ; B ; Γ ⊨_wf CE_op Eq ([V_lit (l1)]^ce) ([V_lit (l2)]^ce) : B_bool " 
      using wfCE_eqI wfCE_leqI   wfCE_eqI wfV_litI wfCE_valI base_for_lit.simps assms by metis
    show "⊨_wf Θ" using assms wfX_wfY by auto 
    show "atom x ♯ Γ" using assms by auto
  qed

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

    hence "is_satis i ((CE_val (V_var x) == CE_val (V_lit (?ll)) ))"   by auto
    thus  "is_satis i ((CE_val (V_var x) == CE_op Eq ([V_lit (l1)]^ce) ([V_lit (l2)]^ce)))" 
      using is_satis_eq_imp assms  by auto
  qed
  ultimately show ?thesis using valid.simps by metis
qed

lemma valid_fst:
  fixes x::x and v₁::v and v₂::v
  assumes   "wfTh Θ" and "wfV Θ B GNil (V_pair v₁ v₂) (B_pair b₁ b₂)"
  shows "Θ ; B ; (x, b₁, [[x]^v]^ce == [v₁]^ce) #_\<Gamma> GNil ⊨ [[x]^v]^ce == [#1[[v₁,v₂]^v]^ce]^ce" 
proof(rule valid_eq_e)
  show ‹∀i s1 s2. (Θ ; B ⊨_wf GNil) ∧ (Θ ; GNil ⊨ i) ∧ (i [ [ v₁ ]^ce ] ~ s1) ∧ (i [ [#1[[ v₁ , v₂ ]^v]^ce]^ce ] ~ s2) ⟶ s1 = s2›
  proof(rule+)
    fix i s1 s2 
    assume as:"Θ ; B ⊨_wf GNil ∧ Θ ; GNil ⊨ i ∧ (i [ [ v₁ ]^ce ] ~ s1) ∧ (i [ [#1[[ v₁ , v₂ ]^v]^ce]^ce ] ~ s2)"
    then obtain s2' where *:"i [ [ v₁ , v₂ ]^v ] ~ SPair s2 s2'" 
      using eval_e_elims(5)[of i "[[ v₁ , v₂ ]^v]^ce" s2] eval_e_elims 
      by meson
    then have " i [ v₁ ] ~ s2" using eval_v_elims(3)[OF *] by auto
    then show "s1 = s2" using eval_v_uniqueness as 
      using eval_e_uniqueness eval_e_valI by blast
  qed

  show ‹ Θ ; B ; GNil ⊨_wf [ v₁ ]^ce : b₁ › using assms 
    by (metis b.eq_iff(4) wfV_elims(3) wfV_wfCE)
  show ‹ Θ ; B ; GNil ⊨_wf [#1[[ v₁ , v₂ ]^v]^ce]^ce : b₁ › using assms using wfCE_fstI 
    using wfCE_valI by blast
qed

lemma valid_snd: 
  fixes x::x and v₁::v and v₂::v
  assumes   "wfTh Θ" and "wfV Θ B GNil (V_pair v₁ v₂) (B_pair b₁ b₂)"
  shows "Θ ; B ; (x, b₂, [[x]^v]^ce == [v₂]^ce) #_\<Gamma> GNil ⊨ [[x]^v]^ce == [#2[[v₁,v₂]^v]^ce]^ce" 
proof(rule valid_eq_e)
  show ‹∀i s1 s2. (Θ ; B ⊨_wf GNil) ∧ (Θ ; GNil ⊨ i) ∧ (i [ [ v₂ ]^ce ] ~ s1) ∧
 i [ [#2[[ v₁ , v₂ ]^v]^ce]^ce ] ~ s2) ⟶ s1 = s2›
  proof(rule+)
    fix i s1 s2 
    assume as:"Θ ; B ⊨_wf GNil ∧ Θ ; GNil ⊨ i ∧ (i [ [ v₂ ]^ce ] ~ s1) ∧ (i [ [#2[[ v₁ , v₂ ]^v]^ce]^ce ] ~ s2)"
    then obtain s2' where *:"i [ [ v₁ , v₂ ]^v ] ~ SPair s2' s2" 
      using eval_e_elims(5)[of i "[[ v₁ , v₂ ]^v]^ce" s2] eval_e_elims 
      by meson
    then have " i [ v₂ ] ~ s2" using eval_v_elims(3)[OF *] by auto
    then show "s1 = s2" using eval_v_uniqueness as 
      using eval_e_uniqueness eval_e_valI by blast
  qed

  show ‹ Θ ; B ; GNil ⊨_wf [ v₂ ]^ce : b₂ › using assms 
    by (metis b.eq_iff wfV_elims wfV_wfCE)
  show ‹ Θ ; B ; GNil ⊨_wf [#2[[ v₁ , v₂ ]^v]^ce]^ce : b₂ › using assms using wfCE_sndI wfCE_valI by blast
qed

lemma valid_concat:
  fixes v1::"bit list" and v2::"bit list"
  assumes " ⊨_wf Π" 
  shows "Π ; B ; (x, B_bitvec, (CE_val (V_var x) == CE_val (V_lit (L_bitvec (v1@ v2))))) #_\<Gamma> GNil ⊨
            (CE_val (V_var x) == CE_concat ([V_lit (L_bitvec v1)]^ce ) ([V_lit (L_bitvec v2)]^ce) )"
proof(rule valid_eq_e)                         
  show ‹∀i s1 s2. ((Π ; B ⊨_wf GNil) ∧ (Π ; GNil ⊨ i) ∧
 (i [ [ [ L_bitvec (v1 @ v2) ]^v ]^ce ] ~ s1) ∧ (i [ [[[ L_bitvec v1 ]^v]^ce @@ [[ L_bitvec v2 ]^v]^ce ]^ce ] ~ s2) ⟶
 s1 = s2)›
  proof(rule+)
    fix i s1 s2 
    assume as: "(Π ; B ⊨_wf GNil) ∧ (Π ; GNil ⊨ i) ∧ (i [ [ [ L_bitvec (v1 @ v2) ]^v ]^ce ] ~ s1) ∧
            (i [ [[[ L_bitvec v1 ]^v]^ce @@ [[ L_bitvec v2 ]^v]^ce]^ce ] ~ s2) "

    hence *: "i [ [[[ L_bitvec v1 ]^v]^ce @@ [[ L_bitvec v2 ]^v]^ce]^ce ] ~ s2"  by auto
    obtain bv1 bv2 where s2:"s2 = SBitvec (bv1 @ bv2) ∧ i [ [ L_bitvec v1 ]^v ] ~ SBitvec bv1 ∧ (i [ [ L_bitvec v2 ]^v ] ~ SBitvec bv2)" 
      using eval_e_elims(7)[OF *] eval_e_elims(1) by metis
    hence "v1 = bv1 ∧ v2 = bv2" using eval_v_elims(1) eval_l.simps(5) by force
    moreover then have "s1 = SBitvec (bv1 @ bv2)" using s2 using eval_v_elims(1) eval_l.simps(5) 
      by (metis as eval_e_elims(1))

    then show "s1 = s2" using s2 by auto
  qed  

  show ‹ Π ; B ; GNil ⊨_wf [ [ L_bitvec (v1 @ v2) ]^v ]^ce : B_bitvec ›
    by (metis assms base_for_lit.simps(5) wfG_nilI wfV_litI wfV_wfCE)
  show ‹ Π ; B ; GNil ⊨_wf [[[ L_bitvec v1 ]^v]^ce @@ [[ L_bitvec v2 ]^v]^ce]^ce : B_bitvec ›
    by (metis assms base_for_lit.simps(5) wfCE_concatI wfG_nilI wfV_litI wfCE_valI)
qed

lemma valid_ce_eq:
  fixes ce::ce
  assumes  "Θ ; B ; Γ ⊨_wf ce : b"
  shows ‹Θ ; B ; Γ ⊨ ce == ce ›
  unfolding valid.simps proof 
  show ‹ Θ ; B ; Γ ⊨_wf ce == ce › using assms wfC_eqI by auto
  show ‹∀i. Θ ; Γ ⊨ i ∧ i ⊨ Γ ⟶ i ⊨ ce == ce › proof(rule+)
    fix i
    assume "Θ ; Γ ⊨ i ∧ i ⊨ Γ"
    then obtain s where "i[ ce ] ~ s" using assms eval_e_exist by metis
    then show "i [ ce == ce ] ~ True " using eval_c_eqI by metis
  qed
qed

lemma valid_eq_imp:
  fixes c1::c and c2::c
  assumes " Θ ; B ; (x, b, c2) #_\<Gamma> Γ ⊨_wf c1 IMP c2"
  shows  " Θ ; B ; (x, b, c2) #_\<Gamma> Γ ⊨ c1 IMP c2 "
proof -
  have "∀i. (Θ ; (x, b, c2) #_\<Gamma> Γ ⊨ i ∧ i ⊨ (x, b, c2) #_\<Gamma> Γ) ⟶ i ⊨ ( c1 IMP c2 )"
  proof(rule,rule)
    fix i
    assume as:"Θ ; (x, b, c2) #_\<Gamma> Γ ⊨ i ∧ i ⊨ (x, b, c2) #_\<Gamma> Γ"

    have "Θ ; B ; (x, b, c2) #_\<Gamma> Γ ⊨_wf c1" using wfC_elims assms by metis

    then obtain sc where "i [ c1 ] ~ sc" using eval_c_exist assms as by metis
    moreover have  "i [ c2 ] ~ True" using as is_satis_g.simps is_satis.simps by auto

    ultimately have "i [ c1 IMP c2 ] ~ True" using eval_c_impI by metis

    thus  "i ⊨ c1 IMP c2" using is_satis.simps by auto
  qed
  thus ?thesis using assms by auto
qed

lemma valid_range:
  assumes "0 ≤ n ∧ n ≤ m" and "⊨_wf Θ"
  shows "Θ ; {||} ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #_\<Gamma> GNil ⊨
                              (C_eq (CE_op LEq (CE_val (V_var x)) (CE_val (V_lit (L_num m)))) [[ L_true ]^v ]^ce) AND
                             (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]^v ]^ce)"
    (is "Θ ; {||} ; ?G ⊨ ?c1 AND ?c2")
proof(rule validI)
  have wfg: " Θ ; {||} ⊨_wf (x, B_int, [ [ x ]^v ]^ce == [ [ L_num n ]^v ]^ce ) #_\<Gamma> GNil " 
    using assms base_for_lit.simps wfG_nilI wfV_litI fresh_GNil wfB_intI wfC_v_eq wfG_cons1I wfG_cons2I by metis

  show "Θ ; {||} ; ?G ⊨_wf ?c1 AND ?c2" 
    using wfC_conjI wfC_eqI wfCE_leqI wfCE_valI wfV_varI wfg lookup.simps base_for_lit.simps wfV_litI wfB_intI wfB_boolI 
    by metis

  show "∀i. Θ ; ?G ⊨ i ∧ i ⊨ ?G ⟶ i ⊨ ?c1 AND ?c2" proof(rule,rule)
    fix i
    assume a:"Θ ; ?G ⊨ i ∧ i ⊨ ?G"
    hence *:"i [ V_var x ] ~ SNum n" 
    proof - 
      obtain sv where sv: "i x = Some sv ∧ Θ ⊨ sv : B_int" using a wfI_def by force
      have "i [ (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n)))) ] ~ True" 
        using a is_satis_g.simps 
        using is_satis.cases by blast
      hence "i x = Some(SNum n)" using sv 
        by (metis eval_c_elims(7) eval_e_elims(1) eval_l.simps(3) eval_v_elims(1) eval_v_elims(2))
      thus ?thesis using eval_v_varI by auto
    qed

    show "i ⊨ ?c1 AND ?c2" 
    proof - 
      have "i [ ?c1 ] ~ True" 
      proof -
        have "i [ [ leq [ [ x ]^v ]^ce [ [ L_num m ]^v ]^ce ]^ce] ~ SBool True" 
          using eval_e_leqI assms eval_v_litI eval_l.simps * 
          by (metis (full_types) eval_e_valI)
        moreover have "i [ [ [ L_true ]^v ]^ce ] ~ SBool True" 
          using eval_v_litI eval_e_valI eval_l.simps by metis
        ultimately show ?thesis using  eval_c_eqI by metis
      qed

      moreover have "i [ ?c2 ] ~ True" 
      proof -
        have "i [ [ leq [ [ L_num 0 ]^v ]^ce [ [ x ]^v ]^ce ]^ce ] ~ SBool True"
          using eval_e_leqI assms eval_v_litI eval_l.simps * 
          by (metis (full_types) eval_e_valI)
        moreover have "i [ [ [ L_true ]^v ]^ce ] ~ SBool True" 
          using eval_v_litI eval_e_valI eval_l.simps by metis
        ultimately show ?thesis using  eval_c_eqI by metis
      qed      
      ultimately show ?thesis using eval_c_conjI is_satis.simps by metis
    qed
  qed
qed

lemma valid_range_length:
  fixes Γ::Γ
  assumes "0 ≤ n ∧ n ≤ int (length v)" and " Θ ; {||} ⊨_wf Γ" and "atom x ♯ Γ"
  shows "Θ ; {||} ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #_\<Gamma> Γ ⊨
                     (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]^v ]^ce) AND
                     (C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]^v ]^ce |]^ce )) [[ L_true ]^v ]^ce)
                            "
    (is "Θ ; {||} ; ?G ⊨ ?c1 AND ?c2")
proof(rule validI)
  have wfg: " Θ ; {||} ⊨_wf (x, B_int, [ [ x ]^v ]^ce == [ [ L_num n ]^v ]^ce ) #_\<Gamma> Γ " apply(rule  wfG_cons1I)
    apply simp
    using assms apply simp+
    using assms base_for_lit.simps wfG_nilI wfV_litI  wfB_intI wfC_v_eq  wfB_intI wfX_wfY assms by metis+

  show "Θ ; {||} ; ?G ⊨_wf ?c1 AND ?c2" 
    using wfC_conjI wfC_eqI wfCE_leqI wfCE_valI wfV_varI wfg lookup.simps base_for_lit.simps wfV_litI wfB_intI wfB_boolI     
    by (metis (full_types) wfCE_lenI)

  show "∀i. Θ ; ?G ⊨ i ∧ i ⊨ ?G ⟶ i ⊨ ?c1 AND ?c2" proof(rule,rule)
    fix i
    assume a:"Θ ; ?G ⊨ i ∧ i ⊨ ?G"
    hence *:"i [ V_var x ] ~ SNum n" 
    proof - 
      obtain sv where sv: "i x = Some sv ∧ Θ ⊨ sv : B_int" using a wfI_def by force
      have "i [ (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n)))) ] ~ True" 
        using a is_satis_g.simps 
        using is_satis.cases by blast
      hence "i x = Some(SNum n)" using sv 
        by (metis eval_c_elims(7) eval_e_elims(1) eval_l.simps(3) eval_v_elims(1) eval_v_elims(2))
      thus ?thesis using eval_v_varI by auto
    qed

    show "i ⊨ ?c1 AND ?c2" 
    proof - 
      have "i [ ?c2 ] ~ True" 
      proof -
        have "i [ [ leq [ [ x ]^v ]^ce [| [ [ L_bitvec v ]^v ]^ce |]^ce ]^ce] ~ SBool True" 
          using eval_e_leqI assms eval_v_litI eval_l.simps * 
          by (metis (full_types) eval_e_lenI eval_e_valI)        
        moreover have "i [ [ [ L_true ]^v ]^ce ] ~ SBool True" 
          using eval_v_litI eval_e_valI eval_l.simps by metis
        ultimately show ?thesis using  eval_c_eqI by metis
      qed

      moreover have "i [ ?c1 ] ~ True" 
      proof -
        have "i [ [ leq [ [ L_num 0 ]^v ]^ce [ [ x ]^v ]^ce ]^ce ] ~ SBool True"
          using eval_e_leqI assms eval_v_litI eval_l.simps * 
          by (metis (full_types) eval_e_valI)
        moreover have "i [ [ [ L_true ]^v ]^ce ] ~ SBool True" 
          using eval_v_litI eval_e_valI eval_l.simps by metis
        ultimately show ?thesis using  eval_c_eqI by metis
      qed      
      ultimately show ?thesis using eval_c_conjI is_satis.simps by metis
    qed
  qed
qed

lemma valid_range_length_inv_gnil:
  fixes Γ::Γ
  assumes  "⊨_wf Θ "
    and  "Θ ; {||} ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #_\<Gamma> GNil ⊨
                     (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]^v ]^ce) AND
                     (C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]^v ]^ce |]^ce )) [[ L_true ]^v ]^ce)
                            "
    (is "Θ ; {||} ; ?G ⊨ ?c1 AND ?c2")
  shows "0 ≤ n ∧ n ≤ int (length v)" 
proof -
  have *:"∀i. Θ ; ?G ⊨ i ∧ i ⊨ ?G ⟶ i ⊨ ?c1 AND ?c2" using assms valid.simps by simp

  obtain i where i: "i x = Some (SNum n)" by auto
  have "Θ ; ?G ⊨ i ∧ i ⊨ ?G" proof 
    show  "Θ ; ?G ⊨ i" unfolding wfI_def using wfRCV_BIntI i * by auto
    have "i [ ([ [ x ]^v ]^ce == [ [ L_num n ]^v ]^ce ) ] ~ True" 
      using * eval_c.intros(7) eval_e.intros eval_v.intros  eval_l.simps 
      by (metis (full_types) i)
    thus  "i ⊨ ?G" unfolding  is_satis_g.simps is_satis.simps by auto
  qed     
  hence **:"i ⊨ ?c1 AND ?c2" using * by auto

  hence  1: "i [ ?c1 ] ~ True" using eval_c_elims(3) is_satis.simps 
    by fastforce
  then obtain sv1 and sv2 where "(sv1 = sv2) = True ∧ i [ [ leq [ [ L_num 0 ]^v ]^ce [ [ x ]^v ]^ce ]^ce ] ~ sv1 ∧ i [ [ [ L_true ]^v ]^ce ] ~ sv2" 
    using eval_c_elims(7) by metis
  hence "sv1 = SBool True" using eval_e_elims eval_v_elims eval_l.simps i by metis
  obtain n1 and n2 where "SBool True = SBool (n1 ≤ n2) ∧ (i [ [ [ L_num 0 ]^v ]^ce ] ~ SNum n1) ∧ (i [ [ [ x ]^v ]^ce ] ~ SNum n2)" 
    using eval_e_elims(3)[of i " [ [ L_num 0 ]^v ]^ce" "[ [ x ]^v ]^ce "  "SBool True"] 
    using ‹(sv1 = sv2) = True ∧ i [ [ leq [ [ L_num 0 ]^v ]^ce [ [ x ]^v ]^ce ]^ce ] ~ sv1 ∧ i [ [ [ L_true ]^v ]^ce ] ~ sv2› ‹sv1 = SBool True› by fastforce
  moreover hence "n1 = 0" and "n2 = n"  using eval_e_elims eval_v_elims i 
    apply (metis eval_l.simps(3) rcl_val.eq_iff(2))
    using eval_e_elims eval_v_elims i 
    by (metis calculation option.inject rcl_val.eq_iff(2))
  ultimately have  le1: "0 ≤ n " by simp

  hence  2: "i [ ?c2 ] ~ True" using ** eval_c_elims(3) is_satis.simps 
    by fastforce
  then obtain sv1 and sv2 where sv: "(sv1 = sv2) = True ∧ i [ [ leq [ [ x ]^v ]^ce [| [ [ L_bitvec v ]^v ]^ce |]^ce ]^ce ] ~ sv1 ∧ i [ [ [ L_true ]^v ]^ce ] ~ sv2" 
    using eval_c_elims(7) by metis
  hence "sv1 = SBool True" using eval_e_elims eval_v_elims eval_l.simps i by metis
  obtain n1 and n2 where ***:"SBool True = SBool (n1 ≤ n2) ∧ (i [ [ [ x ]^v ]^ce ] ~ SNum n1) ∧ (i [ [| [ [ L_bitvec v ]^v ]^ce |]^ce ] ~ SNum n2)" 
    using eval_e_elims(3) 
    using sv ‹sv1 = SBool True› by metis
  moreover hence "n1 = n" using eval_e_elims(1)[of i] eval_v_elims(2)[of i x "SNum n1"] i by auto
  moreover  have "n2 = int (length v)"  using eval_e_elims(8) eval_v_elims(1) eval_l.simps i    
    by (metis "***" eval_e_elims(1) rcl_val.eq_iff(1) rcl_val.eq_iff(2))    
  ultimately have  le2: "n ≤ int (length v) " by simp

  show ?thesis using le1 le2 by auto
qed

lemma wfI_cons:  
  fixes i::valuation and Γ::Γ
  assumes "i' ⊨ Γ" and "Θ ; Γ ⊨ i'" and "i = i' ( x ↦ s)" and "Θ ⊨ s : b" and "atom x ♯ Γ"
  shows "Θ ; (x,b,c) #_\<Gamma> Γ ⊨ i"  
  unfolding wfI_def proof - 
  {  
    fix x' b' c' 
    assume "(x',b',c') ∈ toSet ((x, b, c) #_\<Gamma> Γ)"
    then consider "(x',b',c') = (x,b,c)" | "(x',b',c') ∈ toSet Γ" using toSet.simps by auto
    then have "∃s. Some s = i x' ∧ Θ ⊨ s : b'" proof(cases)
      case 1
      then show ?thesis using assms by auto
    next
      case 2
      then obtain s where s:"Some s = i' x' ∧ Θ ⊨ s : b'" using assms wfI_def by auto
      moreover have "x' ≠ x" using assms 2 fresh_dom_free by auto
      ultimately have "Some s = i x'" using assms by auto
      then show ?thesis using s  wfI_def by auto
    qed
  }
  thus "∀(x, b, c)∈toSet ((x, b, c) #_\<Gamma> Γ). ∃s. Some s = i x ∧ Θ ⊨ s : b" by auto
qed

lemma valid_range_length_inv:
  fixes Γ::Γ
  assumes  "Θ ; B ⊨_wf Γ " and "atom x ♯ Γ" and "∃i. i ⊨ Γ ∧ Θ ; Γ ⊨ i"
    and  "Θ ; B ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #_\<Gamma> Γ ⊨
                     (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]^v ]^ce) AND
                     (C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]^v ]^ce |]^ce )) [[ L_true ]^v ]^ce)
                            "
    (is "Θ ; ?B ; ?G ⊨ ?c1 AND ?c2")
  shows "0 ≤ n ∧ n ≤ int (length v)" 
proof -
  have *:"∀i. Θ ; ?G ⊨ i ∧ i ⊨ ?G ⟶ i ⊨ ?c1 AND ?c2" using assms valid.simps by simp

  obtain i' where idash: "is_satis_g i' Γ ∧ Θ ; Γ ⊨ i'" using assms by auto
  obtain i where i: "i = i' ( x ↦ SNum n)" by auto
  hence ix: "i x = Some (SNum n)" by auto
  have "Θ ; ?G ⊨ i ∧ i ⊨ ?G" proof 
    show  "Θ ; ?G ⊨ i" using wfI_cons i idash ix wfRCV_BIntI assms by simp

    have **:"i [ ([ [ x ]^v ]^ce == [ [ L_num n ]^v ]^ce ) ] ~ True" 
      using * eval_c.intros(7) eval_e.intros eval_v.intros  eval_l.simps i 
      by (metis (full_types) ix)

    show  "i ⊨ ?G" unfolding  is_satis_g.simps proof 
      show ‹ i ⊨ [ [ x ]^v ]^ce == [ [ L_num n ]^v ]^ce › using ** is_satis.simps by auto
      show ‹ i ⊨ Γ › using idash i assms is_satis_g_i_upd by metis
    qed
  qed     
  hence **:"i ⊨ ?c1 AND ?c2" using * by auto

  hence  1: "i [ ?c1 ] ~ True" using eval_c_elims(3) is_satis.simps 
    by fastforce
  then obtain sv1 and sv2 where "(sv1 = sv2) = True ∧ i [ [ leq [ [ L_num 0 ]^v ]^ce [ [ x ]^v ]^ce ]^ce ] ~ sv1 ∧ i [ [ [ L_true ]^v ]^ce ] ~ sv2" 
    using eval_c_elims(7) by metis
  hence "sv1 = SBool True" using eval_e_elims eval_v_elims eval_l.simps i by metis
  obtain n1 and n2 where "SBool True = SBool (n1 ≤ n2) ∧ (i [ [ [ L_num 0 ]^v ]^ce ] ~ SNum n1) ∧ (i [ [ [ x ]^v ]^ce ] ~ SNum n2)" 
    using eval_e_elims(3)[of i " [ [ L_num 0 ]^v ]^ce" "[ [ x ]^v ]^ce "  "SBool True"] 
    using ‹(sv1 = sv2) = True ∧ i [ [ leq [ [ L_num 0 ]^v ]^ce [ [ x ]^v ]^ce ]^ce ] ~ sv1 ∧ i [ [ [ L_true ]^v ]^ce ] ~ sv2› ‹sv1 = SBool True› by fastforce
  moreover hence "n1 = 0" and "n2 = n"  using eval_e_elims eval_v_elims i 
    apply (metis eval_l.simps(3) rcl_val.eq_iff(2))
    using eval_e_elims eval_v_elims i 
      calculation option.inject rcl_val.eq_iff(2)
    by (metis ix)
  ultimately have  le1: "0 ≤ n " by simp

  hence  2: "i [ ?c2 ] ~ True" using ** eval_c_elims(3) is_satis.simps 
    by fastforce
  then obtain sv1 and sv2 where sv: "(sv1 = sv2) = True ∧ i [ [ leq [ [ x ]^v ]^ce [| [ [ L_bitvec v ]^v ]^ce |]^ce ]^ce ] ~ sv1 ∧ i [ [ [ L_true ]^v ]^ce ] ~ sv2" 
    using eval_c_elims(7) by metis
  hence "sv1 = SBool True" using eval_e_elims eval_v_elims eval_l.simps i by metis
  obtain n1 and n2 where ***:"SBool True = SBool (n1 ≤ n2) ∧ (i [ [ [ x ]^v ]^ce ] ~ SNum n1) ∧ (i [ [| [ [ L_bitvec v ]^v ]^ce |]^ce ] ~ SNum n2)" 
    using eval_e_elims(3) 
    using sv ‹sv1 = SBool True› by metis
  moreover hence "n1 = n" using eval_e_elims(1)[of i] eval_v_elims(2)[of i x "SNum n1"] i by auto
  moreover  have "n2 = int (length v)"  using eval_e_elims(8) eval_v_elims(1) eval_l.simps i    
    by (metis "***" eval_e_elims(1) rcl_val.eq_iff(1) rcl_val.eq_iff(2))    
  ultimately have  le2: "n ≤ int (length v) " by simp

  show ?thesis using le1 le2 by auto
qed

lemma eval_c_conj2I[intro]: 
  assumes "i [ c1 ] ~ True" and "i [ c2 ] ~ True"
  shows "i [ (C_conj c1 c2) ] ~ True"
  using assms eval_c_conjI by metis

lemma valid_split:
  assumes "split n v (v1,v2)" and "⊨_wf Θ"
  shows "Θ ; {||} ; (z , [B_bitvec , B_bitvec ]^b , [ [ z ]^v ]^ce == [ [ [ L_bitvec v1 ]^v , [ L_bitvec v2 ]^v ]^v ]^ce) #_\<Gamma> GNil
\<Turnstile> ([ [ 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 "Θ ; {||} ; ?G ⊨ ?c1 AND ?c2")
  unfolding valid.simps proof

  have wfg: " Θ ; {||} ⊨_wf (z, [B_bitvec , B_bitvec ]^b , [ [ z ]^v ]^ce == [ [ [ L_bitvec v1 ]^v , [ L_bitvec v2 ]^v ]^v ]^ce) #_\<Gamma> GNil" 
    using wf_intros assms base_for_lit.simps  fresh_GNil wfC_v_eq  wfG_intros2 by metis   

  show "Θ ; {||} ; ?G ⊨_wf ?c1 AND ?c2" 
    apply(rule wfC_conjI)
    apply(rule wfC_eqI)
    apply(rule wfCE_valI)
    apply(rule wfV_litI)
    using wf_intros wfg lookup.simps base_for_lit.simps wfC_v_eq 
    apply (metis )+
    done

  have len:"int (length v1) = n" using assms split_length by auto

  show "∀i. Θ ; ?G ⊨ i ∧ i ⊨ ?G ⟶ i ⊨ (?c1 AND ?c2)" 
  proof(rule,rule)
    fix i
    assume a:"Θ ; ?G ⊨ i ∧ i ⊨ ?G"
    hence "i [ [ [ z ]^v ]^ce == [ [ [ L_bitvec v1 ]^v , [ L_bitvec v2 ]^v ]^v ]^ce ] ~ True" 
      using is_satis_g.simps is_satis.simps by simp
    then obtain sv where "i [ [ [ z ]^v ]^ce ] ~ sv ∧ i [ [ [ [ L_bitvec v1 ]^v , [ L_bitvec v2 ]^v ]^v ]^ce ] ~ sv" 
      using eval_c_elims by metis
    hence "i [ [ [ z ]^v ]^ce ] ~ (SPair (SBitvec v1) (SBitvec v2))" using eval_c_eqI eval_v.intros eval_l.simps
      by (metis eval_e_elims(1) eval_v_uniqueness)
    hence b:"i z = Some (SPair (SBitvec v1) (SBitvec v2))" using a eval_e_elims eval_v_elims by metis

    have v1: "i [ [#1[ [ z ]^v ]^ce]^ce ] ~ SBitvec v1 "
      using eval_e_fstI eval_e_valI eval_v_varI b by metis
    have v2: "i [ [#2[ [ z ]^v ]^ce]^ce ] ~ SBitvec v2"
      using eval_e_sndI eval_e_valI eval_v_varI b by metis

    have "i [ [ [ L_bitvec v ]^v ]^ce ] ~ SBitvec v" using eval_e.intros eval_v.intros eval_l.simps by metis
    moreover have "i [ [ [#1[ [ z ]^v ]^ce]^ce @@ [#2[ [ z ]^v ]^ce]^ce ]^ce ] ~ SBitvec v"
      using assms split_concat v1 v2 eval_e_concatI by metis
    moreover have "i [ [| [#1[ [ z ]^v ]^ce]^ce |]^ce ] ~ SNum (int (length v1))"
      using v1 eval_e_lenI by auto
    moreover have "i [ [ [ L_num n ]^v ]^ce ] ~ SNum n" using eval_e.intros eval_v.intros eval_l.simps by metis
    ultimately show "i ⊨ ?c1 AND ?c2" using is_satis.intros eval_c_conj2I eval_c_eqI len by metis
  qed
qed


lemma is_satis_eq:
  assumes "wfI Θ G i" and "wfCE Θ B G e b"
  shows "is_satis i (e == e)"
proof(rule)
  obtain s where "eval_e i e s" using eval_e_exist assms by metis
  thus "eval_c i (e == e ) True" using eval_c_eqI by metis
qed

lemma is_satis_g_i_upd2:
  assumes "eval_v i v s" and "is_satis ((i ( x ↦ s))) c0" and "atom x ♯ G" and "wfG Θ B (G3@((x,b,c0)#_\<Gamma>G))" and "wfV Θ B G v b" and "wfI Θ (G3[x::=v]_\<Gamma>_v@G) i"
    and "is_satis_g i (G3[x::=v]_\<Gamma>_v@G)"
  shows "is_satis_g (i ( x ↦ s)) (G3@((x,b,c0)#_\<Gamma>G))"
  using assms proof(induct G3 rule: Γ_induct)
  case GNil
  hence "is_satis_g (i(x ↦ s)) G" using is_satis_g_i_upd by auto
  then show ?case using GNil using is_satis_g.simps append_g.simps by metis
next
  case (GCons x' b' c' Γ')
  hence "x≠x'" using wfG_cons_append by metis
  hence "is_satis_g i (((x', b', c'[x::=v]_cv) #_\<Gamma> (Γ'[x::=v]_\<Gamma>_v) @ G))" using subst_gv.simps GCons by auto
  hence *:"is_satis i c'[x::=v]_cv ∧ is_satis_g i ((Γ'[x::=v]_\<Gamma>_v) @ G)" using subst_gv.simps by auto

  have "is_satis_g (i(x ↦ s)) ((x', b', c') #_\<Gamma> (Γ'@ (x, b, c0) #_\<Gamma> G))" proof(subst is_satis_g.simps,rule)
    show "is_satis (i(x ↦ s)) c'" proof(subst subst_c_satis_full[symmetric])
      show ‹eval_v i v s› using GCons by auto
      show ‹ Θ ; B ; ((x', b', c') #_\<Gamma>Γ')@(x, b, c0) #_\<Gamma> G ⊨_wf c' › using GCons wfC_refl by auto
      show ‹wfI Θ ((((x', b', c') #_\<Gamma> Γ')[x::=v]_\<Gamma>_v) @ G) i› using GCons by auto
      show ‹ Θ ; B ; G ⊨_wf v : b › using GCons by auto
      show ‹is_satis i c'[x::=v]_cv› using * by auto
    qed
    show "is_satis_g (i(x ↦ s)) (Γ' @ (x, b, c0) #_\<Gamma> G)" proof(rule GCons(1))
      show ‹eval_v i v s› using GCons by auto
      show ‹is_satis (i(x ↦ s)) c0› using GCons by metis
      show ‹atom x ♯ G› using GCons by auto
      show ‹ Θ ; B⊨_wf Γ' @ (x, b, c0) #_\<Gamma> G › using GCons wfG_elims append_g.simps by metis
      show ‹is_satis_g i (Γ'[x::=v]_\<Gamma>_v @ G)› using * by auto
      show "wfI Θ (Γ'[x::=v]_\<Gamma>_v @ G) i" using GCons wfI_def subst_g_assoc_cons ‹x≠x'› by auto
      show "Θ ; B ; G ⊨_wf v : b " using GCons by auto
    qed
  qed
  moreover have "((x', b', c') #_\<Gamma> Γ' @ (x, b, c0) #_\<Gamma> G) = (((x', b', c') #_\<Gamma> Γ') @ (x, b, c0) #_\<Gamma> G)" by auto
  ultimately show ?case using GCons by metis
qed


end