Theory Ordered_Resolution_Completeness

theory Ordered_Resolution_Completeness
  imports
    Grounded_Ordered_Resolution
    Ground_Ordered_Resolution_Completeness
begin

section ‹Completeness›

context grounded_ordered_resolution_calculus
begin

subsection ‹Liftings›

lemma factoring_lifting:
  fixes
    D⇩G C⇩G :: "'t⇩G clause" and
    D C :: "'t clause" and
    γ :: 'subst
  defines
    [simp]: "D⇩G ≡ clause.to_ground (D ⋅ γ)" and
    [simp]: "C⇩G ≡ clause.to_ground (C ⋅ γ)"
  assumes
    ground_factoring: "ground.factoring D⇩G C⇩G" and
    D_grounding: "clause.is_ground (D ⋅ γ)" and
    C_grounding: "clause.is_ground (C ⋅ γ)" and
    select: "clause.from_ground (select⇩G D⇩G) = (select D) ⋅ γ" and
    type_preserving_γ: "type_preserving_on (clause.vars D) 𝒱 γ" and
    𝒱: "infinite_variables_per_type 𝒱"
  obtains C'
  where
    "factoring (𝒱, D) (𝒱, C')"
    "Infer [D⇩G] C⇩G ∈ inference_ground_instances (Infer [(𝒱, D)] (𝒱, C'))"
    "C' ⋅ γ = C ⋅ γ"
  using ground_factoring
proof(cases D⇩G C⇩G rule: ground.factoring.cases)
  case ground_factoringI: (factoringI l⇩G D⇩G' t⇩G)

  have "D ≠ {#}"
    using ground_factoringI(3)
    by auto

  then obtain l⇩1 where
    l⇩1_is_maximal: "is_maximal l⇩1 D" and
    l⇩1_γ_is_maximal: "is_maximal (l⇩1 ⋅l γ) (D ⋅ γ)"
    using that obtain_maximal_literal D_grounding
    by blast

  obtain t⇩1 where
    l⇩1: "l⇩1 = (Pos t⇩1)" and
    l⇩1_γ: "l⇩1 ⋅l γ = (Pos (term.from_ground t⇩G))" and
    t⇩1_γ: "t⇩1 ⋅t γ = term.from_ground t⇩G"
  proof-
    have "is_maximal (literal.from_ground l⇩G) (D ⋅ γ)"
      using D_grounding ground_factoringI(2)
      by auto

    then have "l⇩1 ⋅l γ = (Pos (term.from_ground t⇩G))"
      unfolding ground_factoringI(4)
      using unique_maximal_in_ground_clause[OF D_grounding l⇩1_γ_is_maximal]
      by simp

    then show ?thesis
      using that
      by (metis Neg_atm_of_iff clause_safe_unfolds(9) literal.collapse(1) literal.sel(1)
          subst_polarity_stable(2))
  qed

  obtain l⇩2 D' where
    l⇩2_γ: "l⇩2 ⋅l γ = Pos (term.from_ground t⇩G)" and
    D: "D = add_mset l⇩1 (add_mset l⇩2 D')"
  proof-

    obtain D'' where D: "D = add_mset l⇩1 D''"
      using maximal_in_clause[OF l⇩1_is_maximal]
      by (meson multi_member_split)

    moreover have "D ⋅ γ = clause.from_ground (add_mset l⇩G ( add_mset l⇩G D⇩G'))"
      using ground_factoringI(3) C⇩G_def
      by (metis D⇩G_def D_grounding clause.to_ground_inverse)

    ultimately have "D'' ⋅ γ = add_mset (literal.from_ground l⇩G) (clause.from_ground D⇩G')"
      using l⇩1_γ
      by (simp add: ground_factoringI(4))

    then obtain l⇩2 where "l⇩2 ⋅l γ = Pos (term.from_ground t⇩G)" "l⇩2 ∈# D''"
      unfolding clause.subst_def ground_factoringI
      using msed_map_invR
      by force

    then show ?thesis
      using that
      unfolding D
      by (metis mset_add)
  qed

  then obtain t⇩2 where
    l⇩2: "l⇩2 = (Pos t⇩2)" and
    t⇩2_γ: "t⇩2 ⋅t γ = term.from_ground t⇩G"
    unfolding ground_factoringI(2)
    by (metis clause_safe_unfolds(9) is_pos_def literal.sel(1) subst_polarity_stable(2))

  have D'_γ: "D' ⋅ γ = clause.from_ground D⇩G'"
    using D D_grounding ground_factoringI l⇩1_γ l⇩2_γ
    by force

  obtain μ where
    type_preserving_μ: "type_preserving_on (clause.vars D) 𝒱 μ" and
    imgu: "term.is_imgu μ {{t⇩1, t⇩2}}"
  proof (rule obtain_type_preserving_on_imgu[OF _ that], intro conjI)

    show "t⇩1 ⋅t γ = t⇩2 ⋅t γ"
      using t⇩1_γ t⇩2_γ 
      by argo
  next

    show "type_preserving_on (term.vars t⇩1 ∪ term.vars t⇩2) 𝒱 γ"
      using type_preserving_γ
      unfolding D l⇩1 l⇩2
      by auto
  qed

  obtain σ where γ: "γ = μ ⊙ σ"
    using term.obtain_imgu_absorption[of γ, OF _ imgu] t⇩1_γ t⇩2_γ
    by auto

  let ?C'' = "add_mset l⇩1 D'"
  let ?C' = "?C'' ⋅ μ"

  show ?thesis
  proof(rule that)

    show factoring: "factoring (𝒱, D) (𝒱, ?C')"
    proof (rule factoringI; (rule D imgu type_preserving_μ refl 𝒱)?)

      show "select D = {#}"
        using ground_factoringI(1) select
        by simp
    next

      have "l⇩1 ⋅l μ ∈# D ⋅ μ"
        using l⇩1_is_maximal clause.subst_in_to_set_subst maximal_in_clause
        by blast

      then show "is_maximal (l⇩1 ⋅l μ) (D ⋅ μ)"
        using is_maximal_if_grounding_is_maximal D_grounding l⇩1_γ_is_maximal
        unfolding γ
        by auto       
    next

      show "D = add_mset l⇩1 (add_mset (Pos t⇩2) D')"
        unfolding D l⇩2 ..
    next
      show "l⇩1 = Pos t⇩1"
        using l⇩1 .
    qed

    show C'_γ: "?C' ⋅ γ = C ⋅ γ"
    proof-
      have "term.is_idem μ"
        using imgu
        unfolding term.is_imgu_iff_is_idem_and_is_mgu
        by blast

      then have μ_γ: "μ ⊙ γ = γ"
        unfolding γ term.is_idem_def term.assoc[symmetric]
        by argo

      have "C ⋅ γ = clause.from_ground (add_mset (Pos t⇩G) D⇩G')"
        using ground_factoringI(5) clause.to_ground_eq[OF C_grounding clause.ground_is_ground]
        unfolding C⇩G_def
        by (metis clause.from_ground_inverse ground_factoringI(4))

      also have "... = ?C'' ⋅ γ"
        using t⇩1_γ D'_γ l⇩1_γ
        by auto

      also have "... = ?C' ⋅ γ"
        unfolding clause.subst_comp_subst[symmetric] μ_γ ..

      finally show ?thesis ..
    qed

    show "Infer [D⇩G] C⇩G ∈ inference_ground_instances (Infer [(𝒱, D)] (𝒱, ?C'))"
    proof (rule is_inference_ground_instance_one_premise)
      show "is_inference_ground_instance_one_premise (𝒱, D) (𝒱, ?C') (Infer [D⇩G] C⇩G) γ"
      proof(unfold split, intro conjI; (rule refl 𝒱)?)

        show "inference.is_ground (Infer [D] ?C' ⋅ι γ)"
          using C_grounding D_grounding C'_γ
          by auto
      next

        show "Infer [D⇩G] C⇩G = inference.to_ground (Infer [D] ?C' ⋅ι γ)"
          using C'_γ
          by simp
      next

        have "clause.vars ?C' ⊆ clause.vars D"
          using clause.variables_in_base_imgu[OF imgu, of ?C'']
          unfolding D l⇩1 l⇩2
          by auto

        then show "type_preserving_on (clause.vars ?C') 𝒱 γ"
          using type_preserving_γ 
          by blast
      qed

      show "Infer [D⇩G] C⇩G ∈ ground.G_Inf"
        unfolding ground.G_Inf_def
        using ground_factoring
        by blast
    qed
  qed
qed

lemma resolution_lifting:
  fixes 
    E⇩G D⇩G C⇩G :: "'t⇩G clause" and
    E D C :: "'t clause" and
    γ ρ⇩1 ρ⇩2 :: 'subst and
    𝒱⇩1 𝒱⇩2 :: "('v, 'ty) var_types"
  defines
    [simp]: "E⇩G ≡ clause.to_ground (E ⋅ ρ⇩1 ⊙ γ)" and
    [simp]: "D⇩G ≡ clause.to_ground (D ⋅ ρ⇩2 ⊙ γ)" and
    [simp]: "C⇩G ≡ clause.to_ground (C ⋅ γ)" and
    [simp]: "N⇩G ≡ ground_instances 𝒱⇩1 E ∪ ground_instances 𝒱⇩2 D" and
    [simp]: "ι⇩G ≡ Infer [D⇩G, E⇩G] C⇩G"
  assumes
    ground_resolution: "ground.resolution D⇩G E⇩G C⇩G" and
    ρ⇩1: "term.is_renaming ρ⇩1" and
    ρ⇩2: "term.is_renaming ρ⇩2" and
    rename_apart: "clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {}" and
    E_grounding: "clause.is_ground (E ⋅ ρ⇩1 ⊙ γ)" and
    D_grounding: "clause.is_ground (D ⋅ ρ⇩2 ⊙ γ)" and
    C_grounding: "clause.is_ground (C ⋅ γ)" and
    select_from_E: "clause.from_ground (select⇩G E⇩G) = (select E) ⋅ ρ⇩1 ⊙ γ" and
    select_from_D: "clause.from_ground (select⇩G D⇩G) = (select D) ⋅ ρ⇩2 ⊙ γ" and
    type_preserving_ρ⇩1_γ: "type_preserving_on (clause.vars E) 𝒱⇩1 (ρ⇩1 ⊙ γ)" and
    type_preserving_ρ⇩2_γ: "type_preserving_on (clause.vars D) 𝒱⇩2 (ρ⇩2 ⊙ γ)" and
    type_preserving_ρ⇩1: "type_preserving_on (clause.vars E) 𝒱⇩1 ρ⇩1" and
    type_preserving_ρ⇩2: "type_preserving_on (clause.vars D) 𝒱⇩2 ρ⇩2" and
    𝒱⇩1: "infinite_variables_per_type 𝒱⇩1" and
    𝒱⇩2: "infinite_variables_per_type 𝒱⇩2"
  obtains C' 𝒱⇩3
  where
    "resolution (𝒱⇩2, D) (𝒱⇩1, E) (𝒱⇩3, C')"
    "ι⇩G ∈ inference_ground_instances (Infer [(𝒱⇩2, D), (𝒱⇩1, E)] (𝒱⇩3, C'))"
    "C' ⋅ γ = C ⋅ γ"
  using ground_resolution
proof(cases D⇩G E⇩G C⇩G rule: ground.resolution.cases)
  case ground_resolutionI: (resolutionI l⇩G⇩1 l⇩G⇩2 E⇩G' D⇩G' t⇩G)

  have E_γ: "E ⋅ ρ⇩1 ⊙ γ = clause.from_ground (add_mset l⇩G⇩1 E⇩G')"
    using ground_resolutionI(5)
    unfolding E⇩G_def
    by (metis E_grounding clause.to_ground_inverse)

  have D_γ: "D ⋅ ρ⇩2 ⊙ γ = clause.from_ground (add_mset l⇩G⇩2 D⇩G')"
    using ground_resolutionI(6) D⇩G_def
    by (metis D_grounding clause.to_ground_inverse)

  let ?select⇩G_empty = "select⇩G (clause.to_ground (E ⋅ ρ⇩1 ⊙ γ)) = {#}"
  let ?select⇩G_not_empty = "select⇩G (clause.to_ground (E ⋅ ρ⇩1 ⊙ γ)) ≠ {#}"

  obtain l⇩1 where
    l⇩1_γ: "l⇩1 ⋅l ρ⇩1 ⊙ γ = literal.from_ground l⇩G⇩1" and
    l⇩1_is_maximal: "?select⇩G_empty ⟹ is_maximal l⇩1 E" and
    l⇩1_γ_is_maximal: "?select⇩G_empty ⟹ is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ γ) (E ⋅ ρ⇩1 ⊙ γ)" and
    l⇩1_selected: "?select⇩G_not_empty ⟹ is_maximal l⇩1 (select E)" and
    l⇩1_γ_selected: "?select⇩G_not_empty ⟹is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ γ) (select E ⋅ ρ⇩1 ⊙ γ)" and   
    l⇩1_in_E: "l⇩1 ∈# E"
  proof -
    have E_not_empty: "E ≠ {#}"
      using ground_resolutionI(5)
      by auto

    then obtain max_l where
      "is_maximal max_l E" and
      is_max_in_E_γ: "is_maximal (max_l ⋅l ρ⇩1 ⊙ γ) (E ⋅ ρ⇩1 ⊙ γ)"
      using that E_grounding obtain_maximal_literal E_not_empty
      by blast

    moreover then have "max_l ∈# E" 
      unfolding is_maximal_def
      by blast

    moreover have "max_l ⋅l ρ⇩1 ⊙ γ = literal.from_ground l⇩G⇩1" if ?select⇩G_empty
    proof -
      have "ground_is_maximal l⇩G⇩1 E⇩G"
        using ground_resolutionI(2) that
        unfolding is_maximal_def
        by simp

      then show ?thesis
        using unique_maximal_in_ground_clause[OF E_grounding is_max_in_E_γ] E_grounding
        unfolding ground_resolutionI(3)
        by simp
    qed

    moreover then obtain selected_l where
      "is_maximal selected_l (select E)"
      "is_maximal (selected_l ⋅l ρ⇩1 ⊙ γ) ((select E) ⋅ ρ⇩1 ⊙ γ)"
      "selected_l ⋅l ρ⇩1 ⊙ γ = literal.from_ground l⇩G⇩1"
    if ?select⇩G_not_empty
    proof -

      have "is_maximal (literal.from_ground l⇩G⇩1) (select E ⋅ ρ⇩1 ⊙ γ)"
        if ?select⇩G_not_empty
        using ground_resolutionI(2) that
        unfolding ground_resolutionI(3)
        by (metis E⇩G_def select_from_E)

      then show ?thesis
        using
          that
          obtain_maximal_literal[OF _ select_ground_subst[OF E_grounding]]
          unique_maximal_in_ground_clause[OF select_ground_subst[OF E_grounding]]
        by (metis (no_types, lifting) clause.magma_subst_empty(1) is_maximal_not_empty)
    qed

    moreover then have "selected_l ∈# E" if ?select⇩G_not_empty
      using that maximal_in_clause mset_subset_eqD select_subset
      by meson

    ultimately show ?thesis
      using that ground_resolutionI
      by blast
  qed

  obtain E' where E: "E = add_mset l⇩1 E'"
    by (meson l⇩1_in_E multi_member_split)

  then have E'_γ: "E' ⋅ ρ⇩1 ⊙ γ = clause.from_ground E⇩G'"
    using l⇩1_γ E_γ
    by auto

  obtain t⇩1 where 
    l⇩1: "l⇩1 = Neg t⇩1" and
    t⇩1_γ: "t⇩1 ⋅t ρ⇩1 ⊙ γ = term.from_ground t⇩G"
    using l⇩1_γ 
    by (metis Neg_atm_of_iff literal_from_ground_atom_from_ground(1) clause_safe_unfolds(9)
        ground_resolutionI(7) literal.sel(2) subst_polarity_stable(2))

  obtain l⇩2 where
    l⇩2_γ: "l⇩2 ⋅l ρ⇩2 ⊙ γ = literal.from_ground l⇩G⇩2" and
    l⇩2_is_strictly_maximal: "is_strictly_maximal l⇩2 D"
  proof-
    have "is_strictly_maximal (literal.from_ground l⇩G⇩2) (D ⋅ ρ⇩2 ⊙ γ)"
      using ground_resolutionI(4) D_grounding
      by simp

    then show ?thesis
      using obtain_strictly_maximal_literal[OF D_grounding] that
      by force
  qed

  then have l⇩2_in_D: "l⇩2 ∈# D"
    using strictly_maximal_in_clause
    by blast

  from l⇩2_γ have l⇩2_γ: "l⇩2 ⋅l ρ⇩2 ⊙ γ = (Pos (term.from_ground t⇩G))"
    unfolding ground_resolutionI
    by simp

  then obtain t⇩2 where
    l⇩2: "l⇩2 = Pos t⇩2" and
    t⇩2_γ: "t⇩2 ⋅t ρ⇩2 ⊙ γ = term.from_ground t⇩G"
    by (metis clause_safe_unfolds(9) literal.collapse(1) literal.disc(1) literal.sel(1) 
        subst_polarity_stable(2))

  obtain D' where D: "D = add_mset l⇩2 D'"
    by (meson l⇩2_in_D multi_member_split)

  then have D'_γ: "D' ⋅ ρ⇩2 ⊙ γ = clause.from_ground D⇩G'"
    using D_γ l⇩2_γ
    unfolding ground_resolutionI
    by auto

  obtain 𝒱⇩3 where
    𝒱⇩3: "infinite_variables_per_type 𝒱⇩3" and
    𝒱⇩1_𝒱⇩3: "∀x∈clause.vars E. 𝒱⇩1 x = 𝒱⇩3 (term.rename ρ⇩1 x)" and
    𝒱⇩2_𝒱⇩3: "∀x∈clause.vars D. 𝒱⇩2 x = 𝒱⇩3 (term.rename ρ⇩2 x)"
    using clause.obtain_merged_𝒱[OF ρ⇩1 ρ⇩2 rename_apart clause.finite_vars clause.finite_vars 
        infinite_UNIV] .

  have type_preserving_γ: "type_preserving_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 γ"
  proof(unfold Set.ball_Un, intro conjI)

    show "type_preserving_on (clause.vars (E ⋅ ρ⇩1)) 𝒱⇩3 γ"
      using clause.renaming_grounding[OF ρ⇩1 type_preserving_ρ⇩1_γ E_grounding 𝒱⇩1_𝒱⇩3] .
  next

    show "type_preserving_on (clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3 γ"
      using clause.renaming_grounding[OF ρ⇩2 type_preserving_ρ⇩2_γ D_grounding 𝒱⇩2_𝒱⇩3] .
  qed

  obtain μ where
    type_preserving_μ: "type_preserving_on (clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)) 𝒱⇩3  μ" and
    imgu: "term.is_imgu μ {{t⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}}"
  proof (rule obtain_type_preserving_on_imgu[OF _ that], intro conjI)

    show "t⇩1 ⋅t ρ⇩1 ⋅t γ = t⇩2 ⋅t ρ⇩2 ⋅t γ"
      using t⇩1_γ t⇩2_γ
      by simp
  next

    show "type_preserving_on (term.vars (t⇩1 ⋅t ρ⇩1) ∪ term.vars (t⇩2 ⋅t ρ⇩2)) 𝒱⇩3 γ"
      using type_preserving_γ
      unfolding E D l⇩1 l⇩2
      by auto
  qed

  obtain σ where γ: "γ = μ ⊙ σ"
    using term.obtain_imgu_absorption[of γ, OF _ imgu] t⇩1_γ t⇩2_γ
    by auto

  define C' where
    C': "C' = (E' ⋅ ρ⇩1 + D' ⋅ ρ⇩2) ⋅ μ"

  show ?thesis
  proof(rule that)

    show resolution: "resolution (𝒱⇩2, D) (𝒱⇩1, E) (𝒱⇩3, C')"
    proof (rule resolutionI; ((rule ρ⇩1 ρ⇩2 E D l⇩1 l⇩2 imgu type_preserving_μ rename_apart 
            type_preserving_ρ⇩1 type_preserving_ρ⇩2 𝒱⇩1 𝒱⇩2 C' 𝒱⇩1_𝒱⇩3 𝒱⇩2_𝒱⇩3)+)?)

      show "¬ E ⋅ ρ⇩1 ⊙ μ ≼⇩c D ⋅ ρ⇩2 ⊙ μ"
      proof(rule clause.order.ground_less_not_less_eq)

        show "clause.vars (D ⋅ ρ⇩2 ⊙ μ ⋅ σ) = {}"
          using D_grounding
          unfolding γ
          by simp

        show "clause.vars (E ⋅ ρ⇩1 ⊙ μ ⋅ σ) = {}"
          using E_grounding
          unfolding γ
          by simp

        show "D ⋅ ρ⇩2 ⊙ μ ⋅ σ ≺⇩c E ⋅ ρ⇩1 ⊙ μ ⋅ σ"
          using ground_resolutionI(1) D_grounding E_grounding
          unfolding E⇩G_def D⇩G_def clause.order.less⇩G_def γ
          by simp
      qed
    next
      assume "select E = {#}"

      moreover then have ?select⇩G_empty
        using is_maximal_not_empty l⇩1_selected 
        by blast

      moreover have "l⇩1 ⋅l ρ⇩1 ⊙ μ ∈# E ⋅ ρ⇩1 ⊙ μ"
        using l⇩1_in_E
        by blast

      ultimately show "is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (E ⋅ ρ⇩1 ⊙ μ)"
        using l⇩1_γ_is_maximal is_maximal_if_grounding_is_maximal E_grounding 
        unfolding γ
        by force
    next
      assume "select E ≠ {#}"

      then have "¬?select⇩G_empty"
        using is_maximal_not_empty l⇩1_selected select_from_E 
        by auto

      moreover have "l⇩1 ⋅l ρ⇩1 ⊙ μ ∈# select E ⋅ ρ⇩1 ⊙ μ"
        using l⇩1_selected maximal_in_clause calculation 
        by blast

      ultimately show "is_maximal (l⇩1 ⋅l ρ⇩1 ⊙ μ) (select E ⋅ ρ⇩1 ⊙ μ)"
        using select_ground_subst[OF E_grounding] is_maximal_if_grounding_is_maximal l⇩1_γ_selected
        unfolding γ
        by fastforce
    next

      show "select D = {#}"
        using ground_resolutionI(3) select_from_D 
        by fastforce
    next

      show "is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ) (D ⋅ ρ⇩2 ⊙ μ)"
      proof(rule is_strictly_maximal_if_grounding_is_strictly_maximal)

        show "l⇩2 ⋅l ρ⇩2 ⊙ μ ∈# D ⋅ ρ⇩2 ⊙ μ"
          using l⇩2_in_D
          by blast

        show "clause.is_ground (D ⋅ ρ⇩2 ⊙ μ ⋅ σ)"
          using D_grounding[unfolded γ]
          by simp

        show "is_strictly_maximal (l⇩2 ⋅l ρ⇩2 ⊙ μ ⋅l σ) (D ⋅ ρ⇩2 ⊙ μ ⋅ σ)"
          using l⇩2_γ D_γ ground_resolutionI(4)
          unfolding γ ground_resolutionI
          by fastforce
      qed
    qed

    show C'_γ: "C' ⋅ γ = C ⋅ γ"
    proof-

      have "term.is_idem μ"
        using imgu term.is_imgu_iff_is_idem_and_is_mgu
        by blast

      then have μ_γ: "μ ⊙ γ = γ"
        unfolding γ term.is_idem_def
        by (metis term.assoc)

      have "C ⋅ γ = (clause.from_ground E⇩G' + clause.from_ground D⇩G')"
        using ground_resolutionI(8, 9) clause.to_ground_inverse[OF C_grounding]
        by auto

      then show ?thesis
        unfolding
          C'
          E'_γ[symmetric]
          D'_γ[symmetric]
          clause.subst_comp_subst[symmetric]
          μ_γ
        by simp
    qed

    show "ι⇩G ∈ inference_ground_instances (Infer [(𝒱⇩2, D), (𝒱⇩1, E)] (𝒱⇩3, C'))"
    proof (rule is_inference_ground_instance_two_premises)

      show "is_inference_ground_instance_two_premises (𝒱⇩2, D) (𝒱⇩1, E) (𝒱⇩3, C') ι⇩G γ ρ⇩1 ρ⇩2"
      proof(unfold split, intro conjI;
          (rule ρ⇩1 ρ⇩2 rename_apart refl 𝒱⇩1 𝒱⇩2 𝒱⇩3)?)

        show "inference.is_ground (Infer [D ⋅ ρ⇩2, E ⋅ ρ⇩1] C' ⋅ι γ)"
          using D_grounding E_grounding C_grounding C'_γ
          by auto
      next

        show "ι⇩G = inference.to_ground (Infer [D ⋅ ρ⇩2, E ⋅ ρ⇩1] C' ⋅ι γ)"
          using C'_γ
          by simp
      next

        show "type_preserving_on (clause.vars C') 𝒱⇩3 γ"
        proof(rule type_preserving_on_subset[OF type_preserving_γ])

          show "clause.vars C' ⊆ clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)"
          proof (unfold subset_eq, intro ballI)
            fix x

            have is_imgu: "term.is_imgu μ {{t⇩1 ⋅t ρ⇩1, t⇩2 ⋅t ρ⇩2}}"
              using imgu
              by blast

            assume "x ∈ clause.vars C'"

            then consider
              (E') "x ∈ clause.vars (E' ⋅ ρ⇩1 ⊙ μ)" |
              (D') "x ∈ clause.vars (D' ⋅ ρ⇩2 ⊙ μ)"
              unfolding C'
              by auto

            then show "x ∈ clause.vars (E ⋅ ρ⇩1) ∪ clause.vars (D ⋅ ρ⇩2)"
            proof cases
              case E'

              then show ?thesis
                using clause.variables_in_base_imgu[OF is_imgu]
                unfolding E l⇩1 D l⇩2
                by auto
            next
              case D'

              then show ?thesis
                using clause.variables_in_base_imgu[OF is_imgu]
                unfolding E l⇩1 D l⇩2
                by auto
            qed
          qed
        qed
      qed
      show "ι⇩G ∈ ground.G_Inf"
        unfolding ground.G_Inf_def
        using ground_resolution
        by simp
    qed
  qed
qed

subsection ‹Ground instances›

context
  fixes ι⇩G N
  assumes
    subst_stability: "subst_stability_on N" and
    ι⇩G_Inf_from: "ι⇩G ∈ ground.Inf_from_q select⇩G (⋃(uncurried_ground_instances ` N))"
begin

lemma factoring_ground_instance:
  assumes ground_factoring: "ι⇩G ∈ ground.factoring_inferences"
  obtains ι where
    "ι ∈ Inf_from N"
    "ι⇩G ∈ inference_ground_instances ι"
proof -

  obtain D⇩G C⇩G where
    ι⇩G: "ι⇩G = Infer [D⇩G] C⇩G" and
    ground_inference: "ground.factoring D⇩G C⇩G"
    using ground_factoring
    by blast

  have D⇩G_in_groundings: "D⇩G ∈ ⋃(uncurried_ground_instances ` N)"
    using ι⇩G_Inf_from
    unfolding ι⇩G ground.Inf_from_q_def ground.Inf_from_def
    by simp

  obtain D γ 𝒱 where
    D_grounding: "clause.is_ground (D ⋅ γ)" and
    type_preserving_γ: "type_preserving_on (clause.vars D) 𝒱 γ" and
    𝒱: "infinite_variables_per_type 𝒱" and
    D_in_N: "(𝒱, D) ∈ N" and
    "select⇩G D⇩G = clause.to_ground (select D ⋅ γ)"
    "D ⋅ γ = clause.from_ground D⇩G"
    using subst_stability[rule_format, OF D⇩G_in_groundings]
    by blast

  then have
    D⇩G: "D⇩G = clause.to_ground (D ⋅ γ)" and
    select: "clause.from_ground (select⇩G D⇩G) = select D ⋅ γ"
    by (simp_all add: select_ground_subst)

  obtain C where
    C⇩G: "C⇩G = clause.to_ground (C ⋅ γ)" and
    C_grounding: "clause.is_ground (C ⋅ γ)"
    by (metis clause.all_subst_ident_iff_ground clause.from_ground_inverse
        clause.ground_is_ground)

  obtain C' where
    factoring: "factoring (𝒱, D) (𝒱, C')" and
    inference_ground_instances: "ι⇩G ∈ inference_ground_instances (Infer [(𝒱, D)] (𝒱, C'))" and
    C'_C: "C' ⋅ γ = C ⋅ γ"
    using
      factoring_lifting[OF
        ground_inference[unfolded D⇩G C⇩G]
        D_grounding
        C_grounding
        select[unfolded D⇩G]
        type_preserving_γ
        𝒱]
    unfolding D⇩G C⇩G ι⇩G .

  let ?ι = "Infer [(𝒱, D)] (𝒱, C')"

  show ?thesis
  proof(rule that[OF _ inference_ground_instances])

    show "?ι ∈ Inf_from N"
      using D_in_N factoring
      unfolding Inf_from_def inferences_def inference_system.Inf_from_def
      by auto
  qed
qed


lemma resolution_ground_instance:
  assumes ground_resolution: "ι⇩G ∈ ground.resolution_inferences"
  obtains ι where
    "ι ∈ Inf_from N"
    "ι⇩G ∈ inference_ground_instances ι"
proof-
  obtain E⇩G D⇩G C⇩G where
    ι⇩G : "ι⇩G = Infer [D⇩G, E⇩G] C⇩G" and
    ground_resolution: "ground.resolution D⇩G E⇩G C⇩G"
    using assms(1)
    by blast

  have
    E⇩G_in_groundings: "E⇩G ∈ ⋃ (uncurried_ground_instances ` N)" and
    D⇩G_in_groundings: "D⇩G ∈ ⋃ (uncurried_ground_instances ` N)"
    using ι⇩G_Inf_from
    unfolding ι⇩G ground.Inf_from_q_def ground.Inf_from_def
    by simp_all

  obtain E 𝒱⇩1 γ⇩1 where
    E_grounding: "clause.is_ground (E ⋅ γ⇩1)" and
    type_preserving_γ⇩1: "type_preserving_on (clause.vars E) 𝒱⇩1 γ⇩1" and
    𝒱⇩1: "infinite_variables_per_type 𝒱⇩1" and
    E_in_N: "(𝒱⇩1, E) ∈ N" and
    "select⇩G E⇩G = clause.to_ground (select E ⋅ γ⇩1)"
    "E ⋅ γ⇩1 = clause.from_ground E⇩G"
    using subst_stability[rule_format, OF E⇩G_in_groundings]
    by blast

  then have
    E⇩G: "E⇩G = clause.to_ground (E ⋅ γ⇩1)" and
    select_from_E: "clause.from_ground (select⇩G E⇩G) = select E ⋅ γ⇩1"
    by (simp_all add: select_ground_subst)

  obtain D 𝒱⇩2 γ⇩2 where
    D_grounding: "clause.is_ground (D ⋅ γ⇩2)" and
    type_preserving_γ⇩2: "type_preserving_on (clause.vars D) 𝒱⇩2 γ⇩2" and
    𝒱⇩2: "infinite_variables_per_type 𝒱⇩2" and
    D_in_N: "(𝒱⇩2, D) ∈ N" and
    "select⇩G D⇩G = clause.to_ground (select D ⋅ γ⇩2)"
    "D ⋅ γ⇩2 = clause.from_ground D⇩G"
    using subst_stability[rule_format, OF D⇩G_in_groundings]
    by blast

  then have
    D⇩G: "D⇩G = clause.to_ground (D ⋅ γ⇩2)" and
    select_from_D: "clause.from_ground (select⇩G D⇩G) = select D ⋅ γ⇩2"
    by (simp_all add: select_ground_subst)

  obtain ρ⇩1 ρ⇩2 γ where
    ρ⇩1: "term.is_renaming ρ⇩1" and
    ρ⇩2: "term.is_renaming ρ⇩2" and
    rename_apart: "clause.vars (E ⋅ ρ⇩1) ∩ clause.vars (D ⋅ ρ⇩2) = {}" and
    type_preserving_ρ⇩1: "type_preserving_on (clause.vars E) 𝒱⇩1 ρ⇩1" and
    type_preserving_ρ⇩2: "type_preserving_on (clause.vars D) 𝒱⇩2 ρ⇩2" and
    γ⇩1_γ: "∀x ∈ clause.vars E. x ⋅v γ⇩1 = x ⋅v ρ⇩1 ⊙ γ" and
    γ⇩2_γ: "∀x ∈ clause.vars D. x ⋅v γ⇩2 = x ⋅v ρ⇩2 ⊙ γ"
    using clause.obtain_merged_grounding[OF
        type_preserving_γ⇩1 type_preserving_γ⇩2 E_grounding D_grounding 𝒱⇩2 clause.finite_vars] .

  have E_grounding: "clause.is_ground (E ⋅ ρ⇩1 ⊙ γ)"
    using clause.subst_eq γ⇩1_γ E_grounding
    by fastforce

  have E⇩G: "E⇩G = clause.to_ground (E ⋅ ρ⇩1 ⊙ γ)"
    using clause.subst_eq γ⇩1_γ E⇩G
    by fastforce

  have D_grounding: "clause.is_ground (D ⋅ ρ⇩2 ⊙ γ)"
    using clause.subst_eq γ⇩2_γ D_grounding
    by fastforce

  have D⇩G: "D⇩G = clause.to_ground (D ⋅ ρ⇩2 ⊙ γ)"
    using clause.subst_eq γ⇩2_γ D⇩G
    by fastforce

  have type_preserving_ρ⇩1_γ: "type_preserving_on (clause.vars E) 𝒱⇩1 (ρ⇩1 ⊙ γ)"
    using type_preserving_γ⇩1 γ⇩1_γ
    by fastforce

  have type_preserving_ρ⇩2_γ: "type_preserving_on (clause.vars D) 𝒱⇩2 (ρ⇩2 ⊙ γ)"
    using type_preserving_γ⇩2 γ⇩2_γ
    by fastforce

  have select_from_E:
    "clause.from_ground (select⇩G (clause.to_ground (E ⋅ ρ⇩1 ⊙ γ))) = select E ⋅ ρ⇩1 ⊙ γ"
  proof-
    have "E ⋅ γ⇩1 = E ⋅ ρ⇩1 ⊙ γ"
      using γ⇩1_γ clause.subst_eq
      by fast

    moreover have "select E ⋅ γ⇩1 = select E ⋅ ρ⇩1 ⋅ γ"
      using clause.subst_eq γ⇩1_γ select_vars_subset
      by (metis (no_types, lifting) clause.comp_subst.left.monoid_action_compatibility in_mono)

    ultimately show ?thesis
      using select_from_E
      unfolding E⇩G
      by simp
  qed

  have select_from_D:
    "clause.from_ground (select⇩G (clause.to_ground (D ⋅ ρ⇩2 ⊙ γ))) = select D ⋅ ρ⇩2 ⊙ γ"
  proof-
    have "D ⋅ γ⇩2 = D ⋅ ρ⇩2 ⊙ γ"
      using γ⇩2_γ clause.subst_eq
      by fast

    moreover have "select D ⋅ γ⇩2 = select D ⋅ ρ⇩2 ⋅ γ"
      using clause.subst_eq γ⇩2_γ select_vars_subset[of D]
      by (metis (no_types, lifting) clause.comp_subst.left.monoid_action_compatibility in_mono)

    ultimately show ?thesis
      using select_from_D
      unfolding D⇩G
      by simp
  qed

  obtain C where
    C_grounding: "clause.is_ground (C ⋅ γ)" and
    C⇩G: "C⇩G = clause.to_ground (C ⋅ γ)"
    by (metis clause.all_subst_ident_if_ground clause.from_ground_inverse clause.ground_is_ground)

  have "ground_instances 𝒱⇩1 E ∪ ground_instances 𝒱⇩2 D ⊆ ⋃ (uncurried_ground_instances ` N)"
    using E_in_N D_in_N
    by force

  obtain C' 𝒱⇩3 where
    resolution: "resolution (𝒱⇩2, D) (𝒱⇩1, E) (𝒱⇩3, C')" and
    inference_groundings: "ι⇩G ∈ inference_ground_instances (Infer [(𝒱⇩2, D), (𝒱⇩1, E)] (𝒱⇩3, C'))" and
    C'_γ_C_γ: "C' ⋅ γ = C ⋅ γ"
    using resolution_lifting[OF ground_resolution[unfolded E⇩G D⇩G C⇩G]
        ρ⇩1 ρ⇩2
        rename_apart
        E_grounding D_grounding C_grounding 
        select_from_E select_from_D
        type_preserving_ρ⇩1_γ type_preserving_ρ⇩2_γ
        type_preserving_ρ⇩1 type_preserving_ρ⇩2
        𝒱⇩1 𝒱⇩2]
    unfolding ι⇩G C⇩G E⇩G D⇩G .

  let ?ι = "Infer [(𝒱⇩2, D), (𝒱⇩1, E)] (𝒱⇩3, C')"

  show ?thesis
  proof(rule that[OF _ inference_groundings])

    show "?ι ∈ Inf_from N"
      using E_in_N D_in_N resolution
      unfolding Inf_from_def inferences_def inference_system.Inf_from_def
      by auto
  qed
qed

lemma ground_instances:
  obtains ι where
    "ι ∈ Inf_from N"
    "ι⇩G ∈ inference_ground_instances ι"
proof -

  consider
    (resolution) "ι⇩G ∈ ground.resolution_inferences" |
    (factoring) "ι⇩G ∈ ground.factoring_inferences"
    using ι⇩G_Inf_from
    unfolding
      ground.Inf_from_q_def
      ground.G_Inf_def
      inference_system.Inf_from_def
    by fastforce

  then show ?thesis
  proof cases
    case resolution

    then show ?thesis
      using that resolution_ground_instance
      by blast
  next
    case factoring

    then show ?thesis
      using that factoring_ground_instance
      by blast
  qed
qed

end

end

context ordered_resolution_calculus
begin

lemma overapproximation:
  obtains select⇩G where
    "ground_Inf_overapproximated select⇩G premises"
    "is_grounding select⇩G"
proof-
  obtain select⇩G where
    subst_stability: "select_subst_stability_on select select⇩G premises" and
    "is_grounding select⇩G"
    using obtain_subst_stable_on_select_grounding
    by blast

  then interpret grounded_ordered_resolution_calculus
    where select⇩G = select⇩G
    by unfold_locales

  show thesis
  proof(rule that[OF _ select⇩G])

    show "ground_Inf_overapproximated select⇩G premises"
      using ground_instances[OF subst_stability]
      by auto
  qed
qed

sublocale statically_complete_calculus "⊥⇩F" inferences entails_𝒢 Red_I_𝒢 Red_F_𝒢
proof (unfold static_empty_ord_inter_equiv_static_inter,
    rule stat_ref_comp_to_non_ground_fam_inter,
    rule ballI)
  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 "statically_complete_calculus
          ground.G_Bot
          ground.G_Inf
          ground.G_entails
          ground.Red_I
          ground.Red_F"
    by unfold_locales
next

  show "⋀N. ∃select⇩G ∈ select⇩G⇩s. ground_Inf_overapproximated select⇩G N"
    using overapproximation
    unfolding select⇩G⇩s_def
    by (smt (verit, best) mem_Collect_eq)
qed

end

end