theory FL_Validity imports FL_Transition_System FL_Formula begin section ‹Validity With Effects› text ‹The following is needed to prove termination of~@{term FL_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 :: "('e, 'f, 'g, 'h) Tree × ('e, 'f, 'g, 'h) 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 :: "('e,'f,'g,'h) Tree set['e]" 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 f α t assume *: "(x1,t) ∈ hull_rel" and **: "(tAct f α t, x4) ∈ alpha_Tree_rel" from "*" obtain p where x1: "x1 = p ∙ t" using hull_rel.cases by blast from "**" have "tAct f α t =⇩_{α}x4" by (rule alpha_Tree_relE) then obtain q t' where x4: "x4 = tAct f (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 effect_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 (sequential) FL_valid_Tree :: "'state ⇒ ('idx,'pred,'act,'effect) Tree ⇒ bool" where "FL_valid_Tree P (tConj tset) ⟷ (∀t∈set_bset tset. FL_valid_Tree P t)" | "FL_valid_Tree P (tNot t) ⟷ ¬ FL_valid_Tree P t" | "FL_valid_Tree P (tPred f φ) ⟷ ⟨f⟩P ⊢ φ" | "FL_valid_Tree P (tAct f α t) ⟷ (∃α' t' P'. tAct f α t =⇩_{α}tAct f α' t' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ FL_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,'effect) 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,'effect) Tree" show "((P, t), (P, tNot t)) ∈ ?R" by (simp add: Tree_wf.intros(2)) next fix P1 P2 :: 'state and f and α1 α2 and t1 t2 :: "('idx,'pred,'act,'effect) Tree" assume "tAct f α1 t1 =⇩_{α}tAct f α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 f α1 t1)) ∈ ?R" by (simp add: Tree_wf.intros(3)) } qed text ‹@{const FL_valid_Tree} is equivariant.› lemma FL_valid_Tree_eqvt': "FL_valid_Tree P t ⟷ FL_valid_Tree (p ∙ P) (p ∙ t)" proof (induction P t rule: FL_valid_Tree.induct) case (1 P tset) show ?case proof assume *: "FL_valid_Tree P (tConj tset)" { fix t assume "t ∈ p ∙ set_bset tset" with "1.IH" and "*" have "FL_valid_Tree (p ∙ P) t" by (metis (no_types, lifting) imageE permute_set_eq_image FL_valid_Tree.simps(1)) } then show "FL_valid_Tree (p ∙ P) (p ∙ tConj tset)" by simp next assume *: "FL_valid_Tree (p ∙ P) (p ∙ tConj tset)" { fix t assume "t ∈ set_bset tset" with "1.IH" and "*" have "FL_valid_Tree P t" by (metis mem_permute_iff permute_Tree_tConj set_bset_eqvt FL_valid_Tree.simps(1)) } then show "FL_valid_Tree P (tConj tset)" by simp qed next case 2 then show ?case by simp next case 3 show ?case by simp (metis effect_apply_eqvt' permute_minus_cancel(2) satisfies_eqvt) next case (4 P f α t) show ?case proof assume "FL_valid_Tree P (tAct f α t)" then obtain α' t' P' where *: "tAct f α t =⇩_{α}tAct f α' t' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ FL_valid_Tree P' t'" by auto with "4.IH" have "FL_valid_Tree (p ∙ P') (p ∙ t')" by blast moreover from "*" have "p ∙ ⟨f⟩P → ⟨p ∙ α', p ∙ P'⟩" by (metis transition_eqvt') moreover from "*" have "p ∙ tAct f α t =⇩_{α}tAct (p ∙ f) (p ∙ α') (p ∙ t')" by (metis alpha_Tree_eqvt permute_Tree.simps(4)) ultimately show "FL_valid_Tree (p ∙ P) (p ∙ tAct f α t)" by auto next assume "FL_valid_Tree (p ∙ P) (p ∙ tAct f α t)" then obtain α' t' P' where *: "p ∙ tAct f α t =⇩_{α}tAct (p ∙ f) α' t' ∧ (p ∙ ⟨f⟩P) → ⟨α',P'⟩ ∧ FL_valid_Tree P' t'" by auto then have eq: "tAct f α t =⇩_{α}tAct f (-p ∙ α') (-p ∙ t')" by (metis alpha_Tree_eqvt permute_Tree.simps(4) permute_minus_cancel(2)) moreover from "*" have "⟨f⟩P → ⟨-p ∙ α', -p ∙ P'⟩" by (metis permute_minus_cancel(2) transition_eqvt') moreover with "4.IH" have "FL_valid_Tree (-p ∙ P') (-p ∙ t')" using eq and "*" by simp ultimately show "FL_valid_Tree P (tAct f α t)" by auto qed qed lemma FL_valid_Tree_eqvt [eqvt]: assumes "FL_valid_Tree P t" shows "FL_valid_Tree (p ∙ P) (p ∙ t)" using assms by (metis FL_valid_Tree_eqvt') text ‹$\alpha$-equivalent trees validate the same states.› lemma alpha_Tree_FL_valid_Tree: assumes "t1 =⇩_{α}t2" shows "FL_valid_Tree P t1 ⟷ FL_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 f1 α1 t1 f2 α2 t2) show ?case proof assume "FL_valid_Tree P (tAct f1 α1 t1)" then obtain α' t' P' where "tAct f1 α1 t1 =⇩_{α}tAct f1 α' t' ∧ ⟨f1⟩P → ⟨α',P'⟩ ∧ FL_valid_Tree P' t'" by auto moreover from tAct.hyps have "tAct f1 α1 t1 =⇩_{α}tAct f2 α2 t2" using alpha_tAct by blast ultimately show "FL_valid_Tree P (tAct f2 α2 t2)" using tAct.hyps by (metis Tree⇩_{α}.abs_eq_iff FL_valid_Tree.simps(4)) next assume "FL_valid_Tree P (tAct f2 α2 t2)" then obtain α' t' P' where "tAct f2 α2 t2 =⇩_{α}tAct f2 α' t' ∧ ⟨f2⟩P → ⟨α',P'⟩ ∧ FL_valid_Tree P' t'" by auto moreover from tAct.hyps have "tAct f1 α1 t1 =⇩_{α}tAct f2 α2 t2" using alpha_tAct by blast ultimately show "FL_valid_Tree P (tAct f1 α1 t1)" using tAct.hyps by (metis Tree⇩_{α}.abs_eq_iff FL_valid_Tree.simps(4)) qed qed simp_all subsection ‹Validity for trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence› lift_definition FL_valid_Tree⇩_{α}:: "'state ⇒ ('idx,'pred,'act,'effect) Tree⇩_{α}⇒ bool" is FL_valid_Tree by (fact alpha_Tree_FL_valid_Tree) lemma FL_valid_Tree⇩_{α}_eqvt [eqvt]: assumes "FL_valid_Tree⇩_{α}P t" shows "FL_valid_Tree⇩_{α}(p ∙ P) (p ∙ t)" using assms by transfer (fact FL_valid_Tree_eqvt) lemma FL_valid_Tree⇩_{α}_Conj⇩_{α}[simp]: "FL_valid_Tree⇩_{α}P (Conj⇩_{α}tset⇩_{α}) ⟷ (∀t⇩_{α}∈set_bset tset⇩_{α}. FL_valid_Tree⇩_{α}P t⇩_{α})" proof - have "FL_valid_Tree P (rep_Tree⇩_{α}(abs_Tree⇩_{α}(tConj (map_bset rep_Tree⇩_{α}tset⇩_{α})))) ⟷ FL_valid_Tree P (tConj (map_bset rep_Tree⇩_{α}tset⇩_{α}))" by (metis Tree⇩_{α}_rep_abs alpha_Tree_FL_valid_Tree) then show ?thesis by (simp add: FL_valid_Tree⇩_{α}_def Conj⇩_{α}_def map_bset.rep_eq) qed lemma FL_valid_Tree⇩_{α}_Not⇩_{α}[simp]: "FL_valid_Tree⇩_{α}P (Not⇩_{α}t⇩_{α}) ⟷ ¬ FL_valid_Tree⇩_{α}P t⇩_{α}" by transfer simp lemma FL_valid_Tree⇩_{α}_Pred⇩_{α}[simp]: "FL_valid_Tree⇩_{α}P (Pred⇩_{α}f φ) ⟷ ⟨f⟩P ⊢ φ" by transfer simp lemma FL_valid_Tree⇩_{α}_Act⇩_{α}[simp]: "FL_valid_Tree⇩_{α}P (Act⇩_{α}f α t⇩_{α}) ⟷ (∃α' t⇩_{α}' P'. Act⇩_{α}f α t⇩_{α}= Act⇩_{α}f α' t⇩_{α}' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ FL_valid_Tree⇩_{α}P' t⇩_{α}')" proof assume "FL_valid_Tree⇩_{α}P (Act⇩_{α}f α t⇩_{α})" moreover have "Act⇩_{α}f α t⇩_{α}= abs_Tree⇩_{α}(tAct f α (rep_Tree⇩_{α}t⇩_{α}))" by (metis Act⇩_{α}.abs_eq Tree⇩_{α}_abs_rep) ultimately show "∃α' t⇩_{α}' P'. Act⇩_{α}f α t⇩_{α}= Act⇩_{α}f α' t⇩_{α}' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ FL_valid_Tree⇩_{α}P' t⇩_{α}'" by (metis Act⇩_{α}.abs_eq Tree⇩_{α}.abs_eq_iff FL_valid_Tree.simps(4) FL_valid_Tree⇩_{α}.abs_eq) next assume "∃α' t⇩_{α}' P'. Act⇩_{α}f α t⇩_{α}= Act⇩_{α}f α' t⇩_{α}' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ FL_valid_Tree⇩_{α}P' t⇩_{α}'" moreover have "⋀α' t⇩_{α}'. Act⇩_{α}f α' t⇩_{α}' = abs_Tree⇩_{α}(tAct f α' (rep_Tree⇩_{α}t⇩_{α}'))" by (metis Act⇩_{α}.abs_eq Tree⇩_{α}_abs_rep) ultimately show "FL_valid_Tree⇩_{α}P (Act⇩_{α}f α t⇩_{α})" by (metis Tree⇩_{α}.abs_eq_iff FL_valid_Tree.simps(4) FL_valid_Tree⇩_{α}.abs_eq FL_valid_Tree⇩_{α}.rep_eq) qed subsection ‹Validity for infinitary formulas› lift_definition FL_valid :: "'state ⇒ ('idx,'pred,'act,'effect) formula ⇒ bool" (infix "⊨" 70) is FL_valid_Tree⇩_{α}. lemma FL_valid_eqvt [eqvt]: assumes "P ⊨ x" shows "(p ∙ P) ⊨ (p ∙ x)" using assms by transfer (metis FL_valid_Tree⇩_{α}_eqvt) lemma FL_valid_Conj [simp]: assumes "finite (supp xset)" shows "P ⊨ Conj xset ⟷ (∀x∈set_bset xset. P ⊨ x)" using assms by (simp add: FL_valid_def Conj_def map_bset.rep_eq) lemma FL_valid_Not [simp]: "P ⊨ Not x ⟷ ¬ P ⊨ x" by transfer simp lemma FL_valid_Pred [simp]: "P ⊨ Pred f φ ⟷ ⟨f⟩P ⊢ φ" by transfer simp lemma FL_valid_Act: "P ⊨ Act f α x ⟷ (∃α' x' P'. Act f α x = Act f α' x' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ P' ⊨ x')" proof assume "P ⊨ Act f α x" moreover have "Rep_formula (Abs_formula (Act⇩_{α}f α (Rep_formula x))) = Act⇩_{α}f α (Rep_formula x)" by (metis Act.rep_eq Rep_formula_inverse) ultimately show "∃α' x' P'. Act f α x = Act f α' x' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ P' ⊨ x'" by (auto simp add: FL_valid_def Act_def) (metis Abs_formula_inverse Rep_formula' hereditarily_fs_alpha_renaming) next assume "∃α' x' P'. Act f α x = Act f α' x' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ P' ⊨ x'" then show "P ⊨ Act f α x" by (metis Act.rep_eq FL_valid.rep_eq FL_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 FL_valid_Act_strong: assumes "finite (supp X)" shows "P ⊨ Act f α x ⟷ (∃α' x' P'. Act f α x = Act f α' x' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ P' ⊨ x' ∧ bn α' ♯* X)" proof assume "P ⊨ Act f α x" then obtain α' x' P' where eq: "Act f α x = Act f α' x'" and trans: "⟨f⟩P → ⟨α',P'⟩" and valid: "P' ⊨ x'" by (metis FL_valid_Act) have "finite (bn α')" by (fact bn_finite) moreover note ‹finite (supp X)› moreover have "finite (supp (supp x' - bn α', supp α' - bn α', ⟨α',P'⟩))" by (simp add: supp_Pair finite_sets_supp finite_supp) moreover have "bn α' ♯* (supp x' - bn α', supp α' - bn α', ⟨α',P'⟩)" by (simp add: atom_fresh_star_disjoint finite_supp fresh_star_Pair) ultimately obtain p where fresh_X: "(p ∙ bn α') ♯* X" and fresh_p: "supp (supp x' - bn α', supp α' - bn α', ⟨α',P'⟩) ♯* p" by (metis at_set_avoiding2) from fresh_p have "supp (supp x' - bn α') ♯* p" and "supp (supp α' - bn α') ♯* p" and 1: "supp ⟨α',P'⟩ ♯* p" by (meson fresh_Pair fresh_def fresh_star_def)+ then have 2: "(supp x' - bn α') ♯* p" and 3: "(supp α' - bn α') ♯* p" by (simp add: finite_supp supp_finite_atom_set)+ moreover from 2 have "supp (p ∙ x') - bn (p ∙ α') = supp x' - bn α'" by (metis Diff_eqvt atom_set_perm_eq bn_eqvt supp_eqvt) moreover from 3 have "supp (p ∙ α') - bn (p ∙ α') = supp α' - bn α'" by (metis (no_types, opaque_lifting) Diff_eqvt atom_set_perm_eq bn_eqvt supp_eqvt) ultimately have "Act f α' x' = Act f (p ∙ α') (p ∙ x')" by (auto simp add: Act_eq_iff_perm) moreover from 1 have "⟨p ∙ α', p ∙ P'⟩ = ⟨α',P'⟩" by (metis abs_residual_pair_eqvt supp_perm_eq) ultimately show "∃α' x' P'. Act f α x = Act f α' x' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ P' ⊨ x' ∧ bn α' ♯* X" using eq and trans and valid and fresh_X by (metis bn_eqvt FL_valid_eqvt) next assume "∃α' x' P'. Act f α x = Act f α' x' ∧ ⟨f⟩P → ⟨α',P'⟩ ∧ P' ⊨ x' ∧ bn α' ♯* X" then show "P ⊨ Act f α x" by (metis FL_valid_Act) qed lemma FL_valid_Act_fresh: assumes "bn α ♯* ⟨f⟩P" shows "P ⊨ Act f α x ⟷ (∃P'. ⟨f⟩P → ⟨α,P'⟩ ∧ P' ⊨ x)" proof assume "P ⊨ Act f α x" moreover have "finite (supp (⟨f⟩P))" by (fact finite_supp) ultimately obtain α' x' P' where eq: "Act f α x = Act f α' x'" and trans: "⟨f⟩P → ⟨α',P'⟩" and valid: "P' ⊨ x'" and fresh: "bn α' ♯* ⟨f⟩P" by (metis FL_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 α) ♯* ⟨f⟩P" using p_α by (metis bn_eqvt fresh_star_Un) then have "supp p ♯* ⟨f⟩P" using supp_p by (metis fresh_star_def subset_eq) then have p_P: "-p ∙ ⟨f⟩P = ⟨f⟩P" by (metis perm_supp_eq supp_minus_perm) from trans have "⟨f⟩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) FL_valid_eqvt) ultimately show "∃P'. ⟨f⟩P → ⟨α,P'⟩ ∧ P' ⊨ x" by meson next assume "∃P'. ⟨f⟩P → ⟨α,P'⟩ ∧ P' ⊨ x" then show "P ⊨ Act f α x" by (metis FL_valid_Act) qed end end