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