Theory First_Order_Clause.Nonground_Context

theory Nonground_Context
  imports
    Generic_Context
    Nonground_Term

    Abstract_Substitution.Functional_Substitution_Lifting
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 ‹∘cG› 75)
notation ground_hole (‹□G›)
notation apply_ground_context (‹_⟨_⟩G› [1000, 0] 1000)

end

locale nonground_context =
  "term": nonground_term where term_vars = term_vars and term_to_ground = term_to_ground +
  term_based_lifting where
  sub_subst = "(⋅t)" and sub_vars = term.vars and sub_to_ground = term.to_ground and
  sub_from_ground = term.from_ground and term_vars = term.vars and term_subst = "(⋅t)" and
  term_to_ground = term.to_ground and term_from_ground = term.from_ground and
  to_ground_map = to_ground_context_map and ground_map = ground_context_map and 
  from_ground_map = from_ground_context_map and map = map_context and to_set = context_to_set and
  to_set_ground = ground_context_to_set +
  "context" +
  ground_context: ground_context where 
  apply_ground_context = apply_ground_context
for
  term_vars :: "'t ⇒ 'v set" and 
  term_to_ground :: "'t ⇒ 'tG" and
  map_context :: "('t ⇒ 't) ⇒ 'c ⇒ 'c" and
  to_ground_context_map :: "('t ⇒ 'tG) ⇒ 'c ⇒ 'cG" and
  from_ground_context_map :: "('tG ⇒ 't) ⇒ 'cG ⇒ 'c" and
  ground_context_map :: "('tG ⇒ 'tG) ⇒ 'cG ⇒ 'cG" and
  context_to_set ground_context_to_set and
  apply_ground_context :: "'cG ⇒ 'tG ⇒ 'tG" +
assumes
  hole_if_context_ident [simp]: "c⟨t⟩ = t ⟹ c = □" and
  compose_hole [simp]: "c = c ∘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]:
  "⋀cG tG. term.from_ground cG⟨tG⟩G = (from_ground cG)⟨term.from_ground tG⟩" and
  apply_context_is_ground [simp]: "⋀c t. term.is_ground c⟨t⟩ ⟷ is_ground c ∧ term.is_ground t" and
  map_compose [simp]: "⋀f c c'. map_context f (c ∘c c') = map_context f c ∘c map_context f c'" and
  from_ground_compose [simp]:
    "⋀c c'. from_ground (c ∘cG 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⟨Var x⟩)" and
 
  (* TODO: Simplify? + Separate? *)
  subst_to_context: "t ⋅t γ = cG⟨tG⟩ ⟹ term.is_ground (t ⋅t γ) ⟹
    (∃c t'. t = c⟨t'⟩ ∧ t' ⋅t γ = tG ∧ subst c γ = cG) ∨
    (∃c cG' x. t = c⟨Var x⟩ ∧ cG = (subst c γ) ∘c cG')"
begin

notation subst (infixl "⋅tc" 67)

lemma term_from_ground_context_to_ground:
  assumes "is_ground c"
  shows "term.from_ground (to_ground c)⟨tG⟩G = c⟨term.from_ground tG⟩"
  unfolding to_ground_def
  by (metis assms term_from_ground_context_from_ground to_ground_def to_ground_inverse)

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.ground_exists 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 cG = □ ⟷ cG = □G"
  by (metis apply_hole apply_context_is_ground from_ground_inverse ground_context_ident_iff_hole 
      term.ground_exists 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]: "to_ground (c ∘c c') = to_ground c ∘cG to_ground c'"
  using from_ground_compose
  unfolding to_ground_def
  by (metis conversion_map_comp from_ground_def from_ground_inverse map_compose)

lemma hole_subst [simp]: "□ ⋅tc σ = □"
  by (metis all_subst_ident_if_ground apply_hole apply_context_is_ground term.ground_exists)

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

  then obtain c t' where t: "t = c⟨t'⟩" and "t' ⋅t γ = tG" "c ⋅tc γ = cG"
    by metis

  have "is_ground cG"
    using t_γ t_grounding 
    by auto

  obtain x where t': "t' = Var x"
    using ‹c ⋅tc γ = cG› ‹t' ⋅t γ = tG› not_subst_into_Fun t
    by blast

  show ?thesis
  proof (intro exI conjI)

    show "t = c⟨t'⟩"
      using t .
  next

    show "t' = Var x"
      using t' .
  next

    show "cG = (c ⋅tc γ) ∘c □"
      by (simp add: ‹c ⋅tc γ = cG›)
  qed
next
  case False

  then show ?thesis
    using subst_to_context[OF t_γ t_grounding]
    by metis
qed

end

locale occurences =
  nonground_context where map_context = map_context and Var = Var
for 
  map_context :: "('t ⇒ 't) ⇒ 'c ⇒ 'c" and
  Var :: "'v ⇒ 't" +
fixes occurences :: "'t ⇒ 'v ⇒ nat"
assumes
  occurences:
  "⋀tG c x. term.is_ground tG ⟹ occurences (c⟨Var x⟩) x = Suc (occurences (c⟨tG⟩) x)" and
  vars_occurences: "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 
  by auto

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

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

  moreover have "occurences c⟨tG⟩ x = n"
    using assms
    unfolding t occurences[OF update]
    by linarith

  ultimately show ?thesis
    using that
    by metis
qed

lemma one_occurence_obtain_context:
  assumes "occurences t x = 1"
  obtains c where
    "t = c⟨Var x⟩"
    "x ∉ vars c"
  using term.ground_exists 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 +
  occurences
begin

(* TODO: How to not have it multiple times?*)
notation context.subst (infixl "⋅tc" 67)

end

end