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: monomorphic_term_typing where ℱ = unit_typing
  by unfold_locales

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 simp: infinite_UNIV intro: unit_types.exists_witness_if_exists_const_for_all_types)

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: monomorphic_term_typing where ℱ = types
  by unfold_locales

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
proof (unfold_locales, rule example_types.exists_witness_if_exists_const_for_all_types)
  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

end