| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/MiniSail/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 146 kB |
|
Quellcode-Bibliothek RCLogicL.thySprache: Isabelle |
|||||||||||||||
|
(*<*) theory RCLogicL imports RCLogic WellformedL begin (*>*) hide_const Syntax.dom chapter ‹Refinement Constraint Logic Lemmas› section ‹Lemmas› lemma wfI_domi: assumes "Θ ; Γ ⊨ i" shows "fst ` toSet Γ ⊆ dom i" using wfI_def toSet.simps assms by fastforce lemma wfI_lookup: fixes G::Γ and b::b assumes "Some (b,c) = lookup G x" and "P ; G ⊨ i" and "Some s = i x" and "P ; B ⊨wf G" shows "P ⊨ s : b" proof - have "(x,b,c) ∈ toSet G" using lookup.simps assms using lookup_in_g by blast then obtain s' where *:"Some s' = i x ∧ wfRCV P s' b" using wfI_def assms by auto hence "s' = s" using assms by (metis option.inject) thus ?thesis using * by auto qed lemma wfI_restrict_weakening: assumes "wfI Θ Γ' i'" and "i = restrict_map i' (fst `toSet Γ)" and "toSet Γ ⊆ toSet Γ'" shows "Θ ; Γ ⊨ i" proof - { fix x assume "x ∈ toSet Γ" have "case x of (x, b, c) ==> ∃s. Some s = i x ∧ Θ ⊨ s : b" using assms wfI_def proof - have "case x of (x, b, c) ==> ∃s. Some s = i' x ∧ Θ ⊨ s : b" using ‹x ∈ toSet Γ› assms wfI_def by auto then have "∃s. Some s = i (fst x) ∧ wfRCV Θ s (fst (snd x))" by (simp add: ‹x ∈ toSet Γ› assms(2) case_prod_unfold) then show ?thesis by (simp add: case_prod_unfold) qed } thus ?thesis using wfI_def assms by auto qed lemma wfI_suffix: fixes G::Γ assumes "wfI P (G'@G) i" and "P ; B ⊨wf G" shows "P ; G ⊨ i" using wfI_def append_g.simps assms toSet.simps by simp lemma wfI_replace_inside: assumes "wfI Θ (Γ' @ (x, b, c) #\<Gamma> Γ) i" shows "wfI Θ (Γ' @ (x, b, c') #\<Gamma> Γ) i" using wfI_def toSet_splitP assms by simp section ‹Existence of evaluation› lemma eval_l_base: "Θ ⊨ [ l ] : (base_for_lit l)" apply(nominal_induct l rule:l.strong_induct) using wfRCV.intros eval_l.simps base_for_lit.simps by auto+ lemma obtain_fresh_bv_dclist: fixes tm::"'a::fs" assumes "(dc, { x : b | c }) ∈ set dclist" obtains bv1::bv and dclist1 x1 b1 c1 where "AF_typedef_poly tyid bv dclist = AF_typedef ∧ (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 using obtain_fresh_bv by metis moreover hence "[[atom bv]]lst. dclist = [[atom bv1]]lst. dclist1" using type_def.eq moreover then obtain x1 b1 c1 where "(dc, { x1 : b1 | c1 }) ∈ set dclist1" using td_look 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 ∈ s obtains bv1::bv and dclist1 x1 b1 c1 where "AF_typedef_poly tyid bv dclist = AF_typedef ∧ (dc, { x1 : b1 | c1 }) ∈ set dclist1 ∧ atom bv1 ♯ tm ∧ b[bv::=b']bb=b1[bv1::= proof - obtain bv1 dclist1 x1 b1 c1 where *:"AF_typedef_poly tyid bv dclist = AF_typedef_poly ∧ (dc, { x1 : b1 | c1 }) ∈ set dclist1" using obtain_fresh_bv_dclist assms by metis hence "AF_typedef_poly tyid bv1 dclist1 ∈ set P" using assms by metis hence "b[bv::=b']bb = b1[bv1::=b']bb" using wfTh_typedef_poly_b_eq_iff[OF assms(2) assms(1) _ _ assms(3),of bv1 dclist1 x1 b1 c1 b from this that show ?thesis using * by metis qed lemma eval_v_exist: fixes Γ::Γ and v::v and b::b assumes "P ; Γ ⊨ i" and "P ; B ; Γ ⊨wf v : b" shows "∃s. i [ v ] ~ s ∧ P ⊨ s : b " using assms proof(nominal_induct v arbitrary: b rule:v.strong_induct) case (V_lit x) then show ?case using eval_l_base eval_v.intros eval_l.simps wfV_elims rcl_val.supp pure_ next case (V_var x) then obtain c where *:"Some (b,c) = lookup Γ x" using wfV_elims by metis hence "x ∈ fst ` toSet Γ" using lookup_x by blast hence "x ∈ dom i" using wfI_domi using assms by blast then obtain s where "i x = Some s" by auto moreover hence "P ⊨ s : b" using wfRCV.intros wfI_lookup * V_var by (metis wfV_wf) ultimately show ?case using eval_v.intros rcl_val.supp b.supp by metis next case (V_pair v1 v2) then obtain b1 and b2 where *:"P ; B ; Γ ⊨wf v1 : b1 ∧ P ; B ; Γ ⊨wf v2 : b2 ∧ b = B_ then obtain s1 and s2 where "eval_v i v1 s1 ∧ wfRCV P s1 b1 ∧ eval_v i v2 s2 ∧ wfRCV P 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 ] ~ AF_typedef tyid dclist ∈ set P ∧ (dc, { x : b' | c }) ∈ set dclist" using wfV_eli then show ?case using eval_v.intros(4) wfRCV.intros(5) V_cons by metis next case (V_consp tyid dc b' v) obtain b'a::b and bv and dclist and x::x and c::c where *:"(wfV P B Γ v b'a[bv::=b']bb) ∧ AF_typedef_poly tyid bv dclist ∈ set P ∧ (dc, { x : b'a | c }) ∈ set dclist ∧ atom bv ♯ (P, B_app tyid b',B) " using wf_strong_elim(1)[OF V_consp(3)] by metis then obtain s where **:"i [ v ] ~ s ∧ P ⊨ s : b'a[bv::=b']bb" using V_consp by auto have " ⊨wf P" using wfX_wfY V_consp by metis then obtain bv1::bv and dclist1 x1 b1 c1 where 3:"AF_typedef_poly tyid bv dclist = AF_ty ∧ (dc, { x1 : b1 | c1 }) ∈ set dclist1 ∧ atom bv1 ♯ (P, SConsp tyid dc b' s, B ∧ b'a[bv::=b']bb = b1[bv1::=b']bb" using * obtain_fresh_bv_dclist_b_iff by blast have " i [ V_consp tyid dc b' v ] ~ SConsp tyid dc b' s" using eval_v.intros by (simp 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 met show ‹ P ⊨ s : b1[bv1::=b']bb› using 3 ** by auto qed ultimately show ?case using eval_v.intros wfRCV.intros V_consp * by auto qed lemma eval_v_uniqueness: fixes v::v assumes "i [ v ] ~ s" and "i [ v ] ~ s'" shows "s=s'" using assms proof(nominal_induct v arbitrary: s s' rule:v.strong_induct) case (V_lit x) then show ?case using eval_v_elims eval_l.simps by metis next case (V_var x) then show ?case using eval_v_elims by (metis option.inject) next case (V_pair v1 v2) obtain s1 and s2 where s:"i [ v1 ] ~ s1 ∧ i [ v2 ] ~ s2 ∧ s = SPair s1 s2" using eval_ obtain s1' and s2' where s':"i [ v1 ] ~ s1' ∧ i [ v2 ] ~ s2' ∧ s' = SPair s1' s2'" us 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 b moreover obtain sv2 where 2:"i [ v1 ] ~ sv2 ∧ s' = SCons tyid dc sv2" using eval_v_eli ultimately have "sv1 = sv2" using V_cons by auto then show ?case using 1 2 by auto next case (V_consp tyid dc b v1) then show ?case using eval_v_elims by metis qed lemma eval_v_base: fixes Γ::Γ and v::v and b::b assumes "P ; Γ ⊨ i" and "P ; B ; Γ ⊨wf v : b" and "i [ v ] ~ s" shows "P ⊨ s : b" using eval_v_exist eval_v_uniqueness assms by metis lemma eval_e_uniqueness: fixes e::ce assumes "i [ e ] ~ s" and "i [ e ] ~ s'" shows "s=s'" using assms proof(nominal_induct e arbitrary: s s' rule:ce.strong_induct) case (CE_val x) then show ?case using eval_v_uniqueness eval_e_elims by metis next case (CE_op opp x1 x2) consider "opp = Plus" | "opp = LEq" | "opp = Eq" using opp.exhaust by metis thus ?case proof(cases) case 1 hence a1:"eval_e i (CE_op Plus x1 x2) s" and a2:"eval_e i (CE_op Plus x1 x2) s'" usi 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 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 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 show ?case using eval_e_elims(7)[OF a1] eval_e_elims(7)[OF a2] CE_concat eval_e_concatI r proof - assume "∧P. (∧bv1 bv2. [s' = SBitvec (bv1 @ bv2); i [ x1 ] ~ SBitvec bv1 ; i [ x2 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 [ then have "s' = s" by (metis (no_types) ‹∧P. (∧bv1 bv2. [s = SBitvec (bv1 @ bv2); i [ x1 ] ~ SBitvec b then show ?thesis by metis (* 0.0 ms *) qed next case (CE_fst x) then show ?case using eval_v_uniqueness by (meson eval_e_elims rcl_val.eq_iff) next case (CE_snd x) then show ?case using eval_v_uniqueness by (meson eval_e_elims rcl_val.eq_iff) next case (CE_len x) then show ?case using eval_e_elims rcl_val.eq_iff proof - obtain bbs :: "rcl_val ==> ce ==> (x ==> rcl_val option) ==> bit list" where "∀x0 x1 x2. (∃v3. x0 = SNum (int (length v3)) ∧ x2 [ x1 ] ~ SBitvec v3 ) = (x0 = by moura (* 0.0 ms *) then have "∀f c r. ¬ f [ [| c |]ce ] ~ r ∨ r = SNum (int (length (bbs r c f))) ∧ f by (meson eval_e_elims(8)) (* 46 ms *) then show ?thesis by (metis (no_types) CE_len.hyps CE_len.prems(1) CE_len.prems(2) rcl_val.eq_iff(1)) (* 3 qed qed lemma wfV_eval_bitvec: fixes v::v assumes "P ; B ; Γ ⊨wf v : B_bitvec" and "P ; Γ ⊨ i" shows "∃bv. eval_v i v (SBitvec bv)" proof - obtain s where "i [ v ] ~ s ∧ wfRCV P s B_bitvec" using eval_v_exist assms by metis moreover then obtain bv where "s = SBitvec bv" using wfRCV_elims(1)[of P s] by metis ultimately show ?thesis by metis qed lemma wfV_eval_pair: fixes v::v assumes "P ; B ; Γ ⊨wf v : B_pair b1 b2" and "P ; Γ ⊨ i" shows "∃s1 s2. eval_v i v (SPair s1 s2)" proof - obtain s where "i [ v ] ~ s ∧ wfRCV P s (B_pair b1 b2)" using eval_v_exist assms by met moreover then obtain s1 and s2 where "s = SPair s1 s2" using wfRCV_elims(2)[of P s] by metis ultimately show ?thesis by metis qed lemma wfV_eval_int: fixes v::v assumes "P ; B ; Γ ⊨wf v : B_int" and "P ; Γ ⊨ i" shows "∃n. eval_v i v (SNum n)" proof - obtain s where "i [ v ] ~ s ∧ wfRCV P s (B_int)" using eval_v_exist assms by metis moreover then obtain n where "s = SNum n" using wfRCV_elims(3)[of P s] by metis ultimately show ?thesis by metis qed text ‹Well sorted value with a well sorted valuation evaluates› lemma wfI_wfV_eval_v: fixes v::v and b::b assumes "Θ ; B ; Γ ⊨wf v : b" and "wfI Θ Γ i" shows "∃s. i [ v ] ~ s ∧ Θ ⊨ s : b" using eval_v_exist assms by auto lemma wfI_wfCE_eval_e: fixes e::ce and b::b assumes "wfCE P B G e b" and "P ; G ⊨ i" shows "∃s. i [ e ] ~ s ∧ P ⊨ s : b" using assms proof(nominal_induct e arbitrary: b rule: ce.strong_induct) case (CE_val v) obtain s where "i [ v ] ~ s ∧ P ⊨ s : b" using wfI_wfV_eval_v[of P B G v b i] assms wfCE_elim 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 ∧ wf 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 ∧ wf 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 using wfI_wfV_eval_v CE_op by metis hence "eval_e i (CE_op Eq v1 v2) (SBool (s1 = s2))" using eval_e_leqI * by (simp add: eval_e_eqI) moreover have "wfRCV P (SBool (s1 = s2)) B_bool" using wfRCV.intros by auto ultimately show ?thesis using 3 using CE_op.prems wfCE_elims by metis qed next case (CE_concat v1 v2) then obtain s1 and s2 where *:"b = B_bitvec ∧ eval_e i v1 s1 ∧ eval_e i v2 s2 ∧ wfRCV P s1 B_bitvec ∧ wfRCV P s2 B_bitvec" using CE_concat by (meson wfCE_elims(6)) thus ?case using eval_e_concatI wfRCV.intros(1) wfRCV_elims proof - obtain bbs :: "type_def list ==> rcl_val ==> bit list" where "∀ts s. ¬ ts ⊨ s : B_bitvec ∨ s = SBitvec (bbs ts s)" using wfRCV_elims(1) by moura (* 156 ms *) then show ?thesis by (metis (no_types) "local.*" wfRCV_BBitvecI eval_e_concatI) (* 78 ms *) qed next case (CE_fst v1) thus ?case using eval_e_fstI wfRCV.intros wfCE_elims wfI_wfV_eval_v by (metis wfRCV_elims(2) rcl_val.eq_iff(4)) next case (CE_snd v1) thus ?case using eval_e_sndI wfRCV.intros wfCE_elims wfI_wfV_eval_v by (metis wfRCV_elims(2) rcl_val.eq_iff(4)) next case (CE_len x) thus ?case using eval_e_lenI wfRCV.intros wfCE_elims wfI_wfV_eval_v wfV_eval_bitvec by (metis wfRCV_elims(1)) qed lemma eval_e_exist: fixes Γ::Γ and e::ce assumes "P ; Γ ⊨ i" and "P ; B ; Γ ⊨wf e : b" shows "∃s. i [ e ] ~ s" using assms proof(nominal_induct e arbitrary: b rule:ce.strong_induct) case (CE_val v) then show ?case using eval_v_exist wfCE_elims eval_e.intros by metis next case (CE_op op v1 v2) show ?case proof(rule opp.exhaust) assume ‹op = Plus› hence "P ; B ; Γ ⊨wf v1 : B_int ∧ P ; B ; Γ ⊨wf v2 : B_int ∧ b = B_int" using wfCE_ then obtain n1 and n2 where "eval_e i v1 (SNum n1) ∧ eval_e i v2 (SNum n2)" using CE_op e 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› b next assume ‹op = LEq› hence "P ; B ; Γ ⊨wf v1 : B_int ∧ P ; B ; Γ ⊨wf v2 : B_int ∧ b = B_bool" using wfCE then obtain n1 and n2 where "eval_e i v1 (SNum n1) ∧ eval_e i v2 (SNum n2)" using CE_op e 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 next assume ‹op = Eq› then obtain b1 where "P ; B ; Γ ⊨wf v1 : b1 ∧ P ; B ; Γ ⊨wf v2 : b1 ∧ b = B_bool" usi then obtain s1 and s2 where "eval_e i v1 s1 ∧ eval_e i v2 s2" using CE_op eval_v_exist wfV 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 ‹ qed next case (CE_concat v1 v2) then obtain bv1 and bv2 where "eval_e i v1 (SBitvec bv1) ∧ eval_e i v2 (SBitvec bv2)" using wfV_eval_bitvec wfCE_elims(6) by (meson eval_e_elims(7) wfI_wfCE_eval_e) then show ?case using eval_e.intros by metis next case (CE_fst ce) then obtain b2 where b:"P ; B ; Γ ⊨wf ce : B_pair b b2" using wfCE_elims by metis then obtain s where s:"i [ ce ] ~ s" using CE_fst by auto then obtain s1 and s2 where "s = (SPair s1 s2)" using eval_e_elims(4) CE_fst wfI_wfCE_eval by (metis eval_e_uniqueness) then show ?case using s eval_e.intros by metis next case (CE_snd ce) then obtain b1 where b:"P ; B ; Γ ⊨wf ce : B_pair b1 b" using wfCE_elims by metis then obtain s where s:"i [ ce ] ~ s" using CE_snd by auto then obtain s1 and s2 where "s = (SPair s1 s2)" using eval_e_elims(5) CE_snd wfI_wfCE_eval_e[of P B Γ ce "B_pair b1 b" i,OF b] wfRCV_elims(2 eval_e_uniqueness by (metis wfRCV_elims(2)) then show ?case using s eval_e.intros by metis next case (CE_len v1) then obtain bv1 where "eval_e i v1 (SBitvec bv1)" using wfV_eval_bitvec CE_len wfCE_elims eval_e_uniqueness by (metis eval_e_elims(7) wfCE_concatI wfI_wfCE_eval_e) then show ?case using eval_e.intros by metis qed lemma eval_c_exist: fixes Γ::Γ and c::c assumes "P ; Γ ⊨ i" and "P ; B ; Γ ⊨wf c" shows "∃s. i [ c ] ~ s" using assms proof(nominal_induct c rule: c.strong_induct) case C_true then show ?case using eval_c.intros wfC_elims by metis next case C_false then show ?case using eval_c.intros wfC_elims by metis next case (C_conj c1 c2) then show ?case using eval_c.intros wfC_elims by metis next case (C_disj x1 x2) then show ?case using eval_c.intros wfC_elims by metis next case (C_not x) then show ?case using eval_c.intros wfC_elims by metis next case (C_imp x1 x2) then show ?case using eval_c.intros eval_e_exist wfC_elims by metis next case (C_eq x1 x2) then show ?case using eval_c.intros eval_e_exist wfC_elims by metis qed lemma eval_c_uniqueness: fixes c::c assumes "i [ c ] ~ s" and "i [ c ] ~ s'" shows "s=s'" using assms proof(nominal_induct c arbitrary: s s' rule:c.strong_induct) case C_true then show ?case using eval_c_elims by metis next case C_false then show ?case using eval_c_elims by metis next case (C_conj x1 x2) then show ?case using eval_c_elims(3) by (metis (full_types)) next case (C_disj x1 x2) then show ?case using eval_c_elims(4) by (metis (full_types)) next case (C_not x) then show ?case using eval_c_elims(6) by (metis (full_types)) next case (C_imp x1 x2) then show ?case using eval_c_elims(5) by (metis (full_types)) next case (C_eq x1 x2) then show ?case using eval_e_uniqueness eval_c_elims(7) by metis qed lemma wfI_wfC_eval_c: fixes c::c assumes "wfC P B G c" and "P ; G ⊨ i" shows "∃s. i [ c ] ~ s" using assms proof(nominal_induct c rule: c.strong_induct) qed(metis wfC_elims wfI_wfCE_eval_e eval_c.intros)+ section ‹Satisfiability› lemma satis_reflI: fixes c::c assumes "i ⊨ ((x, b, c) #\<Gamma> G)" shows "i ⊨ c" using assms by auto lemma is_satis_mp: fixes c1::c and c2::c assumes "i ⊨ (c1 IMP c2)" and "i ⊨ c1" shows "i ⊨ c2" using assms proof - have "eval_c i (c1 IMP c2) True" using is_satis.simps using assms by blast then obtain b1 and b2 where "True = (b1 ⟶ b2) ∧ eval_c i c1 b1 ∧ eval_c i c2 b2" using eval_c_elims(5) by metis moreover have "eval_c i c1 True" using is_satis.simps using assms by blast moreover have "b1 = True" using calculation eval_c_uniqueness by blast ultimately have "eval_c i c2 True" by auto thus ?thesis using is_satis.intros by auto qed lemma is_satis_imp: fixes c1::c and c2::c assumes "i ⊨ c1 ⟶ i ⊨ c2" and "i [ c1 ] ~ b1" and "i [ c2 ] ~ b2" shows "i ⊨ (c1 IMP c2)" proof(cases b1) case True hence "i ⊨ c2" using assms is_satis.simps by simp hence "b2 = True" using is_satis.simps assms using eval_c_uniqueness by blast then show ?thesis using eval_c_impI is_satis.simps assms by force next case False then show ?thesis using assms eval_c_impI is_satis.simps by metis qed lemma is_satis_iff: "i ⊨ G = (∀x b c. (x,b,c) ∈ toSet G ⟶ i ⊨ c)" by(induct G,auto) lemma is_satis_g_append: "i ⊨ (G1@G2) = (i ⊨ G1 ∧ i ⊨ G2)" using is_satis_g.simps is_satis_iff by auto section ‹Substitution for Evaluation› lemma eval_v_i_upd: fixes v::v assumes "atom x ♯ v" and "i [ v ] ~ s'" shows "eval_v ((i ( x ↦s))) v s' " using assms proof(nominal_induct v arbitrary: s' rule:v.strong_induct) case (V_lit x) then show ?case by (metis eval_v_elims(1) eval_v_litI) next case (V_var y) then obtain s where *: "Some s = i y ∧ s=s'" using eval_v_elims by metis moreover have "x ≠ y" using ‹atom x ♯ V_var y› v.supp by simp ultimately have "(i ( x ↦s)) y = Some s" by (simp add: ‹Some s = i y ∧ s = s'›) then show ?case using eval_v_varI * ‹x ≠ y› by (simp add: eval_v.eval_v_varI) next case (V_pair v1 v2) hence "atom x ♯ v1 ∧ atom x ♯ v2" using v.supp by simp moreover obtain s1 and s2 where *: "eval_v i v1 s1 ∧ eval_v i v2 s2 ∧ s' = SPair s1 s2" ultimately have "eval_v ((i ( x ↦s))) v1 s1 ∧ eval_v ((i ( x ↦s))) v2 s2" using V_pa 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 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_e ultimately have "eval_v ((i ( x ↦s))) v1 s1" using V_consp by blast thus ?case using eval_v_conspI * by meson qed lemma eval_e_i_upd: fixes e::ce assumes "i [ e ] ~ s'" and "atom x ♯ e" shows " (i ( x ↦s)) [ e ] ~ s'" using assms apply(induct rule: eval_e.induct) using eval_v_i_upd eval_e_elims by (meson ce.fresh eval_e.intros)+ lemma eval_c_i_upd: fixes c::c assumes "i [ c ] ~ s'" and "atom x ♯ c" shows "((i ( x ↦s))) [ c ] ~ s' " using assms proof(induct rule:eval_c.induct) case (eval_c_eqI i e1 sv1 e2 sv2) then show ?case using RCLogic.eval_c_eqI eval_e_i_upd c.fresh by metis qed(simp add: eval_c.intros)+ lemma subst_v_eval_v[simp]: fixes v::v and v'::v assumes "i [ v ] ~ s" and "i [ (v'[x::=v]vv) ] ~ s'" shows "(i ( x ↦ s )) [ v' ] ~ s'" using assms proof(nominal_induct v' arbitrary: s' rule:v.strong_induct) case (V_lit x) then show ?case using subst_vv.simps by (metis eval_v_elims(1) eval_v_litI) next case (V_var x') then show ?case proof(cases "x=x'") case True hence "(V_var x')[x::=v]vv = v" using subst_vv.simps by auto then show ?thesis using V_var eval_v_elims eval_v_varI eval_v_uniqueness True by (simp add: eval_v.eval_v_varI) next case False hence "atom x ♯ (V_var x')" by simp then show ?thesis using eval_v_i_upd False V_var by fastforce qed next case (V_pair v1 v2) then obtain s1 and s2 where *:"eval_v i (v1[x::=v]vv) s1 ∧ eval_v i (v2[x::=v]vv) s2 ∧ hence "(i ( x ↦ s )) [ v1 ] ~ s1 ∧ (i ( x ↦ s )) [ v2 ] ~ s2" using V_pair by metis thus ?case using eval_v_pairI subst_vv.simps * V_pair by metis next case (V_cons tyid dc v1) then obtain s1 where "eval_v i (v1[x::=v]vv) s1" using eval_v_elims subst_vv.simps by met thus ?case using eval_v_consI V_cons by (metis eval_v_elims subst_vv.simps) next case (V_consp tyid dc b1 v1) then obtain s1 where *:"eval_v i (v1[x::=v]vv) s1 ∧ s' = SConsp tyid dc b1 s1" using e hence "i ( x ↦ s ) [ v1 ] ~ s1" using V_consp by metis thus ?case using * eval_v_conspI by metis qed lemma subst_e_eval_v[simp]: fixes y::x and e::ce and v::v and e'::ce assumes "i [ e' ] ~ s'" and "e'=(e[y::=v]cev)" and "i [ v ] ~ s" shows "(i ( y ↦ s )) [ e ] ~ s'" using assms proof(induct arbitrary: e rule: eval_e.induct) case (eval_e_valI i v1 sv) then obtain v1' where *:"e = CE_val v1' ∧ v1 = v1'[y::=v]vv" using assms by(nominal_induct e rule:ce.strong_induct,simp+) hence "eval_v i (v1'[y::=v]vv) sv" using eval_e_valI by simp hence "eval_v (i ( y ↦ s )) v1' sv" using subst_v_eval_v eval_e_valI by simp then show ?case using RCLogic.eval_e_valI * by meson next case (eval_e_plusI i v1 n1 v2 n2) then obtain v1' and v2' where *:"e = CE_op Plus v1' v2' ∧ v1 = v1'[y::=v]cev ∧ v2 = v2 using assms by(nominal_induct e rule:ce.strong_induct,simp+) hence "eval_e i (v1'[y::=v]cev) (SNum n1) ∧ eval_e i (v2'[y::=v]cev) (SNum n2)" us hence "eval_e (i ( y ↦ s )) v1' (SNum n1) ∧ eval_e (i ( y ↦ s )) v2' (SNum n2)" u using "local.*" by blast then show ?case using RCLogic.eval_e_plusI * by meson next case (eval_e_leqI i v1 n1 v2 n2) then obtain v1' and v2' where *:"e = CE_op LEq v1' v2' ∧ v1 = v1'[y::=v]cev ∧ v2 = v2' using assms by(nominal_induct e rule:ce.strong_induct,simp+) hence "eval_e i (v1'[y::=v]cev) (SNum n1) ∧ eval_e i (v2'[y::=v]cev) (SNum n2)" us hence "eval_e (i ( y ↦ s )) v1' (SNum n1) ∧ eval_e (i ( y ↦ s )) v2' (SNum n2)" u using * by blast then show ?case using RCLogic.eval_e_leqI * by meson next case (eval_e_eqI i v1 n1 v2 n2) then obtain v1' and v2' where *:"e = CE_op Eq v1' v2' ∧ v1 = v1'[y::=v]cev ∧ v2 = v2'[ using assms by(nominal_induct e rule:ce.strong_induct,simp+) hence "eval_e i (v1'[y::=v]cev) n1 ∧ eval_e i (v2'[y::=v]cev) n2" using eval_e_eqI b hence "eval_e (i ( y ↦ s )) v1' n1 ∧ eval_e (i ( y ↦ s )) v2' n2" using subst_v_ev using * by blast then show ?case using RCLogic.eval_e_eqI * by meson next case (eval_e_fstI i v1 s1 s2) then obtain v1' and v2' where *:"e = CE_fst v1' ∧ v1 = v1'[y::=v]cev" using assms by(nominal_induct e rule:ce.strong_induct,simp+) hence "eval_e i (v1'[y::=v]cev) (SPair s1 s2)" using eval_e_fstI by simp hence "eval_e (i ( y ↦ s )) v1' (SPair s1 s2)" using eval_e_fstI * by metis then show ?case using RCLogic.eval_e_fstI * by meson next case (eval_e_sndI i v1 s1 s2) then obtain v1' and v2' where *:"e = CE_snd v1' ∧ v1 = v1'[y::=v]cev" using assms by(nominal_induct e rule:ce.strong_induct,simp+) hence "eval_e i (v1'[y::=v]cev) (SPair s1 s2)" using eval_e_sndI by simp hence "eval_e (i ( y ↦ s )) v1' (SPair s1 s2)" using subst_v_eval_v eval_e_sndI * by bl then show ?case using RCLogic.eval_e_sndI * by meson next case (eval_e_concatI i v1 bv1 v2 bv2) then obtain v1' and v2' where *:"e = CE_concat v1' v2' ∧ v1 = v1'[y::=v]cev ∧ v2 = v2' using assms by(nominal_induct e rule:ce.strong_induct,simp+) hence "eval_e i (v1'[y::=v]cev) (SBitvec bv1) ∧ eval_e i (v2'[y::=v]cev) (SBitvec moreover hence "eval_e (i ( y ↦ s )) v1' (SBitvec bv1) ∧ eval_e (i ( y ↦ s )) v2' 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_c next case (eval_e_lenI i v1 bv) then obtain v1' where *:"e = CE_len v1' ∧ v1 = v1'[y::=v]cev" using assms by(nominal_induct e rule:ce.strong_induct,simp+) hence "eval_e i (v1'[y::=v]cev) (SBitvec bv)" using eval_e_lenI by simp hence "eval_e (i ( y ↦ s )) v1' (SBitvec bv)" using subst_v_eval_v eval_e_lenI * by bla then show ?case using RCLogic.eval_e_lenI * by meson qed lemma subst_c_eval_v[simp]: fixes v::v and c :: c assumes "i [ v ] ~ s" and "i [ c[x::=v]cv ] ~ s1" and "(i ( x ↦ s)) [ c ] ~ s2" shows "s1 = s2" using assms proof(nominal_induct c arbitrary: s1 s2 rule: c.strong_induct) case C_true hence "s1 = True ∧ s2 = True" using eval_c_elims subst_cv.simps by auto then show ?case by auto next case C_false hence "s1 = False ∧ s2 = False" using eval_c_elims subst_cv.simps by metis then show ?case by auto next case (C_conj c1 c2) hence *:"eval_c i (c1[x::=v]cv AND c2[x::=v]cv) s1" using subst_cv.simps by auto then obtain s11 and s12 where "(s1 = (s11 ∧ s12)) ∧ eval_c i c1[x::=v]cv s11 ∧ eval_c eval_c_elims(3) by metis moreover obtain s21 and s22 where "eval_c (i ( x ↦ s)) c1 s21 ∧ eval_c (i ( x ↦ s)) eval_c_elims(3) C_conj by metis ultimately show ?case using C_conj by (meson eval_c_elims) next case (C_disj c1 c2) hence *:"eval_c i (c1[x::=v]cv OR c2[x::=v]cv) s1" using subst_cv.simps by auto then obtain s11 and s12 where "(s1 = (s11 ∨ s12)) ∧ eval_c i c1[x::=v]cv s11 ∧ eval_c eval_c_elims(4) by metis moreover obtain s21 and s22 where "eval_c (i ( x ↦ s)) c1 s21 ∧ eval_c (i ( x ↦ s)) eval_c_elims(4) C_disj by metis ultimately show ?case using C_disj by (meson eval_c_elims) next case (C_not c1) then obtain s11 where "(s1 = (¬ s11)) ∧ eval_c i c1[x::=v]cv s11" using eval_c_elims(6) by (metis subst_cv.simps(7)) moreover obtain s21 where "eval_c (i ( x ↦ s)) c1 s21 ∧ (s2 = (¬s21))" using eval_c_elims(6) C_not by metis ultimately show ?case using C_not by (meson eval_c_elims) next case (C_imp c1 c2) hence *:"eval_c i (c1[x::=v]cv IMP c2[x::=v]cv) s1" using subst_cv.simps by auto then obtain s11 and s12 where "(s1 = (s11 ⟶ s12)) ∧ eval_c i c1[x::=v]cv s11 ∧ eval_c eval_c_elims(5) by metis moreover obtain s21 and s22 where "eval_c (i ( x ↦ s)) c1 s21 ∧ eval_c (i ( x ↦ s)) eval_c_elims(5) C_imp by metis ultimately show ?case using C_imp by (meson eval_c_elims) next case (C_eq e1 e2) hence *:"eval_c i (e1[x::=v]cev == e2[x::=v]cev) s1" using subst_cv.simps by auto then obtain s11 and s12 where "(s1 = (s11 = s12)) ∧ eval_e i (e1[x::=v]cev) s11 ∧ eval eval_c_elims(7) by metis moreover obtain s21 and s22 where "eval_e (i ( x ↦ s)) e1 s21 ∧ eval_e (i ( x ↦ s)) eval_c_elims(7) C_eq by metis ultimately show ?case using C_eq subst_e_eval_v by (metis eval_e_uniqueness) qed lemma wfI_upd: assumes "wfI Θ Γ i" and "wfRCV Θ s b" and "wfG Θ B ((x, b, c) #\<Gamma> Γ)" shows "wfI Θ ((x, b, c) #\<Gamma> Γ) (i(x ↦ s))" proof(subst wfI_def,rule) fix xa assume as:"xa ∈ toSet ((x, b, c) #\<Gamma> Γ)" then obtain x1::x and b1::b and c1::c where xa: "xa = (x1,b1,c1)" using toSet.simps using prod_cases3 by blast have "∃sa. Some sa = (i(x ↦ s)) x1 ∧ wfRCV Θ sa b1" proof(cases "x=x1") case True hence "b=b1" using as xa wfG_unique assms by metis hence "Some s = (i(x ↦ s)) x1 ∧ wfRCV Θ s b1" using assms True by simp then show ?thesis by auto next case False hence "(x1,b1,c1) ∈ toSet Γ" using xa as by auto then obtain sa where "Some sa = i x1 ∧ wfRCV Θ sa b1" using assms wfI_def as xa by auto hence "Some sa = (i(x ↦ s)) x1 ∧ wfRCV Θ sa b1" using False by auto then show ?thesis by auto qed thus "case xa of (xa, ba, ca) ==> ∃sa. Some sa = (i(x ↦ s)) xa ∧ wfRCV Θ sa ba" usi qed lemma wfI_upd_full: fixes v::v assumes "wfI Θ G i" and "G = ((Γ'[x::=v]\<Gamma>v)@Γ)" and "wfRCV Θ s b" and "wfG Θ B (Γ'@(( shows "wfI Θ (Γ'@((x,b,c)#\<Gamma>Γ)) (i(x ↦ s))" proof(subst wfI_def,rule) fix xa assume as:"xa ∈ toSet (Γ'@((x,b,c)#\<Gamma>Γ))" then obtain x1::x and b1::b and c1::c where xa: "xa = (x1,b1,c1)" using toSet.simps using prod_cases3 by blast have "∃sa. Some sa = (i(x ↦ s)) x1 ∧ wfRCV Θ sa b1" proof(cases "x=x1") case True hence "b=b1" using as xa wfG_unique_full assms by metis hence "Some s = (i(x ↦ s)) x1 ∧ wfRCV Θ s b1" using assms True by simp then show ?thesis by auto next case False hence "(x1,b1,c1) ∈ toSet (Γ'@Γ)" using as xa by auto then obtain c1' where "(x1,b1,c1') ∈ toSet (Γ'[x::=v]\<Gamma>v@Γ)" using xa as wfG_member_s 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" usi qed lemma subst_c_satis[simp]: fixes v::v assumes "i [ v ] ~ s" and "wfC Θ B ((x,b,c')#\<Gamma>Γ) c" and "wfI Θ Γ i" and "Θ ; B ; Γ ⊨w shows "i ⊨ (c[x::=v]cv) ⟷ (i ( x ↦ s)) ⊨ c" proof - have "wfI Θ ((x, b, c') #\<Gamma> Γ) (i(x ↦ s))" using wfI_upd assms wfC_wf eval_v_base by then obtain s1 where s1:"eval_c (i(x ↦ s)) c s1" using eval_c_exist[of Θ "((x,b,c')#\<Gamm have "Θ ; B ; Γ ⊨wf c[x::=v]cv" using wf_subst1(2)[OF assms(2) _ assms(4) , of GNil x ] subs then obtain s2 where s2:"eval_c i c[x::=v]cv s2" using eval_c_exist[of Θ "Γ" "i" B "c[x::=v]c 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 lemma subst_c_satis_full: fixes v::v and Γ'::Γ assumes "i [ v ] ~ s" and "wfC Θ B (Γ'@((x,b,c')#\<Gamma>Γ)) c" and "wfI Θ ((Γ'[x::=v]\<G shows "i ⊨ (c[x::=v]cv) ⟷ (i ( x ↦ s)) ⊨ c" proof - have "wfI Θ (Γ'@((x, b, c')) #\<Gamma> Γ) (i(x ↦ s))" using wfI_upd_full assms wfC_wf eval then obtain s1 where s1:"eval_c (i(x ↦ s)) c s1" using eval_c_exist[of Θ "(Γ'@(x,b,c')#\<Ga have "Θ ; B ; ((Γ'[x::=v]\<Gamma>v)@Γ) ⊨wf c[x::=v]cv" using wbc_subst assms by auto then obtain s2 where s2:"eval_c i c[x::=v]cv s2" using eval_c_exist[of Θ "((Γ'[x::=v]\<Gamm show ?thesis using s1 s2 subst_c_eval_v[OF assms(1) s2 s1] is_satis.cases using eval_c_uniqueness is_satis.simps by auto qed section ‹Validity› lemma validI[intro]: fixes c::c assumes "wfC P B G c" and "∀i. P ; G ⊨ i ∧ i ⊨ G ⟶ i ⊨ c" shows "P ; B ; G ⊨ c" using assms valid.simps by presburger lemma valid_g_wf: fixes c::c and G::Γ assumes "P ; B ; G ⊨ c" shows "P ; B ⊨wf G" using assms wfC_wf valid.simps by blast lemma valid_reflI [intro]: fixes b::b assumes "P ; B ; ((x,b,c1)#\<Gamma>G) ⊨wf c1" and "c1 = c2" shows "P ; B ; ((x,b,c1)#\<Gamma>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.sup 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 restr 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_elim 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.sup 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 rest 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_eli 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 ⊨wf Γ" 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) #\<Gamma> G ⊨wf c" using wfG_wfC GCons by simp moreover hence "supp c ⊆ atom ` d ∪ supp B" using wfC_supp GCons atom_dom_eq by blast ultimately show ?thesis using is_satis_i_restrict[of i' i d c] GCons by simp qed ultimately show ?case by auto qed lemma is_satis_g_restrict: fixes Γ'::Γ and Γ::Γ assumes "toSet Γ ⊆ toSet Γ'" and "i' ⊨ Γ'" and "i = i' |` (fst ` toSet Γ)" and "Θ ; B ⊨wf Γ shows "i ⊨ Γ" using assms is_satis_g_restrict1[OF assms(1) assms(2)] is_satis_g_restrict2[OF _ assms( 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 #\<Gamma> (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')#\<Gamma>Γ))" and "Θ ; B ; Γ'@(x,b0,c0)#\<Gamma>Γ ⊨ c0'" shows "wfG Θ B (Γ'@((x,b0,c0)#\<Gamma>Γ))" proof - have "wfG Θ B (Γ'@(x,b0,c0)#\<Gamma>Γ)" using valid.simps wfC_wf assms by auto thus ?thesis using wfG_replace_inside_full assms by auto qed lemma valid_trans: assumes " Θ ; B ; Γ ⊨ c0[z::=v]v" and " Θ ; B ; (z,b,c0)#\<Gamma>Γ ⊨ c1" and "atom z ♯ Γ" an shows " Θ ; B ; Γ ⊨ c1[z::=v]v" proof - have *:"wfC Θ B ((z,b,c0)#\<Gamma>Γ) c1" using valid.simps assms by auto hence "wfC Θ B Γ (c1[z::=v]v)" using wf_subst1(2)[OF * , of GNil ] assms subst_gv.simps subst 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_e moreover have "is_satis_g (i(z ↦ sv)) Γ" using is_satis_g_i_upd assms by (simp add: as) ultimately have "is_satis_g (i(z ↦ sv)) ((z,b,c0)#\<Gamma>Γ)" using is_satis_g.simps by simp moreover have "wfI Θ ((z,b,c0)#\<Gamma>Γ) (i(z ↦ sv))" using as wfI_upd sv assms valid.simp 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_eli qed ultimately show ?thesis using valid.simps by auto qed lemma valid_trans_full: assumes "Θ ; B ; ((x, b, c1[z1::=V_var x]v) #\<Gamma> Γ) ⊨ c2[z2::=V_var x]v" and "Θ ; B ; ((x, b, c2[z2::=V_var x]v) #\<Gamma> Γ) ⊨ c3[z3::=V_var x]v" shows "Θ ; B ; ((x, b, c1[z1::=V_var x]v) #\<Gamma> Γ) ⊨ c3[z3::=V_var x]v" unfolding valid.simps proof show "Θ ; B ; (x, b, c1[z1::=V_var x]v) #\<Gamma> Γ ⊨wf c3[z3::=V_var x]v" using wf_ show "∀i. ( wfI Θ ((x, b, c1[z1::=V_var x]v) #\<Gamma> Γ) i ∧ (is_satis_g i ((x, proof(rule,rule) fix i assume as: "Θ ; (x, b, c1[z1::=V_var x]v) #\<Gamma> Γ ⊨ i ∧ i ⊨ (x, b, c1[z1::=V_var 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 them in an SUt smt val node. Another way of looking at it is that s' where the is needed to prove subst\_b\_valid - the base-type variable substitution lemma first @{text "rcl_val"} is the expanded form (has type with base-variables repl ; the second is its corresponding form only have one variable so we need to ensure that in all of the @{text "bs_boxe base type. example is an SMT value is (SPair (SInt 1) (SBool true)) and it has sort (BPair boxed version is SPair (SUt (SInt 1)) (SBool true) and is has sort (BPair (BVar that we can obtain from a valuation i, that gives values like the first smt val second. inductive boxed_b :: "Θ ==> rcl_val ==> b ==> bv ==> b ==> rcl_val ==> bool" ( ‹ _ ⊨ boxed_b_BVar1I: "[ bv = bv' ; wfRCV P s b ] ==> boxed_b P s (B_var bv') bv b (SU | boxed_b_BVar2I: "[ bv ≠ bv'; wfRCV P s (B_var bv') ] ==> boxed_b P s (B_var bv | 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' ] ==> box | 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]bb) bv b' s1' ] ==> boxed_b P (SConsp tyid dc b1[bv::=b']bb s1) (B_app tyid b1) bv b' (SConsp tyid d | 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 "supp s = {}"*) and "\<turnstile>\<^sub>w\<^sub>f P" shows "wfRCV P s b[bv::=b']bb ∧ wfRCV P s' b" using assms proof(induct rule: boxed_b.inducts) case (boxed_b_BVar1I bv bv' P s b ) then show ?case using wfRCV.intros by auto next case (boxed_b_BVar2I bv bv' P s ) then show ?case using wfRCV.intros by auto next case (boxed_b_BPairI P s1 b1 bv b s1' s2 b2 s2') then show ?case using wfRCV.intros rcl_val.supp by simp next case (boxed_b_BConsI tyid dclist P dc x b c s1 bv b' s1') hence "supp b = {}" using wfTh_supp_b by metis hence "b [ bv ::= b' ]bb = b" using fresh_def subst_b_b_def forget_subst[of "bv" b b'] by hence " P ⊨ SCons tyid dc s1 : (B_id tyid)" using wfRCV.intros rcl_val.supp subst_bb 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 ty atom bva2 ♯ (bv,(P, SConsp tyid dc b1[bv::=b']bb s1, B_app tyid b1[bv::=b']bb))" 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']bb s1 : (B_app tyid b1[bv::=b']bb)" proof show 1: ‹AF_typedef_poly tyid bva2 dclist2 ∈ set P› using boxed_b_BConspI * by auto show 2: ‹(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]bb = b2[bva2::=b1]bb" using wfTh_typedef_poly_b_eq_iff * 2 bo ultimately show ‹ P ⊨ s1 : b2[bva2::=b1[bv::=b']bb]bb› using boxed_b_BConspI subst_ show "atom bva2 ♯ (P, SConsp tyid dc b1[bv::=b']bb s1, B_app tyid b1[bv::=b']bb)" 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]bb› 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 rc qed ultimately show ?case using subst_bb.simps by simp qed(auto)+ lemma subst_b_var: assumes "B_var bv2 = b[bv::=b']bb" shows "(b = B_var bv ∧ b' = B_var bv2) ∨ (b=B_var bv2 ∧ bv ≠ 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 next lemma for a clearer explanation of what this is. i produces values of sort inductive boxed_i :: "Θ ==> Γ ==> b ==> bv ==> valuation ==> valuation ==> bool" ( ‹ _ 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 equivariance boxed_i nominal_inductive boxed_i . inductive_cases boxed_i_elims: "Θ ;GNil ; b , bv ⊨ i ≈ i'" "Θ ; ((x,b,c)#\<Gamma>Γ) ; 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 using assms proof(nominal_induct "SConsp typid dc bdc s" b avoiding: tm rule:wfRCV.stro 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']bb" 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']bb = B_bitvec" using wfRCV_elims(9)[OF SBitvec(1)] by metis show ?case proof (cases "b = B_var bv") case True moreover have "T ⊨ SBitvec x : B_bitvec" using wfRCV.intros by simp moreover hence "b' = B_bitvec" using True SBitvec subst_bb.simps * by simp ultimately show ?thesis using boxed_b.intros wfRCV.intros by metis next case False hence "b = B_bitvec" using subst_bb_inject * by metis then show ?thesis using * SBitvec boxed_b.intros by metis qed next case (SNum x) have *:"b[bv::=b']bb = 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']bb = B_bool" using wfRCV_elims(11)[OF SBool(1)] by metis show ?case proof (cases "b = B_var bv") case True moreover have "T ⊨ SBool x : B_bool" using wfRCV.intros by simp moreover hence "b' = B_bool" using True SBool subst_bb.simps * by simp ultimately show ?thesis using boxed_b.intros wfRCV.intros by metis 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']bb = B_pair b1 b2 ∧ wfRCV T s1 b1 ∧ wfRCV T s 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']bb ∧ b2=b2'[bv::=b' then show ?thesis using * SPair boxed_b_BPairI by blast qed next case (SCons tyid dc s1) have *:"b[bv::=b']bb = 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 then have "atom bv ♯ b2" using ‹wfTh T› wfTh_lookup_supp_empty[of tyid dclist T dc "{ x : then have "b2 = b2[ bv ::= b']bb" 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 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']bb = B_app typid bdc ∧ AF_typedef_poly typid bva dclist ∈ set T ∧ (dc, { x1 : b1 | c1 }) ∈ set dclist using wfRCV_poly_elims[OF SConsp(2)] by metis then have *:"B_app typid bdc = b[bv::=b']bb" using wfRCV_elims(14)[OF SConsp(2)] by met 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']bb" using * subst (*hence beq:"b = B_app typid bdc" using subst_bb_inject * sory (* going to be like the above as bd 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]bb" using ** by auto moreover have "b1[bva::=bdc']bb[bv::=b']bb = b1[bva::=bdc]bb" using bdc subst_bb_comm ultimately obtain s' where s':"T ⊨ s ~ b1[bva::=bdc']bb [ bv ::= b' ] ∖ s'" using SConsp(1)[of "b1[bva::=bdc']bb"] bdc SConsp by metis have "T ⊨ SConsp typid dc bdc'[bv::=b']bb s ~ (B_app typid bdc') [ bv ::= b' ] ∖ proof - obtain bva3 and dclist3 where 3:"AF_typedef_poly typid bva3 dclist3 = AF_typedef_pol 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']bb = b1[bva::=bdc']bb" 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']bb [ bv ::= b' ] ∖ s' › using s' by auto qed qed then show ?thesis using bdc by auto qed next case SUnit have *:"b[bv::=b']bb = 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']bb= 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]\<Gamma>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]bb" using wfI_def subst_gb.s 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 forc have "boxed_i T ((x', b', c') #\<Gamma> Γ') 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 "⊨wf Θ" 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 ty ∧ AF_typedef tyid dclist2 ∈ set P ∧ (dc2, { x2 : b2 | c2 }) ∈ set dclist2" using 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 me 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']bb s22 ∧ s2' = SConsp tyid dc2 b1 s22' ∧ boxed_b P s22 b2[bva2::=b1]bb bv b' s22' ∧ AF_typedef_poly tyid bva2 dclist2 ∈ set P ∧ (dc2, { x2 : b2 | c2 }) ∈ set dclis show ?case proof(cases "dc = dc2") case True hence "AF_typedef_poly tyid bva2 dclist2 ∈ set P ∧ (dc, { x2 : b2 | c2 }) ∈ set hence "b[bva::=b1]bb = b2[bva2::=b1]bb" using wfTh_typedef_poly_b_eq_iff[OF boxed_b_ 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 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']vb ] ~ s" and "i' [ v ] ~ s'" and "w 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) (* look at defn of bs_boxed *) 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']vb) s1 ∧ eval_v i (v2[bv::=b']vb) s2 ∧ obtain s1' and s2' where s': "eval_v i' v1 s1' ∧ eval_v i' v2 s2' ∧ s' = SPair s1' s2' have "boxed_b Θ (SPair s1 s2) (B_pair b1 b2) bv b' (SPair s1' s2') " proof(rule bo show "boxed_b Θ s1 b1 bv b' s1'" using V_pair eval_v_elims wfV_elims b s s' b.eq_iff by meti show "boxed_b Θ s2 b2 bv b' s2'" using V_pair eval_v_elims wfV_elims b s s' b.eq_iff by meti 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 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']vb) ] ~ s2" using eval_v_ obtain s2' where s2': "s' = SCons tyid dc s2' ∧ i' [ v1 ] ~ s2'" using eval_v_elims V_ 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 (dc, { x2 : b2 | c2 }) ∈ set dclist ∧ Θ ; B ; Γ ⊨wf v1 : b2[bv2::=b1]bb" using wf_strong_elim(1)[OF V_consp (5)] by metis obtain s2 where s2: "s = SConsp tyid dc b1[bv::=b']bb s2 ∧ i [ (v1[bv::=b']vb) ] ~ 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 "⊨wf Θ" using V_consp wfX_wfY by metis then obtain bv3::bv and dclist3 x3 b3 c3 where **:" AF_typedef_poly tyid bv2 dclist = AF (dc, { x3 : b3 | c3 }) ∈ set dclist3 ∧ atom bv3 ♯ (b1, bv, b', s2, s2') ∧ b2[bv 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']bb s2) (B_app tyid b1) bv b' (SConsp ty 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]bb [ 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 "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']ceb ] ~ s" and "wfCE Θ B Γ e b" and "boxed_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 m 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']ceb ] ~ SNum n1 ∧ i [ v obtain n1' and n2' where n':"s' = SNum (n1' + n2') ∧ i' [ v1 ] ~ SNum n1' ∧ i' [ v2 ] have "boxed_b Θ (SNum n1) B_int bv b' (SNum n1')" using boxed_i_eval_v_boxed_b 1 2 n n' C moreover have "boxed_b Θ (SNum n2) B_int bv b' (SNum n2')" using boxed_i_eval_v_boxed 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']ceb ] ~ SNum n1 ∧ i [ obtain n1' and n2' where n':"s' = SBool (n1' ≤ n2') ∧ i' [ v1 ] ~ SNum n1' ∧ i' [ v2 have "boxed_b Θ (SNum n1) B_int bv b' (SNum n1')" using boxed_i_eval_v_boxed_b 1 2 n n' C moreover have "boxed_b Θ (SNum n2) B_int bv b' (SNum n2')" using boxed_i_eval_v_boxed 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› 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']ceb ] ~ n1 ∧ i [ v2[bv obtain n1' and n2' where n':"s' = SBool (n1' = n2') ∧ i' [ v1 ] ~ n1' ∧ i' [ v2 ] ~ n 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 met moreover have "⊨wf Θ" 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']ceb ] ~ SBitvec using eval_e_elims(7) subst_ceb.simps CE_concat.prems(2) eval_e_elims(6) subst_ceb.si obtain bv1' and bv2' where s' : "s' = SBitvec (bv1' @ bv2') ∧ i' [ v1 ] ~ SBitvec bv1' 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_elim next case (CE_fst ce) obtain s2 where 1:"i [ ce[bv::=b']ceb ] ~ SPair s s2" using CE_fst eval_e_elims subst_c 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 \<lbrakk> v[bv::=b']\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ SPair s1 s" using CE_snd obtain s1' where 2:"i' \<lbrakk> v \<rbrakk> ~ SPair s1' s'" using CE_snd eval_e_elims by metis obtain b1 where 3:"wfCE \<Theta> B \<Gamma> v (B_pair b1 b )" using wfCE_elims(5) CE_snd by metis have "boxed_b \<Theta> (SPair s1 s ) (B_pair b1 b ) bv b' (SPair s1' s')" using 1 2 3 CE_snd boxed_i_ev thus ?case using boxed_b_elims(5) by force next case (CE_len v) obtain s1 where s: "i \<lbrakk> v[bv::=b']\<^sub>c\<^sub>e\<^sub>b \<rbrakk> ~ SBitvec s1" using CE_le obtain s1' where s': "i' \<lbrakk> v \<rbrakk> ~ SBitvec s1'" using CE_len eval_e_elims by metis have "\<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f v : B_bitvec \<and> b = B_int" using wfCE_elims C 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 qed lemma eval_c_eq_bs_boxed: fixes c::c assumes "i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s" and "i' \<lbrakk> c \<rbrakk> ~ s'" and "wfC \< and "boxed_i \<Theta> \<Gamma> b bv i i'" shows "s = s'" using assms proof(nominal_induct c arbitrary: s s' rule:c.strong_induct) 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]\<^sub>c\<^sub>b) s1 \<and> eval_c i (c2[bv::=b]\<^su obtain s1' and s2' where 2:"eval_c i' c1 s1' \<and> eval_c i' c2 s2' \<and> s' = (s1'\<and>s2')" using C_ then show ?case using 1 2 wfC_elims C_conj by metis next case (C_disj c1 c2) obtain s1 and s2 where 1: "eval_c i (c1[bv::=b]\<^sub>c\<^sub>b) s1 \<and> eval_c i (c2[bv::=b]\<^su obtain s1' and s2' where 2:"eval_c i' c1 s1' \<and> eval_c i' c2 s2' \<and> s' = (s1'\<or>s2')" using C_d then show ?case using 1 2 wfC_elims C_disj by metis next case (C_not c) obtain s1::bool where 1: "(i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s1) \<and> (s = (\<not> s1))" obtain s1'::bool where 2: "(i' \<lbrakk> c \<rbrakk> ~ s1') \<and> (s' = (\<not> s1'))" using C_not eval_ then show ?case using 1 2 wfC_elims C_not by metis next case (C_imp c1 c2) obtain s1 and s2 where 1: "eval_c i (c1[bv::=b]\<^sub>c\<^sub>b) s1 \<and> eval_c i (c2[bv::=b]\<^su obtain s1' and s2' where 2:"eval_c i' c1 s1' \<and> eval_c i' c2 s2' \<and> s' = (s1' \<longrightarrow> s then show ?case using 1 2 wfC_elims C_imp by metis next case (C_eq e1 e2) obtain be where be: "wfCE \<Theta> B \<Gamma> e1 be \<and> wfCE \<Theta> B \<Gamma> e2 be" using C_eq wfC_eli obtain s1 and s2 where 1: "eval_e i (e1[bv::=b]\<^sub>c\<^sub>e\<^sub>b) s1 \<and> eval_e i (e2[bv::= obtain s1' and s2' where 2:"eval_e i' e1 s1' \<and> eval_e i' e2 s2' \<and> s' = (s1' = s2' )" using C_eq e have "\<turnstile>\<^sub>w\<^sub>f \<Theta>" using C_eq wfX_wfY by metis moreover have "\<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i " using C_eq by auto ultimately show ?case using boxed_b_eq[of \<Theta> s1 be bv b s1' s2 s2'] 1 2 boxed_i_eval_ce_box qed lemma is_satis_bs_boxed: fixes c::c assumes "boxed_i \<Theta> \<Gamma> b bv i i'" and "wfC \<Theta> B \<Gamma> c" and "wfI \<Theta> \<Gamma>[bv:: and "(i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b)" shows "(i' \<Turnstile> c)" proof - have "eval_c i (c[bv::=b]\<^sub>c\<^sub>b) True" using is_satis.simps assms by auto moreover obtain s where "i' \<lbrakk> c \<rbrakk> ~ s" using eval_c_exist assms by metis ultimately show ?thesis using eval_c_eq_bs_boxed assms is_satis.simps by metis qed lemma is_satis_bs_boxed_rev: fixes c::c assumes "boxed_i \<Theta> \<Gamma> b bv i i'" and "wfC \<Theta> B \<Gamma> c" and "wfI \<Theta> \<Gamma>[bv:: and "(i' \<Turnstile> c)" shows "(i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b)" proof - have "eval_c i' c True" using is_satis.simps assms by auto moreover obtain s where "i \<lbrakk> c[bv::=b]\<^sub>c\<^sub>b \<rbrakk> ~ s" using eval_c_exist ass ultimately show ?thesis using eval_c_eq_bs_boxed assms is_satis.simps by metis qed lemma bs_boxed_wfi_aux: fixes b::b and bv::bv and \<Theta>::\<Theta> and B::\<B> assumes "boxed_i \<Theta> \<Gamma> b bv i i'" and "wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i" shows "\<Theta> ; \<Gamma> \<turnstile> i'" using assms proof(induct rule: boxed_i.inducts) case (boxed_i_GNilI T i) then show ?case using wfI_def by auto next case (boxed_i_GConsI s i x1 T b1 bv b s' G i' c1) { fix x2 b2 c2 assume as : "(x2,b2,c2) \<in> toSet ((x1, b1, c1) #\<^sub>\<Gamma> G)" then consider (hd) "(x2,b2,c2) = (x1, b1, c1)" | (tail) "(x2,b2,c2) \<in> toSet G" using toSet.si hence "\<exists>s. Some s = (i'(x1 \<mapsto> s')) x2 \<and> wfRCV T s b2" proof(cases) case hd hence "b1=b2" by auto moreover have "(x2,b2[bv::=b]\<^sub>b\<^sub>b,c2[bv::=b]\<^sub>c\<^sub>b) \<in> toSet ((x1, b1, c moreover hence "wfRCV T s b2[bv::=b]\<^sub>b\<^sub>b" using wfI_def boxed_i_GConsI hd proof - obtain ss :: "b \<Rightarrow> x \<Rightarrow> (x \<Rightarrow> rcl_val option) \<Rightarrow> type_de "\<forall>x1a x2a x3 x4. (\<exists>v5. Some v5 = x3 x2a \<and> wfRCV x4 v5 x1a) = (Some (ss x1a x2a x3 x4) = by moura (* 0.0 ms *) then have f1: "Some (ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T) = i x1 \<and> wfRCV T (ss b2[bv::=b]\<^sub>b\< using boxed_i_GConsI.prems(1) hd wfI_def by auto (* 31 ms *) then have "ss b2[bv::=b]\<^sub>b\<^sub>b x1 i T = s" by (metis (no_types) boxed_i_GConsI.hyps(1) option.inject) (* 0.0 ms *) then show ?thesis using f1 by blast (* 0.0 ms *) qed ultimately have "wfRCV T s' b2" using boxed_i_GConsI boxed_b_wfRCV by metis then show ?thesis using hd by simp next case tail hence "wfI T G i'" using boxed_i_GConsI wfI_suffix wfG_suffix subst_gb.simps by (metis (no_types, lifting) Un_iff toSet.simps(2) wfG_cons2 wfI_def) then show ?thesis using wfI_def[of T G i'] tail using boxed_i_GConsI.prems(3) split_G wfG_cons_fresh2 by fastforce qed } thus ?case using wfI_def by fast qed lemma is_satis_g_bs_boxed_aux: fixes G::\<Gamma> assumes "boxed_i \<Theta> G1 b bv i i'" and "wfI \<Theta> G1[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "wfI \< and "(i \<Turnstile> G[bv::=b]\<^sub>\<Gamma>\<^sub>b) " shows "(i' \<Turnstile> G)" using assms proof(induct G arbitrary: G2 rule: \<Gamma>_induct) case GNil then show ?case by auto next case (GCons x' b' c' \<Gamma>' G2) show ?case proof(subst is_satis_g.simps,rule) have *:"wfC \<Theta> B G1 c'" using GCons wfG_wfC_inside by force show "i' \<Turnstile> c'" using is_satis_bs_boxed[OF assms(1) * ] GCons by auto obtain G3 where "G1 = G3 @ \<Gamma>'" using GCons append_g.simps by (metis append_g_assoc) then show "i' \<Turnstile> \<Gamma>'" using GCons append_g.simps by simp qed qed lemma is_satis_g_bs_boxed: fixes G::\<Gamma> assumes "boxed_i \<Theta> G b bv i i'" and "wfI \<Theta> G[bv::=b]\<^sub>\<Gamma>\<^sub>b i" and "wfI \<Th and "(i \<Turnstile> G[bv::=b]\<^sub>\<Gamma>\<^sub>b) " shows "(i' \<Turnstile> 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 "\<Theta> ; {||} \<turnstile>\<^sub>w\<^sub>f b" and "B = {|bv|}" and "\<Theta> ; {|bv|} ;\<Gamma> shows "\<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b proof(rule validI) show **:"\<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile>\<^sub>w\<^sub>f c[bv::= show "\<forall>i. (wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i \<and> i \<Turnstile> \<Gamma>[bv proof(rule,rule) fix i assume *:"wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i \<and> i \<Turnstile> \<Gamma>[bv::=b]\< obtain i' where idash: "boxed_i \<Theta> \<Gamma> b bv i i'" using boxed_i_ex wfX_wfY assms * by fast have wfc: "\<Theta> ; {|bv|} ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f c" using valid.simps assms by simp have wfg: "\<Theta> ; {|bv|} \<turnstile>\<^sub>w\<^sub>f \<Gamma>" using valid.simps wfX_wfY assms b hence wfi: "wfI \<Theta> \<Gamma> i'" using idash * bs_boxed_wfi_aux subst_gb.simps wfX_wfY by me moreover have "i' \<Turnstile> \<Gamma>" proof (rule is_satis_g_bs_boxed[OF idash ] wfX_wfY(2) show "wfI \<Theta> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b i" using subst_gb.simps * by simp show "wfI \<Theta> \<Gamma> i'" using wfi by auto show "\<Theta> ; B \<turnstile>\<^sub>w\<^sub>f \<Gamma> " using wfg assms by auto show "i \<Turnstile> \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b" using subst_gb.simps * by simp qed ultimately have ic:"i' \<Turnstile> c" using assms valid_def using valid.simps by blast show "i \<Turnstile> c[bv::=b]\<^sub>c\<^sub>b" proof(rule is_satis_bs_boxed_rev) show "\<Theta> ; \<Gamma> ; b , bv \<turnstile> i \<approx> i'" using idash by auto show "\<Theta> ; B ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f c " using wfc assms by auto show "\<Theta> ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile> i" using subst_gb.simps * by sim show "\<Theta> ; \<Gamma> \<turnstile> i'" using wfi by auto show "\<Theta> ; {||} ; \<Gamma>[bv::=b]\<^sub>\<Gamma>\<^sub>b \<turnstile>\<^sub>w\<^sub>f c[bv::=b]\< show "i' \<Turnstile> c" using ic by auto qed qed qed section \<open>Expression Operator Lemmas\<close> lemma is_satis_len_imp: assumes "i \<Turnstile> (CE_val (V_var x) == CE_val (V_lit (L_num (int (length v)))) )" (is "is_s shows "i \<Turnstile> (CE_val (V_var x) == CE_len [V_lit (L_bitvec v)]\<^sup>c\<^sup>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)]\<^sup>c\<^sup>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 \<Turnstile> (CE_val (V_var x) == CE_val (V_lit (L_num (n1+n2))))" (is "is_satis i ?c shows "i \<Turnstile> (CE_val (V_var x) == CE_op Plus ([V_lit (L_num n1)]\<^sup>c\<^sup>e) ([V_lit 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)]\<^sup>c\<^sup>e) ([V_lit (L_num n2)]\<^s 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 \<Turnstile> (CE_val (V_var x) == CE_val (V_lit (if (n1 \<le> n2) then L_true else L_fals shows "i \<Turnstile> (CE_val (V_var x) == CE_op LEq [(V_lit (L_num n1))]\<^sup>c\<^sup>e [(V_lit ( 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 \<le> n2) then L_true else L_false)))) (SBool (n1\<le>n 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\<le>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))]\<^sup>c\<^sup>e [(V_lit (L_num n2) )]\<^s 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 "\<lbrakk> n1 \<rbrakk> = s" and "\<lbrakk> n2 \<rbrakk> = 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 \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s" and "i \<lbrakk> [ [ n2 ]\<^sup>v ]\<^sup>c shows "n1=n2" using eval_lit_inj assms eval_e_elims eval_v_elims by metis lemma is_satis_eq_imp: assumes "i \<Turnstile> (CE_val (V_var x) == CE_val (V_lit (if (n1 = n2) then L_true else L_false) shows "i \<Turnstile> (CE_val (V_var x) == CE_op Eq [(V_lit (n1))]\<^sup>c\<^sup>e [(V_lit (n2))]\< 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))]\<^sup>c\<^sup>e [(V_lit (n2) )]\<^sup>c\<^sup>e) ( proof - obtain s1 and s2 where *:"i \<lbrakk> [ [ n1 ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1 \<and> i \<lbrakk> [ [ n2 ] 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))]\<^sup>c\<^sup>e" s1 "[(V_lit (n2 qed ultimately show ?thesis using eval_c.intros is_satis.simps by fastforce qed lemma valid_eq_e: assumes "\<forall>i s1 s2. wfG P \<B> GNil \<and> wfI P GNil i \<and> eval_e i e1 s1 \<and> eval_e i e2 s2 \<longr and "wfCE P \<B> GNil e1 b" and "wfCE P \<B> GNil e2 b" shows "P ; \<B> ; (x, b , CE_val (V_var x) == e1 )#\<^sub>\<Gamma> GNil \<Turnstile> CE_val (V_var x) == e2" unfolding valid.simps proof(intro conjI) show \<open> P ; \<B> ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == e1 ) #\<^sub>\<Gamma> GNil \<turnstile>\<^sub>w\< using assms wf_intros wfX_wfY b.eq_iff fresh_GNil wfC_e_eq2 wfV_elims by meson show \<open>\<forall>i. ((P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == e1 ) #\<^sub>\<Gamma> GNil \<turnstil (i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == e2)) \<close> proof(rule+) fix i assume as:"P ; (x, b, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == e1 ) #\<^sub>\<Gamma> GNil \<turnstile> i \<and> i \<Tu have *: "P ; GNil \<turnstile> 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 \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>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.c qed moreover have "s1 = s2" using s1 s2 * assms wfG_nilI wfX_wfY by metis ultimately show "i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == e2 \<rbrakk> ~ True" using eval_c.intros eval_e.intros eval_v.intros proof - have "i \<lbrakk> e2 \<rbrakk> ~ s1" by (metis \<open>s1 = s2\<close> s2) (* 0.0 ms *) then show ?thesis by (metis (full_types) \<open>i x = Some s1\<close> eval_c_eqI eval_e_valI eval_v_varI) (* 31 ms * qed qed qed lemma valid_len: assumes " \<turnstile>\<^sub>w\<^sub>f \<Theta>" shows "\<Theta> ; \<B> ; (x, B_int, [[x]\<^sup>v]\<^sup>c\<^sup>e == [[ L_num (int (length v)) ]\<^sup>v]\< proof - have *:"\<Theta> \<turnstile>\<^sub>w\<^sub>f ([]::\<Phi>) \<and> \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\< moreover hence "\<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f CE_val (V_lit (L_num (int (length v using wfCE_valI * wfV_litI base_for_lit.simps by (metis wfE_valI wfX_wfY) moreover have "\<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f CE_len [(V_lit (L_bitvec v))]\<^sup> using wfE_valI * wfV_litI base_for_lit.simps wfE_valI wfX_wfY wfCE_valI by (metis wfCE_lenI) moreover have "atom x \<sharp> GNil" by auto ultimately have "\<Theta> ; \<B> ; ?G \<turnstile>\<^sub>w\<^sub>f ?c" using wfC_e_eq2 assms by simp moreover have "(\<forall>i. wfI \<Theta> ?G i \<and> is_satis_g i ?G \<longrightarrow> is_satis i ?c)" ultimately show ?thesis using valid.simps by auto qed lemma valid_arith_bop: assumes "wfG \<Theta> \<B> \<Gamma>" and "opp = Plus \<and> ll = (L_num (n1+n2)) \<or> (opp = LEq \<and> ll = ( if and "(opp = Plus \<longrightarrow> b = B_int) \<and> (opp = LEq \<longrightarrow> b = B_bool)" and "atom x \<sharp> \<Gamma>" shows "\<Theta>; \<B> ; (x, b, (CE_val (V_var x) == CE_val (V_lit (ll)) )) #\<^sub>\<Gamma> \<Gamma> \<Turnstile> (CE_val (V_var x) == CE_op opp ([V_lit (L_num n1)]\<^sup>c\<^sup>e) ([V_lit (L_num n2 proof - have "wfC \<Theta> \<B> ?G ?c" proof(rule wfC_e_eq2) show "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f CE_val (V_lit ll) : b" using wfCE_valI wfV_l show "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f CE_op opp ([V_lit (L_num n1)]\<^sup>c\<^sup>e using wfCE_plusI wfCE_leqI wfCE_eqI wfV_litI wfCE_valI base_for_lit.simps assms by metis show "\<turnstile>\<^sub>w\<^sub>f \<Theta>" using assms wfX_wfY by auto show "atom x \<sharp> \<Gamma>" using assms by auto qed moreover have "\<forall>i. wfI \<Theta> ?G i \<and> is_satis_g i ?G \<longrightarrow> is_satis i ?c" pr fix i assume "wfI \<Theta> ?G i \<and> 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)]\<^sup>c\<^sup>e) ([V_lit (L_ 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 \<Theta> \<B> \<Gamma>" and "atom x \<sharp> \<Gamma>" and "base_for_lit l1 = base_for_lit l shows "\<Theta>; \<B> ; (x, B_bool, (CE_val (V_var x) == CE_val (V_lit (if l1 = l2 then L_true else L_f \<Turnstile> (CE_val (V_var x) == CE_op Eq ([V_lit (l1)]\<^sup>c\<^sup>e) ([V_lit (l2)]\<^sup>c\<^s proof - let ?ll = "(if l1 = l2 then L_true else L_false)" have "wfC \<Theta> \<B> ?G ?c" proof(rule wfC_e_eq2) show "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f CE_val (V_lit ?ll) : B_bool" using wfCE_val show "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f CE_op Eq ([V_lit (l1)]\<^sup>c\<^sup>e) ([V_l using wfCE_eqI wfCE_leqI wfCE_eqI wfV_litI wfCE_valI base_for_lit.simps assms by metis show "\<turnstile>\<^sub>w\<^sub>f \<Theta>" using assms wfX_wfY by auto show "atom x \<sharp> \<Gamma>" using assms by auto qed moreover have "\<forall>i. wfI \<Theta> ?G i \<and> is_satis_g i ?G \<longrightarrow> is_satis i ?c" pr fix i assume "wfI \<Theta> ?G i \<and> 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)]\<^sup>c\<^sup>e) ([V_lit (l2)]\<^su 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\<^sub>1::v and v\<^sub>2::v assumes "wfTh \<Theta>" and "wfV \<Theta> \<B> GNil (V_pair v\<^sub>1 v\<^sub>2) (B_pair b\<^sub>1 b\<^sub> shows "\<Theta> ; \<B> ; (x, b\<^sub>1, [[x]\<^sup>v]\<^sup>c\<^sup>e == [v\<^sub>1]\<^sup>c\<^sup>e) #\<^sub> proof(rule valid_eq_e) show \<open>\<forall>i s1 s2. (\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f GNil) \<and> (\<Theta> ; GNil \<turn proof(rule+) fix i s1 s2 assume as:"\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f GNil \<and> \<Theta> ; GNil \<turnstile> i \<and> (i \<lb then obtain s2' where *:"i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2 s2'" using eval_e_elims(5)[of i "[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e" s2] eval_e_elims by meson then have " i \<lbrakk> v\<^sub>1 \<rbrakk> ~ 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 \<open> \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>1 ]\<^sup>c\<^sup>e : b\<^sub>1 \<close> by (metis b.eq_iff(4) wfV_elims(3) wfV_wfCE) show \<open> \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#1[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\< using wfCE_valI by blast qed lemma valid_snd: fixes x::x and v\<^sub>1::v and v\<^sub>2::v assumes "wfTh \<Theta>" and "wfV \<Theta> \<B> GNil (V_pair v\<^sub>1 v\<^sub>2) (B_pair b\<^sub>1 b\<^sub> shows "\<Theta> ; \<B> ; (x, b\<^sub>2, [[x]\<^sup>v]\<^sup>c\<^sup>e == [v\<^sub>2]\<^sup>c\<^sup>e) #\<^sub> proof(rule valid_eq_e) show \<open>\<forall>i s1 s2. (\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f GNil) \<and> (\<Theta> ; GNil \<turn (i \<lbrakk> [#2[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ s2) \<longri proof(rule+) fix i s1 s2 assume as:"\<Theta> ; \<B> \<turnstile>\<^sub>w\<^sub>f GNil \<and> \<Theta> ; GNil \<turnstile> i \<and> (i \<lb then obtain s2' where *:"i \<lbrakk> [ v\<^sub>1 , v\<^sub>2 ]\<^sup>v \<rbrakk> ~ SPair s2' s2" using eval_e_elims(5)[of i "[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\<^sup>e" s2] eval_e_elims by meson then have " i \<lbrakk> v\<^sub>2 \<rbrakk> ~ 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 \<open> \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ v\<^sub>2 ]\<^sup>c\<^sup>e : b\<^sub>2 \<close> by (metis b.eq_iff wfV_elims wfV_wfCE) show \<open> \<Theta> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [#2[[ v\<^sub>1 , v\<^sub>2 ]\<^sup>v]\<^sup>c\< qed lemma valid_concat: fixes v1::"bit list" and v2::"bit list" assumes " \<turnstile>\<^sub>w\<^sub>f \<Pi>" shows "\<Pi> ; \<B> ; (x, B_bitvec, (CE_val (V_var x) == CE_val (V_lit (L_bitvec (v1@ v2))))) #\<^sub> (CE_val (V_var x) == CE_concat ([V_lit (L_bitvec v1)]\<^sup>c\<^sup>e ) ([V_lit (L_bitvec v2)]\< proof(rule valid_eq_e) show \<open>\<forall>i s1 s2. ((\<Pi> ; \<B> \<turnstile>\<^sub>w\<^sub>f GNil) \<and> (\<Pi> ; GNil \<turnstile> (i \<lbrakk> [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ s1) \<and> (i \<lbrakk> [[[ L_bitve s1 = s2)\<close> proof(rule+) fix i s1 s2 assume as: "(\<Pi> ; \<B> \<turnstile>\<^sub>w\<^sub>f GNil) \<and> (\<Pi> ; GNil \<turnstile> i) \<and> (i \<lbra (i \<lbrakk> [[[ L_bitvec v1 ]\<^sup>v]\<^sup>c\<^sup>e @@ [[ L_bitvec v2 ]\<^sup>v]\<^sup>c\<^sup>e]\<^s hence *: "i \<lbrakk> [[[ L_bitvec v1 ]\<^sup>v]\<^sup>c\<^sup>e @@ [[ L_bitvec v2 ]\<^sup>v]\<^sup>c\<^s obtain bv1 bv2 where s2:"s2 = SBitvec (bv1 @ bv2) \<and> i \<lbrakk> [ L_bitvec v1 ]\<^sup>v \<rbrakk> ~ SB using eval_e_elims(7)[OF *] eval_e_elims(1) by metis hence "v1 = bv1 \<and> 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 \<open> \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [ [ L_bitvec (v1 @ v2) ]\<^sup>v ]\<^sup>c\<^sup>e : by (metis assms base_for_lit.simps(5) wfG_nilI wfV_litI wfV_wfCE) show \<open> \<Pi> ; \<B> ; GNil \<turnstile>\<^sub>w\<^sub>f [[[ L_bitvec v1 ]\<^sup>v]\<^sup>c\<^sup>e @@ [[ L 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 "\<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce : b" shows \<open>\<Theta> ; \<B> ; \<Gamma> \<Turnstile> ce == ce \<close> unfolding valid.simps proof show \<open> \<Theta> ; \<B> ; \<Gamma> \<turnstile>\<^sub>w\<^sub>f ce == ce \<close> using assms wfC_eqI by au show \<open>\<forall>i. \<Theta> ; \<Gamma> \<turnstile> i \<and> i \<Turnstile> \<Gamma> \<longrightarrow> i \< fix i assume "\<Theta> ; \<Gamma> \<turnstile> i \<and> i \<Turnstile> \<Gamma>" then obtain s where "i\<lbrakk> ce \<rbrakk> ~ s" using assms eval_e_exist by metis then show "i \<lbrakk> ce == ce \<rbrakk> ~ True " using eval_c_eqI by metis qed qed lemma valid_eq_imp: fixes c1::c and c2::c assumes " \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile>\<^sub>w\<^sub>f c1 IMP c2" shows " \<Theta> ; \<B> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<Turnstile> c1 IMP c2 " have <x,,c2#<sub<>\turnstile>i\and> <Turnstile(,b c2 #<sub\amma\Gamma) \longrightarrow>i Turnst proof(rule,rule) fix i assume as:"\<Theta> ; (x, b, c2) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i \<and> i \<Turnstile> * Theta>xb <>GammaGamma\turnstile><sub wfC_elims metis then obtainlet moreover have. ct ultimately have "i \<lbrakk> c1 IMP c2 \<rbrakk> ~ True" using eval_c_impI by metis thus "i \<Turnstile> c1 IMP c2" using is_satis.simps by auto qed thus ?thesis using assms by auto qed lemma valid_range: assumes "0 \<le> n \<and> n \<le> m" and "\<turnstile>\<^sub>w\<^sub>f \<Theta>" shows "\<Theta> ; {||} ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #\<^sub>\< (C_eq (CE_op LEq (CE_val (V_var x)) (CE_val (V_lit (L_num m)))) [[ L_true ]\<^sup>v ]\<^sup>c\<^su (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]\<^sup>v ]\<^sup>c\<^su (is "\<Theta> ; {||} ; ?G \<Turnstile> ?c1 AND ?c2") proof(rule validI) have wfg: " \<Theta> ; {||} \<turnstile>\<^sub>w\<^sub>f (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == [ [ L_ using assms base_for_lit.simps wfG_nilI wfV_litI fresh_GNil wfB_intI wfC_v_eq wfG_cons1I show "\<Theta> ; {||} ; ?G \<turnstile>\<^sub>w\<^sub>f ?c1 AND ?c2" using wfC_conjI wfC_eqI wfCE_leqI wfCE_valI wfV_varI wfg lookup.simps base_for_lit.simps by metis show "\<forall>i. \<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G \<longrightarrow> i \<Turnstile> ?c1 fix i assume a:"\<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G" hence *:"i \<lbrakk> V_var x \<rbrakk> ~ SNum n" proof - obtain sv where sv: "i x = Some sv \<and> \<Theta> \<turnstile> sv : B_int" using a wfI_def by force have "i \<lbrakk> (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n)))) \<rbrakk> ~ 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 thus ?thesis using eval_v_varI by auto qed show "i \<Turnstile> ?c1 AND ?c2" proof - have "i \<lbrakk> ?c1 \<rbrakk> ~ True" proof - have "i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [ [ L_num m ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup> using eval_e_leqI assms eval_v_litI eval_l.simps * by (metis (full_types) eval_e_valI) moreover have "i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ 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 \<lbrakk> ?c2 \<rbrakk> ~ True" proof - have "i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup> using eval_e_leqI assms eval_v_litI eval_l.simps * by (metis (full_types) eval_e_valI) moreover have "i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ 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 \<Gamma>::\<Gamma> assumes "0 \<le> n \<and> n \<le> int (length v)" and " \<Theta> ; {||} \<turnstile>\<^sub>w\<^sub>f \<Gamma>" an shows "\<Theta> ; {||} ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #\<^sub>\< (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]\<^sup>v ]\<^sup>c\<^su (C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e )) " (is "\<Theta> ; {||} ; ?G \<Turnstile> ?c1 AND ?c2") proof(rule validI) have wfg: " \<Theta> ; {||} \<turnstile>\<^sub>w\<^sub>f (x, B_int, [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == [ [ L_ 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 show "\<Theta> ; {||} ; ?G \<turnstile>\<^sub>w\<^sub>f ?c1 AND ?c2" using wfC_conjI wfC_eqI wfCE_leqI wfCE_valI wfV_varI wfg lookup.simps base_for_lit.simps by (metis (full_types) wfCE_lenI) show "\<forall>i. \<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G \<longrightarrow> i \<Turnstile> ?c1 fix i assume a:"\<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G" hence *:"i \<lbrakk> V_var x \<rbrakk> ~ SNum n" proof - obtain sv where sv: "i x = Some sv \<and> \<Theta> \<turnstile> sv : B_int" using a wfI_def by force have "i \<lbrakk> (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n)))) \<rbrakk> ~ 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 thus ?thesis using eval_v_varI by auto qed show "i \<Turnstile> ?c1 AND ?c2" proof - have "i \<lbrakk> ?c2 \<rbrakk> ~ True" proof - have "i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e [| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup> using eval_e_leqI assms eval_v_litI eval_l.simps * by (metis (full_types) eval_e_lenI eval_e_valI) moreover have "i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ 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 \<lbrakk> ?c1 \<rbrakk> ~ True" proof - have "i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e ]\<^sup>c\<^sup> using eval_e_leqI assms eval_v_litI eval_l.simps * by (metis (full_types) eval_e_valI) moreover have "i \<lbrakk> [ [ L_true ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ 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 \<Gamma>::\<Gamma> assumes "\<turnstile>\<^sub>w\<^sub>f \<Theta> " and "\<Theta> ; {||} ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #\<^sub>\<Ga (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]\<^sup>v ]\<^sup>c\<^su (C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e )) " (is "\<Theta> ; {||} ; ?G \<Turnstile> ?c1 AND ?c2") shows "0 \<le> n \<and> n \<le> int (length v)" proof - have *:"\<forall>i. \<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G \<longrightarrow> i \<Turnstile> ? obtain i where i: "i x = Some (SNum n)" by auto have "\<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G" proof show "\<Theta> ; ?G \<turnstile> i" unfolding wfI_def using wfRCV_BIntI i * by auto have "i \<lbrakk> ([ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) \<rbrakk> ~ True using * eval_c.intros(7) eval_e.intros eval_v.intros eval_l.simps by (metis (full_types) i) thus "i \<Turnstile> ?G" unfolding is_satis_g.simps is_satis.simps by auto qed hence **:"i \<Turnstile> ?c1 AND ?c2" using * by auto hence 1: "i \<lbrakk> ?c1 \<rbrakk> ~ True" using eval_c_elims(3) is_satis.simps by fastforce then obtain sv1 and sv2 where "(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^s 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 \<le> n2) \<and> (i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^ using eval_e_elims(3)[of i " [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e" "[ [ x ]\<^sup>v ]\<^sup>c\<^sup>e " " using \<open>(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\< 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 \<le> n " by simp hence 2: "i \<lbrakk> ?c2 \<rbrakk> ~ True" using ** eval_c_elims(3) is_satis.simps by fastforce then obtain sv1 and sv2 where sv: "(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup> 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 \<le> n2) \<and> (i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^s using eval_e_elims(3) using sv \<open>sv1 = SBool True\<close> 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 \<le> int (length v) " by simp show ?thesis using le1 le2 by auto qed lemma wfI_cons: fixes i::valuation and \<Gamma>::\<Gamma> assumes "i' \<Turnstile> \<Gamma>" and "\<Theta> ; \<Gamma> \<turnstile> i'" and "i = i' ( x \<mapsto> s)" and shows "\<Theta> ; (x,b,c) #\<^sub>\<Gamma> \<Gamma> \<turnstile> i" unfolding wfI_def proof - { fix x' b' c' assume "(x',b',c') \<in> toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>)" then consider "(x',b',c') = (x,b,c)" | "(x',b',c') \<in> toSet \<Gamma>" using toSet.simps by aut then have "\<exists>s. Some s = i x' \<and> \<Theta> \<turnstile> 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' \<and> \<Theta> \<turnstile> s : b'" using assms wfI_def by auto moreover have "x' \<noteq> 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 "\<forall>(x, b, c)\<in>toSet ((x, b, c) #\<^sub>\<Gamma> \<Gamma>). \<exists>s. Some s = i x \<and> \<The qed lemma valid_range_length_inv: fixes \<Gamma>::\<Gamma> assumes "\<Theta> ; B \<turnstile>\<^sub>w\<^sub>f \<Gamma> " and "atom x \<sharp> \<Gamma>" and "\<exists>i. and "\<Theta> ; B ; (x, B_int , (C_eq (CE_val (V_var x)) (CE_val (V_lit (L_num n))))) #\<^sub>\<Gamma> (C_eq (CE_op LEq (CE_val (V_lit (L_num 0))) (CE_val (V_var x))) [[ L_true ]\<^sup>v ]\<^sup>c\<^su (C_eq (CE_op LEq (CE_val (V_var x)) ([| [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e )) " (is "\<Theta> ; ?B ; ?G \<Turnstile> ?c1 AND ?c2") shows "0 \<le> n \<and> n \<le> int (length v)" proof - have *:"\<forall>i. \<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G \<longrightarrow> i \<Turnstile> ? obtain i' where idash: "is_satis_g i' \<Gamma> \<and> \<Theta> ; \<Gamma> \<turnstile> i'" using assms by obtain i where i: "i = i' ( x \<mapsto> SNum n)" by auto hence ix: "i x = Some (SNum n)" by auto have "\<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G" proof show "\<Theta> ; ?G \<turnstile> i" using wfI_cons i idash ix wfRCV_BIntI assms by simp have **:"i \<lbrakk> ([ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e ) \<rbrakk> ~ T using * eval_c.intros(7) eval_e.intros eval_v.intros eval_l.simps i by (metis (full_types) ix) show "i \<Turnstile> ?G" unfolding is_satis_g.simps proof show \<open> i \<Turnstile> [ [ x ]\<^sup>v ]\<^sup>c\<^sup>e == [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e \<close> u show \<open> i \<Turnstile> \<Gamma> \<close> using idash i assms is_satis_g_i_upd by metis qed qed hence **:"i \<Turnstile> ?c1 AND ?c2" using * by auto hence 1: "i \<lbrakk> ?c1 \<rbrakk> ~ True" using eval_c_elims(3) is_satis.simps by fastforce then obtain sv1 and sv2 where "(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^s 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 \<le> n2) \<and> (i \<lbrakk> [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^ using eval_e_elims(3)[of i " [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e" "[ [ x ]\<^sup>v ]\<^sup>c\<^sup>e " " using \<open>(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ L_num 0 ]\<^sup>v ]\<^sup>c\<^sup>e [ [ x ]\<^sup>v ]\< 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 \<le> n " by simp hence 2: "i \<lbrakk> ?c2 \<rbrakk> ~ True" using ** eval_c_elims(3) is_satis.simps by fastforce then obtain sv1 and sv2 where sv: "(sv1 = sv2) = True \<and> i \<lbrakk> [ leq [ [ x ]\<^sup>v ]\<^sup>c\<^sup> 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 \<le> n2) \<and> (i \<lbrakk> [ [ x ]\<^sup>v ]\<^sup>c\<^s using eval_e_elims(3) using sv \<open>sv1 = SBool True\<close> 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 \<le> int (length v) " by simp show ?thesis using le1 le2 by auto qed lemma eval_c_conj2I[intro]: assumes "i \<lbrakk> c1 \<rbrakk> ~ True" and "i \<lbrakk> c2 \<rbrakk> ~ True" shows "i \<lbrakk> (C_conj c1 c2) \<rbrakk> ~ True" using assms eval_c_conjI by metis lemma valid_split: assumes "split n v (v1,v2)" and "\<turnstile>\<^sub>w\<^sub>f \<Theta>" shows "\<Theta> ; {||} ; (z , [B_bitvec , B_bitvec ]\<^sup>b , [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e == [ [ [ L_bit \<Turnstile> ([ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e == [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^ (is "\<Theta> ; {||} ; ?G \<Turnstile> ?c1 AND ?c2") unfolding valid.simps proof have wfg: " \<Theta> ; {||} \<turnstile>\<^sub>w\<^sub>f (z, [B_bitvec , B_bitvec ]\<^sup>b , [ [ z ]\<^sup> using wf_intros assms base_for_lit.simps fresh_GNil wfC_v_eq wfG_intros2 by metis show "\<Theta> ; {||} ; ?G \<turnstile>\<^sub>w\<^sub>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 "\<forall>i. \<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G \<longrightarrow> i \<Turnstile> (?c proof(rule,rule) fix i assume a:"\<Theta> ; ?G \<turnstile> i \<and> i \<Turnstile> ?G" hence "i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e == [ [ [ L_bitvec v1 ]\<^sup>v , [ L_bitvec v2 ]\<^sup>v ]\< using is_satis_g.simps is_satis.simps by simp then obtain sv where "i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ sv \<and> i \<lbrakk> [ [ [ L_bitv using eval_c_elims by metis hence "i \<lbrakk> [ [ z ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ (SPair (SBitvec v1) (SBitvec v2))" using 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 met have v1: "i \<lbrakk> [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v1 " using eval_e_fstI eval_e_valI eval_v_varI b by metis have v2: "i \<lbrakk> [#2[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v2" using eval_e_sndI eval_e_valI eval_v_varI b by metis have "i \<lbrakk> [ [ L_bitvec v ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SBitvec v" using eval_e.intros e moreover have "i \<lbrakk> [ [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e @@ [#2[ [ z ]\<^sup>v ]\<^s using assms split_concat v1 v2 eval_e_concatI by metis moreover have "i \<lbrakk> [| [#1[ [ z ]\<^sup>v ]\<^sup>c\<^sup>e]\<^sup>c\<^sup>e |]\<^sup>c\<^sup>e \<rbr using v1 eval_e_lenI by auto moreover have "i \<lbrakk> [ [ L_num n ]\<^sup>v ]\<^sup>c\<^sup>e \<rbrakk> ~ SNum n" using eval_e.intro ultimately show "i \<Turnstile> ?c1 AND ?c2" using is_satis.intros eval_c_conj2I eval_c_eqI l qed qed lemma is_satis_eq: assumes "wfI \<Theta> G i" and "wfCE \<Theta> \<B> G e b" shows "is_satis i (e == e)" proof(rule) obtain s where "eval_e i e s" using eval_e_exist assms by metis thus "eval_c i (e == e ) True" using eval_c_eqI by metis qed lemma is_satis_g_i_upd2: assumes "eval_v i v s" and "is_satis ((i ( x \<mapsto> s))) c0" and "atom x \<sharp> G" and "wfG \<Theta> \< and "is_satis_g i (G3[x::=v]\<^sub>\<Gamma>\<^sub>v@G)" shows "is_satis_g (i ( x \<mapsto> s)) (G3@((x,b,c0)#\<^sub>\<Gamma>G))" using assms proof(induct G3 rule: \<Gamma>_induct) case GNil hence "is_satis_g (i(x \<mapsto> 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' \<Gamma>') hence "x\<noteq>x'" using wfG_cons_append by metis hence "is_satis_g i (((x', b', c'[x::=v]\<^sub>c\<^sub>v) #\<^sub>\<Gamma> (\<Gamma>'[x::=v]\<^sub> hence *:"is_satis i c'[x::=v]\<^sub>c\<^sub>v \<and> is_satis_g i ((\<Gamma>'[x::=v]\<^sub>\<Gamma> have "is_satis_g (i(x \<mapsto> s)) ((x', b', c') #\<^sub>\<Gamma> (\<Gamma>'@ (x, b, c0) #\<^sub>\<Gamm show "is_satis (i(x \<mapsto> s)) c'" proof(subst subst_c_satis_full[symmetric]) show \<open>eval_v i v s\<close> using GCons by auto show \<open> \<Theta> ; \<B> ; ((x', b', c') #\<^sub>\<Gamma>\<Gamma>')@(x, b, c0) #\<^sub>\<Gamma> G \<turnsti show \<open>wfI \<Theta> ((((x', b', c') #\<^sub>\<Gamma> \<Gamma>')[x::=v]\<^sub>\<Gamma>\<^sub>v) @ G) i show \<open> \<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b \<close> using GCons by auto show \<open>is_satis i c'[x::=v]\<^sub>c\<^sub>v\<close> using * by auto qed show "is_satis_g (i(x \<mapsto> s)) (\<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G)" proof(rule GCons(1)) show \<open>eval_v i v s\<close> using GCons by auto show \<open>is_satis (i(x \<mapsto> s)) c0\<close> using GCons by metis show \<open>atom x \<sharp> G\<close> using GCons by auto show \<open> \<Theta> ; \<B>\<turnstile>\<^sub>w\<^sub>f \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G \<close> using show \<open>is_satis_g i (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G)\<close> using * by auto show "wfI \<Theta> (\<Gamma>'[x::=v]\<^sub>\<Gamma>\<^sub>v @ G) i" using GCons wfI_def subst_g_asso show "\<Theta> ; \<B> ; G \<turnstile>\<^sub>w\<^sub>f v : b " using GCons by auto qed qed moreover have "((x', b', c') #\<^sub>\<Gamma> \<Gamma>' @ (x, b, c0) #\<^sub>\<Gamma> G) = (((x', b', c') # ultimately show ?case using GCons by metis qed end
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.117Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-06-10) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-06-09