Structure wotTheory

signature wotTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val StrongWellOrder_def : thm
    val WeakWellOrder_def : thm
    val chain_def : thm
    val cpl_def : thm
    val mex_def : thm
    val mex_less_def : thm
    val mex_less_eq_def : thm
    val preds_image_def : thm
    val setsuc_def : thm
    val succl_def : thm
    val tower_def : thm
    val uncl_def : thm
  
  (*  Theorems  *)
    val StrongWellOrderExists : thm
  
  val wot_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [indexedLists] Parent theory of "wot"
   
   [patternMatches] Parent theory of "wot"
   
   [StrongWellOrder_def]  Definition
      
      |- !R. StrongWellOrder R <=> StrongLinearOrder R /\ WF R
   
   [WeakWellOrder_def]  Definition
      
      |- !R. WeakWellOrder R <=>
             WeakOrder R /\
             !B. B <> {} ==> ?m. m IN B /\ !b. b IN B ==> R m b
   
   [chain_def]  Definition
      
      |- !C. chain C <=> !a b. a IN C /\ b IN C ==> a cpl b
   
   [cpl_def]  Definition
      
      |- !A B. A cpl B <=> A SUBSET B \/ B SUBSET A
   
   [mex_def]  Definition
      
      |- !s. mex s = CHOICE (COMPL s)
   
   [mex_less_def]  Definition
      
      |- $mex_less = STRORD $mex_less_eq
   
   [mex_less_eq_def]  Definition
      
      |- !a b. a mex_less_eq b <=> preds a SUBSET preds b
   
   [preds_image_def]  Definition
      
      |- !X. preds_image X = {preds x | x IN X}
   
   [setsuc_def]  Definition
      
      |- !s. setsuc s = mex s INSERT s
   
   [succl_def]  Definition
      
      |- !c. succl c <=> !s. s IN c ==> setsuc s IN c
   
   [tower_def]  Definition
      
      |- !A. tower A <=> succl A /\ uncl A
   
   [uncl_def]  Definition
      
      |- !c. uncl c <=> !w. w SUBSET c /\ chain w ==> BIGUNION w IN c
   
   [StrongWellOrderExists]  Theorem
      
      |- ?R. StrongLinearOrder R /\ WF R
   
   
*)
end

HOL 4, Kananaskis-14