Theory Superposition_Example

theory Superposition_Example
  imports
    Superposition
    IsaFoR_Term_Copy
begin

(* TODO: Add more examples *)
abbreviation trivial_select :: "'a clause  'a clause" where
  "trivial_select _  {#}"

abbreviation trivial_tiebreakers where
  "trivial_tiebreakers _ _ _  False"

abbreviation unit_types where
  "unit_types _  ([], ())"

interpretation nonground_clause.

interpretation selection_function trivial_select
  by unfold_locales auto

(* TODO: We have to get the ground_critical_pair_theorem into the afp *)
locale superposition_example = 
  ground_critical_pair_theorem "TYPE('f :: weighted)"
begin

sublocale
  superposition_calculus
    "trivial_select :: ('f , 'v :: infinite) select"
    less_kbo
    unit_types
    trivial_tiebreakers
proof unfold_locales
  show "CG. transp (trivial_tiebreakers CG)"
    by simp
next
  show "CG. asymp (trivial_tiebreakers CG)"
    by auto
next
  show "CG. wfp (trivial_tiebreakers CG)"
    by simp
next
  show "τ. f. ([], ()) = ([], τ)"
    by simp
next
  show "|UNIV :: unit set| ≤o |UNIV|"
    unfolding UNIV_unit
    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 "wfp_on (range term.from_ground) less_kbo"
    using wfp_on_subset[OF wfP_less_kbo subset_UNIV] .
next
  show "totalp_on (range term.from_ground) less_kbo"
    using less_kbo_gtotal
    unfolding totalp_on_def Term.ground_vars_term_empty term.is_ground_iff_range_from_ground
    by blast
next
  fix
    c :: "('f, 'v) context" and
    t1 t2 :: "('f, 'v) term" 

  assume "less_kbo t1 t2"

  then show "less_kbo ct1 ct2"
    using KBO.S_ctxt less_kbo_def 
    by blast
next
  fix
    t1 t2 :: "('f, 'v) term" and
    γ :: "('f, 'v) subst"

  assume "less_kbo t1 t2"

  then show "less_kbo (t1 ⋅t γ) (t2 ⋅t γ)"
    using less_kbo_subst by blast
next
  fix
    t :: "('f, 'v) term" and
    c :: "('f, 'v) context"
  assume
    "term.is_ground t"
    "context.is_ground c"
    "c  "
  
  then show "less_kbo t ct"
    by (simp add: KBO.S_supt less_kbo_def nectxt_imp_supt_ctxt)
qed

end

end