Theory FOR_Semantics

theory FOR_Semantics
  imports FOR_Certificate
    Lift_Root_Step
    "FOL-Fitting.FOL_Fitting"
begin

section ‹Semantics of Relations›

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)
  moreover have "ground C⟨r ⋅ τ⟩" using terms(1) w τ_def
    by (auto intro!: ground_substI) (metis term_of_gterm_ctxt_subst_apply_ground)
  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 @{const gcomp_rel} and @{const 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 gmctxt_cl_gmctxtex_onp_conv) (metis refl_onD2 relf_on_gmctxtcl_funas)

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