Theory First_Order_Clause.Nonground_Context

theory Nonground_Context
  imports
    Generic_Context
    Nonground_Term
begin


section ‹Nonground Contexts and Substitutions›

locale ground_context = "context" where 
  hole = ground_hole and apply_context = apply_ground_context and
  compose_context = compose_ground_context 
for ground_hole apply_ground_context compose_ground_context
begin

notation compose_ground_context (infixl ‹∘⇩c⇩G› 75)
notation ground_hole (‹□⇩G›)
notation apply_ground_context (‹_⟨_⟩⇩G› [1000, 0] 1000)

end

locale context_properties =
   based_substitution +
   grounding +
   variables_in_base_imgu

locale nonground_context =
   "term": nonground_term where
   term_to_ground = term_to_ground and term_subst = term_subst and term_vars = term_vars  +

   context_properties where
   base_vars = term_vars and base_subst = term_subst and base_is_ground = term_is_ground and
   to_ground = to_ground +

  "context" +

  ground_context: ground_context where apply_ground_context = apply_ground_context
for
  term_to_ground :: "'t ⇒ 't⇩G" and
  term_subst :: "'t ⇒ 'subst ⇒ 't" and
  term_vars :: "'t ⇒ 'v set" and
  to_ground :: "'c ⇒ 'c⇩G" and
  apply_ground_context :: "'c⇩G ⇒ 't⇩G ⇒ 't⇩G" +
assumes
  (* TODO: Separate *)
  hole_if_context_ident [simp]: "c⟨t⟩ = t ⟹ c = □" and

  term_to_ground_context_to_ground [simp]:
    "⋀c t. term.to_ground c⟨t⟩ = (to_ground c)⟨term.to_ground t⟩⇩G" and
  term_from_ground_context_from_ground [simp]:
    "⋀c⇩G t⇩G. term.from_ground c⇩G⟨t⇩G⟩⇩G = (from_ground c⇩G)⟨term.from_ground t⇩G⟩" and
  apply_context_is_ground [simp]: "⋀c t. term.is_ground c⟨t⟩ ⟷ is_ground c ∧ term.is_ground t" and
  from_ground_compose [simp]: "⋀c c'. from_ground (c ∘⇩c⇩G c') = from_ground c ∘⇩c from_ground c'" and
  apply_context_vars [simp]: "⋀c t. term.vars c⟨t⟩ = vars c ∪ term.vars t" and
  apply_context_subst [simp]: "⋀c t σ. c⟨t⟩ ⋅t σ = (subst c σ)⟨t ⋅t σ⟩" and
  context_Var: "⋀x t. x ∈ term.vars t ⟹ (∃c. t = c⟨term.Var x⟩)" and
 
  (* TODO: Simplify? + Separate? *)
  subst_to_context: 
    "t ⋅t γ = c⇩G⟨t⇩G⟩ ⟹ term.is_ground (t ⋅t γ) ⟹
      (∃c t'. t = c⟨t'⟩ ∧ t' ⋅t γ = t⇩G ∧ subst c γ = c⇩G) ∨
      (∃c c⇩G' x. t = c⟨term.Var x⟩ ∧ c⇩G = (subst c γ) ∘⇩c c⇩G')"
begin

notation subst (infixl "⋅t⇩c" 67)

lemma term_from_ground_context_to_ground:
  assumes "is_ground c"
  shows "term.from_ground (to_ground c)⟨t⇩G⟩⇩G = c⟨term.from_ground t⇩G⟩"
  using assms
  by simp

lemmas safe_unfolds =
  term_to_ground_context_to_ground
  term_from_ground_context_from_ground

lemma composed_context_is_ground [simp]: "is_ground (c ∘⇩c c') ⟷ is_ground c ∧ is_ground c'"
  by (metis term.exists_ground apply_context_is_ground compose_context_iff)

lemma ground_context_ident_iff_hole [simp]: "c⟨t⟩⇩G = t ⟷ c = □⇩G"
  by (metis hole_if_context_ident from_ground_eq ground_context.apply_hole
      term_from_ground_context_from_ground)

lemma from_ground_hole [simp]: "from_ground c⇩G = □ ⟷ c⇩G = □⇩G"
  by (metis apply_hole apply_context_is_ground from_ground_inverse ground_context_ident_iff_hole 
      term.exists_ground term_to_ground_context_to_ground to_ground_inverse)

lemma hole_simps [simp]: "from_ground □⇩G = □" "to_ground □ = □⇩G"
  using from_ground_inverse from_ground_hole
  by metis+

lemma to_ground_compose [simp]: 
  assumes "is_ground c" "is_ground c'"
  shows "to_ground (c ∘⇩c c') = to_ground c ∘⇩c⇩G to_ground c'"
  using from_ground_compose assms
  by (metis from_ground_inverse to_ground_inverse)

lemma hole_subst [simp]: "□ ⋅t⇩c σ = □"
  by (metis all_subst_ident_if_ground apply_hole apply_context_is_ground term.exists_ground)

lemma subst_into_Var:
  assumes 
    t_γ: "t ⋅t γ = c⇩G⟨t⇩G⟩" and
    t_grounding: "term.is_ground (t ⋅t γ)" and
    not_subst_into_Fun: "∄c t'. t = c⟨t'⟩ ∧ t' ⋅t γ = t⇩G ∧ c ⋅t⇩c γ = c⇩G ∧ ¬ term.is_Var t'"
shows "∃c t' c⇩G'. t = c⟨t'⟩ ∧ term.is_Var t' ∧ c⇩G = (c ⋅t⇩c γ) ∘⇩c c⇩G'"
proof (cases "∃c t'. t = c⟨t'⟩ ∧ t' ⋅t γ = t⇩G ∧ c ⋅t⇩c γ = c⇩G")
  case True

  then obtain c t' where 
    t: "t = c⟨t'⟩" and
    c_γ: "c ⋅t⇩c γ = c⇩G" and
    "t' ⋅t γ = t⇩G"
    by metis

  then obtain x where t': "t' = term.Var x" and exists_nonground: "term.exists_nonground"
    using not_subst_into_Fun 
    by presburger

  show ?thesis
  proof (intro exI conjI impI; (rule t t')?)

    show "c⇩G = (c ⋅t⇩c γ) ∘⇩c □"
      by (simp add: c_γ)
  next

    show "¬ term.is_ground t'"
      using t' term.vars_id_subst[OF exists_nonground] term.no_vars_if_is_ground
      by auto
  qed
next
  case False

  then show ?thesis
    using subst_to_context[OF t_γ t_grounding]
    by (metis apply_context_is_ground subst_ident_if_ground t_γ
        term.all_subst_ident_if_ground)
qed

end

(* TODO: not minimal assumptions *)
locale occurences =
  nonground_context where term_vars = term_vars and apply_context = apply_context
for apply_context :: "'c ⇒ 't ⇒ 't" and term_vars :: "'t ⇒ 'v set" +
fixes occurences :: "'t ⇒ 'v ⇒ nat"
assumes
  occurences:
  "⋀t⇩G c x. term.exists_nonground ⟹ term.is_ground t⇩G ⟹
      occurences (c⟨term.Var x⟩) x = Suc (occurences (c⟨t⇩G⟩) x)" and
  vars_occurences: "⋀x t. x ∈ term.vars t ⟷ 0 < occurences t x"
begin

lemma is_ground_no_occurences: "term.is_ground t ⟹ occurences t x = 0"
  using vars_occurences term.no_vars_if_is_ground 
  by auto

lemma occurences_obtain_context:
  assumes update: "term.is_ground t⇩G" and occurences_in_t: "occurences t x = Suc n" 
  obtains c where 
    "t = c⟨term.Var x⟩"
    "occurences c⟨t⇩G⟩ x = n"
proof -

  obtain c where t: "t = c⟨term.Var x⟩"
    using occurences_in_t context_Var vars_occurences zero_less_Suc 
    by presburger

  moreover have "occurences c⟨t⇩G⟩ x = n"
    using assms is_ground_no_occurences occurences
    unfolding t
    by fastforce

  ultimately show ?thesis
    using that
    by metis
qed

lemma one_occurence_obtain_context:
  assumes "occurences t x = 1"
  obtains c where
    "t = c⟨term.Var x⟩"
    "x ∉ vars c"
  using term.exists_ground occurences_obtain_context[OF _ assms[unfolded One_nat_def]]
  by (metis Un_iff apply_context_vars order_less_irrefl vars_occurences)

end

locale nonground_term_with_context =
  "term": nonground_term +
  "context": nonground_context where
  is_ground = context_is_ground and subst = context_subst and vars = context_vars and
  from_ground = context_from_ground and to_ground = context_to_ground +
  occurences where
  is_ground = context_is_ground and subst = context_subst and vars = context_vars and
  from_ground = context_from_ground and to_ground = context_to_ground
for context_is_ground context_subst context_vars context_from_ground context_to_ground
begin

(* TODO: How to not have it multiple times?*)
notation context_subst (infixl "⋅t⇩c" 67)

end

end