Structure ordinalNotationTheory


Source File Identifier index Theory binding index

signature ordinalNotationTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val cf1_def : thm
    val cf2_def : thm
    val coeff_def : thm
    val expt_def : thm
    val finp_def : thm
    val ord_less_def : thm
    val osyntax_TY_DEF : thm
    val osyntax_case_def : thm
    val osyntax_size_def : thm
    val padd_def : thm
    val rank_def : thm
    val restn_def : thm
    val tail_def : thm
  
  (*  Theorems  *)
    val WF_ord_less : thm
    val datatype_osyntax : thm
    val decompose_plus : thm
    val e0_INDUCTION : thm
    val e0_RECURSION : thm
    val is_ord_cases : thm
    val is_ord_coeff_pos : thm
    val is_ord_downclosed : thm
    val is_ord_equations : thm
    val is_ord_expt_closed : thm
    val is_ord_ind : thm
    val is_ord_rules : thm
    val is_ord_strong_ind : thm
    val is_ord_strongind : thm
    val is_ord_tail_closed : thm
    val lemma : thm
    val main_lemma : thm
    val oless_End_End : thm
    val oless_antirefl : thm
    val oless_antisym : thm
    val oless_cases : thm
    val oless_equations : thm
    val oless_expt : thm
    val oless_imp_rank_leq : thm
    val oless_ind : thm
    val oless_rules : thm
    val oless_strong_ind : thm
    val oless_strongind : thm
    val oless_tail : thm
    val ord_add_def : thm
    val ord_add_ind : thm
    val ord_mult_def : thm
    val ord_mult_ind : thm
    val ord_sub_def : thm
    val ord_sub_ind : thm
    val osyntax_11 : thm
    val osyntax_Axiom : thm
    val osyntax_case_cong : thm
    val osyntax_case_eq : thm
    val osyntax_distinct : thm
    val osyntax_induction : thm
    val osyntax_nchotomy : thm
    val padd_compute : thm
    val pmult_def : thm
    val pmult_ind : thm
    val rank_0_End : thm
    val rank_expt : thm
    val rank_finp : thm
    val rank_less_imp_oless : thm
    val rank_positive : thm
    val rank_positive_exists : thm
    val rank_positive_expt : thm
    val restn_compute : thm
  
  val ordinalNotation_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [indexedLists] Parent theory of "ordinalNotation"
   
   [patternMatches] Parent theory of "ordinalNotation"
   
   [cf1_def]  Definition
      
      ⊢ (∀v0 b. cf1 (End v0) b = 0) ∧
        ∀e1 c1 k1 b.
          cf1 (Plus e1 c1 k1) b =
          if ord_less (expt b) e1 then 1 + cf1 k1 b else 0
   
   [cf2_def]  Definition
      
      ⊢ ∀a b n. cf2 a b n = n + cf1 (restn a n) b
   
   [coeff_def]  Definition
      
      ⊢ (∀x. coeff (End x) = x) ∧ ∀e k t. coeff (Plus e k t) = k
   
   [expt_def]  Definition
      
      ⊢ (∀v0. expt (End v0) = End 0) ∧ ∀e k t. expt (Plus e k t) = e
   
   [finp_def]  Definition
      
      ⊢ (∀v0. finp (End v0) ⇔ T) ∧ ∀v1 v2 v3. finp (Plus v1 v2 v3) ⇔ F
   
   [ord_less_def]  Definition
      
      ⊢ ∀x y. ord_less x y ⇔ is_ord x ∧ is_ord y ∧ oless x y
   
   [osyntax_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0'.
                 ∀ $var$('osyntax').
                   (∀a0'.
                      (∃a. a0' =
                           (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM))
                             a) ∨
                      (∃a0 a1 a2.
                         (a0' =
                          (λa0 a1 a2.
                               ind_type$CONSTR (SUC 0) a1
                                 (ind_type$FCONS a0
                                    (ind_type$FCONS a2
                                       (λn. ind_type$BOTTOM)))) a0 a1 a2) ∧
                         $var$('osyntax') a0 ∧ $var$('osyntax') a2) ⇒
                      $var$('osyntax') a0') ⇒
                   $var$('osyntax') a0') rep
   
   [osyntax_case_def]  Definition
      
      ⊢ (∀a f f1. osyntax_CASE (End a) f f1 = f a) ∧
        ∀a0 a1 a2 f f1. osyntax_CASE (Plus a0 a1 a2) f f1 = f1 a0 a1 a2
   
   [osyntax_size_def]  Definition
      
      ⊢ (∀a. osyntax_size (End a) = 1 + a) ∧
        ∀a0 a1 a2.
          osyntax_size (Plus a0 a1 a2) =
          1 + (osyntax_size a0 + (a1 + osyntax_size a2))
   
   [padd_def]  Definition
      
      ⊢ (∀a b. padd a b 0 = ord_add a b) ∧
        ∀a b n.
          padd a b (SUC n) = Plus (expt a) (coeff a) (padd (tail a) b n)
   
   [rank_def]  Definition
      
      ⊢ (∀v0. rank (End v0) = 0) ∧ ∀e k t. rank (Plus e k t) = 1 + rank e
   
   [restn_def]  Definition
      
      ⊢ (∀a. restn a 0 = a) ∧ ∀a n. restn a (SUC n) = restn (tail a) n
   
   [tail_def]  Definition
      
      ⊢ ∀e k t. tail (Plus e k t) = t
   
   [WF_ord_less]  Theorem
      
      ⊢ WF ord_less
   
   [datatype_osyntax]  Theorem
      
      ⊢ DATATYPE (osyntax End Plus)
   
   [decompose_plus]  Theorem
      
      ⊢ ∀e k t.
          is_ord (Plus e k t) ⇒
          is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ oless (expt t) e
   
   [e0_INDUCTION]  Theorem
      
      ⊢ ∀P f. (∀x. (∀y. ord_less (f y) (f x) ⇒ P y) ⇒ P x) ⇒ ∀x. P x
   
   [e0_RECURSION]  Theorem
      
      ⊢ ∀f. ∃!g. ∀x. g x = M (RESTRICT g (λx y. ord_less (f x) (f y)) x) x
   
   [is_ord_cases]  Theorem
      
      ⊢ ∀a0.
          is_ord a0 ⇔
          (∃k. a0 = End k) ∨
          ∃e k t.
            (a0 = Plus e k t) ∧ is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧
            oless (expt t) e
   
   [is_ord_coeff_pos]  Theorem
      
      ⊢ ∀x. ¬finp x ∧ is_ord x ⇒ 0 < coeff x
   
   [is_ord_downclosed]  Theorem
      
      ⊢ is_ord (Plus w k t) ⇒ is_ord w ∧ is_ord t
   
   [is_ord_equations]  Theorem
      
      ⊢ (is_ord (End k) ⇔ T) ∧
        (is_ord (Plus e k t) ⇔
         is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ oless (expt t) e)
   
   [is_ord_expt_closed]  Theorem
      
      ⊢ ∀x. is_ord x ⇒ is_ord (expt x)
   
   [is_ord_ind]  Theorem
      
      ⊢ ∀is_ord'.
          (∀k. is_ord' (End k)) ∧
          (∀e k t.
             is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord' t ∧ oless (expt t) e ⇒
             is_ord' (Plus e k t)) ⇒
          ∀a0. is_ord a0 ⇒ is_ord' a0
   
   [is_ord_rules]  Theorem
      
      ⊢ (∀k. is_ord (End k)) ∧
        ∀e k t.
          is_ord e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧ oless (expt t) e ⇒
          is_ord (Plus e k t)
   
   [is_ord_strong_ind]  Theorem
      
      ⊢ ∀is_ord'.
          (∀k. is_ord' (End k)) ∧
          (∀e k t.
             is_ord e ∧ is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧
             is_ord' t ∧ oless (expt t) e ⇒
             is_ord' (Plus e k t)) ⇒
          ∀a0. is_ord a0 ⇒ is_ord' a0
   
   [is_ord_strongind]  Theorem
      
      ⊢ ∀is_ord'.
          (∀k. is_ord' (End k)) ∧
          (∀e k t.
             is_ord e ∧ is_ord' e ∧ e ≠ End 0 ∧ 0 < k ∧ is_ord t ∧
             is_ord' t ∧ oless (expt t) e ⇒
             is_ord' (Plus e k t)) ⇒
          ∀a0. is_ord a0 ⇒ is_ord' a0
   
   [is_ord_tail_closed]  Theorem
      
      ⊢ ∀x. ¬finp x ∧ is_ord x ⇒ is_ord (tail x)
   
   [lemma]  Theorem
      
      ⊢ ∀n P.
          (∃x. is_ord x ∧ P x ∧ rank x ≤ n) ⇒
          ∃m. is_ord m ∧ P m ∧ rank m ≤ n ∧
              ∀y. is_ord y ∧ rank y ≤ n ∧ oless y m ⇒ ¬P y
   
   [main_lemma]  Theorem
      
      ⊢ ∀P. (∃x. P x ∧ is_ord x) ⇒
            ∃x. P x ∧ is_ord x ∧ ∀y. is_ord y ∧ oless y x ⇒ ¬P y
   
   [oless_End_End]  Theorem
      
      ⊢ ∀k1 k2. oless (End k1) (End k2) ⇒ k1 < k2
   
   [oless_antirefl]  Theorem
      
      ⊢ ∀x. is_ord x ⇒ ¬oless x x
   
   [oless_antisym]  Theorem
      
      ⊢ ∀x y. is_ord x ∧ is_ord y ∧ oless x y ⇒ ¬oless y x
   
   [oless_cases]  Theorem
      
      ⊢ ∀a0 a1.
          oless a0 a1 ⇔
          (∃k1 k2. (a0 = End k1) ∧ (a1 = End k2) ∧ k1 < k2) ∨
          (∃k1 e2 k2 t2. (a0 = End k1) ∧ (a1 = Plus e2 k2 t2)) ∨
          (∃e1 k1 t1 e2 k2 t2.
             (a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ oless e1 e2) ∨
          (∃e1 k1 t1 e2 k2 t2.
             (a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ (e1 = e2) ∧
             k1 < k2) ∨
          ∃e1 k1 t1 e2 k2 t2.
            (a0 = Plus e1 k1 t1) ∧ (a1 = Plus e2 k2 t2) ∧ (e1 = e2) ∧
            (k1 = k2) ∧ oless t1 t2
   
   [oless_equations]  Theorem
      
      ⊢ (oless (End m) (End n) ⇔ m < n) ∧
        (oless (End m) (Plus e k t) ⇔ T) ∧
        (oless (Plus e k t) (End m) ⇔ F) ∧
        (oless (Plus e1 k1 t1) (Plus e2 k2 t2) ⇔
         if oless e1 e2 then T
         else if (e1 = e2) ∧ k1 < k2 then T
         else if (e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 then T
         else F)
   
   [oless_expt]  Theorem
      
      ⊢ ∀e k t. is_ord (Plus e k t) ⇒ oless e (Plus e k t)
   
   [oless_imp_rank_leq]  Theorem
      
      ⊢ ∀x y. is_ord x ∧ is_ord y ∧ oless x y ⇒ rank x ≤ rank y
   
   [oless_ind]  Theorem
      
      ⊢ ∀oless'.
          (∀k1 k2. k1 < k2 ⇒ oless' (End k1) (End k2)) ∧
          (∀k1 e2 k2 t2. oless' (End k1) (Plus e2 k2 t2)) ∧
          (∀e1 k1 t1 e2 k2 t2.
             oless' e1 e2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
          (∀e1 k1 t1 e2 k2 t2.
             (e1 = e2) ∧ k1 < k2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
          (∀e1 k1 t1 e2 k2 t2.
             (e1 = e2) ∧ (k1 = k2) ∧ oless' t1 t2 ⇒
             oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
          ∀a0 a1. oless a0 a1 ⇒ oless' a0 a1
   
   [oless_rules]  Theorem
      
      ⊢ (∀k1 k2. k1 < k2 ⇒ oless (End k1) (End k2)) ∧
        (∀k1 e2 k2 t2. oless (End k1) (Plus e2 k2 t2)) ∧
        (∀e1 k1 t1 e2 k2 t2.
           oless e1 e2 ⇒ oless (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
        (∀e1 k1 t1 e2 k2 t2.
           (e1 = e2) ∧ k1 < k2 ⇒ oless (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
        ∀e1 k1 t1 e2 k2 t2.
          (e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 ⇒
          oless (Plus e1 k1 t1) (Plus e2 k2 t2)
   
   [oless_strong_ind]  Theorem
      
      ⊢ ∀oless'.
          (∀k1 k2. k1 < k2 ⇒ oless' (End k1) (End k2)) ∧
          (∀k1 e2 k2 t2. oless' (End k1) (Plus e2 k2 t2)) ∧
          (∀e1 k1 t1 e2 k2 t2.
             oless e1 e2 ∧ oless' e1 e2 ⇒
             oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
          (∀e1 k1 t1 e2 k2 t2.
             (e1 = e2) ∧ k1 < k2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
          (∀e1 k1 t1 e2 k2 t2.
             (e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 ∧ oless' t1 t2 ⇒
             oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
          ∀a0 a1. oless a0 a1 ⇒ oless' a0 a1
   
   [oless_strongind]  Theorem
      
      ⊢ ∀oless'.
          (∀k1 k2. k1 < k2 ⇒ oless' (End k1) (End k2)) ∧
          (∀k1 e2 k2 t2. oless' (End k1) (Plus e2 k2 t2)) ∧
          (∀e1 k1 t1 e2 k2 t2.
             oless e1 e2 ∧ oless' e1 e2 ⇒
             oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
          (∀e1 k1 t1 e2 k2 t2.
             (e1 = e2) ∧ k1 < k2 ⇒ oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ∧
          (∀e1 k1 t1 e2 k2 t2.
             (e1 = e2) ∧ (k1 = k2) ∧ oless t1 t2 ∧ oless' t1 t2 ⇒
             oless' (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
          ∀a0 a1. oless a0 a1 ⇒ oless' a0 a1
   
   [oless_tail]  Theorem
      
      ⊢ ∀x. is_ord x ∧ ¬finp x ⇒ oless (tail x) x
   
   [ord_add_def]  Theorem
      
      ⊢ (∀n m. ord_add (End m) (End n) = End (m + n)) ∧
        (∀t p m k. ord_add (End m) (Plus p k t) = Plus p k t) ∧
        (∀t m k e.
           ord_add (Plus e k t) (End m) = Plus e k (ord_add t (End m))) ∧
        ∀t2 t1 k2 k1 e2 e1.
          ord_add (Plus e1 k1 t1) (Plus e2 k2 t2) =
          if oless e1 e2 then Plus e2 k2 t2
          else if e1 = e2 then Plus e2 (k1 + k2) t2
          else Plus e1 k1 (ord_add t1 (Plus e2 k2 t2))
   
   [ord_add_ind]  Theorem
      
      ⊢ ∀P. (∀m n. P (End m) (End n)) ∧
            (∀m p k t. P (End m) (Plus p k t)) ∧
            (∀e k t m. P t (End m) ⇒ P (Plus e k t) (End m)) ∧
            (∀e1 k1 t1 e2 k2 t2.
               (¬oless e1 e2 ∧ e1 ≠ e2 ⇒ P t1 (Plus e2 k2 t2)) ⇒
               P (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
            ∀v v1. P v v1
   
   [ord_mult_def]  Theorem
      
      ⊢ ∀y x.
          ord_mult x y =
          if (x = End 0) ∨ (y = End 0) then End 0
          else
            case (x,y) of
              (End m,End n) => End (m * n)
            | (End m,Plus e k t) =>
              Plus (ord_add (End 0) e) k (ord_mult (End m) t)
            | (Plus e' k' t',End n') => Plus e' (k' * n') t'
            | (Plus e' k' t',Plus e2 k2 t2) =>
              Plus (ord_add e' e2) k2 (ord_mult (Plus e' k' t') t2)
   
   [ord_mult_ind]  Theorem
      
      ⊢ ∀P. (∀x y.
               (∀v v1 m e k t.
                  ¬((x = End 0) ∨ (y = End 0)) ∧ ((x,y) = (v,v1)) ∧
                  (v = End m) ∧ (v1 = Plus e k t) ⇒
                  P (End m) t) ∧
               (∀v v1 e' k' t' e2 k2 t2.
                  ¬((x = End 0) ∨ (y = End 0)) ∧ ((x,y) = (v,v1)) ∧
                  (v = Plus e' k' t') ∧ (v1 = Plus e2 k2 t2) ⇒
                  P (Plus e' k' t') t2) ⇒
               P x y) ⇒
            ∀v v1. P v v1
   
   [ord_sub_def]  Theorem
      
      ⊢ (∀n m. ord_sub (End m) (End n) = End (m − n)) ∧
        (∀t p m k. ord_sub (End m) (Plus p k t) = End 0) ∧
        (∀t m k e. ord_sub (Plus e k t) (End m) = Plus e k t) ∧
        ∀t2 t1 k2 k1 e2 e1.
          ord_sub (Plus e1 k1 t1) (Plus e2 k2 t2) =
          if oless e1 e2 then End 0
          else if e1 = e2 then
            if k1 < k2 then End 0
            else if k1 > k2 then Plus e1 (k1 − k2) t1
            else ord_sub t1 t2
          else Plus e1 k1 t1
   
   [ord_sub_ind]  Theorem
      
      ⊢ ∀P. (∀m n. P (End m) (End n)) ∧
            (∀m p k t. P (End m) (Plus p k t)) ∧
            (∀e k t m. P (Plus e k t) (End m)) ∧
            (∀e1 k1 t1 e2 k2 t2.
               (¬oless e1 e2 ∧ (e1 = e2) ∧ ¬(k1 < k2) ∧ ¬(k1 > k2) ⇒
                P t1 t2) ⇒
               P (Plus e1 k1 t1) (Plus e2 k2 t2)) ⇒
            ∀v v1. P v v1
   
   [osyntax_11]  Theorem
      
      ⊢ (∀a a'. (End a = End a') ⇔ (a = a')) ∧
        ∀a0 a1 a2 a0' a1' a2'.
          (Plus a0 a1 a2 = Plus a0' a1' a2') ⇔
          (a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2')
   
   [osyntax_Axiom]  Theorem
      
      ⊢ ∀f0 f1. ∃fn.
          (∀a. fn (End a) = f0 a) ∧
          ∀a0 a1 a2. fn (Plus a0 a1 a2) = f1 a1 a0 a2 (fn a0) (fn a2)
   
   [osyntax_case_cong]  Theorem
      
      ⊢ ∀M M' f f1.
          (M = M') ∧ (∀a. (M' = End a) ⇒ (f a = f' a)) ∧
          (∀a0 a1 a2. (M' = Plus a0 a1 a2) ⇒ (f1 a0 a1 a2 = f1' a0 a1 a2)) ⇒
          (osyntax_CASE M f f1 = osyntax_CASE M' f' f1')
   
   [osyntax_case_eq]  Theorem
      
      ⊢ (osyntax_CASE x f f1 = v) ⇔
        (∃n. (x = End n) ∧ (f n = v)) ∨
        ∃o' n o0. (x = Plus o' n o0) ∧ (f1 o' n o0 = v)
   
   [osyntax_distinct]  Theorem
      
      ⊢ ∀a2 a1 a0 a. End a ≠ Plus a0 a1 a2
   
   [osyntax_induction]  Theorem
      
      ⊢ ∀P. (∀n. P (End n)) ∧ (∀ $o o0. P $o ∧ P o0 ⇒ ∀n. P (Plus $o n o0)) ⇒
            ∀ $o. P $o
   
   [osyntax_nchotomy]  Theorem
      
      ⊢ ∀oo. (∃n. oo = End n) ∨ ∃ $o n o0. oo = Plus $o n o0
   
   [padd_compute]  Theorem
      
      ⊢ (∀a b. padd a b 0 = ord_add a b) ∧
        (∀a b n.
           padd a b (NUMERAL (BIT1 n)) =
           Plus (expt a) (coeff a) (padd (tail a) b (NUMERAL (BIT1 n) − 1))) ∧
        ∀a b n.
          padd a b (NUMERAL (BIT2 n)) =
          Plus (expt a) (coeff a) (padd (tail a) b (NUMERAL (BIT1 n)))
   
   [pmult_def]  Theorem
      
      ⊢ ∀n b a.
          pmult a b n =
          if (a = End 0) ∨ (b = End 0) then End 0
          else
            case (a,b) of
              (End i,End j) => End (i * j)
            | (Plus e1 c1 k1,End j) => Plus e1 (c1 * j) k1
            | (v,Plus e2 c2 k2) =>
              (let
                 m = cf2 (expt a) e2 n
               in
                 Plus (padd (expt a) e2 m) c2 (pmult a k2 m))
   
   [pmult_ind]  Theorem
      
      ⊢ ∀P. (∀a b n.
               (∀v v1 e2 c2 k2 m.
                  ¬((a = End 0) ∨ (b = End 0)) ∧ ((a,b) = (v,v1)) ∧
                  (v1 = Plus e2 c2 k2) ∧ (m = cf2 (expt a) e2 n) ⇒
                  P a k2 m) ⇒
               P a b n) ⇒
            ∀v v1 v2. P v v1 v2
   
   [rank_0_End]  Theorem
      
      ⊢ ∀x. (rank x = 0) ⇔ ∃n. x = End n
   
   [rank_expt]  Theorem
      
      ⊢ ∀x n. is_ord x ∧ (rank x = SUC n) ⇒ (rank (expt x) = n)
   
   [rank_finp]  Theorem
      
      ⊢ ∀x. (rank x = 0) ⇔ finp x
   
   [rank_less_imp_oless]  Theorem
      
      ⊢ ∀x y. is_ord x ∧ is_ord y ∧ rank x < rank y ⇒ oless x y
   
   [rank_positive]  Theorem
      
      ⊢ ∀x. 0 < rank x ⇔ (x = Plus (expt x) (coeff x) (tail x))
   
   [rank_positive_exists]  Theorem
      
      ⊢ ∀x. 0 < rank x ⇔ ∃e c t. x = Plus e c t
   
   [rank_positive_expt]  Theorem
      
      ⊢ ∀x n. (rank x = SUC n) ⇒ (rank (expt x) = n)
   
   [restn_compute]  Theorem
      
      ⊢ (∀a. restn a 0 = a) ∧
        (∀a n.
           restn a (NUMERAL (BIT1 n)) =
           restn (tail a) (NUMERAL (BIT1 n) − 1)) ∧
        ∀a n.
          restn a (NUMERAL (BIT2 n)) = restn (tail a) (NUMERAL (BIT1 n))
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1