theory Weak_Formula imports Weak_Transition_System Disjunction begin section ‹Weak Formulas› subsection ‹Lemmas about \texorpdfstring{$\alpha$}{alpha}-equivalence involving \texorpdfstring{$\tau$}{tau}› context weak_nominal_ts begin lemma Act_tau_eq_iff [simp]: "Act τ x1 = Act α x2 ⟷ α = τ ∧ x2 = x1" (is "?l ⟷ ?r") proof assume "?l" then obtain p where p_α: "p ∙ τ = α" and p_x: "p ∙ x1 = x2" and fresh: "(supp x1 - bn τ) ♯* p" by (metis Act_eq_iff_perm) from p_α have "α = τ" by (metis tau_eqvt) moreover from fresh and p_x have "x2 = x1" by (simp add: supp_perm_eq) ultimately show "?r" .. next assume "?r" then show "?l" by simp qed end subsection ‹Weak action modality› text ‹The definition of (strong) formulas is parametric in the index type, but from now on we want to work with a fixed (sufficiently large) index type. Also, we use~@{term τ} in our definition of weak formulas.› locale indexed_weak_nominal_ts = weak_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|" and card_idx_nat: "|UNIV::nat set| <o |UNIV::'idx set|" begin text ‹The assumption @{thm card_idx_nat} is redundant: it is already implied by @{thm card_idx_perm}. A formal proof of this fact is left for future work.› lemma card_idx_nat' [simp]: "|UNIV::nat set| <o natLeq +c |UNIV::'idx set|" proof - note card_idx_nat also have "|UNIV :: 'idx set| ≤o natLeq +c |UNIV :: 'idx set|" by (metis Cnotzero_UNIV ordLeq_csum2) finally show ?thesis . qed primrec tau_steps :: "('idx,'pred::fs,'act::bn) formula ⇒ nat ⇒ ('idx,'pred,'act) formula" where "tau_steps x 0 = x" | "tau_steps x (Suc n) = Act τ (tau_steps x n)" lemma tau_steps_eqvt (*[eqvt]*) [simp]: "p ∙ tau_steps x n = tau_steps (p ∙ x) (p ∙ n)" by (induct n) (simp_all add: permute_nat_def tau_eqvt) lemma tau_steps_eqvt' [simp]: "p ∙ tau_steps x = tau_steps (p ∙ x)" by (simp add: permute_fun_def) lemma tau_steps_eqvt_raw [simp]: "p ∙ tau_steps = tau_steps" by (simp add: permute_fun_def) lemma tau_steps_add [simp]: "tau_steps (tau_steps x m) n = tau_steps x (m + n)" by (induct n) auto lemma tau_steps_not_self: "x = tau_steps x n ⟷ n = 0" proof assume "x = tau_steps x n" then show "n = 0" proof (induct n arbitrary: x) case 0 show ?case .. next case (Suc n) then have "x = Act τ (tau_steps x n)" by simp then show "Suc n = 0" proof (induct x) case (Act α x) then have "x = tau_steps (Act τ x) n" by (metis Act_tau_eq_iff) with Act.hyps show ?thesis by (metis add_Suc tau_steps.simps(2) tau_steps_add) qed simp_all qed next assume "n = 0" then show "x = tau_steps x n" by simp qed definition weak_tau_modality :: "('idx,'pred::fs,'act::bn) formula ⇒ ('idx,'pred,'act) formula" where "weak_tau_modality x ≡ Disj (map_bset (tau_steps x) (Abs_bset UNIV))" lemma finite_supp_map_bset_tau_steps [simp]: "finite (supp (map_bset (tau_steps x) (Abs_bset UNIV :: nat set['idx])))" proof - have "eqvt map_bset" and "eqvt tau_steps" by (simp add: eqvtI)+ then have "supp (map_bset (tau_steps x)) ⊆ supp x" using supp_fun_eqvt supp_fun_app supp_fun_app_eqvt by blast moreover have "supp (Abs_bset UNIV :: nat set['idx]) = {}" by (simp add: eqvtI supp_fun_eqvt) ultimately have "supp (map_bset (tau_steps x) (Abs_bset UNIV :: nat set['idx])) ⊆ supp x" using supp_fun_app by blast then show ?thesis by (metis finite_subset finite_supp) qed lemma weak_tau_modality_eqvt (*[eqvt]*) [simp]: "p ∙ weak_tau_modality x = weak_tau_modality (p ∙ x)" unfolding weak_tau_modality_def by (simp add: map_bset_eqvt) lemma weak_tau_modality_eq_iff [simp]: "weak_tau_modality x = weak_tau_modality y ⟷ x = y" proof assume "weak_tau_modality x = weak_tau_modality y" then have "map_bset (tau_steps x) (Abs_bset UNIV :: _ set['idx]) = map_bset (tau_steps y) (Abs_bset UNIV)" unfolding weak_tau_modality_def by simp with card_idx_nat' have "range (tau_steps x) = range (tau_steps y)" (is "?X = ?Y") by (metis Abs_bset_inverse' map_bset.rep_eq) then have "x ∈ range (tau_steps y)" and "y ∈ range (tau_steps x)" by (metis range_eqI tau_steps.simps(1))+ then obtain nx ny where x: "x = tau_steps y nx" and y: "y = tau_steps x ny" by blast then have "ny + nx = 0" by (simp add: tau_steps_not_self) with x and y show "x = y" by simp next assume "x = y" then show "weak_tau_modality x = weak_tau_modality y" by simp qed lemma supp_weak_tau_modality [simp]: "supp (weak_tau_modality x) = supp x" unfolding supp_def by simp lemma Act_weak_tau_modality_eq_iff [simp]: "Act α1 (weak_tau_modality x1) = Act α2 (weak_tau_modality x2) ⟷ Act α1 x1 = Act α2 x2" by (simp add: Act_eq_iff_perm) definition weak_action_modality :: "'act ⇒ ('idx,'pred::fs,'act::bn) formula ⇒ ('idx,'pred,'act) formula" ("⟨⟨_⟩⟩_") where "⟨⟨α⟩⟩x ≡ if α = τ then weak_tau_modality x else weak_tau_modality (Act α (weak_tau_modality x))" lemma weak_action_modality_eqvt (*[eqvt]*) [simp]: "p ∙ (⟨⟨α⟩⟩x) = ⟨⟨p ∙ α⟩⟩(p ∙ x)" using tau_eqvt weak_action_modality_def by fastforce lemma weak_action_modality_tau: "(⟨⟨τ⟩⟩x) = weak_tau_modality x" unfolding weak_action_modality_def by simp lemma weak_action_modality_not_tau: assumes "α ≠ τ" shows "(⟨⟨α⟩⟩x) = weak_tau_modality (Act α (weak_tau_modality x))" using assms unfolding weak_action_modality_def by simp text ‹Equality is modulo $\alpha$-equivalence.› text ‹Note that the converse of the following lemma does not hold. For instance, for~@{prop "α ≠ τ"} we have @{prop "(⟨⟨τ⟩⟩(Act α (weak_tau_modality x))) = ⟨⟨α⟩⟩x"} by definition, but clearly not @{prop "Act τ (Act α (weak_tau_modality x)) = Act α x"}.› lemma weak_action_modality_eq: assumes "Act α1 x1 = Act α2 x2" shows "(⟨⟨α1⟩⟩x1) = (⟨⟨α2⟩⟩x2)" proof (cases "α1 = τ") case True with assms have "α2 = α1 ∧ x2 = x1" by (metis Act_tau_eq_iff) then show ?thesis by simp next case False from assms 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 Act_eq_iff_perm) from 1 have "supp (weak_tau_modality x1) - bn α1 = supp (weak_tau_modality x2) - bn α2" by (metis supp_weak_tau_modality) moreover from 2 have "(supp (weak_tau_modality x1) - bn α1) ♯* p" by (metis supp_weak_tau_modality) moreover from 3 have "p ∙ weak_tau_modality x1 = weak_tau_modality x2" by (metis weak_tau_modality_eqvt) ultimately have "Act α1 (weak_tau_modality x1) = Act α2 (weak_tau_modality x2)" using 4 and 5 and 6 and Act_eq_iff_perm by blast moreover from ‹α1 ≠ τ› and assms have "α2 ≠ τ" by (metis Act_tau_eq_iff) ultimately show ?thesis using ‹α1 ≠ τ› by (simp add: weak_action_modality_not_tau) qed subsection ‹Weak formulas› inductive weak_formula :: "('idx,'pred::fs,'act::bn) formula ⇒ bool" where wf_Conj: "finite (supp xset) ⟹ (⋀x. x ∈ set_bset xset ⟹ weak_formula x) ⟹ weak_formula (Conj xset)" | wf_Not: "weak_formula x ⟹ weak_formula (Not x)" | wf_Act: "weak_formula x ⟹ weak_formula (⟨⟨α⟩⟩x)" | wf_Pred: "weak_formula x ⟹ weak_formula (⟨⟨τ⟩⟩(Conj (binsert (Pred φ) (bsingleton x))))" lemma finite_supp_wf_Pred [simp]: "finite (supp (binsert (Pred φ) (bsingleton x)))" proof - have "supp (bsingleton x) ⊆ supp x" by (simp add: eqvtI supp_fun_app_eqvt) moreover have "eqvt binsert" by (simp add: eqvtI) ultimately have "supp (binsert (Pred φ) (bsingleton x)) ⊆ supp φ ∪ supp x" using supp_fun_app supp_fun_app_eqvt by fastforce then show ?thesis by (metis finite_UnI finite_supp rev_finite_subset) qed text ‹@{const weak_formula} is equivariant.› lemma weak_formula_eqvt (*[eqvt]*) [simp]: "weak_formula x ⟹ weak_formula (p ∙ x)" proof (induct rule: weak_formula.induct) case (wf_Conj xset) then show ?case by simp (metis (no_types, lifting) imageE permute_finite permute_set_eq_image set_bset_eqvt supp_eqvt weak_formula.wf_Conj) next case (wf_Not x) then show ?case by (simp add: weak_formula.wf_Not) next case (wf_Act x α) then show ?case by (simp add: weak_formula.wf_Act) next case (wf_Pred x φ) then show ?case by (simp add: tau_eqvt weak_formula.wf_Pred) qed end end