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