Theory First_Order_Clause.Entailment_Lifting

theory Entailment_Lifting
  imports Abstract_Substitution.Based_Substitution_Lifting
begin

locale entailment =
  based: based_substitution where base_subst = base_subst and vars = vars +
  base: grounding where subst = base_subst and vars = base_vars and to_ground = base_to_ground and
  from_ground = base_from_ground for
  vars :: "'expr ⇒ 'var set" and
  base_subst :: "'base ⇒ 'subst ⇒ 'base" and
  base_to_ground :: "'base ⇒ 'base⇩G" and
  base_from_ground +
fixes 
  entails_def :: "'expr ⇒ bool" ("(⊨ _)" [50] 50) and 
  I ::  "('base⇩G × 'base⇩G) set"
assumes
  congruence: "⋀expr γ x update.
        based.base.is_ground update ⟹
        based.base.is_ground (x ⋅v γ) ⟹
        (base_to_ground (x ⋅v γ), base_to_ground update) ∈ I ⟹
        based.is_ground (expr ⋅ γ) ⟹
        ⊨ expr ⋅ γ⟦x := update⟧ ⟹
        ⊨ expr ⋅ γ"
begin

abbreviation entails where
  "entails ≡ entails_def"

end

locale symmetric_entailment = entailment +
  assumes sym: "sym I"
begin

lemma symmetric_congruence:
  assumes
    update_is_ground: "based.base.is_ground update" and
    var_grounding: "based.base.is_ground (x ⋅v γ)" and
    var_update: "(base_to_ground (x ⋅v γ), base_to_ground update) ∈ I" and
    expr_grounding: "based.is_ground (subst expr γ)"
  shows "⊨ expr ⋅ γ⟦x := update⟧ ⟷ ⊨ expr ⋅ γ"
proof (rule iffI)
  assume "⊨ expr ⋅ subst_update γ x update"

  then show "⊨ expr ⋅ γ"
    by(rule congruence[OF assms])
next
  assume "⊨ expr ⋅ γ"
  then show "⊨ expr ⋅ subst_update γ x update"
    using congruence[OF var_grounding, of x "(subst_update γ x update)" expr] assms
    by (metis based.ground_subst_update based.subst_eq based.subst_update sym symE)
qed

end

locale symmetric_base_entailment =
  base_substitution where subst = subst +
  grounding where subst = subst and to_ground = to_ground for
  subst :: "'base ⇒ 'subst ⇒ 'base"  (infixl "⋅" 70) and
  to_ground :: "'base ⇒ 'base⇩G" +
fixes I :: "('base⇩G × 'base⇩G) set"
assumes
  sym: "sym I" and
  congruence: "⋀expr expr' update γ x.
      is_ground update ⟹
      is_ground (x ⋅v γ) ⟹
      (to_ground (x ⋅v γ), to_ground update) ∈ I ⟹
      is_ground (expr ⋅ γ) ⟹
      (to_ground (expr ⋅ γ⟦x := update⟧), expr') ∈ I ⟹
      (to_ground (expr ⋅ γ), expr') ∈ I"
begin

lemma symmetric_congruence:
  assumes
    update_is_ground: "is_ground update" and
    var_grounding: "is_ground (x ⋅v γ)" and
    expr_grounding: "is_ground (expr ⋅ γ)" and
    var_update: "(to_ground (x ⋅v γ), to_ground update) ∈ I"
  shows "(to_ground (expr ⋅ γ⟦x := update⟧), expr') ∈ I ⟷ (to_ground (expr ⋅ γ), expr') ∈ I"
  using assms congruence[OF var_grounding, of x "γ⟦x := update⟧"] congruence
  by (smt (verit, del_insts) ground_subst_update sym subst_eq symE subst_update)

lemma simultaneous_congruence:
  assumes
    update_is_ground: "is_ground update" and
    var_grounding: "is_ground (x ⋅v γ)" and
    var_update: "(to_ground (x ⋅v γ), to_ground update) ∈ I" and
    expr_grounding: "is_ground (expr ⋅ γ)" "is_ground (expr' ⋅ γ)"
  shows
    "(to_ground (expr ⋅ (γ⟦x := update⟧)), to_ground (expr' ⋅ (γ⟦x := update⟧))) ∈ I ⟷
        (to_ground (expr ⋅ γ), to_ground (expr' ⋅ γ))  ∈ I"
  using assms
  by (meson sym symD symmetric_congruence)

end

locale entailment_lifting =
  based_substitution_lifting where map = "map :: ('sub ⇒ 'sub) ⇒ 'expr ⇒ 'expr" +
  finite_variables_lifting +
  sub: symmetric_entailment where subst = sub_subst and vars = sub_vars and entails_def = sub_entails
  for sub_entails ("(⊨⇩s _)" [50] 50) +
  fixes
    is_negated :: "'expr ⇒ bool" and
    empty :: bool and
    connective :: "bool ⇒ bool ⇒ bool" and
    entails_def ("(⊨ _)" [50] 50)
  assumes
    is_negated_subst: "⋀expr σ. is_negated (expr ⋅ σ) ⟷ is_negated expr" and
    entails_def: "⋀expr. ⊨ expr ⟷
      (if is_negated expr then Not else (λx. x))
        (Finite_Set.fold connective empty (sub_entails  ` to_set expr))"
begin

sublocale symmetric_entailment where subst = subst and vars = vars and entails_def = entails_def
proof unfold_locales
  fix expr γ x update P
  assume
    "base.is_ground update"
    "base.is_ground (x ⋅v γ)"
    "is_ground (expr ⋅ γ)"
    "(base_to_ground (x ⋅v γ), base_to_ground update) ∈ I"
    "⊨ expr ⋅ γ⟦x := update⟧"

  moreover then have "∀sub ∈ to_set expr. (⊨⇩s sub ⋅⇩s γ⟦x := update⟧) ⟷ ⊨⇩s sub ⋅⇩s γ"
    using sub.symmetric_congruence to_set_is_ground_subst
    by blast

  ultimately show "⊨ expr ⋅ γ"
    unfolding is_negated_subst entails_def
    by(auto simp: image_image subst_def)

qed (simp_all add: is_grounding_iff_vars_grounded sub.sym )

end

locale entailment_lifting_conj = entailment_lifting where
  connective = "(∧)" and empty = True

locale entailment_lifting_disj = entailment_lifting where
  connective = "(∨)" and empty = False

end