Theory Superposition

theory Superposition
  imports
    First_Order_Clause.Nonground_Order
    First_Order_Clause.Nonground_Selection_Function
    First_Order_Clause.Nonground_Typing
    First_Order_Clause.Typed_Tiebreakers
    First_Order_Clause.Welltyped_IMGU

    Ground_Superposition
begin


section ‹Nonground Layer›

locale superposition_calculus =
  nonground_inhabited_typing  +
  nonground_equality_order lesst +
  nonground_selection_function select +
  typed_tiebreakers tiebreakers +
  ground_critical_pair_theorem "TYPE('f)"
  for
    select :: "('f, 'v :: infinite) select" and
    lesst :: "('f, 'v) term  ('f, 'v) term  bool" and
     :: "('f, 'ty) fun_types" and
    tiebreakers :: "('f, 'v) tiebreakers" +
  assumes
    types_ordLeq_variables: "|UNIV :: 'ty set| ≤o |UNIV :: 'v set|"
begin

interpretation term_order_notation.

inductive eq_resolution :: "('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  bool" where
  eq_resolutionI: 
   "D = add_mset l D' 
    l = t !≈ t' 
    welltyped_imgu_on (clause.vars D) 𝒱 t t' μ 
    select D = {#}  is_maximal (l ⋅l μ) (D  μ)  is_maximal (l ⋅l μ) (select D  μ) 
    C = D'  μ 
    eq_resolution (D, 𝒱) (C, 𝒱)"

inductive eq_factoring :: "('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  bool" where
  eq_factoringI: 
   "D = add_mset l1 (add_mset l2 D') 
    l1 = t1  t1' 
    l2 = t2  t2' 
    select D = {#} 
    is_maximal (l1 ⋅l μ) (D  μ) 
    ¬ (t1 ⋅t μ t t1' ⋅t μ) 
    welltyped_imgu_on (clause.vars D) 𝒱 t1 t2 μ 
    C = add_mset (t1  t2') (add_mset (t1' !≈ t2') D')  μ 
    eq_factoring (D, 𝒱) (C, 𝒱)"

inductive superposition ::
  "('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  bool"
where
  superpositionI:
   "infinite_variables_per_type 𝒱1 
    infinite_variables_per_type 𝒱2 
    term_subst.is_renaming ρ1 
    term_subst.is_renaming ρ2 
    clause.vars (E  ρ1)  clause.vars (D  ρ2) = {} 
    E = add_mset l1 E' 
    D = add_mset l2 D' 
    𝒫  {Pos, Neg} 
    l1 = 𝒫 (Upair c1t1 t1') 
    l2 = t2  t2' 
    ¬ is_Var t1 
    welltyped_imgu_on (clause.vars (E  ρ1)  clause.vars (D  ρ2)) 𝒱3 (t1 ⋅t ρ1) (t2 ⋅t ρ2) μ 
    x  clause.vars E. 𝒱1 x = 𝒱3 (term.rename ρ1 x) 
    x  clause.vars D. 𝒱2 x = 𝒱3 (term.rename ρ2 x) 
    term.subst.is_welltyped_on (clause.vars E) 𝒱1 ρ1 
    term.subst.is_welltyped_on (clause.vars D) 𝒱2 ρ2 
    (τ τ'. typed 𝒱2 t2 τ  typed 𝒱2 t2' τ'  τ = τ') 
    ¬ (E  ρ1  μ c D  ρ2  μ) 
    (𝒫 = Pos  select E = {#}) 
    (𝒫 = Pos  is_strictly_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ)) 
    (𝒫 = Neg  select E = {#}  is_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ)) 
    (𝒫 = Neg  select E  {#}  is_maximal (l1 ⋅l ρ1  μ) ((select E)  ρ1  μ)) 
    select D = {#} 
    is_strictly_maximal (l2 ⋅l ρ2  μ) (D  ρ2  μ) 
    ¬ (c1t1 ⋅t ρ1  μ t t1' ⋅t ρ1  μ) 
    ¬ (t2 ⋅t ρ2  μ t t2' ⋅t ρ2  μ) 
    C = add_mset (𝒫 (Upair (c1 ⋅tc ρ1)t2' ⋅t ρ2 (t1' ⋅t ρ1))) (E'  ρ1 + D'  ρ2)  μ 
    superposition (D, 𝒱2) (E, 𝒱1) (C, 𝒱3)"

abbreviation eq_factoring_inferences where
  "eq_factoring_inferences  { Infer [D] C | D C. eq_factoring D C }"

abbreviation eq_resolution_inferences where
  "eq_resolution_inferences  { Infer [D] C | D C. eq_resolution D C }"

abbreviation superposition_inferences where
  "superposition_inferences  { Infer [D, E] C | D E C. superposition D E C}"

definition inferences :: "('f, 'v, 'ty) typed_clause inference set" where
  "inferences  superposition_inferences  eq_resolution_inferences  eq_factoring_inferences"

abbreviation bottomF :: "('f, 'v, 'ty) typed_clause set" ("F") where
  "bottomF  {({#}, 𝒱) | 𝒱. infinite_variables_per_type 𝒱 }"

subsubsection ‹Alternative Specification of the Superposition Rule›

inductive superposition' ::
  "('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  bool"
where
  superposition'I:
   "infinite_variables_per_type 𝒱1 
    infinite_variables_per_type 𝒱2 
    term_subst.is_renaming ρ1 
    term_subst.is_renaming ρ2 
    clause.vars (E  ρ1)  clause.vars (D  ρ2) = {} 
    E = add_mset l1 E' 
    D = add_mset l2 D' 
    𝒫  {Pos, Neg} 
    l1 = 𝒫 (Upair c1t1 t1') 
    l2 = t2  t2' 
    ¬ is_Var t1 
    welltyped_imgu_on (clause.vars (E  ρ1)  clause.vars (D  ρ2)) 𝒱3 (t1 ⋅t ρ1) (t2 ⋅t ρ2) μ 
    x  clause.vars E. 𝒱1 x = 𝒱3 (term.rename ρ1 x) 
    x  clause.vars D. 𝒱2 x = 𝒱3 (term.rename ρ2 x) 
    term.subst.is_welltyped_on (clause.vars E) 𝒱1 ρ1 
    term.subst.is_welltyped_on (clause.vars D) 𝒱2 ρ2 
    (τ τ'. typed 𝒱2 t2 τ  typed 𝒱2 t2' τ'  τ = τ') 
    ¬ (E  ρ1  μ c D  ρ2  μ) 
    (𝒫 = Pos  select E = {#}  is_strictly_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ) 
     𝒫 = Neg  (select E = {#}  is_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ) 
                  is_maximal (l1 ⋅l ρ1  μ) ((select E)  ρ1  μ))) 
    select D = {#} 
    is_strictly_maximal (l2 ⋅l ρ2  μ) (D  ρ2  μ) 
    ¬ (c1t1 ⋅t ρ1  μ t t1' ⋅t ρ1  μ) 
    ¬ (t2 ⋅t ρ2  μ t t2' ⋅t ρ2  μ) 
    C = add_mset (𝒫 (Upair (c1 ⋅tc ρ1)t2' ⋅t ρ2 (t1' ⋅t ρ1))) (E'  ρ1 + D'  ρ2)  μ 
    superposition' (D, 𝒱2) (E, 𝒱1) (C, 𝒱3)"  

lemma superposition_eq_superposition': "superposition = superposition'"
proof (intro ext iffI)
  fix D E C
  assume "superposition D E C" 
  then show "superposition' D E C"
  
  proof (cases D E C rule: superposition.cases)
    case (superpositionI 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' 𝒫 c1 t1 t1' t2 t2' 𝒱3 μ C)

    show ?thesis
    proof (unfold superpositionI(1-3), rule superposition'I[of 𝒱1 𝒱2 ρ1 ρ2]; (rule superpositionI)?)

      show "𝒫 = Pos  select E = {#}  is_strictly_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ) 
       𝒫 = Neg  (select E = {#}  is_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ) 
                   is_maximal (l1 ⋅l ρ1  μ) (select E  ρ1  μ))"
        using superpositionI(11,22-25)
        by fastforce
    qed
  qed
next
  fix D E C
  assume "superposition' D E C" 
  then show "superposition D E C"
  proof (cases D E C rule: superposition'.cases)
    case (superposition'I 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' 𝒫 c1 t1 t1' t2 t2' 𝒱3 μ C)

    show ?thesis
    proof (unfold superposition'I(1-3), rule superpositionI[of 𝒱1 𝒱2 ρ1 ρ2]; (rule superposition'I)?)

      show
        "𝒫 = Pos  select E = {#}" 
        "𝒫 = Pos  is_strictly_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ)"
        "𝒫 = Neg  select E = {#}  is_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ)"
        "𝒫 = Neg  select E  {#}  is_maximal (l1 ⋅l ρ1  μ) (select E  ρ1  μ)"
        using superposition'I(22) is_maximal_not_empty
        by auto
    qed 
  qed
qed

inductive pos_superposition ::
  "('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  bool"
where
  pos_superpositionI: 
   "infinite_variables_per_type 𝒱1 
    infinite_variables_per_type 𝒱2 
    term_subst.is_renaming ρ1 
    term_subst.is_renaming ρ2 
    clause.vars (E  ρ1)  clause.vars (D  ρ2) = {} 
    E = add_mset l1 E' 
    D = add_mset l2 D' 
    l1 = c1t1  t1' 
    l2 = t2  t2' 
    ¬ is_Var t1 
    welltyped_imgu_on (clause.vars (E  ρ1)  clause.vars (D  ρ2)) 𝒱3 (t1 ⋅t ρ1) (t2 ⋅t ρ2) μ 
    x  clause.vars E. 𝒱1 x = 𝒱3 (term.rename ρ1 x) 
    x  clause.vars D. 𝒱2 x = 𝒱3 (term.rename ρ2 x) 
    term.subst.is_welltyped_on (clause.vars E) 𝒱1 ρ1 
    term.subst.is_welltyped_on (clause.vars D) 𝒱2 ρ2 
    (τ τ'. typed 𝒱2 t2 τ  typed 𝒱2 t2' τ'  τ = τ') 
    ¬ (E  ρ1  μ c D  ρ2  μ) 
    select E = {#} 
    is_strictly_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ) 
    select D = {#} 
    is_strictly_maximal (l2 ⋅l ρ2  μ) (D  ρ2  μ) 
    ¬ (c1t1 ⋅t ρ1  μ t t1' ⋅t ρ1  μ) 
    ¬ (t2 ⋅t ρ2  μ t t2' ⋅t ρ2  μ) 
    C = add_mset ((c1 ⋅tc ρ1)t2' ⋅t ρ2  (t1' ⋅t ρ1)) (E'  ρ1 + D'  ρ2)  μ 
    pos_superposition (D, 𝒱2) (E, 𝒱1) (C, 𝒱3)"

lemma superposition_if_pos_superposition:
  assumes "pos_superposition D E C"
  shows "superposition D E C"
  using assms
proof (cases rule: pos_superposition.cases)
  case (pos_superpositionI 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' c1 t1 t1' t2 t2' μ 𝒱3  C)
  then show ?thesis
    using superpositionI[of 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' Pos c1 t1 t1' t2 t2' μ 𝒱3 C]
    by blast
qed

inductive neg_superposition ::
  "('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  ('f, 'v, 'ty) typed_clause  bool"
where
  neg_superpositionI: 
   "infinite_variables_per_type 𝒱1 
    infinite_variables_per_type 𝒱2 
    term_subst.is_renaming ρ1 
    term_subst.is_renaming ρ2 
    clause.vars (E  ρ1)  clause.vars (D  ρ2) = {} 
    E = add_mset l1 E' 
    D = add_mset l2 D' 
    l1 = c1t1 !≈ t1' 
    l2 = t2  t2' 
    ¬ is_Var t1 
    welltyped_imgu_on (clause.vars (E  ρ1)  clause.vars (D  ρ2)) 𝒱3 (t1 ⋅t ρ1) (t2 ⋅t ρ2) μ 
    x  clause.vars E. 𝒱1 x = 𝒱3 (term.rename ρ1 x) 
    x  clause.vars D. 𝒱2 x = 𝒱3 (term.rename ρ2 x) 
    term.subst.is_welltyped_on (clause.vars E) 𝒱1 ρ1 
    term.subst.is_welltyped_on (clause.vars D) 𝒱2 ρ2 
    (τ τ'. typed 𝒱2 t2 τ  typed 𝒱2 t2' τ'  τ = τ') 
    ¬ (E  ρ1  μ c D  ρ2  μ) 
    (select E = {#}  is_maximal (l1 ⋅l ρ1  μ) (E  ρ1  μ)) 
    (select E  {#}  is_maximal (l1 ⋅l ρ1  μ) ((select E)  ρ1  μ)) 
    select D = {#} 
    is_strictly_maximal (l2 ⋅l ρ2  μ) (D  ρ2  μ) 
    ¬ (c1t1 ⋅t ρ1  μ t t1' ⋅t ρ1  μ) 
    ¬ (t2 ⋅t ρ2  μ t t2' ⋅t ρ2  μ) 
    C = add_mset ((c1 ⋅tc ρ1)t2' ⋅t ρ2 !≈ (t1' ⋅t ρ1)) (E'  ρ1 + D'  ρ2)  μ 
    neg_superposition (D, 𝒱2) (E, 𝒱1) (C, 𝒱3)"

lemma superposition_if_neg_superposition:
  assumes "neg_superposition E D C"
  shows "superposition E D C"
  using assms
proof (cases E D C rule: neg_superposition.cases)
  case (neg_superpositionI 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' c1 t1 t1' t2 t2' μ 𝒱3 C)
  then show ?thesis
    using 
      superpositionI[of 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' Neg c1 t1 t1' t2 t2' μ 𝒱3 C]
      literals_distinct(2)
    by blast
qed

lemma superposition_iff_pos_or_neg:
  "superposition D E C  pos_superposition D E C  neg_superposition D E C"
proof (rule iffI)
  assume "superposition D E C"
  thus "pos_superposition D E C  neg_superposition D E C"
  proof (cases D E C rule: superposition.cases)
    case (superpositionI 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' 𝒫 c1 t1 t1' t2 t2' 𝒱3 μ C)

    show ?thesis 
    proof(cases "𝒫 = Pos")
      case True
      then have "pos_superposition (D, 𝒱2) (E, 𝒱1) (C, 𝒱3)"
        using 
          superpositionI 
          pos_superpositionI[of 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' c1 t1 t1' t2 t2' 𝒱3 μ C]
        by argo

      then show ?thesis
        unfolding superpositionI(1-3)
        by simp
        
    next
      case False

      then have "𝒫 = Neg"
        using superpositionI(11) 
        by blast

      then have "neg_superposition (D, 𝒱2) (E, 𝒱1) (C, 𝒱3)"
        using 
          superpositionI 
          neg_superpositionI[of 𝒱1 𝒱2 ρ1 ρ2 E D l1 E' l2 D' c1 t1 t1' t2 t2' 𝒱3 μ C]
        by argo

      then show ?thesis
        unfolding superpositionI(1-3)
        by simp
    qed
  qed
next
  assume "pos_superposition D E C  neg_superposition D E C"
  thus "superposition D E C"
    using superposition_if_neg_superposition superposition_if_pos_superposition 
    by metis
qed

end

end