src/ZF/Ordinal.thy
changeset 24893 b8ef7afe3a6b
parent 22808 a7daa74e2980
child 35762 af3ff2ba4c54
     1.1 --- a/src/ZF/Ordinal.thy	Sun Oct 07 15:49:25 2007 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Sun Oct 07 21:19:31 2007 +0200
     1.3 @@ -9,21 +9,24 @@
     1.4  
     1.5  theory Ordinal imports WF Bool equalities begin
     1.6  
     1.7 -constdefs
     1.8 -
     1.9 -  Memrel        :: "i=>i"
    1.10 +definition
    1.11 +  Memrel        :: "i=>i"  where
    1.12      "Memrel(A)   == {z: A*A . EX x y. z=<x,y> & x:y }"
    1.13  
    1.14 -  Transset  :: "i=>o"
    1.15 +definition
    1.16 +  Transset  :: "i=>o"  where
    1.17      "Transset(i) == ALL x:i. x<=i"
    1.18  
    1.19 -  Ord  :: "i=>o"
    1.20 +definition
    1.21 +  Ord  :: "i=>o"  where
    1.22      "Ord(i)      == Transset(i) & (ALL x:i. Transset(x))"
    1.23  
    1.24 -  lt        :: "[i,i] => o"  (infixl "<" 50)   (*less-than on ordinals*)
    1.25 +definition
    1.26 +  lt        :: "[i,i] => o"  (infixl "<" 50)   (*less-than on ordinals*)  where
    1.27      "i<j         == i:j & Ord(j)"
    1.28  
    1.29 -  Limit         :: "i=>o"
    1.30 +definition
    1.31 +  Limit         :: "i=>o"  where
    1.32      "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
    1.33  
    1.34  abbreviation
    1.35 @@ -736,134 +739,4 @@
    1.36  apply (blast intro!: equalityI)
    1.37  done
    1.38  
    1.39 -ML 
    1.40 -{*
    1.41 -val Memrel_def = thm "Memrel_def";
    1.42 -val Transset_def = thm "Transset_def";
    1.43 -val Ord_def = thm "Ord_def";
    1.44 -val lt_def = thm "lt_def";
    1.45 -val Limit_def = thm "Limit_def";
    1.46 -
    1.47 -val Transset_iff_Pow = thm "Transset_iff_Pow";
    1.48 -val Transset_iff_Union_succ = thm "Transset_iff_Union_succ";
    1.49 -val Transset_iff_Union_subset = thm "Transset_iff_Union_subset";
    1.50 -val Transset_doubleton_D = thm "Transset_doubleton_D";
    1.51 -val Transset_Pair_D = thm "Transset_Pair_D";
    1.52 -val Transset_includes_domain = thm "Transset_includes_domain";
    1.53 -val Transset_includes_range = thm "Transset_includes_range";
    1.54 -val Transset_0 = thm "Transset_0";
    1.55 -val Transset_Un = thm "Transset_Un";
    1.56 -val Transset_Int = thm "Transset_Int";
    1.57 -val Transset_succ = thm "Transset_succ";
    1.58 -val Transset_Pow = thm "Transset_Pow";
    1.59 -val Transset_Union = thm "Transset_Union";
    1.60 -val Transset_Union_family = thm "Transset_Union_family";
    1.61 -val Transset_Inter_family = thm "Transset_Inter_family";
    1.62 -val OrdI = thm "OrdI";
    1.63 -val Ord_is_Transset = thm "Ord_is_Transset";
    1.64 -val Ord_contains_Transset = thm "Ord_contains_Transset";
    1.65 -val Ord_in_Ord = thm "Ord_in_Ord";
    1.66 -val Ord_succD = thm "Ord_succD";
    1.67 -val Ord_subset_Ord = thm "Ord_subset_Ord";
    1.68 -val OrdmemD = thm "OrdmemD";
    1.69 -val Ord_trans = thm "Ord_trans";
    1.70 -val Ord_succ_subsetI = thm "Ord_succ_subsetI";
    1.71 -val Ord_0 = thm "Ord_0";
    1.72 -val Ord_succ = thm "Ord_succ";
    1.73 -val Ord_1 = thm "Ord_1";
    1.74 -val Ord_succ_iff = thm "Ord_succ_iff";
    1.75 -val Ord_Un = thm "Ord_Un";
    1.76 -val Ord_Int = thm "Ord_Int";
    1.77 -val Ord_Inter = thm "Ord_Inter";
    1.78 -val Ord_INT = thm "Ord_INT";
    1.79 -val ON_class = thm "ON_class";
    1.80 -val ltI = thm "ltI";
    1.81 -val ltE = thm "ltE";
    1.82 -val ltD = thm "ltD";
    1.83 -val not_lt0 = thm "not_lt0";
    1.84 -val lt_Ord = thm "lt_Ord";
    1.85 -val lt_Ord2 = thm "lt_Ord2";
    1.86 -val le_Ord2 = thm "le_Ord2";
    1.87 -val lt0E = thm "lt0E";
    1.88 -val lt_trans = thm "lt_trans";
    1.89 -val lt_not_sym = thm "lt_not_sym";
    1.90 -val lt_asym = thm "lt_asym";
    1.91 -val lt_irrefl = thm "lt_irrefl";
    1.92 -val lt_not_refl = thm "lt_not_refl";
    1.93 -val le_iff = thm "le_iff";
    1.94 -val leI = thm "leI";
    1.95 -val le_eqI = thm "le_eqI";
    1.96 -val le_refl = thm "le_refl";
    1.97 -val le_refl_iff = thm "le_refl_iff";
    1.98 -val leCI = thm "leCI";
    1.99 -val leE = thm "leE";
   1.100 -val le_anti_sym = thm "le_anti_sym";
   1.101 -val le0_iff = thm "le0_iff";
   1.102 -val le0D = thm "le0D";
   1.103 -val Memrel_iff = thm "Memrel_iff";
   1.104 -val MemrelI = thm "MemrelI";
   1.105 -val MemrelE = thm "MemrelE";
   1.106 -val Memrel_type = thm "Memrel_type";
   1.107 -val Memrel_mono = thm "Memrel_mono";
   1.108 -val Memrel_0 = thm "Memrel_0";
   1.109 -val Memrel_1 = thm "Memrel_1";
   1.110 -val wf_Memrel = thm "wf_Memrel";
   1.111 -val trans_Memrel = thm "trans_Memrel";
   1.112 -val Transset_Memrel_iff = thm "Transset_Memrel_iff";
   1.113 -val Transset_induct = thm "Transset_induct";
   1.114 -val Ord_induct = thm "Ord_induct";
   1.115 -val trans_induct = thm "trans_induct";
   1.116 -val Ord_linear = thm "Ord_linear";
   1.117 -val Ord_linear_lt = thm "Ord_linear_lt";
   1.118 -val Ord_linear2 = thm "Ord_linear2";
   1.119 -val Ord_linear_le = thm "Ord_linear_le";
   1.120 -val le_imp_not_lt = thm "le_imp_not_lt";
   1.121 -val not_lt_imp_le = thm "not_lt_imp_le";
   1.122 -val Ord_mem_iff_lt = thm "Ord_mem_iff_lt";
   1.123 -val not_lt_iff_le = thm "not_lt_iff_le";
   1.124 -val not_le_iff_lt = thm "not_le_iff_lt";
   1.125 -val Ord_0_le = thm "Ord_0_le";
   1.126 -val Ord_0_lt = thm "Ord_0_lt";
   1.127 -val Ord_0_lt_iff = thm "Ord_0_lt_iff";
   1.128 -val zero_le_succ_iff = thm "zero_le_succ_iff";
   1.129 -val subset_imp_le = thm "subset_imp_le";
   1.130 -val le_imp_subset = thm "le_imp_subset";
   1.131 -val le_subset_iff = thm "le_subset_iff";
   1.132 -val le_succ_iff = thm "le_succ_iff";
   1.133 -val all_lt_imp_le = thm "all_lt_imp_le";
   1.134 -val lt_trans1 = thm "lt_trans1";
   1.135 -val lt_trans2 = thm "lt_trans2";
   1.136 -val le_trans = thm "le_trans";
   1.137 -val succ_leI = thm "succ_leI";
   1.138 -val succ_leE = thm "succ_leE";
   1.139 -val succ_le_iff = thm "succ_le_iff";
   1.140 -val succ_le_imp_le = thm "succ_le_imp_le";
   1.141 -val lt_subset_trans = thm "lt_subset_trans";
   1.142 -val Un_upper1_le = thm "Un_upper1_le";
   1.143 -val Un_upper2_le = thm "Un_upper2_le";
   1.144 -val Un_least_lt = thm "Un_least_lt";
   1.145 -val Un_least_lt_iff = thm "Un_least_lt_iff";
   1.146 -val Un_least_mem_iff = thm "Un_least_mem_iff";
   1.147 -val Int_greatest_lt = thm "Int_greatest_lt";
   1.148 -val Ord_Union = thm "Ord_Union";
   1.149 -val Ord_UN = thm "Ord_UN";
   1.150 -val UN_least_le = thm "UN_least_le";
   1.151 -val UN_succ_least_lt = thm "UN_succ_least_lt";
   1.152 -val UN_upper_le = thm "UN_upper_le";
   1.153 -val le_implies_UN_le_UN = thm "le_implies_UN_le_UN";
   1.154 -val Ord_equality = thm "Ord_equality";
   1.155 -val Ord_Union_subset = thm "Ord_Union_subset";
   1.156 -val Limit_Union_eq = thm "Limit_Union_eq";
   1.157 -val Limit_is_Ord = thm "Limit_is_Ord";
   1.158 -val Limit_has_0 = thm "Limit_has_0";
   1.159 -val Limit_has_succ = thm "Limit_has_succ";
   1.160 -val non_succ_LimitI = thm "non_succ_LimitI";
   1.161 -val succ_LimitE = thm "succ_LimitE";
   1.162 -val not_succ_Limit = thm "not_succ_Limit";
   1.163 -val Limit_le_succD = thm "Limit_le_succD";
   1.164 -val Ord_cases_disj = thm "Ord_cases_disj";
   1.165 -val Ord_cases = thm "Ord_cases";
   1.166 -val trans_induct3 = thm "trans_induct3";
   1.167 -*}
   1.168 -
   1.169  end