theory FOR_Semantics
imports FOR_Certificate Lift_Root_Step UL.Basic_Utils "FOL-Fitting.FOL_Fitting"
begin
subsection ‹Semantics of Relations›
thm gcomp_rel_def
thm gtrancl_rel_def
definition is_to_trs :: "('f, 'v) trs list ⇒ ftrs list ⇒ ('f, 'v) trs" where
"is_to_trs Rs is = ⋃(set (map (case_ftrs ((!) Rs) ((`) prod.swap ∘ (!) Rs)) is))"
primrec eval_gtt_rel :: "('f × nat) set ⇒ ('f, 'v) trs list ⇒ ftrs gtt_rel ⇒ 'f gterm rel" where
"eval_gtt_rel ℱ Rs (ARoot is) = Restr (grrstep (is_to_trs Rs is)) (𝒯⇩G ℱ)"
| "eval_gtt_rel ℱ Rs (GInv g) = prod.swap ` (eval_gtt_rel ℱ Rs g)"
| "eval_gtt_rel ℱ Rs (AUnion g1 g2) = (eval_gtt_rel ℱ Rs g1) ∪ (eval_gtt_rel ℱ Rs g2)"
| "eval_gtt_rel ℱ Rs (ATrancl g) = (eval_gtt_rel ℱ Rs g)⇧+"
| "eval_gtt_rel ℱ Rs (AComp g1 g2) = (eval_gtt_rel ℱ Rs g1) O (eval_gtt_rel ℱ Rs g2)"
| "eval_gtt_rel ℱ Rs (GTrancl g) = gtrancl_rel ℱ (eval_gtt_rel ℱ Rs g)"
| "eval_gtt_rel ℱ Rs (GComp g1 g2) = gcomp_rel ℱ (eval_gtt_rel ℱ Rs g1) (eval_gtt_rel ℱ Rs g2)"
primrec eval_rr1_rel :: "('f × nat) set ⇒ ('f, 'v) trs list ⇒ ftrs rr1_rel ⇒ 'f gterm set"
and eval_rr2_rel :: "('f × nat) set ⇒ ('f, 'v) trs list ⇒ ftrs rr2_rel ⇒ 'f gterm rel" where
"eval_rr1_rel ℱ Rs R1Terms = (𝒯⇩G ℱ)"
| "eval_rr1_rel ℱ Rs (R1Union R S) = (eval_rr1_rel ℱ Rs R) ∪ (eval_rr1_rel ℱ Rs S)"
| "eval_rr1_rel ℱ Rs (R1Inter R S) = (eval_rr1_rel ℱ Rs R) ∩ (eval_rr1_rel ℱ Rs S)"
| "eval_rr1_rel ℱ Rs (R1Diff R S) = (eval_rr1_rel ℱ Rs R) - (eval_rr1_rel ℱ Rs S)"
| "eval_rr1_rel ℱ Rs (R1Proj n R) = (case n of 0 ⇒ fst ` (eval_rr2_rel ℱ Rs R)
| _ ⇒ snd ` (eval_rr2_rel ℱ Rs R))"
| "eval_rr1_rel ℱ Rs (R1NF is) = NF (Restr (grstep (is_to_trs Rs is)) (𝒯⇩G ℱ)) ∩ (𝒯⇩G ℱ)"
| "eval_rr1_rel ℱ Rs (R1Inf R) = {s. infinite (eval_rr2_rel ℱ Rs R `` {s})}"
| "eval_rr2_rel ℱ Rs (R2GTT_Rel A W X) = lift_root_step ℱ W X (eval_gtt_rel ℱ Rs A)"
| "eval_rr2_rel ℱ Rs (R2Inv R) = prod.swap ` (eval_rr2_rel ℱ Rs R)"
| "eval_rr2_rel ℱ Rs (R2Union R S) = (eval_rr2_rel ℱ Rs R) ∪ (eval_rr2_rel ℱ Rs S)"
| "eval_rr2_rel ℱ Rs (R2Inter R S) = (eval_rr2_rel ℱ Rs R) ∩ (eval_rr2_rel ℱ Rs S)"
| "eval_rr2_rel ℱ Rs (R2Diff R S) = (eval_rr2_rel ℱ Rs R) - (eval_rr2_rel ℱ Rs S)"
| "eval_rr2_rel ℱ Rs (R2Comp R S) = (eval_rr2_rel ℱ Rs R) O (eval_rr2_rel ℱ Rs S)"
| "eval_rr2_rel ℱ Rs (R2Diag R) = Id_on (eval_rr1_rel ℱ Rs R)"
| "eval_rr2_rel ℱ Rs (R2Prod R S) = (eval_rr1_rel ℱ Rs R) × (eval_rr1_rel ℱ Rs S)"
subsection ‹Semantics of Formulas›
fun eval_formula :: "('f × nat) set ⇒ ('f, 'v) trs list ⇒ (nat ⇒ 'f gterm) ⇒
ftrs formula ⇒ bool" where
"eval_formula ℱ Rs α (FRR1 r1 x) ⟷ α x ∈ eval_rr1_rel ℱ Rs r1"
| "eval_formula ℱ Rs α (FRR2 r2 x y) ⟷ (α x, α y) ∈ eval_rr2_rel ℱ Rs r2"
| "eval_formula ℱ Rs α (FAnd fs) ⟷ (∀f ∈ set fs. eval_formula ℱ Rs α f)"
| "eval_formula ℱ Rs α (FOr fs) ⟷ (∃f ∈ set fs. eval_formula ℱ Rs α f)"
| "eval_formula ℱ Rs α (FNot f) ⟷ ¬ eval_formula ℱ Rs α f"
| "eval_formula ℱ Rs α (FExists f) ⟷ (∃z ∈ 𝒯⇩G ℱ. eval_formula ℱ Rs (α⟨0 : z⟩) f)"
| "eval_formula ℱ Rs α (FForall f) ⟷ (∀z ∈ 𝒯⇩G ℱ. eval_formula ℱ Rs (α⟨0 : z⟩) f)"
fun formula_arity :: "'trs formula ⇒ nat" where
"formula_arity (FRR1 r1 x) = Suc x"
| "formula_arity (FRR2 r2 x y) = max (Suc x) (Suc y)"
| "formula_arity (FAnd fs) = max_list (map formula_arity fs)"
| "formula_arity (FOr fs) = max_list (map formula_arity fs)"
| "formula_arity (FNot f) = formula_arity f"
| "formula_arity (FExists f) = formula_arity f - 1"
| "formula_arity (FForall f) = formula_arity f - 1"
lemma R1NF_reps:
assumes "funas_trs R ⊆ ℱ" "∀ t. (term_of_gterm s, term_of_gterm t) ∈ rstep R ⟶ ¬funas_gterm t ⊆ ℱ"
and "funas_gterm s ⊆ ℱ" "(l, r) ∈ R" "term_of_gterm s = C⟨l ⋅ (σ :: 'b ⇒ ('a, 'b) Term.term)⟩"
shows False
proof -
obtain c where w: "funas_term (c :: ('a, 'b) Term.term) ⊆ ℱ" "ground c"
using assms(3) funas_term_of_gterm_conv ground_term_of_gterm by blast
define τ where "τ x = (if x ∈ vars_term l then σ x else c)" for x
from assms(4-) have terms: "term_of_gterm s = C⟨l ⋅ τ⟩" "(C⟨l ⋅ τ⟩, C⟨r ⋅ τ⟩) ∈ rstep R"
using τ_def by auto (metis term_subst_eq)
from this(1) have [simp]: "funas_gterm s = funas_term C⟨l ⋅ τ⟩" by (metis funas_term_of_gterm_conv)
from w assms(1, 3, 4) have [simp]: "funas_term C⟨r ⋅ τ⟩ ⊆ ℱ" using τ_def
by (auto simp: funas_trs_def funas_term_subst) (meson assms(1) rhs_wf subsetD)
moreover have "ground C⟨r ⋅ τ⟩" using terms(1) w τ_def
by auto (metis ground_ctxt_apply ground_term_of_gterm ground_subst)+
ultimately show ?thesis using assms(2) terms(2)
by (metis funas_term_of_gterm_conv ground_term_to_gtermD terms(1))
qed
text ‹The central property we are interested in is satisfiability›
definition formula_satisfiable where
"formula_satisfiable ℱ Rs f ⟷ (∃α. range α ⊆ 𝒯⇩G ℱ ∧ eval_formula ℱ Rs α f)"
subsection ‹Validation›
subsection ‹Defining properties of gcomp_rel and gtrancl_rel›
lemma gcomp_rel_sig:
assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ" and "S ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "gcomp_rel ℱ R S ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
using assms subsetD[OF signature_pres_funas_cl(2)[OF assms(1)]]
by (auto simp: gcomp_rel_def lift_root_step.simps) (metis refl_onD2 relf_on_gmctxtcl_funas)
thm gcomp_rel
lemma gtrancl_rel_sig:
assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "gtrancl_rel ℱ R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
using gtrancl_rel_sound[OF assms] by simp
lemma gtrancl_rel:
assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "lift_root_step ℱ PAny EStrictParallel (gtrancl_rel ℱ R) = (lift_root_step ℱ PAny ESingle R)⇧+"
unfolding lift_root_step.simps using gmctxtcl_funas_strict_gtrancl_rel[OF assms] .
lemma gtrancl_rel':
assumes "R ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
shows "lift_root_step ℱ PAny EParallel (gtrancl_rel ℱ R) = Restr ((lift_root_step ℱ PAny ESingle R)⇧*) (𝒯⇩G ℱ)"
using assms gtrancl_rel[OF assms]
by (auto simp: lift_root_step_Parallel_conv
simp flip: reflcl_trancl dest: Restr_simps(5)[OF lift_root_step_sig, THEN subsetD])
text ‹GTT relation semantics respects the signature›
lemma eval_gtt_rel_sig:
"eval_gtt_rel ℱ Rs g ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
proof -
show ?thesis by (induct g) (auto 0 3 simp: gtrancl_rel_sig gcomp_rel_sig dest: tranclD tranclD2)
qed
text ‹RR1 and RR2 relation semantics respect the signature›
lemma eval_rr12_rel_sig:
"eval_rr1_rel ℱ Rs r1 ⊆ 𝒯⇩G ℱ"
"eval_rr2_rel ℱ Rs r2 ⊆ 𝒯⇩G ℱ × 𝒯⇩G ℱ"
proof (induct r1 and r2)
case (R1Inf r2) then show ?case by (auto dest!: infinite_imp_nonempty)
next
case (R1Proj i r2) then show ?case by (fastforce split: nat.splits)
next
case (R2GTT_Rel g W X) then show ?case by (simp add: lift_root_step_sig eval_gtt_rel_sig)
qed auto
subsection ‹Correctness of derived constructions›
lemma R1Fin:
"eval_rr1_rel ℱ Rs (R1Fin r) = {t ∈ 𝒯⇩G ℱ. finite {s. (t, s) ∈ eval_rr2_rel ℱ Rs r}}"
by (auto simp: R1Fin_def Image_def)
lemma R2Eq:
"eval_rr2_rel ℱ Rs R2Eq = Id_on (𝒯⇩G ℱ)"
by (auto simp: 𝒯⇩G_funas_gterm_conv R2Eq_def)
lemma R2Reflc:
"eval_rr2_rel ℱ Rs (R2Reflc r) = eval_rr2_rel ℱ Rs r ∪ Id_on (𝒯⇩G ℱ)"
"eval_rr2_rel ℱ Rs (R2Reflc r) = Restr ((eval_rr2_rel ℱ Rs r)⇧=) (𝒯⇩G ℱ)"
using eval_rr12_rel_sig(2)[of ℱ Rs "R2Reflc r"]
by (auto simp: R2Reflc_def R2Eq)
lemma R2Step:
"eval_rr2_rel ℱ Rs (R2Step ts) = Restr (grstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
by (auto simp: lift_root_step.simps R2Step_def grstep_lift_root_step grrstep_subst_cl_conv grstepD_grstep_conv grstepD_def)
lemma R2StepEq:
"eval_rr2_rel ℱ Rs (R2StepEq ts) = Restr ((grstep (is_to_trs Rs ts))⇧=) (𝒯⇩G ℱ)"
by (auto simp: R2StepEq_def R2Step R2Reflc(2))
lemma R2Steps:
fixes ℱ Rs ts defines "R ≡ Restr (grstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
shows "eval_rr2_rel ℱ Rs (R2Steps ts) = R⇧+"
by (simp add: R2Steps_def GSteps_def R_def gtrancl_rel grstep_lift_root_step)
(metis FOR_Semantics.gtrancl_rel Sigma_cong grstep_lift_root_step inf.cobounded2 lift_root_Any_EStrict_eq)
lemma R2StepsEq:
fixes ℱ Rs ts defines "R ≡ Restr (grstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
shows "eval_rr2_rel ℱ Rs (R2StepsEq ts) = Restr (R⇧*) (𝒯⇩G ℱ)"
using R2Steps[of ℱ Rs ts]
by (simp add: R2StepsEq_def R2Steps_def lift_root_step_Parallel_conv Int_Un_distrib2 R_def Restr_simps flip: reflcl_trancl)
lemma R2StepsNF:
fixes ℱ Rs ts defines "R ≡ Restr (grstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
shows "eval_rr2_rel ℱ Rs (R2StepsNF ts) = Restr (R⇧* ∩ UNIV × NF R) (𝒯⇩G ℱ)"
using R2StepsEq[of ℱ Rs ts]
by (auto simp: R2StepsNF_def R2StepsEq_def R_def)
lemma R2ParStep:
"eval_rr2_rel ℱ Rs (R2ParStep ts) = Restr (gpar_rstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
by (simp add: R2ParStep_def gar_rstep_lift_root_step)
lemma R2RootStep:
"eval_rr2_rel ℱ Rs (R2RootStep ts) = Restr (grrstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
by (simp add: R2RootStep_def lift_root_step.simps)
lemma R2RootStepEq:
"eval_rr2_rel ℱ Rs (R2RootStepEq ts) = Restr ((grrstep (is_to_trs Rs ts))⇧=) (𝒯⇩G ℱ)"
by (auto simp: R2RootStepEq_def R2RootStep R2Reflc(2))
lemma R2RootSteps:
fixes ℱ Rs ts defines "R ≡ Restr (grrstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
shows "eval_rr2_rel ℱ Rs (R2RootSteps ts) = R⇧+"
by (simp add: R2RootSteps_def R_def lift_root_step.simps)
lemma R2RootStepsEq:
fixes ℱ Rs ts defines "R ≡ Restr (grrstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
shows "eval_rr2_rel ℱ Rs (R2RootStepsEq ts) = Restr (R⇧*) (𝒯⇩G ℱ)"
by (auto simp: R2RootStepsEq_def R2Reflc_def R2RootSteps R_def R2Eq_def Int_Un_distrib2 Restr_simps simp flip: reflcl_trancl)
lemma R2NonRootStep:
"eval_rr2_rel ℱ Rs (R2NonRootStep ts) = Restr (gnrrstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
by (simp add: R2NonRootStep_def grrstep_lift_root_gnrrstep)
lemma R2NonRootStepEq:
"eval_rr2_rel ℱ Rs (R2NonRootStepEq ts) = Restr ((gnrrstep (is_to_trs Rs ts))⇧=) (𝒯⇩G ℱ)"
by (auto simp: R2NonRootStepEq_def R2Reflc_def R2Eq_def R2NonRootStep Int_Un_distrib2)
lemma R2NonRootSteps:
fixes ℱ Rs ts defines "R ≡ Restr (gnrrstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
shows "eval_rr2_rel ℱ Rs (R2NonRootSteps ts) = R⇧+"
apply (simp add: lift_root_step.simps gnrrstepD_gnrrstep_conv gnrrstepD_def
grrstep_subst_cl_conv R2NonRootSteps_def R_def GSteps_def lift_root_step_Parallel_conv)
apply (intro gmctxtex_funas_nroot_strict_gtrancl_rel)
by simp
lemma R2NonRootStepsEq:
fixes ℱ Rs ts defines "R ≡ Restr (gnrrstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
shows "eval_rr2_rel ℱ Rs (R2NonRootStepsEq ts) = Restr (R⇧*) (𝒯⇩G ℱ)"
using R2NonRootSteps[of ℱ Rs ts]
by (simp add: R2NonRootSteps_def R2NonRootStepsEq_def lift_root_step_Parallel_conv
R_def Int_Un_distrib2 Restr_simps flip: reflcl_trancl)
lemma converse_to_prod_swap:
"R¯ = prod.swap ` R"
by auto
lemma R2Meet:
fixes ℱ Rs ts defines "R ≡ Restr (grstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
shows "eval_rr2_rel ℱ Rs (R2Meet ts) = Restr ((R¯)⇧* O R⇧*) (𝒯⇩G ℱ)"
apply (simp add: R2Meet_def R_def GSteps_def converse_to_prod_swap gcomp_rel[folded lift_root_step.simps] gtrancl_rel' swap_lift_root_step grstep_lift_root_step)
apply (simp add: Restr_simps converse_Int converse_Un converse_Times Int_Un_distrib2 flip: reflcl_trancl trancl_converse converse_to_prod_swap)
done
lemma R2Join:
fixes ℱ Rs ts defines "R ≡ Restr (grstep (is_to_trs Rs ts)) (𝒯⇩G ℱ)"
shows "eval_rr2_rel ℱ Rs (R2Join ts) = Restr (R⇧* O (R¯)⇧*) (𝒯⇩G ℱ)"
apply (simp add: R2Join_def R_def GSteps_def converse_to_prod_swap gcomp_rel[folded lift_root_step.simps] gtrancl_rel' swap_lift_root_step grstep_lift_root_step)
apply (simp add: Restr_simps converse_to_prod_swap[symmetric] converse_Int converse_Un converse_Times Int_Un_distrib2 flip: reflcl_trancl trancl_converse)
done
end