*** empty log message ***
authornipkow
Fri Oct 13 08:28:21 2000 +0200 (2000-10-13)
changeset 1021477349ed89f45
parent 10213 01c2744a3786
child 10215 1ead773b365e
*** empty log message ***
src/HOL/Arithmetic.ML
src/HOL/Arithmetic.thy
src/HOL/Datatype_Universe.thy
src/HOL/Divides.thy
src/HOL/Integ/IntDef.thy
src/HOL/IsaMakefile
src/HOL/NatArith.ML
src/HOL/NatArith.thy
src/HOL/Real/Hyperreal/Series.ML
src/HOL/SetInterval.thy
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
     1.1 --- a/src/HOL/Arithmetic.ML	Thu Oct 12 18:44:35 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,187 +0,0 @@
     1.4 -(*  Title:      HOL/Arithmetic.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1998  University of Cambridge
     1.8 -
     1.9 -Further proofs about elementary arithmetic, using the arithmetic proof
    1.10 -procedures.
    1.11 -*)
    1.12 -
    1.13 -(*legacy ...*)
    1.14 -structure Arithmetic = struct val thy = the_context () end;
    1.15 -
    1.16 -
    1.17 -Goal "m <= m*(m::nat)";
    1.18 -by (induct_tac "m" 1);
    1.19 -by Auto_tac;
    1.20 -qed "le_square";
    1.21 -
    1.22 -Goal "(m::nat) <= m*(m*m)";
    1.23 -by (induct_tac "m" 1);
    1.24 -by Auto_tac;
    1.25 -qed "le_cube";
    1.26 -
    1.27 -
    1.28 -(*** Subtraction laws -- mostly from Clemens Ballarin ***)
    1.29 -
    1.30 -Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
    1.31 -by (arith_tac 1);
    1.32 -qed "diff_less_mono";
    1.33 -
    1.34 -Goal "(i < j-k) = (i+k < (j::nat))";
    1.35 -by (arith_tac 1);
    1.36 -qed "less_diff_conv";
    1.37 -
    1.38 -Goal "(j-k <= (i::nat)) = (j <= i+k)";
    1.39 -by (arith_tac 1);
    1.40 -qed "le_diff_conv";
    1.41 -
    1.42 -Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
    1.43 -by (arith_tac 1);
    1.44 -qed "le_diff_conv2";
    1.45 -
    1.46 -Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
    1.47 -by (arith_tac 1);
    1.48 -qed "Suc_diff_Suc";
    1.49 -
    1.50 -Goal "i <= (n::nat) ==> n - (n - i) = i";
    1.51 -by (arith_tac 1);
    1.52 -qed "diff_diff_cancel";
    1.53 -Addsimps [diff_diff_cancel];
    1.54 -
    1.55 -Goal "k <= (n::nat) ==> m <= n + m - k";
    1.56 -by (arith_tac 1);
    1.57 -qed "le_add_diff";
    1.58 -
    1.59 -Goal "m-1 < n ==> m <= n";
    1.60 -by (arith_tac 1);
    1.61 -qed "pred_less_imp_le";
    1.62 -
    1.63 -Goal "j<=i ==> i - j < Suc i - j";
    1.64 -by (arith_tac 1);
    1.65 -qed "diff_less_Suc_diff";
    1.66 -
    1.67 -Goal "i - j <= Suc i - j";
    1.68 -by (arith_tac 1);
    1.69 -qed "diff_le_Suc_diff";
    1.70 -AddIffs [diff_le_Suc_diff];
    1.71 -
    1.72 -Goal "n - Suc i <= n - i";
    1.73 -by (arith_tac 1);
    1.74 -qed "diff_Suc_le_diff";
    1.75 -AddIffs [diff_Suc_le_diff];
    1.76 -
    1.77 -Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)";
    1.78 -by (arith_tac 1);
    1.79 -qed "le_pred_eq";
    1.80 -
    1.81 -Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)";
    1.82 -by (arith_tac 1);
    1.83 -qed "less_pred_eq";
    1.84 -
    1.85 -(*Replaces the previous diff_less and le_diff_less, which had the stronger
    1.86 -  second premise n<=m*)
    1.87 -Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
    1.88 -by (arith_tac 1);
    1.89 -qed "diff_less";
    1.90 -
    1.91 -Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)";
    1.92 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.93 -qed "diff_add_assoc_diff";
    1.94 -
    1.95 -
    1.96 -(*** Reducing subtraction to addition ***)
    1.97 -
    1.98 -Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
    1.99 -by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.100 -qed_spec_mp "Suc_diff_add_le";
   1.101 -
   1.102 -Goal "i<n ==> n - Suc i < n - i";
   1.103 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.104 -qed "diff_Suc_less_diff";
   1.105 -
   1.106 -Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
   1.107 -by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.108 -qed "if_Suc_diff_le";
   1.109 -
   1.110 -Goal "Suc(m)-n <= Suc(m-n)";
   1.111 -by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.112 -qed "diff_Suc_le_Suc_diff";
   1.113 -
   1.114 -(** Simplification of relational expressions involving subtraction **)
   1.115 -
   1.116 -Goal "[| k <= m;  k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
   1.117 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.118 -qed "diff_diff_eq";
   1.119 -
   1.120 -Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
   1.121 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
   1.122 -qed "eq_diff_iff";
   1.123 -
   1.124 -Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
   1.125 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
   1.126 -qed "less_diff_iff";
   1.127 -
   1.128 -Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
   1.129 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
   1.130 -qed "le_diff_iff";
   1.131 -
   1.132 -
   1.133 -(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
   1.134 -
   1.135 -(* Monotonicity of subtraction in first argument *)
   1.136 -Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
   1.137 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.138 -qed "diff_le_mono";
   1.139 -
   1.140 -Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
   1.141 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.142 -qed "diff_le_mono2";
   1.143 -
   1.144 -Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
   1.145 -by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.146 -qed "diff_less_mono2";
   1.147 -
   1.148 -Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n";
   1.149 -by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.150 -qed "diffs0_imp_equal";
   1.151 -
   1.152 -(** Lemmas for ex/Factorization **)
   1.153 -
   1.154 -Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
   1.155 -by (case_tac "m" 1);
   1.156 -by Auto_tac;
   1.157 -qed "one_less_mult"; 
   1.158 -
   1.159 -Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
   1.160 -by (case_tac "m" 1);
   1.161 -by Auto_tac;
   1.162 -qed "n_less_m_mult_n"; 
   1.163 -
   1.164 -Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
   1.165 -by (case_tac "m" 1);
   1.166 -by Auto_tac;
   1.167 -qed "n_less_n_mult_m"; 
   1.168 -
   1.169 -
   1.170 -(** Rewriting to pull differences out **)
   1.171 -
   1.172 -Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
   1.173 -by (arith_tac 1);
   1.174 -qed "diff_diff_right";
   1.175 -
   1.176 -Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
   1.177 -by (arith_tac 1);
   1.178 -qed "diff_Suc_diff_eq1"; 
   1.179 -
   1.180 -Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
   1.181 -by (arith_tac 1);
   1.182 -qed "diff_Suc_diff_eq2"; 
   1.183 -
   1.184 -(*The others are
   1.185 -      i - j - k = i - (j + k),
   1.186 -      k <= j ==> j - k + i = j + i - k,
   1.187 -      k <= j ==> i + (j - k) = i + j - k *)
   1.188 -Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 
   1.189 -	  diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
   1.190 -
     2.1 --- a/src/HOL/Arithmetic.thy	Thu Oct 12 18:44:35 2000 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,21 +0,0 @@
     2.4 -(*  Title:      HOL/Arithmetic.thy
     2.5 -    ID:         $Id$
     2.6 -
     2.7 -Setup arithmetic proof procedures.
     2.8 -*)
     2.9 -
    2.10 -theory Arithmetic = Nat
    2.11 -files "arith_data.ML":
    2.12 -
    2.13 -setup arith_setup
    2.14 -
    2.15 -(*elimination of `-' on nat*)
    2.16 -lemma nat_diff_split:
    2.17 -    "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
    2.18 -  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
    2.19 -
    2.20 -ML {* val nat_diff_split = thm "nat_diff_split" *}
    2.21 -
    2.22 -lemmas [arith_split] = nat_diff_split split_min split_max
    2.23 -
    2.24 -end
     3.1 --- a/src/HOL/Datatype_Universe.thy	Thu Oct 12 18:44:35 2000 +0200
     3.2 +++ b/src/HOL/Datatype_Universe.thy	Fri Oct 13 08:28:21 2000 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  Could <*> be generalized to a general summation (Sigma)?
     3.5  *)
     3.6  
     3.7 -Datatype_Universe = Arithmetic + Sum_Type +
     3.8 +Datatype_Universe = NatArith + Sum_Type +
     3.9  
    3.10  
    3.11  (** lists, trees will be sets of nodes **)
     4.1 --- a/src/HOL/Divides.thy	Thu Oct 12 18:44:35 2000 +0200
     4.2 +++ b/src/HOL/Divides.thy	Fri Oct 13 08:28:21 2000 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  The division operators div, mod and the divides relation "dvd"
     4.5  *)
     4.6  
     4.7 -Divides = Arithmetic +
     4.8 +Divides = NatArith +
     4.9  
    4.10  (*We use the same class for div and mod;
    4.11    moreover, dvd is defined whenever multiplication is*)
     5.1 --- a/src/HOL/Integ/IntDef.thy	Thu Oct 12 18:44:35 2000 +0200
     5.2 +++ b/src/HOL/Integ/IntDef.thy	Fri Oct 13 08:28:21 2000 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  The integers as equivalence classes over nat*nat.
     5.5  *)
     5.6  
     5.7 -IntDef = Equiv + Arithmetic +
     5.8 +IntDef = Equiv + NatArith +
     5.9  constdefs
    5.10    intrel      :: "((nat * nat) * (nat * nat)) set"
    5.11    "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
     6.1 --- a/src/HOL/IsaMakefile	Thu Oct 12 18:44:35 2000 +0200
     6.2 +++ b/src/HOL/IsaMakefile	Fri Oct 13 08:28:21 2000 +0200
     6.3 @@ -69,7 +69,7 @@
     6.4    $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml \
     6.5    $(SRC)/TFL/rules.sml $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sml \
     6.6    $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sml \
     6.7 -  Arithmetic.ML Arithmetic.thy Calculation.thy Datatype.thy Divides.ML \
     6.8 +  NatArith.ML NatArith.thy Calculation.thy Datatype.thy Divides.ML \
     6.9    Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \
    6.10    HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \
    6.11    Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/NatArith.ML	Fri Oct 13 08:28:21 2000 +0200
     7.3 @@ -0,0 +1,187 @@
     7.4 +(*  Title:      HOL/NatArith.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 +    Copyright   1998  University of Cambridge
     7.8 +
     7.9 +Further proofs about elementary arithmetic, using the arithmetic proof
    7.10 +procedures.
    7.11 +*)
    7.12 +
    7.13 +(*legacy ...*)
    7.14 +structure NatArith = struct val thy = the_context () end;
    7.15 +
    7.16 +
    7.17 +Goal "m <= m*(m::nat)";
    7.18 +by (induct_tac "m" 1);
    7.19 +by Auto_tac;
    7.20 +qed "le_square";
    7.21 +
    7.22 +Goal "(m::nat) <= m*(m*m)";
    7.23 +by (induct_tac "m" 1);
    7.24 +by Auto_tac;
    7.25 +qed "le_cube";
    7.26 +
    7.27 +
    7.28 +(*** Subtraction laws -- mostly from Clemens Ballarin ***)
    7.29 +
    7.30 +Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c";
    7.31 +by (arith_tac 1);
    7.32 +qed "diff_less_mono";
    7.33 +
    7.34 +Goal "(i < j-k) = (i+k < (j::nat))";
    7.35 +by (arith_tac 1);
    7.36 +qed "less_diff_conv";
    7.37 +
    7.38 +Goal "(j-k <= (i::nat)) = (j <= i+k)";
    7.39 +by (arith_tac 1);
    7.40 +qed "le_diff_conv";
    7.41 +
    7.42 +Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
    7.43 +by (arith_tac 1);
    7.44 +qed "le_diff_conv2";
    7.45 +
    7.46 +Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
    7.47 +by (arith_tac 1);
    7.48 +qed "Suc_diff_Suc";
    7.49 +
    7.50 +Goal "i <= (n::nat) ==> n - (n - i) = i";
    7.51 +by (arith_tac 1);
    7.52 +qed "diff_diff_cancel";
    7.53 +Addsimps [diff_diff_cancel];
    7.54 +
    7.55 +Goal "k <= (n::nat) ==> m <= n + m - k";
    7.56 +by (arith_tac 1);
    7.57 +qed "le_add_diff";
    7.58 +
    7.59 +Goal "m-1 < n ==> m <= n";
    7.60 +by (arith_tac 1);
    7.61 +qed "pred_less_imp_le";
    7.62 +
    7.63 +Goal "j<=i ==> i - j < Suc i - j";
    7.64 +by (arith_tac 1);
    7.65 +qed "diff_less_Suc_diff";
    7.66 +
    7.67 +Goal "i - j <= Suc i - j";
    7.68 +by (arith_tac 1);
    7.69 +qed "diff_le_Suc_diff";
    7.70 +AddIffs [diff_le_Suc_diff];
    7.71 +
    7.72 +Goal "n - Suc i <= n - i";
    7.73 +by (arith_tac 1);
    7.74 +qed "diff_Suc_le_diff";
    7.75 +AddIffs [diff_Suc_le_diff];
    7.76 +
    7.77 +Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)";
    7.78 +by (arith_tac 1);
    7.79 +qed "le_pred_eq";
    7.80 +
    7.81 +Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)";
    7.82 +by (arith_tac 1);
    7.83 +qed "less_pred_eq";
    7.84 +
    7.85 +(*Replaces the previous diff_less and le_diff_less, which had the stronger
    7.86 +  second premise n<=m*)
    7.87 +Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
    7.88 +by (arith_tac 1);
    7.89 +qed "diff_less";
    7.90 +
    7.91 +Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)";
    7.92 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    7.93 +qed "diff_add_assoc_diff";
    7.94 +
    7.95 +
    7.96 +(*** Reducing subtraction to addition ***)
    7.97 +
    7.98 +Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
    7.99 +by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
   7.100 +qed_spec_mp "Suc_diff_add_le";
   7.101 +
   7.102 +Goal "i<n ==> n - Suc i < n - i";
   7.103 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   7.104 +qed "diff_Suc_less_diff";
   7.105 +
   7.106 +Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
   7.107 +by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
   7.108 +qed "if_Suc_diff_le";
   7.109 +
   7.110 +Goal "Suc(m)-n <= Suc(m-n)";
   7.111 +by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
   7.112 +qed "diff_Suc_le_Suc_diff";
   7.113 +
   7.114 +(** Simplification of relational expressions involving subtraction **)
   7.115 +
   7.116 +Goal "[| k <= m;  k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)";
   7.117 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   7.118 +qed "diff_diff_eq";
   7.119 +
   7.120 +Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k = n-k) = (m=n)";
   7.121 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
   7.122 +qed "eq_diff_iff";
   7.123 +
   7.124 +Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k < n-k) = (m<n)";
   7.125 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
   7.126 +qed "less_diff_iff";
   7.127 +
   7.128 +Goal "[| k <= m;  k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)";
   7.129 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]));
   7.130 +qed "le_diff_iff";
   7.131 +
   7.132 +
   7.133 +(** (Anti)Monotonicity of subtraction -- by Stephan Merz **)
   7.134 +
   7.135 +(* Monotonicity of subtraction in first argument *)
   7.136 +Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
   7.137 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   7.138 +qed "diff_le_mono";
   7.139 +
   7.140 +Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
   7.141 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   7.142 +qed "diff_le_mono2";
   7.143 +
   7.144 +Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
   7.145 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   7.146 +qed "diff_less_mono2";
   7.147 +
   7.148 +Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==>  m=n";
   7.149 +by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   7.150 +qed "diffs0_imp_equal";
   7.151 +
   7.152 +(** Lemmas for ex/Factorization **)
   7.153 +
   7.154 +Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
   7.155 +by (case_tac "m" 1);
   7.156 +by Auto_tac;
   7.157 +qed "one_less_mult"; 
   7.158 +
   7.159 +Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
   7.160 +by (case_tac "m" 1);
   7.161 +by Auto_tac;
   7.162 +qed "n_less_m_mult_n"; 
   7.163 +
   7.164 +Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
   7.165 +by (case_tac "m" 1);
   7.166 +by Auto_tac;
   7.167 +qed "n_less_n_mult_m"; 
   7.168 +
   7.169 +
   7.170 +(** Rewriting to pull differences out **)
   7.171 +
   7.172 +Goal "k<=j --> i - (j - k) = i + (k::nat) - j";
   7.173 +by (arith_tac 1);
   7.174 +qed "diff_diff_right";
   7.175 +
   7.176 +Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j";
   7.177 +by (arith_tac 1);
   7.178 +qed "diff_Suc_diff_eq1"; 
   7.179 +
   7.180 +Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)";
   7.181 +by (arith_tac 1);
   7.182 +qed "diff_Suc_diff_eq2"; 
   7.183 +
   7.184 +(*The others are
   7.185 +      i - j - k = i - (j + k),
   7.186 +      k <= j ==> j - k + i = j + i - k,
   7.187 +      k <= j ==> i + (j - k) = i + j - k *)
   7.188 +Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 
   7.189 +	  diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2];
   7.190 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/NatArith.thy	Fri Oct 13 08:28:21 2000 +0200
     8.3 @@ -0,0 +1,21 @@
     8.4 +(*  Title:      HOL/NatArith.thy
     8.5 +    ID:         $Id$
     8.6 +
     8.7 +Setup arithmetic proof procedures.
     8.8 +*)
     8.9 +
    8.10 +theory NatArith = Nat
    8.11 +files "arith_data.ML":
    8.12 +
    8.13 +setup arith_setup
    8.14 +
    8.15 +(*elimination of `-' on nat*)
    8.16 +lemma nat_diff_split:
    8.17 +    "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
    8.18 +  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
    8.19 +
    8.20 +ML {* val nat_diff_split = thm "nat_diff_split" *}
    8.21 +
    8.22 +lemmas [arith_split] = nat_diff_split split_min split_max
    8.23 +
    8.24 +end
     9.1 --- a/src/HOL/Real/Hyperreal/Series.ML	Thu Oct 12 18:44:35 2000 +0200
     9.2 +++ b/src/HOL/Real/Hyperreal/Series.ML	Fri Oct 13 08:28:21 2000 +0200
     9.3 @@ -94,7 +94,7 @@
     9.4      [real_minus_add_distrib]));
     9.5  qed "sumr_minus";
     9.6  
     9.7 -context Arithmetic.thy;
     9.8 +context NatArith.thy;
     9.9  
    9.10  Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
    9.11  by (auto_tac (claset() addSDs [not_leE],simpset()));
    10.1 --- a/src/HOL/SetInterval.thy	Thu Oct 12 18:44:35 2000 +0200
    10.2 +++ b/src/HOL/SetInterval.thy	Fri Oct 13 08:28:21 2000 +0200
    10.3 @@ -6,7 +6,7 @@
    10.4  lessThan, greaterThan, atLeast, atMost
    10.5  *)
    10.6  
    10.7 -SetInterval = equalities + Arithmetic + 
    10.8 +SetInterval = equalities + NatArith + 
    10.9  
   10.10  constdefs
   10.11   lessThan    :: "('a::ord) => 'a set"	("(1{.._'(})")
    11.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Oct 12 18:44:35 2000 +0200
    11.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Oct 13 08:28:21 2000 +0200
    11.3 @@ -417,7 +417,7 @@
    11.4      val descr' = flat descr;
    11.5      val recTs = get_rec_types descr' sorts;
    11.6  
    11.7 -    val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
    11.8 +    val size_name = Sign.intern_const (Theory.sign_of (theory "NatArith")) "size";
    11.9      val size_names = replicate (length (hd descr)) size_name @
   11.10        map (Sign.full_name (Theory.sign_of thy1)) (DatatypeProp.indexify_names
   11.11          (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));
    12.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Oct 12 18:44:35 2000 +0200
    12.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Oct 13 08:28:21 2000 +0200
    12.3 @@ -715,7 +715,7 @@
    12.4      val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    12.5        [descr] sorts thy7;
    12.6      val (thy9, size_thms) =
    12.7 -      if exists (equal "Arithmetic") (Sign.stamp_names_of (Theory.sign_of thy8)) then
    12.8 +      if exists (equal "NatArith") (Sign.stamp_names_of (Theory.sign_of thy8)) then
    12.9          DatatypeAbsProofs.prove_size_thms false new_type_names
   12.10            [descr] sorts reccomb_names rec_thms thy8
   12.11        else (thy8, []);
    13.1 --- a/src/HOL/Tools/datatype_prop.ML	Thu Oct 12 18:44:35 2000 +0200
    13.2 +++ b/src/HOL/Tools/datatype_prop.ML	Fri Oct 13 08:28:21 2000 +0200
    13.3 @@ -398,7 +398,7 @@
    13.4      val descr' = flat descr;
    13.5      val recTs = get_rec_types descr' sorts;
    13.6  
    13.7 -    val size_name = Sign.intern_const (Theory.sign_of (theory "Arithmetic")) "size";
    13.8 +    val size_name = Sign.intern_const (Theory.sign_of (theory "NatArith")) "size";
    13.9      val size_names = replicate (length (hd descr)) size_name @
   13.10        map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
   13.11          (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs))));