# Theory Weak_Formula

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"
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)"

lemma tau_steps_eqvt_raw [simp]:
"p ∙ tau_steps = tau_steps"

"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
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"
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]) = {}"
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"
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"

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"
moreover have "eqvt binsert"
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