removed theory NatArith (now part of Nat);
authorwenzelm
Wed Nov 08 13:48:29 2006 +0100 (2006-11-08)
changeset 21243afffe1f72143
parent 21242 d73735bb33c1
child 21244 0e9d222db727
removed theory NatArith (now part of Nat);
doc-src/TutorialI/Types/numerics.tex
src/HOL/Datatype.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Integ/IntDef.thy
src/HOL/Integ/int_arith1.ML
src/HOL/Nat.thy
src/HOL/NatArith.thy
src/HOL/Real/rat_arith.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/res_atp.ML
src/HOL/arith_data.ML
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Wed Nov 08 11:23:09 2006 +0100
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Wed Nov 08 13:48:29 2006 +0100
     1.3 @@ -48,7 +48,10 @@
     1.4  \index{numeric literals|(}%
     1.5  The constants \cdx{0} and \cdx{1} are overloaded.  They denote zero and one,
     1.6  respectively, for all numeric types.  Other values are expressed by numeric
     1.7 -literals, which consist of one or more decimal digits optionally preceeded by a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and
\isa{441223334678}.  Literals are available for the types of natural
numbers, integers, rationals, reals, etc.; they denote integer values of
arbitrary size.
     1.8 +literals, which consist of one or more decimal digits optionally preceeded by a minus sign (\isa{-}).  Examples are \isa{2}, \isa{-3} and
     1.9 +\isa{441223334678}.  Literals are available for the types of natural
    1.10 +numbers, integers, rationals, reals, etc.; they denote integer values of
    1.11 +arbitrary size.
    1.12  
    1.13  Literals look like constants, but they abbreviate 
    1.14  terms representing the number in a two's complement binary notation. 
    1.15 @@ -102,7 +105,7 @@
    1.16  \index{natural numbers|(}\index{*nat (type)|(}%
    1.17  This type requires no introduction: we have been using it from the
    1.18  beginning.  Hundreds of theorems about the natural numbers are
    1.19 -proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.  
    1.20 +proved in the theories \isa{Nat} and \isa{Divides}.  
    1.21  Basic properties of addition and multiplication are available through the
    1.22  axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}).
    1.23  
    1.24 @@ -234,7 +237,12 @@
    1.25  
    1.26  \index{integers|(}\index{*int (type)|(}%
    1.27  Reasoning methods for the integers resemble those for the natural numbers, 
    1.28 -but induction and
the constant \isa{Suc} are not available.  HOL provides many lemmas for
proving inequalities involving integer multiplication and division, similar
to those shown above for type~\isa{nat}. The laws of addition, subtraction
and multiplication are available through the axiomatic type class for rings
(\S\ref{sec:numeric-axclasses}).
    1.29 +but induction and
    1.30 +the constant \isa{Suc} are not available.  HOL provides many lemmas for
    1.31 +proving inequalities involving integer multiplication and division, similar
    1.32 +to those shown above for type~\isa{nat}. The laws of addition, subtraction
    1.33 +and multiplication are available through the axiomatic type class for rings
    1.34 +(\S\ref{sec:numeric-axclasses}).
    1.35  
    1.36  The \rmindex{absolute value} function \cdx{abs} is overloaded, and is 
    1.37  defined for all types that involve negative numbers, including the integers.
    1.38 @@ -324,8 +332,13 @@
    1.39  \rulename{dense}
    1.40  \end{isabelle}
    1.41  
    1.42 -The real numbers are, moreover, \textbf{complete}: every set of reals that
is bounded above has a least upper bound.  Completeness distinguishes the
reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
upper bound.  (It could only be $\surd2$, which is irrational. The
formalization of completeness, which is complicated, 
    1.43 -can be found in theory \texttt{RComplete} of directory
\texttt{Real}.
    1.44 +The real numbers are, moreover, \textbf{complete}: every set of reals that
    1.45 +is bounded above has a least upper bound.  Completeness distinguishes the
    1.46 +reals from the rationals, for which the set $\{x\mid x^2<2\}$ has no least
    1.47 +upper bound.  (It could only be $\surd2$, which is irrational. The
    1.48 +formalization of completeness, which is complicated, 
    1.49 +can be found in theory \texttt{RComplete} of directory
    1.50 +\texttt{Real}.
    1.51  
    1.52  Numeric literals\index{numeric literals!for type \protect\isa{real}}
    1.53  for type \isa{real} have the same syntax as those for type
    1.54 @@ -375,18 +388,36 @@
    1.55  the following type classes:
    1.56  \begin{itemize}
    1.57  \item 
    1.58 -\tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring}
provides the operators \isa{+} and~\isa{*}, which are commutative and
associative, with the usual distributive law and with \isa{0} and~\isa{1}
as their respective identities. An \emph{ordered semiring} is also linearly
ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring.
    1.59 +\tcdx{semiring} and \tcdx{ordered_semiring}: a \emph{semiring}
    1.60 +provides the operators \isa{+} and~\isa{*}, which are commutative and
    1.61 +associative, with the usual distributive law and with \isa{0} and~\isa{1}
    1.62 +as their respective identities. An \emph{ordered semiring} is also linearly
    1.63 +ordered, with addition and multiplication respecting the ordering. Type \isa{nat} is an ordered semiring.
    1.64  \item 
    1.65 -\tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring
with unary minus (the additive inverse) and subtraction (both
denoted~\isa{-}). An \emph{ordered ring} includes the absolute value
function, \cdx{abs}. Type \isa{int} is an ordered ring.
    1.66 +\tcdx{ring} and \tcdx{ordered_ring}: a \emph{ring} extends a semiring
    1.67 +with unary minus (the additive inverse) and subtraction (both
    1.68 +denoted~\isa{-}). An \emph{ordered ring} includes the absolute value
    1.69 +function, \cdx{abs}. Type \isa{int} is an ordered ring.
    1.70  \item 
    1.71 -\tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the
multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/}).
An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
    1.72 +\tcdx{field} and \tcdx{ordered_field}: a field extends a ring with the
    1.73 +multiplicative inverse (called simply \cdx{inverse} and division~(\isa{/}).
    1.74 +An ordered field is based on an ordered ring. Type \isa{complex} is a field, while type \isa{real} is an ordered field.
    1.75  \item 
    1.76  \tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}
    1.77  and \isa{a / 0 = 0}. These include all of Isabelle's standard numeric types.
    1.78  However, the basic properties of fields are derived without assuming
    1.79 -division by zero.
\end{itemize}
    1.80 +division by zero.
    1.81 +\end{itemize}
    1.82  
    1.83 -Theory \thydx{Ring_and_Field} proves over 250 lemmas, each of which
holds for all types in the corresponding type class. In most
cases, it is obvious whether a property is valid for a particular type. All
abstract properties involving subtraction require a ring, and therefore do
not hold for type \isa{nat}, although we have theorems such as
\isa{diff_mult_distrib} proved specifically about subtraction on
type~\isa{nat}. All abstract properties involving division require a field.
Obviously, all properties involving orderings required an ordered
structure.
    1.84 +Theory \thydx{Ring_and_Field} proves over 250 lemmas, each of which
    1.85 +holds for all types in the corresponding type class. In most
    1.86 +cases, it is obvious whether a property is valid for a particular type. All
    1.87 +abstract properties involving subtraction require a ring, and therefore do
    1.88 +not hold for type \isa{nat}, although we have theorems such as
    1.89 +\isa{diff_mult_distrib} proved specifically about subtraction on
    1.90 +type~\isa{nat}. All abstract properties involving division require a field.
    1.91 +Obviously, all properties involving orderings required an ordered
    1.92 +structure.
    1.93  
    1.94  The following two theorems are less obvious. Although they
    1.95  mention no ordering, they require an ordered ring. However, if we have a 
     2.1 --- a/src/HOL/Datatype.thy	Wed Nov 08 11:23:09 2006 +0100
     2.2 +++ b/src/HOL/Datatype.thy	Wed Nov 08 13:48:29 2006 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  header{*Analogues of the Cartesian Product and Disjoint Sum for Datatypes*}
     2.5  
     2.6  theory Datatype
     2.7 -imports NatArith Sum_Type
     2.8 +imports Nat Sum_Type
     2.9  begin
    2.10  
    2.11  typedef (Node)
     3.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Nov 08 11:23:09 2006 +0100
     3.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Nov 08 13:48:29 2006 +0100
     3.3 @@ -7,7 +7,7 @@
     3.4  header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
     3.5  
     3.6  theory Hilbert_Choice
     3.7 -imports NatArith
     3.8 +imports Nat
     3.9  uses ("Tools/meson.ML") ("Tools/specification_package.ML")
    3.10  begin
    3.11  
     4.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Wed Nov 08 11:23:09 2006 +0100
     4.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Wed Nov 08 13:48:29 2006 +0100
     4.3 @@ -47,7 +47,7 @@
     4.4    "SUC_NOT" > "Nat.nat.simps_2"
     4.5    "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
     4.6    "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
     4.7 -  "SUB_SUB" > "NatArith.diff_diff_right"
     4.8 +  "SUB_SUB" > "Nat.diff_diff_right"
     4.9    "SUB_RIGHT_SUB" > "Nat.diff_diff_left"
    4.10    "SUB_RIGHT_LESS_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_LESS_EQ"
    4.11    "SUB_RIGHT_LESS" > "HOL4Base.arithmetic.SUB_RIGHT_LESS"
    4.12 @@ -64,8 +64,8 @@
    4.13    "SUB_LEFT_SUC" > "HOL4Base.arithmetic.SUB_LEFT_SUC"
    4.14    "SUB_LEFT_SUB" > "HOL4Base.arithmetic.SUB_LEFT_SUB"
    4.15    "SUB_LEFT_LESS_EQ" > "HOL4Base.arithmetic.SUB_LEFT_LESS_EQ"
    4.16 -  "SUB_LEFT_LESS" > "NatArith.less_diff_conv"
    4.17 -  "SUB_LEFT_GREATER_EQ" > "NatArith.le_diff_conv"
    4.18 +  "SUB_LEFT_LESS" > "Nat.less_diff_conv"
    4.19 +  "SUB_LEFT_GREATER_EQ" > "Nat.le_diff_conv"
    4.20    "SUB_LEFT_GREATER" > "HOL4Base.arithmetic.SUB_LEFT_GREATER"
    4.21    "SUB_LEFT_EQ" > "HOL4Base.arithmetic.SUB_LEFT_EQ"
    4.22    "SUB_LEFT_ADD" > "HOL4Base.arithmetic.SUB_LEFT_ADD"
    4.23 @@ -185,10 +185,10 @@
    4.24    "LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
    4.25    "LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"
    4.26    "LESS_EQ_IMP_LESS_SUC" > "Nat.le_imp_less_Suc"
    4.27 -  "LESS_EQ_EXISTS" > "NatArith.le_iff_add"
    4.28 +  "LESS_EQ_EXISTS" > "Nat.le_iff_add"
    4.29    "LESS_EQ_CASES" > "Nat.nat_le_linear"
    4.30    "LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM"
    4.31 -  "LESS_EQ_ADD_SUB" > "NatArith.add_diff_assoc"
    4.32 +  "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc"
    4.33    "LESS_EQ_ADD" > "Nat.le_add1"
    4.34    "LESS_EQ_0" > "Nat.le_0_eq"
    4.35    "LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym"
    4.36 @@ -249,7 +249,7 @@
    4.37    "DIVISION" > "HOL4Compat.DIVISION"
    4.38    "DA" > "HOL4Base.arithmetic.DA"
    4.39    "COMPLETE_INDUCTION" > "Nat.less_induct"
    4.40 -  "CANCEL_SUB" > "NatArith.eq_diff_iff"
    4.41 +  "CANCEL_SUB" > "Nat.eq_diff_iff"
    4.42    "ALT_ZERO" > "HOL4Compat.ALT_ZERO_def"
    4.43    "ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
    4.44    "ADD_SUC" > "Nat.add_Suc_right"
     5.1 --- a/src/HOL/Integ/IntDef.thy	Wed Nov 08 11:23:09 2006 +0100
     5.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Nov 08 13:48:29 2006 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} 
     5.5  
     5.6  theory IntDef
     5.7 -imports Equiv_Relations NatArith
     5.8 +imports Equiv_Relations Nat
     5.9  begin
    5.10  
    5.11  constdefs
     6.1 --- a/src/HOL/Integ/int_arith1.ML	Wed Nov 08 11:23:09 2006 +0100
     6.2 +++ b/src/HOL/Integ/int_arith1.ML	Wed Nov 08 13:48:29 2006 +0100
     6.3 @@ -530,7 +530,7 @@
     6.4      simpset = simpset addsimps add_rules
     6.5                        addsimprocs Int_Numeral_Base_Simprocs
     6.6                        addcongs [if_weak_cong]}) #>
     6.7 -  arith_inj_const ("NatArith.of_nat", HOLogic.natT --> HOLogic.intT) #>
     6.8 +  arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #>
     6.9    arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
    6.10    arith_discrete "IntDef.int"
    6.11  
     7.1 --- a/src/HOL/Nat.thy	Wed Nov 08 11:23:09 2006 +0100
     7.2 +++ b/src/HOL/Nat.thy	Wed Nov 08 13:48:29 2006 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4  (*  Title:      HOL/Nat.thy
     7.5      ID:         $Id$
     7.6 -    Author:     Tobias Nipkow and Lawrence C Paulson
     7.7 +    Author:     Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
     7.8  
     7.9  Type "nat" is a linear order, and a datatype; arithmetic operators + -
    7.10  and * (for div, mod and dvd, see theory Divides).
    7.11 @@ -10,6 +10,7 @@
    7.12  
    7.13  theory Nat
    7.14  imports Wellfounded_Recursion Ring_and_Field
    7.15 +uses ("arith_data.ML")
    7.16  begin
    7.17  
    7.18  subsection {* Type @{text ind} *}
    7.19 @@ -40,7 +41,10 @@
    7.20  global
    7.21  
    7.22  typedef (open Nat)
    7.23 -  nat = Nat by (rule exI, rule Nat.Zero_RepI)
    7.24 +  nat = Nat
    7.25 +proof
    7.26 +  show "Zero_Rep : Nat" by (rule Nat.Zero_RepI)
    7.27 +qed
    7.28  
    7.29  instance nat :: "{ord, zero, one}" ..
    7.30  
    7.31 @@ -107,6 +111,10 @@
    7.32  lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
    7.33    by auto
    7.34  
    7.35 +
    7.36 +text {* size of a datatype value; overloaded *}
    7.37 +consts size :: "'a => nat"
    7.38 +
    7.39  text {* @{typ nat} is a datatype *}
    7.40  
    7.41  rep_datatype nat
    7.42 @@ -378,6 +386,7 @@
    7.43  
    7.44  lemmas less_induct = nat_less_induct [rule_format, case_names less]
    7.45  
    7.46 +
    7.47  subsection {* Properties of "less than or equal" *}
    7.48  
    7.49  text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
    7.50 @@ -519,6 +528,7 @@
    7.51  lemma one_reorient: "(1 = x) = (x = 1)"
    7.52    by auto
    7.53  
    7.54 +
    7.55  subsection {* Arithmetic operators *}
    7.56  
    7.57  axclass power < type
    7.58 @@ -531,9 +541,6 @@
    7.59  
    7.60  instance nat :: "{plus, minus, times, power}" ..
    7.61  
    7.62 -text {* size of a datatype value; overloaded *}
    7.63 -consts size :: "'a => nat"
    7.64 -
    7.65  primrec
    7.66    add_0:    "0 + n = n"
    7.67    add_Suc:  "Suc m + n = Suc (m + n)"
    7.68 @@ -589,6 +596,7 @@
    7.69    apply (blast intro: less_trans)+
    7.70    done
    7.71  
    7.72 +
    7.73  subsection {* @{text LEAST} theorems for type @{typ nat}*}
    7.74  
    7.75  lemma Least_Suc:
    7.76 @@ -608,7 +616,6 @@
    7.77    by (erule (1) Least_Suc [THEN ssubst], simp)
    7.78  
    7.79  
    7.80 -
    7.81  subsection {* @{term min} and @{term max} *}
    7.82  
    7.83  lemma min_0L [simp]: "min 0 n = (0::nat)"
    7.84 @@ -764,6 +771,7 @@
    7.85    apply (induct_tac [2] n, simp_all)
    7.86    done
    7.87  
    7.88 +
    7.89  subsection {* Monotonicity of Addition *}
    7.90  
    7.91  text {* strict, in 1st argument *}
    7.92 @@ -906,7 +914,6 @@
    7.93      simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
    7.94  
    7.95  
    7.96 -
    7.97  subsection {* Difference *}
    7.98  
    7.99  lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
   7.100 @@ -1121,4 +1128,240 @@
   7.101  lemma [code func]:
   7.102    "Code_Generator.eq 0 (Suc m) = False" unfolding eq_def by auto
   7.103  
   7.104 +
   7.105 +subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
   7.106 +
   7.107 +use "arith_data.ML"
   7.108 +setup arith_setup
   7.109 +
   7.110 +text{*The following proofs may rely on the arithmetic proof procedures.*}
   7.111 +
   7.112 +lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
   7.113 +  by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add)
   7.114 +
   7.115 +lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
   7.116 +by (simp add: less_eq reflcl_trancl [symmetric]
   7.117 +            del: reflcl_trancl, arith)
   7.118 +
   7.119 +lemma nat_diff_split:
   7.120 +    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
   7.121 +    -- {* elimination of @{text -} on @{text nat} *}
   7.122 +  by (cases "a<b" rule: case_split)
   7.123 +     (auto simp add: diff_is_0_eq [THEN iffD2])
   7.124 +
   7.125 +lemma nat_diff_split_asm:
   7.126 +    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
   7.127 +    -- {* elimination of @{text -} on @{text nat} in assumptions *}
   7.128 +  by (simp split: nat_diff_split)
   7.129 +
   7.130 +lemmas [arith_split] = nat_diff_split split_min split_max
   7.131 +
   7.132 +
   7.133 +
   7.134 +lemma le_square: "m \<le> m * (m::nat)"
   7.135 +  by (induct m) auto
   7.136 +
   7.137 +lemma le_cube: "(m::nat) \<le> m * (m * m)"
   7.138 +  by (induct m) auto
   7.139 +
   7.140 +
   7.141 +text{*Subtraction laws, mostly by Clemens Ballarin*}
   7.142 +
   7.143 +lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
   7.144 +by arith
   7.145 +
   7.146 +lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
   7.147 +by arith
   7.148 +
   7.149 +lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
   7.150 +by arith
   7.151 +
   7.152 +lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
   7.153 +by arith
   7.154 +
   7.155 +lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
   7.156 +by arith
   7.157 +
   7.158 +lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
   7.159 +by arith
   7.160 +
   7.161 +(*Replaces the previous diff_less and le_diff_less, which had the stronger
   7.162 +  second premise n\<le>m*)
   7.163 +lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
   7.164 +by arith
   7.165 +
   7.166 +
   7.167 +(** Simplification of relational expressions involving subtraction **)
   7.168 +
   7.169 +lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
   7.170 +by (simp split add: nat_diff_split)
   7.171 +
   7.172 +lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
   7.173 +by (auto split add: nat_diff_split)
   7.174 +
   7.175 +lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
   7.176 +by (auto split add: nat_diff_split)
   7.177 +
   7.178 +lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
   7.179 +by (auto split add: nat_diff_split)
   7.180 +
   7.181 +
   7.182 +text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
   7.183 +
   7.184 +(* Monotonicity of subtraction in first argument *)
   7.185 +lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
   7.186 +by (simp split add: nat_diff_split)
   7.187 +
   7.188 +lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
   7.189 +by (simp split add: nat_diff_split)
   7.190 +
   7.191 +lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
   7.192 +by (simp split add: nat_diff_split)
   7.193 +
   7.194 +lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
   7.195 +by (simp split add: nat_diff_split)
   7.196 +
   7.197 +text{*Lemmas for ex/Factorization*}
   7.198 +
   7.199 +lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
   7.200 +by (case_tac "m", auto)
   7.201 +
   7.202 +lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
   7.203 +by (case_tac "m", auto)
   7.204 +
   7.205 +lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
   7.206 +by (case_tac "m", auto)
   7.207 +
   7.208 +
   7.209 +text{*Rewriting to pull differences out*}
   7.210 +
   7.211 +lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
   7.212 +by arith
   7.213 +
   7.214 +lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
   7.215 +by arith
   7.216 +
   7.217 +lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
   7.218 +by arith
   7.219 +
   7.220 +(*The others are
   7.221 +      i - j - k = i - (j + k),
   7.222 +      k \<le> j ==> j - k + i = j + i - k,
   7.223 +      k \<le> j ==> i + (j - k) = i + j - k *)
   7.224 +lemmas add_diff_assoc = diff_add_assoc [symmetric]
   7.225 +lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
   7.226 +declare diff_diff_left [simp]  add_diff_assoc [simp]  add_diff_assoc2[simp]
   7.227 +
   7.228 +text{*At present we prove no analogue of @{text not_less_Least} or @{text
   7.229 +Least_Suc}, since there appears to be no need.*}
   7.230 +
   7.231 +ML
   7.232 +{*
   7.233 +val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
   7.234 +val nat_diff_split = thm "nat_diff_split";
   7.235 +val nat_diff_split_asm = thm "nat_diff_split_asm";
   7.236 +val le_square = thm "le_square";
   7.237 +val le_cube = thm "le_cube";
   7.238 +val diff_less_mono = thm "diff_less_mono";
   7.239 +val less_diff_conv = thm "less_diff_conv";
   7.240 +val le_diff_conv = thm "le_diff_conv";
   7.241 +val le_diff_conv2 = thm "le_diff_conv2";
   7.242 +val diff_diff_cancel = thm "diff_diff_cancel";
   7.243 +val le_add_diff = thm "le_add_diff";
   7.244 +val diff_less = thm "diff_less";
   7.245 +val diff_diff_eq = thm "diff_diff_eq";
   7.246 +val eq_diff_iff = thm "eq_diff_iff";
   7.247 +val less_diff_iff = thm "less_diff_iff";
   7.248 +val le_diff_iff = thm "le_diff_iff";
   7.249 +val diff_le_mono = thm "diff_le_mono";
   7.250 +val diff_le_mono2 = thm "diff_le_mono2";
   7.251 +val diff_less_mono2 = thm "diff_less_mono2";
   7.252 +val diffs0_imp_equal = thm "diffs0_imp_equal";
   7.253 +val one_less_mult = thm "one_less_mult";
   7.254 +val n_less_m_mult_n = thm "n_less_m_mult_n";
   7.255 +val n_less_n_mult_m = thm "n_less_n_mult_m";
   7.256 +val diff_diff_right = thm "diff_diff_right";
   7.257 +val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
   7.258 +val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
   7.259 +*}
   7.260 +
   7.261 +subsection{*Embedding of the Naturals into any @{text
   7.262 +semiring_1_cancel}: @{term of_nat}*}
   7.263 +
   7.264 +consts of_nat :: "nat => 'a::semiring_1_cancel"
   7.265 +
   7.266 +primrec
   7.267 +  of_nat_0:   "of_nat 0 = 0"
   7.268 +  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
   7.269 +
   7.270 +lemma of_nat_1 [simp]: "of_nat 1 = 1"
   7.271 +by simp
   7.272 +
   7.273 +lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
   7.274 +apply (induct m)
   7.275 +apply (simp_all add: add_ac)
   7.276 +done
   7.277 +
   7.278 +lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
   7.279 +apply (induct m)
   7.280 +apply (simp_all add: add_ac left_distrib)
   7.281 +done
   7.282 +
   7.283 +lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
   7.284 +apply (induct m, simp_all)
   7.285 +apply (erule order_trans)
   7.286 +apply (rule less_add_one [THEN order_less_imp_le])
   7.287 +done
   7.288 +
   7.289 +lemma less_imp_of_nat_less:
   7.290 +     "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
   7.291 +apply (induct m n rule: diff_induct, simp_all)
   7.292 +apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
   7.293 +done
   7.294 +
   7.295 +lemma of_nat_less_imp_less:
   7.296 +     "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
   7.297 +apply (induct m n rule: diff_induct, simp_all)
   7.298 +apply (insert zero_le_imp_of_nat)
   7.299 +apply (force simp add: linorder_not_less [symmetric])
   7.300 +done
   7.301 +
   7.302 +lemma of_nat_less_iff [simp]:
   7.303 +     "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
   7.304 +by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
   7.305 +
   7.306 +text{*Special cases where either operand is zero*}
   7.307 +lemmas of_nat_0_less_iff = of_nat_less_iff [of 0, simplified]
   7.308 +lemmas of_nat_less_0_iff = of_nat_less_iff [of _ 0, simplified]
   7.309 +declare of_nat_0_less_iff [simp]
   7.310 +declare of_nat_less_0_iff [simp]
   7.311 +
   7.312 +lemma of_nat_le_iff [simp]:
   7.313 +     "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
   7.314 +by (simp add: linorder_not_less [symmetric])
   7.315 +
   7.316 +text{*Special cases where either operand is zero*}
   7.317 +lemmas of_nat_0_le_iff = of_nat_le_iff [of 0, simplified]
   7.318 +lemmas of_nat_le_0_iff = of_nat_le_iff [of _ 0, simplified]
   7.319 +declare of_nat_0_le_iff [simp]
   7.320 +declare of_nat_le_0_iff [simp]
   7.321 +
   7.322 +text{*The ordering on the @{text semiring_1_cancel} is necessary
   7.323 +to exclude the possibility of a finite field, which indeed wraps back to
   7.324 +zero.*}
   7.325 +lemma of_nat_eq_iff [simp]:
   7.326 +     "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
   7.327 +by (simp add: order_eq_iff)
   7.328 +
   7.329 +text{*Special cases where either operand is zero*}
   7.330 +lemmas of_nat_0_eq_iff = of_nat_eq_iff [of 0, simplified]
   7.331 +lemmas of_nat_eq_0_iff = of_nat_eq_iff [of _ 0, simplified]
   7.332 +declare of_nat_0_eq_iff [simp]
   7.333 +declare of_nat_eq_0_iff [simp]
   7.334 +
   7.335 +lemma of_nat_diff [simp]:
   7.336 +     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
   7.337 +by (simp del: of_nat_add
   7.338 +	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
   7.339 +
   7.340  end
     8.1 --- a/src/HOL/NatArith.thy	Wed Nov 08 11:23:09 2006 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,246 +0,0 @@
     8.4 -(*  Title:      HOL/NatArith.thy
     8.5 -    ID:         $Id$
     8.6 -    Author:     Tobias Nipkow and Markus Wenzel
     8.7 -*)
     8.8 -
     8.9 -header {*Further Arithmetic Facts Concerning the Natural Numbers*}
    8.10 -
    8.11 -theory NatArith
    8.12 -imports Nat
    8.13 -uses "arith_data.ML"
    8.14 -begin
    8.15 -
    8.16 -setup arith_setup
    8.17 -
    8.18 -text{*The following proofs may rely on the arithmetic proof procedures.*}
    8.19 -
    8.20 -lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
    8.21 -  by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add)
    8.22 -
    8.23 -lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
    8.24 -by (simp add: less_eq reflcl_trancl [symmetric]
    8.25 -            del: reflcl_trancl, arith)
    8.26 -
    8.27 -lemma nat_diff_split:
    8.28 -    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
    8.29 -    -- {* elimination of @{text -} on @{text nat} *}
    8.30 -  by (cases "a<b" rule: case_split)
    8.31 -     (auto simp add: diff_is_0_eq [THEN iffD2])
    8.32 -
    8.33 -lemma nat_diff_split_asm:
    8.34 -    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
    8.35 -    -- {* elimination of @{text -} on @{text nat} in assumptions *}
    8.36 -  by (simp split: nat_diff_split)
    8.37 -
    8.38 -lemmas [arith_split] = nat_diff_split split_min split_max
    8.39 -
    8.40 -
    8.41 -
    8.42 -lemma le_square: "m \<le> m*(m::nat)"
    8.43 -by (induct_tac "m", auto)
    8.44 -
    8.45 -lemma le_cube: "(m::nat) \<le> m*(m*m)"
    8.46 -by (induct_tac "m", auto)
    8.47 -
    8.48 -
    8.49 -text{*Subtraction laws, mostly by Clemens Ballarin*}
    8.50 -
    8.51 -lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
    8.52 -by arith
    8.53 -
    8.54 -lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
    8.55 -by arith
    8.56 -
    8.57 -lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
    8.58 -by arith
    8.59 -
    8.60 -lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
    8.61 -by arith
    8.62 -
    8.63 -lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
    8.64 -by arith
    8.65 -
    8.66 -lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
    8.67 -by arith
    8.68 -
    8.69 -(*Replaces the previous diff_less and le_diff_less, which had the stronger
    8.70 -  second premise n\<le>m*)
    8.71 -lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
    8.72 -by arith
    8.73 -
    8.74 -
    8.75 -(** Simplification of relational expressions involving subtraction **)
    8.76 -
    8.77 -lemma diff_diff_eq: "[| k \<le> m;  k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
    8.78 -by (simp split add: nat_diff_split)
    8.79 -
    8.80 -lemma eq_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
    8.81 -by (auto split add: nat_diff_split)
    8.82 -
    8.83 -lemma less_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
    8.84 -by (auto split add: nat_diff_split)
    8.85 -
    8.86 -lemma le_diff_iff: "[| k \<le> m;  k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
    8.87 -by (auto split add: nat_diff_split)
    8.88 -
    8.89 -
    8.90 -text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
    8.91 -
    8.92 -(* Monotonicity of subtraction in first argument *)
    8.93 -lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
    8.94 -by (simp split add: nat_diff_split)
    8.95 -
    8.96 -lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
    8.97 -by (simp split add: nat_diff_split)
    8.98 -
    8.99 -lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
   8.100 -by (simp split add: nat_diff_split)
   8.101 -
   8.102 -lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n"
   8.103 -by (simp split add: nat_diff_split)
   8.104 -
   8.105 -text{*Lemmas for ex/Factorization*}
   8.106 -
   8.107 -lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
   8.108 -by (case_tac "m", auto)
   8.109 -
   8.110 -lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
   8.111 -by (case_tac "m", auto)
   8.112 -
   8.113 -lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
   8.114 -by (case_tac "m", auto)
   8.115 -
   8.116 -
   8.117 -text{*Rewriting to pull differences out*}
   8.118 -
   8.119 -lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
   8.120 -by arith
   8.121 -
   8.122 -lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
   8.123 -by arith
   8.124 -
   8.125 -lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
   8.126 -by arith
   8.127 -
   8.128 -(*The others are
   8.129 -      i - j - k = i - (j + k),
   8.130 -      k \<le> j ==> j - k + i = j + i - k,
   8.131 -      k \<le> j ==> i + (j - k) = i + j - k *)
   8.132 -lemmas add_diff_assoc = diff_add_assoc [symmetric]
   8.133 -lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
   8.134 -declare diff_diff_left [simp]  add_diff_assoc [simp]  add_diff_assoc2[simp]
   8.135 -
   8.136 -text{*At present we prove no analogue of @{text not_less_Least} or @{text
   8.137 -Least_Suc}, since there appears to be no need.*}
   8.138 -
   8.139 -ML
   8.140 -{*
   8.141 -val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
   8.142 -val nat_diff_split = thm "nat_diff_split";
   8.143 -val nat_diff_split_asm = thm "nat_diff_split_asm";
   8.144 -val le_square = thm "le_square";
   8.145 -val le_cube = thm "le_cube";
   8.146 -val diff_less_mono = thm "diff_less_mono";
   8.147 -val less_diff_conv = thm "less_diff_conv";
   8.148 -val le_diff_conv = thm "le_diff_conv";
   8.149 -val le_diff_conv2 = thm "le_diff_conv2";
   8.150 -val diff_diff_cancel = thm "diff_diff_cancel";
   8.151 -val le_add_diff = thm "le_add_diff";
   8.152 -val diff_less = thm "diff_less";
   8.153 -val diff_diff_eq = thm "diff_diff_eq";
   8.154 -val eq_diff_iff = thm "eq_diff_iff";
   8.155 -val less_diff_iff = thm "less_diff_iff";
   8.156 -val le_diff_iff = thm "le_diff_iff";
   8.157 -val diff_le_mono = thm "diff_le_mono";
   8.158 -val diff_le_mono2 = thm "diff_le_mono2";
   8.159 -val diff_less_mono2 = thm "diff_less_mono2";
   8.160 -val diffs0_imp_equal = thm "diffs0_imp_equal";
   8.161 -val one_less_mult = thm "one_less_mult";
   8.162 -val n_less_m_mult_n = thm "n_less_m_mult_n";
   8.163 -val n_less_n_mult_m = thm "n_less_n_mult_m";
   8.164 -val diff_diff_right = thm "diff_diff_right";
   8.165 -val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
   8.166 -val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
   8.167 -*}
   8.168 -
   8.169 -subsection{*Embedding of the Naturals into any @{text
   8.170 -semiring_1_cancel}: @{term of_nat}*}
   8.171 -
   8.172 -consts of_nat :: "nat => 'a::semiring_1_cancel"
   8.173 -
   8.174 -primrec
   8.175 -  of_nat_0:   "of_nat 0 = 0"
   8.176 -  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
   8.177 -
   8.178 -lemma of_nat_1 [simp]: "of_nat 1 = 1"
   8.179 -by simp
   8.180 -
   8.181 -lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
   8.182 -apply (induct m)
   8.183 -apply (simp_all add: add_ac)
   8.184 -done
   8.185 -
   8.186 -lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
   8.187 -apply (induct m)
   8.188 -apply (simp_all add: add_ac left_distrib)
   8.189 -done
   8.190 -
   8.191 -lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
   8.192 -apply (induct m, simp_all)
   8.193 -apply (erule order_trans)
   8.194 -apply (rule less_add_one [THEN order_less_imp_le])
   8.195 -done
   8.196 -
   8.197 -lemma less_imp_of_nat_less:
   8.198 -     "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
   8.199 -apply (induct m n rule: diff_induct, simp_all)
   8.200 -apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
   8.201 -done
   8.202 -
   8.203 -lemma of_nat_less_imp_less:
   8.204 -     "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
   8.205 -apply (induct m n rule: diff_induct, simp_all)
   8.206 -apply (insert zero_le_imp_of_nat)
   8.207 -apply (force simp add: linorder_not_less [symmetric])
   8.208 -done
   8.209 -
   8.210 -lemma of_nat_less_iff [simp]:
   8.211 -     "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
   8.212 -by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
   8.213 -
   8.214 -text{*Special cases where either operand is zero*}
   8.215 -lemmas of_nat_0_less_iff = of_nat_less_iff [of 0, simplified]
   8.216 -lemmas of_nat_less_0_iff = of_nat_less_iff [of _ 0, simplified]
   8.217 -declare of_nat_0_less_iff [simp]
   8.218 -declare of_nat_less_0_iff [simp]
   8.219 -
   8.220 -lemma of_nat_le_iff [simp]:
   8.221 -     "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
   8.222 -by (simp add: linorder_not_less [symmetric])
   8.223 -
   8.224 -text{*Special cases where either operand is zero*}
   8.225 -lemmas of_nat_0_le_iff = of_nat_le_iff [of 0, simplified]
   8.226 -lemmas of_nat_le_0_iff = of_nat_le_iff [of _ 0, simplified]
   8.227 -declare of_nat_0_le_iff [simp]
   8.228 -declare of_nat_le_0_iff [simp]
   8.229 -
   8.230 -text{*The ordering on the @{text semiring_1_cancel} is necessary
   8.231 -to exclude the possibility of a finite field, which indeed wraps back to
   8.232 -zero.*}
   8.233 -lemma of_nat_eq_iff [simp]:
   8.234 -     "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
   8.235 -by (simp add: order_eq_iff)
   8.236 -
   8.237 -text{*Special cases where either operand is zero*}
   8.238 -lemmas of_nat_0_eq_iff = of_nat_eq_iff [of 0, simplified]
   8.239 -lemmas of_nat_eq_0_iff = of_nat_eq_iff [of _ 0, simplified]
   8.240 -declare of_nat_0_eq_iff [simp]
   8.241 -declare of_nat_eq_0_iff [simp]
   8.242 -
   8.243 -lemma of_nat_diff [simp]:
   8.244 -     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
   8.245 -by (simp del: of_nat_add
   8.246 -	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
   8.247 -
   8.248 -
   8.249 -end
     9.1 --- a/src/HOL/Real/rat_arith.ML	Wed Nov 08 11:23:09 2006 +0100
     9.2 +++ b/src/HOL/Real/rat_arith.ML	Wed Nov 08 13:48:29 2006 +0100
     9.3 @@ -48,7 +48,7 @@
     9.4      neqE =  neqE,
     9.5      simpset = simpset addsimps simps
     9.6                        addsimprocs simprocs}) #>
     9.7 -  arith_inj_const ("NatArith.of_nat", HOLogic.natT --> ratT) #>
     9.8 +  arith_inj_const ("Nat.of_nat", HOLogic.natT --> ratT) #>
     9.9    arith_inj_const ("IntDef.of_int", HOLogic.intT --> ratT) #>
    9.10    (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy))
    9.11  
    10.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Nov 08 11:23:09 2006 +0100
    10.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 08 13:48:29 2006 +0100
    10.3 @@ -877,7 +877,7 @@
    10.4      val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    10.5        [descr] sorts thy7;
    10.6      val (size_thms, thy9) =
    10.7 -      if Context.exists_name "NatArith" thy8 then
    10.8 +      if Context.exists_name "Nat" thy8 then
    10.9          DatatypeAbsProofs.prove_size_thms false new_type_names
   10.10            [descr] sorts reccomb_names rec_thms thy8
   10.11        else ([], thy8);
    11.1 --- a/src/HOL/Tools/res_atp.ML	Wed Nov 08 11:23:09 2006 +0100
    11.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Nov 08 13:48:29 2006 +0100
    11.3 @@ -361,9 +361,9 @@
    11.4     "Nat.less_one", (*not directional? obscure*)
    11.5     "Nat.not_gr0",
    11.6     "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
    11.7 -   "NatArith.of_nat_0_eq_iff",
    11.8 -   "NatArith.of_nat_eq_0_iff",
    11.9 -   "NatArith.of_nat_le_0_iff",
   11.10 +   "Nat.of_nat_0_eq_iff",
   11.11 +   "Nat.of_nat_eq_0_iff",
   11.12 +   "Nat.of_nat_le_0_iff",
   11.13     "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
   11.14     "NatSimprocs.divide_less_0_iff_number_of",
   11.15     "NatSimprocs.equation_minus_iff_1",  (*not directional*)
    12.1 --- a/src/HOL/arith_data.ML	Wed Nov 08 11:23:09 2006 +0100
    12.2 +++ b/src/HOL/arith_data.ML	Wed Nov 08 13:48:29 2006 +0100
    12.3 @@ -61,8 +61,8 @@
    12.4    let val ss0 = HOL_ss addsimps rules
    12.5    in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    12.6  
    12.7 -val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
    12.8 -val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
    12.9 +val add_rules = [thm "add_Suc", thm "add_Suc_right", thm "add_0", thm "add_0_right"];
   12.10 +val mult_rules = [thm "mult_Suc", thm "mult_Suc_right", thm "mult_0", thm "mult_0_right"];
   12.11  
   12.12  fun prep_simproc (name, pats, proc) =
   12.13    Simplifier.simproc (the_context ()) name pats proc;
   12.14 @@ -104,7 +104,7 @@
   12.15    open Sum;
   12.16    val mk_bal = HOLogic.mk_eq;
   12.17    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   12.18 -  val uncancel_tac = gen_uncancel_tac nat_add_left_cancel;
   12.19 +  val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel");
   12.20  end);
   12.21  
   12.22  (* nat less *)
   12.23 @@ -114,7 +114,7 @@
   12.24    open Sum;
   12.25    val mk_bal = HOLogic.mk_binrel "Orderings.less";
   12.26    val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT;
   12.27 -  val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
   12.28 +  val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel_less");
   12.29  end);
   12.30  
   12.31  (* nat le *)
   12.32 @@ -124,7 +124,7 @@
   12.33    open Sum;
   12.34    val mk_bal = HOLogic.mk_binrel "Orderings.less_eq";
   12.35    val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT;
   12.36 -  val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
   12.37 +  val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel_le");
   12.38  end);
   12.39  
   12.40  (* nat diff *)
   12.41 @@ -134,7 +134,7 @@
   12.42    open Sum;
   12.43    val mk_bal = HOLogic.mk_binop "HOL.minus";
   12.44    val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
   12.45 -  val uncancel_tac = gen_uncancel_tac diff_cancel;
   12.46 +  val uncancel_tac = gen_uncancel_tac (thm "diff_cancel");
   12.47  end);
   12.48  
   12.49  (** prepare nat_cancel simprocs **)
   12.50 @@ -175,6 +175,7 @@
   12.51  val sym = sym;
   12.52  val not_lessD = linorder_not_less RS iffD1;
   12.53  val not_leD = linorder_not_le RS iffD1;
   12.54 +val le0 = thm "le0";
   12.55  
   12.56  fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
   12.57  
   12.58 @@ -931,10 +932,10 @@
   12.59     Most of the work is done by the cancel tactics.
   12.60  *)
   12.61  val add_rules =
   12.62 - [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
   12.63 -  One_nat_def,
   12.64 -  order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one,
   12.65 -  zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
   12.66 + [thm "add_zero_left", thm "add_zero_right", thm "Zero_not_Suc", thm "Suc_not_Zero",
   12.67 +  thm "le_0_eq", thm "One_nat_def", thm "order_less_irrefl", thm "zero_neq_one",
   12.68 +  thm "zero_less_one", thm "zero_le_one", thm "zero_neq_one" RS not_sym, thm "not_one_le_zero",
   12.69 +  thm "not_one_less_zero"];
   12.70  
   12.71  val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
   12.72   (fn prems => [cut_facts_tac prems 1,
   12.73 @@ -966,8 +967,8 @@
   12.74      add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
   12.75      mult_mono_thms = mult_mono_thms,
   12.76      inj_thms = inj_thms,
   12.77 -    lessD = lessD @ [Suc_leI],
   12.78 -    neqE = [linorder_neqE_nat,
   12.79 +    lessD = lessD @ [thm "Suc_leI"],
   12.80 +    neqE = [thm "linorder_neqE_nat",
   12.81        get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
   12.82      simpset = HOL_basic_ss addsimps add_rules
   12.83                     addsimprocs [ab_group_add_cancel.sum_conv,