src/HOL/Nat.ML
author paulson
Wed Dec 15 17:32:40 2004 +0100 (2004-12-15)
changeset 15413 901d1bfedf09
parent 15341 254f6f00b60e
child 15921 b6e345548913
permissions -rw-r--r--
removal of archaic Abs/Rep proofs
     1 (*  Title:      HOL/Nat.ML
     2     ID:         $Id$
     3 *)
     4 
     5 (** legacy ML bindings **)
     6 
     7 structure nat =
     8 struct
     9   val distinct = thms "nat.distinct";
    10   val inject = thms "nat.inject";
    11   val exhaust = thm "nat.exhaust";
    12   val cases = thms "nat.cases";
    13   val split = thm "nat.split";
    14   val split_asm = thm "nat.split_asm";
    15   val induct = thm "nat.induct";
    16   val recs = thms "nat.recs";
    17   val simps = thms "nat.simps";
    18 end;
    19 
    20 val [nat_rec_0, nat_rec_Suc] = thms "nat.recs";
    21 bind_thm ("nat_rec_0", nat_rec_0);
    22 bind_thm ("nat_rec_Suc", nat_rec_Suc);
    23 
    24 val [nat_case_0, nat_case_Suc] = thms "nat.cases";
    25 bind_thm ("nat_case_0", nat_case_0);
    26 bind_thm ("nat_case_Suc", nat_case_Suc);
    27 
    28 val Least_Suc = thm "Least_Suc";
    29 val Least_Suc2 = thm "Least_Suc2";
    30 val One_nat_def = thm "One_nat_def";
    31 val Suc_Suc_eq = thm "Suc_Suc_eq";
    32 val Suc_def = thm "Suc_def";
    33 val Suc_diff_diff = thm "Suc_diff_diff";
    34 val Suc_diff_le = thm "Suc_diff_le";
    35 val Suc_inject = thm "Suc_inject";
    36 val Suc_leD = thm "Suc_leD";
    37 val Suc_leI = thm "Suc_leI";
    38 val Suc_le_D = thm "Suc_le_D";
    39 val Suc_le_eq = thm "Suc_le_eq";
    40 val Suc_le_lessD = thm "Suc_le_lessD";
    41 val Suc_le_mono = thm "Suc_le_mono";
    42 val Suc_lessD = thm "Suc_lessD";
    43 val Suc_lessE = thm "Suc_lessE";
    44 val Suc_lessI = thm "Suc_lessI";
    45 val Suc_less_SucD = thm "Suc_less_SucD";
    46 val Suc_less_eq = thm "Suc_less_eq";
    47 val Suc_mono = thm "Suc_mono";
    48 val Suc_mult_cancel1 = thm "Suc_mult_cancel1";
    49 val Suc_mult_le_cancel1 = thm "Suc_mult_le_cancel1";
    50 val Suc_mult_less_cancel1 = thm "Suc_mult_less_cancel1";
    51 val Suc_n_not_le_n = thm "Suc_n_not_le_n";
    52 val Suc_n_not_n = thm "Suc_n_not_n";
    53 val Suc_neq_Zero = thm "Suc_neq_Zero";
    54 val Suc_not_Zero = thm "Suc_not_Zero";
    55 val Suc_pred = thm "Suc_pred";
    56 val Zero_nat_def = thm "Zero_nat_def";
    57 val Zero_neq_Suc = thm "Zero_neq_Suc";
    58 val Zero_not_Suc = thm "Zero_not_Suc";
    59 val add_0 = thm "add_0";
    60 val add_0_right = thm "add_0_right";
    61 val add_Suc = thm "add_Suc";
    62 val add_Suc_right = thm "add_Suc_right";
    63 val add_ac = thms "add_ac";
    64 val add_assoc = thm "add_assoc";
    65 val add_commute = thm "add_commute";
    66 val add_diff_inverse = thm "add_diff_inverse";
    67 val add_eq_self_zero = thm "add_eq_self_zero";
    68 val add_gr_0 = thm "add_gr_0";
    69 val add_is_0 = thm "add_is_0";
    70 val add_is_1 = thm "add_is_1";
    71 val add_leD1 = thm "add_leD1";
    72 val add_leD2 = thm "add_leD2";
    73 val add_leE = thm "add_leE";
    74 val add_le_mono = thm "add_le_mono";
    75 val add_le_mono1 = thm "add_le_mono1";
    76 val nat_add_left_cancel = thm "nat_add_left_cancel";
    77 val nat_add_left_cancel_le = thm "nat_add_left_cancel_le";
    78 val nat_add_left_cancel_less = thm "nat_add_left_cancel_less";
    79 val add_left_commute = thm "add_left_commute";
    80 val add_lessD1 = thm "add_lessD1";
    81 val add_less_mono = thm "add_less_mono";
    82 val add_less_mono1 = thm "add_less_mono1";
    83 val add_mult_distrib = thm "add_mult_distrib";
    84 val add_mult_distrib2 = thm "add_mult_distrib2";
    85 val nat_add_right_cancel = thm "nat_add_right_cancel";
    86 val def_nat_rec_0 = thm "def_nat_rec_0";
    87 val def_nat_rec_Suc = thm "def_nat_rec_Suc";
    88 val diff_0 = thm "diff_0";
    89 val diff_0_eq_0 = thm "diff_0_eq_0";
    90 val diff_Suc = thm "diff_Suc";
    91 val diff_Suc_Suc = thm "diff_Suc_Suc";
    92 val diff_Suc_less = thm "diff_Suc_less";
    93 val diff_add_0 = thm "diff_add_0";
    94 val diff_add_assoc = thm "diff_add_assoc";
    95 val diff_add_assoc2 = thm "diff_add_assoc2";
    96 val diff_add_inverse = thm "diff_add_inverse";
    97 val diff_add_inverse2 = thm "diff_add_inverse2";
    98 val diff_cancel = thm "diff_cancel";
    99 val diff_cancel2 = thm "diff_cancel2";
   100 val diff_commute = thm "diff_commute";
   101 val diff_diff_left = thm "diff_diff_left";
   102 val diff_induct = thm "diff_induct";
   103 val diff_is_0_eq = thm "diff_is_0_eq";
   104 val diff_le_self = thm "diff_le_self";
   105 val diff_less_Suc = thm "diff_less_Suc";
   106 val diff_mult_distrib = thm "diff_mult_distrib"; 
   107 val diff_mult_distrib2 = thm "diff_mult_distrib2"; 
   108 val diff_self_eq_0 = thm "diff_self_eq_0";
   109 val eq_imp_le = thm "eq_imp_le";
   110 val gr0I = thm "gr0I";
   111 val gr0_conv_Suc = thm "gr0_conv_Suc";
   112 val gr_implies_not0 = thm "gr_implies_not0";
   113 val inj_Suc = thm "inj_Suc";
   114 val le0 = thm "le0";
   115 val leD = thm "leD";
   116 val leE = thm "leE";
   117 val leI = thm "leI";
   118 val le_0_eq = thm "le_0_eq";
   119 val le_SucE = thm "le_SucE";
   120 val le_SucI = thm "le_SucI";
   121 val le_Suc_eq = thm "le_Suc_eq";
   122 val le_add1 = thm "le_add1";
   123 val le_add2 = thm "le_add2";
   124 val le_add_diff_inverse = thm "le_add_diff_inverse";
   125 val le_add_diff_inverse2 = thm "le_add_diff_inverse2";
   126 val le_anti_sym = thm "le_anti_sym";
   127 val le_def = thm "le_def";
   128 val le_eq_less_or_eq = thm "le_eq_less_or_eq";
   129 val le_imp_diff_is_add = thm "le_imp_diff_is_add";
   130 val le_imp_less_Suc = thm "le_imp_less_Suc";
   131 val le_imp_less_or_eq = thm "le_imp_less_or_eq";
   132 val le_less_trans = thm "le_less_trans";
   133 val le_neq_implies_less = thm "le_neq_implies_less";
   134 val le_refl = thm "le_refl";
   135 val le_simps = thms "le_simps";
   136 val le_trans = thm "le_trans";
   137 val lessE = thm "lessE";
   138 val lessI = thm "lessI";
   139 val less_Suc0 = thm "less_Suc0";
   140 val less_SucE = thm "less_SucE";
   141 val less_SucI = thm "less_SucI";
   142 val less_Suc_eq = thm "less_Suc_eq";
   143 val less_Suc_eq_0_disj = thm "less_Suc_eq_0_disj";
   144 val less_Suc_eq_le = thm "less_Suc_eq_le";
   145 val less_add_Suc1 = thm "less_add_Suc1";
   146 val less_add_Suc2 = thm "less_add_Suc2";
   147 val less_add_eq_less = thm "less_add_eq_less";
   148 val less_asym = thm "less_asym";
   149 val less_def = thm "less_def";
   150 val less_eq = thm "less_eq";
   151 val less_iff_Suc_add = thm "less_iff_Suc_add";
   152 val less_imp_Suc_add = thm "less_imp_Suc_add";
   153 val less_imp_add_positive = thm "less_imp_add_positive";
   154 val less_imp_diff_less = thm "less_imp_diff_less";
   155 val less_imp_le = thm "less_imp_le";
   156 val less_irrefl = thm "less_irrefl";
   157 val less_le_trans = thm "less_le_trans";
   158 val less_linear = thm "less_linear";
   159 val less_mono_imp_le_mono = thm "less_mono_imp_le_mono";
   160 val less_not_refl = thm "less_not_refl";
   161 val less_not_refl2 = thm "less_not_refl2";
   162 val less_not_refl3 = thm "less_not_refl3";
   163 val less_not_sym = thm "less_not_sym";
   164 val less_one = thm "less_one";
   165 val less_or_eq_imp_le = thm "less_or_eq_imp_le";
   166 val less_trans = thm "less_trans";
   167 val less_trans_Suc = thm "less_trans_Suc";
   168 val less_zeroE = thm "less_zeroE";
   169 val max_0L = thm "max_0L";
   170 val max_0R = thm "max_0R";
   171 val max_Suc_Suc = thm "max_Suc_Suc";
   172 val min_0L = thm "min_0L";
   173 val min_0R = thm "min_0R";
   174 val min_Suc_Suc = thm "min_Suc_Suc";
   175 val mult_0 = thm "mult_0";
   176 val mult_0_right = thm "mult_0_right";
   177 val mult_1 = thm "mult_1";
   178 val mult_1_right = thm "mult_1_right";
   179 val mult_Suc = thm "mult_Suc";
   180 val mult_Suc_right = thm "mult_Suc_right";
   181 val mult_ac = thms "mult_ac";
   182 val mult_assoc = thm "mult_assoc";
   183 val mult_cancel1 = thm "mult_cancel1";
   184 val mult_cancel2 = thm "mult_cancel2";
   185 val mult_commute = thm "mult_commute";
   186 val mult_eq_1_iff = thm "mult_eq_1_iff";
   187 val mult_eq_self_implies_10 = thm "mult_eq_self_implies_10";
   188 val mult_is_0 = thm "mult_is_0";
   189 val mult_le_cancel1 = thm "mult_le_cancel1";
   190 val mult_le_cancel2 = thm "mult_le_cancel2";
   191 val mult_le_mono = thm "mult_le_mono";
   192 val mult_le_mono1 = thm "mult_le_mono1";
   193 val mult_le_mono2 = thm "mult_le_mono2";
   194 val mult_left_commute = thm "mult_left_commute";
   195 val mult_less_cancel1 = thm "mult_less_cancel1";
   196 val mult_less_cancel2 = thm "mult_less_cancel2";
   197 val mult_less_mono1 = thm "mult_less_mono1";
   198 val mult_less_mono2 = thm "mult_less_mono2";
   199 val n_not_Suc_n = thm "n_not_Suc_n";
   200 val nat_distrib = thms "nat_distrib";
   201 val nat_induct = thm "nat_induct";
   202 val nat_induct2 = thm "nat_induct2";
   203 val nat_le_linear = thm "nat_le_linear";
   204 val nat_less_cases = thm "nat_less_cases";
   205 val nat_less_induct = thm "nat_less_induct";
   206 val nat_less_le = thm "nat_less_le";
   207 val nat_neq_iff = thm "nat_neq_iff";
   208 val nat_not_singleton = thm "nat_not_singleton";
   209 val neq0_conv = thm "neq0_conv";
   210 val not0_implies_Suc = thm "not0_implies_Suc";
   211 val not_add_less1 = thm "not_add_less1";
   212 val not_add_less2 = thm "not_add_less2";
   213 val not_gr0 = thm "not_gr0";
   214 val not_leE = thm "not_leE";
   215 val not_le_iff_less = thm "not_le_iff_less";
   216 val not_less0 = thm "not_less0";
   217 val not_less_eq = thm "not_less_eq";
   218 val not_less_iff_le = thm "not_less_iff_le";
   219 val not_less_less_Suc_eq = thm "not_less_less_Suc_eq";
   220 val not_less_simps = thms "not_less_simps";
   221 val one_eq_mult_iff = thm "one_eq_mult_iff";
   222 val one_is_add = thm "one_is_add";
   223 val one_le_mult_iff = thm "one_le_mult_iff";
   224 val one_reorient = thm "one_reorient";
   225 val powerI = thm "powerI";
   226 val pred_nat_def = thm "pred_nat_def";
   227 val trans_le_add1 = thm "trans_le_add1";
   228 val trans_le_add2 = thm "trans_le_add2";
   229 val trans_less_add1 = thm "trans_less_add1";
   230 val trans_less_add2 = thm "trans_less_add2";
   231 val wf_less = thm "wf_less";
   232 val wf_pred_nat = thm "wf_pred_nat";
   233 val zero_induct = thm "zero_induct";
   234 val zero_induct_lemma = thm "zero_induct_lemma";
   235 val zero_less_Suc = thm "zero_less_Suc";
   236 val zero_less_diff = thm "zero_less_diff";
   237 val zero_less_mult_iff = thm "zero_less_mult_iff";
   238 val zero_reorient = thm "zero_reorient";