# Theory Nominal_Bounded_Set

theory Nominal_Bounded_Set imports Nominal2.Nominal2 "HOL-Cardinals.Bounded_Set" begin section ‹Bounded Sets Equipped With a Permutation Action› text ‹Additional lemmas about bounded sets.› interpretation bset_lifting: bset_lifting . lemma Abs_bset_inverse' [simp]: assumes "|A| <o natLeq +c |UNIV :: 'k set|" shows "set_bset (Abs_bset A :: 'a set['k]) = A" by (metis Abs_bset_inverse assms mem_Collect_eq) text ‹Bounded sets are equipped with a permutation action, provided their elements are.› instantiation bset :: (pt,type) pt begin lift_definition permute_bset :: "perm ⇒ 'a set['b] ⇒ 'a set['b]" is permute proof - fix p and A :: "'a set" have "|p ∙ A| ≤o |A|" by (simp add: permute_set_eq_image) also assume "|A| <o natLeq +c |UNIV :: 'b set|" finally show "|p ∙ A| <o natLeq +c |UNIV :: 'b set|" . qed instance by standard (transfer, simp)+ end lemma Abs_bset_eqvt [simp]: assumes "|A| <o natLeq +c |UNIV :: 'k set|" shows "p ∙ (Abs_bset A :: 'a::pt set['k]) = Abs_bset (p ∙ A)" by (simp add: permute_bset_def map_bset_def image_def permute_set_def) (metis (no_types, lifting) Abs_bset_inverse' assms) lemma supp_Abs_bset [simp]: assumes "|A| <o natLeq +c |UNIV :: 'k set|" shows "supp (Abs_bset A :: 'a::pt set['k]) = supp A" proof - from assms have "⋀p. p ∙ (Abs_bset A :: 'a::pt set['k]) ≠ Abs_bset A ⟷ p ∙ A ≠ A" by simp (metis map_bset.rep_eq permute_set_eq_image set_bset_inverse set_bset_to_set_bset) then show ?thesis unfolding supp_def by simp qed lemma map_bset_permute: "p ∙ B = map_bset (permute p) B" by transfer (auto simp add: image_def permute_set_def) lemma set_bset_eqvt [eqvt]: "p ∙ set_bset B = set_bset (p ∙ B)" by transfer simp lemma map_bset_eqvt [eqvt]: "p ∙ map_bset f B = map_bset (p ∙ f) (p ∙ B)" by transfer simp lemma bempty_eqvt [eqvt]: "p ∙ bempty = bempty" by transfer simp lemma binsert_eqvt [eqvt]: "p ∙ (binsert x B) = binsert (p ∙ x) (p ∙ B)" by transfer simp lemma bsingleton_eqvt [eqvt]: "p ∙ bsingleton x = bsingleton (p ∙ x)" by (simp add: map_bset_permute) end

# Theory Nominal_Wellfounded

theory Nominal_Wellfounded imports Nominal2.Nominal2 begin section ‹Lemmas about Well-Foundedness and Permutations› definition less_bool_rel :: "bool rel" where "less_bool_rel ≡ {(x,y). x<y}" lemma less_bool_rel_iff [simp]: "(a,b) ∈ less_bool_rel ⟷ ¬ a ∧ b" by (metis less_bool_def less_bool_rel_def mem_Collect_eq split_conv) lemma wf_less_bool_rel: "wf less_bool_rel" by (metis less_bool_rel_iff wfUNIVI) subsection ‹Hull and well-foundedness› inductive_set hull_rel where "(p ∙ x, x) ∈ hull_rel" lemma hull_relp_reflp: "reflp hull_relp" by (metis hull_relp.intros permute_zero reflpI) lemma hull_relp_symp: "symp hull_relp" by (metis (poly_guards_query) hull_relp.simps permute_minus_cancel(2) sympI) lemma hull_relp_transp: "transp hull_relp" by (metis (full_types) hull_relp.simps permute_plus transpI) lemma hull_relp_equivp: "equivp hull_relp" by (metis equivpI hull_relp_reflp hull_relp_symp hull_relp_transp) lemma hull_rel_relcomp_subset: assumes "eqvt R" shows "R O hull_rel ⊆ hull_rel O R" proof fix x assume "x ∈ R O hull_rel" then obtain x1 x2 y where x: "x = (x1,x2)" and R: "(x1,y) ∈ R" and "(y,x2) ∈ hull_rel" by auto then obtain p where "y = p ∙ x2" by (metis hull_rel.simps) then have "-p ∙ y = x2" by (metis permute_minus_cancel(2)) then have "(-p ∙ x1, x2) ∈ R" using R assms by (metis Pair_eqvt eqvt_def mem_permute_iff) moreover have "(x1, -p ∙ x1) ∈ hull_rel" by (metis hull_rel.intros permute_minus_cancel(2)) ultimately show "x ∈ hull_rel O R" using x by auto qed lemma wf_hull_rel_relcomp: assumes "wf R" and "eqvt R" shows "wf (hull_rel O R)" using assms by (metis hull_rel_relcomp_subset wf_relcomp_compatible) lemma hull_rel_relcompI [simp]: assumes "(x, y) ∈ R" shows "(p ∙ x, y) ∈ hull_rel O R" using assms by (metis hull_rel.intros relcomp.relcompI) lemma hull_rel_relcomp_trivialI [simp]: assumes "(x, y) ∈ R" shows "(x, y) ∈ hull_rel O R" using assms by (metis hull_rel_relcompI permute_zero) end

# Theory Residual

theory Residual imports Nominal2.Nominal2 begin section ‹Residuals› subsection ‹Binding names› text ‹To define $\alpha$-equivalence, we require actions to be equipped with an equivariant function~@{term bn} that gives their binding names. Actions may only bind finitely many names. This is necessary to ensure that we can use a finite permutation to rename the binding names in an action.› class bn = fs + fixes bn :: "'a ⇒ atom set" assumes bn_eqvt: "p ∙ (bn α) = bn (p ∙ α)" and bn_finite: "finite (bn α)" lemma bn_subset_supp: "bn α ⊆ supp α" by (metis (erased, hide_lams) bn_eqvt bn_finite eqvt_at_def finite_supp supp_eqvt_at supp_finite_atom_set) subsection ‹Raw residuals and \texorpdfstring{$\alpha$}{alpha}-equivalence› text ‹Raw residuals are simply pairs of actions and states. Binding names in the action bind into (the action and) the state.› fun alpha_residual :: "('act::bn × 'state::pt) ⇒ ('act × 'state) ⇒ bool" where "alpha_residual (α1,P1) (α2,P2) ⟷ [bn α1]set. (α1, P1) = [bn α2]set. (α2, P2)" text ‹$\alpha$-equivalence is equivariant.› lemma alpha_residual_eqvt [eqvt]: assumes "alpha_residual r1 r2" shows "alpha_residual (p ∙ r1) (p ∙ r2)" using assms by (cases r1, cases r2) (simp, metis Pair_eqvt bn_eqvt permute_Abs_set) text ‹$\alpha$-equivalence is an equivalence relation.› lemma alpha_residual_reflp: "reflp alpha_residual" by (metis alpha_residual.simps prod.exhaust reflpI) lemma alpha_residual_symp: "symp alpha_residual" by (metis alpha_residual.simps prod.exhaust sympI) lemma alpha_residual_transp: "transp alpha_residual" by (rule transpI) (metis alpha_residual.simps prod.exhaust) lemma alpha_residual_equivp: "equivp alpha_residual" by (metis alpha_residual_reflp alpha_residual_symp alpha_residual_transp equivpI) subsection ‹Residuals› text ‹Residuals are raw residuals quotiented by $\alpha$-equivalence.› quotient_type ('act,'state) residual = "'act::bn × 'state::pt" / "alpha_residual" by (fact alpha_residual_equivp) lemma residual_abs_rep [simp]: "abs_residual (rep_residual res) = res" by (metis Quotient_residual Quotient_abs_rep) lemma residual_rep_abs [simp]: "alpha_residual (rep_residual (abs_residual r)) r" by (metis residual.abs_eq_iff residual_abs_rep) text ‹The permutation operation is lifted from raw residuals.› instantiation residual :: (bn,pt) pt begin lift_definition permute_residual :: "perm ⇒ ('a,'b) residual ⇒ ('a,'b) residual" is permute by (fact alpha_residual_eqvt) instance proof fix res :: "(_,_) residual" show "0 ∙ res = res" by transfer (metis alpha_residual_equivp equivp_reflp permute_zero) next fix p q :: perm and res :: "(_,_) residual" show "(p + q) ∙ res = p ∙ q ∙ res" by transfer (metis alpha_residual_equivp equivp_reflp permute_plus) qed end text ‹The abstraction function from raw residuals to residuals is equivariant. The representation function is equivariant modulo $\alpha$-equivalence.› lemmas permute_residual.abs_eq [eqvt, simp] lemma alpha_residual_permute_rep_commute [simp]: "alpha_residual (p ∙ rep_residual res) (rep_residual (p ∙ res))" by (metis residual.abs_eq_iff residual_abs_rep permute_residual.abs_eq) subsection ‹Notation for pairs as residuals› abbreviation abs_residual_pair :: "'act::bn ⇒ 'state::pt ⇒ ('act,'state) residual" ("⟨_,_⟩" [0,0] 1000) where "⟨α,P⟩ == abs_residual (α,P)" lemma abs_residual_pair_eqvt [simp]: "p ∙ ⟨α,P⟩ = ⟨p ∙ α, p ∙ P⟩" by (metis Pair_eqvt permute_residual.abs_eq) subsection ‹Support of residuals› text ‹We only consider finitely supported states now.› lemma supp_abs_residual_pair: "supp ⟨α, P::'state::fs⟩ = supp (α,P) - bn α" proof - have "supp ⟨α,P⟩ = supp ([bn α]set. (α, P))" by (simp add: supp_def residual.abs_eq_iff bn_eqvt) then show ?thesis by (simp add: supp_Abs) qed lemma bn_abs_residual_fresh [simp]: "bn α ♯* ⟨α,P::'state::fs⟩" by (simp add: fresh_star_def fresh_def supp_abs_residual_pair) lemma finite_supp_abs_residual_pair [simp]: "finite (supp ⟨α, P::'state::fs⟩)" by (metis finite_Diff finite_supp supp_abs_residual_pair) subsection ‹Equality between residuals› lemma residual_eq_iff_perm: "⟨α1,P1⟩ = ⟨α2,P2⟩ ⟷ (∃p. supp (α1, P1) - bn α1 = supp (α2, P2) - bn α2 ∧ (supp (α1, P1) - bn α1) ♯* p ∧ p ∙ (α1, P1) = (α2, P2) ∧ p ∙ bn α1 = bn α2)" (is "?l ⟷ ?r") proof assume *: "?l" then have "[bn α1]set. (α1, P1) = [bn α2]set. (α2, P2)" by (simp add: residual.abs_eq_iff) then obtain p where "(bn α1, (α1,P1)) ≈set ((=)) supp p (bn α2, (α2,P2))" using Abs_eq_iff(1) by blast then show "?r" by (metis (mono_tags, lifting) alpha_set.simps) next assume *: "?r" then obtain p where "(bn α1, (α1,P1)) ≈set ((=)) supp p (bn α2, (α2,P2))" using alpha_set.simps by blast then have "[bn α1]set. (α1, P1) = [bn α2]set. (α2, P2)" using Abs_eq_iff(1) by blast then show "?l" by (simp add: residual.abs_eq_iff) qed lemma residual_eq_iff_perm_renaming: "⟨α1,P1⟩ = ⟨α2,P2⟩ ⟷ (∃p. supp (α1, P1) - bn α1 = supp (α2, P2) - bn α2 ∧ (supp (α1, P1) - bn α1) ♯* p ∧ p ∙ (α1, P1) = (α2, P2) ∧ p ∙ bn α1 = bn α2 ∧ supp p ⊆ bn α1 ∪ p ∙ bn α1)" (is "?l ⟷ ?r") proof assume "?l" then obtain p where p: "supp (α1, P1) - bn α1 = supp (α2, P2) - bn α2 ∧ (supp (α1, P1) - bn α1) ♯* p ∧ p ∙ (α1, P1) = (α2, P2) ∧ p ∙ bn α1 = bn α2" by (metis residual_eq_iff_perm) moreover obtain q where q_p: "∀b∈bn α1. q ∙ b = p ∙ b" and supp_q: "supp q ⊆ bn α1 ∪ p ∙ bn α1" by (metis set_renaming_perm2) have "supp q ⊆ supp p" proof fix a assume *: "a ∈ supp q" then show "a ∈ supp p" proof (cases "a ∈ bn α1") case True then show ?thesis using "*" q_p by (metis mem_Collect_eq supp_perm) next case False then have "a ∈ p ∙ bn α1" using "*" supp_q using UnE subsetCE by blast with False have "p ∙ a ≠ a" by (metis mem_permute_iff) then show ?thesis using fresh_def fresh_perm by blast qed qed with p have "(supp (α1, P1) - bn α1) ♯* q" by (meson fresh_def fresh_star_def subset_iff) moreover with p and q_p have "⋀a. a ∈ supp α1 ⟹ q ∙ a = p ∙ a" and "⋀a. a ∈ supp P1 ⟹ q ∙ a = p ∙ a" by (metis Diff_iff fresh_perm fresh_star_def UnCI supp_Pair)+ then have "q ∙ α1 = p ∙ α1" and "q ∙ P1 = p ∙ P1" by (metis supp_perm_perm_eq)+ ultimately show "?r" using supp_q by (metis Pair_eqvt bn_eqvt) next assume "?r" then show "?l" by (meson residual_eq_iff_perm) qed subsection ‹Strong induction› lemma residual_strong_induct: assumes "⋀(act::'act::bn) (state::'state::fs) (c::'a::fs). bn act ♯* c ⟹ P c ⟨act,state⟩" shows "P c residual" proof (rule residual.abs_induct, clarify) fix act :: 'act and state :: 'state obtain p where 1: "(p ∙ bn act) ♯* c" and 2: "supp ⟨act,state⟩ ♯* p" proof (rule at_set_avoiding2[of "bn act" c "⟨act,state⟩", THEN exE]) show "finite (bn act)" by (fact bn_finite) next show "finite (supp c)" by (fact finite_supp) next show "finite (supp ⟨act,state⟩)" by (fact finite_supp_abs_residual_pair) next show "bn act ♯* ⟨act,state⟩" by (fact bn_abs_residual_fresh) qed metis from 2 have "⟨p ∙ act, p ∙ state⟩ = ⟨act,state⟩" using supp_perm_eq by fastforce then show "P c ⟨act,state⟩" using assms 1 by (metis bn_eqvt) qed subsection ‹Other lemmas› lemma residual_empty_bn_eq_iff: assumes "bn α1 = {}" shows "⟨α1,P1⟩ = ⟨α2,P2⟩ ⟷ α1 = α2 ∧ P1 = P2" proof assume "⟨α1,P1⟩ = ⟨α2,P2⟩" with assms have "[{}]set. (α1, P1) = [bn α2]set. (α2, P2)" by (simp add: residual.abs_eq_iff) then obtain p where "({}, (α1, P1)) ≈set ((=)) supp p (bn α2, (α2, P2))" using Abs_eq_iff(1) by blast then show "α1 = α2 ∧ P1 = P2" unfolding alpha_set using supp_perm_eq by fastforce next assume "α1 = α2 ∧ P1 = P2" then show "⟨α1,P1⟩ = ⟨α2,P2⟩" by simp qed ― ‹The following lemma is not about residuals, but we have no better place for it.› lemma set_bounded_supp: assumes "finite S" and "⋀x. x∈X ⟹ supp x ⊆ S" shows "supp X ⊆ S" proof - have "S supports X" unfolding supports_def proof (clarify) fix a b assume a: "a ∉ S" and b: "b ∉ S" { fix x assume "x ∈ X" then have "(a ⇌ b) ∙ x = x" using a b ‹⋀x. x∈X ⟹ supp x ⊆ S› by (meson fresh_def subsetCE swap_fresh_fresh) } then show "(a ⇌ b) ∙ X = X" by auto (metis (full_types) eqvt_bound mem_permute_iff, metis mem_permute_iff) qed then show "supp X ⊆ S" using assms(1) by (fact supp_is_subset) qed end

# Theory Transition_System

theory Transition_System imports Residual begin section ‹Nominal Transition Systems and Bisimulations› subsection ‹Basic Lemmas› lemma symp_eqvt [eqvt]: assumes "symp R" shows "symp (p ∙ R)" using assms unfolding symp_def by (subst permute_fun_def)+ (simp add: permute_pure) subsection ‹Nominal transition systems› locale nominal_ts = fixes satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool" (infix "⊢" 70) and transition :: "'state ⇒ ('act::bn,'state) residual ⇒ bool" (infix "→" 70) assumes satisfies_eqvt [eqvt]: "P ⊢ φ ⟹ p ∙ P ⊢ p ∙ φ" and transition_eqvt [eqvt]: "P → αQ ⟹ p ∙ P → p ∙ αQ" begin lemma transition_eqvt': assumes "P → ⟨α,Q⟩" shows "p ∙ P → ⟨p ∙ α, p ∙ Q⟩" using assms by (metis abs_residual_pair_eqvt transition_eqvt) end subsection ‹Bisimulations› context nominal_ts begin definition is_bisimulation :: "('state ⇒ 'state ⇒ bool) ⇒ bool" where "is_bisimulation R ≡ symp R ∧ (∀P Q. R P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)) ∧ (∀P Q. R P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ R P' Q')))" definition bisimilar :: "'state ⇒ 'state ⇒ bool" (infix "∼⋅" 100) where "P ∼⋅ Q ≡ ∃R. is_bisimulation R ∧ R P Q" text ‹@{const bisimilar} is an equivariant equivalence relation.› lemma is_bisimulation_eqvt (*[eqvt]*): assumes "is_bisimulation R" shows "is_bisimulation (p ∙ R)" using assms unfolding is_bisimulation_def proof (clarify) assume 1: "symp R" assume 2: "∀P Q. R P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)" assume 3: "∀P Q. R P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ R P' Q'))" have "symp (p ∙ R)" (is ?S) using 1 by (simp add: symp_eqvt) moreover have "∀P Q. (p ∙ R) P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)" (is ?T) proof (clarify) fix P Q φ assume *: "(p ∙ R) P Q" and **: "P ⊢ φ" from * have "R (-p ∙ P) (-p ∙ Q)" by (simp add: eqvt_lambda permute_bool_def unpermute_def) then show "Q ⊢ φ" using 2 ** by (metis permute_minus_cancel(1) satisfies_eqvt) qed moreover have "∀P Q. (p ∙ R) P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ (p ∙ R) P' Q'))" (is ?U) proof (clarify) fix P Q α P' assume *: "(p ∙ R) P Q" and **: "bn α ♯* Q" and ***: "P → ⟨α,P'⟩" from * have "R (-p ∙ P) (-p ∙ Q)" by (simp add: eqvt_lambda permute_bool_def unpermute_def) moreover have "bn (-p ∙ α) ♯* (-p ∙ Q)" using ** by (metis bn_eqvt fresh_star_permute_iff) moreover have "-p ∙ P → ⟨-p ∙ α, -p ∙ P'⟩" using *** by (metis transition_eqvt') ultimately obtain Q' where T: "-p ∙ Q → ⟨-p ∙ α,Q'⟩" and R: "R (-p ∙ P') Q'" using 3 by metis from T have "Q → ⟨α, p ∙ Q'⟩" by (metis permute_minus_cancel(1) transition_eqvt') moreover from R have "(p ∙ R) P' (p ∙ Q')" by (metis eqvt_apply eqvt_lambda permute_bool_def unpermute_def) ultimately show "∃Q'. Q → ⟨α,Q'⟩ ∧ (p ∙ R) P' Q'" by metis qed ultimately show "?S ∧ ?T ∧ ?U" by simp qed lemma bisimilar_eqvt (*[eqvt]*): assumes "P ∼⋅ Q" shows "(p ∙ P) ∼⋅ (p ∙ Q)" proof - from assms obtain R where *: "is_bisimulation R ∧ R P Q" unfolding bisimilar_def .. then have "is_bisimulation (p ∙ R)" by (simp add: is_bisimulation_eqvt) moreover from "*" have "(p ∙ R) (p ∙ P) (p ∙ Q)" by (metis eqvt_apply permute_boolI) ultimately show "(p ∙ P) ∼⋅ (p ∙ Q)" unfolding bisimilar_def by auto qed lemma bisimilar_reflp: "reflp bisimilar" proof (rule reflpI) fix x have "is_bisimulation (=)" unfolding is_bisimulation_def by (simp add: symp_def) then show "x ∼⋅ x" unfolding bisimilar_def by auto qed lemma bisimilar_symp: "symp bisimilar" proof (rule sympI) fix P Q assume "P ∼⋅ Q" then obtain R where *: "is_bisimulation R ∧ R P Q" unfolding bisimilar_def .. then have "R Q P" unfolding is_bisimulation_def by (simp add: symp_def) with "*" show "Q ∼⋅ P" unfolding bisimilar_def by auto qed lemma bisimilar_is_bisimulation: "is_bisimulation bisimilar" unfolding is_bisimulation_def proof show "symp (∼⋅)" by (fact bisimilar_symp) next show "(∀P Q. P ∼⋅ Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)) ∧ (∀P Q. P ∼⋅ Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ P' ∼⋅ Q')))" by (auto simp add: is_bisimulation_def bisimilar_def) blast qed lemma bisimilar_transp: "transp bisimilar" proof (rule transpI) fix P Q R assume PQ: "P ∼⋅ Q" and QR: "Q ∼⋅ R" let ?bisim = "bisimilar OO bisimilar" have "symp ?bisim" proof (rule sympI) fix P R assume "?bisim P R" then obtain Q where "P ∼⋅ Q" and "Q ∼⋅ R" by blast then have "R ∼⋅ Q" and "Q ∼⋅ P" by (metis bisimilar_symp sympE)+ then show "?bisim R P" by blast qed moreover have "∀P Q. ?bisim P Q ⟶ (∀φ. P ⊢ φ ⟶ Q ⊢ φ)" using bisimilar_is_bisimulation is_bisimulation_def by auto moreover have "∀P Q. ?bisim P Q ⟶ (∀α P'. bn α ♯* Q ⟶ P → ⟨α,P'⟩ ⟶ (∃Q'. Q → ⟨α,Q'⟩ ∧ ?bisim P' Q'))" proof (clarify) fix P R Q α P' assume PR: "P ∼⋅ R" and RQ: "R ∼⋅ Q" and fresh: "bn α ♯* Q" and trans: "P → ⟨α,P'⟩" ― ‹rename~@{term "⟨α,P'⟩"} to avoid~@{term R}, without touching~@{term Q}› obtain p where 1: "(p ∙ bn α) ♯* R" and 2: "supp (⟨α,P'⟩, Q) ♯* p" proof (rule at_set_avoiding2[of "bn α" R "(⟨α,P'⟩, Q)", THEN exE]) show "finite (bn α)" by (fact bn_finite) next show "finite (supp R)" by (fact finite_supp) next show "finite (supp (⟨α,P'⟩, Q))" by (simp add: finite_supp supp_Pair) next show "bn α ♯* (⟨α,P'⟩, Q)" by (simp add: fresh fresh_star_Pair) qed metis from 2 have 3: "supp ⟨α,P'⟩ ♯* p" and 4: "supp Q ♯* p" by (simp add: fresh_star_Un supp_Pair)+ from 3 have "⟨p ∙ α, p ∙ P'⟩ = ⟨α,P'⟩" using supp_perm_eq by fastforce then obtain pR' where 5: "R → ⟨p ∙ α, pR'⟩" and 6: "(p ∙ P') ∼⋅ pR'" using PR trans 1 by (metis (mono_tags, lifting) bisimilar_is_bisimulation bn_eqvt is_bisimulation_def) from fresh and 4 have "bn (p ∙ α) ♯* Q" by (metis bn_eqvt fresh_star_permute_iff supp_perm_eq) then obtain pQ' where 7: "Q → ⟨p ∙ α, pQ'⟩" and 8: "pR' ∼⋅ pQ'" using RQ 5 by (metis (full_types) bisimilar_is_bisimulation is_bisimulation_def) from 7 have "Q → ⟨α, -p ∙ pQ'⟩" using 4 by (metis permute_minus_cancel(2) supp_perm_eq transition_eqvt') moreover from 6 and 8 have "?bisim P' (-p ∙ pQ')" by (metis (no_types, hide_lams) bisimilar_eqvt permute_minus_cancel(2) relcompp.simps) ultimately show "∃Q'. Q → ⟨α,Q'⟩ ∧ ?bisim P' Q'" by metis qed ultimately have "is_bisimulation ?bisim" unfolding is_bisimulation_def by metis moreover have "?bisim P R" using PQ QR by blast ultimately show "P ∼⋅ R" unfolding bisimilar_def by meson qed lemma bisimilar_equivp: "equivp bisimilar" by (metis bisimilar_reflp bisimilar_symp bisimilar_transp equivp_reflp_symp_transp) lemma bisimilar_simulation_step: assumes "P ∼⋅ Q" and "bn α ♯* Q" and "P → ⟨α,P'⟩" obtains Q' where "Q → ⟨α,Q'⟩" and "P' ∼⋅ Q'" using assms by (metis (poly_guards_query) bisimilar_is_bisimulation is_bisimulation_def) end end

# Theory Formula

theory Formula imports Nominal_Bounded_Set Nominal_Wellfounded Residual begin section ‹Infinitary Formulas› subsection ‹Infinitely branching trees› text ‹First, we define a type of trees, with a constructor~@{term tConj} that maps (potentially infinite) sets of trees into trees. To avoid paradoxes (note that there is no injection from the powerset of trees into the set of trees), the cardinality of the argument set must be bounded.› datatype ('idx,'pred,'act) Tree = tConj "('idx,'pred,'act) Tree set['idx]" ― ‹potentially infinite sets of trees› | tNot "('idx,'pred,'act) Tree" | tPred 'pred | tAct 'act "('idx,'pred,'act) Tree" text ‹The (automatically generated) induction principle for trees allows us to prove that the following relation over trees is well-founded. This will be useful for termination proofs when we define functions by recursion over trees.› inductive_set Tree_wf :: "('idx,'pred,'act) Tree rel" where "t ∈ set_bset tset ⟹ (t, tConj tset) ∈ Tree_wf" | "(t, tNot t) ∈ Tree_wf" | "(t, tAct α t) ∈ Tree_wf" lemma wf_Tree_wf: "wf Tree_wf" unfolding wf_def proof (rule allI, rule impI, rule allI) fix P :: "('idx,'pred,'act) Tree ⇒ bool" and t assume "∀x. (∀y. (y, x) ∈ Tree_wf ⟶ P y) ⟶ P x" then show "P t" proof (induction t) case tConj then show ?case by (metis Tree.distinct(2) Tree.distinct(5) Tree.inject(1) Tree_wf.cases) next case tNot then show ?case by (metis Tree.distinct(1) Tree.distinct(9) Tree.inject(2) Tree_wf.cases) next case tPred then show ?case by (metis Tree.distinct(11) Tree.distinct(3) Tree.distinct(7) Tree_wf.cases) next case tAct then show ?case by (metis Tree.distinct(10) Tree.distinct(6) Tree.inject(4) Tree_wf.cases) qed qed text ‹We define a permutation operation on the type of trees.› instantiation Tree :: (type, pt, pt) pt begin primrec permute_Tree :: "perm ⇒ (_,_,_) Tree ⇒ (_,_,_) Tree" where "p ∙ (tConj tset) = tConj (map_bset (permute p) tset)" ― ‹neat trick to get around the fact that~@{term tset} is not of permutation type yet› | "p ∙ (tNot t) = tNot (p ∙ t)" | "p ∙ (tPred φ) = tPred (p ∙ φ)" | "p ∙ (tAct α t) = tAct (p ∙ α) (p ∙ t)" instance proof fix t :: "(_,_,_) Tree" show "0 ∙ t = t" proof (induction t) case tConj then show ?case by (simp, transfer) (auto simp: image_def) qed simp_all next fix p q :: perm and t :: "(_,_,_) Tree" show "(p + q) ∙ t = p ∙ q ∙ t" proof (induction t) case tConj then show ?case by (simp, transfer) (auto simp: image_def) qed simp_all qed end text ‹Now that the type of trees---and hence the type of (bounded) sets of trees---is a permutation type, we can massage the definition of~@{term "p ∙ tConj tset"} into its more usual form.› lemma permute_Tree_tConj [simp]: "p ∙ tConj tset = tConj (p ∙ tset)" by (simp add: map_bset_permute) declare permute_Tree.simps(1) [simp del] text ‹The relation~@{const Tree_wf} is equivariant.› lemma Tree_wf_eqvt_aux: assumes "(t1, t2) ∈ Tree_wf" shows "(p ∙ t1, p ∙ t2) ∈ Tree_wf" using assms proof (induction rule: Tree_wf.induct) fix t :: "('a,'b,'c) Tree" and tset :: "('a,'b,'c) Tree set['a]" assume "t ∈ set_bset tset" then show "(p ∙ t, p ∙ tConj tset) ∈ Tree_wf" by (metis Tree_wf.intros(1) mem_permute_iff permute_Tree_tConj set_bset_eqvt) next fix t :: "('a,'b,'c) Tree" show "(p ∙ t, p ∙ tNot t) ∈ Tree_wf" by (metis Tree_wf.intros(2) permute_Tree.simps(2)) next fix t :: "('a,'b,'c) Tree" and α show "(p ∙ t, p ∙ tAct α t) ∈ Tree_wf" by (metis Tree_wf.intros(3) permute_Tree.simps(4)) qed lemma Tree_wf_eqvt [eqvt, simp]: "p ∙ Tree_wf = Tree_wf" proof show "p ∙ Tree_wf ⊆ Tree_wf" by (auto simp add: permute_set_def) (rule Tree_wf_eqvt_aux) next show "Tree_wf ⊆ p ∙ Tree_wf" by (auto simp add: permute_set_def) (metis Tree_wf_eqvt_aux permute_minus_cancel(1)) qed lemma Tree_wf_eqvt': "eqvt Tree_wf" by (metis Tree_wf_eqvt eqvtI) text ‹The definition of~@{const permute} for trees gives rise to the usual notion of support. The following lemmas, one for each constructor, describe the support of trees.› lemma supp_tConj [simp]: "supp (tConj tset) = supp tset" unfolding supp_def by simp lemma supp_tNot [simp]: "supp (tNot t) = supp t" unfolding supp_def by simp lemma supp_tPred [simp]: "supp (tPred φ) = supp φ" unfolding supp_def by simp lemma supp_tAct [simp]: "supp (tAct α t) = supp α ∪ supp t" unfolding supp_def by (simp add: Collect_imp_eq Collect_neg_eq) subsection ‹Trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence› text ‹We generalize the notion of support, which considers whether a permuted element is \emph{equal} to itself, to arbitrary endorelations. This is available as @{const supp_rel} in Nominal Isabelle.› lemma supp_rel_eqvt [eqvt]: "p ∙ supp_rel R x = supp_rel (p ∙ R) (p ∙ x)" by (simp add: supp_rel_def) text ‹Usually, the definition of $\alpha$-equivalence presupposes a notion of free variables. However, the variables that are ``free'' in an infinitary conjunction are not necessarily those that are free in one of the conjuncts. For instance, consider a conjunction over \emph{all} names. Applying any permutation will yield the same conjunction, i.e., this conjunction has \emph{no} free variables. To obtain the correct notion of free variables for infinitary conjunctions, we initially defined $\alpha$-equivalence and free variables via mutual recursion. In particular, we defined the free variables of a conjunction as term @{term "fv_Tree (tConj tset) = supp_rel alpha_Tree (tConj tset)"}. We then realized that it is not necessary to define the concept of ``free variables'' at all, but the definition of $\alpha$-equivalence becomes much simpler (in particular, it is no longer mutually recursive) if we directly use the support modulo $\alpha$-equivalence.› text ‹The following lemmas and constructions are used to prove termination of our definition.› lemma supp_rel_cong [fundef_cong]: "⟦ x=x'; ⋀a b. R ((a ⇌ b) ∙ x') x' ⟷ R' ((a ⇌ b) ∙ x') x' ⟧ ⟹ supp_rel R x = supp_rel R' x'" by (simp add: supp_rel_def) lemma rel_bset_cong [fundef_cong]: "⟦ x=x'; y=y'; ⋀a b. a ∈ set_bset x' ⟹ b ∈ set_bset y' ⟹ R a b ⟷ R' a b ⟧ ⟹ rel_bset R x y ⟷ rel_bset R' x' y'" by (simp add: rel_bset_def rel_set_def) lemma alpha_set_cong [fundef_cong]: "⟦ bs=bs'; x=x'; R (p' ∙ x') y' ⟷ R' (p' ∙ x') y'; f x' = f' x'; f y' = f' y'; p=p'; cs=cs'; y=y' ⟧ ⟹ alpha_set (bs, x) R f p (cs, y) ⟷ alpha_set (bs', x') R' f' p' (cs', y')" by (simp add: alpha_set) quotient_type ('idx,'pred,'act) Tree⇩_{p}= "('idx,'pred::pt,'act::bn) Tree" / "hull_relp" by (fact hull_relp_equivp) lemma abs_Tree⇩_{p}_eq [simp]: "abs_Tree⇩_{p}(p ∙ t) = abs_Tree⇩_{p}t" by (metis hull_relp.simps Tree⇩_{p}.abs_eq_iff) lemma permute_rep_abs_Tree⇩_{p}: obtains p where "rep_Tree⇩_{p}(abs_Tree⇩_{p}t) = p ∙ t" by (metis Quotient3_Tree⇩_{p}Tree⇩_{p}.abs_eq_iff rep_abs_rsp hull_relp.simps) lift_definition Tree_wf⇩_{p}:: "('idx,'pred::pt,'act::bn) Tree⇩_{p}rel" is Tree_wf . lemma Tree_wf⇩_{p}I [simp]: assumes "(a, b) ∈ Tree_wf" shows "(abs_Tree⇩_{p}(p ∙ a), abs_Tree⇩_{p}b) ∈ Tree_wf⇩_{p}" using assms by (metis (erased, lifting) Tree⇩_{p}.abs_eq_iff Tree_wf⇩_{p}.abs_eq hull_relp.intros map_prod_simp rev_image_eqI) lemma Tree_wf⇩_{p}_trivialI [simp]: assumes "(a, b) ∈ Tree_wf" shows "(abs_Tree⇩_{p}a, abs_Tree⇩_{p}b) ∈ Tree_wf⇩_{p}" using assms by (metis Tree_wf⇩_{p}I permute_zero) lemma Tree_wf⇩_{p}E: assumes "(a⇩_{p}, b⇩_{p}) ∈ Tree_wf⇩_{p}" obtains a b where "a⇩_{p}= abs_Tree⇩_{p}a" and "b⇩_{p}= abs_Tree⇩_{p}b" and "(a,b) ∈ Tree_wf" using assms by (metis Pair_inject Tree_wf⇩_{p}.abs_eq prod_fun_imageE) lemma wf_Tree_wf⇩_{p}: "wf Tree_wf⇩_{p}" proof (rule wf_subset[of "inv_image (hull_rel O Tree_wf) rep_Tree⇩_{p}"]) show "wf (inv_image (hull_rel O Tree_wf) rep_Tree⇩_{p})" by (metis Tree_wf_eqvt' wf_Tree_wf wf_hull_rel_relcomp wf_inv_image) next show "Tree_wf⇩_{p}⊆ inv_image (hull_rel O Tree_wf) rep_Tree⇩_{p}" proof (standard, case_tac "x", clarify) fix a⇩_{p}b⇩_{p}:: "('d, 'e, 'f) Tree⇩_{p}" assume "(a⇩_{p}, b⇩_{p}) ∈ Tree_wf⇩_{p}" then obtain a b where 1: "a⇩_{p}= abs_Tree⇩_{p}a" and 2: "b⇩_{p}= abs_Tree⇩_{p}b" and 3: "(a,b) ∈ Tree_wf" by (rule Tree_wf⇩_{p}E) from 1 obtain p where 4: "rep_Tree⇩_{p}a⇩_{p}= p ∙ a" by (metis permute_rep_abs_Tree⇩_{p}) from 2 obtain q where 5: "rep_Tree⇩_{p}b⇩_{p}= q ∙ b" by (metis permute_rep_abs_Tree⇩_{p}) have "(p ∙ a, q ∙ a) ∈ hull_rel" by (metis hull_rel.simps permute_minus_cancel(2) permute_plus) moreover from 3 have "(q ∙ a, q ∙ b) ∈ Tree_wf" by (rule Tree_wf_eqvt_aux) ultimately show "(a⇩_{p}, b⇩_{p}) ∈ inv_image (hull_rel O Tree_wf) rep_Tree⇩_{p}" using 4 5 by auto qed qed fun alpha_Tree_termination :: "('a, 'b, 'c) Tree × ('a, 'b, 'c) Tree ⇒ ('a, 'b::pt, 'c::bn) Tree⇩_{p}set" where "alpha_Tree_termination (t1, t2) = {abs_Tree⇩_{p}t1, abs_Tree⇩_{p}t2}" text ‹Here it comes \ldots› function (sequential) alpha_Tree :: "('idx,'pred::pt,'act::bn) Tree ⇒ ('idx,'pred,'act) Tree ⇒ bool" (infix "=⇩_{α}" 50) where ― ‹@{const alpha_Tree}› alpha_tConj: "tConj tset1 =⇩_{α}tConj tset2 ⟷ rel_bset alpha_Tree tset1 tset2" | alpha_tNot: "tNot t1 =⇩_{α}tNot t2 ⟷ t1 =⇩_{α}t2" | alpha_tPred: "tPred φ1 =⇩_{α}tPred φ2 ⟷ φ1 = φ2" ― ‹the action may have binding names› | alpha_tAct: "tAct α1 t1 =⇩_{α}tAct α2 t2 ⟷ (∃p. (bn α1, t1) ≈set alpha_Tree (supp_rel alpha_Tree) p (bn α2, t2) ∧ (bn α1, α1) ≈set ((=)) supp p (bn α2, α2))" | alpha_other: "_ =⇩_{α}_ ⟷ False" ― ‹254 subgoals (!)› by pat_completeness auto termination proof let ?R = "inv_image (max_ext Tree_wf⇩_{p}) alpha_Tree_termination" show "wf ?R" by (metis max_ext_wf wf_Tree_wf⇩_{p}wf_inv_image) qed (auto simp add: max_ext.simps Tree_wf.simps simp del: permute_Tree_tConj) text ‹We provide more descriptive case names for the automatically generated induction principle.› lemmas alpha_Tree_induct' = alpha_Tree.induct[case_names alpha_tConj alpha_tNot alpha_tPred alpha_tAct "alpha_other(1)" "alpha_other(2)" "alpha_other(3)" "alpha_other(4)" "alpha_other(5)" "alpha_other(6)" "alpha_other(7)" "alpha_other(8)" "alpha_other(9)" "alpha_other(10)" "alpha_other(11)" "alpha_other(12)" "alpha_other(13)" "alpha_other(14)" "alpha_other(15)" "alpha_other(16)" "alpha_other(17)" "alpha_other(18)"] lemma alpha_Tree_induct[case_names tConj tNot tPred tAct, consumes 1]: assumes "t1 =⇩_{α}t2" and "⋀tset1 tset2. (⋀a b. a ∈ set_bset tset1 ⟹ b ∈ set_bset tset2 ⟹ a =⇩_{α}b ⟹ P a b) ⟹ rel_bset (=⇩_{α}) tset1 tset2 ⟹ P (tConj tset1) (tConj tset2)" and "⋀t1 t2. t1 =⇩_{α}t2 ⟹ P t1 t2 ⟹ P (tNot t1) (tNot t2)" and "⋀φ. P (tPred φ) (tPred φ)" and "⋀α1 t1 α2 t2. (⋀p. p ∙ t1 =⇩_{α}t2 ⟹ P (p ∙ t1) t2) ⟹ (⋀a b. ((a ⇌ b) ∙ t1) =⇩_{α}t1 ⟹ P ((a ⇌ b) ∙ t1) t1) ⟹ (⋀a b. ((a ⇌ b) ∙ t2) =⇩_{α}t2 ⟹ P ((a ⇌ b) ∙ t2) t2) ⟹ (∃p. (bn α1, t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) p (bn α2, t2) ∧ (bn α1, α1) ≈set (=) supp p (bn α2, α2)) ⟹ P (tAct α1 t1) (tAct α2 t2)" shows "P t1 t2" using assms by (induction t1 t2 rule: alpha_Tree.induct) simp_all text ‹$\alpha$-equivalence is equivariant.› lemma alpha_Tree_eqvt_aux: assumes "⋀a b. (a ⇌ b) ∙ t =⇩_{α}t ⟷ p ∙ (a ⇌ b) ∙ t =⇩_{α}p ∙ t" shows "p ∙ supp_rel (=⇩_{α}) t = supp_rel (=⇩_{α}) (p ∙ t)" proof - { fix a let ?B = "{b. ¬ ((a ⇌ b) ∙ t) =⇩_{α}t}" let ?pB = "{b. ¬ ((p ∙ a ⇌ b) ∙ p ∙ t) =⇩_{α}(p ∙ t)}" { assume "finite ?B" moreover have "inj_on (unpermute p) ?pB" by (simp add: inj_on_def unpermute_def) moreover have "unpermute p ` ?pB ⊆ ?B" using assms by auto (metis (erased, lifting) eqvt_bound permute_eqvt swap_eqvt) ultimately have "finite ?pB" by (metis inj_on_finite) } moreover { assume "finite ?pB" moreover have "inj_on (permute p) ?B" by (simp add: inj_on_def) moreover have "permute p ` ?B ⊆ ?pB" using assms by auto (metis (erased, lifting) permute_eqvt swap_eqvt) ultimately have "finite ?B" by (metis inj_on_finite) } ultimately have "infinite ?B ⟷ infinite ?pB" by auto } then show ?thesis by (auto simp add: supp_rel_def permute_set_def) (metis eqvt_bound) qed lemma alpha_Tree_eqvt': "t1 =⇩_{α}t2 ⟷ p ∙ t1 =⇩_{α}p ∙ t2" proof (induction t1 t2 rule: alpha_Tree_induct') case (alpha_tConj tset1 tset2) show ?case proof assume *: "tConj tset1 =⇩_{α}tConj tset2" { fix x assume "x ∈ set_bset (p ∙ tset1)" then obtain x' where 1: "x' ∈ set_bset tset1" and 2: "x = p ∙ x'" by (metis imageE permute_bset.rep_eq permute_set_eq_image) from 1 obtain y' where 3: "y' ∈ set_bset tset2" and 4: "x' =⇩_{α}y'" using "*" by (metis (mono_tags, lifting) Formula.alpha_tConj rel_bset.rep_eq rel_set_def) from 3 have "p ∙ y' ∈ set_bset (p ∙ tset2)" by (metis mem_permute_iff set_bset_eqvt) moreover from 1 and 2 and 3 and 4 have "x =⇩_{α}p ∙ y'" using alpha_tConj.IH by blast ultimately have "∃y∈set_bset (p ∙ tset2). x =⇩_{α}y" .. } moreover { fix y assume "y ∈ set_bset (p ∙ tset2)" then obtain y' where 1: "y' ∈ set_bset tset2" and 2: "p ∙ y' = y" by (metis imageE permute_bset.rep_eq permute_set_eq_image) from 1 obtain x' where 3: "x' ∈ set_bset tset1" and 4: "x' =⇩_{α}y'" using "*" by (metis (mono_tags, lifting) Formula.alpha_tConj rel_bset.rep_eq rel_set_def) from 3 have "p ∙ x' ∈ set_bset (p ∙ tset1)" by (metis mem_permute_iff set_bset_eqvt) moreover from 1 and 2 and 3 and 4 have "p ∙ x' =⇩_{α}y" using alpha_tConj.IH by blast ultimately have "∃x∈set_bset (p ∙ tset1). x =⇩_{α}y" .. } ultimately show "p ∙ tConj tset1 =⇩_{α}p ∙ tConj tset2" by (simp add: rel_bset_def rel_set_def) next assume *: "p ∙ tConj tset1 =⇩_{α}p ∙ tConj tset2" { fix x assume 1: "x ∈ set_bset tset1" then have "p ∙ x ∈ set_bset (p ∙ tset1)" by (metis mem_permute_iff set_bset_eqvt) then obtain y' where 2: "y' ∈ set_bset (p ∙ tset2)" and 3: "p ∙ x =⇩_{α}y'" using "*" by (metis Formula.alpha_tConj permute_Tree_tConj rel_bset.rep_eq rel_set_def) from 2 obtain y where 4: "y ∈ set_bset tset2" and 5: "y' = p ∙ y" by (metis imageE permute_bset.rep_eq permute_set_eq_image) from 1 and 3 and 4 and 5 have "x =⇩_{α}y" using alpha_tConj.IH by blast with 4 have "∃y∈set_bset tset2. x =⇩_{α}y" .. } moreover { fix y assume 1: "y ∈ set_bset tset2" then have "p ∙ y ∈ set_bset (p ∙ tset2)" by (metis mem_permute_iff set_bset_eqvt) then obtain x' where 2: "x' ∈ set_bset (p ∙ tset1)" and 3: "x' =⇩_{α}p ∙ y" using "*" by (metis Formula.alpha_tConj permute_Tree_tConj rel_bset.rep_eq rel_set_def) from 2 obtain x where 4: "x ∈ set_bset tset1" and 5: "p ∙ x = x'" by (metis imageE permute_bset.rep_eq permute_set_eq_image) from 1 and 3 and 4 and 5 have "x =⇩_{α}y" using alpha_tConj.IH by blast with 4 have "∃x∈set_bset tset1. x =⇩_{α}y" .. } ultimately show "tConj tset1 =⇩_{α}tConj tset2" by (simp add: rel_bset_def rel_set_def) qed next case (alpha_tAct α1 t1 α2 t2) from alpha_tAct.IH(2) have t1: "p ∙ supp_rel (=⇩_{α}) t1 = supp_rel (=⇩_{α}) (p ∙ t1)" by (rule alpha_Tree_eqvt_aux) from alpha_tAct.IH(3) have t2: "p ∙ supp_rel (=⇩_{α}) t2 = supp_rel (=⇩_{α}) (p ∙ t2)" by (rule alpha_Tree_eqvt_aux) show ?case proof assume "tAct α1 t1 =⇩_{α}tAct α2 t2" then obtain q where 1: "(bn α1, t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) q (bn α2, t2)" and 2: "(bn α1, α1) ≈set (=) supp q (bn α2, α2)" by auto from 1 and t1 and t2 have "supp_rel (=⇩_{α}) (p ∙ t1) - bn (p ∙ α1) = supp_rel (=⇩_{α}) (p ∙ t2) - bn (p ∙ α2)" by (metis Diff_eqvt alpha_set bn_eqvt) moreover from 1 and t1 have "(supp_rel (=⇩_{α}) (p ∙ t1) - bn (p ∙ α1)) ♯* (p + q - p)" by (metis Diff_eqvt alpha_set bn_eqvt fresh_star_permute_iff permute_perm_def) moreover from 1 and alpha_tAct.IH(1) have "p ∙ q ∙ t1 =⇩_{α}p ∙ t2" by (simp add: alpha_set) moreover from 2 have "p ∙ q ∙ -p ∙ bn (p ∙ α1) = bn (p ∙ α2)" by (simp add: alpha_set bn_eqvt) ultimately have "(bn (p ∙ α1), p ∙ t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) (p + q - p) (bn (p ∙ α2), p ∙ t2)" by (simp add: alpha_set) moreover from 2 have "(bn (p ∙ α1), p ∙ α1) ≈set (=) supp (p + q - p) (bn (p ∙ α2), p ∙ α2)" by (simp add: alpha_set) (metis (mono_tags, lifting) Diff_eqvt bn_eqvt fresh_star_permute_iff permute_minus_cancel(2) permute_perm_def supp_eqvt) ultimately show "p ∙ tAct α1 t1 =⇩_{α}p ∙ tAct α2 t2" by auto next assume "p ∙ tAct α1 t1 =⇩_{α}p ∙ tAct α2 t2" then obtain q where 1: "(bn (p ∙ α1), p ∙ t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) q (bn (p ∙ α2), p ∙ t2)" and 2: "(bn (p ∙ α1), p ∙ α1) ≈set (=) supp q (bn (p ∙ α2), p ∙ α2)" by auto { from 1 and t1 and t2 have "supp_rel (=⇩_{α}) t1 - bn α1 = supp_rel (=⇩_{α}) t2 - bn α2" by (metis (no_types, lifting) Diff_eqvt alpha_set bn_eqvt permute_eq_iff) moreover with 1 and t2 have "(supp_rel (=⇩_{α}) t1 - bn α1) ♯* (- p + q + p)" by (auto simp add: fresh_star_def fresh_perm alphas) (metis (no_types, lifting) DiffI bn_eqvt mem_permute_iff permute_minus_cancel(2)) moreover from 1 have "- p ∙ q ∙ p ∙ t1 =⇩_{α}t2" using alpha_tAct.IH(1) by (simp add: alpha_set) (metis (no_types, lifting) permute_eqvt permute_minus_cancel(2)) moreover from 1 have "- p ∙ q ∙ p ∙ bn α1 = bn α2" by (metis alpha_set bn_eqvt permute_minus_cancel(2)) ultimately have "(bn α1, t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) (-p + q + p) (bn α2, t2)" by (simp add: alpha_set) } moreover { from 2 have "supp α1 - bn α1 = supp α2 - bn α2" by (metis (no_types, lifting) Diff_eqvt alpha_set bn_eqvt permute_eq_iff supp_eqvt) moreover with 2 have "(supp α1 - bn α1) ♯* (-p + q + p)" by (auto simp add: fresh_star_def fresh_perm alphas) (metis (no_types, lifting) DiffI bn_eqvt mem_permute_iff permute_minus_cancel(1) supp_eqvt) moreover from 2 have "-p ∙ q ∙ p ∙ α1 = α2" by (simp add: alpha_set) moreover have "-p ∙ q ∙ p ∙ bn α1 = bn α2" by (simp add: bn_eqvt calculation(3)) ultimately have "(bn α1, α1) ≈set (=) supp (-p + q + p) (bn α2, α2)" by (simp add: alpha_set) } ultimately show "tAct α1 t1 =⇩_{α}tAct α2 t2" by auto qed qed simp_all lemma alpha_Tree_eqvt [eqvt]: "t1 =⇩_{α}t2 ⟹ p ∙ t1 =⇩_{α}p ∙ t2" by (metis alpha_Tree_eqvt') text ‹@{const alpha_Tree} is an equivalence relation.› lemma alpha_Tree_reflp: "reflp alpha_Tree" proof (rule reflpI) fix t :: "('a,'b,'c) Tree" show "t =⇩_{α}t" proof (induction t) case tConj then show ?case by (metis alpha_tConj rel_bset.rep_eq rel_setI) next case tNot then show ?case by (metis alpha_tNot) next case tPred show ?case by (metis alpha_tPred) next case tAct then show ?case by (metis (mono_tags) alpha_tAct alpha_refl(1)) qed qed lemma alpha_Tree_symp: "symp alpha_Tree" proof (rule sympI) fix x y :: "('a,'b,'c) Tree" assume "x =⇩_{α}y" then show "y =⇩_{α}x" proof (induction x y rule: alpha_Tree_induct) case tConj then show ?case by (simp add: rel_bset_def rel_set_def) metis next case (tAct α1 t1 α2 t2) then obtain p where "(bn α1, t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) p (bn α2, t2) ∧ (bn α1, α1) ≈set (=) supp p (bn α2, α2)" by auto then have "(bn α2, t2) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) (-p) (bn α1, t1) ∧ (bn α2, α2) ≈set (=) supp (-p) (bn α1, α1)" using tAct.IH by (metis (mono_tags, lifting) alpha_Tree_eqvt alpha_sym(1) permute_minus_cancel(2)) then show ?case by auto qed simp_all qed lemma alpha_Tree_transp: "transp alpha_Tree" proof (rule transpI) fix x y z:: "('a,'b,'c) Tree" assume "x =⇩_{α}y" and "y =⇩_{α}z" then show "x =⇩_{α}z" proof (induction x y arbitrary: z rule: alpha_Tree_induct) case (tConj tset_x tset_y) show ?case proof (cases z) fix tset_z assume z: "z = tConj tset_z" have "rel_bset (=⇩_{α}) tset_x tset_z" unfolding rel_bset.rep_eq rel_set_def Ball_def Bex_def proof show "∀x'. x' ∈ set_bset tset_x ⟶ (∃z'. z' ∈ set_bset tset_z ∧ x' =⇩_{α}z')" proof (rule allI, rule impI) fix x' assume 1: "x' ∈ set_bset tset_x" then obtain y' where 2: "y' ∈ set_bset tset_y" and 3: "x' =⇩_{α}y'" by (metis rel_bset.rep_eq rel_set_def tConj.hyps) from 2 obtain z' where 4: "z' ∈ set_bset tset_z" and 5: "y' =⇩_{α}z'" by (metis alpha_tConj rel_bset.rep_eq rel_set_def tConj.prems z) from 1 2 3 5 have "x' =⇩_{α}z'" by (rule tConj.IH) with 4 show "∃z'. z' ∈ set_bset tset_z ∧ x' =⇩_{α}z'" by auto qed next show "∀z'. z' ∈ set_bset tset_z ⟶ (∃x'. x' ∈ set_bset tset_x ∧ x' =⇩_{α}z')" proof (rule allI, rule impI) fix z' assume 1: "z' ∈ set_bset tset_z" then obtain y' where 2: "y' ∈ set_bset tset_y" and 3: "y' =⇩_{α}z'" by (metis alpha_tConj rel_bset.rep_eq rel_set_def tConj.prems z) from 2 obtain x' where 4: "x' ∈ set_bset tset_x" and 5: "x' =⇩_{α}y'" by (metis rel_bset.rep_eq rel_set_def tConj.hyps) from 4 2 5 3 have "x' =⇩_{α}z'" by (rule tConj.IH) with 4 show "∃x'. x' ∈ set_bset tset_x ∧ x' =⇩_{α}z'" by auto qed qed with z show "tConj tset_x =⇩_{α}z" by simp qed (insert tConj.prems, auto) next case tNot then show ?case by (cases z) simp_all next case tPred then show ?case by simp next case (tAct α1 t1 α2 t2) show ?case proof (cases z) fix α t assume z: "z = tAct α t" obtain p where 1: "(bn α1, t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) p (bn α2, t2) ∧ (bn α1, α1) ≈set (=) supp p (bn α2, α2)" using tAct.hyps by auto obtain q where 2: "(bn α2, t2) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) q (bn α, t) ∧ (bn α2, α2) ≈set (=) supp q (bn α, α)" using tAct.prems z by auto have "(bn α1, t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) (q + p) (bn α, t)" proof - have "supp_rel (=⇩_{α}) t1 - bn α1 = supp_rel (=⇩_{α}) t - bn α" using 1 and 2 by (metis alpha_set) moreover have "(supp_rel (=⇩_{α}) t1 - bn α1) ♯* (q + p)" using 1 and 2 by (metis alpha_set fresh_star_plus) moreover have "(q + p) ∙ t1 =⇩_{α}t" using 1 and 2 and tAct.IH by (metis (no_types, lifting) alpha_Tree_eqvt alpha_set permute_minus_cancel(1) permute_plus) moreover have "(q + p) ∙ bn α1 = bn α" using 1 and 2 by (metis alpha_set permute_plus) ultimately show ?thesis by (metis alpha_set) qed moreover have "(bn α1, α1) ≈set (=) supp (q + p) (bn α, α)" using 1 and 2 by (metis (mono_tags) alpha_trans(1) permute_plus) ultimately show "tAct α1 t1 =⇩_{α}z" using z by auto qed (insert tAct.prems, auto) qed qed lemma alpha_Tree_equivp: "equivp alpha_Tree" by (auto intro: equivpI alpha_Tree_reflp alpha_Tree_symp alpha_Tree_transp) text ‹$alpha$-equivalent trees have the same support modulo $alpha$-equivalence.› lemma alpha_Tree_supp_rel: assumes "t1 =⇩_{α}t2" shows "supp_rel (=⇩_{α}) t1 = supp_rel (=⇩_{α}) t2" using assms proof (induction rule: alpha_Tree_induct) case (tConj tset1 tset2) have sym: "⋀x y. rel_bset (=⇩_{α}) x y ⟷ rel_bset (=⇩_{α}) y x" by (meson alpha_Tree_symp bset.rel_symp sympE) { fix a b from tConj.hyps have *: "rel_bset (=⇩_{α}) ((a ⇌ b) ∙ tset1) ((a ⇌ b) ∙ tset2)" by (metis alpha_tConj alpha_Tree_eqvt permute_Tree_tConj) have "rel_bset (=⇩_{α}) ((a ⇌ b) ∙ tset1) tset1 ⟷ rel_bset (=⇩_{α}) ((a ⇌ b) ∙ tset2) tset2" by (rule iffI) (metis "*" alpha_Tree_transp bset.rel_transp sym tConj.hyps transpE)+ } then show ?case by (simp add: supp_rel_def) next case tNot then show ?case by (simp add: supp_rel_def) next case (tAct α1 t1 α2 t2) { fix a b have "tAct α1 t1 =⇩_{α}tAct α2 t2" using tAct.hyps by simp then have "(a ⇌ b) ∙ tAct α1 t1 =⇩_{α}tAct α1 t1 ⟷ (a ⇌ b) ∙ tAct α2 t2 =⇩_{α}tAct α2 t2" by (metis (no_types, lifting) alpha_Tree_eqvt alpha_Tree_symp alpha_Tree_transp sympE transpE) } then show ?case by (simp add: supp_rel_def) qed simp_all text ‹@{const tAct} preserves $\alpha$-equivalence.› lemma alpha_Tree_tAct: assumes "t1 =⇩_{α}t2" shows "tAct α t1 =⇩_{α}tAct α t2" proof - have "(bn α, t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) 0 (bn α, t2)" using assms by (simp add: alpha_Tree_supp_rel alpha_set fresh_star_zero) moreover have "(bn α, α) ≈set (=) supp 0 (bn α, α)" by (metis (full_types) alpha_refl(1)) ultimately show ?thesis by auto qed text ‹The following lemmas describe the support modulo $alpha$-equivalence.› lemma supp_rel_tNot [simp]: "supp_rel (=⇩_{α}) (tNot t) = supp_rel (=⇩_{α}) t" unfolding supp_rel_def by simp lemma supp_rel_tPred [simp]: "supp_rel (=⇩_{α}) (tPred φ) = supp φ" unfolding supp_rel_def supp_def by simp text ‹The support modulo $\alpha$-equivalence of~@{term "tAct α t"} is not easily described: when~@{term t} has infinite support (modulo $\alpha$-equivalence), the support (modulo $\alpha$-equivalence) of~@{term "tAct α t"} may still contain names in~@{term "bn α"}. This incongruity is avoided when~@{term t} has finite support modulo $\alpha$-equivalence.› lemma infinite_mono: "infinite S ⟹ (⋀x. x ∈ S ⟹ x ∈ T) ⟹ infinite T" by (metis infinite_super subsetI) lemma supp_rel_tAct [simp]: assumes "finite (supp_rel (=⇩_{α}) t)" shows "supp_rel (=⇩_{α}) (tAct α t) = supp α ∪ supp_rel (=⇩_{α}) t - bn α" proof show "supp α ∪ supp_rel (=⇩_{α}) t - bn α ⊆ supp_rel (=⇩_{α}) (tAct α t)" proof fix x assume "x ∈ supp α ∪ supp_rel (=⇩_{α}) t - bn α" moreover { assume x1: "x ∈ supp α" and x2: "x ∉ bn α" from x1 have "infinite {b. (x ⇌ b) ∙ α ≠ α}" unfolding supp_def .. then have "infinite ({b. (x ⇌ b) ∙ α ≠ α} - supp α)" by (simp add: finite_supp) moreover { fix b assume "b ∈ {b. (x ⇌ b) ∙ α ≠ α} - supp α" then have b1: "(x ⇌ b) ∙ α ≠ α" and b2: "b ∉ supp α - bn α" by simp+ from b1 have "sort_of x = sort_of b" using swap_different_sorts by fastforce then have "(x ⇌ b) ∙ (supp α - bn α) ≠ supp α - bn α" using b2 x1 x2 by (simp add: swap_set_in) then have "b ∈ {b. ¬ (x ⇌ b) ∙ tAct α t =⇩_{α}tAct α t}" by (auto simp add: alpha_set Diff_eqvt bn_eqvt) } ultimately have "infinite {b. ¬ (x ⇌ b) ∙ tAct α t =⇩_{α}tAct α t}" by (rule infinite_mono) then have "x ∈ supp_rel (=⇩_{α}) (tAct α t)" unfolding supp_rel_def .. } moreover { assume x1: "x ∈ supp_rel (=⇩_{α}) t" and x2: "x ∉ bn α" from x1 have "infinite {b. ¬ (x ⇌ b) ∙ t =⇩_{α}t}" unfolding supp_rel_def .. then have "infinite ({b. ¬ (x ⇌ b) ∙ t =⇩_{α}t} - supp_rel (=⇩_{α}) t)" using assms by simp moreover { fix b assume "b ∈ {b. ¬ (x ⇌ b) ∙ t =⇩_{α}t} - supp_rel (=⇩_{α}) t" then have b1: "¬ (x ⇌ b) ∙ t =⇩_{α}t" and b2: "b ∉ supp_rel (=⇩_{α}) t - bn α" by simp+ from b1 have "(x ⇌ b) ∙ t ≠ t" by (metis alpha_Tree_reflp reflpE) then have "sort_of x = sort_of b" using swap_different_sorts by fastforce then have "(x ⇌ b) ∙ (supp_rel (=⇩_{α}) t - bn α) ≠ supp_rel (=⇩_{α}) t - bn α" using b2 x1 x2 by (simp add: swap_set_in) then have "supp_rel (=⇩_{α}) ((x ⇌ b) ∙ t) - bn ((x ⇌ b) ∙ α) ≠ supp_rel (=⇩_{α}) t - bn α" by (simp add: Diff_eqvt bn_eqvt) then have "b ∈ {b. ¬ (x ⇌ b) ∙ tAct α t =⇩_{α}tAct α t}" by (simp add: alpha_set) } ultimately have "infinite {b. ¬ (x ⇌ b) ∙ tAct α t =⇩_{α}tAct α t}" by (rule infinite_mono) then have "x ∈ supp_rel (=⇩_{α}) (tAct α t)" unfolding supp_rel_def .. } ultimately show "x ∈ supp_rel (=⇩_{α}) (tAct α t)" by auto qed next show "supp_rel (=⇩_{α}) (tAct α t) ⊆ supp α ∪ supp_rel (=⇩_{α}) t - bn α" proof fix x assume "x ∈ supp_rel (=⇩_{α}) (tAct α t)" then have *: "infinite {b. ¬ (x ⇌ b) ∙ tAct α t =⇩_{α}tAct α t}" unfolding supp_rel_def .. moreover { fix b assume "¬ (x ⇌ b) ∙ tAct α t =⇩_{α}tAct α t" then have "(x ⇌ b) ∙ α ≠ α ∨ ¬ (x ⇌ b) ∙ t =⇩_{α}t" using alpha_Tree_tAct by force } ultimately have "infinite {b. (x ⇌ b) ∙ α ≠ α ∨ ¬ (x ⇌ b) ∙ t =⇩_{α}t}" by (metis (mono_tags, lifting) infinite_mono mem_Collect_eq) then have "infinite {b. (x ⇌ b) ∙ α ≠ α} ∨ infinite {b. ¬ (x ⇌ b) ∙ t =⇩_{α}t}" by (metis (mono_tags) finite_Collect_disjI) then have "x ∈ supp α ∪ supp_rel (=⇩_{α}) t" by (simp add: supp_def supp_rel_def) moreover { assume **: "x ∈ bn α" from "*" obtain b where b1: "¬ (x ⇌ b) ∙ tAct α t =⇩_{α}tAct α t" and b2: "b ∉ supp α" and b3: "b ∉ supp_rel (=⇩_{α}) t" using assms by (metis (no_types, lifting) UnCI finite_UnI finite_supp infinite_mono mem_Collect_eq) let ?p = "(x ⇌ b)" have "supp_rel (=⇩_{α}) ((x ⇌ b) ∙ t) - bn ((x ⇌ b) ∙ α) = supp_rel (=⇩_{α}) t - bn α" using "**" and b3 by (metis (no_types, lifting) Diff_eqvt Diff_iff alpha_Tree_eqvt' alpha_Tree_eqvt_aux bn_eqvt swap_set_not_in) moreover then have "(supp_rel (=⇩_{α}) ((x ⇌ b) ∙ t) - bn ((x ⇌ b) ∙ α)) ♯* ?p" using "**" and b3 by (metis Diff_iff fresh_perm fresh_star_def swap_atom_simps(3)) moreover have "?p ∙ (x ⇌ b) ∙ t =⇩_{α}t" using alpha_Tree_reflp reflpE by force moreover have "?p ∙ bn ((x ⇌ b) ∙ α) = bn α" by (simp add: bn_eqvt) moreover have "supp ((x ⇌ b) ∙ α) - bn ((x ⇌ b) ∙ α) = supp α - bn α" using "**" and b2 by (metis (mono_tags, hide_lams) Diff_eqvt Diff_iff bn_eqvt supp_eqvt swap_set_not_in) moreover then have "(supp ((x ⇌ b) ∙ α) - bn ((x ⇌ b) ∙ α)) ♯* ?p" using "**" and b2 by (simp add: fresh_star_def fresh_def supp_perm) (metis Diff_iff swap_atom_simps(3)) moreover have "?p ∙ (x ⇌ b) ∙ α = α" by simp ultimately have "(x ⇌ b) ∙ tAct α t =⇩_{α}tAct α t" by (auto simp add: alpha_set) with b1 have "False" .. } ultimately show "x ∈ supp α ∪ supp_rel (=⇩_{α}) t - bn α" by blast qed qed text ‹We define the type of (infinitely branching) trees quotiented by $\alpha$-equivalence.› (* FIXME: No map function defined. No relator found. *) quotient_type ('idx,'pred,'act) Tree⇩_{α}= "('idx,'pred::pt,'act::bn) Tree" / "alpha_Tree" by (fact alpha_Tree_equivp) lemma Tree⇩_{α}_abs_rep [simp]: "abs_Tree⇩_{α}(rep_Tree⇩_{α}t⇩_{α}) = t⇩_{α}" by (metis Quotient_Tree⇩_{α}Quotient_abs_rep) lemma Tree⇩_{α}_rep_abs [simp]: "rep_Tree⇩_{α}(abs_Tree⇩_{α}t) =⇩_{α}t" by (metis Tree⇩_{α}.abs_eq_iff Tree⇩_{α}_abs_rep) text ‹The permutation operation is lifted from trees.› instantiation Tree⇩_{α}:: (type, pt, bn) pt begin lift_definition permute_Tree⇩_{α}:: "perm ⇒ ('a,'b,'c) Tree⇩_{α}⇒ ('a,'b,'c) Tree⇩_{α}" is permute by (fact alpha_Tree_eqvt) instance proof fix t⇩_{α}:: "(_,_,_) Tree⇩_{α}" show "0 ∙ t⇩_{α}= t⇩_{α}" by transfer (metis alpha_Tree_equivp equivp_reflp permute_zero) next fix p q :: perm and t⇩_{α}:: "(_,_,_) Tree⇩_{α}" show "(p + q) ∙ t⇩_{α}= p ∙ q ∙ t⇩_{α}" by transfer (metis alpha_Tree_equivp equivp_reflp permute_plus) qed end text ‹The abstraction function from trees to trees modulo $\alpha$-equivalence is equivariant. The representation function is equivariant modulo $\alpha$-equivalence.› lemmas permute_Tree⇩_{α}.abs_eq [eqvt, simp] lemma alpha_Tree_permute_rep_commute [simp]: "p ∙ rep_Tree⇩_{α}t⇩_{α}=⇩_{α}rep_Tree⇩_{α}(p ∙ t⇩_{α})" by (metis Tree⇩_{α}.abs_eq_iff Tree⇩_{α}_abs_rep permute_Tree⇩_{α}.abs_eq) subsection ‹Constructors for trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence› text ‹The constructors are lifted from trees.› lift_definition Conj⇩_{α}:: "('idx,'pred,'act) Tree⇩_{α}set['idx] ⇒ ('idx,'pred::pt,'act::bn) Tree⇩_{α}" is tConj by simp lemma map_bset_abs_rep_Tree⇩_{α}: "map_bset abs_Tree⇩_{α}(map_bset rep_Tree⇩_{α}tset⇩_{α}) = tset⇩_{α}" by (metis (full_types) Quotient_Tree⇩_{α}Quotient_abs_rep bset_lifting.bset_quot_map) lemma Conj⇩_{α}_def': "Conj⇩_{α}tset⇩_{α}= abs_Tree⇩_{α}(tConj (map_bset rep_Tree⇩_{α}tset⇩_{α}))" by (metis Conj⇩_{α}.abs_eq map_bset_abs_rep_Tree⇩_{α}) lift_definition Not⇩_{α}:: "('idx,'pred,'act) Tree⇩_{α}⇒ ('idx,'pred::pt,'act::bn) Tree⇩_{α}" is tNot by simp lift_definition Pred⇩_{α}:: "'pred ⇒ ('idx,'pred::pt,'act::bn) Tree⇩_{α}" is tPred . lift_definition Act⇩_{α}:: "'act ⇒ ('idx,'pred,'act) Tree⇩_{α}⇒ ('idx,'pred::pt,'act::bn) Tree⇩_{α}" is tAct by (fact alpha_Tree_tAct) text ‹The lifted constructors are equivariant.› lemma Conj⇩_{α}_eqvt [eqvt, simp]: "p ∙ Conj⇩_{α}tset⇩_{α}= Conj⇩_{α}(p ∙ tset⇩_{α})" proof - { fix x assume "x ∈ set_bset (p ∙ map_bset rep_Tree⇩_{α}tset⇩_{α})" then obtain y where "y ∈ set_bset (map_bset rep_Tree⇩_{α}tset⇩_{α})" and "x = p ∙ y" by (metis imageE permute_bset.rep_eq permute_set_eq_image) then obtain t⇩_{α}where 1: "t⇩_{α}∈ set_bset tset⇩_{α}" and 2: "x = p ∙ rep_Tree⇩_{α}t⇩_{α}" by (metis imageE map_bset.rep_eq) let ?x' = "rep_Tree⇩_{α}(p ∙ t⇩_{α})" from 1 have "p ∙ t⇩_{α}∈ set_bset (p ∙ tset⇩_{α})" by (metis mem_permute_iff permute_bset.rep_eq) then have "?x' ∈ set_bset (map_bset rep_Tree⇩_{α}(p ∙ tset⇩_{α}))" by (simp add: bset.set_map) moreover from 2 have "x =⇩_{α}?x'" by (metis alpha_Tree_permute_rep_commute) ultimately have "∃x'∈set_bset (map_bset rep_Tree⇩_{α}(p ∙ tset⇩_{α})). x =⇩_{α}x'" .. } moreover { fix y assume "y ∈ set_bset (map_bset rep_Tree⇩_{α}(p ∙ tset⇩_{α}))" then obtain x where "x ∈ set_bset (p ∙ tset⇩_{α})" and "rep_Tree⇩_{α}x = y" by (metis imageE map_bset.rep_eq) then obtain t⇩_{α}where 1: "t⇩_{α}∈ set_bset tset⇩_{α}" and 2: "rep_Tree⇩_{α}(p ∙ t⇩_{α}) = y" by (metis imageE permute_bset.rep_eq permute_set_eq_image) let ?y' = "p ∙ rep_Tree⇩_{α}t⇩_{α}" from 1 have "rep_Tree⇩_{α}t⇩_{α}∈ set_bset (map_bset rep_Tree⇩_{α}tset⇩_{α})" by (simp add: bset.set_map) then have "?y' ∈ set_bset (p ∙ map_bset rep_Tree⇩_{α}tset⇩_{α})" by (metis mem_permute_iff permute_bset.rep_eq) moreover from 2 have "?y' =⇩_{α}y" by (metis alpha_Tree_permute_rep_commute) ultimately have "∃y'∈set_bset (p ∙ map_bset rep_Tree⇩_{α}tset⇩_{α}). y' =⇩_{α}y" .. } ultimately show ?thesis by (simp add: Conj⇩_{α}_def' map_bset_eqvt rel_bset_def rel_set_def Tree⇩_{α}.abs_eq_iff) qed lemma Not⇩_{α}_eqvt [eqvt, simp]: "p ∙ Not⇩_{α}t⇩_{α}= Not⇩_{α}(p ∙ t⇩_{α})" by (induct t⇩_{α}) (simp add: Not⇩_{α}.abs_eq) lemma Pred⇩_{α}_eqvt [eqvt, simp]: "p ∙ Pred⇩_{α}φ = Pred⇩_{α}(p ∙ φ)" by (simp add: Pred⇩_{α}.abs_eq) lemma Act⇩_{α}_eqvt [eqvt, simp]: "p ∙ Act⇩_{α}α t⇩_{α}= Act⇩_{α}(p ∙ α) (p ∙ t⇩_{α})" by (induct t⇩_{α}) (simp add: Act⇩_{α}.abs_eq) text ‹The lifted constructors are injective (except for~@{const Act⇩_{α}}).› lemma Conj⇩_{α}_eq_iff [simp]: "Conj⇩_{α}tset1⇩_{α}= Conj⇩_{α}tset2⇩_{α}⟷ tset1⇩_{α}= tset2⇩_{α}" proof assume "Conj⇩_{α}tset1⇩_{α}= Conj⇩_{α}tset2⇩_{α}" then have "tConj (map_bset rep_Tree⇩_{α}tset1⇩_{α}) =⇩_{α}tConj (map_bset rep_Tree⇩_{α}tset2⇩_{α})" by (metis Conj⇩_{α}_def' Tree⇩_{α}.abs_eq_iff) then have "rel_bset (=⇩_{α}) (map_bset rep_Tree⇩_{α}tset1⇩_{α}) (map_bset rep_Tree⇩_{α}tset2⇩_{α})" by (auto elim: alpha_Tree.cases) then show "tset1⇩_{α}= tset2⇩_{α}" using Quotient_Tree⇩_{α}Quotient_rel_abs2 bset_lifting.bset_quot_map map_bset_abs_rep_Tree⇩_{α}by fastforce qed (fact arg_cong) lemma Not⇩_{α}_eq_iff [simp]: "Not⇩_{α}t1⇩_{α}= Not⇩_{α}t2⇩_{α}⟷ t1⇩_{α}= t2⇩_{α}" proof assume "Not⇩_{α}t1⇩_{α}= Not⇩_{α}t2⇩_{α}" then have "tNot (rep_Tree⇩_{α}t1⇩_{α}) =⇩_{α}tNot (rep_Tree⇩_{α}t2⇩_{α})" by (metis Not⇩_{α}.abs_eq Tree⇩_{α}.abs_eq_iff Tree⇩_{α}_abs_rep) then have "rep_Tree⇩_{α}t1⇩_{α}=⇩_{α}rep_Tree⇩_{α}t2⇩_{α}" using alpha_Tree.cases by auto then show "t1⇩_{α}= t2⇩_{α}" by (metis Tree⇩_{α}.abs_eq_iff Tree⇩_{α}_abs_rep) next assume "t1⇩_{α}= t2⇩_{α}" then show "Not⇩_{α}t1⇩_{α}= Not⇩_{α}t2⇩_{α}" by simp qed lemma Pred⇩_{α}_eq_iff [simp]: "Pred⇩_{α}φ1 = Pred⇩_{α}φ2 ⟷ φ1 = φ2" proof assume "Pred⇩_{α}φ1 = Pred⇩_{α}φ2" then have "(tPred φ1 :: ('d, 'b, 'e) Tree) =⇩_{α}tPred φ2" ― ‹note the unrelated type› by (metis Pred⇩_{α}.abs_eq Tree⇩_{α}.abs_eq_iff) then show "φ1 = φ2" using alpha_Tree.cases by auto next assume "φ1 = φ2" then show "Pred⇩_{α}φ1 = Pred⇩_{α}φ2" by simp qed lemma Act⇩_{α}_eq_iff: "Act⇩_{α}α1 t1 = Act⇩_{α}α2 t2 ⟷ tAct α1 (rep_Tree⇩_{α}t1) =⇩_{α}tAct α2 (rep_Tree⇩_{α}t2)" by (metis Act⇩_{α}.abs_eq Tree⇩_{α}.abs_eq_iff Tree⇩_{α}_abs_rep) text ‹The lifted constructors are free (except for~@{const Act⇩_{α}}).› lemma Tree⇩_{α}_free [simp]: shows "Conj⇩_{α}tset⇩_{α}≠ Not⇩_{α}t⇩_{α}" and "Conj⇩_{α}tset⇩_{α}≠ Pred⇩_{α}φ" and "Conj⇩_{α}tset⇩_{α}≠ Act⇩_{α}α t⇩_{α}" and "Not⇩_{α}t⇩_{α}≠ Pred⇩_{α}φ" and "Not⇩_{α}t1⇩_{α}≠ Act⇩_{α}α t2⇩_{α}" and "Pred⇩_{α}φ ≠ Act⇩_{α}α t⇩_{α}" by (simp add: Conj⇩_{α}_def' Not⇩_{α}_def Pred⇩_{α}_def Act⇩_{α}_def Tree⇩_{α}.abs_eq_iff)+ text ‹The following lemmas describe the support of constructed trees modulo $\alpha$-equivalence.› lemma supp_alpha_supp_rel: "supp t⇩_{α}= supp_rel (=⇩_{α}) (rep_Tree⇩_{α}t⇩_{α})" unfolding supp_def supp_rel_def by (metis (mono_tags, lifting) Collect_cong Tree⇩_{α}.abs_eq_iff Tree⇩_{α}_abs_rep alpha_Tree_permute_rep_commute) lemma supp_Conj⇩_{α}[simp]: "supp (Conj⇩_{α}tset⇩_{α}) = supp tset⇩_{α}" unfolding supp_def by simp lemma supp_Not⇩_{α}[simp]: "supp (Not⇩_{α}t⇩_{α}) = supp t⇩_{α}" unfolding supp_def by simp lemma supp_Pred⇩_{α}[simp]: "supp (Pred⇩_{α}φ) = supp φ" unfolding supp_def by simp lemma supp_Act⇩_{α}[simp]: assumes "finite (supp t⇩_{α})" shows "supp (Act⇩_{α}α t⇩_{α}) = supp α ∪ supp t⇩_{α}- bn α" using assms by (metis Act⇩_{α}.abs_eq Tree⇩_{α}_abs_rep Tree⇩_{α}_rep_abs alpha_Tree_supp_rel supp_alpha_supp_rel supp_rel_tAct) subsection ‹Induction over trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence› lemma Tree⇩_{α}_induct [case_names Conj⇩_{α}Not⇩_{α}Pred⇩_{α}Act⇩_{α}Env⇩_{α}, induct type: Tree⇩_{α}]: fixes t⇩_{α}assumes "⋀tset⇩_{α}. (⋀x. x ∈ set_bset tset⇩_{α}⟹ P x) ⟹ P (Conj⇩_{α}tset⇩_{α})" and "⋀t⇩_{α}. P t⇩_{α}⟹ P (Not⇩_{α}t⇩_{α})" and "⋀pred. P (Pred⇩_{α}pred)" and "⋀act t⇩_{α}. P t⇩_{α}⟹ P (Act⇩_{α}act t⇩_{α})" shows "P t⇩_{α}" proof (rule Tree⇩_{α}.abs_induct) fix t show "P (abs_Tree⇩_{α}t)" proof (induction t) case (tConj tset) let ?tset⇩_{α}= "map_bset abs_Tree⇩_{α}tset" have "abs_Tree⇩_{α}(tConj tset) = Conj⇩_{α}?tset⇩_{α}" by (simp add: Conj⇩_{α}.abs_eq) then show ?case using assms(1) tConj.IH by (metis imageE map_bset.rep_eq) next case tNot then show ?case using assms(2) by (metis Not⇩_{α}.abs_eq) next case tPred show ?case using assms(3) by (metis Pred⇩_{α}.abs_eq) next case tAct then show ?case using assms(4) by (metis Act⇩_{α}.abs_eq) qed qed text ‹There is no (obvious) strong induction principle for trees modulo $\alpha$-equivalence: since their support may be infinite, we may not be able to rename bound variables without also renaming free variables.› subsection ‹Hereditarily finitely supported trees› text ‹We cannot obtain the type of infinitary formulas simply as the sub-type of all trees (modulo $\alpha$-equivalence) that are finitely supported: since an infinite set of trees may be finitely supported even though its members are not (and thus, would not be formulas), the sub-type of \emph{all} finitely supported trees does not validate the induction principle that we desire for formulas. Instead, we define \emph{hereditarily} finitely supported trees. We require that environments and state predicates are finitely supported.› inductive hereditarily_fs :: "('idx,'pred::fs,'act::bn) Tree⇩_{α}⇒ bool" where Conj⇩_{α}: "finite (supp tset⇩_{α}) ⟹ (⋀t⇩_{α}. t⇩_{α}∈ set_bset tset⇩_{α}⟹ hereditarily_fs t⇩_{α}) ⟹ hereditarily_fs (Conj⇩_{α}tset⇩_{α})" | Not⇩_{α}: "hereditarily_fs t⇩_{α}⟹ hereditarily_fs (Not⇩_{α}t⇩_{α})" | Pred⇩_{α}: "hereditarily_fs (Pred⇩_{α}φ)" | Act⇩_{α}: "hereditarily_fs t⇩_{α}⟹ hereditarily_fs (Act⇩_{α}α t⇩_{α})" text ‹@{const hereditarily_fs} is equivariant.› lemma hereditarily_fs_eqvt [eqvt]: assumes "hereditarily_fs t⇩_{α}" shows "hereditarily_fs (p ∙ t⇩_{α})" using assms proof (induction rule: hereditarily_fs.induct) case Conj⇩_{α}then show ?case by (metis (erased, hide_lams) Conj⇩_{α}_eqvt hereditarily_fs.Conj⇩_{α}mem_permute_iff permute_finite permute_minus_cancel(1) set_bset_eqvt supp_eqvt) next case Not⇩_{α}then show ?case by (metis Not⇩_{α}_eqvt hereditarily_fs.Not⇩_{α}) next case Pred⇩_{α}then show ?case by (metis Pred⇩_{α}_eqvt hereditarily_fs.Pred⇩_{α}) next case Act⇩_{α}then show ?case by (metis Act⇩_{α}_eqvt hereditarily_fs.Act⇩_{α}) qed text ‹@{const hereditarily_fs} is preserved under $\alpha$-renaming.› lemma hereditarily_fs_alpha_renaming: assumes "Act⇩_{α}α t⇩_{α}= Act⇩_{α}α' t⇩_{α}'" shows "hereditarily_fs t⇩_{α}⟷ hereditarily_fs t⇩_{α}'" proof assume "hereditarily_fs t⇩_{α}" then show "hereditarily_fs t⇩_{α}'" using assms by (auto simp add: Act⇩_{α}_def Tree⇩_{α}.abs_eq_iff alphas) (metis Tree⇩_{α}.abs_eq_iff Tree⇩_{α}_abs_rep hereditarily_fs_eqvt permute_Tree⇩_{α}.abs_eq) next assume "hereditarily_fs t⇩_{α}'" then show "hereditarily_fs t⇩_{α}" using assms by (auto simp add: Act⇩_{α}_def Tree⇩_{α}.abs_eq_iff alphas) (metis Tree⇩_{α}.abs_eq_iff Tree⇩_{α}_abs_rep hereditarily_fs_eqvt permute_Tree⇩_{α}.abs_eq permute_minus_cancel(2)) qed text ‹Hereditarily finitely supported trees have finite support.› lemma hereditarily_fs_implies_finite_supp: assumes "hereditarily_fs t⇩_{α}" shows "finite (supp t⇩_{α})" using assms by (induction rule: hereditarily_fs.induct) (simp_all add: finite_supp) subsection ‹Infinitary formulas› text ‹Now, infinitary formulas are simply the sub-type of hereditarily finitely supported trees.› typedef ('idx,'pred::fs,'act::bn) formula = "{t⇩_{α}::('idx,'pred,'act) Tree⇩_{α}. hereditarily_fs t⇩_{α}}" by (metis hereditarily_fs.Pred⇩_{α}mem_Collect_eq) text ‹We set up Isabelle's lifting infrastructure so that we can lift definitions from the type of trees modulo $\alpha$-equivalence to the sub-type of formulas.› (* FIXME: No relator found. *) setup_lifting type_definition_formula lemma Abs_formula_inverse [simp]: assumes "hereditarily_fs t⇩_{α}" shows "Rep_formula (Abs_formula t⇩_{α}) = t⇩_{α}" using assms by (metis Abs_formula_inverse mem_Collect_eq) lemma Rep_formula' [simp]: "hereditarily_fs (Rep_formula x)" by (metis Rep_formula mem_Collect_eq) text ‹Now we lift the permutation operation.› instantiation formula :: (type, fs, bn) pt begin lift_definition permute_formula :: "perm ⇒ ('a,'b,'c) formula ⇒ ('a,'b,'c) formula" is permute by (fact hereditarily_fs_eqvt) instance by standard (transfer, simp)+ end text ‹The abstraction and representation functions for formulas are equivariant, and they preserve support.› lemma Abs_formula_eqvt [simp]: assumes "hereditarily_fs t⇩_{α}" shows "p ∙ Abs_formula t⇩_{α}= Abs_formula (p ∙ t⇩_{α})" by (metis assms eq_onp_same_args permute_formula.abs_eq) lemma supp_Abs_formula [simp]: assumes "hereditarily_fs t⇩_{α}" shows "supp (Abs_formula t⇩_{α}) = supp t⇩_{α}" proof - { fix p :: perm have "p ∙ Abs_formula t⇩_{α}= Abs_formula (p ∙ t⇩_{α})" using assms by (metis Abs_formula_eqvt) moreover have "hereditarily_fs (p ∙ t⇩_{α})" using assms by (metis hereditarily_fs_eqvt) ultimately have "p ∙ Abs_formula t⇩_{α}= Abs_formula t⇩_{α}⟷ p ∙ t⇩_{α}= t⇩_{α}" using assms by (metis Abs_formula_inverse) } then show ?thesis unfolding supp_def by simp qed lemmas Rep_formula_eqvt [eqvt, simp] = permute_formula.rep_eq[symmetric] lemma supp_Rep_formula [simp]: "supp (Rep_formula x) = supp x" by (metis Rep_formula' Rep_formula_inverse supp_Abs_formula) lemma supp_map_bset_Rep_formula [simp]: "supp (map_bset Rep_formula xset) = supp xset" proof have "eqvt (map_bset Rep_formula)" unfolding eqvt_def by (simp add: ext) then show "supp (map_bset Rep_formula xset) ⊆ supp xset" by (fact supp_fun_app_eqvt) next { fix a :: atom have "inj (map_bset Rep_formula)" by (metis bset.inj_map Rep_formula_inject injI) then have "⋀x y. x ≠ y ⟹ map_bset Rep_formula x ≠ map_bset Rep_formula y" by (metis inj_eq) then have "{b. (a ⇌ b) ∙ xset ≠ xset} ⊆ {b. (a ⇌ b) ∙ map_bset Rep_formula xset ≠ map_bset Rep_formula xset}" (is "?S ⊆ ?T") by auto then have "infinite ?S ⟹ infinite ?T" by (metis infinite_super) } then show "supp xset ⊆ supp (map_bset Rep_formula xset)" unfolding supp_def by auto qed text ‹Formulas are in fact finitely supported.› instance formula :: (type, fs, bn) fs by standard (metis Rep_formula' hereditarily_fs_implies_finite_supp supp_Rep_formula) subsection ‹Constructors for infinitary formulas› text ‹We lift the constructors for trees (modulo $\alpha$-equivalence) to infinitary formulas. Since~@{const Conj⇩_{α}} does not necessarily yield a (hereditarily) finitely supported tree when applied to a (potentially infinite) set of (hereditarily) finitely supported trees, we cannot use Isabelle's {\bf lift\_definition} to define~@{term Conj}. Instead, theorems about terms of the form~@{term "Conj xset"} will usually carry an assumption that~@{term xset} is finitely supported.› definition Conj :: "('idx,'pred,'act) formula set['idx] ⇒ ('idx,'pred::fs,'act::bn) formula" where "Conj xset = Abs_formula (Conj⇩_{α}(map_bset Rep_formula xset))" lemma finite_supp_implies_hereditarily_fs_Conj⇩_{α}[simp]: assumes "finite (supp xset)" shows "hereditarily_fs (Conj⇩_{α}(map_bset Rep_formula xset))" proof (rule hereditarily_fs.Conj⇩_{α}) show "finite (supp (map_bset Rep_formula xset))" using assms by (metis supp_map_bset_Rep_formula) next fix t⇩_{α}assume "t⇩_{α}∈ set_bset (map_bset Rep_formula xset)" then show "hereditarily_fs t⇩_{α}" by (auto simp add: bset.set_map) qed lemma Conj_rep_eq: assumes "finite (supp xset)" shows "Rep_formula (Conj xset) = Conj⇩_{α}(map_bset Rep_formula xset)" using assms unfolding Conj_def by simp lift_definition Not :: "('idx,'pred,'act) formula ⇒ ('idx,'pred::fs,'act::bn) formula" is Not⇩_{α}by (fact hereditarily_fs.Not⇩_{α}) lift_definition Pred :: "'pred ⇒ ('idx,'pred::fs,'act::bn) formula" is Pred⇩_{α}by (fact hereditarily_fs.Pred⇩_{α}) lift_definition Act :: "'act ⇒ ('idx,'pred,'act) formula ⇒ ('idx,'pred::fs,'act::bn) formula" is Act⇩_{α}by (fact hereditarily_fs.Act⇩_{α}) text ‹The lifted constructors are equivariant (in the case of~@{const Conj}, on finitely supported arguments).› lemma Conj_eqvt [simp]: assumes "finite (supp xset)" shows "p ∙ Conj xset = Conj (p ∙ xset)" using assms unfolding Conj_def by simp lemma Not_eqvt [eqvt, simp]: "p ∙ Not x = Not (p ∙ x)" by transfer simp lemma Pred_eqvt [eqvt, simp]: "p ∙ Pred φ = Pred (p ∙ φ)" by transfer simp lemma Act_eqvt [eqvt, simp]: "p ∙ Act α x = Act (p ∙ α) (p ∙ x)" by transfer simp text ‹The following lemmas describe the support of constructed formulas.› lemma supp_Conj [simp]: assumes "finite (supp xset)" shows "supp (Conj xset) = supp xset" using assms unfolding Conj_def by simp lemma supp_Not [simp]: "supp (Not x) = supp x" by (metis Not.rep_eq supp_Not⇩_{α}supp_Rep_formula) lemma supp_Pred [simp]: "supp (Pred φ) = supp φ" by (metis Pred.rep_eq supp_Pred⇩_{α}supp_Rep_formula) lemma supp_Act [simp]: "supp (Act α x) = supp α ∪ supp x - bn α" by (metis Act.rep_eq finite_supp supp_Act⇩_{α}supp_Rep_formula) lemma bn_fresh_Act [simp]: "bn α ♯* Act α x" by (simp add: fresh_def fresh_star_def) text ‹The lifted constructors are injective (except for @{const Act}).› lemma Conj_eq_iff [simp]: assumes "finite (supp xset1)" and "finite (supp xset2)" shows "Conj xset1 = Conj xset2 ⟷ xset1 = xset2" using assms by (metis (erased, hide_lams) Conj⇩_{α}_eq_iff Conj_rep_eq Rep_formula_inverse injI inj_eq bset.inj_map) lemma Not_eq_iff [simp]: "Not x1 = Not x2 ⟷ x1 = x2" by (metis Not.rep_eq Not⇩_{α}_eq_iff Rep_formula_inverse) lemma Pred_eq_iff [simp]: "Pred φ1 = Pred φ2 ⟷ φ1 = φ2" by (metis Pred.rep_eq Pred⇩_{α}_eq_iff) lemma Act_eq_iff: "Act α1 x1 = Act α2 x2 ⟷ Act⇩_{α}α1 (Rep_formula x1) = Act⇩_{α}α2 (Rep_formula x2)" by (metis Act.rep_eq Rep_formula_inverse) text ‹Helpful lemmas for dealing with equalities involving~@{const Act}.› lemma Act_eq_iff_perm: "Act α1 x1 = Act α2 x2 ⟷ (∃p. supp x1 - bn α1 = supp x2 - bn α2 ∧ (supp x1 - bn α1) ♯* p ∧ p ∙ x1 = x2 ∧ supp α1 - bn α1 = supp α2 - bn α2 ∧ (supp α1 - bn α1) ♯* p ∧ p ∙ α1 = α2)" (is "?l ⟷ ?r") proof assume "?l" then obtain p where alpha: "(bn α1, rep_Tree⇩_{α}(Rep_formula x1)) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) p (bn α2, rep_Tree⇩_{α}(Rep_formula x2))" and eq: "(bn α1, α1) ≈set (=) supp p (bn α2, α2)" by (metis Act_eq_iff Act⇩_{α}_eq_iff alpha_tAct) from alpha have "supp x1 - bn α1 = supp x2 - bn α2" by (metis alpha_set.simps supp_Rep_formula supp_alpha_supp_rel) moreover from alpha have "(supp x1 - bn α1) ♯* p" by (metis alpha_set.simps supp_Rep_formula supp_alpha_supp_rel) moreover from alpha have "p ∙ x1 = x2" by (metis Rep_formula_eqvt Rep_formula_inject Tree⇩_{α}.abs_eq_iff Tree⇩_{α}_abs_rep alpha_Tree_permute_rep_commute alpha_set.simps) moreover from eq have "supp α1 - bn α1 = supp α2 - bn α2" by (metis alpha_set.simps) moreover from eq have "(supp α1 - bn α1) ♯* p" by (metis alpha_set.simps) moreover from eq have "p ∙ α1 = α2" by (simp add: alpha_set.simps) ultimately show "?r" by metis next assume "?r" then obtain p where 1: "supp x1 - bn α1 = supp x2 - bn α2" and 2: "(supp x1 - bn α1) ♯* p" and 3: "p ∙ x1 = x2" and 4: "supp α1 - bn α1 = supp α2 - bn α2" and 5: "(supp α1 - bn α1) ♯* p" and 6: "p ∙ α1 = α2" by metis from 1 2 3 6 have "(bn α1, rep_Tree⇩_{α}(Rep_formula x1)) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) p (bn α2, rep_Tree⇩_{α}(Rep_formula x2))" by (metis (no_types, lifting) Rep_formula_eqvt alpha_Tree_permute_rep_commute alpha_set.simps bn_eqvt supp_Rep_formula supp_alpha_supp_rel) moreover from 4 5 6 have "(bn α1, α1) ≈set (=) supp p (bn α2, α2)" by (simp add: alpha_set.simps bn_eqvt) ultimately show "Act α1 x1 = Act α2 x2" by (metis Act_eq_iff Act⇩_{α}_eq_iff alpha_tAct) qed lemma Act_eq_iff_perm_renaming: "Act α1 x1 = Act α2 x2 ⟷ (∃p. supp x1 - bn α1 = supp x2 - bn α2 ∧ (supp x1 - bn α1) ♯* p ∧ p ∙ x1 = x2 ∧ supp α1 - bn α1 = supp α2 - bn α2 ∧ (supp α1 - bn α1) ♯* p ∧ p ∙ α1 = α2 ∧ supp p ⊆ bn α1 ∪ p ∙ bn α1)" (is "?l ⟷ ?r") proof assume "?l" then obtain p where p: "supp x1 - bn α1 = supp x2 - bn α2 ∧ (supp x1 - bn α1) ♯* p ∧ p ∙ x1 = x2 ∧ supp α1 - bn α1 = supp α2 - bn α2 ∧ (supp α1 - bn α1) ♯* p ∧ p ∙ α1 = α2" by (metis Act_eq_iff_perm) moreover obtain q where q_p: "∀b∈bn α1. q ∙ b = p ∙ b" and supp_q: "supp q ⊆ bn α1 ∪ p ∙ bn α1" by (metis set_renaming_perm2) have "supp q ⊆ supp p" proof fix a assume *: "a ∈ supp q" then show "a ∈ supp p" proof (cases "a ∈ bn α1") case True then show ?thesis using "*" q_p by (metis mem_Collect_eq supp_perm) next case False then have "a ∈ p ∙ bn α1" using "*" supp_q using UnE subsetCE by blast with False have "p ∙ a ≠ a" by (metis mem_permute_iff) then show ?thesis using fresh_def fresh_perm by blast qed qed with p have "(supp x1 - bn α1) ♯* q" and "(supp α1 - bn α1) ♯* q" by (meson fresh_def fresh_star_def subset_iff)+ moreover with p and q_p have "⋀a. a ∈ supp α1 ⟹ q ∙ a = p ∙ a" and "⋀a. a ∈ supp x1 ⟹ q ∙ a = p ∙ a" by (metis Diff_iff fresh_perm fresh_star_def)+ then have "q ∙ α1 = p ∙ α1" and "q ∙ x1 = p ∙ x1" by (metis supp_perm_perm_eq)+ ultimately show "?r" using supp_q by (metis bn_eqvt) next assume "?r" then show "?l" by (meson Act_eq_iff_perm) qed text ‹The lifted constructors are free (except for @{const Act}).› lemma Tree_free [simp]: shows "finite (supp xset) ⟹ Conj xset ≠ Not x" and "finite (supp xset) ⟹ Conj xset ≠ Pred φ" and "finite (supp xset) ⟹ Conj xset ≠ Act α x" and "Not x ≠ Pred φ" and "Not x1 ≠ Act α x2" and "Pred φ ≠ Act α x" proof - show "finite (supp xset) ⟹ Conj xset ≠ Not x" by (metis Conj_rep_eq Not.rep_eq Tree⇩_{α}_free(1)) next show "finite (supp xset) ⟹ Conj xset ≠ Pred φ" by (metis Conj_rep_eq Pred.rep_eq Tree⇩_{α}_free(2)) next show "finite (supp xset) ⟹ Conj xset ≠ Act α x" by (metis Conj_rep_eq Act.rep_eq Tree⇩_{α}_free(3)) next show "Not x ≠ Pred φ" by (metis Not.rep_eq Pred.rep_eq Tree⇩_{α}_free(4)) next show "Not x1 ≠ Act α x2" by (metis Not.rep_eq Act.rep_eq Tree⇩_{α}_free(5)) next show "Pred φ ≠ Act α x" by (metis Pred.rep_eq Act.rep_eq Tree⇩_{α}_free(6)) qed subsection ‹Induction over infinitary formulas› lemma formula_induct [case_names Conj Not Pred Act, induct type: formula]: fixes x assumes "⋀xset. finite (supp xset) ⟹ (⋀x. x ∈ set_bset xset ⟹ P x) ⟹ P (Conj xset)" and "⋀formula. P formula ⟹ P (Not formula)" and "⋀pred. P (Pred pred)" and "⋀act formula. P formula ⟹ P (Act act formula)" shows "P x" proof (induction x) fix t⇩_{α}:: "('a,'b,'c) Tree⇩_{α}" assume "t⇩_{α}∈ {t⇩_{α}. hereditarily_fs t⇩_{α}}" then have "hereditarily_fs t⇩_{α}" by simp then show "P (Abs_formula t⇩_{α})" proof (induction t⇩_{α}) case (Conj⇩_{α}tset⇩_{α}) show ?case proof - let ?tset = "map_bset Abs_formula tset⇩_{α}" have "⋀t⇩_{α}'. t⇩_{α}' ∈ set_bset tset⇩_{α}⟹ t⇩_{α}' = (Rep_formula ∘ Abs_formula) t⇩_{α}'" by (simp add: Conj⇩_{α}.hyps) then have "tset⇩_{α}= map_bset (Rep_formula ∘ Abs_formula) tset⇩_{α}" by (metis bset.map_cong0 bset.map_id id_apply) then have *: "tset⇩_{α}= map_bset Rep_formula ?tset" by (metis bset.map_comp) then have "Abs_formula (Conj⇩_{α}tset⇩_{α}) = Conj ?tset" by (metis Conj_def) moreover from "*" have "finite (supp ?tset)" using Conj⇩_{α}.hyps(1) by (metis supp_map_bset_Rep_formula) moreover have "(⋀t. t ∈ set_bset ?tset ⟹ P t)" using Conj⇩_{α}.IH by (metis imageE map_bset.rep_eq) ultimately show ?thesis using assms(1) by metis qed next case Not⇩_{α}then show ?case using assms(2) by (metis Formula.Abs_formula_inverse Not.rep_eq Rep_formula_inverse) next case Pred⇩_{α}show ?case using assms(3) by (metis Pred.abs_eq) next case Act⇩_{α}then show ?case using assms(4) by (metis Formula.Abs_formula_inverse Act.rep_eq Rep_formula_inverse) qed qed subsection ‹Strong induction over infinitary formulas› lemma formula_strong_induct_aux: fixes x assumes "⋀xset c. finite (supp xset) ⟹ (⋀x. x ∈ set_bset xset ⟹ (⋀c. P c x)) ⟹ P c (Conj xset)" and "⋀formula c. (⋀c. P c formula) ⟹ P c (Not formula)" and "⋀pred c. P c (Pred pred)" and "⋀act formula c. bn act ♯* c ⟹ (⋀c. P c formula) ⟹ P c (Act act formula)" shows "⋀(c :: 'd::fs) p. P c (p ∙ x)" proof (induction x) case (Conj xset) moreover then have "finite (supp (p ∙ xset))" by (metis permute_finite supp_eqvt) moreover have "(⋀x c. x ∈ set_bset (p ∙ xset) ⟹ P c x)" using Conj.IH by (metis (full_types) eqvt_bound mem_permute_iff set_bset_eqvt) ultimately show ?case using assms(1) by simp next case Not then show ?case using assms(2) by simp next case Pred show ?case using assms(3) by simp next case (Act α x) show ?case proof - ― ‹rename~@{term "bn (p ∙ α)"} to avoid~@{term c}, without touching~@{term "Act (p ∙ α) (p ∙ x)"}› obtain q where 1: "(q ∙ bn (p ∙ α)) ♯* c" and 2: "supp (Act (p ∙ α) (p ∙ x)) ♯* q" proof (rule at_set_avoiding2[of "bn (p ∙ α)" c "Act (p ∙ α) (p ∙ x)", THEN exE]) show "finite (bn (p ∙ α))" by (fact bn_finite) next show "finite (supp c)" by (fact finite_supp) next show "finite (supp (Act (p ∙ α) (p ∙ x)))" by (simp add: finite_supp) next show "bn (p ∙ α) ♯* Act (p ∙ α) (p ∙ x)" by (simp add: fresh_def fresh_star_def) qed metis from 1 have "bn (q ∙ p ∙ α) ♯* c" by (simp add: bn_eqvt) moreover from Act.IH have "⋀c. P c (q ∙ p ∙ x)" by (metis permute_plus) ultimately have "P c (Act (q ∙ p ∙ α) (q ∙ p ∙ x))" using assms(4) by simp moreover from 2 have "Act (q ∙ p ∙ α) (q ∙ p ∙ x) = Act (p ∙ α) (p ∙ x)" using supp_perm_eq by fastforce ultimately show ?thesis by simp qed qed lemmas formula_strong_induct = formula_strong_induct_aux[where p=0, simplified] declare formula_strong_induct [case_names Conj Not Pred Act] end

# Theory Validity

theory Validity imports Transition_System Formula begin section ‹Validity› text ‹The following is needed to prove termination of~@{term validTree}.› definition alpha_Tree_rel where "alpha_Tree_rel ≡ {(x,y). x =⇩_{α}y}" lemma alpha_Tree_relI [simp]: assumes "x =⇩_{α}y" shows "(x,y) ∈ alpha_Tree_rel" using assms unfolding alpha_Tree_rel_def by simp lemma alpha_Tree_relE: assumes "(x,y) ∈ alpha_Tree_rel" and "x =⇩_{α}y ⟹ P" shows P using assms unfolding alpha_Tree_rel_def by simp lemma wf_alpha_Tree_rel_hull_rel_Tree_wf: "wf (alpha_Tree_rel O hull_rel O Tree_wf)" proof (rule wf_relcomp_compatible) show "wf (hull_rel O Tree_wf)" by (metis Tree_wf_eqvt' wf_Tree_wf wf_hull_rel_relcomp) next show "(hull_rel O Tree_wf) O alpha_Tree_rel ⊆ alpha_Tree_rel O (hull_rel O Tree_wf)" proof fix x :: "('d, 'e, 'f) Tree × ('d, 'e, 'f) Tree" assume "x ∈ (hull_rel O Tree_wf) O alpha_Tree_rel" then obtain x1 x2 x3 x4 where x: "x = (x1,x4)" and 1: "(x1,x2) ∈ hull_rel" and 2: "(x2,x3) ∈ Tree_wf" and 3: "(x3,x4) ∈ alpha_Tree_rel" by auto from 2 have "(x1,x4) ∈ alpha_Tree_rel O hull_rel O Tree_wf" using 1 and 3 proof (induct rule: Tree_wf.induct) ― ‹@{const tConj}› fix t and tset :: "('d,'e,'f) Tree set['d]" assume *: "t ∈ set_bset tset" and **: "(x1,t) ∈ hull_rel" and ***: "(tConj tset, x4) ∈ alpha_Tree_rel" from "**" obtain p where x1: "x1 = p ∙ t" using hull_rel.cases by blast from "***" have "tConj tset =⇩_{α}x4" by (rule alpha_Tree_relE) then obtain tset' where x4: "x4 = tConj tset'" and "rel_bset (=⇩_{α}) tset tset'" by (cases "x4") simp_all with "*" obtain t' where t': "t' ∈ set_bset tset'" and "t =⇩_{α}t'" by (metis rel_bset.rep_eq rel_set_def) with x1 have "(x1, p ∙ t') ∈ alpha_Tree_rel" by (metis Tree⇩_{α}.abs_eq_iff alpha_Tree_relI permute_Tree⇩_{α}.abs_eq) moreover have "(p ∙ t', t') ∈ hull_rel" by (rule hull_rel.intros) moreover from x4 and t' have "(t', x4) ∈ Tree_wf" by (simp add: Tree_wf.intros(1)) ultimately show "(x1,x4) ∈ alpha_Tree_rel O hull_rel O Tree_wf" by auto next ― ‹@{const tNot}› fix t assume *: "(x1,t) ∈ hull_rel" and **: "(tNot t, x4) ∈ alpha_Tree_rel" from "*" obtain p where x1: "x1 = p ∙ t" using hull_rel.cases by blast from "**" have "tNot t =⇩_{α}x4" by (rule alpha_Tree_relE) then obtain t' where x4: "x4 = tNot t'" and "t =⇩_{α}t'" by (cases "x4") simp_all with x1 have "(x1, p ∙ t') ∈ alpha_Tree_rel" by (metis Tree⇩_{α}.abs_eq_iff alpha_Tree_relI permute_Tree⇩_{α}.abs_eq x1) moreover have "(p ∙ t', t') ∈ hull_rel" by (rule hull_rel.intros) moreover from x4 have "(t', x4) ∈ Tree_wf" using Tree_wf.intros(2) by blast ultimately show "(x1,x4) ∈ alpha_Tree_rel O hull_rel O Tree_wf" by auto next ― ‹@{const tAct}› fix α t assume *: "(x1,t) ∈ hull_rel" and **: "(tAct α t, x4) ∈ alpha_Tree_rel" from "*" obtain p where x1: "x1 = p ∙ t" using hull_rel.cases by blast from "**" have "tAct α t =⇩_{α}x4" by (rule alpha_Tree_relE) then obtain q t' where x4: "x4 = tAct (q ∙ α) t'" and "q ∙ t =⇩_{α}t'" by (cases "x4") (auto simp add: alpha_set) with x1 have "(x1, p ∙ -q ∙ t') ∈ alpha_Tree_rel" by (metis Tree⇩_{α}.abs_eq_iff alpha_Tree_relI permute_Tree⇩_{α}.abs_eq permute_minus_cancel(1)) moreover have "(p ∙ -q ∙ t', t') ∈ hull_rel" by (metis hull_rel.simps permute_plus) moreover from x4 have "(t', x4) ∈ Tree_wf" by (simp add: Tree_wf.intros(3)) ultimately show "(x1,x4) ∈ alpha_Tree_rel O hull_rel O Tree_wf" by auto qed with x show "x ∈ alpha_Tree_rel O hull_rel O Tree_wf" by simp qed qed lemma alpha_Tree_rel_relcomp_trivialI [simp]: assumes "(x, y) ∈ R" shows "(x, y) ∈ alpha_Tree_rel O R" using assms unfolding alpha_Tree_rel_def by (metis Tree⇩_{α}.abs_eq_iff case_prodI mem_Collect_eq relcomp.relcompI) lemma alpha_Tree_rel_relcompI [simp]: assumes "x =⇩_{α}x'" and "(x', y) ∈ R" shows "(x, y) ∈ alpha_Tree_rel O R" using assms unfolding alpha_Tree_rel_def by (metis case_prodI mem_Collect_eq relcomp.relcompI) subsection ‹Validity for infinitely branching trees› context nominal_ts begin text ‹Since we defined formulas via a manual quotient construction, we also need to define validity via lifting from the underlying type of infinitely branching trees. We cannot use {\bf nominal\_function} because that generates proof obligations where, for formulas of the form~@{term "Conj xset"}, the assumption that~@{term xset} has finite support is missing.› declare conj_cong [fundef_cong] function valid_Tree :: "'state ⇒ ('idx,'pred,'act) Tree ⇒ bool" where "valid_Tree P (tConj tset) ⟷ (∀t∈set_bset tset. valid_Tree P t)" | "valid_Tree P (tNot t) ⟷ ¬ valid_Tree P t" | "valid_Tree P (tPred φ) ⟷ P ⊢ φ" | "valid_Tree P (tAct α t) ⟷ (∃α' t' P'. tAct α t =⇩_{α}tAct α' t' ∧ P → ⟨α',P'⟩ ∧ valid_Tree P' t')" by pat_completeness auto termination proof let ?R = "inv_image (alpha_Tree_rel O hull_rel O Tree_wf) snd" { show "wf ?R" by (metis wf_alpha_Tree_rel_hull_rel_Tree_wf wf_inv_image) next fix P :: 'state and tset :: "('idx,'pred,'act) Tree set['idx]" and t assume "t ∈ set_bset tset" then show "((P, t), (P, tConj tset)) ∈ ?R" by (simp add: Tree_wf.intros(1)) next fix P :: 'state and t :: "('idx,'pred,'act) Tree" show "((P, t), (P, tNot t)) ∈ ?R" by (simp add: Tree_wf.intros(2)) next fix P1 P2 :: 'state and α1 α2 :: 'act and t1 t2 :: "('idx,'pred,'act) Tree" assume "tAct α1 t1 =⇩_{α}tAct α2 t2" then obtain p where "t2 =⇩_{α}p ∙ t1" by (auto simp add: alphas) (metis alpha_Tree_symp sympE) then show "((P2, t2), (P1, tAct α1 t1)) ∈ ?R" by (simp add: Tree_wf.intros(3)) } qed text ‹@{const valid_Tree} is equivariant.› lemma valid_Tree_eqvt': "valid_Tree P t ⟷ valid_Tree (p ∙ P) (p ∙ t)" proof (induction P t rule: valid_Tree.induct) case (1 P tset) show ?case proof assume *: "valid_Tree P (tConj tset)" { fix t assume "t ∈ p ∙ set_bset tset" with "1.IH" and "*" have "valid_Tree (p ∙ P) t" by (metis (no_types, lifting) imageE permute_set_eq_image valid_Tree.simps(1)) } then show "valid_Tree (p ∙ P) (p ∙ tConj tset)" by simp next assume *: "valid_Tree (p ∙ P) (p ∙ tConj tset)" { fix t assume "t ∈ set_bset tset" with "1.IH" and "*" have "valid_Tree P t" by (metis mem_permute_iff permute_Tree_tConj set_bset_eqvt valid_Tree.simps(1)) } then show "valid_Tree P (tConj tset)" by simp qed next case 2 then show ?case by simp next case 3 show ?case by simp (metis permute_minus_cancel(2) satisfies_eqvt) next case (4 P α t) show ?case proof assume "valid_Tree P (tAct α t)" then obtain α' t' P' where *: "tAct α t =⇩_{α}tAct α' t' ∧ P → ⟨α',P'⟩ ∧ valid_Tree P' t'" by auto with "4.IH" have "valid_Tree (p ∙ P') (p ∙ t')" by blast moreover from "*" have "p ∙ P → ⟨p ∙ α', p ∙ P'⟩" by (metis transition_eqvt') moreover from "*" have "p ∙ tAct α t =⇩_{α}tAct (p ∙ α') (p ∙ t')" by (metis alpha_Tree_eqvt permute_Tree.simps(4)) ultimately show "valid_Tree (p ∙ P) (p ∙ tAct α t)" by auto next assume "valid_Tree (p ∙ P) (p ∙ tAct α t)" then obtain α' t' P' where *: "p ∙ tAct α t =⇩_{α}tAct α' t' ∧ (p ∙ P) → ⟨α',P'⟩ ∧ valid_Tree P' t'" by auto then have eq: "tAct α t =⇩_{α}tAct (-p ∙ α') (-p ∙ t')" by (metis alpha_Tree_eqvt permute_Tree.simps(4) permute_minus_cancel(2)) moreover from "*" have "P → ⟨-p ∙ α', -p ∙ P'⟩" by (metis permute_minus_cancel(2) transition_eqvt') moreover with "4.IH" have "valid_Tree (-p ∙ P') (-p ∙ t')" using eq and "*" by simp ultimately show "valid_Tree P (tAct α t)" by auto qed qed lemma valid_Tree_eqvt (*[eqvt]*): assumes "valid_Tree P t" shows "valid_Tree (p ∙ P) (p ∙ t)" using assms by (metis valid_Tree_eqvt') text ‹$\alpha$-equivalent trees validate the same states.› lemma alpha_Tree_valid_Tree: assumes "t1 =⇩_{α}t2" shows "valid_Tree P t1 ⟷ valid_Tree P t2" using assms proof (induction t1 t2 arbitrary: P rule: alpha_Tree_induct) case tConj then show ?case by auto (metis (mono_tags) rel_bset.rep_eq rel_set_def)+ next case (tAct α1 t1 α2 t2) show ?case proof assume "valid_Tree P (tAct α1 t1)" then obtain α' t' P' where "tAct α1 t1 =⇩_{α}tAct α' t' ∧ P → ⟨α',P'⟩ ∧ valid_Tree P' t'" by auto moreover from tAct.hyps have "tAct α1 t1 =⇩_{α}tAct α2 t2" using alpha_tAct by blast ultimately show "valid_Tree P (tAct α2 t2)" by (metis Tree⇩_{α}.abs_eq_iff valid_Tree.simps(4)) next assume "valid_Tree P (tAct α2 t2)" then obtain α' t' P' where "tAct α2 t2 =⇩_{α}tAct α' t' ∧ P → ⟨α',P'⟩ ∧ valid_Tree P' t'" by auto moreover from tAct.hyps have "tAct α1 t1 =⇩_{α}tAct α2 t2" using alpha_tAct by blast ultimately show "valid_Tree P (tAct α1 t1)" by (metis Tree⇩_{α}.abs_eq_iff valid_Tree.simps(4)) qed qed simp_all subsection ‹Validity for trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence› lift_definition valid_Tree⇩_{α}:: "'state ⇒ ('idx,'pred,'act) Tree⇩_{α}⇒ bool" is valid_Tree by (fact alpha_Tree_valid_Tree) lemma valid_Tree⇩_{α}_eqvt (*[eqvt]*): assumes "valid_Tree⇩_{α}P t" shows "valid_Tree⇩_{α}(p ∙ P) (p ∙ t)" using assms by transfer (fact valid_Tree_eqvt) lemma valid_Tree⇩_{α}_Conj⇩_{α}[simp]: "valid_Tree⇩_{α}P (Conj⇩_{α}tset⇩_{α}) ⟷ (∀t⇩_{α}∈set_bset tset⇩_{α}. valid_Tree⇩_{α}P t⇩_{α})" proof - have "valid_Tree P (rep_Tree⇩_{α}(abs_Tree⇩_{α}(tConj (map_bset rep_Tree⇩_{α}tset⇩_{α})))) ⟷ valid_Tree P (tConj (map_bset rep_Tree⇩_{α}tset⇩_{α}))" by (metis Tree⇩_{α}_rep_abs alpha_Tree_valid_Tree) then show ?thesis by (simp add: valid_Tree⇩_{α}_def Conj⇩_{α}_def map_bset.rep_eq) qed lemma valid_Tree⇩_{α}_Not⇩_{α}[simp]: "valid_Tree⇩_{α}P (Not⇩_{α}t⇩_{α}) ⟷ ¬ valid_Tree⇩_{α}P t⇩_{α}" by transfer simp lemma valid_Tree⇩_{α}_Pred⇩_{α}[simp]: "valid_Tree⇩_{α}P (Pred⇩_{α}φ) ⟷ P ⊢ φ" by transfer simp lemma valid_Tree⇩_{α}_Act⇩_{α}[simp]: "valid_Tree⇩_{α}P (Act⇩_{α}α t⇩_{α}) ⟷ (∃α' t⇩_{α}' P'. Act⇩_{α}α t⇩_{α}= Act⇩_{α}α' t⇩_{α}' ∧ P → ⟨α',P'⟩ ∧ valid_Tree⇩_{α}P' t⇩_{α}')" proof assume "valid_Tree⇩_{α}P (Act⇩_{α}α t⇩_{α})" moreover have "Act⇩_{α}α t⇩_{α}= abs_Tree⇩_{α}(tAct α (rep_Tree⇩_{α}t⇩_{α}))" by (metis Act⇩_{α}.abs_eq Tree⇩_{α}_abs_rep) ultimately show "∃α' t⇩_{α}' P'. Act⇩_{α}α t⇩_{α}= Act⇩_{α}α' t⇩_{α}' ∧ P → ⟨α',P'⟩ ∧ valid_Tree⇩_{α}P' t⇩_{α}'" by (metis Act⇩_{α}.abs_eq Tree⇩_{α}.abs_eq_iff valid_Tree.simps(4) valid_Tree⇩_{α}.abs_eq) next assume "∃α' t⇩_{α}' P'. Act⇩_{α}α t⇩_{α}= Act⇩_{α}α' t⇩_{α}' ∧ P → ⟨α',P'⟩ ∧ valid_Tree⇩_{α}P' t⇩_{α}'" moreover have "⋀α' t⇩_{α}'. Act⇩_{α}α' t⇩_{α}' = abs_Tree⇩_{α}(tAct α' (rep_Tree⇩_{α}t⇩_{α}'))" by (metis Act⇩_{α}.abs_eq Tree⇩_{α}_abs_rep) ultimately show "valid_Tree⇩_{α}P (Act⇩_{α}α t⇩_{α})" by (metis Tree⇩_{α}.abs_eq_iff valid_Tree.simps(4) valid_Tree⇩_{α}.abs_eq valid_Tree⇩_{α}.rep_eq) qed subsection ‹Validity for infinitary formulas› lift_definition valid :: "'state ⇒ ('idx,'pred,'act) formula ⇒ bool" (infix "⊨" 70) is valid_Tree⇩_{α}. lemma valid_eqvt (*[eqvt]*): assumes "P ⊨ x" shows "(p ∙ P) ⊨ (p ∙ x)" using assms by transfer (metis valid_Tree⇩_{α}_eqvt) lemma valid_Conj [simp]: assumes "finite (supp xset)" shows "P ⊨ Conj xset ⟷ (∀x∈set_bset xset. P ⊨ x)" using assms by (simp add: valid_def Conj_def map_bset.rep_eq) lemma valid_Not [simp]: "P ⊨ Not x ⟷ ¬ P ⊨ x" by transfer simp lemma valid_Pred [simp]: "P ⊨ Pred φ ⟷ P ⊢ φ" by transfer simp lemma valid_Act: "P ⊨ Act α x ⟷ (∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x')" proof assume "P ⊨ Act α x" moreover have "Rep_formula (Abs_formula (Act⇩_{α}α (Rep_formula x))) = Act⇩_{α}α (Rep_formula x)" by (metis Act.rep_eq Rep_formula_inverse) ultimately show "∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x'" by (auto simp add: valid_def Act_def) (metis Abs_formula_inverse Rep_formula' hereditarily_fs_alpha_renaming) next assume "∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x'" then show "P ⊨ Act α x" by (metis Act.rep_eq valid.rep_eq valid_Tree⇩_{α}_Act⇩_{α}) qed text ‹The binding names in the alpha-variant that witnesses validity may be chosen fresh for any finitely supported context.› lemma valid_Act_strong: assumes "finite (supp X)" shows "P ⊨ Act α x ⟷ (∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x' ∧ bn α' ♯* X)" proof assume "P ⊨ Act α x" then obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P → ⟨α',P'⟩" and valid: "P' ⊨ x'" by (metis valid_Act) have "finite (bn α')" by (fact bn_finite) moreover note ‹finite (supp X)› moreover have "finite (supp (Act α' x', ⟨α',P'⟩))" by (metis finite_Diff finite_UnI finite_supp supp_Pair supp_abs_residual_pair) moreover have "bn α' ♯* (Act α' x', ⟨α',P'⟩)" by (auto simp add: fresh_star_def fresh_def supp_Pair supp_abs_residual_pair) ultimately obtain p where fresh_X: "(p ∙ bn α') ♯* X" and "supp (Act α' x', ⟨α',P'⟩) ♯* p" by (metis at_set_avoiding2) then have "supp (Act α' x') ♯* p" and "supp ⟨α',P'⟩ ♯* p" by (metis fresh_star_Un supp_Pair)+ then have "Act (p ∙ α') (p ∙ x') = Act α' x'" and "⟨p ∙ α', p ∙ P'⟩ = ⟨α',P'⟩" by (metis Act_eqvt supp_perm_eq, metis abs_residual_pair_eqvt supp_perm_eq) then show "∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x' ∧ bn α' ♯* X" using eq and trans and valid and fresh_X by (metis bn_eqvt valid_eqvt) next assume "∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x' ∧ bn α' ♯* X" then show "P ⊨ Act α x" by (metis valid_Act) qed lemma valid_Act_fresh: assumes "bn α ♯* P" shows "P ⊨ Act α x ⟷ (∃P'. P → ⟨α,P'⟩ ∧ P' ⊨ x)" proof assume "P ⊨ Act α x" moreover have "finite (supp P)" by (fact finite_supp) ultimately obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P → ⟨α',P'⟩" and valid: "P' ⊨ x'" and fresh: "bn α' ♯* P" by (metis valid_Act_strong) from eq obtain p where p_α: "α' = p ∙ α" and p_x: "x' = p ∙ x" and supp_p: "supp p ⊆ bn α ∪ p ∙ bn α" by (metis Act_eq_iff_perm_renaming) from assms and fresh have "(bn α ∪ p ∙ bn α) ♯* P" using p_α by (metis bn_eqvt fresh_star_Un) then have "supp p ♯* P" using supp_p by (metis fresh_star_def subset_eq) then have p_P: "-p ∙ P = P" by (metis perm_supp_eq supp_minus_perm) from trans have "P → ⟨α,-p ∙ P'⟩" using p_P p_α by (metis permute_minus_cancel(1) transition_eqvt') moreover from valid have "-p ∙ P' ⊨ x" using p_x by (metis permute_minus_cancel(1) valid_eqvt) ultimately show "∃P'. P → ⟨α,P'⟩ ∧ P' ⊨ x" by meson next assume "∃P'. P → ⟨α,P'⟩ ∧ P' ⊨ x" then show "P ⊨ Act α x" by (metis valid_Act) qed end end

# Theory Logical_Equivalence

theory Logical_Equivalence imports Validity begin section ‹(Strong) Logical Equivalence› text ‹The definition of formulas is parametric in the index type, but from now on we want to work with a fixed (sufficiently large) index type.› locale indexed_nominal_ts = nominal_ts satisfies transition for satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool" (infix "⊢" 70) and transition :: "'state ⇒ ('act::bn,'state) residual ⇒ bool" (infix "→" 70) + assumes card_idx_perm: "|UNIV::perm set| <o |UNIV::'idx set|" and card_idx_state: "|UNIV::'state set| <o |UNIV::'idx set|" begin definition logically_equivalent :: "'state ⇒ 'state ⇒ bool" where "logically_equivalent P Q ≡ (∀x::('idx,'pred,'act) formula. P ⊨ x ⟷ Q ⊨ x)" notation logically_equivalent (infix "=⋅" 50) lemma logically_equivalent_eqvt: assumes "P =⋅ Q" shows "p ∙ P =⋅ p ∙ Q" using assms unfolding logically_equivalent_def by (metis (mono_tags) permute_minus_cancel(1) valid_eqvt) end end

# Theory Bisimilarity_Implies_Equivalence

theory Bisimilarity_Implies_Equivalence imports Logical_Equivalence begin section ‹Bisimilarity Implies Logical Equivalence› context indexed_nominal_ts begin lemma bisimilarity_implies_equivalence_Act: assumes "⋀P Q. P ∼⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x" and "P ∼⋅ Q" and "P ⊨ Act α x" shows "Q ⊨ Act α x" proof - have "finite (supp Q)" by (fact finite_supp) with ‹P ⊨ Act α x› obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P → ⟨α',P'⟩" and valid: "P' ⊨ x'" and fresh: "bn α' ♯* Q" by (metis valid_Act_strong) from ‹P ∼⋅ Q› and fresh and trans obtain Q' where trans': "Q → ⟨α',Q'⟩" and bisim': "P' ∼⋅ Q'" by (metis bisimilar_simulation_step) from eq obtain p where px: "x' = p ∙ x" by (metis Act_eq_iff_perm) with valid have "-p ∙ P' ⊨ x" by (metis permute_minus_cancel(1) valid_eqvt) moreover from bisim' have "(-p ∙ P') ∼⋅ (-p ∙ Q')" by (metis bisimilar_eqvt) ultimately have "-p ∙ Q' ⊨ x" using ‹⋀P Q. P ∼⋅ Q ⟹ P ⊨ x ⟷ Q ⊨ x› by metis with px have "Q' ⊨ x'" by (metis permute_minus_cancel(1) valid_eqvt) with eq and trans' show "Q ⊨ Act α x" unfolding valid_Act by metis qed theorem bisimilarity_implies_equivalence: assumes "P ∼⋅ Q" shows "P =⋅ Q" unfolding logically_equivalent_def proof fix x :: "('idx, 'pred, 'act) formula" from assms show "P ⊨ x ⟷ Q ⊨ x" proof (induction x arbitrary: P Q) case (Conj xset) then show ?case by simp next case Not then show ?case by simp next case Pred then show ?case by (metis bisimilar_is_bisimulation is_bisimulation_def symp_def valid_Pred) next case (Act α x) then show ?case by (metis bisimilar_symp bisimilarity_implies_equivalence_Act sympE) qed qed end end

# Theory Equivalence_Implies_Bisimilarity

theory Equivalence_Implies_Bisimilarity imports Logical_Equivalence begin section ‹Logical Equivalence Implies Bisimilarity› context indexed_nominal_ts begin definition is_distinguishing_formula :: "('idx, 'pred, 'act) formula ⇒ 'state ⇒ 'state ⇒ bool" ("_ distinguishes _ from _" [100,100,100] 100) where "x distinguishes P from Q ≡ P ⊨ x ∧ ¬ Q ⊨ x" lemma is_distinguishing_formula_eqvt (*[eqvt]*): assumes "x distinguishes P from Q" shows "(p ∙ x) distinguishes (p ∙ P) from (p ∙ Q)" using assms unfolding is_distinguishing_formula_def by (metis permute_minus_cancel(2) valid_eqvt) lemma equivalent_iff_not_distinguished: "(P =⋅ Q) ⟷ ¬(∃x. x distinguishes P from Q)" by (metis (full_types) is_distinguishing_formula_def logically_equivalent_def valid_Not) text ‹There exists a distinguishing formula for~@{term P} and~@{term Q} whose support is contained in~@{term "supp P"}.› lemma distinguished_bounded_support: assumes "x distinguishes P from Q" obtains y where "supp y ⊆ supp P" and "y distinguishes P from Q" proof - let ?B = "{p ∙ x|p. supp P ♯* p}" have "supp P supports ?B" unfolding supports_def proof (clarify) fix a b assume a: "a ∉ supp P" and b: "b ∉ supp P" have "(a ⇌ b) ∙ ?B ⊆ ?B" proof fix x' assume "x' ∈ (a ⇌ b) ∙ ?B" then obtain p where 1: "x' = (a ⇌ b) ∙ p ∙ x" and 2: "supp P ♯* p" by (auto simp add: permute_set_def) let ?q = "(a ⇌ b) + p" from 1 have "x' = ?q ∙ x" by simp moreover from a and b and 2 have "supp P ♯* ?q" by (metis fresh_perm fresh_star_def fresh_star_plus swap_atom_simps(3)) ultimately show "x' ∈ ?B" by blast qed moreover have "?B ⊆ (a ⇌ b) ∙ ?B" proof fix x' assume "x' ∈ ?B" then obtain p where 1: "x' = p ∙ x" and 2: "supp P ♯* p" by auto let ?q = "(a ⇌ b) + p" from 1 have "x' = (a ⇌ b) ∙ ?q ∙ x" by simp moreover from a and b and 2 have "supp P ♯* ?q" by (metis fresh_perm fresh_star_def fresh_star_plus swap_atom_simps(3)) ultimately show "x' ∈ (a ⇌ b) ∙ ?B" using mem_permute_iff by blast qed ultimately show "(a ⇌ b) ∙ ?B = ?B" .. qed then have supp_B_subset_supp_P: "supp ?B ⊆ supp P" by (metis (erased, lifting) finite_supp supp_is_subset) then have finite_supp_B: "finite (supp ?B)" using finite_supp rev_finite_subset by blast have "?B ⊆ (λp. p ∙ x) ` UNIV" by auto then have "|?B| ≤o |UNIV :: perm set|" by (rule surj_imp_ordLeq) also have "|UNIV :: perm set| <o |UNIV :: 'idx set|" by (metis card_idx_perm) also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|" by (metis Cnotzero_UNIV ordLeq_csum2) finally have card_B: "|?B| <o natLeq +c |UNIV :: 'idx set|" . let ?y = "Conj (Abs_bset ?B) :: ('idx, 'pred, 'act) formula" from finite_supp_B and card_B and supp_B_subset_supp_P have "supp ?y ⊆ supp P" by simp moreover have "?y distinguishes P from Q" unfolding is_distinguishing_formula_def proof from assms show "P ⊨ ?y" by (auto simp add: card_B finite_supp_B) (metis is_distinguishing_formula_def supp_perm_eq valid_eqvt) next from assms show "¬ Q ⊨ ?y" by (auto simp add: card_B finite_supp_B) (metis is_distinguishing_formula_def permute_zero fresh_star_zero) qed ultimately show ?thesis .. qed lemma equivalence_is_bisimulation: "is_bisimulation logically_equivalent" proof - have "symp logically_equivalent" by (metis logically_equivalent_def sympI) moreover { fix P Q φ assume "P =⋅ Q" then have "P ⊢ φ ⟶ Q ⊢ φ" by (metis logically_equivalent_def valid_Pred) } moreover { fix P Q α P' assume "P =⋅ Q" and "bn α ♯* Q" and "P → ⟨α,P'⟩" then have "∃Q'. Q → ⟨α,Q'⟩ ∧ P' =⋅ Q'" proof - { let ?Q' = "{Q'. Q → ⟨α,Q'⟩}" assume "∀Q'∈?Q'. ¬ P' =⋅ Q'" then have "∀Q'∈?Q'. ∃x :: ('idx, 'pred, 'act) formula. x distinguishes P' from Q'" by (metis equivalent_iff_not_distinguished) then have "∀Q'∈?Q'. ∃x :: ('idx, 'pred, 'act) formula. supp x ⊆ supp P' ∧ x distinguishes P' from Q'" by (metis distinguished_bounded_support) then obtain f :: "'state ⇒ ('idx, 'pred, 'act) formula" where *: "∀Q'∈?Q'. supp (f Q') ⊆ supp P' ∧ (f Q') distinguishes P' from Q'" by metis have "supp (f ` ?Q') ⊆ supp P'" by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast) then have finite_supp_image: "finite (supp (f ` ?Q'))" using finite_supp rev_finite_subset by blast have "|f ` ?Q'| ≤o |UNIV :: 'state set|" by (metis card_of_UNIV card_of_image ordLeq_transitive) also have "|UNIV :: 'state set| <o |UNIV :: 'idx set|" by (metis card_idx_state) also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|" by (metis Cnotzero_UNIV ordLeq_csum2) finally have card_image: "|f ` ?Q'| <o natLeq +c |UNIV :: 'idx set|" . let ?y = "Conj (Abs_bset (f ` ?Q')) :: ('idx, 'pred, 'act) formula" have "P ⊨ Act α ?y" unfolding valid_Act proof (standard+) show "P → ⟨α,P'⟩" by fact next { fix Q' assume "Q → ⟨α,Q'⟩" with "*" have "P' ⊨ f Q'" by (metis is_distinguishing_formula_def mem_Collect_eq) } then show "P' ⊨ ?y" by (simp add: finite_supp_image card_image) qed moreover have "¬ Q ⊨ Act α ?y" proof assume "Q ⊨ Act α ?y" then obtain Q' where 1: "Q → ⟨α,Q'⟩" and 2: "Q' ⊨ ?y" using ‹bn α ♯* Q› by (metis valid_Act_fresh) from 2 have "⋀Q''. Q → ⟨α,Q''⟩ ⟶ Q' ⊨ f Q''" by (simp add: finite_supp_image card_image) with 1 and "*" show False using is_distinguishing_formula_def by blast qed ultimately have False by (metis ‹P =⋅ Q› logically_equivalent_def) } then show ?thesis by auto qed } ultimately show ?thesis unfolding is_bisimulation_def by metis qed theorem equivalence_implies_bisimilarity: assumes "P =⋅ Q" shows "P ∼⋅ Q" using assms by (metis bisimilar_def equivalence_is_bisimulation) end end

# Theory Disjunction

theory Disjunction imports Formula Validity begin section ‹Disjunction› definition Disj :: "('idx,'pred::fs,'act::bn) formula set['idx] ⇒ ('idx,'pred,'act) formula" where "Disj xset = Not (Conj (map_bset Not xset))" lemma finite_supp_map_bset_Not [simp]: assumes "finite (supp xset)" shows "finite (supp (map_bset Not xset))" proof - have "eqvt map_bset" and "eqvt Not" by (simp add: eqvtI)+ then have "supp (map_bset Not) = {}" using supp_fun_eqvt supp_fun_app_eqvt by blast then have "supp (map_bset Not xset) ⊆ supp xset" using supp_fun_app by blast with assms show "finite (supp (map_bset Not xset))" by (metis finite_subset) qed lemma Disj_eqvt [simp]: assumes "finite (supp xset)" shows "p ∙ Disj xset = Disj (p ∙ xset)" using assms unfolding Disj_def by simp lemma Disj_eq_iff [simp]: assumes "finite (supp xset1)" and "finite (supp xset2)" shows "Disj xset1 = Disj xset2 ⟷ xset1 = xset2" using assms unfolding Disj_def by (metis Conj_eq_iff Not_eq_iff bset.inj_map_strong finite_supp_map_bset_Not) context nominal_ts begin lemma valid_Disj [simp]: assumes "finite (supp xset)" shows "P ⊨ Disj xset ⟷ (∃x∈set_bset xset. P ⊨ x)" using assms by (simp add: Disj_def map_bset.rep_eq) end end

# Theory Expressive_Completeness

theory Expressive_Completeness imports Bisimilarity_Implies_Equivalence Equivalence_Implies_Bisimilarity Disjunction begin section ‹Expressive Completeness› context indexed_nominal_ts begin subsection ‹Distinguishing formulas› text ‹Lemma \emph{distinguished\_bounded\_support} only shows the existence of a distinguishing formula, without stating what this formula looks like. We now define an explicit function that returns a distinguishing formula, in a way that this function is equivariant (on pairs of non-equivalent states). Note that this definition uses Hilbert's choice operator~$\varepsilon$, which is not necessarily equivariant. This is immediately remedied by a hull construction.› definition distinguishing_formula :: "'state ⇒ 'state ⇒ ('idx, 'pred, 'act) formula" where "distinguishing_formula P Q ≡ Conj (Abs_bset {-p ∙ (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))|p. True})" ― ‹just an auxiliary lemma that will be useful further below› lemma distinguishing_formula_card_aux: "|{-p ∙ (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))|p. True}| <o natLeq +c |UNIV :: 'idx set|" proof - let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))" let ?B = "{-p ∙ ?some p|p. True}" have "?B ⊆ (λp. -p ∙ ?some p) ` UNIV" by auto then have "|?B| ≤o |UNIV :: perm set|" by (rule surj_imp_ordLeq) also have "|UNIV :: perm set| <o |UNIV :: 'idx set|" by (metis card_idx_perm) also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|" by (metis Cnotzero_UNIV ordLeq_csum2) finally show ?thesis . qed ― ‹just an auxiliary lemma that will be useful further below› lemma distinguishing_formula_supp_aux: assumes "¬ (P =⋅ Q)" shows "supp (Abs_bset {-p ∙ (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))|p. True} :: _ set['idx]) ⊆ supp P" proof - let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))" let ?B = "{-p ∙ ?some p|p. True}" { fix p from assms have "¬ (p ∙ P =⋅ p ∙ Q)" by (metis logically_equivalent_eqvt permute_minus_cancel(2)) then have "supp (?some p) ⊆ supp (p ∙ P)" using distinguished_bounded_support by (metis (mono_tags, lifting) equivalent_iff_not_distinguished someI_ex) } note supp_some = this { fix x assume "x ∈ ?B" then obtain p where "x = -p ∙ ?some p" by blast with supp_some have "supp (p ∙ x) ⊆ supp (p ∙ P)" by simp then have "supp x ⊆ supp P" by (metis (full_types) permute_boolE subset_eqvt supp_eqvt) } note "*" = this have supp_B: "supp ?B ⊆ supp P" by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast) from supp_B and distinguishing_formula_card_aux show ?thesis using supp_Abs_bset by blast qed lemma distinguishing_formula_eqvt [simp]: assumes "¬ (P =⋅ Q)" shows "p ∙ distinguishing_formula P Q = distinguishing_formula (p ∙ P) (p ∙ Q)" proof - let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))" let ?B = "{-p ∙ ?some p|p. True}" from assms have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P" by (rule distinguishing_formula_supp_aux) then have "finite (supp (Abs_bset ?B :: _ set['idx]))" using finite_supp rev_finite_subset by blast with distinguishing_formula_card_aux have *: "p ∙ Conj (Abs_bset ?B) = Conj (Abs_bset (p ∙ ?B))" by simp let ?some' = "λp'. (ϵx. supp x ⊆ supp (p' ∙ p ∙ P) ∧ x distinguishes (p' ∙ p ∙ P) from (p' ∙ p ∙ Q))" let ?B' = "{-p' ∙ ?some' p'|p'. True}" have "p ∙ ?B = ?B'" proof { fix px assume "px ∈ p ∙ ?B" then obtain x where 1: "px = p ∙ x" and 2: "x ∈ ?B" by (metis (no_types, lifting) image_iff permute_set_eq_image) from 2 obtain p' where 3: "x = -p' ∙ ?some p'" by blast from 1 and 3 have "px = -(p' - p) ∙ ?some' (p' - p)" by simp then have "px ∈ ?B'" by blast } then show "p ∙ ?B ⊆ ?B'" by blast next { fix x assume "x ∈ ?B'" then obtain p' where "x = -p' ∙ ?some' p'" by blast then have "x = p ∙ -(p' + p) ∙ ?some (p' + p)" by (simp add: add.inverse_distrib_swap) then have "x ∈ p ∙ ?B" using mem_permute_iff by blast } then show "?B' ⊆ p ∙ ?B" by blast qed with "*" show ?thesis unfolding distinguishing_formula_def by simp qed lemma supp_distinguishing_formula: assumes "¬ (P =⋅ Q)" shows "supp (distinguishing_formula P Q) ⊆ supp P" proof - let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))" let ?B = "{- p ∙ ?some p|p. True}" from assms have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P" by (rule distinguishing_formula_supp_aux) moreover from this have "finite (supp (Abs_bset ?B :: _ set['idx]))" using finite_supp rev_finite_subset by blast ultimately show ?thesis unfolding distinguishing_formula_def by simp qed lemma distinguishing_formula_distinguishes: assumes "¬ (P =⋅ Q)" shows "(distinguishing_formula P Q) distinguishes P from Q" proof - let ?some = "λp. (ϵx. supp x ⊆ supp (p ∙ P) ∧ x distinguishes (p ∙ P) from (p ∙ Q))" let ?B = "{- p ∙ ?some p|p. True}" { fix p have "(?some p) distinguishes (p ∙ P) from (p ∙ Q)" using assms by (metis (mono_tags, lifting) is_distinguishing_formula_eqvt distinguished_bounded_support equivalent_iff_not_distinguished someI_ex) } note some_distinguishes = this { fix P' from assms have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P" by (rule distinguishing_formula_supp_aux) then have "finite (supp (Abs_bset ?B :: _ set['idx]))" using finite_supp rev_finite_subset by blast with distinguishing_formula_card_aux have "P' ⊨ distinguishing_formula P Q ⟷ (∀x∈?B. P' ⊨ x)" unfolding distinguishing_formula_def by simp } note valid_distinguishing_formula = this { fix p have "P ⊨ -p ∙ ?some p" by (metis (mono_tags) is_distinguishing_formula_def permute_minus_cancel(2) some_distinguishes valid_eqvt) } then have "P ⊨ distinguishing_formula P Q" using valid_distinguishing_formula by blast moreover have "¬ Q ⊨ distinguishing_formula P Q" using valid_distinguishing_formula by (metis (mono_tags, lifting) is_distinguishing_formula_def mem_Collect_eq permute_minus_cancel(1) some_distinguishes valid_eqvt) ultimately show "(distinguishing_formula P Q) distinguishes P from Q" using is_distinguishing_formula_def by blast qed subsection ‹Characteristic formulas› text ‹A \emph{characteristic formula} for a state~$P$ is valid for (exactly) those states that are bisimilar to~$P$.› definition characteristic_formula :: "'state ⇒ ('idx, 'pred, 'act) formula" where "characteristic_formula P ≡ Conj (Abs_bset {distinguishing_formula P Q|Q. ¬ (P =⋅ Q)})" ― ‹just an auxiliary lemma that will be useful further below› lemma characteristic_formula_card_aux: "|{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}| <o natLeq +c |UNIV :: 'idx set|" proof - let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}" have "?B ⊆ (distinguishing_formula P) ` UNIV" by auto then have "|?B| ≤o |UNIV :: 'state set|" by (rule surj_imp_ordLeq) also have "|UNIV :: 'state set| <o |UNIV :: 'idx set|" by (metis card_idx_state) also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|" by (metis Cnotzero_UNIV ordLeq_csum2) finally show ?thesis . qed ― ‹just an auxiliary lemma that will be useful further below› lemma characteristic_formula_supp_aux: shows "supp (Abs_bset {distinguishing_formula P Q|Q. ¬ (P =⋅ Q)} :: _ set['idx]) ⊆ supp P" proof - let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}" { fix x assume "x ∈ ?B" then obtain Q where "x = distinguishing_formula P Q" and "¬ (P =⋅ Q)" by blast with supp_distinguishing_formula have "supp x ⊆ supp P" by metis } note "*" = this have supp_B: "supp ?B ⊆ supp P" by (rule set_bounded_supp, fact finite_supp, cut_tac "*", blast) from supp_B and characteristic_formula_card_aux show ?thesis using supp_Abs_bset by blast qed lemma characteristic_formula_eqvt (*[eqvt]*) [simp]: "p ∙ characteristic_formula P = characteristic_formula (p ∙ P)" proof - let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}" have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P" by (fact characteristic_formula_supp_aux) then have "finite (supp (Abs_bset ?B :: _ set['idx]))" using finite_supp rev_finite_subset by blast with characteristic_formula_card_aux have *: "p ∙ Conj (Abs_bset ?B) = Conj (Abs_bset (p ∙ ?B))" by simp let ?B' = "{distinguishing_formula (p ∙ P) Q|Q. ¬ ((p ∙ P) =⋅ Q)}" have "p ∙ ?B = ?B'" proof { fix px assume "px ∈ p ∙ ?B" then obtain x where 1: "px = p ∙ x" and 2: "x ∈ ?B" by (metis (no_types, lifting) image_iff permute_set_eq_image) from 2 obtain Q where 3: "x = distinguishing_formula P Q" and 4: "¬ (P =⋅ Q)" by blast with 1 have "px = distinguishing_formula (p ∙ P) (p ∙ Q)" by simp moreover from 4 have "¬ ((p ∙ P) =⋅ (p ∙ Q))" by (metis logically_equivalent_eqvt permute_minus_cancel(2)) ultimately have "px ∈ ?B'" by blast } then show "p ∙ ?B ⊆ ?B'" by blast next { fix x assume "x ∈ ?B'" then obtain Q where 1: "x = distinguishing_formula (p ∙ P) Q" and 2: "¬ ((p ∙ P) =⋅ Q)" by blast from 2 have "¬ (P =⋅ (-p ∙ Q))" by (metis logically_equivalent_eqvt permute_minus_cancel(1)) moreover from this and 1 have "x = p ∙ distinguishing_formula P (-p ∙ Q)" by simp ultimately have "x ∈ p ∙ ?B" using mem_permute_iff by blast } then show "?B' ⊆ p ∙ ?B" by blast qed with "*" show ?thesis unfolding characteristic_formula_def by simp qed lemma characteristic_formula_eqvt_raw [simp]: "p ∙ characteristic_formula = characteristic_formula" by (simp add: permute_fun_def) lemma characteristic_formula_is_characteristic': "Q ⊨ characteristic_formula P ⟷ P =⋅ Q" proof - let ?B = "{distinguishing_formula P Q|Q. ¬ (P =⋅ Q)}" { fix P' have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp P" by (fact characteristic_formula_supp_aux) then have "finite (supp (Abs_bset ?B :: _ set['idx]))" using finite_supp rev_finite_subset by blast with characteristic_formula_card_aux have "P' ⊨ characteristic_formula P ⟷ (∀x∈?B. P' ⊨ x)" unfolding characteristic_formula_def by simp } note valid_characteristic_formula = this show ?thesis proof assume *: "Q ⊨ characteristic_formula P" show "P =⋅ Q" proof (rule ccontr) assume "¬ (P =⋅ Q)" with "*" show False using distinguishing_formula_distinguishes is_distinguishing_formula_def valid_characteristic_formula by auto qed next assume "P =⋅ Q" moreover have "P ⊨ characteristic_formula P" using distinguishing_formula_distinguishes is_distinguishing_formula_def valid_characteristic_formula by auto ultimately show "Q ⊨ characteristic_formula P" using logically_equivalent_def by blast qed qed lemma characteristic_formula_is_characteristic: "Q ⊨ characteristic_formula P ⟷ P ∼⋅ Q" using characteristic_formula_is_characteristic' by (meson bisimilarity_implies_equivalence equivalence_implies_bisimilarity) subsection ‹Expressive completeness› text ‹Every finitely supported set of states that is closed under bisimulation can be described by a formula; namely, by a disjunction of characteristic formulas.› theorem expressive_completeness: assumes "finite (supp S)" and "⋀P Q. P ∈ S ⟹ P ∼⋅ Q ⟹ Q ∈ S" shows "P ⊨ Disj (Abs_bset (characteristic_formula ` S)) ⟷ P ∈ S" proof - let ?B = "characteristic_formula ` S" have "?B ⊆ characteristic_formula ` UNIV" by auto then have "|?B| ≤o |UNIV :: 'state set|" by (rule surj_imp_ordLeq) also have "|UNIV :: 'state set| <o |UNIV :: 'idx set|" by (metis card_idx_state) also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|" by (metis Cnotzero_UNIV ordLeq_csum2) finally have card_B: "|?B| <o natLeq +c |UNIV :: 'idx set|" . have "eqvt image" and "eqvt characteristic_formula" by (simp add: eqvtI)+ then have "supp ?B ⊆ supp S" using supp_fun_eqvt supp_fun_app supp_fun_app_eqvt by blast with card_B have "supp (Abs_bset ?B :: _ set['idx]) ⊆ supp S" using supp_Abs_bset by blast with ‹finite (supp S)› have "finite (supp (Abs_bset ?B :: _ set['idx]))" using finite_supp rev_finite_subset by blast with card_B have "P ⊨ Disj (Abs_bset (characteristic_formula ` S)) ⟷ (∃x∈?B. P ⊨ x)" by simp with ‹⋀P Q. P ∈ S ⟹ P ∼⋅ Q ⟹ Q ∈ S› show ?thesis using characteristic_formula_is_characteristic characteristic_formula_is_characteristic' logically_equivalent_def by fastforce qed end end

# Theory FS_Set

theory FS_Set imports Nominal2.Nominal2 begin section ‹Finitely Supported Sets› text ‹We define the type of finitely supported sets (over some permutation type~@{typ "'a::pt"}). Note that we cannot more generally define the (sub-)type of finitely supported elements for arbitrary permutation types~@{typ "'a::pt"}: there is no guarantee that this type is non-empty.› typedef 'a fs_set = "{x::'a::pt set. finite (supp x)}" by (simp add: exI[where x="{}"] supp_set_empty) setup_lifting type_definition_fs_set text ‹Type~@{typ "'a fs_set"} is a finitely supported permutation type.› instantiation fs_set :: (pt) pt begin lift_definition permute_fs_set :: "perm ⇒ 'a fs_set ⇒ 'a fs_set" is permute by (metis permute_finite supp_eqvt) instance apply (intro_classes) apply (metis (mono_tags) permute_fs_set.rep_eq Rep_fs_set_inverse permute_zero) apply (metis (mono_tags) permute_fs_set.rep_eq Rep_fs_set_inverse permute_plus) done end instantiation fs_set :: (pt) fs begin instance proof (intro_classes) fix x :: "'a fs_set" from Rep_fs_set have "finite (supp (Rep_fs_set x))" by simp hence "finite {a. infinite {b. (a ⇌ b) ∙ Rep_fs_set x ≠ Rep_fs_set x}}" by (unfold supp_def) hence "finite {a. infinite {b. ((a ⇌ b) ∙ x) ≠ x}}" by transfer thus "finite (supp x)" by (fold supp_def) qed end text ‹Set membership.› lift_definition member_fs_set :: "'a::pt ⇒ 'a fs_set ⇒ bool" is "(∈)" . notation member_fs_set ("'(∈⇩_{f}⇩_{s}')") and member_fs_set ("(_/ ∈⇩_{f}⇩_{s}_)" [51, 51] 50) lemma member_fs_set_permute_iff [simp]: "p ∙ x ∈⇩_{f}⇩_{s}p ∙ X ⟷ x ∈⇩_{f}⇩_{s}X" by transfer (simp add: mem_permute_iff) lemma member_fs_set_eqvt [eqvt]: "x ∈⇩_{f}⇩_{s}X ⟹ p ∙ x ∈⇩_{f}⇩_{s}p ∙ X" by simp end

# Theory FL_Transition_System

theory FL_Transition_System imports Transition_System FS_Set begin section ‹Nominal Transition Systems with Effects and \texorpdfstring{$F/L$}{F/L}-Bisimilarity› subsection ‹Nominal transition systems with effects› text ‹The paper defines an effect as a finitely supported function from states to states. It then fixes an equivariant set~@{term ℱ} of effects. In our formalization, we avoid working with such a (carrier) set, and instead introduce a type of (finitely supported) effects together with an (equivariant) application operator for effects and states. Equivariance (of the type of effects) is implicitly guaranteed (by the type of~@{const permute}). \emph{First} represents the (finitely supported) set of effects that must be observed before following a transition.› type_synonym 'eff first = "'eff fs_set" text ‹\emph{Later} is a function that represents how the set~$F$ (for \emph{first}) changes depending on the action of a transition and the chosen effect.› type_synonym ('a,'eff) later = "'a × 'eff first × 'eff ⇒ 'eff first" locale effect_nominal_ts = nominal_ts satisfies transition for satisfies :: "'state::fs ⇒ 'pred::fs ⇒ bool" (infix "⊢" 70) and transition :: "'state ⇒ ('act::bn,'state) residual ⇒ bool" (infix "→" 70) + fixes effect_apply :: "'effect::fs ⇒ 'state ⇒ 'state" ("⟨_⟩_" [0,101] 100) and L :: "('act,'effect) later" assumes effect_apply_eqvt: "eqvt effect_apply" (* using [eqvt] here generates an error message *) and L_eqvt: "eqvt L" ― ‹@{term L} is assumed to be equivariant.› (* using [eqvt] here generates an error message *) begin lemma effect_apply_eqvt_aux [simp]: "p ∙ effect_apply = effect_apply" by (metis effect_apply_eqvt eqvt_def) lemma effect_apply_eqvt' [eqvt]: "p ∙ ⟨f⟩P = ⟨p ∙ f⟩(p ∙ P)" by simp lemma L_eqvt_aux [simp]: "p ∙ L = L" by (metis L_eqvt eqvt_def) lemma L_eqvt' [eqvt]: "p ∙ L (α, P, f) = L (p ∙ α, p ∙ P, p ∙ f)" by simp end subsection ‹\texorpdfstring{$L$}{L}-bisimulations and \texorpdfstring{$F/L$}{F/L}-bisimilarity› context effect_nominal_ts begin definition is_L_bisimulation:: "('effect first ⇒ 'state ⇒ 'state ⇒ bool) ⇒ bool" where "is_L_bisimulation R ≡ ∀F. symp (R F) ∧ (∀P Q. R F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))) ∧ (∀P Q. R F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶ ⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ R (L (α,F,f)) P' Q'))))" definition FL_bisimilar :: "'effect first ⇒ 'state ⇒ 'state ⇒ bool" where "FL_bisimilar F P Q ≡ ∃R. is_L_bisimulation R ∧ (R F) P Q" abbreviation FL_bisimilar' ("_ ∼⋅[_] _" [51,0,51] 50) where "P ∼⋅[F] Q ≡ FL_bisimilar F P Q" text ‹@{term "FL_bisimilar"} is an equivariant relation, and (for every~@{term F}) an equivalence.› lemma is_L_bisimulation_eqvt [eqvt]: assumes "is_L_bisimulation R" shows "is_L_bisimulation (p ∙ R)" unfolding is_L_bisimulation_def proof (clarify) fix F have "symp ((p ∙ R) F)" (is ?S) using assms unfolding is_L_bisimulation_def by (metis eqvt_lambda symp_eqvt) moreover have "∀P Q. (p ∙ R) F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" (is ?T) proof (clarify) fix P Q f φ assume pR: "(p ∙ R) F P Q" and effect: "f ∈⇩_{f}⇩_{s}F" and satisfies: "⟨f⟩P ⊢ φ" from pR have "R (-p ∙ F) (-p ∙ P) (-p ∙ Q)" by (simp add: eqvt_lambda permute_bool_def unpermute_def) moreover have "(-p ∙ f) ∈⇩_{f}⇩_{s}(-p ∙ F)" using effect by simp moreover have "⟨-p ∙ f⟩(-p ∙ P) ⊢ -p ∙ φ" using satisfies by (metis effect_apply_eqvt' satisfies_eqvt) ultimately have "⟨-p ∙ f⟩(-p ∙ Q) ⊢ -p ∙ φ" using assms unfolding is_L_bisimulation_def by auto then show "⟨f⟩Q ⊢ φ" by (metis (full_types) effect_apply_eqvt' permute_minus_cancel(1) satisfies_eqvt) qed moreover have "∀P Q. (p ∙ R) F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶ ⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ (p ∙ R) (L (α, F, f)) P' Q')))" (is ?U) proof (clarify) fix P Q f α P' assume pR: "(p ∙ R) F P Q" and effect: "f ∈⇩_{f}⇩_{s}F" and fresh: "bn α ♯* (⟨f⟩Q, F, f)" and trans: "⟨f⟩P → ⟨α,P'⟩" from pR have "R (-p ∙ F) (-p ∙ P) (-p ∙ Q)" by (simp add: eqvt_lambda permute_bool_def unpermute_def) moreover have "(-p ∙ f) ∈⇩_{f}⇩_{s}(-p ∙ F)" using effect by simp moreover have "bn (-p ∙ α) ♯* (⟨-p ∙ f⟩(-p ∙ Q), -p ∙ F, -p ∙ f)" using fresh by (metis (full_types) effect_apply_eqvt' bn_eqvt fresh_star_Pair fresh_star_permute_iff) moreover have "⟨-p ∙ f⟩(-p ∙ P) → ⟨-p ∙ α, -p ∙ P'⟩" using trans by (metis effect_apply_eqvt' transition_eqvt') ultimately obtain Q' where T: "⟨-p ∙ f⟩(-p ∙ Q) → ⟨-p ∙ α,Q'⟩" and R: "R (L (-p ∙ α, -p ∙ F, -p ∙ f)) (-p ∙ P') Q'" using assms unfolding is_L_bisimulation_def by meson from T have "⟨f⟩Q → ⟨α, p ∙ Q'⟩" by (metis (no_types, lifting) effect_apply_eqvt' abs_residual_pair_eqvt permute_minus_cancel(1) transition_eqvt) moreover from R have "(p ∙ R) (p ∙ L (-p ∙ α, -p ∙ F, -p ∙ f)) (p ∙ -p ∙ P') (p ∙ Q')" by (metis permute_boolI permute_fun_def permute_minus_cancel(2)) then have "(p ∙ R) (L (α,F,f)) P' (p ∙ Q')" by (simp add: permute_self) ultimately show "∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ (p ∙ R) (L (α,F,f)) P' Q'" by metis qed ultimately show "?S ∧ ?T ∧ ?U" by simp qed lemma FL_bisimilar_eqvt: assumes "P ∼⋅[F] Q" shows "(p ∙ P) ∼⋅[p ∙ F] (p ∙ Q)" using assms by (metis eqvt_apply permute_boolI is_L_bisimulation_eqvt FL_bisimilar_def) lemma FL_bisimilar_reflp: "reflp (FL_bisimilar F)" proof (rule reflpI) fix x have "is_L_bisimulation (λ_. (=))" unfolding is_L_bisimulation_def by (simp add: symp_def) then show "x ∼⋅[F] x" unfolding FL_bisimilar_def by auto qed lemma FL_bisimilar_symp: "symp (FL_bisimilar F)" proof (rule sympI) fix P Q assume "P ∼⋅[F] Q" then obtain R where *: "is_L_bisimulation R ∧ R F P Q" unfolding FL_bisimilar_def .. then have "R F Q P" unfolding is_L_bisimulation_def by (simp add: symp_def) with "*" show "Q ∼⋅[F] P" unfolding FL_bisimilar_def by auto qed lemma FL_bisimilar_is_L_bisimulation: "is_L_bisimulation FL_bisimilar" unfolding is_L_bisimulation_def proof fix F have "symp (FL_bisimilar F)" (is ?R) by (fact FL_bisimilar_symp) moreover have "∀P Q. P ∼⋅[F] Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" (is ?S) by (auto simp add: is_L_bisimulation_def FL_bisimilar_def) moreover have "∀P Q. P ∼⋅[F] Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶ ⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ P' ∼⋅[L (α, F, f)] Q')))" (is ?T) by (auto simp add: is_L_bisimulation_def FL_bisimilar_def) blast ultimately show "?R ∧ ?S ∧ ?T" by metis qed lemma FL_bisimilar_simulation_step: assumes "P ∼⋅[F] Q" and "f ∈⇩_{f}⇩_{s}F" and "bn α ♯* (⟨f⟩Q, F, f)" and "⟨f⟩P → ⟨α,P'⟩" obtains Q' where "⟨f⟩Q → ⟨α,Q'⟩" and "P' ∼⋅[L (α,F,f)] Q'" using assms by (metis (poly_guards_query) FL_bisimilar_is_L_bisimulation is_L_bisimulation_def) lemma FL_bisimilar_transp: "transp (FL_bisimilar F)" proof (rule transpI) fix P Q R assume PQ: "P ∼⋅[F] Q" and QR: "Q ∼⋅[F] R" let ?FL_bisim = "λF. (FL_bisimilar F) OO (FL_bisimilar F)" have "⋀F. symp (?FL_bisim F)" proof (rule sympI) fix F P R assume "?FL_bisim F P R" then obtain Q where "P ∼⋅[F] Q" and "Q ∼⋅[F] R" by blast then have "R ∼⋅[F] Q" and "Q ∼⋅[F] P" by (metis FL_bisimilar_symp sympE)+ then show "?FL_bisim F R P" by blast qed moreover have "⋀F. ∀P Q. ?FL_bisim F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀φ. ⟨f⟩P ⊢ φ ⟶ ⟨f⟩Q ⊢ φ))" using FL_bisimilar_is_L_bisimulation is_L_bisimulation_def by auto moreover have "⋀F. ∀P Q. ?FL_bisim F P Q ⟶ (∀f. f ∈⇩_{f}⇩_{s}F ⟶ (∀α P'. bn α ♯* (⟨f⟩Q, F, f) ⟶ ⟨f⟩P → ⟨α,P'⟩ ⟶ (∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ ?FL_bisim (L (α,F,f)) P' Q')))" proof (clarify) fix F P R Q f α P' assume PR: "P ∼⋅[F] R" and RQ: "R ∼⋅[F] Q" and effect: "f ∈⇩_{f}⇩_{s}F" and fresh: "bn α ♯* (⟨f⟩Q, F, f)" and trans: "⟨f⟩P → ⟨α,P'⟩" ― ‹rename~@{term "⟨α,P'⟩"} to avoid~@{term "(⟨f⟩R, F)"}, without touching~@{term "(⟨f⟩Q, F, f)"}› obtain p where 1: "(p ∙ bn α) ♯* (⟨f⟩R, F, f)" and 2: "supp (⟨α,P'⟩, (⟨f⟩Q, F, f)) ♯* p" proof (rule at_set_avoiding2[of "bn α" "(⟨f⟩R, F, f)" "(⟨α,P'⟩, (⟨f⟩Q, F, f))", THEN exE]) show "finite (bn α)" by (fact bn_finite) next show "finite (supp (⟨f⟩R, F, f))" by (fact finite_supp) next show "finite (supp (⟨α,P'⟩, (⟨f⟩Q, F, f)))" by (simp add: finite_supp supp_Pair) next show "bn α ♯* (⟨α,P'⟩, (⟨f⟩Q, F, f))" using bn_abs_residual_fresh fresh fresh_star_Pair by blast qed metis from 2 have 3: "supp ⟨α,P'⟩ ♯* p" and 4: "supp (⟨f⟩Q, F, f) ♯* p" by (simp add: fresh_star_Un supp_Pair)+ from 3 have "⟨p ∙ α, p ∙ P'⟩ = ⟨α,P'⟩" using supp_perm_eq by fastforce then obtain pR' where 5: "⟨f⟩R → ⟨p ∙ α, pR'⟩" and 6: "(p ∙ P') ∼⋅[L (p ∙ α,F,f)] pR'" using PR effect trans 1 by (metis FL_bisimilar_simulation_step bn_eqvt) from fresh and 4 have "bn (p ∙ α) ♯* (⟨f⟩Q, F, f)" by (metis bn_eqvt fresh_star_permute_iff supp_perm_eq) then obtain pQ' where 7: "⟨f⟩Q → ⟨p ∙ α, pQ'⟩" and 8: "pR' ∼⋅[L (p ∙ α,F,f)] pQ'" using RQ effect 5 by (metis FL_bisimilar_simulation_step) from 4 have "supp (⟨f⟩Q) ♯* p" by (simp add: fresh_star_Un supp_Pair) with 7 have "⟨f⟩Q → ⟨α, -p ∙ pQ'⟩" by (metis permute_minus_cancel(2) supp_perm_eq transition_eqvt') moreover from 6 and 8 have "?FL_bisim (L (p ∙ α, F, f)) (p ∙ P') pQ'" by (metis relcompp.relcompI) then have "?FL_bisim (-p ∙ L (p ∙ α, F, f)) (-p ∙ p ∙ P') (-p ∙ pQ')" using FL_bisimilar_eqvt by blast then have "?FL_bisim (L (α, -p ∙ F, -p ∙ f)) P' (-p ∙ pQ')" by (simp add: L_eqvt') then have "?FL_bisim (L (α,F,f)) P' (-p ∙ pQ')" using 4 by (metis fresh_star_Un permute_minus_cancel(2) supp_Pair supp_perm_eq) ultimately show "∃Q'. ⟨f⟩Q → ⟨α,Q'⟩ ∧ ?FL_bisim (L (α,F,f)) P' Q'" by metis qed ultimately have "is_L_bisimulation ?FL_bisim" unfolding is_L_bisimulation_def by metis moreover have "?FL_bisim F P R" using PQ QR by blast ultimately show "P ∼⋅[F] R" unfolding FL_bisimilar_def by meson qed lemma FL_bisimilar_equivp: "equivp (FL_bisimilar F)" by (metis FL_bisimilar_reflp FL_bisimilar_symp FL_bisimilar_transp equivp_reflp_symp_transp) end end

# Theory FL_Formula

theory FL_Formula imports Nominal_Bounded_Set Nominal_Wellfounded Residual FL_Transition_System begin section ‹Infinitary Formulas With Effects› subsection ‹Infinitely branching trees› text ‹First, we define a type of trees, with a constructor~@{term tConj} that maps (potentially infinite) sets of trees into trees. To avoid paradoxes (note that there is no injection from the powerset of trees into the set of trees), the cardinality of the argument set must be bounded.› text ‹The effect consequence operator~‹⟨f⟩› is always and only used as a prefix to a predicate or an action formula. So to simplify the representation of formula trees with effects, the effect operator is merged into the predicate or action it precedes.› datatype ('idx,'pred,'act,'eff) Tree = tConj "('idx,'pred,'act,'eff) Tree set['idx]" ― ‹potentially infinite sets of trees› | tNot "('idx,'pred,'act,'eff) Tree" | tPred 'eff 'pred | tAct 'eff 'act "('idx,'pred,'act,'eff) Tree" text ‹The (automatically generated) induction principle for trees allows us to prove that the following relation over trees is well-founded. This will be useful for termination proofs when we define functions by recursion over trees.› inductive_set Tree_wf :: "('idx,'pred,'act,'eff) Tree rel" where "t ∈ set_bset tset ⟹ (t, tConj tset) ∈ Tree_wf" | "(t, tNot t) ∈ Tree_wf" | "(t, tAct f α t) ∈ Tree_wf" lemma wf_Tree_wf: "wf Tree_wf" unfolding wf_def proof (rule allI, rule impI, rule allI) fix P :: "('idx,'pred,'act,'eff) Tree ⇒ bool" and t assume "∀x. (∀y. (y, x) ∈ Tree_wf ⟶ P y) ⟶ P x" then show "P t" proof (induction t) case tConj then show ?case by (metis Tree.distinct(2) Tree.distinct(5) Tree.inject(1) Tree_wf.cases) next case tNot then show ?case by (metis Tree.distinct(1) Tree.distinct(9) Tree.inject(2) Tree_wf.cases) next case tPred then show ?case by (metis Tree.distinct(11) Tree.distinct(3) Tree.distinct(7) Tree_wf.cases) next case tAct then show ?case by (metis Tree.distinct(10) Tree.distinct(6) Tree.inject(4) Tree_wf.cases) qed qed text ‹We define a permutation operation on the type of trees.› instantiation Tree :: (type, pt, pt, pt) pt begin primrec permute_Tree :: "perm ⇒ (_,_,_,_) Tree ⇒ (_,_,_,_) Tree" where "p ∙ (tConj tset) = tConj (map_bset (permute p) tset)" ― ‹neat trick to get around the fact that~@{term tset} is not of permutation type yet› | "p ∙ (tNot t) = tNot (p ∙ t)" | "p ∙ (tPred f φ) = tPred (p ∙ f) (p ∙ φ)" | "p ∙ (tAct f α t) = tAct (p ∙ f) (p ∙ α) (p ∙ t)" instance proof fix t :: "(_,_,_,_) Tree" show "0 ∙ t = t" proof (induction t) case tConj then show ?case by (simp, transfer) (auto simp: image_def) qed simp_all next fix p q :: perm and t :: "(_,_,_,_) Tree" show "(p + q) ∙ t = p ∙ q ∙ t" proof (induction t) case tConj then show ?case by (simp, transfer) (auto simp: image_def) qed simp_all qed end text ‹Now that the type of trees---and hence the type of (bounded) sets of trees---is a permutation type, we can massage the definition of~@{term "p ∙ tConj tset"} into its more usual form.› lemma permute_Tree_tConj [simp]: "p ∙ tConj tset = tConj (p ∙ tset)" by (simp add: map_bset_permute) declare permute_Tree.simps(1) [simp del] text ‹The relation~@{const Tree_wf} is equivariant.› lemma Tree_wf_eqvt_aux: assumes "(t1, t2) ∈ Tree_wf" shows "(p ∙ t1, p ∙ t2) ∈ Tree_wf" using assms proof (induction rule: Tree_wf.induct) fix t :: "('a,'b,'c,'d) Tree" and tset :: "('a,'b,'c,'d) Tree set['a]" assume "t ∈ set_bset tset" then show "(p ∙ t, p ∙ tConj tset) ∈ Tree_wf" by (metis Tree_wf.intros(1) mem_permute_iff permute_Tree_tConj set_bset_eqvt) next fix t :: "('a,'b,'c,'d) Tree" show "(p ∙ t, p ∙ tNot t) ∈ Tree_wf" by (metis Tree_wf.intros(2) permute_Tree.simps(2)) next fix t :: "('a,'b,'c,'d) Tree" and f and α show "(p ∙ t, p ∙ tAct f α t) ∈ Tree_wf" by (metis Tree_wf.intros(3) permute_Tree.simps(4)) qed lemma Tree_wf_eqvt [eqvt, simp]: "p ∙ Tree_wf = Tree_wf" proof show "p ∙ Tree_wf ⊆ Tree_wf" by (auto simp add: permute_set_def) (rule Tree_wf_eqvt_aux) next show "Tree_wf ⊆ p ∙ Tree_wf" by (auto simp add: permute_set_def) (metis Tree_wf_eqvt_aux permute_minus_cancel(1)) qed lemma Tree_wf_eqvt': "eqvt Tree_wf" by (metis Tree_wf_eqvt eqvtI) text ‹The definition of~@{const permute} for trees gives rise to the usual notion of support. The following lemmas, one for each constructor, describe the support of trees.› lemma supp_tConj [simp]: "supp (tConj tset) = supp tset" unfolding supp_def by simp lemma supp_tNot [simp]: "supp (tNot t) = supp t" unfolding supp_def by simp lemma supp_tPred [simp]: "supp (tPred f φ) = supp f ∪ supp φ" unfolding supp_def by (simp add: Collect_imp_eq Collect_neg_eq) lemma supp_tAct [simp]: "supp (tAct f α t) = supp f ∪ supp α ∪ supp t" unfolding supp_def by (auto simp add: Collect_imp_eq Collect_neg_eq) subsection ‹Trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence› text ‹We generalize the notion of support, which considers whether a permuted element is \emph{equal} to itself, to arbitrary endorelations. This is available as @{const supp_rel} in Nominal Isabelle.› lemma supp_rel_eqvt [eqvt]: "p ∙ supp_rel R x = supp_rel (p ∙ R) (p ∙ x)" by (simp add: supp_rel_def) text ‹Usually, the definition of $\alpha$-equivalence presupposes a notion of free variables. However, the variables that are ``free'' in an infinitary conjunction are not necessarily those that are free in one of the conjuncts. For instance, consider a conjunction over \emph{all} names. Applying any permutation will yield the same conjunction, i.e., this conjunction has \emph{no} free variables. To obtain the correct notion of free variables for infinitary conjunctions, we initially defined $\alpha$-equivalence and free variables via mutual recursion. In particular, we defined the free variables of a conjunction as term @{term "fv_Tree (tConj tset) = supp_rel alpha_Tree (tConj tset)"}. We then realized that it is not necessary to define the concept of ``free variables'' at all, but the definition of $\alpha$-equivalence becomes much simpler (in particular, it is no longer mutually recursive) if we directly use the support modulo $\alpha$-equivalence.› text ‹The following lemmas and constructions are used to prove termination of our definition.› lemma supp_rel_cong [fundef_cong]: "⟦ x=x'; ⋀a b. R ((a ⇌ b) ∙ x') x' ⟷ R' ((a ⇌ b) ∙ x') x' ⟧ ⟹ supp_rel R x = supp_rel R' x'" by (simp add: supp_rel_def) lemma rel_bset_cong [fundef_cong]: "⟦ x=x'; y=y'; ⋀a b. a ∈ set_bset x' ⟹ b ∈ set_bset y' ⟹ R a b ⟷ R' a b ⟧ ⟹ rel_bset R x y ⟷ rel_bset R' x' y'" by (simp add: rel_bset_def rel_set_def) lemma alpha_set_cong [fundef_cong]: "⟦ bs=bs'; x=x'; R (p' ∙ x') y' ⟷ R' (p' ∙ x') y'; f x' = f' x'; f y' = f' y'; p=p'; cs=cs'; y=y' ⟧ ⟹ alpha_set (bs, x) R f p (cs, y) ⟷ alpha_set (bs', x') R' f' p' (cs', y')" by (simp add: alpha_set) quotient_type ('idx,'pred,'act,'eff) Tree⇩_{p}= "('idx,'pred::pt,'act::bn,'eff::fs) Tree" / "hull_relp" by (fact hull_relp_equivp) lemma abs_Tree⇩_{p}_eq [simp]: "abs_Tree⇩_{p}(p ∙ t) = abs_Tree⇩_{p}t" by (metis hull_relp.simps Tree⇩_{p}.abs_eq_iff) lemma permute_rep_abs_Tree⇩_{p}: obtains p where "rep_Tree⇩_{p}(abs_Tree⇩_{p}t) = p ∙ t" by (metis Quotient3_Tree⇩_{p}Tree⇩_{p}.abs_eq_iff rep_abs_rsp hull_relp.simps) lift_definition Tree_wf⇩_{p}:: "('idx,'pred::pt,'act::bn,'eff::fs) Tree⇩_{p}rel" is Tree_wf . lemma Tree_wf⇩_{p}I [simp]: assumes "(a, b) ∈ Tree_wf" shows "(abs_Tree⇩_{p}(p ∙ a), abs_Tree⇩_{p}b) ∈ Tree_wf⇩_{p}" using assms by (metis (erased, lifting) Tree⇩_{p}.abs_eq_iff Tree_wf⇩_{p}.abs_eq hull_relp.intros map_prod_simp rev_image_eqI) lemma Tree_wf⇩_{p}_trivialI [simp]: assumes "(a, b) ∈ Tree_wf" shows "(abs_Tree⇩_{p}a, abs_Tree⇩_{p}b) ∈ Tree_wf⇩_{p}" using assms by (metis Tree_wf⇩_{p}I permute_zero) lemma Tree_wf⇩_{p}E: assumes "(a⇩_{p}, b⇩_{p}) ∈ Tree_wf⇩_{p}" obtains a b where "a⇩_{p}= abs_Tree⇩_{p}a" and "b⇩_{p}= abs_Tree⇩_{p}b" and "(a,b) ∈ Tree_wf" using assms by (metis (erased, lifting) Pair_inject Tree_wf⇩_{p}.abs_eq prod_fun_imageE) (* DIFF *) lemma wf_Tree_wf⇩_{p}: "wf Tree_wf⇩_{p}" apply (rule wf_subset[of "inv_image (hull_rel O Tree_wf) rep_Tree⇩_{p}"]) apply (metis Tree_wf_eqvt' wf_Tree_wf wf_hull_rel_relcomp wf_inv_image) apply (auto elim!: Tree_wf⇩_{p}E) apply (rename_tac t1 t2) apply (rule_tac t=t1 in permute_rep_abs_Tree⇩_{p}) apply (rule_tac t=t2 in permute_rep_abs_Tree⇩_{p}) apply (rename_tac p1 p2) apply (subgoal_tac "(p2 ∙ t1, p2 ∙ t2) ∈ Tree_wf") apply (subgoal_tac "(p1 ∙ t1, p2 ∙ t1) ∈ hull_rel") apply (metis relcomp.relcompI) apply (metis hull_rel.simps permute_minus_cancel(2) permute_plus) apply (metis Tree_wf_eqvt_aux) done fun alpha_Tree_termination :: "('a, 'b, 'c, 'd) Tree × ('a, 'b, 'c, 'd) Tree ⇒ ('a, 'b::pt, 'c::bn, 'd::fs) Tree⇩_{p}set" where "alpha_Tree_termination (t1, t2) = {abs_Tree⇩_{p}t1, abs_Tree⇩_{p}t2}" text ‹Here it comes \ldots› function (sequential) alpha_Tree :: "('idx,'pred::pt,'act::bn,'eff::fs) Tree ⇒ ('idx,'pred,'act,'eff) Tree ⇒ bool" (infix "=⇩_{α}" 50) where ― ‹@{const alpha_Tree}› alpha_tConj: "tConj tset1 =⇩_{α}tConj tset2 ⟷ rel_bset alpha_Tree tset1 tset2" | alpha_tNot: "tNot t1 =⇩_{α}tNot t2 ⟷ t1 =⇩_{α}t2" | alpha_tPred: "tPred f1 φ1 =⇩_{α}tPred f2 φ2 ⟷ f1 = f2 ∧ φ1 = φ2" ― ‹the action may have binding names› | alpha_tAct: "tAct f1 α1 t1 =⇩_{α}tAct f2 α2 t2 ⟷ f1 = f2 ∧ (∃p. (bn α1, t1) ≈set alpha_Tree (supp_rel alpha_Tree) p (bn α2, t2) ∧ (bn α1, α1) ≈set ((=)) supp p (bn α2, α2))" | alpha_other: "_ =⇩_{α}_ ⟷ False" ― ‹254 subgoals (!)› by pat_completeness auto termination proof let ?R = "inv_image (max_ext Tree_wf⇩_{p}) alpha_Tree_termination" show "wf ?R" by (metis max_ext_wf wf_Tree_wf⇩_{p}wf_inv_image) qed (auto simp add: max_ext.simps Tree_wf.simps simp del: permute_Tree_tConj) text ‹We provide more descriptive case names for the automatically generated induction principle, and specialize it to an induction rule for $\alpha$-equivalence.› lemmas alpha_Tree_induct' = alpha_Tree.induct[case_names alpha_tConj alpha_tNot alpha_tPred alpha_tAct "alpha_other(1)" "alpha_other(2)" "alpha_other(3)" "alpha_other(4)" "alpha_other(5)" "alpha_other(6)" "alpha_other(7)" "alpha_other(8)" "alpha_other(9)" "alpha_other(10)" "alpha_other(11)" "alpha_other(12)" "alpha_other(13)" "alpha_other(14)" "alpha_other(15)" "alpha_other(16)" "alpha_other(17)" "alpha_other(18)"] lemma alpha_Tree_induct[case_names tConj tNot tPred tAct, consumes 1]: assumes "t1 =⇩_{α}t2" and "⋀tset1 tset2. (⋀a b. a ∈ set_bset tset1 ⟹ b ∈ set_bset tset2 ⟹ a =⇩_{α}b ⟹ P a b) ⟹ rel_bset (=⇩_{α}) tset1 tset2 ⟹ P (tConj tset1) (tConj tset2)" and "⋀t1 t2. t1 =⇩_{α}t2 ⟹ P t1 t2 ⟹ P (tNot t1) (tNot t2)" and "⋀f φ. P (tPred f φ) (tPred f φ)" and "⋀f1 α1 t1 f2 α2 t2. (⋀p. p ∙ t1 =⇩_{α}t2 ⟹ P (p ∙ t1) t2) ⟹ f1 = f2 ⟹ (∃p. (bn α1, t1) ≈set (=⇩_{α}) (supp_rel (=⇩_{α})) p (bn α2, t2) ∧ (bn α1, α1) ≈set (=) supp p (bn α2, α2)) ⟹ P (tAct f1 α1 t1) (tAct f2 α2 t2)" shows "P t1 t2" using assms by (induction t1 t2 rule: alpha_Tree.induct) simp_all text ‹$\alpha$-equivalence is equivariant.› lemma alpha_Tree_eqvt_aux: assumes "⋀a b. (a ⇌ b) ∙ t =⇩_{α}t ⟷ p ∙ (a ⇌ b) ∙ t =⇩_{α}p ∙ t" shows "p ∙ supp_rel (=⇩_{α}) t = supp_rel (=⇩_{α}) (p ∙ t)" proof - { fix a let ?B = "{b. ¬ ((a ⇌ b) ∙ t) =⇩_{α}t}" let ?pB =