Theory First_Order_Clause.Nonground_Entailment

theory Nonground_Entailment
  imports
    Nonground_Context
    Nonground_Clause_With_Equality
    Ground_Term_Rewrite_System
    Entailment_Lifting
    Fold_Extra
begin

section ‹Entailment›

context nonground_clause
begin

lemma not_literal_entails [simp]:
  "¬ upair ` I ⊫l Neg a ⟷ upair ` I ⊫l Pos a"
  "¬ upair ` I ⊫l Pos a ⟷ upair ` I ⊫l Neg a"
  by auto

lemmas literal_entails_unfolds =
  not_literal_entails
  true_lit_simps

end

locale clause_entailment =
  nonground_clause where 
  term_vars = "term_vars :: 't ⇒ 'v set" and term_to_ground = "term_to_ground :: 't ⇒ 't⇩G" +

  nonground_term_with_context +

  ground_term_rewrite_system where
  apply_context = apply_ground_context and compose_context = compose_ground_context and
  hole = ground_hole +

  fixes I :: "'t⇩G rel"
  assumes
    trans: "trans I" and
    sym: "sym I" and
    compatible_with_ground_context: "compatible_with_context I"
begin

lemma symmetric_context_congruence:
  assumes "(t, t') ∈ I"
  shows "(c⟨t⟩⇩G, t'') ∈ I ⟷ (c⟨t'⟩⇩G, t'') ∈ I"
  by (meson assms compatible_with_ground_context compatible_with_contextD sym trans symD transE)

lemma symmetric_upair_context_congruence:
  assumes "Upair t t' ∈ upair ` I"
  shows "Upair c⟨t⟩⇩G t'' ∈  upair ` I ⟷ Upair c⟨t'⟩⇩G t'' ∈  upair ` I"
  using assms uprod_mem_image_iff_prod_mem[OF sym] symmetric_context_congruence
  by simp

lemma upair_compatible_with_gctxtI [intro]:
  "Upair t t' ∈ upair ` I ⟹ Upair c⟨t⟩⇩G c⟨t'⟩⇩G ∈ upair ` I"
  using compatible_with_ground_context
  unfolding compatible_with_context_def
  by (simp add: sym)

sublocale "term": symmetric_base_entailment where vars = "term.vars :: 't ⇒ 'v set" and
  id_subst = Var and comp_subst = "(⊙)" and subst = "(⋅t)" and to_ground = term.to_ground and
  from_ground = term.from_ground
proof unfold_locales
  fix γ :: "'v ⇒ 't" and t t' update x

  assume
    update_is_ground: "term.is_ground update" and
    var_grounding: "term.is_ground (γ x)" and
    var_update: "(term.to_ground (γ x), term.to_ground update) ∈ I" and
    term_grounding: "term.is_ground (t ⋅t γ)" and
    updated_term: "(term.to_ground (t ⋅t γ(x := update)), t') ∈ I"

  from term_grounding updated_term
  show "(term.to_ground (t ⋅t γ), t') ∈ I"
  proof (induction "occurences t x" arbitrary: t)
    case 0

    then have "x ∉ term.vars t"
      using context.context_Var occurences
      by auto

    then have "t ⋅t γ(x := update) = t ⋅t γ"
      using term.subst_reduntant_upd
      by presburger

    with 0 show ?case
      by argo
  next
    case (Suc n)

    obtain c where t: "t = c⟨Var x⟩"
      using Suc.hyps(2)
      by (metis context.context_Var vars_occurences zero_less_Suc)

    let ?t' = "c⟨update⟩"

    have "(term.to_ground (?t' ⋅t γ), t') ∈ I"
    proof (rule Suc.hyps)
      show "n = occurences ?t' x"
        using Suc.hyps(2) occurences t update_is_ground 
        by auto
    next
      show "term.is_ground (?t' ⋅t γ)"
        using Suc.prems(1) t update_is_ground 
        by auto
    next
      show "(term.to_ground (?t' ⋅t γ(x := update)), t') ∈ I"
        using Suc.prems(2) update_is_ground
        unfolding t
        by auto
    qed

    then show ?case
      using symmetric_context_congruence update_is_ground var_update
      unfolding t
      by auto
  qed
qed (rule sym)

sublocale atom: symmetric_entailment
  where comp_subst = "(⊙)" and id_subst = Var
    and base_subst = "(⋅t)" and base_vars = term.vars and subst = "(⋅a)" and vars = atom.vars
    and base_to_ground = term.to_ground and base_from_ground = term.from_ground and I = I
    and entails_def = "λa. atom.to_ground a ∈ upair ` I"
proof unfold_locales
  fix a :: "'t atom" and  γ var update P

  assume assms:
    "term.is_ground update"
    "term.is_ground (γ var)"
    "(term.to_ground (γ var), term.to_ground update) ∈ I"
    "atom.is_ground (a ⋅a γ)"
    "(atom.to_ground (a ⋅a γ(var := update)) ∈ upair ` I)"

  show "(atom.to_ground (a ⋅a γ) ∈ upair ` I)"
  proof(cases a)
    case (Upair t t')

    moreover have
      "(term.to_ground (t' ⋅t γ), term.to_ground (t ⋅t γ)) ∈ I ⟷
       (term.to_ground (t ⋅t γ), term.to_ground (t' ⋅t γ)) ∈ I"
      by (metis local.sym symD)

    ultimately show ?thesis
      using assms
      unfolding atom.to_ground_def atom.subst_def atom.vars_def
      by(auto simp: sym term.simultaneous_congruence)
  qed
qed (simp_all add: sym)

sublocale literal: entailment_lifting_conj
  where comp_subst = "(⊙)" and id_subst = Var
    and base_subst = "(⋅t)" and base_vars = term.vars and sub_subst = "(⋅a)" and sub_vars = atom.vars
    and base_to_ground = term.to_ground and base_from_ground = term.from_ground and I = I
    and sub_entails = atom.entails and map = "map_literal" and to_set = "set_literal"
    and is_negated = is_neg and entails_def = "λl. upair ` I ⊫l literal.to_ground l"
proof unfold_locales
  fix l :: "'t atom literal"

  show "(upair ` I ⊫l literal.to_ground l) =
    (if is_neg l then Not else (λx. x))
      (Finite_Set.fold (∧) True ((λa. atom.to_ground a ∈ upair ` I) ` set_literal l))"
    unfolding literal.vars_def literal.to_ground_def
    by(cases l)(auto)

qed auto

sublocale clause: entailment_lifting_disj
  where comp_subst = "(⊙)" and id_subst = Var
    and base_subst = "(⋅t)" and base_vars = term.vars
    and base_to_ground = term.to_ground and base_from_ground = term.from_ground and I = I
    and sub_subst = "(⋅l)" and sub_vars = literal.vars and sub_entails = literal.entails
    and map = image_mset and to_set = set_mset and is_negated = "λ_. False"
    and entails_def = "λC. upair ` I ⊫ clause.to_ground C"
proof unfold_locales
  fix C :: "'t clause"

  show "upair ` I ⊫ clause.to_ground C ⟷
    (if False then Not else (λx. x)) (Finite_Set.fold (∨) False (literal.entails ` set_mset C))"
    unfolding clause.to_ground_def
    by (induction C) auto

qed auto

lemma literal_compatible_with_gctxtI [intro]:
   "literal.entails (t ≈ t') ⟹ literal.entails (c⟨t⟩ ≈ c⟨t'⟩)"
  by (simp add: upair_compatible_with_gctxtI)

lemma symmetric_literal_context_congruence:
  assumes "Upair t t' ∈ upair ` I"
  shows
    "upair ` I ⊫l c⟨t⟩⇩G ≈ t'' ⟷ upair ` I ⊫l c⟨t'⟩⇩G ≈ t''"
    "upair ` I ⊫l c⟨t⟩⇩G !≈ t'' ⟷ upair ` I ⊫l c⟨t'⟩⇩G !≈ t''"
  using assms symmetric_upair_context_congruence
  by auto

end

end