Structure wellorderTheory

signature wellorderTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val ADD1_def : thm
    val elsOf_def : thm
    val finite_def : thm
    val fromNatWO_def : thm
    val iseg_def : thm
    val orderiso_def : thm
    val orderlt_def : thm
    val remove_def : thm
    val wZERO_def : thm
    val wellfounded_def : thm
    val wellorder_ABSREP : thm
    val wellorder_TY_DEF : thm
    val wellorder_def : thm
    val wleast_def : thm
    val wo2wo_def : thm
    val wobound_def : thm
  
  (*  Theorems  *)
    val FORALL_NUM : thm
    val IMAGE_wo2wo_SUBSET : thm
    val INJ_preserves_antisym : thm
    val INJ_preserves_linear_order : thm
    val INJ_preserves_transitive : thm
    val INJ_preserves_wellorder : thm
    val LT_wZERO : thm
    val WEXTENSION : thm
    val WIN_ADD1 : thm
    val WIN_REFL : thm
    val WIN_TRANS : thm
    val WIN_WF : thm
    val WIN_WF2 : thm
    val WIN_WLE : thm
    val WIN_elsOf : thm
    val WIN_remove : thm
    val WIN_trichotomy : thm
    val WIN_wZERO : thm
    val WIN_wobound : thm
    val WLE_ANTISYM : thm
    val WLE_TRANS : thm
    val WLE_WIN : thm
    val WLE_WIN_EQ : thm
    val WLE_elsOf : thm
    val WLE_wZERO : thm
    val WLE_wobound : thm
    val allsets_wellorderable : thm
    val antisym_rrestrict : thm
    val destWO_mkWO : thm
    val domain_IMAGE_ff : thm
    val elsOf_ADD1 : thm
    val elsOf_EQ_EMPTY : thm
    val elsOf_WLE : thm
    val elsOf_cardeq_iso : thm
    val elsOf_fromNatWO : thm
    val elsOf_remove : thm
    val elsOf_wZERO : thm
    val elsOf_wobound : thm
    val finite_iso : thm
    val finite_wZERO : thm
    val fromNatWO_11 : thm
    val linear_order_rrestrict : thm
    val mkWO_destWO : thm
    val mono_woseg : thm
    val orderiso_REFL : thm
    val orderiso_SYM : thm
    val orderiso_TRANS : thm
    val orderiso_thm : thm
    val orderiso_unique : thm
    val orderiso_wZERO : thm
    val orderlt_REFL : thm
    val orderlt_TRANS : thm
    val orderlt_WF : thm
    val orderlt_orderiso : thm
    val orderlt_trichotomy : thm
    val range_IMAGE_ff : thm
    val reflexive_rrestrict : thm
    val rrestrict_SUBSET : thm
    val seteq_wlog : thm
    val strict_UNION : thm
    val strict_subset : thm
    val transitive_rrestrict : thm
    val transitive_strict : thm
    val wellfounded_WF : thm
    val wellfounded_subset : thm
    val wellorder_ADD1 : thm
    val wellorder_EMPTY : thm
    val wellorder_SING : thm
    val wellorder_cases : thm
    val wellorder_fromNat : thm
    val wellorder_fromNat_SUM : thm
    val wellorder_remove : thm
    val wellorder_rrestrict : thm
    val wleast_EQ_NONE : thm
    val wleast_IN_wo : thm
    val wleast_SUBSET : thm
    val wo2wo_11 : thm
    val wo2wo_EQ_NONE : thm
    val wo2wo_EQ_NONE_woseg : thm
    val wo2wo_EQ_SOME_downwards : thm
    val wo2wo_IN_w2 : thm
    val wo2wo_ONTO : thm
    val wo2wo_mono : thm
    val wo2wo_thm : thm
    val wo_INDUCTION : thm
    val wobound2 : thm
    val wobounds_preserve_bijections : thm
  
  val wellorder_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [indexedLists] Parent theory of "wellorder"
   
   [patternMatches] Parent theory of "wellorder"
   
   [set_relation] Parent theory of "wellorder"
   
   [ADD1_def]  Definition
      
      ⊢ ∀e w.
            ADD1 e w =
            if e ∈ elsOf w then w
            else mkWO (destWO w ∪ {(x,e) | x ∈ elsOf w} ∪ {(e,e)})
   
   [elsOf_def]  Definition
      
      ⊢ ∀w. elsOf w = domain (destWO w) ∪ wrange w
   
   [finite_def]  Definition
      
      ⊢ ∀w. finite w ⇔ FINITE (elsOf w)
   
   [fromNatWO_def]  Definition
      
      ⊢ ∀n. fromNatWO n = mkWO {(INL i,INL j) | i ≤ j ∧ j < n}
   
   [iseg_def]  Definition
      
      ⊢ ∀w x. iseg w x = {y | (y,x) WIN w}
   
   [orderiso_def]  Definition
      
      ⊢ ∀w1 w2.
            orderiso w1 w2 ⇔
            ∃f.
                (∀x. x ∈ elsOf w1 ⇒ f x ∈ elsOf w2) ∧
                (∀x1 x2.
                     x1 ∈ elsOf w1 ∧ x2 ∈ elsOf w1 ⇒
                     ((f x1 = f x2) ⇔ (x1 = x2))) ∧
                (∀y. y ∈ elsOf w2 ⇒ ∃x. x ∈ elsOf w1 ∧ (f x = y)) ∧
                ∀x y. (x,y) WIN w1 ⇒ (f x,f y) WIN w2
   
   [orderlt_def]  Definition
      
      ⊢ ∀w1 w2.
            orderlt w1 w2 ⇔ ∃x. x ∈ elsOf w2 ∧ orderiso w1 (wobound x w2)
   
   [remove_def]  Definition
      
      ⊢ ∀e w. remove e w = mkWO {(x,y) | x ≠ e ∧ y ≠ e ∧ (x,y) WLE w}
   
   [wZERO_def]  Definition
      
      ⊢ wZERO = mkWO ∅
   
   [wellfounded_def]  Definition
      
      ⊢ ∀R.
            wellfounded R ⇔
            ∀s. (∃w. w ∈ s) ⇒ ∃min. min ∈ s ∧ ∀w. (w,min) ∈ R ⇒ w ∉ s
   
   [wellorder_ABSREP]  Definition
      
      ⊢ (∀a. mkWO (destWO a) = a) ∧ ∀r. wellorder r ⇔ (destWO (mkWO r) = r)
   
   [wellorder_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION wellorder rep
   
   [wellorder_def]  Definition
      
      ⊢ ∀R.
            wellorder R ⇔
            wellfounded (strict R) ∧ linear_order R (domain R ∪ range R) ∧
            reflexive R (domain R ∪ range R)
   
   [wleast_def]  Definition
      
      ⊢ ∀w s.
            wleast w s =
            some x.
                x ∈ elsOf w ∧ x ∉ s ∧
                ∀y. y ∈ elsOf w ∧ y ∉ s ∧ x ≠ y ⇒ (x,y) WIN w
   
   [wo2wo_def]  Definition
      
      ⊢ ∀w1 w2.
            wo2wo w1 w2 =
            WFREC (λx y. (x,y) WIN w1)
              (λf x.
                   (let
                      s0 = IMAGE f (iseg w1 x) ;
                      s1 = IMAGE THE (s0 DELETE NONE)
                    in
                      if s1 = elsOf w2 then NONE else wleast w2 s1))
   
   [wobound_def]  Definition
      
      ⊢ ∀x w. wobound x w = mkWO (rrestrict (destWO w) (iseg w x))
   
   [FORALL_NUM]  Theorem
      
      ⊢ (∀n. P n) ⇔ P 0 ∧ ∀n. P (SUC n)
   
   [IMAGE_wo2wo_SUBSET]  Theorem
      
      ⊢ woseg w1 w2 x ⊆ elsOf w2
   
   [INJ_preserves_antisym]  Theorem
      
      ⊢ antisym r ∧ INJ f (domain r ∪ range r) t ⇒
        antisym (IMAGE (f ## f) r)
   
   [INJ_preserves_linear_order]  Theorem
      
      ⊢ linear_order r (domain r ∪ range r) ∧ INJ f (domain r ∪ range r) t ⇒
        linear_order (IMAGE (f ## f) r) (IMAGE f (domain r ∪ range r))
   
   [INJ_preserves_transitive]  Theorem
      
      ⊢ transitive r ∧ INJ f (domain r ∪ range r) t ⇒
        transitive (IMAGE (f ## f) r)
   
   [INJ_preserves_wellorder]  Theorem
      
      ⊢ wellorder r ∧ INJ f (domain r ∪ range r) t ⇒
        wellorder (IMAGE (f ## f) r)
   
   [LT_wZERO]  Theorem
      
      ⊢ orderlt w wZERO ⇔ F
   
   [WEXTENSION]  Theorem
      
      ⊢ (w1 = w2) ⇔ ∀a b. (a,b) WLE w1 ⇔ (a,b) WLE w2
   
   [WIN_ADD1]  Theorem
      
      ⊢ (x,y) WIN ADD1 e w ⇔
        e ∉ elsOf w ∧ x ∈ elsOf w ∧ (y = e) ∨ (x,y) WIN w
   
   [WIN_REFL]  Theorem
      
      ⊢ (x,x) WIN w ⇔ F
   
   [WIN_TRANS]  Theorem
      
      ⊢ (x,y) WIN w ∧ (y,z) WIN w ⇒ (x,z) WIN w
   
   [WIN_WF]  Theorem
      
      ⊢ wellfounded (λp. p WIN w)
   
   [WIN_WF2]  Theorem
      
      ⊢ WF (λx y. (x,y) WIN w)
   
   [WIN_WLE]  Theorem
      
      ⊢ (x,y) WIN w ⇒ (x,y) WLE w
   
   [WIN_elsOf]  Theorem
      
      ⊢ (x,y) WIN w ⇒ x ∈ elsOf w ∧ y ∈ elsOf w
   
   [WIN_remove]  Theorem
      
      ⊢ (x,y) WIN remove e w ⇔ x ≠ e ∧ y ≠ e ∧ (x,y) WIN w
   
   [WIN_trichotomy]  Theorem
      
      ⊢ ∀x y.
            x ∈ elsOf w ∧ y ∈ elsOf w ⇒ (x,y) WIN w ∨ (x = y) ∨ (y,x) WIN w
   
   [WIN_wZERO]  Theorem
      
      ⊢ (x,y) WIN wZERO ⇔ F
   
   [WIN_wobound]  Theorem
      
      ⊢ (x,y) WIN wobound z w ⇔ (x,z) WIN w ∧ (y,z) WIN w ∧ (x,y) WIN w
   
   [WLE_ANTISYM]  Theorem
      
      ⊢ (x,y) WLE w ∧ (y,x) WLE w ⇒ (x = y)
   
   [WLE_TRANS]  Theorem
      
      ⊢ (x,y) WLE w ∧ (y,z) WLE w ⇒ (x,z) WLE w
   
   [WLE_WIN]  Theorem
      
      ⊢ (x,y) WLE w ⇒ (x = y) ∨ (x,y) WIN w
   
   [WLE_WIN_EQ]  Theorem
      
      ⊢ (x,y) WLE w ⇔ (x = y) ∧ x ∈ elsOf w ∨ (x,y) WIN w
   
   [WLE_elsOf]  Theorem
      
      ⊢ (x,y) WLE w ⇒ x ∈ elsOf w ∧ y ∈ elsOf w
   
   [WLE_wZERO]  Theorem
      
      ⊢ (x,y) WLE wZERO ⇔ F
   
   [WLE_wobound]  Theorem
      
      ⊢ (x,y) WLE wobound z w ⇔ (x,z) WIN w ∧ (y,z) WIN w ∧ (x,y) WLE w
   
   [allsets_wellorderable]  Theorem
      
      ⊢ ∀s. ∃wo. elsOf wo = s
   
   [antisym_rrestrict]  Theorem
      
      ⊢ antisym r ⇒ antisym (rrestrict r s)
   
   [destWO_mkWO]  Theorem
      
      ⊢ ∀r. wellorder r ⇒ (destWO (mkWO r) = r)
   
   [domain_IMAGE_ff]  Theorem
      
      ⊢ domain (IMAGE (f ## g) r) = IMAGE f (domain r)
   
   [elsOf_ADD1]  Theorem
      
      ⊢ elsOf (ADD1 e w) = e INSERT elsOf w
   
   [elsOf_EQ_EMPTY]  Theorem
      
      ⊢ (elsOf w = ∅) ⇔ (w = wZERO)
   
   [elsOf_WLE]  Theorem
      
      ⊢ x ∈ elsOf w ⇔ (x,x) WLE w
   
   [elsOf_cardeq_iso]  Theorem
      
      ⊢ INJ f (elsOf wo) 𝕌(:α) ⇒ ∃wo'. orderiso wo wo'
   
   [elsOf_fromNatWO]  Theorem
      
      ⊢ elsOf (fromNatWO n) = IMAGE INL (count n)
   
   [elsOf_remove]  Theorem
      
      ⊢ elsOf (remove e w) = elsOf w DELETE e
   
   [elsOf_wZERO]  Theorem
      
      ⊢ elsOf wZERO = ∅
   
   [elsOf_wobound]  Theorem
      
      ⊢ elsOf (wobound x w) = {y | (y,x) WIN w}
   
   [finite_iso]  Theorem
      
      ⊢ orderiso w1 w2 ⇒ (finite w1 ⇔ finite w2)
   
   [finite_wZERO]  Theorem
      
      ⊢ finite wZERO
   
   [fromNatWO_11]  Theorem
      
      ⊢ (fromNatWO i = fromNatWO j) ⇔ (i = j)
   
   [linear_order_rrestrict]  Theorem
      
      ⊢ linear_order r (domain r ∪ range r) ⇒
        linear_order (rrestrict r s)
          (domain (rrestrict r s) ∪ range (rrestrict r s))
   
   [mkWO_destWO]  Theorem
      
      ⊢ ∀a. mkWO (destWO a) = a
   
   [mono_woseg]  Theorem
      
      ⊢ (x1,x2) WIN w1 ⇒ woseg w1 w2 x1 ⊆ woseg w1 w2 x2
   
   [orderiso_REFL]  Theorem
      
      ⊢ ∀w. orderiso w w
   
   [orderiso_SYM]  Theorem
      
      ⊢ ∀w1 w2. orderiso w1 w2 ⇒ orderiso w2 w1
   
   [orderiso_TRANS]  Theorem
      
      ⊢ ∀w1 w2 w3. orderiso w1 w2 ∧ orderiso w2 w3 ⇒ orderiso w1 w3
   
   [orderiso_thm]  Theorem
      
      ⊢ orderiso w1 w2 ⇔
        ∃f.
            BIJ f (elsOf w1) (elsOf w2) ∧
            ∀x y. (x,y) WIN w1 ⇒ (f x,f y) WIN w2
   
   [orderiso_unique]  Theorem
      
      ⊢ BIJ f1 (elsOf w1) (elsOf w2) ∧ BIJ f2 (elsOf w1) (elsOf w2) ∧
        (∀x y. (x,y) WIN w1 ⇒ (f1 x,f1 y) WIN w2) ∧
        (∀x y. (x,y) WIN w1 ⇒ (f2 x,f2 y) WIN w2) ⇒
        ∀x. x ∈ elsOf w1 ⇒ (f1 x = f2 x)
   
   [orderiso_wZERO]  Theorem
      
      ⊢ orderiso wZERO w ⇔ (w = wZERO)
   
   [orderlt_REFL]  Theorem
      
      ⊢ orderlt w w ⇔ F
   
   [orderlt_TRANS]  Theorem
      
      ⊢ ∀w1 w2 w3. orderlt w1 w2 ∧ orderlt w2 w3 ⇒ orderlt w1 w3
   
   [orderlt_WF]  Theorem
      
      ⊢ WF orderlt
   
   [orderlt_orderiso]  Theorem
      
      ⊢ orderiso x0 y0 ∧ orderiso a0 b0 ⇒ (orderlt x0 a0 ⇔ orderlt y0 b0)
   
   [orderlt_trichotomy]  Theorem
      
      ⊢ orderlt w1 w2 ∨ orderiso w1 w2 ∨ orderlt w2 w1
   
   [range_IMAGE_ff]  Theorem
      
      ⊢ range (IMAGE (f ## g) r) = IMAGE g (range r)
   
   [reflexive_rrestrict]  Theorem
      
      ⊢ reflexive r (domain r ∪ range r) ⇒
        reflexive (rrestrict r s)
          (domain (rrestrict r s) ∪ range (rrestrict r s))
   
   [rrestrict_SUBSET]  Theorem
      
      ⊢ rrestrict r s ⊆ r
   
   [seteq_wlog]  Theorem
      
      ⊢ ∀f.
            (∀a b. P a b ⇒ P b a) ∧ (∀x a b. P a b ∧ x ∈ f a ⇒ x ∈ f b) ⇒
            ∀a b. P a b ⇒ (f a = f b)
   
   [strict_UNION]  Theorem
      
      ⊢ strict (r1 ∪ r2) = strict r1 ∪ strict r2
   
   [strict_subset]  Theorem
      
      ⊢ r1 ⊆ r2 ⇒ strict r1 ⊆ strict r2
   
   [transitive_rrestrict]  Theorem
      
      ⊢ transitive r ⇒ transitive (rrestrict r s)
   
   [transitive_strict]  Theorem
      
      ⊢ transitive r ∧ antisym r ⇒ transitive (strict r)
   
   [wellfounded_WF]  Theorem
      
      ⊢ wellfounded R ⇔ WF (CURRY R)
   
   [wellfounded_subset]  Theorem
      
      ⊢ ∀r0 r. wellfounded r ∧ r0 ⊆ r ⇒ wellfounded r0
   
   [wellorder_ADD1]  Theorem
      
      ⊢ e ∉ elsOf w ⇒
        wellorder (destWO w ∪ {(x,e) | x ∈ elsOf w} ∪ {(e,e)})
   
   [wellorder_EMPTY]  Theorem
      
      ⊢ wellorder ∅
   
   [wellorder_SING]  Theorem
      
      ⊢ wellorder {(x,y)} ⇔ (x = y)
   
   [wellorder_cases]  Theorem
      
      ⊢ ∀w. ∃s. wellorder s ∧ (w = mkWO s)
   
   [wellorder_fromNat]  Theorem
      
      ⊢ wellorder {(i,j) | i ≤ j ∧ j < n}
   
   [wellorder_fromNat_SUM]  Theorem
      
      ⊢ wellorder {(INL i,INL j) | i ≤ j ∧ j < n}
   
   [wellorder_remove]  Theorem
      
      ⊢ wellorder {(x,y) | x ≠ e ∧ y ≠ e ∧ (x,y) WLE w}
   
   [wellorder_rrestrict]  Theorem
      
      ⊢ wellorder (rrestrict (destWO w) s)
   
   [wleast_EQ_NONE]  Theorem
      
      ⊢ (wleast w s = NONE) ⇒ elsOf w ⊆ s
   
   [wleast_IN_wo]  Theorem
      
      ⊢ (wleast w s = SOME x) ⇒
        x ∈ elsOf w ∧ x ∉ s ∧ ∀y. y ∈ elsOf w ∧ y ∉ s ∧ x ≠ y ⇒ (x,y) WIN w
   
   [wleast_SUBSET]  Theorem
      
      ⊢ (wleast w s1 = SOME x) ∧ (wleast w s2 = SOME y) ∧ s1 ⊆ s2 ⇒
        (x = y) ∨ (x,y) WIN w
   
   [wo2wo_11]  Theorem
      
      ⊢ x1 ∈ elsOf w1 ∧ x2 ∈ elsOf w1 ∧ (wo2wo w1 w2 x1 = SOME y) ∧
        (wo2wo w1 w2 x2 = SOME y) ⇒
        (x1 = x2)
   
   [wo2wo_EQ_NONE]  Theorem
      
      ⊢ ∀x.
            (wo2wo w1 w2 x = NONE) ⇒
            ∀y. (x,y) WIN w1 ⇒ (wo2wo w1 w2 y = NONE)
   
   [wo2wo_EQ_NONE_woseg]  Theorem
      
      ⊢ (wo2wo w1 w2 x = NONE) ⇒ (elsOf w2 = woseg w1 w2 x)
   
   [wo2wo_EQ_SOME_downwards]  Theorem
      
      ⊢ ∀x y.
            (wo2wo w1 w2 x = SOME y) ⇒
            ∀x0. (x0,x) WIN w1 ⇒ ∃y0. wo2wo w1 w2 x0 = SOME y0
   
   [wo2wo_IN_w2]  Theorem
      
      ⊢ ∀x y. (wo2wo w1 w2 x = SOME y) ⇒ y ∈ elsOf w2
   
   [wo2wo_ONTO]  Theorem
      
      ⊢ x ∈ elsOf w1 ∧ (wo2wo w1 w2 x = SOME y) ∧ (y0,y) WIN w2 ⇒
        ∃x0. x0 ∈ elsOf w1 ∧ (wo2wo w1 w2 x0 = SOME y0)
   
   [wo2wo_mono]  Theorem
      
      ⊢ (wo2wo w1 w2 x0 = SOME y0) ∧ (wo2wo w1 w2 x = SOME y) ∧
        (x0,x) WIN w1 ⇒
        (y0,y) WIN w2
   
   [wo2wo_thm]  Theorem
      
      ⊢ ∀x.
            wo2wo w w2 x =
            (let
               s0 = IMAGE (wo2wo w w2) (iseg w x) ;
               s1 = IMAGE THE (s0 DELETE NONE)
             in
               if s1 = elsOf w2 then NONE else wleast w2 s1)
   
   [wo_INDUCTION]  Theorem
      
      ⊢ ∀P w.
            (∀x. (∀y. (y,x) WIN w ⇒ y ∈ elsOf w ⇒ P y) ⇒ x ∈ elsOf w ⇒ P x) ⇒
            ∀x. x ∈ elsOf w ⇒ P x
   
   [wobound2]  Theorem
      
      ⊢ (a,b) WIN w ⇒ (wobound a (wobound b w) = wobound a w)
   
   [wobounds_preserve_bijections]  Theorem
      
      ⊢ BIJ f (elsOf w1) (elsOf w2) ∧ x ∈ elsOf w1 ∧
        (∀x y. (x,y) WIN w1 ⇒ (f x,f y) WIN w2) ⇒
        BIJ f (elsOf (wobound x w1)) (elsOf (wobound (f x) w2))
   
   
*)
end

HOL 4, Kananaskis-11