--- a/doc-src/TutorialI/Types/numerics.tex Wed Nov 08 11:23:09 2006 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Wed Nov 08 13:48:29 2006 +0100
@@ -48,7 +48,10 @@
\index{numeric literals|(}%
The constants \cdx{0} and \cdx{1} are overloaded. They denote zero and one,
respectively, for all numeric types. Other values are expressed by numeric
-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.
+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.
Literals look like constants, but they abbreviate
terms representing the number in a two's complement binary notation.
@@ -102,7 +105,7 @@
\index{natural numbers|(}\index{*nat (type)|(}%
This type requires no introduction: we have been using it from the
beginning. Hundreds of theorems about the natural numbers are
-proved in the theories \isa{Nat}, \isa{NatArith} and \isa{Divides}.
+proved in the theories \isa{Nat} and \isa{Divides}.
Basic properties of addition and multiplication are available through the
axiomatic type class for semirings (\S\ref{sec:numeric-axclasses}).
@@ -234,7 +237,12 @@
\index{integers|(}\index{*int (type)|(}%
Reasoning methods for the integers resemble those for the natural numbers,
-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}).
+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}).
The \rmindex{absolute value} function \cdx{abs} is overloaded, and is
defined for all types that involve negative numbers, including the integers.
@@ -324,8 +332,13 @@
\rulename{dense}
\end{isabelle}
-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,
-can be found in theory \texttt{RComplete} of directory
\texttt{Real}.
+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,
+can be found in theory \texttt{RComplete} of directory
+\texttt{Real}.
Numeric literals\index{numeric literals!for type \protect\isa{real}}
for type \isa{real} have the same syntax as those for type
@@ -375,18 +388,36 @@
the following type classes:
\begin{itemize}
\item
-\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.
+\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.
\item
-\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.
+\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.
\item
-\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.
+\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.
\item
\tcdx{division_by_zero} includes all types where \isa{inverse 0 = 0}
and \isa{a / 0 = 0}. These include all of Isabelle's standard numeric types.
However, the basic properties of fields are derived without assuming
-division by zero.
\end{itemize}
+division by zero.
+\end{itemize}
-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.
+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.
The following two theorems are less obvious. Although they
mention no ordering, they require an ordered ring. However, if we have a
--- a/src/HOL/Datatype.thy Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Datatype.thy Wed Nov 08 13:48:29 2006 +0100
@@ -9,7 +9,7 @@
header{*Analogues of the Cartesian Product and Disjoint Sum for Datatypes*}
theory Datatype
-imports NatArith Sum_Type
+imports Nat Sum_Type
begin
typedef (Node)
--- a/src/HOL/Hilbert_Choice.thy Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Hilbert_Choice.thy Wed Nov 08 13:48:29 2006 +0100
@@ -7,7 +7,7 @@
header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
theory Hilbert_Choice
-imports NatArith
+imports Nat
uses ("Tools/meson.ML") ("Tools/specification_package.ML")
begin
--- a/src/HOL/Import/HOL/arithmetic.imp Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp Wed Nov 08 13:48:29 2006 +0100
@@ -47,7 +47,7 @@
"SUC_NOT" > "Nat.nat.simps_2"
"SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
"SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
- "SUB_SUB" > "NatArith.diff_diff_right"
+ "SUB_SUB" > "Nat.diff_diff_right"
"SUB_RIGHT_SUB" > "Nat.diff_diff_left"
"SUB_RIGHT_LESS_EQ" > "HOL4Base.arithmetic.SUB_RIGHT_LESS_EQ"
"SUB_RIGHT_LESS" > "HOL4Base.arithmetic.SUB_RIGHT_LESS"
@@ -64,8 +64,8 @@
"SUB_LEFT_SUC" > "HOL4Base.arithmetic.SUB_LEFT_SUC"
"SUB_LEFT_SUB" > "HOL4Base.arithmetic.SUB_LEFT_SUB"
"SUB_LEFT_LESS_EQ" > "HOL4Base.arithmetic.SUB_LEFT_LESS_EQ"
- "SUB_LEFT_LESS" > "NatArith.less_diff_conv"
- "SUB_LEFT_GREATER_EQ" > "NatArith.le_diff_conv"
+ "SUB_LEFT_LESS" > "Nat.less_diff_conv"
+ "SUB_LEFT_GREATER_EQ" > "Nat.le_diff_conv"
"SUB_LEFT_GREATER" > "HOL4Base.arithmetic.SUB_LEFT_GREATER"
"SUB_LEFT_EQ" > "HOL4Base.arithmetic.SUB_LEFT_EQ"
"SUB_LEFT_ADD" > "HOL4Base.arithmetic.SUB_LEFT_ADD"
@@ -185,10 +185,10 @@
"LESS_EQ_LESS_TRANS" > "Nat.le_less_trans"
"LESS_EQ_LESS_EQ_MONO" > "Nat.add_le_mono"
"LESS_EQ_IMP_LESS_SUC" > "Nat.le_imp_less_Suc"
- "LESS_EQ_EXISTS" > "NatArith.le_iff_add"
+ "LESS_EQ_EXISTS" > "Nat.le_iff_add"
"LESS_EQ_CASES" > "Nat.nat_le_linear"
"LESS_EQ_ANTISYM" > "HOL4Base.arithmetic.LESS_EQ_ANTISYM"
- "LESS_EQ_ADD_SUB" > "NatArith.add_diff_assoc"
+ "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc"
"LESS_EQ_ADD" > "Nat.le_add1"
"LESS_EQ_0" > "Nat.le_0_eq"
"LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym"
@@ -249,7 +249,7 @@
"DIVISION" > "HOL4Compat.DIVISION"
"DA" > "HOL4Base.arithmetic.DA"
"COMPLETE_INDUCTION" > "Nat.less_induct"
- "CANCEL_SUB" > "NatArith.eq_diff_iff"
+ "CANCEL_SUB" > "Nat.eq_diff_iff"
"ALT_ZERO" > "HOL4Compat.ALT_ZERO_def"
"ADD_SYM" > "Finite_Set.AC_add.f.AC_2"
"ADD_SUC" > "Nat.add_Suc_right"
--- a/src/HOL/Integ/IntDef.thy Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Wed Nov 08 13:48:29 2006 +0100
@@ -8,7 +8,7 @@
header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
theory IntDef
-imports Equiv_Relations NatArith
+imports Equiv_Relations Nat
begin
constdefs
--- a/src/HOL/Integ/int_arith1.ML Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Integ/int_arith1.ML Wed Nov 08 13:48:29 2006 +0100
@@ -530,7 +530,7 @@
simpset = simpset addsimps add_rules
addsimprocs Int_Numeral_Base_Simprocs
addcongs [if_weak_cong]}) #>
- arith_inj_const ("NatArith.of_nat", HOLogic.natT --> HOLogic.intT) #>
+ arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #>
arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
arith_discrete "IntDef.int"
--- a/src/HOL/Nat.thy Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Nat.thy Wed Nov 08 13:48:29 2006 +0100
@@ -1,6 +1,6 @@
(* Title: HOL/Nat.thy
ID: $Id$
- Author: Tobias Nipkow and Lawrence C Paulson
+ Author: Tobias Nipkow and Lawrence C Paulson and Markus Wenzel
Type "nat" is a linear order, and a datatype; arithmetic operators + -
and * (for div, mod and dvd, see theory Divides).
@@ -10,6 +10,7 @@
theory Nat
imports Wellfounded_Recursion Ring_and_Field
+uses ("arith_data.ML")
begin
subsection {* Type @{text ind} *}
@@ -40,7 +41,10 @@
global
typedef (open Nat)
- nat = Nat by (rule exI, rule Nat.Zero_RepI)
+ nat = Nat
+proof
+ show "Zero_Rep : Nat" by (rule Nat.Zero_RepI)
+qed
instance nat :: "{ord, zero, one}" ..
@@ -107,6 +111,10 @@
lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
by auto
+
+text {* size of a datatype value; overloaded *}
+consts size :: "'a => nat"
+
text {* @{typ nat} is a datatype *}
rep_datatype nat
@@ -378,6 +386,7 @@
lemmas less_induct = nat_less_induct [rule_format, case_names less]
+
subsection {* Properties of "less than or equal" *}
text {* Was @{text le_eq_less_Suc}, but this orientation is more useful *}
@@ -519,6 +528,7 @@
lemma one_reorient: "(1 = x) = (x = 1)"
by auto
+
subsection {* Arithmetic operators *}
axclass power < type
@@ -531,9 +541,6 @@
instance nat :: "{plus, minus, times, power}" ..
-text {* size of a datatype value; overloaded *}
-consts size :: "'a => nat"
-
primrec
add_0: "0 + n = n"
add_Suc: "Suc m + n = Suc (m + n)"
@@ -589,6 +596,7 @@
apply (blast intro: less_trans)+
done
+
subsection {* @{text LEAST} theorems for type @{typ nat}*}
lemma Least_Suc:
@@ -608,7 +616,6 @@
by (erule (1) Least_Suc [THEN ssubst], simp)
-
subsection {* @{term min} and @{term max} *}
lemma min_0L [simp]: "min 0 n = (0::nat)"
@@ -764,6 +771,7 @@
apply (induct_tac [2] n, simp_all)
done
+
subsection {* Monotonicity of Addition *}
text {* strict, in 1st argument *}
@@ -906,7 +914,6 @@
simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
-
subsection {* Difference *}
lemma diff_self_eq_0 [simp]: "(m::nat) - m = 0"
@@ -1121,4 +1128,240 @@
lemma [code func]:
"Code_Generator.eq 0 (Suc m) = False" unfolding eq_def by auto
+
+subsection {* Further Arithmetic Facts Concerning the Natural Numbers *}
+
+use "arith_data.ML"
+setup arith_setup
+
+text{*The following proofs may rely on the arithmetic proof procedures.*}
+
+lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
+ by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add)
+
+lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
+by (simp add: less_eq reflcl_trancl [symmetric]
+ del: reflcl_trancl, arith)
+
+lemma nat_diff_split:
+ "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
+ -- {* elimination of @{text -} on @{text nat} *}
+ by (cases "a<b" rule: case_split)
+ (auto simp add: diff_is_0_eq [THEN iffD2])
+
+lemma nat_diff_split_asm:
+ "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
+ -- {* elimination of @{text -} on @{text nat} in assumptions *}
+ by (simp split: nat_diff_split)
+
+lemmas [arith_split] = nat_diff_split split_min split_max
+
+
+
+lemma le_square: "m \<le> m * (m::nat)"
+ by (induct m) auto
+
+lemma le_cube: "(m::nat) \<le> m * (m * m)"
+ by (induct m) auto
+
+
+text{*Subtraction laws, mostly by Clemens Ballarin*}
+
+lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
+by arith
+
+lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
+by arith
+
+lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
+by arith
+
+lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
+by arith
+
+lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
+by arith
+
+lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
+by arith
+
+(*Replaces the previous diff_less and le_diff_less, which had the stronger
+ second premise n\<le>m*)
+lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
+by arith
+
+
+(** Simplification of relational expressions involving subtraction **)
+
+lemma diff_diff_eq: "[| k \<le> m; k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
+by (simp split add: nat_diff_split)
+
+lemma eq_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
+by (auto split add: nat_diff_split)
+
+lemma less_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
+by (auto split add: nat_diff_split)
+
+lemma le_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
+by (auto split add: nat_diff_split)
+
+
+text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
+
+(* Monotonicity of subtraction in first argument *)
+lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
+by (simp split add: nat_diff_split)
+
+lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
+by (simp split add: nat_diff_split)
+
+lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
+by (simp split add: nat_diff_split)
+
+lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n"
+by (simp split add: nat_diff_split)
+
+text{*Lemmas for ex/Factorization*}
+
+lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
+by (case_tac "m", auto)
+
+lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
+by (case_tac "m", auto)
+
+lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
+by (case_tac "m", auto)
+
+
+text{*Rewriting to pull differences out*}
+
+lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
+by arith
+
+lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
+by arith
+
+lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
+by arith
+
+(*The others are
+ i - j - k = i - (j + k),
+ k \<le> j ==> j - k + i = j + i - k,
+ k \<le> j ==> i + (j - k) = i + j - k *)
+lemmas add_diff_assoc = diff_add_assoc [symmetric]
+lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
+declare diff_diff_left [simp] add_diff_assoc [simp] add_diff_assoc2[simp]
+
+text{*At present we prove no analogue of @{text not_less_Least} or @{text
+Least_Suc}, since there appears to be no need.*}
+
+ML
+{*
+val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
+val nat_diff_split = thm "nat_diff_split";
+val nat_diff_split_asm = thm "nat_diff_split_asm";
+val le_square = thm "le_square";
+val le_cube = thm "le_cube";
+val diff_less_mono = thm "diff_less_mono";
+val less_diff_conv = thm "less_diff_conv";
+val le_diff_conv = thm "le_diff_conv";
+val le_diff_conv2 = thm "le_diff_conv2";
+val diff_diff_cancel = thm "diff_diff_cancel";
+val le_add_diff = thm "le_add_diff";
+val diff_less = thm "diff_less";
+val diff_diff_eq = thm "diff_diff_eq";
+val eq_diff_iff = thm "eq_diff_iff";
+val less_diff_iff = thm "less_diff_iff";
+val le_diff_iff = thm "le_diff_iff";
+val diff_le_mono = thm "diff_le_mono";
+val diff_le_mono2 = thm "diff_le_mono2";
+val diff_less_mono2 = thm "diff_less_mono2";
+val diffs0_imp_equal = thm "diffs0_imp_equal";
+val one_less_mult = thm "one_less_mult";
+val n_less_m_mult_n = thm "n_less_m_mult_n";
+val n_less_n_mult_m = thm "n_less_n_mult_m";
+val diff_diff_right = thm "diff_diff_right";
+val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
+val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
+*}
+
+subsection{*Embedding of the Naturals into any @{text
+semiring_1_cancel}: @{term of_nat}*}
+
+consts of_nat :: "nat => 'a::semiring_1_cancel"
+
+primrec
+ of_nat_0: "of_nat 0 = 0"
+ of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
+
+lemma of_nat_1 [simp]: "of_nat 1 = 1"
+by simp
+
+lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
+apply (induct m)
+apply (simp_all add: add_ac)
+done
+
+lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
+apply (induct m)
+apply (simp_all add: add_ac left_distrib)
+done
+
+lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
+apply (induct m, simp_all)
+apply (erule order_trans)
+apply (rule less_add_one [THEN order_less_imp_le])
+done
+
+lemma less_imp_of_nat_less:
+ "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
+apply (induct m n rule: diff_induct, simp_all)
+apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
+done
+
+lemma of_nat_less_imp_less:
+ "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
+apply (induct m n rule: diff_induct, simp_all)
+apply (insert zero_le_imp_of_nat)
+apply (force simp add: linorder_not_less [symmetric])
+done
+
+lemma of_nat_less_iff [simp]:
+ "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
+by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
+
+text{*Special cases where either operand is zero*}
+lemmas of_nat_0_less_iff = of_nat_less_iff [of 0, simplified]
+lemmas of_nat_less_0_iff = of_nat_less_iff [of _ 0, simplified]
+declare of_nat_0_less_iff [simp]
+declare of_nat_less_0_iff [simp]
+
+lemma of_nat_le_iff [simp]:
+ "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
+by (simp add: linorder_not_less [symmetric])
+
+text{*Special cases where either operand is zero*}
+lemmas of_nat_0_le_iff = of_nat_le_iff [of 0, simplified]
+lemmas of_nat_le_0_iff = of_nat_le_iff [of _ 0, simplified]
+declare of_nat_0_le_iff [simp]
+declare of_nat_le_0_iff [simp]
+
+text{*The ordering on the @{text semiring_1_cancel} is necessary
+to exclude the possibility of a finite field, which indeed wraps back to
+zero.*}
+lemma of_nat_eq_iff [simp]:
+ "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
+by (simp add: order_eq_iff)
+
+text{*Special cases where either operand is zero*}
+lemmas of_nat_0_eq_iff = of_nat_eq_iff [of 0, simplified]
+lemmas of_nat_eq_0_iff = of_nat_eq_iff [of _ 0, simplified]
+declare of_nat_0_eq_iff [simp]
+declare of_nat_eq_0_iff [simp]
+
+lemma of_nat_diff [simp]:
+ "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
+by (simp del: of_nat_add
+ add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
+
end
--- a/src/HOL/NatArith.thy Wed Nov 08 11:23:09 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,246 +0,0 @@
-(* Title: HOL/NatArith.thy
- ID: $Id$
- Author: Tobias Nipkow and Markus Wenzel
-*)
-
-header {*Further Arithmetic Facts Concerning the Natural Numbers*}
-
-theory NatArith
-imports Nat
-uses "arith_data.ML"
-begin
-
-setup arith_setup
-
-text{*The following proofs may rely on the arithmetic proof procedures.*}
-
-lemma le_iff_add: "(m::nat) \<le> n = (\<exists>k. n = m + k)"
- by (auto simp: le_eq_less_or_eq dest: less_imp_Suc_add)
-
-lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m \<le> n)"
-by (simp add: less_eq reflcl_trancl [symmetric]
- del: reflcl_trancl, arith)
-
-lemma nat_diff_split:
- "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
- -- {* elimination of @{text -} on @{text nat} *}
- by (cases "a<b" rule: case_split)
- (auto simp add: diff_is_0_eq [THEN iffD2])
-
-lemma nat_diff_split_asm:
- "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
- -- {* elimination of @{text -} on @{text nat} in assumptions *}
- by (simp split: nat_diff_split)
-
-lemmas [arith_split] = nat_diff_split split_min split_max
-
-
-
-lemma le_square: "m \<le> m*(m::nat)"
-by (induct_tac "m", auto)
-
-lemma le_cube: "(m::nat) \<le> m*(m*m)"
-by (induct_tac "m", auto)
-
-
-text{*Subtraction laws, mostly by Clemens Ballarin*}
-
-lemma diff_less_mono: "[| a < (b::nat); c \<le> a |] ==> a-c < b-c"
-by arith
-
-lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
-by arith
-
-lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
-by arith
-
-lemma le_diff_conv2: "k \<le> j ==> (i \<le> j-k) = (i+k \<le> (j::nat))"
-by arith
-
-lemma diff_diff_cancel [simp]: "i \<le> (n::nat) ==> n - (n - i) = i"
-by arith
-
-lemma le_add_diff: "k \<le> (n::nat) ==> m \<le> n + m - k"
-by arith
-
-(*Replaces the previous diff_less and le_diff_less, which had the stronger
- second premise n\<le>m*)
-lemma diff_less[simp]: "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"
-by arith
-
-
-(** Simplification of relational expressions involving subtraction **)
-
-lemma diff_diff_eq: "[| k \<le> m; k \<le> (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"
-by (simp split add: nat_diff_split)
-
-lemma eq_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k = n-k) = (m=n)"
-by (auto split add: nat_diff_split)
-
-lemma less_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k < n-k) = (m<n)"
-by (auto split add: nat_diff_split)
-
-lemma le_diff_iff: "[| k \<le> m; k \<le> (n::nat) |] ==> (m-k \<le> n-k) = (m\<le>n)"
-by (auto split add: nat_diff_split)
-
-
-text{*(Anti)Monotonicity of subtraction -- by Stephan Merz*}
-
-(* Monotonicity of subtraction in first argument *)
-lemma diff_le_mono: "m \<le> (n::nat) ==> (m-l) \<le> (n-l)"
-by (simp split add: nat_diff_split)
-
-lemma diff_le_mono2: "m \<le> (n::nat) ==> (l-n) \<le> (l-m)"
-by (simp split add: nat_diff_split)
-
-lemma diff_less_mono2: "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"
-by (simp split add: nat_diff_split)
-
-lemma diffs0_imp_equal: "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n"
-by (simp split add: nat_diff_split)
-
-text{*Lemmas for ex/Factorization*}
-
-lemma one_less_mult: "[| Suc 0 < n; Suc 0 < m |] ==> Suc 0 < m*n"
-by (case_tac "m", auto)
-
-lemma n_less_m_mult_n: "[| Suc 0 < n; Suc 0 < m |] ==> n<m*n"
-by (case_tac "m", auto)
-
-lemma n_less_n_mult_m: "[| Suc 0 < n; Suc 0 < m |] ==> n<n*m"
-by (case_tac "m", auto)
-
-
-text{*Rewriting to pull differences out*}
-
-lemma diff_diff_right [simp]: "k\<le>j --> i - (j - k) = i + (k::nat) - j"
-by arith
-
-lemma diff_Suc_diff_eq1 [simp]: "k \<le> j ==> m - Suc (j - k) = m + k - Suc j"
-by arith
-
-lemma diff_Suc_diff_eq2 [simp]: "k \<le> j ==> Suc (j - k) - m = Suc j - (k + m)"
-by arith
-
-(*The others are
- i - j - k = i - (j + k),
- k \<le> j ==> j - k + i = j + i - k,
- k \<le> j ==> i + (j - k) = i + j - k *)
-lemmas add_diff_assoc = diff_add_assoc [symmetric]
-lemmas add_diff_assoc2 = diff_add_assoc2[symmetric]
-declare diff_diff_left [simp] add_diff_assoc [simp] add_diff_assoc2[simp]
-
-text{*At present we prove no analogue of @{text not_less_Least} or @{text
-Least_Suc}, since there appears to be no need.*}
-
-ML
-{*
-val pred_nat_trancl_eq_le = thm "pred_nat_trancl_eq_le";
-val nat_diff_split = thm "nat_diff_split";
-val nat_diff_split_asm = thm "nat_diff_split_asm";
-val le_square = thm "le_square";
-val le_cube = thm "le_cube";
-val diff_less_mono = thm "diff_less_mono";
-val less_diff_conv = thm "less_diff_conv";
-val le_diff_conv = thm "le_diff_conv";
-val le_diff_conv2 = thm "le_diff_conv2";
-val diff_diff_cancel = thm "diff_diff_cancel";
-val le_add_diff = thm "le_add_diff";
-val diff_less = thm "diff_less";
-val diff_diff_eq = thm "diff_diff_eq";
-val eq_diff_iff = thm "eq_diff_iff";
-val less_diff_iff = thm "less_diff_iff";
-val le_diff_iff = thm "le_diff_iff";
-val diff_le_mono = thm "diff_le_mono";
-val diff_le_mono2 = thm "diff_le_mono2";
-val diff_less_mono2 = thm "diff_less_mono2";
-val diffs0_imp_equal = thm "diffs0_imp_equal";
-val one_less_mult = thm "one_less_mult";
-val n_less_m_mult_n = thm "n_less_m_mult_n";
-val n_less_n_mult_m = thm "n_less_n_mult_m";
-val diff_diff_right = thm "diff_diff_right";
-val diff_Suc_diff_eq1 = thm "diff_Suc_diff_eq1";
-val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
-*}
-
-subsection{*Embedding of the Naturals into any @{text
-semiring_1_cancel}: @{term of_nat}*}
-
-consts of_nat :: "nat => 'a::semiring_1_cancel"
-
-primrec
- of_nat_0: "of_nat 0 = 0"
- of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
-
-lemma of_nat_1 [simp]: "of_nat 1 = 1"
-by simp
-
-lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
-apply (induct m)
-apply (simp_all add: add_ac)
-done
-
-lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
-apply (induct m)
-apply (simp_all add: add_ac left_distrib)
-done
-
-lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
-apply (induct m, simp_all)
-apply (erule order_trans)
-apply (rule less_add_one [THEN order_less_imp_le])
-done
-
-lemma less_imp_of_nat_less:
- "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
-apply (induct m n rule: diff_induct, simp_all)
-apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
-done
-
-lemma of_nat_less_imp_less:
- "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
-apply (induct m n rule: diff_induct, simp_all)
-apply (insert zero_le_imp_of_nat)
-apply (force simp add: linorder_not_less [symmetric])
-done
-
-lemma of_nat_less_iff [simp]:
- "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
-by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
-
-text{*Special cases where either operand is zero*}
-lemmas of_nat_0_less_iff = of_nat_less_iff [of 0, simplified]
-lemmas of_nat_less_0_iff = of_nat_less_iff [of _ 0, simplified]
-declare of_nat_0_less_iff [simp]
-declare of_nat_less_0_iff [simp]
-
-lemma of_nat_le_iff [simp]:
- "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
-by (simp add: linorder_not_less [symmetric])
-
-text{*Special cases where either operand is zero*}
-lemmas of_nat_0_le_iff = of_nat_le_iff [of 0, simplified]
-lemmas of_nat_le_0_iff = of_nat_le_iff [of _ 0, simplified]
-declare of_nat_0_le_iff [simp]
-declare of_nat_le_0_iff [simp]
-
-text{*The ordering on the @{text semiring_1_cancel} is necessary
-to exclude the possibility of a finite field, which indeed wraps back to
-zero.*}
-lemma of_nat_eq_iff [simp]:
- "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
-by (simp add: order_eq_iff)
-
-text{*Special cases where either operand is zero*}
-lemmas of_nat_0_eq_iff = of_nat_eq_iff [of 0, simplified]
-lemmas of_nat_eq_0_iff = of_nat_eq_iff [of _ 0, simplified]
-declare of_nat_0_eq_iff [simp]
-declare of_nat_eq_0_iff [simp]
-
-lemma of_nat_diff [simp]:
- "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::ring_1)"
-by (simp del: of_nat_add
- add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
-
-
-end
--- a/src/HOL/Real/rat_arith.ML Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Real/rat_arith.ML Wed Nov 08 13:48:29 2006 +0100
@@ -48,7 +48,7 @@
neqE = neqE,
simpset = simpset addsimps simps
addsimprocs simprocs}) #>
- arith_inj_const ("NatArith.of_nat", HOLogic.natT --> ratT) #>
+ arith_inj_const ("Nat.of_nat", HOLogic.natT --> ratT) #>
arith_inj_const ("IntDef.of_int", HOLogic.intT --> ratT) #>
(fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy))
--- a/src/HOL/Tools/datatype_package.ML Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Nov 08 13:48:29 2006 +0100
@@ -877,7 +877,7 @@
val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
[descr] sorts thy7;
val (size_thms, thy9) =
- if Context.exists_name "NatArith" thy8 then
+ if Context.exists_name "Nat" thy8 then
DatatypeAbsProofs.prove_size_thms false new_type_names
[descr] sorts reccomb_names rec_thms thy8
else ([], thy8);
--- a/src/HOL/Tools/res_atp.ML Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML Wed Nov 08 13:48:29 2006 +0100
@@ -361,9 +361,9 @@
"Nat.less_one", (*not directional? obscure*)
"Nat.not_gr0",
"Nat.one_eq_mult_iff", (*duplicate by symmetry*)
- "NatArith.of_nat_0_eq_iff",
- "NatArith.of_nat_eq_0_iff",
- "NatArith.of_nat_le_0_iff",
+ "Nat.of_nat_0_eq_iff",
+ "Nat.of_nat_eq_0_iff",
+ "Nat.of_nat_le_0_iff",
"NatSimprocs.divide_le_0_iff_number_of", (*too many clauses*)
"NatSimprocs.divide_less_0_iff_number_of",
"NatSimprocs.equation_minus_iff_1", (*not directional*)
--- a/src/HOL/arith_data.ML Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/arith_data.ML Wed Nov 08 13:48:29 2006 +0100
@@ -61,8 +61,8 @@
let val ss0 = HOL_ss addsimps rules
in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
-val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
-val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
+val add_rules = [thm "add_Suc", thm "add_Suc_right", thm "add_0", thm "add_0_right"];
+val mult_rules = [thm "mult_Suc", thm "mult_Suc_right", thm "mult_0", thm "mult_0_right"];
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (the_context ()) name pats proc;
@@ -104,7 +104,7 @@
open Sum;
val mk_bal = HOLogic.mk_eq;
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac nat_add_left_cancel;
+ val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel");
end);
(* nat less *)
@@ -114,7 +114,7 @@
open Sum;
val mk_bal = HOLogic.mk_binrel "Orderings.less";
val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_less;
+ val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel_less");
end);
(* nat le *)
@@ -124,7 +124,7 @@
open Sum;
val mk_bal = HOLogic.mk_binrel "Orderings.less_eq";
val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac nat_add_left_cancel_le;
+ val uncancel_tac = gen_uncancel_tac (thm "nat_add_left_cancel_le");
end);
(* nat diff *)
@@ -134,7 +134,7 @@
open Sum;
val mk_bal = HOLogic.mk_binop "HOL.minus";
val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT;
- val uncancel_tac = gen_uncancel_tac diff_cancel;
+ val uncancel_tac = gen_uncancel_tac (thm "diff_cancel");
end);
(** prepare nat_cancel simprocs **)
@@ -175,6 +175,7 @@
val sym = sym;
val not_lessD = linorder_not_less RS iffD1;
val not_leD = linorder_not_le RS iffD1;
+val le0 = thm "le0";
fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
@@ -931,10 +932,10 @@
Most of the work is done by the cancel tactics.
*)
val add_rules =
- [add_zero_left,add_zero_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
- One_nat_def,
- order_less_irrefl, zero_neq_one, zero_less_one, zero_le_one,
- zero_neq_one RS not_sym, not_one_le_zero, not_one_less_zero];
+ [thm "add_zero_left", thm "add_zero_right", thm "Zero_not_Suc", thm "Suc_not_Zero",
+ thm "le_0_eq", thm "One_nat_def", thm "order_less_irrefl", thm "zero_neq_one",
+ thm "zero_less_one", thm "zero_le_one", thm "zero_neq_one" RS not_sym, thm "not_one_le_zero",
+ thm "not_one_less_zero"];
val add_mono_thms_ordered_semiring = map (fn s => prove_goal (the_context ()) s
(fn prems => [cut_facts_tac prems 1,
@@ -966,8 +967,8 @@
add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
- lessD = lessD @ [Suc_leI],
- neqE = [linorder_neqE_nat,
+ lessD = lessD @ [thm "Suc_leI"],
+ neqE = [thm "linorder_neqE_nat",
get_thm (theory "Ring_and_Field") (Name "linorder_neqE_ordered_idom")],
simpset = HOL_basic_ss addsimps add_rules
addsimprocs [ab_group_add_cancel.sum_conv,