Theory First_Order_Clause.Nonground_Clause_With_Equality

theory Nonground_Clause_With_Equality
  imports
    Nonground_Term
    Nonground_Clause_Generic
    Uprod_Literal_Functor
begin

section ‹Nonground Clauses with Equality›

locale nonground_clause = "term": nonground_term
begin

subsection ‹Nonground Atoms›

sublocale atom: term_based_lifting where
  sub_subst = "(⋅t)" and sub_vars = term.vars and map = map_uprod and to_set = set_uprod and
  sub_to_ground = term.to_ground and sub_from_ground = term.from_ground and
  to_ground_map = map_uprod and from_ground_map = map_uprod and ground_map = map_uprod and
  to_set_ground = set_uprod
  by unfold_locales

(* TODO: *)
notation atom.subst (infixl "⋅a" 67)

lemma vars_atom [simp]: "atom.vars (Upair t⇩1 t⇩2) = term.vars t⇩1 ∪ term.vars t⇩2"
  by (simp_all add: atom.vars_def)

lemma subst_atom [simp]:
  "Upair t⇩1 t⇩2 ⋅a σ = Upair (t⇩1 ⋅t σ) (t⇩2 ⋅t σ)"
  unfolding atom.subst_def
  by simp_all

lemma atom_from_ground_term_from_ground [simp]:
  "atom.from_ground (Upair t⇩G⇩1 t⇩G⇩2) = Upair (term.from_ground t⇩G⇩1) (term.from_ground t⇩G⇩2)"
  by (simp add: atom.from_ground_def)

lemma atom_to_ground_term_to_ground [simp]:
  "atom.to_ground (Upair t⇩1 t⇩2) = Upair (term.to_ground t⇩1) (term.to_ground t⇩2)"
  by (simp add: atom.to_ground_def)

lemma atom_is_ground_term_is_ground [simp]:
  "atom.is_ground (Upair t⇩1 t⇩2) ⟷ term.is_ground t⇩1 ∧ term.is_ground t⇩2"
  by simp

lemma obtain_from_atom_subst:
  assumes "Upair t⇩1' t⇩2' = a ⋅a σ"
  obtains t⇩1 t⇩2
  where "a = Upair t⇩1 t⇩2" "t⇩1' = t⇩1 ⋅t σ" "t⇩2' = t⇩2 ⋅t σ"
  using assms
  unfolding atom.subst_def
  by(cases a) force

subsection ‹Nonground Literals›

sublocale nonground_clause_generic where 
  atom_vars = atom.vars and atom_subst = "(⋅a)" and atom_to_ground = atom.to_ground and
  atom_from_ground = atom.from_ground
  by unfold_locales

lemma obtain_from_pos_literal_subst:
  assumes "l ⋅l σ = t⇩1' ≈ t⇩2'"
  obtains t⇩1 t⇩2
  where "l = t⇩1 ≈ t⇩2" "t⇩1' = t⇩1 ⋅t σ" "t⇩2' = t⇩2 ⋅t σ"
  using assms obtain_from_atom_subst subst_pos_stable
  by (metis is_pos_def literal.sel(1) subst_literal(3))

lemma obtain_from_neg_literal_subst:
  assumes "l ⋅l σ = t⇩1' !≈ t⇩2'"
  obtains t⇩1 t⇩2
  where "l = t⇩1 !≈ t⇩2" "t⇩1 ⋅t σ = t⇩1'" "t⇩2 ⋅t σ = t⇩2'"
  using assms obtain_from_atom_subst subst_neg_stable
  by (metis literal.collapse(2) literal.disc(2) literal.sel(2) subst_literal(3))

lemmas obtain_from_literal_subst = obtain_from_pos_literal_subst obtain_from_neg_literal_subst

subsection ‹Nonground Literals - Alternative›

lemma uprod_literal_subst_eq_literal_subst: "map_uprod_literal (λt. t ⋅t σ) l = l ⋅l σ"
  unfolding atom.subst_def literal.subst_def
  by auto

lemma uprod_literal_vars_eq_literal_vars: "⋃ (term.vars ` uprod_literal_to_set l) = literal.vars l"
  unfolding literal.vars_def atom.vars_def
  by(cases l) simp_all

lemma uprod_literal_from_ground_eq_literal_from_ground:
  "map_uprod_literal term.from_ground l⇩G = literal.from_ground l⇩G"
  unfolding literal.from_ground_def atom.from_ground_def ..

lemma uprod_literal_to_ground_eq_literal_to_ground:
  "map_uprod_literal term.to_ground l = literal.to_ground l"
  unfolding literal.to_ground_def atom.to_ground_def ..

sublocale uprod_literal: term_based_lifting where
  sub_subst = "(⋅t)" and sub_vars = term.vars and map = map_uprod_literal and
  to_set = uprod_literal_to_set and sub_to_ground = term.to_ground and
  sub_from_ground = term.from_ground and to_ground_map = map_uprod_literal and
  from_ground_map = map_uprod_literal and ground_map = map_uprod_literal and
  to_set_ground = uprod_literal_to_set
rewrites
  uprod_literal_subst [simp]: "⋀l σ. uprod_literal.subst l σ = literal.subst l σ" and
  uprod_literal_vars [simp]: "⋀l. uprod_literal.vars l = literal.vars l" and
  uprod_literal_from_ground [simp]: "⋀l⇩G. uprod_literal.from_ground l⇩G = literal.from_ground l⇩G" and
  uprod_literal_to_ground [simp]:"⋀l. uprod_literal.to_ground l = literal.to_ground l"
proof unfold_locales

  interpret term_based_lifting where
    sub_vars = term.vars and sub_subst = "(⋅t)" and map = map_uprod_literal and
    to_set = uprod_literal_to_set and sub_to_ground = term.to_ground and
    sub_from_ground = term.from_ground and to_ground_map = map_uprod_literal and
    from_ground_map = map_uprod_literal and ground_map = map_uprod_literal and
    to_set_ground = uprod_literal_to_set
    by unfold_locales

  fix l and σ

  show "subst l σ = l ⋅l σ"
    unfolding subst_def literal.subst_def atom.subst_def
    by simp

  show "vars l = literal.vars l"
    unfolding atom.vars_def vars_def literal.vars_def
    by(cases l) simp_all

  fix l⇩G 
  show "from_ground l⇩G = literal.from_ground l⇩G"
    unfolding from_ground_def literal.from_ground_def atom.from_ground_def..

  fix l
  show "to_ground l = literal.to_ground l"
    unfolding to_ground_def literal.to_ground_def atom.to_ground_def ..
qed

subsection ‹Nonground Clauses›

lemmas clause_safe_unfolds =
  atom_to_ground_term_to_ground
  literal_to_ground_atom_to_ground
  atom_from_ground_term_from_ground
  literal_from_ground_atom_from_ground
  literal_from_ground_polarity_stable
  subst_atom
  subst_literal
  vars_atom
  vars_literal

end

end