Theory Superposition_Example

theory Superposition_Example
  imports
    Monomorphic_Superposition

    First_Order_Clause.IsaFoR_KBO
begin

(* TODO: use strictly_generalizes *)
abbreviation trivial_tiebreakers ::
  "'f gterm clause ⇒ ('f,'v) term clause ⇒ ('f,'v) term clause ⇒ bool" where
  "trivial_tiebreakers ≡ ⊥"

abbreviation trivial_select :: "'a clause ⇒ 'a clause" where
  "trivial_select _ ≡ {#}"

abbreviation unit_typing where
  "unit_typing _ _ ≡ Some ([], ())"

interpretation unit_types: witnessed_monomorphic_term_typing where ℱ = unit_typing
  by unfold_locales auto
                                           
interpretation example1: monomorphic_superposition_calculus where
    select = "trivial_select :: (('f :: weighted , 'v :: infinite) term atom) select" and
    lesst = less_kbo and
    ℱ = unit_typing and
    tiebreakers = trivial_tiebreakers
  by unfold_locales auto

instantiation nat :: infinite
begin

instance
  by intro_classes simp

end

datatype type = A | B

abbreviation types :: "nat ⇒ nat ⇒ (type list × type) option" where
  "types f n ≡
    let type = if even f then A else B
    in Some (replicate n type, type)"

interpretation example_types: witnessed_monomorphic_term_typing where ℱ = types
proof unfold_locales
  fix τ
  show "∃f. types f 0 = Some ([], τ)"
  proof (cases τ)
    case A
    show ?thesis
      unfolding A
      by (rule exI[of _ 0]) auto
  next
    case B
    show ?thesis
      unfolding B
      by (rule exI[of _ 1]) auto
  qed
qed

interpretation example2: monomorphic_superposition_calculus where
    select = "KBO.select_max :: (nat, nat) term atom select" and
    lesst = less_kbo and
    ℱ = types and
    tiebreakers = trivial_tiebreakers
  by unfold_locales

end