--- a/src/HOL/Arithmetic.ML Thu Oct 12 18:44:35 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,187 +0,0 @@
-(* Title: HOL/Arithmetic.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1998 University of Cambridge
-
-Further proofs about elementary arithmetic, using the arithmetic proof
-procedures.
-*)
-
-(*legacy ...*)
-structure Arithmetic = struct val thy = the_context () end;
-
-
-Goal "m <= m*(m::nat)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "le_square";
-
-Goal "(m::nat) <= m*(m*m)";
-by (induct_tac "m" 1);
-by Auto_tac;
-qed "le_cube";
-
-
-(*** Subtraction laws -- mostly from Clemens Ballarin ***)
-
-Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
-by (arith_tac 1);
-qed "diff_less_mono";
-
-Goal "(i < j-k) = (i+k < (j::nat))";
-by (arith_tac 1);
-qed "less_diff_conv";
-
-Goal "(j-k <= (i::nat)) = (j <= i+k)";
-by (arith_tac 1);
-qed "le_diff_conv";
-
-Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
-by (arith_tac 1);
-qed "le_diff_conv2";
-
-Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
-by (arith_tac 1);
-qed "Suc_diff_Suc";
-
-Goal "i <= (n::nat) ==> n - (n - i) = i";
-by (arith_tac 1);
-qed "diff_diff_cancel";
-Addsimps [diff_diff_cancel];
-
-Goal "k <= (n::nat) ==> m <= n + m - k";
-by (arith_tac 1);
-qed "le_add_diff";
-
-Goal "m-1 < n ==> m <= n";
-by (arith_tac 1);
-qed "pred_less_imp_le";
-
-Goal "j<=i ==> i - j < Suc i - j";
-by (arith_tac 1);
-qed "diff_less_Suc_diff";
-
-Goal "i - j <= Suc i - j";
-by (arith_tac 1);
-qed "diff_le_Suc_diff";
-AddIffs [diff_le_Suc_diff];
-
-Goal "n - Suc i <= n - i";
-by (arith_tac 1);
-qed "diff_Suc_le_diff";
-AddIffs [diff_Suc_le_diff];
-
-Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)";
-by (arith_tac 1);
-qed "le_pred_eq";
-
-Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)";
-by (arith_tac 1);
-qed "less_pred_eq";
-
-(*Replaces the previous diff_less and le_diff_less, which had the stronger
- second premise n<=m*)
-Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
-by (arith_tac 1);
-qed "diff_less";
-
-Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_add_assoc_diff";
-
-
-(*** Reducing subtraction to addition ***)
-
-Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
-by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed_spec_mp "Suc_diff_add_le";
-
-Goal "i<n ==> n - Suc i < n - i";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_Suc_less_diff";
-
-Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
-by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "if_Suc_diff_le";
-
-Goal "Suc(m)-n <= Suc(m-n)";
-by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_Suc_le_Suc_diff";
-
-(** Simplification of relational expressions involving subtraction **)
-
-Goal "[| k <= m; k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_diff_eq";
-
-Goal "[| k <= m; k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "eq_diff_iff";
-
-Goal "[| k <= m; k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "less_diff_iff";
-
-Goal "[| k <= m; k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
-by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
-qed "le_diff_iff";
-
-
-(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
-
-(* Monotonicity of subtraction in first argument *)
-Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_le_mono";
-
-Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_le_mono2";
-
-Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
-by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diff_less_mono2";
-
-Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n";
-by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
-qed "diffs0_imp_equal";
-
-(** Lemmas for ex/Factorization **)
-
-Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "one_less_mult";
-
-Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "n_less_m_mult_n";
-
-Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
-by (case_tac "m" 1);
-by Auto_tac;
-qed "n_less_n_mult_m";
-
-
-(** Rewriting to pull differences out **)
-
-Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
-by (arith_tac 1);
-qed "diff_diff_right";
-
-Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
-by (arith_tac 1);
-qed "diff_Suc_diff_eq1";
-
-Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
-by (arith_tac 1);
-qed "diff_Suc_diff_eq2";
-
-(*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 *)
-Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym,
- diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
-
--- a/src/HOL/Arithmetic.thy Thu Oct 12 18:44:35 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(* Title: HOL/Arithmetic.thy
- ID: $Id$
-
-Setup arithmetic proof procedures.
-*)
-
-theory Arithmetic = Nat
-files "arith_data.ML":
-
-setup arith_setup
-
-(*elimination of `-' on nat*)
-lemma nat_diff_split:
- "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
- by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
-
-ML {* val nat_diff_split = thm "nat_diff_split" *}
-
-lemmas [arith_split] = nat_diff_split split_min split_max
-
-end
--- a/src/HOL/Datatype_Universe.thy Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/Datatype_Universe.thy Fri Oct 13 08:28:21 2000 +0200
@@ -9,7 +9,7 @@
Could <*> be generalized to a general summation (Sigma)?
*)
-Datatype_Universe = Arithmetic + Sum_Type +
+Datatype_Universe = NatArith + Sum_Type +
(** lists, trees will be sets of nodes **)
--- a/src/HOL/Divides.thy Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/Divides.thy Fri Oct 13 08:28:21 2000 +0200
@@ -6,7 +6,7 @@
The division operators div, mod and the divides relation "dvd"
*)
-Divides = Arithmetic +
+Divides = NatArith +
(*We use the same class for div and mod;
moreover, dvd is defined whenever multiplication is*)
--- a/src/HOL/Integ/IntDef.thy Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/Integ/IntDef.thy Fri Oct 13 08:28:21 2000 +0200
@@ -6,7 +6,7 @@
The integers as equivalence classes over nat*nat.
*)
-IntDef = Equiv + Arithmetic +
+IntDef = Equiv + NatArith +
constdefs
intrel :: "((nat * nat) * (nat * nat)) set"
"intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
--- a/src/HOL/IsaMakefile Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 13 08:28:21 2000 +0200
@@ -69,7 +69,7 @@
$(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \
$(SRC)/TFL/rules.sml $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sml \
$(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sml \
- Arithmetic.ML Arithmetic.thy Calculation.thy Datatype.thy Divides.ML \
+ NatArith.ML NatArith.thy Calculation.thy Datatype.thy Divides.ML \
Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \
Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NatArith.ML Fri Oct 13 08:28:21 2000 +0200
@@ -0,0 +1,187 @@
+(* Title: HOL/NatArith.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Further proofs about elementary arithmetic, using the arithmetic proof
+procedures.
+*)
+
+(*legacy ...*)
+structure NatArith = struct val thy = the_context () end;
+
+
+Goal "m <= m*(m::nat)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "le_square";
+
+Goal "(m::nat) <= m*(m*m)";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "le_cube";
+
+
+(*** Subtraction laws -- mostly from Clemens Ballarin ***)
+
+Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
+by (arith_tac 1);
+qed "diff_less_mono";
+
+Goal "(i < j-k) = (i+k < (j::nat))";
+by (arith_tac 1);
+qed "less_diff_conv";
+
+Goal "(j-k <= (i::nat)) = (j <= i+k)";
+by (arith_tac 1);
+qed "le_diff_conv";
+
+Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
+by (arith_tac 1);
+qed "le_diff_conv2";
+
+Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
+by (arith_tac 1);
+qed "Suc_diff_Suc";
+
+Goal "i <= (n::nat) ==> n - (n - i) = i";
+by (arith_tac 1);
+qed "diff_diff_cancel";
+Addsimps [diff_diff_cancel];
+
+Goal "k <= (n::nat) ==> m <= n + m - k";
+by (arith_tac 1);
+qed "le_add_diff";
+
+Goal "m-1 < n ==> m <= n";
+by (arith_tac 1);
+qed "pred_less_imp_le";
+
+Goal "j<=i ==> i - j < Suc i - j";
+by (arith_tac 1);
+qed "diff_less_Suc_diff";
+
+Goal "i - j <= Suc i - j";
+by (arith_tac 1);
+qed "diff_le_Suc_diff";
+AddIffs [diff_le_Suc_diff];
+
+Goal "n - Suc i <= n - i";
+by (arith_tac 1);
+qed "diff_Suc_le_diff";
+AddIffs [diff_Suc_le_diff];
+
+Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)";
+by (arith_tac 1);
+qed "le_pred_eq";
+
+Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)";
+by (arith_tac 1);
+qed "less_pred_eq";
+
+(*Replaces the previous diff_less and le_diff_less, which had the stronger
+ second premise n<=m*)
+Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
+by (arith_tac 1);
+qed "diff_less";
+
+Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_add_assoc_diff";
+
+
+(*** Reducing subtraction to addition ***)
+
+Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
+by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed_spec_mp "Suc_diff_add_le";
+
+Goal "i<n ==> n - Suc i < n - i";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_Suc_less_diff";
+
+Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
+by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "if_Suc_diff_le";
+
+Goal "Suc(m)-n <= Suc(m-n)";
+by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_Suc_le_Suc_diff";
+
+(** Simplification of relational expressions involving subtraction **)
+
+Goal "[| k <= m; k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_diff_eq";
+
+Goal "[| k <= m; k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
+qed "eq_diff_iff";
+
+Goal "[| k <= m; k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
+qed "less_diff_iff";
+
+Goal "[| k <= m; k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
+by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
+qed "le_diff_iff";
+
+
+(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
+
+(* Monotonicity of subtraction in first argument *)
+Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_le_mono";
+
+Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_le_mono2";
+
+Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
+by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diff_less_mono2";
+
+Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n";
+by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
+qed "diffs0_imp_equal";
+
+(** Lemmas for ex/Factorization **)
+
+Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
+by (case_tac "m" 1);
+by Auto_tac;
+qed "one_less_mult";
+
+Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
+by (case_tac "m" 1);
+by Auto_tac;
+qed "n_less_m_mult_n";
+
+Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
+by (case_tac "m" 1);
+by Auto_tac;
+qed "n_less_n_mult_m";
+
+
+(** Rewriting to pull differences out **)
+
+Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
+by (arith_tac 1);
+qed "diff_diff_right";
+
+Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
+by (arith_tac 1);
+qed "diff_Suc_diff_eq1";
+
+Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
+by (arith_tac 1);
+qed "diff_Suc_diff_eq2";
+
+(*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 *)
+Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym,
+ diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NatArith.thy Fri Oct 13 08:28:21 2000 +0200
@@ -0,0 +1,21 @@
+(* Title: HOL/NatArith.thy
+ ID: $Id$
+
+Setup arithmetic proof procedures.
+*)
+
+theory NatArith = Nat
+files "arith_data.ML":
+
+setup arith_setup
+
+(*elimination of `-' on nat*)
+lemma nat_diff_split:
+ "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
+ by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
+
+ML {* val nat_diff_split = thm "nat_diff_split" *}
+
+lemmas [arith_split] = nat_diff_split split_min split_max
+
+end
--- a/src/HOL/Real/Hyperreal/Series.ML Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Series.ML Fri Oct 13 08:28:21 2000 +0200
@@ -94,7 +94,7 @@
[real_minus_add_distrib]));
qed "sumr_minus";
-context Arithmetic.thy;
+context NatArith.thy;
Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
by (auto_tac (claset() addSDs [not_leE],simpset()));
--- a/src/HOL/SetInterval.thy Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/SetInterval.thy Fri Oct 13 08:28:21 2000 +0200
@@ -6,7 +6,7 @@
lessThan, greaterThan, atLeast, atMost
*)
-SetInterval = equalities + Arithmetic +
+SetInterval = equalities + NatArith +
constdefs
lessThan :: "('a::ord) => 'a set" ("(1{.._'(})")
--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Fri Oct 13 08:28:21 2000 +0200
@@ -417,7 +417,7 @@
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
- val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
+ val size_name = Sign.intern_const (Theory.sign_of (theory "NatArith")) "size";
val size_names = replicate (length (hd descr)) size_name @
map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
(map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
--- a/src/HOL/Tools/datatype_package.ML Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML Fri Oct 13 08:28:21 2000 +0200
@@ -715,7 +715,7 @@
val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
[descr] sorts thy7;
val (thy9, size_thms) =
- if exists (equal "Arithmetic") (Sign.stamp_names_of (Theory.sign_of thy8)) then
+ if exists (equal "NatArith") (Sign.stamp_names_of (Theory.sign_of thy8)) then
DatatypeAbsProofs.prove_size_thms false new_type_names
[descr] sorts reccomb_names rec_thms thy8
else (thy8, []);
--- a/src/HOL/Tools/datatype_prop.ML Thu Oct 12 18:44:35 2000 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Fri Oct 13 08:28:21 2000 +0200
@@ -398,7 +398,7 @@
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
- val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
+ val size_name = Sign.intern_const (Theory.sign_of (theory "NatArith")) "size";
val size_names = replicate (length (hd descr)) size_name @
map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
(map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));