Theory RCLogicL
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 ⊢⇩w⇩f 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 ⊢⇩w⇩f 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) #⇩Γ Γ) i"
shows "wfI Θ (Γ' @ (x, b, c') #⇩Γ Γ) 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 "⊢⇩w⇩f 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']⇩b⇩b=b1[bv1::=b']⇩b⇩b"
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']⇩b⇩b = b1[bv1::=b']⇩b⇩b"
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 ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f v1 : b1 ∧ P ; B ; Γ ⊢⇩w⇩f 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']⇩b⇩b) ∧ 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']⇩b⇩b" using V_consp by auto
have " ⊢⇩w⇩f 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']⇩b⇩b = b1[bv1::=b']⇩b⇩b"
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']⇩b⇩b› 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 ; Γ ⊢⇩w⇩f 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›)
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))
then show ?thesis
by metis
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
then have "∀f c r. ¬ f ⟦ [| c |]⇧c⇧e ⟧ ~ r ∨ r = SNum (int (length (bbs r c f))) ∧ f ⟦ c ⟧ ~ SBitvec (bbs r c f)"
by (meson eval_e_elims(8))
then show ?thesis
by (metis (no_types) CE_len.hyps CE_len.prems(1) CE_len.prems(2) rcl_val.eq_iff(1))
qed
qed
lemma wfV_eval_bitvec:
fixes v::v
assumes "P ; B ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f 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
then show ?thesis
by (metis (no_types) "local.*" wfRCV_BBitvecI eval_e_concatI)
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 ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f v1 : B_int ∧ P ; B ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f v1 : B_int ∧ P ; B ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f v1 : b1 ∧ P ; B ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f 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 ; Γ ⊢⇩w⇩f 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) #⇩Γ 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]⇩v⇩v) ⟧ ~ 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]⇩v⇩v = 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]⇩v⇩v) s1 ∧ eval_v i (v2[x::=v]⇩v⇩v) 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]⇩v⇩v) 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]⇩v⇩v) 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]⇩c⇩e⇩v)" 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]⇩v⇩v"
using assms by(nominal_induct e rule:ce.strong_induct,simp+)
hence "eval_v i (v1'[y::=v]⇩v⇩v) 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]⇩c⇩e⇩v ∧ v2 = v2'[y::=v]⇩c⇩e⇩v"
using assms by(nominal_induct e rule:ce.strong_induct,simp+)
hence "eval_e i (v1'[y::=v]⇩c⇩e⇩v) (SNum n1) ∧ eval_e i (v2'[y::=v]⇩c⇩e⇩v) (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]⇩c⇩e⇩v ∧ v2 = v2'[y::=v]⇩c⇩e⇩v"
using assms by(nominal_induct e rule:ce.strong_induct,simp+)
hence "eval_e i (v1'[y::=v]⇩c⇩e⇩v) (SNum n1) ∧ eval_e i (v2'[y::=v]⇩c⇩e⇩v) (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]⇩c⇩e⇩v ∧ v2 = v2'[y::=v]⇩c⇩e⇩v"
using assms by(nominal_induct e rule:ce.strong_induct,simp+)
hence "eval_e i (v1'[y::=v]⇩c⇩e⇩v) n1 ∧ eval_e i (v2'[y::=v]⇩c⇩e⇩v) 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]⇩c⇩e⇩v"
using assms by(nominal_induct e rule:ce.strong_induct,simp+)
hence "eval_e i (v1'[y::=v]⇩c⇩e⇩v) (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]⇩c⇩e⇩v"
using assms by(nominal_induct e rule:ce.strong_induct,simp+)
hence "eval_e i (v1'[y::=v]⇩c⇩e⇩v) (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]⇩c⇩e⇩v ∧ v2 = v2'[y::=v]⇩c⇩e⇩v"
using assms by(nominal_induct e rule:ce.strong_induct,simp+)
hence "eval_e i (v1'[y::=v]⇩c⇩e⇩v) (SBitvec bv1) ∧ eval_e i (v2'[y::=v]⇩c⇩e⇩v) (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]⇩c⇩e⇩v"
using assms by(nominal_induct e rule:ce.strong_induct,simp+)
hence "eval_e i (v1'[y::=v]⇩c⇩e⇩v) (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]⇩c⇩v ⟧ ~ 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]⇩c⇩v AND c2[x::=v]⇩c⇩v) s1" using subst_cv.simps by auto
then obtain s11 and s12 where "(s1 = (s11 ∧ s12)) ∧ eval_c i c1[x::=v]⇩c⇩v s11 ∧ eval_c i c2[x::=v]⇩c⇩v 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]⇩c⇩v OR c2[x::=v]⇩c⇩v) s1" using subst_cv.simps by auto
then obtain s11 and s12 where "(s1 = (s11 ∨ s12)) ∧ eval_c i c1[x::=v]⇩c⇩v s11 ∧ eval_c i c2[x::=v]⇩c⇩v 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]⇩c⇩v 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]⇩c⇩v IMP c2[x::=v]⇩c⇩v) s1" using subst_cv.simps by auto
then obtain s11 and s12 where "(s1 = (s11 ⟶ s12)) ∧ eval_c i c1[x::=v]⇩c⇩v s11 ∧ eval_c i c2[x::=v]⇩c⇩v 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]⇩c⇩e⇩v == e2[x::=v]⇩c⇩e⇩v) s1" using subst_cv.simps by auto
then obtain s11 and s12 where "(s1 = (s11 = s12)) ∧ eval_e i (e1[x::=v]⇩c⇩e⇩v) s11 ∧ eval_e i (e2[x::=v]⇩c⇩e⇩v) 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) #⇩Γ Γ)"
shows "wfI Θ ((x, b, c) #⇩Γ Γ) (i(x ↦ s))"
proof(subst wfI_def,rule)
fix xa
assume as:"xa ∈ toSet ((x, b, c) #⇩Γ Γ)"
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]⇩Γ⇩v)@Γ)" and "wfRCV Θ s b" and "wfG Θ B (Γ'@((x,b,c)#⇩ΓΓ))" and "Θ ; B ; Γ ⊢⇩w⇩f v : b"
shows "wfI Θ (Γ'@((x,b,c)#⇩ΓΓ)) (i(x ↦ s))"
proof(subst wfI_def,rule)
fix xa
assume as:"xa ∈ toSet (Γ'@((x,b,c)#⇩ΓΓ))"
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]⇩Γ⇩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')#⇩ΓΓ) c" and "wfI Θ Γ i" and "Θ ; B ; Γ ⊢⇩w⇩f v : b"
shows "i ⊨ (c[x::=v]⇩c⇩v) ⟷ (i ( x ↦ s)) ⊨ c"
proof -
have "wfI Θ ((x, b, c') #⇩Γ Γ) (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')#⇩ΓΓ)" "(i ( x ↦ s))" B c ] assms by auto
have "Θ ; B ; Γ ⊢⇩w⇩f c[x::=v]⇩c⇩v" 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]⇩c⇩v s2" using eval_c_exist[of Θ "Γ" "i" B "c[x::=v]⇩c⇩v" ] 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')#⇩ΓΓ)) c" and "wfI Θ ((Γ'[x::=v]⇩Γ⇩v)@Γ) i" and "Θ ; B ; Γ ⊢⇩w⇩f v : b"
shows "i ⊨ (c[x::=v]⇩c⇩v) ⟷ (i ( x ↦ s)) ⊨ c"
proof -
have "wfI Θ (Γ'@((x, b, c')) #⇩Γ Γ) (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')#⇩ΓΓ)" "(i ( x ↦ s))" B c ] assms by auto
have "Θ ; B ; ((Γ'[x::=v]⇩Γ⇩v)@Γ) ⊢⇩w⇩f c[x::=v]⇩c⇩v" using wbc_subst assms by auto
then obtain s2 where s2:"eval_c i c[x::=v]⇩c⇩v s2" using eval_c_exist[of Θ "((Γ'[x::=v]⇩Γ⇩v)@Γ)" "i" B "c[x::=v]⇩c⇩v" ] 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 ⊢⇩w⇩f G"
using assms wfC_wf valid.simps by blast
lemma valid_reflI [intro]:
fixes b::b
assumes "P ; B ; ((x,b,c1)#⇩ΓG) ⊢⇩w⇩f c1" and "c1 = c2"
shows "P ; B ; ((x,b,c1)#⇩ΓG) ⊨ c2"
using satis_reflI assms by simp
subsection ‹Weakening and Strengthening›
text ‹ Adding to the domain of a valuation doesn't change the result ›
lemma eval_v_weakening:
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 -
show ?thesis
by (metis UnE V_var.prems(2) ‹atom x ∉ supp B› singletonI subset_iff supp_at_base v.supp(2))
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)
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 ⟦ 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 -
show ?thesis
by (metis UnE V_var.prems(2) ‹atom x ∉ supp B› singletonI subset_iff supp_at_base v.supp(2))
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)
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' ⟦ 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_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 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_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
case (eval_e_leqI 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
next
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' ⟦ e ⟧ ~ s" and "i = i' |` d" and "supp e ⊆ atom ` d ∪ supp B "
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_eqI i v1 n1 v2 n2)
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)
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 ?case using ce.supp eval_e.intros
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 ⟦ 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_restrict by auto
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 Γ'::Γ and Γ::Γ
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 subset_iff
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 ⊨ Γ" and "i' = i |` d" and "atom_dom Γ ⊆ atom ` d" and "Θ ; B ⊢⇩w⇩f Γ"
shows "i' ⊨ Γ"
using assms proof(induct Γ rule: Γ_induct)
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) #⇩Γ G ⊢⇩w⇩f 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 Γ'::Γ and Γ::Γ
assumes "toSet Γ ⊆ toSet Γ'" and "i' ⊨ Γ'" and "i = i' |` (fst ` toSet Γ)" and "Θ ; B ⊢⇩w⇩f Γ"
shows "i ⊨ Γ"
using assms is_satis_g_restrict1[OF assms(1) assms(2)] is_satis_g_restrict2[OF _ assms(3)] by simp
subsection ‹Updating valuation›
lemma is_satis_c_i_upd:
fixes c::c
assumes "atom x ♯ c" and "i ⊨ c"
shows "((i ( x ↦s))) ⊨ c"
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 (GCons x' b' c' G')
hence *:"atom x ♯ G' ∧ atom x ♯ c'"
using fresh_def fresh_GCons GCons by force
moreover hence "is_satis ((i ( x ↦s))) c'"
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:
assumes "Θ ; B ; Γ ⊨ c" and "toSet Γ ⊆ toSet Γ'" and "wfG Θ B Γ'"
shows "Θ ; B ; Γ' ⊨ c"
proof -
have "wfC Θ B Γ c" using assms valid.simps by auto
hence sp: "supp c ⊆ atom `(fst `toSet Γ) ∪ supp B" using wfX_wfY wfG_elims
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 Θ Γ' i ∧ i ⊨ Γ' ⟶ i ⊨ c)" proof(rule allI, rule impI)
fix i
assume as: "wfI Θ Γ' i ∧ i ⊨ Γ'"
hence as1: "fst ` toSet Γ ⊆ dom i" using assms wfI_domi by blast
obtain i' where idash: "i' = restrict_map i (fst `toSet Γ)" by blast
hence as2: "dom i' = (fst `toSet Γ)" using dom_restrict as1 by auto
have id2: "Θ ; Γ ⊢ i' ∧ i' ⊨ Γ" proof -
have "wfI Θ Γ i'" using as2 wfI_restrict_weakening[of Θ Γ' i i' Γ] as assms
using idash by blast
moreover have "i' ⊨ Γ" using is_satis_g_restrict[OF assms(2)] wfg as idash by auto
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 blast
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 ⊨ G"
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: "xbc=(x,b,c)"
using prod_cases3 by blast
hence " i ⊨ (xbc #⇩Γ (x2 @ G))" using append_g.simps GCons by fastforce
then show ?case using is_satis_g.simps GCons xbc by blast
qed
lemma wfG_inside_valid2:
fixes x::x and Γ::Γ and c0::c and c0'::c
assumes "wfG Θ B (Γ'@((x,b0,c0')#⇩ΓΓ))" and
"Θ ; B ; Γ'@(x,b0,c0)#⇩ΓΓ ⊨ c0'"
shows "wfG Θ B (Γ'@((x,b0,c0)#⇩ΓΓ))"
proof -
have "wfG Θ B (Γ'@(x,b0,c0)#⇩ΓΓ)" using valid.simps wfC_wf assms by auto
thus ?thesis using wfG_replace_inside_full assms by auto
qed
lemma valid_trans:
assumes " Θ ; ℬ ; Γ ⊨ c0[z::=v]⇩v" and " Θ ; ℬ ; (z,b,c0)#⇩ΓΓ ⊨ c1" and "atom z ♯ Γ" and "wfV Θ ℬ Γ v b"
shows " Θ ; ℬ ; Γ ⊨ c1[z::=v]⇩v"
proof -
have *:"wfC Θ ℬ ((z,b,c0)#⇩ΓΓ) c1" using valid.simps assms by auto
hence "wfC Θ ℬ Γ (c1[z::=v]⇩v)" using wf_subst1(2)[OF * , of GNil ] assms subst_gv.simps subst_v_c_def by force
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 ∧ wfRCV Θ sv b" using eval_v_exist assms by metis
hence "is_satis i (c0[z::=v]⇩v)" using assms valid.simps as by metis
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)#⇩ΓΓ)"
using is_satis_g.simps by simp
moreover have "wfI Θ ((z,b,c0)#⇩ΓΓ) (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 "Θ ; ℬ ; ((x, b, c1[z1::=V_var x]⇩v) #⇩Γ Γ) ⊨ c2[z2::=V_var x]⇩v" and
"Θ ; ℬ ; ((x, b, c2[z2::=V_var x]⇩v) #⇩Γ Γ) ⊨ c3[z3::=V_var x]⇩v"
shows "Θ ; ℬ ; ((x, b, c1[z1::=V_var x]⇩v) #⇩Γ Γ) ⊨ c3[z3::=V_var x]⇩v"
unfolding valid.simps proof
show "Θ ; ℬ ; (x, b, c1[z1::=V_var x]⇩v) #⇩Γ Γ ⊢⇩w⇩f c3[z3::=V_var x]⇩v" using wf_trans valid.simps assms by metis
show "∀i. ( wfI Θ ((x, b, c1[z1::=V_var x]⇩v) #⇩Γ Γ) i ∧ (is_satis_g i ((x, b, c1[z1::=V_var x]⇩v) #⇩Γ Γ)) ⟶ (is_satis i (c3[z3::=V_var x]⇩v)) ) "
proof(rule,rule)
fix i
assume as: "Θ ; (x, b, c1[z1::=V_var x]⇩v) #⇩Γ Γ ⊢ i ∧ i ⊨ (x, b, c1[z1::=V_var x]⇩v) #⇩Γ Γ"
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' ⟦ c ⟧ ~ s" and "atom x ♯ c" and "i = i' (x ↦ s')"
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
case (eval_v_pairI i v1 s1 v2 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 show ?case using eval_v.intros by auto
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
case (eval_e_leqI i v1 n1 v2 n2)
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
next
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'" using fresh_GCons fresh_prodN by simp
moreover hence "i ⊨ c'" using is_satis_weakening_x is_satis_g.simps(2) GCons by metis
then show ?case using is_satis_g.simps(2)[of i x' b' c' Γ'] GCons fresh_GCons by simp
qed
section ‹Base Type Substitution›
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.
›
inductive boxed_b :: "Θ ⇒ rcl_val ⇒ b ⇒ bv ⇒ b ⇒ rcl_val ⇒ bool" ( " _ ⊢ _ ~ _ [ _ ::= _ ] ∖ _ " [50,50] 50) where
boxed_b_BVar1I: "⟦ bv = bv' ; wfRCV P s b ⟧ ⟹ boxed_b P s (B_var bv') bv b (SUt s)"
| 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:"wfRCV P s B_bool ⟹ boxed_b P s B_bool _ _ s "
| 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:"⟦
AF_typedef tyid dclist ∈ set P;
(dc, ⦃ x : b | c ⦄) ∈ set dclist ;
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');
(dc, ⦃ x : b | c ⦄) ∈ set dclist ;
boxed_b P s1 (b[bva::=b1]⇩b⇩b) bv b' s1'
⟧ ⟹
boxed_b P (SConsp tyid dc b1[bv::=b']⇩b⇩b s1) (B_app tyid b1) bv b' (SConsp tyid dc b1 s1')"
| boxed_b_Bbitvec: "wfRCV P s B_bitvec ⟹ boxed_b P s B_bitvec bv b s"
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 "⊢⇩w⇩f P"
shows "wfRCV P s b[bv::=b']⇩b⇩b ∧ 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' ]⇩b⇩b = b" using fresh_def subst_b_b_def forget_subst[of "bv" b b'] by auto
hence " P ⊢ SCons tyid dc s1 : (B_id tyid)" using wfRCV.intros rcl_val.supp subst_bb.simps boxed_b_BConsI by metis
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 metis
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']⇩b⇩b s1, B_app tyid b1[bv::=b']⇩b⇩b))"
using obtain_fresh_bv by metis
then obtain x2 and b2 and c2 where **:‹(dc, ⦃ x2 : b2 | c2 ⦄) ∈ set dclist2›
using boxed_b_BConspI td_lookup_eq_iff type_def.eq_iff by metis
have "P ⊢ SConsp tyid dc b1[bv::=b']⇩b⇩b s1 : (B_app tyid b1[bv::=b']⇩b⇩b)" proof
show 1: ‹AF_typedef_poly tyid bva2 dclist2 ∈ set P› using boxed_b_BConspI * by auto
show 2: ‹(dc, ⦃ x2 : b2 | c2 ⦄) ∈ set dclist2› using boxed_b_BConspI using ** by simp
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 ≠ bva2" using * fresh_Pair fresh_at_base by metis
ultimately show ?thesis using fresh_def by force
qed
moreover have "b[bva::=b1]⇩b⇩b = b2[bva2::=b1]⇩b⇩b" using wfTh_typedef_poly_b_eq_iff * 2 boxed_b_BConspI by metis
ultimately show ‹ P ⊢ s1 : b2[bva2::=b1[bv::=b']⇩b⇩b]⇩b⇩b› using boxed_b_BConspI subst_b_b_def subst_bb_commute by auto
show "atom bva2 ♯ (P, SConsp tyid dc b1[bv::=b']⇩b⇩b s1, B_app tyid b1[bv::=b']⇩b⇩b)" using * fresh_Pair by metis
qed
moreover have "P ⊢ SConsp tyid dc b1 s1' : B_app tyid b1" proof
show ‹AF_typedef_poly tyid bva dclist ∈ set P› using boxed_b_BConspI by auto
show ‹(dc, ⦃ x : b | c ⦄) ∈ set dclist› using boxed_b_BConspI by auto
show ‹ P ⊢ s1' : b[bva::=b1]⇩b⇩b› using boxed_b_BConspI by auto
have "atom bva ♯ P" using boxed_b_BConspI wfTh_fresh by metis
thus "atom bva ♯ (P, SConsp tyid dc b1 s1', B_app tyid b1)" using boxed_b_BConspI rcl_val.fresh b.fresh pure_fresh fresh_prodN by metis
qed
ultimately show ?case using subst_bb.simps by simp
qed(auto)+
lemma subst_b_var:
assumes "B_var bv2 = b[bv::=b']⇩b⇩b"
shows "(b = B_var bv ∧ b' = B_var bv2) ∨ (b=B_var bv2 ∧ bv ≠ bv2)"
using assms by(nominal_induct b rule: b.strong_induct,auto+)
text ‹Here the valuation i' is the conv wrap version of i. For every x in G, i' x is the conv wrap version of i x.
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: "⟦ Some s = i x; boxed_b Θ s b bv b' s' ; Θ ; Γ ; b' , bv ⊢ i ≈ i' ⟧ ⟹ Θ ; ((x,b,c)#⇩ΓΓ) ; b' , bv ⊢ i ≈ (i'(x ↦ s'))"
equivariance boxed_i
nominal_inductive boxed_i .
inductive_cases boxed_i_elims:
"Θ ;GNil ; b , bv ⊢ i ≈ i'"
"Θ ; ((x,b,c)#⇩ΓΓ) ; b' , bv ⊢ i ≈ i'"
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 ∧ (dc, ⦃ x1 : b1 | c1 ⦄) ∈ set dclist ∧ T ⊢ s : b1[bva::=bdc]⇩b⇩b ∧ atom bva ♯ tm"
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_ex:
assumes "wfRCV T s b[bv::=b']⇩b⇩b" and "wfTh T"
shows "∃s'. boxed_b T s b bv b' s'"
using assms proof(nominal_induct s arbitrary: b rule: rcl_val.strong_induct)
case (SBitvec x)
have *:"b[bv::=b']⇩b⇩b = 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']⇩b⇩b = B_int" using wfRCV_elims(10)[OF SNum(1)] by metis
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
ultimately show ?thesis using boxed_b_BVar1I wfRCV.intros by metis
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']⇩b⇩b = 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
next
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']⇩b⇩b = B_pair b1 b2 ∧ wfRCV T s1 b1 ∧ wfRCV T s2 b2" using wfRCV_elims(12) by metis
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 "b' = B_pair b1 b2" using True SPair subst_bb.simps(1) * by simp
ultimately show ?thesis using boxed_b_BVar1I by metis
next
case False
then obtain b1' and b2' where "b = B_pair b1' b2' ∧ b1=b1'[bv::=b']⇩b⇩b ∧ b2=b2'[bv::=b']⇩b⇩b" using subst_bb_inject(5)[OF _ False ] * by metis
then show ?thesis using * SPair boxed_b_BPairI by blast
qed
next
case (SCons tyid dc s1)
have *:"b[bv::=b']⇩b⇩b = B_id tyid" using wfRCV_elims(13)[OF SCons(2)] by metis
show ?case proof (cases "b = B_var bv")
case True
moreover have "T ⊢ SCons tyid dc s1 : B_id 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, ⦃ x : b2 | c ⦄) ∈ set dclist ∧ wfRCV T s1 b2" using wfRCV_elims(13) * SCons by metis
then have "atom bv ♯ b2" using ‹wfTh T› wfTh_lookup_supp_empty[of tyid dclist T dc "⦃ x : b2 | c ⦄"] τ.fresh fresh_def by auto
then have "b2 = b2[ bv ::= b']⇩b⇩b" using forget_subst subst_b_b_def by metis
then obtain s1' where s1:"T ⊢ s1 ~ b2 [ bv ::= b' ] ∖ s1'" using SCons ** by metis
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 ⦄) ∈ set dclist" using ** by auto
show "T ⊢ s1 ~ b2 [ bv ::= b' ] ∖ s1' " using s1 ** by auto
qed
thus ?thesis using beq by metis
qed
next
case (SConsp typid dc bdc s)
obtain bva dclist x1 b1 c1 where **:"b[bv::=b']⇩b⇩b = B_app typid bdc ∧
AF_typedef_poly typid bva dclist ∈ set T ∧ (dc, ⦃ x1 : b1 | c1 ⦄) ∈ set dclist ∧ T ⊢ s : b1[bva::=bdc]⇩b⇩b ∧ atom bva ♯ bv"
using wfRCV_poly_elims[OF SConsp(2)] by metis
then have *:"B_app typid bdc = b[bv::=b']⇩b⇩b" using wfRCV_elims(14)[OF SConsp(2)] by metis
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 subst_bb.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']⇩b⇩b" using * subst_bb_inject(8)[OF *] by metis
have "atom bv ♯ b1" proof -
have "supp b1 ⊆ { atom bva }" using wfTh_poly_supp_b ** SConsp by metis
moreover have "bv ≠ bva" using ** by auto
ultimately show ?thesis using fresh_def by force
qed
have "T ⊢ s : b1[bva::=bdc]⇩b⇩b" using ** by auto
moreover have "b1[bva::=bdc']⇩b⇩b[bv::=b']⇩b⇩b = b1[bva::=bdc]⇩b⇩b" using bdc subst_bb_commute ‹atom bv ♯ b1› by auto
ultimately obtain s' where s':"T ⊢ s ~ b1[bva::=bdc']⇩b⇩b [ bv ::= b' ] ∖ s'"
using SConsp(1)[of "b1[bva::=bdc']⇩b⇩b"] bdc SConsp by metis
have "T ⊢ SConsp typid dc bdc'[bv::=b']⇩b⇩b s ~ (B_app typid bdc') [ bv ::= b' ] ∖ SConsp typid dc bdc' s'"
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 c3 where 4:"(dc, ⦃ x3 : b3 | c3 ⦄) ∈ set dclist3"
using boxed_b_BConspI td_lookup_eq_iff type_def.eq_iff
by (metis "**")
show ?thesis proof
show ‹AF_typedef_poly typid bva3 dclist3 ∈ set T› using 3 ** by metis
show ‹atom bva3 ♯ (bdc', bv, b', s, s')› using 3 by metis
show 4:‹(dc, ⦃ x3 : b3 | c3 ⦄) ∈ set dclist3› using 4 by auto
have "b3[bva3::=bdc']⇩b⇩b = b1[bva::=bdc']⇩b⇩b" proof(rule wfTh_typedef_poly_b_eq_iff)
show ‹AF_typedef_poly typid bva3 dclist3 ∈ set T› using 3 ** by metis
show ‹(dc, ⦃ x3 : b3 | c3 ⦄) ∈ set dclist3› using 4 by auto
show ‹AF_typedef_poly typid bva dclist ∈ set T› using ** by auto
show ‹(dc, ⦃ x1 : b1 | c1 ⦄) ∈ set dclist› using ** by auto
qed(simp add: ** SConsp)
thus ‹ T ⊢ s ~ b3[bva3::=bdc']⇩b⇩b [ bv ::= b' ] ∖ s' › using s' by auto
qed
qed
then show ?thesis using bdc by auto
qed
next
case SUnit
have *:"b[bv::=b']⇩b⇩b = B_unit" using wfRCV_elims SUnit by metis
show ?case proof (cases "b = B_var bv")
case True
moreover have "T ⊢ 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']⇩b⇩b= B_var bv'" using wfRCV_elims by metis
show ?case proof (cases "b = B_var bv")
case True
then show ?thesis using boxed_b_BVar1I
using "local.*" wfRCV_BVarI by fastforce
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 "wfI T Γ[bv::=b]⇩Γ⇩b i" and "wfTh T"
shows "∃i'. T ; Γ ; b , bv ⊢ i ≈ i'"
using assms proof(induct Γ arbitrary: i rule:Γ_induct)
case GNil
then show ?case using boxed_i_GNilI by metis
next
case (GCons x' b' c' Γ')
then obtain s where 1:"Some s = i x' ∧ wfRCV T s b'[bv::=b]⇩b⇩b" using wfI_def subst_gb.simps by auto
then obtain s' where 2: "boxed_b T s b' bv b s'" using boxed_b_ex GCons by metis
then obtain i' where 3: "boxed_i T Γ' b bv i i'" using GCons wfI_def subst_gb.simps by force
have "boxed_i T ((x', b', c') #⇩Γ Γ') b bv i (i'(x' ↦ s'))" proof
show "Some s = i x'" using 1 by auto
show "boxed_b T s b' bv b s'" using 2 by auto
show "T ; Γ' ; b , bv ⊢ i ≈ i'" using "3" by auto
qed
thus ?case by auto
qed
lemma boxed_b_eq:
assumes "boxed_b Θ s1 b bv b' s1'" and "⊢⇩w⇩f Θ"
shows "wfTh Θ ⟹ boxed_b Θ s2 b bv b' s2' ⟹ ( s1 = s2 ) = ( s1' = s2' )"
using assms proof(induct arbitrary: s2 s2' rule: boxed_b.inducts )
case (boxed_b_BVar1I bv bv' P s b )
then show ?case
using boxed_b_elims(1) rcl_val.eq_iff by metis
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 by auto
next
case (boxed_b_BBoolI P s uw ux)
hence "s2 = s2'" using boxed_b_elims by metis
then show ?case by auto
next
case (boxed_b_BUnitI P s uy uz)
hence "s2 = s2'" using boxed_b_elims by metis
then show ?case by auto
next
case (boxed_b_BPairI P s1 b1 bv b s1' s2a b2 s2a')
then show ?case
by (metis boxed_b_elims(5) rcl_val.eq_iff(4))
next
case (boxed_b_BConsI tyid dclist P dc x b c s1 bv b' s1')
obtain s22 and s22' dclist2 dc2 x2 b2 c2 where *:"s2 = SCons tyid dc2 s22 ∧ s2' = SCons tyid dc2 s22' ∧ boxed_b P s22 b2 bv b' s22'
∧ AF_typedef tyid dclist2 ∈ set P ∧ (dc2, ⦃ x2 : b2 | c2 ⦄) ∈ set dclist2" using boxed_b_elims(6)[OF boxed_b_BConsI(6)] by metis
show ?case proof(cases "dc = dc2")
case True
hence "b = b2" using wfTh_ctor_unique τ.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_BConsI by simp
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 b1 bv b' s1 s1' dc x b c)
obtain bva2 s22 s22' dclist2 dc2 x2 b2 c2 where *:"
s2 = SConsp tyid dc2 b1[bv::=b']⇩b⇩b s22 ∧
s2' = SConsp tyid dc2 b1 s22' ∧
boxed_b P s22 b2[bva2::=b1]⇩b⇩b bv b' s22' ∧
AF_typedef_poly tyid bva2 dclist2 ∈ set P ∧ (dc2, ⦃ x2 : b2 | c2 ⦄) ∈ 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 ∈ set P ∧ (dc, ⦃ x2 : b2 | c2 ⦄) ∈ set dclist2" using * by auto
hence "b[bva::=b1]⇩b⇩b = b2[bva2::=b1]⇩b⇩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
lemma bs_boxed_var:
assumes "boxed_i Θ Γ b' bv i i'"
shows "Some (b,c) = lookup Γ x ⟹ Some s = i x ⟹ Some s' = i' x ⟹ boxed_b Θ 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 Θ b1 bv b' s' Γ 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:
assumes "⟦ l ⟧ = s"
shows "boxed_b Θ 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
assumes "boxed_i Θ Γ b' bv i i'" and "i ⟦ v[bv::=b']⇩v⇩b ⟧ ~ s" and "i' ⟦ v ⟧ ~ s'" and "wfV Θ B Γ v b" and "wfI Θ Γ i'"
shows "boxed_b Θ s b bv b' s'"
using assms proof(nominal_induct v arbitrary: s s' b rule:v.strong_induct)
case (V_lit l)
hence "⟦ l ⟧ = s ∧ ⟦ l ⟧ = 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)
hence "Some s = i x ∧ Some s' = i' x" using eval_v_elims subst_vb.simps by metis
moreover obtain c1 where bc:"Some (b,c1) = lookup Γ x" using wfV_elims V_var by metis
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 metis
obtain s1 and s2 where s: "eval_v i (v1[bv::=b']⇩v⇩b) s1 ∧ eval_v i (v2[bv::=b']⇩v⇩b) s2 ∧ s = SPair s1 s2" using eval_v_elims V_pair subst_vb.simps by metis
obtain s1' and s2' where s': "eval_v i' v1 s1' ∧ eval_v i' v2 s2' ∧ s' = SPair s1' s2'" using eval_v_elims V_pair by metis
have "boxed_b Θ (SPair s1 s2) (B_pair b1 b2) bv b' (SPair s1' s2') " proof(rule boxed_b_BPairI)
show "boxed_b Θ s1 b1 bv b' s1'" using V_pair eval_v_elims wfV_elims b s s' b.eq_iff by metis
show "boxed_b Θ s2 b2 bv b' s2'" using V_pair eval_v_elims wfV_elims b s s' b.eq_iff by metis
qed
then show ?case using s s' b by auto
next
case (V_cons tyid dc v1)
obtain dclist x b1 c where *: "b = B_id tyid ∧ AF_typedef tyid dclist ∈ set Θ ∧ (dc, ⦃ x : b1 | c ⦄) ∈ set dclist ∧ Θ ; B ; Γ ⊢⇩w⇩f v1 : b1"
using wfV_elims(4)[OF V_cons(5)] V_cons by metis
obtain s2 where s2: "s = SCons tyid dc s2 ∧ i ⟦ (v1[bv::=b']⇩v⇩b) ⟧ ~ s2" using eval_v_elims V_cons subst_vb.simps by metis
obtain s2' where s2': "s' = SCons tyid dc s2' ∧ i' ⟦ v1 ⟧ ~ s2'" using eval_v_elims V_cons by metis
have sp: "supp ⦃ x : b1 | c ⦄ = {}" using wfTh_lookup_supp_empty * wfX_wfY by metis
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 ∈ set Θ" using * by auto
show 2:"(dc, ⦃ x : b1 | c ⦄) ∈ set dclist" using * by auto
have bvf:"atom bv ♯ b1" using sp τ.fresh fresh_def by auto
show "Θ ⊢ s2 ~ b1 [ bv ::= b' ] ∖ s2'" using V_cons s2 s2' * by metis
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 ∧ AF_typedef_poly tyid bv2 dclist ∈ set Θ ∧
(dc, ⦃ x2 : b2 | c2 ⦄) ∈ set dclist ∧ Θ ; B ; Γ ⊢⇩w⇩f v1 : b2[bv2::=b1]⇩b⇩b"
using wf_strong_elim(1)[OF V_consp (5)] by metis
obtain s2 where s2: "s = SConsp tyid dc b1[bv::=b']⇩b⇩b s2 ∧ i ⟦ (v1[bv::=b']⇩v⇩b) ⟧ ~ s2"
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 eval_v_elims V_consp by metis
have "⊢⇩w⇩f Θ" using V_consp wfX_wfY by metis
then obtain bv3::bv and dclist3 x3 b3 c3 where **:" AF_typedef_poly tyid bv2 dclist = AF_typedef_poly tyid bv3 dclist3 ∧
(dc, ⦃ x3 : b3 | c3 ⦄) ∈ set dclist3 ∧ atom bv3 ♯ (b1, bv, b', s2, s2') ∧ b2[bv2::=b1]⇩b⇩b = b3[bv3::=b1]⇩b⇩b"
using * obtain_fresh_bv_dclist_b_iff[where tm="(b1, bv, b', s2, s2')"] by metis
have "boxed_b Θ (SConsp tyid dc b1[bv::=b']⇩b⇩b s2) (B_app tyid b1) bv b' (SConsp tyid dc b1 s2')"
proof(rule boxed_b_BConspI[of tyid bv3 dclist3 Θ, where x=x3 and b=b3 and c=c3])
show 1:"AF_typedef_poly tyid bv3 dclist3 ∈ set Θ" using * ** by auto
show 2:"(dc, ⦃ x3 : b3 | c3 ⦄) ∈ set dclist3" using ** by auto
show "atom bv3 ♯ (b1, bv, b', s2, s2')" using ** by auto
show " Θ ⊢ s2 ~ b3[bv3::=b1]⇩b⇩b [ bv ::= b' ] ∖ s2'" using V_consp s2 s2' * ** by metis
qed
then show ?case using * s2 s2' by simp
qed
lemma boxed_b_eq_eq:
assumes "boxed_b Θ n1 b1 bv b' n1'" and "boxed_b Θ n2 b1 bv b' n2'" and "s = SBool (n1 = n2)" and "⊢⇩w⇩f Θ"
"s' = SBool (n1' = n2')"
shows "s=s'"
using boxed_b_eq assms by auto
lemma boxed_i_eval_ce_boxed_b:
fixes e::ce
assumes "i' ⟦ e ⟧ ~ s'" and "i ⟦ e[bv::=b']⇩c⇩e⇩b ⟧ ~ s" and "wfCE Θ B Γ e b" and "boxed_i Θ Γ b' bv i i'" and "wfI Θ Γ i'"
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 x)
then show ?case using boxed_i_eval_v_boxed_b eval_e_elims wfCE_elims subst_ceb.simps by metis
next
case (CE_op opp v1 v2)
show ?case proof(rule opp.exhaust)
assume ‹opp = Plus›
have 1:"wfCE Θ B Γ v1 (B_int)" using wfCE_elims CE_op ‹opp = Plus› by metis
have 2:"wfCE Θ B Γ v2 (B_int)" using wfCE_elims CE_op ‹opp = Plus› by metis
have *:"b = B_int" using CE_op wfCE_elims
by (metis ‹opp = plus›)
obtain n1 and n2 where n:"s = SNum (n1 + n2) ∧ i ⟦ v1[bv::=b']⇩c⇩e⇩b ⟧ ~ SNum n1 ∧ i ⟦ v2[bv::=b']⇩c⇩e⇩b ⟧ ~ SNum n2" using eval_e_elims CE_op subst_ceb.simps ‹opp = plus› by metis
obtain n1' and n2' where n':"s' = SNum (n1' + n2') ∧ i' ⟦ v1 ⟧ ~ SNum n1' ∧ i' ⟦ v2 ⟧ ~ SNum n2'" using eval_e_elims Plus CE_op ‹opp = plus› by metis
have "boxed_b Θ (SNum n1) B_int bv b' (SNum n1')" using boxed_i_eval_v_boxed_b 1 2 n n' CE_op ‹opp = plus› by metis
moreover have "boxed_b Θ (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 ‹opp = LEq›
have 1:"wfCE Θ B Γ v1 (B_int)" using wfCE_elims CE_op ‹opp = LEq› by metis
have 2:"wfCE Θ B Γ v2 (B_int)" using wfCE_elims CE_op ‹opp = LEq› by metis
hence *:"b = B_bool" using CE_op wfCE_elims ‹opp = LEq› by metis
obtain n1 and n2 where n:"s = SBool (n1 ≤ n2) ∧ i ⟦ v1[bv::=b']⇩c⇩e⇩b ⟧ ~ SNum n1 ∧ i ⟦ v2[bv::=b']⇩c⇩e⇩b ⟧ ~ SNum n2" using eval_e_elims subst_ceb.simps CE_op ‹opp = LEq› by metis
obtain n1' and n2' where n':"s' = SBool (n1' ≤ n2') ∧ i' ⟦ v1 ⟧ ~ SNum n1' ∧ i' ⟦ v2 ⟧ ~ SNum n2'" using eval_e_elims CE_op ‹opp = LEq› by metis
have "boxed_b Θ (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 Θ (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.intros ‹opp = LEq› by simp
next
assume ‹opp = Eq›
obtain b1 where b1:"wfCE Θ B Γ v1 b1 ∧ wfCE Θ B Γ v2 b1" using wfCE_elims CE_op ‹opp = Eq› by metis
hence *:"b = B_bool" using CE_op wfCE_elims ‹opp = Eq› by metis
obtain n1 and n2 where n:"s = SBool (n1 = n2) ∧ i ⟦ v1[bv::=b']⇩c⇩e⇩b ⟧ ~ n1 ∧ i ⟦ v2[bv::=b']⇩c⇩e⇩b ⟧ ~ n2" using eval_e_elims subst_ceb.simps CE_op ‹opp = Eq› by metis
obtain n1' and n2' where n':"s' = SBool (n1' = n2') ∧ i' ⟦ v1 ⟧ ~ n1' ∧ i' ⟦ v2 ⟧ ~ n2'" using eval_e_elims CE_op ‹opp = Eq› by metis
have "boxed_b Θ n1 b1 bv b' n1'" using boxed_i_eval_v_boxed_b b1 n n' CE_op by metis
moreover have "boxed_b Θ n2 b1 bv b' n2'" using boxed_i_eval_v_boxed_b b1 n n' CE_op by metis
moreover have "⊢⇩w⇩f Θ" using b1 wfX_wfY by metis
ultimately have "s=s'" using n' n boxed_b_elims
boxed_b_eq_eq by metis
thus ?thesis using * n n' boxed_b_BBoolI CE_op wfRCV.intros ‹opp = Eq› by simp
qed
next
case (CE_concat v1 v2)
obtain bv1 and bv2 where s : "s = SBitvec (bv1 @ bv2) ∧ (i ⟦ v1[bv::=b']⇩c⇩e⇩b ⟧ ~ SBitvec bv1) ∧ i ⟦ v2[bv::=b']⇩c⇩e⇩b ⟧ ~ SBitvec bv2"
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') ∧ i' ⟦ v1 ⟧ ~ SBitvec bv1' ∧ i' ⟦ v2 ⟧ ~ SBitvec bv2'"
using eval_e_elims(7) CE_concat by metis
then show ?case using boxed_i_eval_v_boxed_b wfCE_elims s s' CE_concat
by (metis CE_concat.prems(3) assms assms(5) wfRCV_BBitvecI boxed_b_Bbitvec boxed_b_elims(7) eval_e_concatI eval_e_uniqueness)
next
case (CE_fst ce)
obtain s2 where 1:"i ⟦ ce[bv::=b']⇩c⇩e⇩b ⟧ ~ SPair s s2" using CE_fst eval_e_elims subst_ceb.simps by metis
obtain s2' where 2:"i' ⟦ ce ⟧ ~ SPair s' s2'" using CE_fst eval_e_elims by metis
obtain b2 where 3:"wfCE Θ B Γ ce (B_pair b b2)" using wfCE_elims(4) CE_fst by metis
have "boxed_b Θ (SPair s s2) (B_pair b b2) bv b' (SPair s' s2')"
using 1 2 3 CE_fst boxed_i_eval_v_boxed_b boxed_b_BPairI by auto
thus ?case using boxed_b_elims(5) by force
next
case (CE_snd v)
obtain s1 where 1:"i ⟦ v[bv::=b']⇩c⇩e⇩b ⟧ ~ SPair s1 s" using CE_snd eval_e_elims subst_ceb.simps by metis
obtain s1' where 2:"i' ⟦ v ⟧ ~ SPair s1' s'" using CE_snd eval_e_elims by metis
obtain b1 where 3:"wfCE Θ B Γ v (B_pair b1 b )" using wfCE_elims(5) CE_snd by metis
have "boxed_b Θ (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)
obtain s1 where s: "i ⟦ v[bv::=b']⇩c⇩e⇩b ⟧ ~ SBitvec s1" using CE_len eval_e_elims subst_ceb.simps by metis
obtain s1' where s': "i' ⟦ v ⟧ ~ SBitvec s1'" using CE_len eval_e_elims by metis
have "Θ ; B ; Γ ⊢⇩w⇩f v : B_bitvec ∧ b = B_int" using wfCE_elims CE_len by metis
then show ?case using boxed_i_eval_v_boxed_b s s' CE_len
by (metis boxed_b_BIntI boxed_b_elims(7) eval_e_lenI eval_e_uniqueness subst_ceb.simps(5) wfI_wfCE_eval_e)
qed
lemma eval_c_eq_bs_boxed:
fixes c::c
assumes "i ⟦ c[bv::=b]⇩c⇩b ⟧ ~ s" and "i' ⟦ c ⟧ ~ s'" and "wfC Θ B Γ c" and "wfI Θ Γ i'" and "Θ ; Γ[bv::=b]⇩Γ⇩b ⊢ i "
and "boxed_i Θ Γ b bv i i'"
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 subst_cb.simps by metis
next
case C_false
then show ?case using eval_c_elims subst_cb.simps by metis
next
case (C_conj c1 c2)
obtain s1 and s2 where 1: "eval_c i (c1[bv::=b]⇩c⇩b) s1 ∧ eval_c i (c2[bv::=b]⇩c⇩b) s2 ∧ s = (s1∧s2)" using C_conj eval_c_elims(3) subst_cb.simps(3) by metis
obtain s1' and s2' where 2:"eval_c i' c1 s1' ∧ eval_c i' c2 s2' ∧ s' = (s1'∧s2')" using C_conj eval_c_elims(3) by metis
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]⇩c⇩b) s1 ∧ eval_c i (c2[bv::=b]⇩c⇩b) s2 ∧ s = (s1∨s2)" using C_disj eval_c_elims(4) subst_cb.simps(4) by metis
obtain s1' and s2' where 2:"eval_c i' c1 s1' ∧ eval_c i' c2 s2' ∧ s' = (s1'∨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 ⟦ c[bv::=b]⇩c⇩b ⟧ ~ s1) ∧ (s = (¬ s1))" using C_not eval_c_elims(6) subst_cb.simps(7) by metis
obtain s1'::bool where 2: "(i' ⟦ c ⟧ ~ s1') ∧ (s' = (¬ 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]⇩c⇩b) s1 ∧ eval_c i (c2[bv::=b]⇩c⇩b) s2 ∧ s = (s1 ⟶ 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' ∧ eval_c i' c2 s2' ∧ s' = (s1' ⟶ 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 Θ B Γ e1 be ∧ wfCE Θ B Γ e2 be" using C_eq wfC_elims by metis
obtain s1 and s2 where 1: "eval_e i (e1[bv::=b]⇩c⇩e⇩b) s1 ∧ eval_e i (e2[bv::=b]⇩c⇩e⇩b) s2 ∧ 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' ∧ eval_e i' e2 s2' ∧ s' = (s1' = s2' )" using C_eq eval_c_elims(7) by metis
have "⊢⇩w⇩f Θ" using C_eq wfX_wfY by metis
moreover have "Θ ; Γ[bv::=b]⇩Γ⇩b ⊢ i " using C_eq by auto
ultimately show ?case using boxed_b_eq[of Θ 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 Θ Γ b bv i i'" and "wfC Θ B Γ c" and "wfI Θ Γ[bv::=b]⇩Γ⇩b i" and "Θ ; Γ ⊢ i'"
and "(i ⊨ c[bv::=b]⇩c⇩b)"
shows "(i' ⊨ c)"
proof -
have "eval_c i (c[bv::=b]⇩c⇩b) True" using is_satis.simps assms by auto
moreover obtain s where "i' ⟦ c ⟧ ~ 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 Θ Γ b bv i i'" and "wfC Θ B Γ c" and "wfI Θ Γ[bv::=b]⇩Γ⇩b i" and "Θ ; Γ ⊢ i'" and "wfC Θ {||} Γ[bv::=b]⇩Γ⇩b (c[bv::=b]⇩c⇩b)"
and "(i' ⊨ c)"
shows "(i ⊨ c[bv::=b]⇩c⇩b)"
proof -
have "eval_c i' c True" using is_satis.simps assms by auto
moreover obtain s where "i ⟦ c[bv::=b]⇩c⇩b ⟧ ~ 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 Θ::Θ and B::ℬ
assumes "boxed_i Θ Γ b bv i i'" and "wfI Θ Γ[bv::=b]⇩Γ⇩b i" and "⊢⇩w⇩f Θ" and "wfG Θ B Γ"
shows "Θ ; Γ ⊢ 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) ∈ toSet ((x1, b1, c1) #⇩Γ G)"
then consider (hd) "(x2,b2,c2) = (x1, b1, c1)" | (tail) "(x2,b2,c2) ∈ toSet G" using toSet.simps by auto
hence "∃s. Some s = (i'(x1 ↦ s')) x2 ∧ wfRCV T s b2" proof(cases)
case hd
hence "b1=b2" by auto
moreover have "(x2,b2[bv::=b]⇩b⇩b,c2[bv::=b]⇩c⇩b) ∈ toSet ((x1, b1, c1) #⇩Γ G)[bv::=b]⇩Γ⇩b" using hd subst_gb.simps by simp
moreover hence "wfRCV T s b2[bv::=b]⇩b⇩b" using wfI_def boxed_i_GConsI hd
proof -
obtain ss :: "b ⇒ x ⇒ (x ⇒ rcl_val option) ⇒ type_def list ⇒ rcl_val" where
"∀x1a x2a x3 x4. (∃v5. Some v5 = x3 x2a ∧ wfRCV x4 v5 x1a) = (Some (ss x1a x2a x3 x4) = x3 x2a ∧ wfRCV x4 (ss x1a x2a x3 x4) x1a)"
by moura
then have f1: "Some (ss b2[bv::=b]⇩b⇩b x1 i T) = i x1 ∧ wfRCV T (ss b2[bv::=b]⇩b⇩b x1 i T) b2[bv::=b]⇩b⇩b"
using boxed_i_GConsI.prems(1) hd wfI_def by auto
then have "ss b2[bv::=b]⇩b⇩b x1 i T = s"
by (metis (no_types) boxed_i_GConsI.hyps(1) option.inject)
then show ?thesis
using f1 by blast
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]⇩Γ⇩b i" and "wfI Θ G1 i'" and "G1 = (G2@G)" and "wfG Θ B G1"
and "(i ⊨ G[bv::=b]⇩Γ⇩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]⇩Γ⇩b i" and "wfI Θ G i'" and "wfG Θ B G"
and "(i ⊨ G[bv::=b]⇩Γ⇩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 "Θ ; {||} ⊢⇩w⇩f b" and "B = {|bv|}" and "Θ ; {|bv|} ;Γ ⊨ c"
shows "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊨ c[bv::=b]⇩c⇩b "
proof(rule validI)
show **:"Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f c[bv::=b]⇩c⇩b " using assms valid.simps wf_b_subst subst_gb.simps by metis
show "∀i. (wfI Θ Γ[bv::=b]⇩Γ⇩b i ∧ i ⊨ Γ[bv::=b]⇩Γ⇩b) ⟶ i ⊨ c[bv::=b]⇩c⇩b "
proof(rule,rule)
fix i
assume *:"wfI Θ Γ[bv::=b]⇩Γ⇩b i ∧ i ⊨ Γ[bv::=b]⇩Γ⇩b"
obtain i' where idash: "boxed_i Θ Γ b bv i i'" using boxed_i_ex wfX_wfY assms * by fastforce
have wfc: "Θ ; {|bv|} ; Γ ⊢⇩w⇩f c" using valid.simps assms by simp
have wfg: "Θ ; {|bv|} ⊢⇩w⇩f Γ" 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]⇩Γ⇩b i" using subst_gb.simps * by simp
show "wfI Θ Γ i'" using wfi by auto
show "Θ ; B ⊢⇩w⇩f Γ " using wfg assms by auto
show "i ⊨ Γ[bv::=b]⇩Γ⇩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]⇩c⇩b" proof(rule is_satis_bs_boxed_rev)
show "Θ ; Γ ; b , bv ⊢ i ≈ i'" using idash by auto
show "Θ ; B ; Γ ⊢⇩w⇩f c " using wfc assms by auto
show "Θ ; Γ[bv::=b]⇩Γ⇩b ⊢ i" using subst_gb.simps * by simp
show "Θ ; Γ ⊢ i'" using wfi by auto
show "Θ ; {||} ; Γ[bv::=b]⇩Γ⇩b ⊢⇩w⇩f c[bv::=b]⇩c⇩b " 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)]⇧c⇧e)"
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)]⇧c⇧e) (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)]⇧c⇧e) ([V_lit (L_num n2)]⇧c⇧e))"
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)]⇧c⇧e) ([V_lit (L_num n2)]⇧c⇧e)) (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))]⇧c⇧e [(V_lit (L_num n2))]⇧c⇧e)"
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))]⇧c⇧e [(V_lit (L_num n2) )]⇧c⇧e) (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 ]⇧c⇧e ⟧ ~ s" and "i ⟦ [ [ n2 ]⇧v ]⇧c⇧e ⟧ ~ 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))]⇧c⇧e [(V_lit (n2))]⇧c⇧e)"
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))]⇧c⇧e [(V_lit (n2) )]⇧c⇧e) (SBool (n1=n2))"
proof -
obtain s1 and s2 where *:"i ⟦ [ [ n1 ]⇧v ]⇧c⇧e ⟧ ~ s1 ∧ i ⟦ [ [ n2 ]⇧v ]⇧c⇧e ⟧ ~ 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))]⇧c⇧e" s1 "[(V_lit (n2))]⇧c⇧e" 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 ℬ GNil ∧ wfI P GNil i ∧ eval_e i e1 s1 ∧ eval_e i e2 s2 ⟶ s1 = s2"
and "wfCE P ℬ GNil e1 b" and "wfCE P ℬ GNil e2 b"
shows "P ; ℬ ; (x, b , CE_val (V_var x) == e1 )#⇩Γ GNil ⊨ CE_val (V_var x) == e2"
unfolding valid.simps
proof(intro conjI)
show ‹ P ; ℬ ; (x, b, [ [ x ]⇧v ]⇧c⇧e == e1 ) #⇩Γ GNil ⊢⇩w⇩f [ [ x ]⇧v ]⇧c⇧e == 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 ]⇧c⇧e == e1 ) #⇩Γ GNil ⊢ i) ∧ (i ⊨ (x, b, [ [ x ]⇧v ]⇧c⇧e == e1 ) #⇩Γ GNil) ⟶
(i ⊨ [ [ x ]⇧v ]⇧c⇧e == e2)) › proof(rule+)
fix i
assume as:"P ; (x, b, [ [ x ]⇧v ]⇧c⇧e == e1 ) #⇩Γ GNil ⊢ i ∧ i ⊨ (x, b, [ [ x ]⇧v ]⇧c⇧e == e1 ) #⇩Γ 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 ]⇧c⇧e == 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 ]⇧c⇧e == e2 ⟧ ~ True"
using eval_c.intros eval_e.intros eval_v.intros
proof -
have "i ⟦ e2 ⟧ ~ s1"
by (metis ‹s1 = s2› s2)
then show ?thesis
by (metis (full_types) ‹i x = Some s1› eval_c_eqI eval_e_valI eval_v_varI)
qed
qed
qed
lemma valid_len:
assumes " ⊢⇩w⇩f Θ"
shows "Θ ; ℬ ; (x, B_int, [[x]⇧v]⇧c⇧e == [[ L_num (int (length v)) ]⇧v]⇧c⇧e) #⇩Γ GNil ⊨ [[x]⇧v]⇧c⇧e == CE_len [[ L_bitvec v ]⇧v]⇧c⇧e" (is "Θ ; ℬ ; ?G ⊨ ?c" )
proof -
have *:"Θ ⊢⇩w⇩f ([]::Φ) ∧ Θ ; ℬ ; GNil ⊢⇩w⇩f []⇩Δ " using assms wfG_nilI wfD_emptyI wfPhi_emptyI by auto
moreover hence "Θ ; ℬ ; GNil ⊢⇩w⇩f 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 "Θ ; ℬ ; GNil ⊢⇩w⇩f CE_len [(V_lit (L_bitvec v))]⇧c⇧e : 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 "Θ ; ℬ ; ?G ⊢⇩w⇩f ?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 Θ ℬ Γ" 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 "Θ; ℬ ; (x, b, (CE_val (V_var x) == CE_val (V_lit (ll)) )) #⇩Γ Γ
⊨ (CE_val (V_var x) == CE_op opp ([V_lit (L_num n1)]⇧c⇧e) ([V_lit (L_num n2)]⇧c⇧e ))" (is "Θ ; ℬ ; ?G ⊨ ?c")
proof -
have "wfC Θ ℬ ?G ?c" proof(rule wfC_e_eq2)
show "Θ ; ℬ ; Γ ⊢⇩w⇩f CE_val (V_lit ll) : b" using wfCE_valI wfV_litI assms base_for_lit.simps by metis
show "Θ ; ℬ ; Γ ⊢⇩w⇩f CE_op opp ([V_lit (L_num n1)]⇧c⇧e) ([V_lit (L_num n2)]⇧c⇧e) : b "
using wfCE_plusI wfCE_leqI wfCE_eqI wfV_litI wfCE_valI base_for_lit.simps assms by metis
show "⊢⇩w⇩f Θ" 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)]⇧c⇧e) ([V_lit (L_num n2)]⇧c⇧e)))"
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 Θ ℬ Γ" and "atom x ♯ Γ" and "base_for_lit l1 = base_for_lit l2"
shows "Θ; ℬ ; (x, B_bool, (CE_val (V_var x) == CE_val (V_lit (if l1 = l2 then L_true else L_false)) )) #⇩Γ Γ
⊨ (CE_val (V_var x) == CE_op Eq ([V_lit (l1)]⇧c⇧e) ([V_lit (l2)]⇧c⇧e ))" (is "Θ ; ℬ ; ?G ⊨ ?c")
proof -
let ?ll = "(if l1 = l2 then L_true else L_false)"
have "wfC Θ ℬ ?G ?c" proof(rule wfC_e_eq2)
show "Θ ; ℬ ; Γ ⊢⇩w⇩f CE_val (V_lit ?ll) : B_bool" using wfCE_valI wfV_litI assms base_for_lit.simps by metis
show "Θ ; ℬ ; Γ ⊢⇩w⇩f CE_op Eq ([V_lit (l1)]⇧c⇧e) ([V_lit (l2)]⇧c⇧e) : B_bool "
using wfCE_eqI wfCE_leqI wfCE_eqI wfV_litI wfCE_valI base_for_lit.simps assms by metis
show "⊢⇩w⇩f Θ" 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)]⇧c⇧e) ([V_lit (l2)]⇧c⇧e)))"
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⇩1::v and v⇩2::v
assumes "wfTh Θ" and "wfV Θ ℬ GNil (V_pair v⇩1 v⇩2) (B_pair b⇩1 b⇩2)"
shows "Θ ; ℬ ; (x, b⇩1, [[x]⇧v]⇧c⇧e == [v⇩1]⇧c⇧e) #⇩Γ GNil ⊨ [[x]⇧v]⇧c⇧e == [#1[[v⇩1,v⇩2]⇧v]⇧c⇧e]⇧c⇧e"
proof(rule valid_eq_e)
show ‹∀i s1 s2. (Θ ; ℬ ⊢⇩w⇩f GNil) ∧ (Θ ; GNil ⊢ i) ∧ (i ⟦ [ v⇩1 ]⇧c⇧e ⟧ ~ s1) ∧ (i ⟦ [#1[[ v⇩1 , v⇩2 ]⇧v]⇧c⇧e]⇧c⇧e ⟧ ~ s2) ⟶ s1 = s2›
proof(rule+)
fix i s1 s2
assume as:"Θ ; ℬ ⊢⇩w⇩f GNil ∧ Θ ; GNil ⊢ i ∧ (i ⟦ [ v⇩1 ]⇧c⇧e ⟧ ~ s1) ∧ (i ⟦ [#1[[ v⇩1 , v⇩2 ]⇧v]⇧c⇧e]⇧c⇧e ⟧ ~ s2)"
then obtain s2' where *:"i ⟦ [ v⇩1 , v⇩2 ]⇧v ⟧ ~ SPair s2 s2'"
using eval_e_elims(5)[of i "[[ v⇩1 , v⇩2 ]⇧v]⇧c⇧e" s2] eval_e_elims
by meson
then have " i ⟦ v⇩1 ⟧ ~ 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 ‹ Θ ; ℬ ; GNil ⊢⇩w⇩f [ v⇩1 ]⇧c⇧e : b⇩1 › using assms
by (metis b.eq_iff(4) wfV_elims(3) wfV_wfCE)
show ‹ Θ ; ℬ ; GNil ⊢⇩w⇩f [#1[[ v⇩1 , v⇩2 ]⇧v]⇧c⇧e]⇧c⇧e : b⇩1 › using assms using wfCE_fstI
using wfCE_valI by blast
qed
lemma valid_snd:
fixes x::x and v⇩1::v and v⇩2::v
assumes "wfTh Θ" and "wfV Θ ℬ GNil (V_pair v⇩1 v⇩2) (B_pair b⇩1 b⇩2)"
shows "Θ ; ℬ ; (x, b⇩2, [[x]⇧v]⇧c⇧e == [v⇩2]⇧c⇧e) #⇩Γ GNil ⊨ [[x]⇧v]⇧c⇧e == [#2[[v⇩1,v⇩2]⇧v]⇧c⇧e]⇧c⇧e"
proof(rule valid_eq_e)
show ‹∀i s1 s2. (Θ ; ℬ ⊢⇩w⇩f GNil) ∧ (Θ ; GNil ⊢ i) ∧ (i ⟦ [ v⇩2 ]⇧c⇧e ⟧ ~ s1) ∧
(i ⟦ [#2[[ v⇩1 , v⇩2 ]⇧v]⇧c⇧e]⇧c⇧e ⟧ ~ s2) ⟶ s1 = s2›
proof(rule+)
fix i s1 s2
assume as:"Θ ; ℬ ⊢⇩w⇩f GNil ∧ Θ ; GNil ⊢ i ∧ (i ⟦ [ v⇩2 ]⇧c⇧e ⟧ ~ s1) ∧ (i ⟦ [#2[[ v⇩1 , v⇩2 ]⇧v]⇧c⇧e]⇧c⇧e ⟧ ~ s2)"
then obtain s2' where *:"i ⟦ [ v⇩1 , v⇩2 ]⇧v ⟧ ~ SPair s2' s2"
using eval_e_elims(5)[of i "[[ v⇩1 , v⇩2 ]⇧v]⇧c⇧e" s2] eval_e_elims
by meson
then have " i ⟦ v⇩2 ⟧ ~ 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 ‹ Θ ; ℬ ; GNil ⊢⇩w⇩f [ v⇩2 ]⇧c⇧e : b⇩2 › using assms
by (metis b.eq_iff wfV_elims wfV_wfCE)
show ‹ Θ ; ℬ ; GNil ⊢⇩w⇩f [#2[[ v⇩1 , v⇩2 ]⇧v]⇧c⇧e]⇧c⇧e : b⇩2 › using assms using wfCE_sndI wfCE_valI by blast
qed
lemma valid_concat:
fixes v1::"bit list" and v2::"bit list"
assumes " ⊢⇩w⇩f Π"
shows "Π ; ℬ ; (x, B_bitvec, (CE_val (V_var x) == CE_val (V_lit (L_bitvec (v1@ v2))))) #⇩Γ GNil ⊨
(CE_val (V_var x) == CE_concat ([V_lit (L_bitvec v1)]⇧c⇧e ) ([V_lit (L_bitvec v2)]⇧c⇧e) )"
proof(rule valid_eq_e)
show ‹∀i s1 s2. ((Π ; ℬ ⊢⇩w⇩f GNil) ∧ (Π ; GNil ⊢ i) ∧
(i ⟦ [ [ L_bitvec (v1 @ v2) ]⇧v ]⇧c⇧e ⟧ ~ s1) ∧ (i ⟦ [[[ L_bitvec v1 ]⇧v]⇧c⇧e @@ [[ L_bitvec v2 ]⇧v]⇧c⇧e ]⇧c⇧e ⟧ ~ s2) ⟶
s1 = s2)›
proof(rule+)
fix i s1 s2
assume as: "(Π ; ℬ ⊢⇩w⇩f GNil) ∧ (Π ; GNil ⊢ i) ∧ (i ⟦ [ [ L_bitvec (v1 @ v2) ]⇧v ]⇧c⇧e ⟧ ~ s1) ∧
(i ⟦ [[[ L_bitvec v1 ]⇧v]⇧c⇧e @@ [[ L_bitvec v2 ]⇧v]⇧c⇧e]⇧c⇧e ⟧ ~ s2) "
hence *: "i ⟦ [[[ L_bitvec v1 ]⇧v]⇧c⇧e @@ [[ L_bitvec v2 ]⇧v]⇧c⇧e]⇧c⇧e ⟧ ~ 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 ‹ Π ; ℬ ; GNil ⊢⇩w⇩f [ [ L_bitvec (v1 @ v2) ]⇧v ]⇧c⇧e : B_bitvec ›
by (metis assms base_for_lit.simps(5) wfG_nilI wfV_litI wfV_wfCE)
show ‹ Π ; ℬ ; GNil ⊢⇩w⇩f [[[ L_bitvec v1 ]⇧v]⇧c⇧e @@ [[ L_bitvec v2 ]⇧v]⇧c⇧e]⇧c⇧e : 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 "Θ ; ℬ ; Γ ⊢⇩w⇩f ce : b"
shows ‹Θ ; ℬ ; Γ ⊨ ce == ce ›
unfolding valid.simps proof
show ‹ Θ ; ℬ ; Γ ⊢⇩w⇩f 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 " Θ ; ℬ ; (x, b, c2) #⇩Γ Γ ⊢⇩w⇩f c1 IMP c2"
shows " Θ ; ℬ ; (x, b, c2) #⇩Γ Γ ⊨ c1 IMP c2 "
proof -
have "∀i. (Θ ; (x, b, c2) #⇩Γ Γ ⊢ i ∧ i ⊨ (x, b, c2) #⇩Γ Γ) ⟶ i ⊨ ( c1 IMP c2 )"
proof(rule,rule)
fix i
assume as:"Θ ; (x, b, c2) #⇩Γ Γ ⊢ i ∧ i ⊨ (x, b, c2) #⇩Γ Γ"
have "Θ ; ℬ ; (x, b, c2) #⇩Γ Γ ⊢⇩w⇩f 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 "⊢⇩w⇩f Θ"
shows "Θ ; {||} ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #⇩Γ GNil ⊨
(C_eq (CE_op LEq (CE_val (V_var x)) (CE_val (V_lit (L_num m)))) [[ L_true ]⇧v ]⇧c⇧e) AND
(C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]⇧v ]⇧c⇧e)"
(is "Θ ; {||} ; ?G ⊨ ?c1 AND ?c2")
proof(rule validI)
have wfg: " Θ ; {||} ⊢⇩w⇩f (x, B_int, [ [ x ]⇧v ]⇧c⇧e == [ [ L_num n ]⇧v ]⇧c⇧e ) #⇩Γ 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 ⊢⇩w⇩f ?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 ]⇧c⇧e [ [ L_num m ]⇧v ]⇧c⇧e ]⇧c⇧e⟧ ~ 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 ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e [ [ x ]⇧v ]⇧c⇧e ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e ⟧ ~ 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 " Θ ; {||} ⊢⇩w⇩f Γ" and "atom x ♯ Γ"
shows "Θ ; {||} ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #⇩Γ Γ ⊨
(C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]⇧v ]⇧c⇧e) AND
(C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]⇧v ]⇧c⇧e |]⇧c⇧e )) [[ L_true ]⇧v ]⇧c⇧e)
"
(is "Θ ; {||} ; ?G ⊨ ?c1 AND ?c2")
proof(rule validI)
have wfg: " Θ ; {||} ⊢⇩w⇩f (x, B_int, [ [ x ]⇧v ]⇧c⇧e == [ [ L_num n ]⇧v ]⇧c⇧e ) #⇩Γ Γ " 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 ⊢⇩w⇩f ?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 ]⇧c⇧e [| [ [ L_bitvec v ]⇧v ]⇧c⇧e |]⇧c⇧e ]⇧c⇧e⟧ ~ 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 ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e [ [ x ]⇧v ]⇧c⇧e ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e ⟧ ~ 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 "⊢⇩w⇩f Θ "
and "Θ ; {||} ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #⇩Γ GNil ⊨
(C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]⇧v ]⇧c⇧e) AND
(C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]⇧v ]⇧c⇧e |]⇧c⇧e )) [[ L_true ]⇧v ]⇧c⇧e)
"
(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 ]⇧c⇧e == [ [ L_num n ]⇧v ]⇧c⇧e ) ⟧ ~ 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 ]⇧c⇧e [ [ x ]⇧v ]⇧c⇧e ]⇧c⇧e ⟧ ~ sv1 ∧ i ⟦ [ [ L_true ]⇧v ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e ⟧ ~ SNum n1) ∧ (i ⟦ [ [ x ]⇧v ]⇧c⇧e ⟧ ~ SNum n2)"
using eval_e_elims(3)[of i " [ [ L_num 0 ]⇧v ]⇧c⇧e" "[ [ x ]⇧v ]⇧c⇧e " "SBool True"]
using ‹(sv1 = sv2) = True ∧ i ⟦ [ leq [ [ L_num 0 ]⇧v ]⇧c⇧e [ [ x ]⇧v ]⇧c⇧e ]⇧c⇧e ⟧ ~ sv1 ∧ i ⟦ [ [ L_true ]⇧v ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e [| [ [ L_bitvec v ]⇧v ]⇧c⇧e |]⇧c⇧e ]⇧c⇧e ⟧ ~ sv1 ∧ i ⟦ [ [ L_true ]⇧v ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e ⟧ ~ SNum n1) ∧ (i ⟦ [| [ [ L_bitvec v ]⇧v ]⇧c⇧e |]⇧c⇧e ⟧ ~ 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) #⇩Γ Γ ⊢ i"
unfolding wfI_def proof -
{
fix x' b' c'
assume "(x',b',c') ∈ toSet ((x, b, c) #⇩Γ Γ)"
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) #⇩Γ Γ). ∃s. Some s = i x ∧ Θ ⊢ s : b" by auto
qed
lemma valid_range_length_inv:
fixes Γ::Γ
assumes "Θ ; B ⊢⇩w⇩f Γ " 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))))) #⇩Γ Γ ⊨
(C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]⇧v ]⇧c⇧e) AND
(C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]⇧v ]⇧c⇧e |]⇧c⇧e )) [[ L_true ]⇧v ]⇧c⇧e)
"
(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 ]⇧c⇧e == [ [ L_num n ]⇧v ]⇧c⇧e ) ⟧ ~ 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 ]⇧c⇧e == [ [ L_num n ]⇧v ]⇧c⇧e › 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 ]⇧c⇧e [ [ x ]⇧v ]⇧c⇧e ]⇧c⇧e ⟧ ~ sv1 ∧ i ⟦ [ [ L_true ]⇧v ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e ⟧ ~ SNum n1) ∧ (i ⟦ [ [ x ]⇧v ]⇧c⇧e ⟧ ~ SNum n2)"
using eval_e_elims(3)[of i " [ [ L_num 0 ]⇧v ]⇧c⇧e" "[ [ x ]⇧v ]⇧c⇧e " "SBool True"]
using ‹(sv1 = sv2) = True ∧ i ⟦ [ leq [ [ L_num 0 ]⇧v ]⇧c⇧e [ [ x ]⇧v ]⇧c⇧e ]⇧c⇧e ⟧ ~ sv1 ∧ i ⟦ [ [ L_true ]⇧v ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e [| [ [ L_bitvec v ]⇧v ]⇧c⇧e |]⇧c⇧e ]⇧c⇧e ⟧ ~ sv1 ∧ i ⟦ [ [ L_true ]⇧v ]⇧c⇧e ⟧ ~ 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 ]⇧c⇧e ⟧ ~ SNum n1) ∧ (i ⟦ [| [ [ L_bitvec v ]⇧v ]⇧c⇧e |]⇧c⇧e ⟧ ~ 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 "⊢⇩w⇩f Θ"
shows "Θ ; {||} ; (z , [B_bitvec , B_bitvec ]⇧b , [ [ z ]⇧v ]⇧c⇧e == [ [ [ L_bitvec v1 ]⇧v , [ L_bitvec v2 ]⇧v ]⇧v ]⇧c⇧e) #⇩Γ GNil
⊨ ([ [ L_bitvec v ]⇧v ]⇧c⇧e == [ [#1[ [ z ]⇧v ]⇧c⇧e]⇧c⇧e @@ [#2[ [ z ]⇧v ]⇧c⇧e]⇧c⇧e ]⇧c⇧e) AND ([| [#1[ [ z ]⇧v ]⇧c⇧e]⇧c⇧e |]⇧c⇧e == [ [ L_num n ]⇧v ]⇧c⇧e)"
(is "Θ ; {||} ; ?G ⊨ ?c1 AND ?c2")
unfolding valid.simps proof
have wfg: " Θ ; {||} ⊢⇩w⇩f (z, [B_bitvec , B_bitvec ]⇧b , [ [ z ]⇧v ]⇧c⇧e == [ [ [ L_bitvec v1 ]⇧v , [ L_bitvec v2 ]⇧v ]⇧v ]⇧c⇧e) #⇩Γ GNil"
using wf_intros assms base_for_lit.simps fresh_GNil wfC_v_eq wfG_intros2 by metis
show "Θ ; {||} ; ?G ⊢⇩w⇩f ?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 ]⇧c⇧e == [ [ [ L_bitvec v1 ]⇧v , [ L_bitvec v2 ]⇧v ]⇧v ]⇧c⇧e ⟧ ~ True"
using is_satis_g.simps is_satis.simps by simp
then obtain sv where "i ⟦ [ [ z ]⇧v ]⇧c⇧e ⟧ ~ sv ∧ i ⟦ [ [ [ L_bitvec v1 ]⇧v , [ L_bitvec v2 ]⇧v ]⇧v ]⇧c⇧e ⟧ ~ sv"
using eval_c_elims by metis
hence "i ⟦ [ [ z ]⇧v ]⇧c⇧e ⟧ ~ (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 ]⇧c⇧e]⇧c⇧e ⟧ ~ SBitvec v1 "
using eval_e_fstI eval_e_valI eval_v_varI b by metis
have v2: "i ⟦ [#2[ [ z ]⇧v ]⇧c⇧e]⇧c⇧e ⟧ ~ SBitvec v2"
using eval_e_sndI eval_e_valI eval_v_varI b by metis
have "i ⟦ [ [ L_bitvec v ]⇧v ]⇧c⇧e ⟧ ~ SBitvec v" using eval_e.intros eval_v.intros eval_l.simps by metis
moreover have "i ⟦ [ [#1[ [ z ]⇧v ]⇧c⇧e]⇧c⇧e @@ [#2[ [ z ]⇧v ]⇧c⇧e]⇧c⇧e ]⇧c⇧e ⟧ ~ SBitvec v"
using assms split_concat v1 v2 eval_e_concatI by metis
moreover have "i ⟦ [| [#1[ [ z ]⇧v ]⇧c⇧e]⇧c⇧e |]⇧c⇧e ⟧ ~ SNum (int (length v1))"
using v1 eval_e_lenI by auto
moreover have "i ⟦ [ [ L_num n ]⇧v ]⇧c⇧e ⟧ ~ 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 Θ ℬ 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 Θ ℬ (G3@((x,b,c0)#⇩ΓG))" and "wfV Θ ℬ G v b" and "wfI Θ (G3[x::=v]⇩Γ⇩v@G) i"
and "is_satis_g i (G3[x::=v]⇩Γ⇩v@G)"
shows "is_satis_g (i ( x ↦ s)) (G3@((x,b,c0)#⇩Γ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]⇩c⇩v) #⇩Γ (Γ'[x::=v]⇩Γ⇩v) @ G))" using subst_gv.simps GCons by auto
hence *:"is_satis i c'[x::=v]⇩c⇩v ∧ is_satis_g i ((Γ'[x::=v]⇩Γ⇩v) @ G)" using subst_gv.simps by auto
have "is_satis_g (i(x ↦ s)) ((x', b', c') #⇩Γ (Γ'@ (x, b, c0) #⇩Γ 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 ‹ Θ ; ℬ ; ((x', b', c') #⇩ΓΓ')@(x, b, c0) #⇩Γ G ⊢⇩w⇩f c' › using GCons wfC_refl by auto
show ‹wfI Θ ((((x', b', c') #⇩Γ Γ')[x::=v]⇩Γ⇩v) @ G) i› using GCons by auto
show ‹ Θ ; ℬ ; G ⊢⇩w⇩f v : b › using GCons by auto
show ‹is_satis i c'[x::=v]⇩c⇩v› using * by auto
qed
show "is_satis_g (i(x ↦ s)) (Γ' @ (x, b, c0) #⇩Γ 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 ‹ Θ ; ℬ⊢⇩w⇩f Γ' @ (x, b, c0) #⇩Γ G › using GCons wfG_elims append_g.simps by metis
show ‹is_satis_g i (Γ'[x::=v]⇩Γ⇩v @ G)› using * by auto
show "wfI Θ (Γ'[x::=v]⇩Γ⇩v @ G) i" using GCons wfI_def subst_g_assoc_cons ‹x≠x'› by auto
show "Θ ; ℬ ; G ⊢⇩w⇩f v : b " using GCons by auto
qed
qed
moreover have "((x', b', c') #⇩Γ Γ' @ (x, b, c0) #⇩Γ G) = (((x', b', c') #⇩Γ Γ') @ (x, b, c0) #⇩Γ G)" by auto
ultimately show ?case using GCons by metis
qed
end