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
```