Structure gcdsetTheory

signature gcdsetTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val gcdset_def : thm

  (*  Theorems  *)
    val gcdset_EMPTY : thm
    val gcdset_INSERT : thm
    val gcdset_divides : thm
    val gcdset_greatest : thm

  val gcdset_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [gcd] Parent theory of "gcdset"

   [pred_set] Parent theory of "gcdset"

   [gcdset_def]  Definition

      |- ∀s.
           gcdset s =
           if (s = ∅) ∨ (s = {0}) then 0
           else
             MAX_SET
               ({n | n ≤ MIN_SET (s DELETE 0)} ∩
                {d | ∀e. e ∈ s ⇒ divides d e})

   [gcdset_EMPTY]  Theorem

      |- gcdset ∅ = 0

   [gcdset_INSERT]  Theorem

      |- gcdset (x INSERT s) = gcd x (gcdset s)

   [gcdset_divides]  Theorem

      |- ∀e. e ∈ s ⇒ divides (gcdset s) e

   [gcdset_greatest]  Theorem

      |- (∀e. e ∈ s ⇒ divides g e) ⇒ divides g (gcdset s)


*)
end

HOL 4, Kananaskis-11