# HG changeset patch
# User nipkow
# Date 971418501 -7200
# Node ID 77349ed89f4536014e5deee466bf8f5426b4ddfb
# Parent  01c2744a378621dad14341a7a8ef83c1e6812ec3
*** empty log message ***

diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Arithmetic.ML
--- 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];
-
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Arithmetic.thy
--- 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
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Datatype_Universe.thy
--- 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 **)
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Divides.thy
--- 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*)
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Integ/IntDef.thy
--- 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}"
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/IsaMakefile
--- 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 \
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/NatArith.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];
+
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/NatArith.thy
--- /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
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Real/Hyperreal/Series.ML
--- 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()));
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/SetInterval.thy
--- 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{.._'(})")
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Tools/datatype_abs_proofs.ML
--- 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))));
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Tools/datatype_package.ML
--- 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, []);
diff -r 01c2744a3786 -r 77349ed89f45 src/HOL/Tools/datatype_prop.ML
--- 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))));