Theory Grounded_Ordered_Resolution

theory Grounded_Ordered_Resolution
  imports
    Ordered_Resolution
    Ground_Ordered_Resolution

    First_Order_Clause.Grounded_Selection_Function
    First_Order_Clause.Nonground_Inference
    Saturation_Framework.Lifting_to_Non_Ground_Calculi

    Polynomial_Factorization.Missing_List
begin

locale grounded_ordered_resolution_calculus =
  ordered_resolution_calculus where
  select = select and welltyped = welltyped and
  term_from_ground = "term_from_ground :: 't⇩G ⇒ 't" and id_subst = "id_subst :: 'subst" +

  grounded_selection_function where
  select = select and atom_subst = "(⋅t)" and atom_vars = "term.vars" and
  atom_from_ground = "term.from_ground" and atom_to_ground = "term.to_ground" and
  is_ground_instance = is_ground_instance
  for
    select :: "'t select" and
    welltyped :: "('v :: infinite, 'ty) var_types ⇒ 't ⇒ 'ty ⇒ bool"
begin

sublocale ground: ground_ordered_resolution_calculus where
  less⇩t = "(≺⇩t⇩G)" and select = select⇩G
rewrites
  "multiset_extension.multiset_extension (≺⇩t⇩G) ground.literal_to_mset = (≺⇩l⇩G)" and
  "multiset_extension.multiset_extension (≺⇩l⇩G) (λx. x) = (≺⇩c⇩G)" and
  "⋀l⇩G C⇩G. ground.is_maximal l⇩G C⇩G ⟷ ground_is_maximal l⇩G C⇩G" and
  "⋀l⇩G C⇩G. ground.is_strictly_maximal l⇩G C⇩G ⟷ ground_is_strictly_maximal l⇩G C⇩G"
  unfolding is_maximal_rewrite[symmetric] is_strictly_maximal_rewrite[symmetric]
  by unfold_locales simp_all

abbreviation is_inference_ground_instance_one_premise where
  "is_inference_ground_instance_one_premise D C ι⇩G γ ≡
     case (D, C) of ((𝒱', D), (𝒱, C)) ⇒
      inference.is_ground (Infer [D] C ⋅ι γ) ∧
      ι⇩G = inference.to_ground (Infer [D] C ⋅ι γ) ∧
      type_preserving_on (clause.vars C) 𝒱 γ ∧
      𝒱 = 𝒱' ∧
      infinite_variables_per_type 𝒱"

abbreviation is_inference_ground_instance_two_premises where
  "is_inference_ground_instance_two_premises D E C ι⇩G γ ρ⇩1 ρ⇩2 ≡
    case (D, E, C) of ((𝒱⇩2, D), (𝒱⇩1, E), (𝒱⇩3, C)) ⇒
      term.is_renaming ρ⇩1 ∧
      term.is_renaming ρ⇩2 ∧
      clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {} ∧
      inference.is_ground (Infer [D ⋅ ρ⇩2, E ⋅ ρ⇩1] C ⋅ι γ) ∧
      ι⇩G = inference.to_ground (Infer [D ⋅ ρ⇩2, E ⋅ ρ⇩1] C ⋅ι γ) ∧
      type_preserving_on (clause.vars C) 𝒱⇩3 γ ∧
      infinite_variables_per_type 𝒱⇩1 ∧
      infinite_variables_per_type 𝒱⇩2 ∧
      infinite_variables_per_type 𝒱⇩3"

abbreviation is_inference_ground_instance where
  "is_inference_ground_instance ι ι⇩G γ ≡
  (case ι of
      Infer [D] C ⇒ is_inference_ground_instance_one_premise D C ι⇩G γ
    | Infer [D, E] C ⇒ ∃ρ⇩1 ρ⇩2. is_inference_ground_instance_two_premises D E C ι⇩G γ ρ⇩1 ρ⇩2
    | _ ⇒ False)
  ∧ ι⇩G ∈ ground.G_Inf"

definition inference_ground_instances where
  "inference_ground_instances ι = { ι⇩G | ι⇩G γ. is_inference_ground_instance ι ι⇩G γ }"

lemma is_inference_ground_instance:
  "is_inference_ground_instance ι ι⇩G γ ⟹ ι⇩G ∈ inference_ground_instances ι"
  unfolding inference_ground_instances_def
  by blast

lemma is_inference_ground_instance_one_premise:
  assumes "is_inference_ground_instance_one_premise D C ι⇩G γ" "ι⇩G ∈ ground.G_Inf"
  shows "ι⇩G ∈ inference_ground_instances (Infer [D] C)"
  using assms
  unfolding inference_ground_instances_def
  by auto

lemma is_inference_ground_instance_two_premises:
  assumes "is_inference_ground_instance_two_premises D E C ι⇩G γ ρ⇩1 ρ⇩2" "ι⇩G ∈ ground.G_Inf"
  shows "ι⇩G ∈ inference_ground_instances (Infer [D, E] C)"
  using assms
  unfolding inference_ground_instances_def
  by auto

lemma ground_inference⇩_concl_in_ground_instances:
  assumes "ι⇩G ∈ inference_ground_instances ι"
  shows "concl_of ι⇩G ∈ uncurried_ground_instances (concl_of ι)"
proof -
  obtain "premises" C 𝒱 where
    ι: "ι = Infer premises (C, 𝒱)"
    using Calculus.inference.exhaust
    by (metis prod.collapse)

  show ?thesis
    using assms
    unfolding ι inference_ground_instances_def ground_instances_def
    by (cases "premises" rule: list_4_cases) auto
qed

lemma ground_inference_red_in_ground_instances_of_concl:
  assumes "ι⇩G ∈ inference_ground_instances ι"
  shows "ι⇩G ∈ ground.Red_I (uncurried_ground_instances (concl_of ι))"
proof -
  from assms have "ι⇩G ∈ ground.G_Inf"
    unfolding inference_ground_instances_def
    by blast

  moreover have "concl_of ι⇩G ∈ uncurried_ground_instances (concl_of ι)"
    using assms ground_inference⇩_concl_in_ground_instances
    by auto

  ultimately show "ι⇩G ∈ ground.Red_I (uncurried_ground_instances (concl_of ι))"
    using ground.Red_I_of_Inf_to_N
    by blast
qed

sublocale lifting:
  tiebreaker_lifting
    "⊥⇩F"
    inferences
    ground.G_Bot
    ground.G_entails
    ground.G_Inf
    ground.GRed_I
    ground.GRed_F
    uncurried_ground_instances
    "Some ∘ inference_ground_instances"
    typed_tiebreakers
proof (unfold_locales; (intro impI typed_tiebreakers.wfp typed_tiebreakers.transp)?)

  show "⊥⇩F ≠ {}"
    using obtain_infinite_variables_per_type_on''[of "{}"]
    by auto
next
  fix bottom
  assume "bottom ∈ ⊥⇩F"

  then show "uncurried_ground_instances bottom ≠ {}"
    unfolding ground_instances_def
    by fastforce
next
  fix bottom
  assume "bottom ∈ ⊥⇩F"

  then show "uncurried_ground_instances bottom ⊆ ground.G_Bot"
    unfolding ground_instances_def
    by auto
next
  fix C :: "('t, 'v, 'ty) typed_clause"

  assume "uncurried_ground_instances C ∩ ground.G_Bot ≠ {}"

  moreover then have "snd C = {#}"
    unfolding ground_instances_def
    by simp

  then have "C = (fst C, {#})"
    by (metis split_pairs)

  ultimately show "C ∈ ⊥⇩F"
    unfolding ground_instances_def
    by blast
next
  fix ι :: "('t, 'v, 'ty) typed_clause inference"

  show "the ((Some ∘ inference_ground_instances) ι) ⊆
          ground.GRed_I (uncurried_ground_instances (concl_of ι))"
    using ground_inference_red_in_ground_instances_of_concl
    by auto
qed
end

context ordered_resolution_calculus
begin

abbreviation grounded_inference_ground_instances where
  "grounded_inference_ground_instances select⇩G ≡
    grounded_ordered_resolution_calculus.inference_ground_instances
      (⊙) apply_subst (⋅t) term.vars term.to_ground (≺⇩t) id_subst term.from_ground select⇩G welltyped"

sublocale
  lifting_intersection
    inferences
    "{{#}}"
    select⇩G⇩s
    "ground_ordered_resolution_calculus.G_Inf (≺⇩t⇩G)"
    "λ_. ground_ordered_resolution_calculus.G_entails"
    "ground_ordered_resolution_calculus.GRed_I (≺⇩t⇩G)"
    "λ_. ground_ordered_resolution_calculus.GRed_F (≺⇩t⇩G)"
    "⊥⇩F"
    "λ_. uncurried_ground_instances"
    "λselect⇩G. Some ∘ grounded_inference_ground_instances select⇩G"
    typed_tiebreakers
proof (unfold_locales; (intro ballI)?)

  show "select⇩G⇩s ≠ {}"
    using select⇩G_simple
    unfolding select⇩G⇩s_def
    by blast
next
  fix select⇩G
  assume "select⇩G ∈ select⇩G⇩s"

  then interpret grounded_ordered_resolution_calculus
    where select⇩G = select⇩G
    by unfold_locales (simp add: select⇩G⇩s_def)

  show "consequence_relation ground.G_Bot ground.G_entails"
    using ground.consequence_relation_axioms .

  show "tiebreaker_lifting
          ⊥⇩F
          inferences
          ground.G_Bot
          ground.G_entails
          ground.G_Inf
          ground.GRed_I
          ground.GRed_F
          uncurried_ground_instances
          (Some ∘ inference_ground_instances)
          typed_tiebreakers"
    by unfold_locales
qed

end

end