Theory First_Order_Clause.Entailment_Lifting

theory Entailment_Lifting
  imports Abstract_Substitution.Based_Substitution_Lifting
begin

locale entailment =
  based: based_subst_update where base_subst = base_subst and vars = vars +
  base: grounding where
  subst = base_subst and vars = base_vars and is_ground = base_is_ground 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.
        base_is_ground update ⟹
        base_is_ground (x ⋅v γ) ⟹
        (base_to_ground (x ⋅v γ), base_to_ground update) ∈ I ⟹
        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: "base_is_ground update" and
    var_grounding: "base_is_ground (x ⋅v γ)" and
    var_update: "(base_to_ground (x ⋅v γ), base_to_ground update) ∈ I" and
    expr_grounding: "is_ground (subst expr γ)"
  shows "⊨ expr ⋅ γ⟦x := update⟧ ⟷ ⊨ expr ⋅ γ"
proof (rule iffI)
  assume "⊨ expr ⋅ γ⟦x := update⟧"

  then show "⊨ expr ⋅ γ"
    by(rule congruence[OF assms])
next
  assume expr_γ: "⊨ expr ⋅ γ"

  show "⊨ expr ⋅ γ⟦x := update⟧"
  proof (cases based.base.exists_nonground)
    case exists_nonground: True

    show ?thesis
    proof (rule congruence[OF var_grounding, of x "γ⟦x := update⟧" expr])

      show "base_is_ground (x ⋅v γ⟦x := update⟧)"
        by (metis update_is_ground based.exists_nonground_iff_base_exists_nonground
            based.subst_update_var(1))
    next

      show "(base_to_ground (x ⋅v γ⟦x := update⟧), base_to_ground (x ⋅v γ)) ∈ I"
        by (metis based.exists_nonground_iff_base_exists_nonground based.subst_update_var(1)
            exists_nonground local.sym symE var_update)
    next

      show "is_ground (expr ⋅ γ⟦x := update⟧)"
        by (simp add: expr_grounding update_is_ground)
    next

      show "⊨ expr ⋅ (γ⟦x := update⟧)⟦x := x ⋅v γ⟧"
        by (simp add: expr_γ)
    qed
  next
    case False

    then show ?thesis
      using expr_γ based.exists_nonground_iff_base_exists_nonground
      by (metis based.all_subst_ident_if_ground)
  qed
qed

end

locale symmetric_base_entailment =
  base_substitution where subst = subst +
  based_subst_update where 
  subst = subst and base_subst = subst and base_is_ground = is_ground and base_vars = vars +

  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 (metis all_subst_ident_if_ground ground_subst_update sym subst_update(2) subst_update_twice
      subst_update_var(1) symE)

lemma simultaneous_congruence:
  assumes
    "is_ground update" and "is_ground update'"  and
    "is_ground (x ⋅v γ)" and "is_ground (x' ⋅v γ)"
    "(to_ground (x ⋅v γ), to_ground update) ∈ I" and
    "(to_ground (x' ⋅v γ), to_ground update') ∈ I" and
    "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)

lemma simultaneous_congruence_same:
  assumes
    "is_ground update" and "is_ground (x ⋅v γ)" and
    "(to_ground (x ⋅v γ), to_ground update) ∈ I" and
     "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 simultaneous_congruence assms
  by metis

end

locale entailment_lifting =
  based_substitution_lifting where map = "map :: ('sub ⇒ 'sub) ⇒ 'expr ⇒ 'expr" +
  finite_variables_lifting +
  based_subst_update_lifting +

  sub: symmetric_entailment where
  subst = sub_subst and vars = sub_vars and is_ground = sub_is_ground 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 is_ground = is_ground 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 (rule 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