src/ZF/CardinalArith.thy
changeset 39159 0dec18004e75
parent 32960 69916a850301
child 45602 2a858377c3d2
     1.1 --- a/src/ZF/CardinalArith.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -911,89 +911,89 @@
     1.4  
     1.5  
     1.6  ML{*
     1.7 -val InfCard_def = thm "InfCard_def"
     1.8 -val cmult_def = thm "cmult_def"
     1.9 -val cadd_def = thm "cadd_def"
    1.10 -val jump_cardinal_def = thm "jump_cardinal_def"
    1.11 -val csucc_def = thm "csucc_def"
    1.12 +val InfCard_def = @{thm InfCard_def};
    1.13 +val cmult_def = @{thm cmult_def};
    1.14 +val cadd_def = @{thm cadd_def};
    1.15 +val jump_cardinal_def = @{thm jump_cardinal_def};
    1.16 +val csucc_def = @{thm csucc_def};
    1.17  
    1.18 -val sum_commute_eqpoll = thm "sum_commute_eqpoll";
    1.19 -val cadd_commute = thm "cadd_commute";
    1.20 -val sum_assoc_eqpoll = thm "sum_assoc_eqpoll";
    1.21 -val well_ord_cadd_assoc = thm "well_ord_cadd_assoc";
    1.22 -val sum_0_eqpoll = thm "sum_0_eqpoll";
    1.23 -val cadd_0 = thm "cadd_0";
    1.24 -val sum_lepoll_self = thm "sum_lepoll_self";
    1.25 -val cadd_le_self = thm "cadd_le_self";
    1.26 -val sum_lepoll_mono = thm "sum_lepoll_mono";
    1.27 -val cadd_le_mono = thm "cadd_le_mono";
    1.28 -val eq_imp_not_mem = thm "eq_imp_not_mem";
    1.29 -val sum_succ_eqpoll = thm "sum_succ_eqpoll";
    1.30 -val nat_cadd_eq_add = thm "nat_cadd_eq_add";
    1.31 -val prod_commute_eqpoll = thm "prod_commute_eqpoll";
    1.32 -val cmult_commute = thm "cmult_commute";
    1.33 -val prod_assoc_eqpoll = thm "prod_assoc_eqpoll";
    1.34 -val well_ord_cmult_assoc = thm "well_ord_cmult_assoc";
    1.35 -val sum_prod_distrib_eqpoll = thm "sum_prod_distrib_eqpoll";
    1.36 -val well_ord_cadd_cmult_distrib = thm "well_ord_cadd_cmult_distrib";
    1.37 -val prod_0_eqpoll = thm "prod_0_eqpoll";
    1.38 -val cmult_0 = thm "cmult_0";
    1.39 -val prod_singleton_eqpoll = thm "prod_singleton_eqpoll";
    1.40 -val cmult_1 = thm "cmult_1";
    1.41 -val prod_lepoll_self = thm "prod_lepoll_self";
    1.42 -val cmult_le_self = thm "cmult_le_self";
    1.43 -val prod_lepoll_mono = thm "prod_lepoll_mono";
    1.44 -val cmult_le_mono = thm "cmult_le_mono";
    1.45 -val prod_succ_eqpoll = thm "prod_succ_eqpoll";
    1.46 -val nat_cmult_eq_mult = thm "nat_cmult_eq_mult";
    1.47 -val cmult_2 = thm "cmult_2";
    1.48 -val sum_lepoll_prod = thm "sum_lepoll_prod";
    1.49 -val lepoll_imp_sum_lepoll_prod = thm "lepoll_imp_sum_lepoll_prod";
    1.50 -val nat_cons_lepoll = thm "nat_cons_lepoll";
    1.51 -val nat_cons_eqpoll = thm "nat_cons_eqpoll";
    1.52 -val nat_succ_eqpoll = thm "nat_succ_eqpoll";
    1.53 -val InfCard_nat = thm "InfCard_nat";
    1.54 -val InfCard_is_Card = thm "InfCard_is_Card";
    1.55 -val InfCard_Un = thm "InfCard_Un";
    1.56 -val InfCard_is_Limit = thm "InfCard_is_Limit";
    1.57 -val ordermap_eqpoll_pred = thm "ordermap_eqpoll_pred";
    1.58 -val ordermap_z_lt = thm "ordermap_z_lt";
    1.59 -val InfCard_le_cmult_eq = thm "InfCard_le_cmult_eq";
    1.60 -val InfCard_cmult_eq = thm "InfCard_cmult_eq";
    1.61 -val InfCard_cdouble_eq = thm "InfCard_cdouble_eq";
    1.62 -val InfCard_le_cadd_eq = thm "InfCard_le_cadd_eq";
    1.63 -val InfCard_cadd_eq = thm "InfCard_cadd_eq";
    1.64 -val Ord_jump_cardinal = thm "Ord_jump_cardinal";
    1.65 -val jump_cardinal_iff = thm "jump_cardinal_iff";
    1.66 -val K_lt_jump_cardinal = thm "K_lt_jump_cardinal";
    1.67 -val Card_jump_cardinal = thm "Card_jump_cardinal";
    1.68 -val csucc_basic = thm "csucc_basic";
    1.69 -val Card_csucc = thm "Card_csucc";
    1.70 -val lt_csucc = thm "lt_csucc";
    1.71 -val Ord_0_lt_csucc = thm "Ord_0_lt_csucc";
    1.72 -val csucc_le = thm "csucc_le";
    1.73 -val lt_csucc_iff = thm "lt_csucc_iff";
    1.74 -val Card_lt_csucc_iff = thm "Card_lt_csucc_iff";
    1.75 -val InfCard_csucc = thm "InfCard_csucc";
    1.76 -val Finite_into_Fin = thm "Finite_into_Fin";
    1.77 -val Fin_into_Finite = thm "Fin_into_Finite";
    1.78 -val Finite_Fin_iff = thm "Finite_Fin_iff";
    1.79 -val Finite_Un = thm "Finite_Un";
    1.80 -val Finite_Union = thm "Finite_Union";
    1.81 -val Finite_induct = thm "Finite_induct";
    1.82 -val Fin_imp_not_cons_lepoll = thm "Fin_imp_not_cons_lepoll";
    1.83 -val Finite_imp_cardinal_cons = thm "Finite_imp_cardinal_cons";
    1.84 -val Finite_imp_succ_cardinal_Diff = thm "Finite_imp_succ_cardinal_Diff";
    1.85 -val Finite_imp_cardinal_Diff = thm "Finite_imp_cardinal_Diff";
    1.86 -val nat_implies_well_ord = thm "nat_implies_well_ord";
    1.87 -val nat_sum_eqpoll_sum = thm "nat_sum_eqpoll_sum";
    1.88 -val Diff_sing_Finite = thm "Diff_sing_Finite";
    1.89 -val Diff_Finite = thm "Diff_Finite";
    1.90 -val Ord_subset_natD = thm "Ord_subset_natD";
    1.91 -val Ord_nat_subset_into_Card = thm "Ord_nat_subset_into_Card";
    1.92 -val Finite_cardinal_in_nat = thm "Finite_cardinal_in_nat";
    1.93 -val Finite_Diff_sing_eq_diff_1 = thm "Finite_Diff_sing_eq_diff_1";
    1.94 -val cardinal_lt_imp_Diff_not_0 = thm "cardinal_lt_imp_Diff_not_0";
    1.95 +val sum_commute_eqpoll = @{thm sum_commute_eqpoll};
    1.96 +val cadd_commute = @{thm cadd_commute};
    1.97 +val sum_assoc_eqpoll = @{thm sum_assoc_eqpoll};
    1.98 +val well_ord_cadd_assoc = @{thm well_ord_cadd_assoc};
    1.99 +val sum_0_eqpoll = @{thm sum_0_eqpoll};
   1.100 +val cadd_0 = @{thm cadd_0};
   1.101 +val sum_lepoll_self = @{thm sum_lepoll_self};
   1.102 +val cadd_le_self = @{thm cadd_le_self};
   1.103 +val sum_lepoll_mono = @{thm sum_lepoll_mono};
   1.104 +val cadd_le_mono = @{thm cadd_le_mono};
   1.105 +val eq_imp_not_mem = @{thm eq_imp_not_mem};
   1.106 +val sum_succ_eqpoll = @{thm sum_succ_eqpoll};
   1.107 +val nat_cadd_eq_add = @{thm nat_cadd_eq_add};
   1.108 +val prod_commute_eqpoll = @{thm prod_commute_eqpoll};
   1.109 +val cmult_commute = @{thm cmult_commute};
   1.110 +val prod_assoc_eqpoll = @{thm prod_assoc_eqpoll};
   1.111 +val well_ord_cmult_assoc = @{thm well_ord_cmult_assoc};
   1.112 +val sum_prod_distrib_eqpoll = @{thm sum_prod_distrib_eqpoll};
   1.113 +val well_ord_cadd_cmult_distrib = @{thm well_ord_cadd_cmult_distrib};
   1.114 +val prod_0_eqpoll = @{thm prod_0_eqpoll};
   1.115 +val cmult_0 = @{thm cmult_0};
   1.116 +val prod_singleton_eqpoll = @{thm prod_singleton_eqpoll};
   1.117 +val cmult_1 = @{thm cmult_1};
   1.118 +val prod_lepoll_self = @{thm prod_lepoll_self};
   1.119 +val cmult_le_self = @{thm cmult_le_self};
   1.120 +val prod_lepoll_mono = @{thm prod_lepoll_mono};
   1.121 +val cmult_le_mono = @{thm cmult_le_mono};
   1.122 +val prod_succ_eqpoll = @{thm prod_succ_eqpoll};
   1.123 +val nat_cmult_eq_mult = @{thm nat_cmult_eq_mult};
   1.124 +val cmult_2 = @{thm cmult_2};
   1.125 +val sum_lepoll_prod = @{thm sum_lepoll_prod};
   1.126 +val lepoll_imp_sum_lepoll_prod = @{thm lepoll_imp_sum_lepoll_prod};
   1.127 +val nat_cons_lepoll = @{thm nat_cons_lepoll};
   1.128 +val nat_cons_eqpoll = @{thm nat_cons_eqpoll};
   1.129 +val nat_succ_eqpoll = @{thm nat_succ_eqpoll};
   1.130 +val InfCard_nat = @{thm InfCard_nat};
   1.131 +val InfCard_is_Card = @{thm InfCard_is_Card};
   1.132 +val InfCard_Un = @{thm InfCard_Un};
   1.133 +val InfCard_is_Limit = @{thm InfCard_is_Limit};
   1.134 +val ordermap_eqpoll_pred = @{thm ordermap_eqpoll_pred};
   1.135 +val ordermap_z_lt = @{thm ordermap_z_lt};
   1.136 +val InfCard_le_cmult_eq = @{thm InfCard_le_cmult_eq};
   1.137 +val InfCard_cmult_eq = @{thm InfCard_cmult_eq};
   1.138 +val InfCard_cdouble_eq = @{thm InfCard_cdouble_eq};
   1.139 +val InfCard_le_cadd_eq = @{thm InfCard_le_cadd_eq};
   1.140 +val InfCard_cadd_eq = @{thm InfCard_cadd_eq};
   1.141 +val Ord_jump_cardinal = @{thm Ord_jump_cardinal};
   1.142 +val jump_cardinal_iff = @{thm jump_cardinal_iff};
   1.143 +val K_lt_jump_cardinal = @{thm K_lt_jump_cardinal};
   1.144 +val Card_jump_cardinal = @{thm Card_jump_cardinal};
   1.145 +val csucc_basic = @{thm csucc_basic};
   1.146 +val Card_csucc = @{thm Card_csucc};
   1.147 +val lt_csucc = @{thm lt_csucc};
   1.148 +val Ord_0_lt_csucc = @{thm Ord_0_lt_csucc};
   1.149 +val csucc_le = @{thm csucc_le};
   1.150 +val lt_csucc_iff = @{thm lt_csucc_iff};
   1.151 +val Card_lt_csucc_iff = @{thm Card_lt_csucc_iff};
   1.152 +val InfCard_csucc = @{thm InfCard_csucc};
   1.153 +val Finite_into_Fin = @{thm Finite_into_Fin};
   1.154 +val Fin_into_Finite = @{thm Fin_into_Finite};
   1.155 +val Finite_Fin_iff = @{thm Finite_Fin_iff};
   1.156 +val Finite_Un = @{thm Finite_Un};
   1.157 +val Finite_Union = @{thm Finite_Union};
   1.158 +val Finite_induct = @{thm Finite_induct};
   1.159 +val Fin_imp_not_cons_lepoll = @{thm Fin_imp_not_cons_lepoll};
   1.160 +val Finite_imp_cardinal_cons = @{thm Finite_imp_cardinal_cons};
   1.161 +val Finite_imp_succ_cardinal_Diff = @{thm Finite_imp_succ_cardinal_Diff};
   1.162 +val Finite_imp_cardinal_Diff = @{thm Finite_imp_cardinal_Diff};
   1.163 +val nat_implies_well_ord = @{thm nat_implies_well_ord};
   1.164 +val nat_sum_eqpoll_sum = @{thm nat_sum_eqpoll_sum};
   1.165 +val Diff_sing_Finite = @{thm Diff_sing_Finite};
   1.166 +val Diff_Finite = @{thm Diff_Finite};
   1.167 +val Ord_subset_natD = @{thm Ord_subset_natD};
   1.168 +val Ord_nat_subset_into_Card = @{thm Ord_nat_subset_into_Card};
   1.169 +val Finite_cardinal_in_nat = @{thm Finite_cardinal_in_nat};
   1.170 +val Finite_Diff_sing_eq_diff_1 = @{thm Finite_Diff_sing_eq_diff_1};
   1.171 +val cardinal_lt_imp_Diff_not_0 = @{thm cardinal_lt_imp_Diff_not_0};
   1.172  *}
   1.173  
   1.174  end