Theory FL_Validity

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