# Theory Validity

theory Validity
imports
Transition_System
Formula
begin

section ‹Validity›

text ‹The following is needed to prove termination of~@{term 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 :: "('d, 'e, 'f) Tree × ('d, 'e, 'f) 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 :: "('d,'e,'f) Tree set['d]"
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"
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 α t
assume *: "(x1,t) ∈ hull_rel" and **: "(tAct α t, x4) ∈ alpha_Tree_rel"
from "*" obtain p where x1: "x1 = p ∙ t"
using hull_rel.cases by blast
from "**" have "tAct α t =⇩α x4"
by (rule alpha_Tree_relE)
then obtain q t' where x4: "x4 = tAct (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"
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 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 valid_Tree :: "'state ⇒ ('idx,'pred,'act) Tree ⇒ bool" where
"valid_Tree P (tConj tset) ⟷ (∀t∈set_bset tset. valid_Tree P t)"
| "valid_Tree P (tNot t) ⟷ ¬ valid_Tree P t"
| "valid_Tree P (tPred φ) ⟷ P ⊢ φ"
| "valid_Tree P (tAct α t) ⟷ (∃α' t' P'. tAct α t =⇩α tAct α' t' ∧ P → ⟨α',P'⟩ ∧ 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) Tree set['idx]" and t
assume "t ∈ set_bset tset" then show "((P, t), (P, tConj tset)) ∈ ?R"
next
fix P :: 'state and t :: "('idx,'pred,'act) Tree"
show "((P, t), (P, tNot t)) ∈ ?R"
next
fix P1 P2 :: 'state and α1 α2 :: 'act and t1 t2 :: "('idx,'pred,'act) Tree"
assume "tAct α1 t1 =⇩α tAct α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 α1 t1)) ∈ ?R"
}
qed

text ‹@{const valid_Tree} is equivariant.›

lemma valid_Tree_eqvt': "valid_Tree P t ⟷ valid_Tree (p ∙ P) (p ∙ t)"
proof (induction P t rule: valid_Tree.induct)
case (1 P tset) show ?case
proof
assume *: "valid_Tree P (tConj tset)"
{
fix t
assume "t ∈ p ∙ set_bset tset"
with "1.IH" and "*" have "valid_Tree (p ∙ P) t"
by (metis (no_types, lifting) imageE permute_set_eq_image valid_Tree.simps(1))
}
then show "valid_Tree (p ∙ P) (p ∙ tConj tset)"
by simp
next
assume *: "valid_Tree (p ∙ P) (p ∙ tConj tset)"
{
fix t
assume "t ∈ set_bset tset"
with "1.IH" and "*" have "valid_Tree P t"
by (metis mem_permute_iff permute_Tree_tConj set_bset_eqvt valid_Tree.simps(1))
}
then show "valid_Tree P (tConj tset)"
by simp
qed
next
case 2 then show ?case by simp
next
case 3 show ?case by simp (metis permute_minus_cancel(2) satisfies_eqvt)
next
case (4 P α t) show ?case
proof
assume "valid_Tree P (tAct α t)"
then obtain α' t' P' where *: "tAct α t =⇩α tAct α' t' ∧ P → ⟨α',P'⟩ ∧ valid_Tree P' t'"
by auto
with "4.IH" have "valid_Tree (p ∙ P') (p ∙ t')"
by blast
moreover from "*" have "p ∙ P → ⟨p ∙ α', p ∙ P'⟩"
by (metis transition_eqvt')
moreover from "*" have "p ∙ tAct α t =⇩α tAct (p ∙ α') (p ∙ t')"
by (metis alpha_Tree_eqvt permute_Tree.simps(4))
ultimately show "valid_Tree (p ∙ P) (p ∙ tAct α t)"
by auto
next
assume "valid_Tree (p ∙ P) (p ∙ tAct α t)"
then obtain α' t' P' where *: "p ∙ tAct α t =⇩α tAct α' t' ∧ (p ∙ P) → ⟨α',P'⟩ ∧ valid_Tree P' t'"
by auto
then have eq: "tAct α t =⇩α tAct (-p ∙ α') (-p ∙ t')"
by (metis alpha_Tree_eqvt permute_Tree.simps(4) permute_minus_cancel(2))
moreover from "*" have "P → ⟨-p ∙ α', -p ∙ P'⟩"
by (metis permute_minus_cancel(2) transition_eqvt')
moreover with "4.IH" have "valid_Tree (-p ∙ P') (-p ∙ t')"
using eq and "*" by simp
ultimately show "valid_Tree P (tAct α t)"
by auto
qed
qed

lemma valid_Tree_eqvt (*[eqvt]*):
assumes "valid_Tree P t" shows "valid_Tree (p ∙ P) (p ∙ t)"
using assms by (metis valid_Tree_eqvt')

text ‹$\alpha$-equivalent trees validate the same states.›

lemma alpha_Tree_valid_Tree:
assumes "t1 =⇩α t2"
shows "valid_Tree P t1 ⟷ 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 α1 t1 α2 t2) show ?case
proof
assume "valid_Tree P (tAct α1 t1)"
then obtain α' t' P' where "tAct α1 t1 =⇩α tAct α' t' ∧ P → ⟨α',P'⟩ ∧ valid_Tree P' t'"
by auto
moreover from tAct.hyps have "tAct α1 t1 =⇩α tAct α2 t2"
using alpha_tAct by blast
ultimately show "valid_Tree P (tAct α2 t2)"
by (metis Tree⇩α.abs_eq_iff valid_Tree.simps(4))
next
assume "valid_Tree P (tAct α2 t2)"
then obtain α' t' P' where "tAct α2 t2 =⇩α tAct α' t' ∧ P → ⟨α',P'⟩ ∧ valid_Tree P' t'"
by auto
moreover from tAct.hyps have "tAct α1 t1 =⇩α tAct α2 t2"
using alpha_tAct by blast
ultimately show "valid_Tree P (tAct α1 t1)"
by (metis Tree⇩α.abs_eq_iff valid_Tree.simps(4))
qed
qed simp_all

subsection ‹Validity for trees modulo \texorpdfstring{$\alpha$}{alpha}-equivalence›

lift_definition valid_Tree⇩α :: "'state ⇒ ('idx,'pred,'act) Tree⇩α ⇒ bool" is
valid_Tree
by (fact alpha_Tree_valid_Tree)

lemma valid_Tree⇩α_eqvt (*[eqvt]*):
assumes "valid_Tree⇩α P t" shows "valid_Tree⇩α (p ∙ P) (p ∙ t)"
using assms by transfer (fact valid_Tree_eqvt)

lemma valid_Tree⇩α_Conj⇩α [simp]: "valid_Tree⇩α P (Conj⇩α tset⇩α) ⟷ (∀t⇩α∈set_bset tset⇩α. valid_Tree⇩α P t⇩α)"
proof -
have "valid_Tree P (rep_Tree⇩α (abs_Tree⇩α (tConj (map_bset rep_Tree⇩α tset⇩α)))) ⟷ valid_Tree P (tConj (map_bset rep_Tree⇩α tset⇩α))"
by (metis Tree⇩α_rep_abs alpha_Tree_valid_Tree)
then show ?thesis
by (simp add: valid_Tree⇩α_def Conj⇩α_def map_bset.rep_eq)
qed

lemma valid_Tree⇩α_Not⇩α [simp]: "valid_Tree⇩α P (Not⇩α t⇩α) ⟷ ¬ valid_Tree⇩α P t⇩α"
by transfer simp

lemma valid_Tree⇩α_Pred⇩α [simp]: "valid_Tree⇩α P (Pred⇩α φ) ⟷ P ⊢ φ"
by transfer simp

lemma valid_Tree⇩α_Act⇩α [simp]: "valid_Tree⇩α P (Act⇩α α t⇩α) ⟷ (∃α' t⇩α' P'. Act⇩α α t⇩α = Act⇩α α' t⇩α' ∧ P → ⟨α',P'⟩ ∧ valid_Tree⇩α P' t⇩α')"
proof
assume "valid_Tree⇩α P (Act⇩α α t⇩α)"
moreover have "Act⇩α α t⇩α = abs_Tree⇩α (tAct α (rep_Tree⇩α t⇩α))"
by (metis Act⇩α.abs_eq Tree⇩α_abs_rep)
ultimately show "∃α' t⇩α' P'. Act⇩α α t⇩α = Act⇩α α' t⇩α' ∧ P → ⟨α',P'⟩ ∧ valid_Tree⇩α P' t⇩α'"
by (metis Act⇩α.abs_eq Tree⇩α.abs_eq_iff valid_Tree.simps(4) valid_Tree⇩α.abs_eq)
next
assume "∃α' t⇩α' P'. Act⇩α α t⇩α = Act⇩α α' t⇩α' ∧ P → ⟨α',P'⟩ ∧ valid_Tree⇩α P' t⇩α'"
moreover have "⋀α' t⇩α'. Act⇩α α' t⇩α' = abs_Tree⇩α (tAct α' (rep_Tree⇩α t⇩α'))"
by (metis Act⇩α.abs_eq Tree⇩α_abs_rep)
ultimately show "valid_Tree⇩α P (Act⇩α α t⇩α)"
by (metis Tree⇩α.abs_eq_iff valid_Tree.simps(4) valid_Tree⇩α.abs_eq valid_Tree⇩α.rep_eq)
qed

subsection ‹Validity for infinitary formulas›

lift_definition valid :: "'state ⇒ ('idx,'pred,'act) formula ⇒ bool" (infix "⊨" 70) is
valid_Tree⇩α
.

lemma valid_eqvt (*[eqvt]*):
assumes "P ⊨ x" shows "(p ∙ P) ⊨ (p ∙ x)"
using assms by transfer (metis valid_Tree⇩α_eqvt)

lemma valid_Conj [simp]:
assumes "finite (supp xset)"
shows "P ⊨ Conj xset ⟷ (∀x∈set_bset xset. P ⊨ x)"
using assms by (simp add: valid_def Conj_def map_bset.rep_eq)

lemma valid_Not [simp]: "P ⊨ Not x ⟷ ¬ P ⊨ x"
by transfer simp

lemma valid_Pred [simp]: "P ⊨ Pred φ ⟷ P ⊢ φ"
by transfer simp

lemma valid_Act: "P ⊨ Act α x ⟷ (∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x')"
proof
assume "P ⊨ Act α x"
moreover have "Rep_formula (Abs_formula (Act⇩α α (Rep_formula x))) = Act⇩α α (Rep_formula x)"
by (metis Act.rep_eq Rep_formula_inverse)
ultimately show "∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x'"
by (auto simp add: valid_def Act_def) (metis Abs_formula_inverse Rep_formula' hereditarily_fs_alpha_renaming)
next
assume "∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x'"
then show "P ⊨ Act α x"
by (metis Act.rep_eq valid.rep_eq 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 valid_Act_strong:
assumes "finite (supp X)"
shows "P ⊨ Act α x ⟷ (∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x' ∧ bn α' ♯* X)"
proof
assume "P ⊨ Act α x"
then obtain α' x' P' where eq: "Act α x = Act α' x'" and trans: "P → ⟨α',P'⟩" and valid: "P' ⊨ x'"
by (metis valid_Act)
have "finite (bn α')"
by (fact bn_finite)
moreover note ‹finite (supp X)›
moreover have "finite (supp (Act α' x', ⟨α',P'⟩))"
by (metis finite_Diff finite_UnI finite_supp supp_Pair supp_abs_residual_pair)
moreover have "bn α' ♯* (Act α' x', ⟨α',P'⟩)"
by (auto simp add: fresh_star_def fresh_def supp_Pair supp_abs_residual_pair)
ultimately obtain p where fresh_X: "(p ∙ bn α') ♯* X" and "supp (Act α' x', ⟨α',P'⟩) ♯* p"
by (metis at_set_avoiding2)
then have "supp (Act α' x') ♯* p" and "supp ⟨α',P'⟩ ♯* p"
by (metis fresh_star_Un supp_Pair)+
then have "Act (p ∙ α') (p ∙ x') = Act α' x'" and "⟨p ∙ α', p ∙ P'⟩ = ⟨α',P'⟩"
by (metis Act_eqvt supp_perm_eq, metis abs_residual_pair_eqvt supp_perm_eq)
then show "∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x' ∧ bn α' ♯* X"
using eq and trans and valid and fresh_X by (metis bn_eqvt valid_eqvt)
next
assume "∃α' x' P'. Act α x = Act α' x' ∧ P → ⟨α',P'⟩ ∧ P' ⊨ x' ∧ bn α' ♯* X"
then show "P ⊨ Act α x"
by (metis valid_Act)
qed

lemma valid_Act_fresh:
assumes "bn α ♯* P"
shows "P ⊨ Act α x ⟷ (∃P'. P → ⟨α,P'⟩ ∧ P' ⊨ x)"
proof
assume "P ⊨ Act α x"

moreover have "finite (supp P)"
by (fact finite_supp)
ultimately obtain α' x' P' where
eq: "Act α x = Act α' x'" and trans: "P → ⟨α',P'⟩" and valid: "P' ⊨ x'" and fresh: "bn α' ♯* P"
by (metis 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 α) ♯* P"
using p_α by (metis bn_eqvt fresh_star_Un)
then have "supp p ♯* P"
using supp_p by (metis fresh_star_def subset_eq)
then have p_P: "-p ∙ P = P"
by (metis perm_supp_eq supp_minus_perm)

from trans have "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) valid_eqvt)
ultimately show "∃P'. P → ⟨α,P'⟩ ∧ P' ⊨ x"
by meson
next
assume "∃P'. P → ⟨α,P'⟩ ∧ P' ⊨ x" then show "P ⊨ Act α x"
by (metis valid_Act)
qed

end

end