Theory Entailment_Lifting

theory Entailment_Lifting
  imports Abstract_Substitution.Functional_Substitution_Lifting
begin

locale entailment =
  based: based_functional_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 ⇒ ('var ⇒ 'base) ⇒ 'base" and
  base_to_ground :: "'base ⇒ 'base⇩G" and
  base_from_ground +
fixes entails_def :: "'expr ⇒ bool" and I ::  "('base⇩G × 'base⇩G) set"
assumes
  congruence: "⋀expr γ var update.
        based.base.is_ground update ⟹
        based.base.is_ground (γ var) ⟹
        (base_to_ground (γ var), base_to_ground update) ∈ I ⟹
        based.is_ground (subst expr γ) ⟹
        entails_def (subst expr (γ(var := update))) ⟹
        entails_def (subst expr γ)"
begin

abbreviation "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 (γ var)" and
    var_update: "(base_to_ground (γ var), base_to_ground update) ∈ I" and
    expr_grounding: "based.is_ground (subst expr γ)"
  shows
    "entails (subst expr (γ(var := update))) ⟷ entails (subst expr γ)"
  using congruence[OF var_grounding, of "γ(var := update)"] assms
  by (metis based.ground_subst_update congruence fun_upd_same fun_upd_triv fun_upd_upd sym symD)

end

locale symmetric_base_entailment =
  base_functional_substitution where subst = subst +
  grounding where subst = subst and to_ground = to_ground for
  subst :: "'base ⇒ ('var ⇒ 'base) ⇒ '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 γ var.
      is_ground update ⟹
      is_ground (γ var) ⟹
      (to_ground (γ var), to_ground update) ∈ I ⟹
      is_ground (expr ⋅ γ) ⟹
      (to_ground (expr ⋅ (γ(var := update))), expr') ∈ I ⟹
      (to_ground (expr ⋅ γ), expr') ∈ I"
begin

lemma symmetric_congruence:
  assumes
    update_is_ground: "is_ground update" and
    var_grounding: "is_ground (γ var)" and
    expr_grounding: "is_ground (expr ⋅ γ)" and
    var_update: "(to_ground (γ var), to_ground update) ∈ I"
  shows "(to_ground (expr ⋅ (γ(var := update))), expr') ∈ I ⟷ (to_ground (expr ⋅ γ), expr') ∈ I"
  using assms congruence[OF var_grounding, of "γ(var := update)" var] congruence
  by (metis fun_upd_same fun_upd_triv fun_upd_upd ground_subst_update sym symD)

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

end

locale entailment_lifting =
  based_functional_substitution_lifting +
  finite_variables_lifting +
  sub: symmetric_entailment
  where subst = sub_subst and vars = sub_vars and entails_def = sub_entails
  for sub_entails +
  fixes
    is_negated :: "'d ⇒ bool" and
    empty :: bool and
    connective :: "bool ⇒ bool ⇒ bool" and
    entails_def
  assumes
    is_negated_subst: "⋀expr σ. is_negated (subst expr σ) ⟷ is_negated expr" and
    entails_def: "⋀expr. entails_def expr ⟷
      (if is_negated expr then Not else (λx. x))
        (Finite_Set.fold connective empty (sub_entails  ` to_set expr))"
begin

notation sub_entails ("(⊨⇩s _)" [50] 50)
notation entails_def ("(⊨ _)" [50] 50)

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

  moreover then have "∀sub ∈ to_set expr. (⊨⇩s sub ⋅⇩s γ(var := update)) ⟷ ⊨⇩s sub ⋅⇩s γ"
    using sub.symmetric_congruence[of update γ] 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