Theory First_Order_Superposition_Example

theory First_Order_Superposition_Example
  imports
    IsaFoR_Term_Copy
    First_Order_Superposition
begin

abbreviation trivial_select :: "('f, 'v) select" where
  "trivial_select _ ≡ {#}"

abbreviation trivial_tiebreakers where
  "trivial_tiebreakers _ _ _ ≡ False"

context
  assumes ground_critical_pair_theorem:
    "⋀(R :: ('f :: weighted) gterm rel). ground_critical_pair_theorem R"
begin

interpretation first_order_superposition_calculus 
  "trivial_select :: ('f :: weighted, 'v :: infinite) select" 
  less_kbo
  trivial_tiebreakers
  "λ_. ([], ())"
proof(unfold_locales)
  fix clause :: "('f, 'v) atom clause"

  show "trivial_select clause ⊆# clause"
    by simp
next
  fix clause :: "('f, 'v) atom clause" and literal

  assume "literal ∈# trivial_select clause"

  then show "is_neg literal"
    by simp
next
  show "transp less_kbo"
    using KBO.S_trans 
    unfolding transp_def less_kbo_def
    by blast
next
  show "asymp less_kbo"
    using wfP_imp_asymp wfP_less_kbo 
    by blast
next
  show "Wellfounded.wfp_on {term. term.is_ground term} less_kbo"
    using Wellfounded.wfp_on_subset[OF wfP_less_kbo subset_UNIV] .
next
  show "totalp_on {term. term.is_ground term} less_kbo"
    using less_kbo_gtotal
    unfolding totalp_on_def Term.ground_vars_term_empty
    by blast
next
  fix 
    context⇩G :: "('f, 'v) context" and
    term⇩G⇩1 term⇩G⇩2 :: "('f, 'v) term" 

  assume "less_kbo term⇩G⇩1 term⇩G⇩2" 

  then show "less_kbo context⇩G⟨term⇩G⇩1⟩ context⇩G⟨term⇩G⇩2⟩"
    using KBO.S_ctxt less_kbo_def by blast
next
  fix 
    term⇩1 term⇩2 :: "('f, 'v) term" and 
    γ :: "('f, 'v) subst"

  assume "less_kbo term⇩1 term⇩2"

  then show "less_kbo (term⇩1 ⋅t γ) (term⇩2 ⋅t γ)"
    using less_kbo_subst by blast
next
  fix
    term⇩G :: "('f, 'v) term" and
    context⇩G :: "('f, 'v) context"
  assume 
    "term.is_ground term⇩G" 
    "context.is_ground context⇩G" 
    "context⇩G ≠ □"
  
  then show "less_kbo term⇩G context⇩G⟨term⇩G⟩"
    by (simp add: KBO.S_supt less_kbo_def nectxt_imp_supt_ctxt)
next
  show "⋀(R :: ('f gterm × 'f gterm) set). ground_critical_pair_theorem R"
    using ground_critical_pair_theorem .
next
  show "⋀clause⇩G. wfP (λ_ _. False) ∧ transp (λ_ _. False) ∧ asymp (λ_ _. False)"
    by (simp add: asympI)
next
  show "⋀τ. ∃f. ([], ()) = ([], τ)"
    by simp
next
  show "|UNIV :: unit set| ≤o |UNIV|"
    unfolding UNIV_unit
    by simp
qed

end

end