# HG changeset patch # User wenzelm # Date 1162990109 -3600 # Node ID afffe1f721431bf19dad53bcb6f55877019bad7f # Parent d73735bb33c1255f3be8005db0152d10645d7a37 removed theory NatArith (now part of Nat); diff -r d73735bb33c1 -r afffe1f72143 doc-src/TutorialI/Types/numerics.tex --- 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 diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Datatype.thy --- 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) diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Hilbert_Choice.thy --- 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 diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Import/HOL/arithmetic.imp --- 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" diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Integ/IntDef.thy --- 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 diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Integ/int_arith1.ML --- 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" diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Nat.thy --- 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: "(\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) \ n = (\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 \ n)" +by (simp add: less_eq reflcl_trancl [symmetric] + del: reflcl_trancl, arith) + +lemma nat_diff_split: + "P(a - b::nat) = ((a P 0) & (ALL d. a = b + d --> P d))" + -- {* elimination of @{text -} on @{text nat} *} + by (cases "a m * (m::nat)" + by (induct m) auto + +lemma le_cube: "(m::nat) \ m * (m * m)" + by (induct m) auto + + +text{*Subtraction laws, mostly by Clemens Ballarin*} + +lemma diff_less_mono: "[| a < (b::nat); c \ 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 \ (i::nat)) = (j \ i+k)" +by arith + +lemma le_diff_conv2: "k \ j ==> (i \ j-k) = (i+k \ (j::nat))" +by arith + +lemma diff_diff_cancel [simp]: "i \ (n::nat) ==> n - (n - i) = i" +by arith + +lemma le_add_diff: "k \ (n::nat) ==> m \ n + m - k" +by arith + +(*Replaces the previous diff_less and le_diff_less, which had the stronger + second premise n\m*) +lemma diff_less[simp]: "!!m::nat. [| 0 m - n < m" +by arith + + +(** Simplification of relational expressions involving subtraction **) + +lemma diff_diff_eq: "[| k \ m; k \ (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)" +by (simp split add: nat_diff_split) + +lemma eq_diff_iff: "[| k \ m; k \ (n::nat) |] ==> (m-k = n-k) = (m=n)" +by (auto split add: nat_diff_split) + +lemma less_diff_iff: "[| k \ m; k \ (n::nat) |] ==> (m-k < n-k) = (m m; k \ (n::nat) |] ==> (m-k \ n-k) = (m\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 \ (n::nat) ==> (m-l) \ (n-l)" +by (simp split add: nat_diff_split) + +lemma diff_le_mono2: "m \ (n::nat) ==> (l-n) \ (l-m)" +by (simp split add: nat_diff_split) + +lemma diff_less_mono2: "[| m < (n::nat); m (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 nj --> i - (j - k) = i + (k::nat) - j" +by arith + +lemma diff_Suc_diff_eq1 [simp]: "k \ j ==> m - Suc (j - k) = m + k - Suc j" +by arith + +lemma diff_Suc_diff_eq2 [simp]: "k \ j ==> Suc (j - k) - m = Suc j - (k + m)" +by arith + +(*The others are + i - j - k = i - (j + k), + k \ j ==> j - k + i = j + i - k, + k \ 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 \ (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 (of_nat n::'a::ordered_semidom)) = (m \ 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 \ 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 diff -r d73735bb33c1 -r afffe1f72143 src/HOL/NatArith.thy --- 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) \ n = (\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 \ n)" -by (simp add: less_eq reflcl_trancl [symmetric] - del: reflcl_trancl, arith) - -lemma nat_diff_split: - "P(a - b::nat) = ((a P 0) & (ALL d. a = b + d --> P d))" - -- {* elimination of @{text -} on @{text nat} *} - by (cases "a m*(m::nat)" -by (induct_tac "m", auto) - -lemma le_cube: "(m::nat) \ m*(m*m)" -by (induct_tac "m", auto) - - -text{*Subtraction laws, mostly by Clemens Ballarin*} - -lemma diff_less_mono: "[| a < (b::nat); c \ 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 \ (i::nat)) = (j \ i+k)" -by arith - -lemma le_diff_conv2: "k \ j ==> (i \ j-k) = (i+k \ (j::nat))" -by arith - -lemma diff_diff_cancel [simp]: "i \ (n::nat) ==> n - (n - i) = i" -by arith - -lemma le_add_diff: "k \ (n::nat) ==> m \ n + m - k" -by arith - -(*Replaces the previous diff_less and le_diff_less, which had the stronger - second premise n\m*) -lemma diff_less[simp]: "!!m::nat. [| 0 m - n < m" -by arith - - -(** Simplification of relational expressions involving subtraction **) - -lemma diff_diff_eq: "[| k \ m; k \ (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)" -by (simp split add: nat_diff_split) - -lemma eq_diff_iff: "[| k \ m; k \ (n::nat) |] ==> (m-k = n-k) = (m=n)" -by (auto split add: nat_diff_split) - -lemma less_diff_iff: "[| k \ m; k \ (n::nat) |] ==> (m-k < n-k) = (m m; k \ (n::nat) |] ==> (m-k \ n-k) = (m\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 \ (n::nat) ==> (m-l) \ (n-l)" -by (simp split add: nat_diff_split) - -lemma diff_le_mono2: "m \ (n::nat) ==> (l-n) \ (l-m)" -by (simp split add: nat_diff_split) - -lemma diff_less_mono2: "[| m < (n::nat); m (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 nj --> i - (j - k) = i + (k::nat) - j" -by arith - -lemma diff_Suc_diff_eq1 [simp]: "k \ j ==> m - Suc (j - k) = m + k - Suc j" -by arith - -lemma diff_Suc_diff_eq2 [simp]: "k \ j ==> Suc (j - k) - m = Suc j - (k + m)" -by arith - -(*The others are - i - j - k = i - (j + k), - k \ j ==> j - k + i = j + i - k, - k \ 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 \ (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 (of_nat n::'a::ordered_semidom)) = (m \ 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 \ 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 diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Real/rat_arith.ML --- 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)) diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Tools/datatype_package.ML --- 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); diff -r d73735bb33c1 -r afffe1f72143 src/HOL/Tools/res_atp.ML --- 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*) diff -r d73735bb33c1 -r afffe1f72143 src/HOL/arith_data.ML --- 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,