# HG changeset patch
# User paulson
# Date 959097982 -7200
# Node ID 548901d05a0ee88323064718b4298ed434a53966
# Parent  39d0cc787d477d7cccf12db1ed839c66711effa1
added type constraint ::nat because 0 is now overloaded

diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/Arith.ML	Tue May 23 18:06:22 2000 +0200
@@ -12,7 +12,7 @@
 
 (** Difference **)
 
-Goal "0 - n = 0";
+Goal "0 - n = (0::nat)";
 by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_0_eq_0";
@@ -42,7 +42,7 @@
 
 (*** Addition ***)
 
-Goal "m + 0 = m";
+Goal "m + 0 = (m::nat)";
 by (induct_tac "m" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "add_0_right";
@@ -105,42 +105,42 @@
 
 (** Reasoning about m+0=0, etc. **)
 
-Goal "(m+n = 0) = (m=0 & n=0)";
+Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)";
 by (case_tac "m" 1);
 by (Auto_tac);
 qed "add_is_0";
 AddIffs [add_is_0];
 
-Goal "(0 = m+n) = (m=0 & n=0)";
+Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
 by (case_tac "m" 1);
 by (Auto_tac);
 qed "zero_is_add";
 AddIffs [zero_is_add];
 
-Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
+Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
 by (case_tac "m" 1);
 by (Auto_tac);
 qed "add_is_1";
 
-Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
+Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
 by (case_tac "m" 1);
 by (Auto_tac);
 qed "one_is_add";
 
-Goal "(0<m+n) = (0<m | 0<n)";
+Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
 by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
 qed "add_gr_0";
 AddIffs [add_gr_0];
 
 (* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
-Goal "0<n ==> m + (n-1) = (m+n)-1";
+Goal "!!m::nat. 0<n ==> m + (n-1) = (m+n)-1";
 by (case_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
                                       addsplits [nat.split])));
 qed "add_pred";
 Addsimps [add_pred];
 
-Goal "m + n = m ==> n = 0";
+Goal "!!m::nat. m + n = m ==> n = 0";
 by (dtac (add_0_right RS ssubst) 1);
 by (asm_full_simp_tac (simpset() addsimps [add_assoc]
                                  delsimps [add_0_right]) 1);
@@ -270,7 +270,7 @@
 (*** Multiplication ***)
 
 (*right annihilation in product*)
-Goal "m * 0 = 0";
+Goal "!!m::nat. m * 0 = 0";
 by (induct_tac "m" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "mult_0_right";
@@ -324,15 +324,15 @@
 
 bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
 
-Goal "(m*n = 0) = (m=0 | n=0)";
+Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)";
 by (induct_tac "m" 1);
 by (induct_tac "n" 2);
 by (ALLGOALS Asm_simp_tac);
 qed "mult_is_0";
 
-Goal "(0 = m*n) = (0=m | 0=n)";
-by (cut_facts_tac [mult_is_0] 1);
-by (full_simp_tac (simpset() addsimps [eq_commute]) 1);
+Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
+by (stac eq_commute 1 THEN stac mult_is_0 1);
+by Auto_tac;
 qed "zero_is_mult";
 
 Addsimps [mult_is_0, zero_is_mult];
@@ -340,7 +340,7 @@
 
 (*** Difference ***)
 
-Goal "m - m = 0";
+Goal "!!m::nat. m - m = 0";
 by (induct_tac "m" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_self_eq_0";
@@ -432,24 +432,24 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2])));
 qed "le_imp_diff_is_add";
 
-Goal "(m-n = 0) = (m <= n)";
+Goal "!!m::nat. (m-n = 0) = (m <= n)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_is_0_eq";
 
-Goal "(0 = m-n) = (m <= n)";
+Goal "!!m::nat. (0 = m-n) = (m <= n)";
 by (stac (diff_is_0_eq RS sym) 1);
 by (rtac eq_sym_conv 1);
 qed "zero_is_diff_eq";
 Addsimps [diff_is_0_eq, zero_is_diff_eq];
 
-Goal "(0<n-m) = (m<n)";
+Goal "!!m::nat. (0<n-m) = (m<n)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "zero_less_diff";
 Addsimps [zero_less_diff];
 
-Goal "i < j  ==> ? k. 0<k & i+k = j";
+Goal "i < j  ==> ? k::nat. 0<k & i+k = j";
 by (res_inst_tac [("x","j - i")] exI 1);
 by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
 qed "less_imp_add_positive";
@@ -475,7 +475,7 @@
     (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1);
 qed "diff_cancel2";
 
-Goal "n - (n+m) = 0";
+Goal "n - (n+m) = (0::nat)";
 by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_add_0";
@@ -514,19 +514,19 @@
 qed "mult_le_mono";
 
 (*strict, in 1st argument; proof is by induction on k>0*)
-Goal "[| i<j; 0<k |] ==> k*i < k*j";
+Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
 by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
 by (Asm_simp_tac 1);
 by (induct_tac "x" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
 qed "mult_less_mono2";
 
-Goal "[| i<j; 0<k |] ==> i*k < j*k";
+Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
 by (dtac mult_less_mono2 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
 qed "mult_less_mono1";
 
-Goal "(0 < m*n) = (0<m & 0<n)";
+Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)";
 by (induct_tac "m" 1);
 by (case_tac "n" 2);
 by (ALLGOALS Asm_simp_tac);
@@ -549,23 +549,24 @@
 qed "mult_eq_1_iff";
 Addsimps [mult_eq_1_iff];
 
-Goal "0<k ==> (m*k < n*k) = (m<n)";
+Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
 by (safe_tac (claset() addSIs [mult_less_mono1]));
 by (cut_facts_tac [less_linear] 1);
 by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
 qed "mult_less_cancel2";
 
-Goal "0<k ==> (k*m < k*n) = (m<n)";
+Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
 by (dtac mult_less_cancel2 1);
-by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
+by (etac subst 1);
+by (simp_tac (simpset() addsimps [mult_commute]) 1);
 qed "mult_less_cancel1";
 Addsimps [mult_less_cancel1, mult_less_cancel2];
 
-Goal "0<k ==> (m*k <= n*k) = (m<=n)";
+Goal "!!m::nat. 0<k ==> (m*k <= n*k) = (m<=n)";
 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
 qed "mult_le_cancel2";
 
-Goal "0<k ==> (k*m <= k*n) = (m<=n)";
+Goal "!!m::nat. 0<k ==> (k*m <= k*n) = (m<=n)";
 by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
 qed "mult_le_cancel1";
 Addsimps [mult_le_cancel1, mult_le_cancel2];
@@ -580,7 +581,7 @@
 by (rtac Suc_mult_less_cancel1 1);
 qed "Suc_mult_le_cancel1";
 
-Goal "0<k ==> (m*k = n*k) = (m=n)";
+Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)";
 by (cut_facts_tac [less_linear] 1);
 by Safe_tac;
 by (assume_tac 2);
@@ -588,7 +589,7 @@
 by (ALLGOALS Asm_full_simp_tac);
 qed "mult_cancel2";
 
-Goal "0<k ==> (k*m = k*n) = (m=n)";
+Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)";
 by (dtac mult_cancel2 1);
 by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
 qed "mult_cancel1";
@@ -601,7 +602,7 @@
 
 
 (*Lemma for gcd*)
-Goal "m = m*n ==> n=1 | m=0";
+Goal "!!m::nat. m = m*n ==> n=1 | m=0";
 by (dtac sym 1);
 by (rtac disjCI 1);
 by (rtac nat_less_cases 1 THEN assume_tac 2);
@@ -1088,17 +1089,17 @@
 qed "diff_Suc_le_diff";
 AddIffs [diff_Suc_le_diff];
 
-Goal "0 < n ==> (m <= n-1) = (m<n)";
+Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)";
 by (arith_tac 1);
 qed "le_pred_eq";
 
-Goal "0 < n ==> (m-1 < n) = (m<=n)";
+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 "[| 0<n; 0<m |] ==> m - n < m";
+Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m";
 by (arith_tac 1);
 qed "diff_less";
 
@@ -1159,23 +1160,23 @@
 by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
 qed "diff_less_mono2";
 
-Goal "[| m-n = 0; n-m = 0 |] ==>  m=n";
+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 "[| 1<n; 1<m |] ==> 1<m*n";
+Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
 by (case_tac "m" 1);
 by Auto_tac;
 qed "one_less_mult"; 
 
-Goal "[| 1<n; 1<m |] ==> n<m*n";
+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 "[| 1<n; 1<m |] ==> n<n*m";
+Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
 by (case_tac "m" 1);
 by Auto_tac;
 qed "n_less_n_mult_m"; 
diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/Divides.ML	Tue May 23 18:06:22 2000 +0200
@@ -26,12 +26,12 @@
 (** Aribtrary definitions for division by zero.  Useful to simplify 
     certain equations **)
 
-Goal "a div 0 = 0";
+Goal "a div 0 = (0::nat)";
 by (rtac (div_eq RS wf_less_trans) 1);
 by (Asm_simp_tac 1);
 qed "DIVISION_BY_ZERO_DIV";  (*NOT for adding to default simpset*)
 
-Goal "a mod 0 = a";
+Goal "a mod 0 = (a::nat)";
 by (rtac (mod_eq RS wf_less_trans) 1);
 by (Asm_simp_tac 1);
 qed "DIVISION_BY_ZERO_MOD";  (*NOT for adding to default simpset*)
@@ -65,13 +65,13 @@
 by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
 qed "mod_if";
 
-Goal "m mod 1 = 0";
+Goal "m mod 1 = (0::nat)";
 by (induct_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [mod_geq])));
 qed "mod_1";
 Addsimps [mod_1];
 
-Goal "n mod n = 0";
+Goal "n mod n = (0::nat)";
 by (div_undefined_case_tac "n=0" 1);
 by (asm_simp_tac (simpset() addsimps [mod_geq]) 1);
 qed "mod_self";
@@ -117,7 +117,7 @@
 			 mod_mult_distrib]) 1);
 qed "mod_mult_distrib2";
 
-Goal "(m*n) mod n = 0";
+Goal "(m*n) mod n = (0::nat)";
 by (div_undefined_case_tac "n=0" 1);
 by (induct_tac "m" 1);
 by (Asm_simp_tac 1);
@@ -126,7 +126,7 @@
 by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
 qed "mod_mult_self_is_0";
 
-Goal "(n*m) mod n = 0";
+Goal "(n*m) mod n = (0::nat)";
 by (simp_tac (simpset() addsimps [mult_commute, mod_mult_self_is_0]) 1);
 qed "mod_mult_self1_is_0";
 Addsimps [mod_mult_self_is_0, mod_mult_self1_is_0];
@@ -134,7 +134,7 @@
 
 (*** Quotient ***)
 
-Goal "m<n ==> m div n = 0";
+Goal "m<n ==> m div n = (0::nat)";
 by (rtac (div_eq RS wf_less_trans) 1);
 by (Asm_simp_tac 1);
 qed "div_less";
@@ -178,7 +178,7 @@
 qed "div_1";
 Addsimps [div_1];
 
-Goal "0<n ==> n div n = 1";
+Goal "0<n ==> n div n = (1::nat)";
 by (asm_simp_tac (simpset() addsimps [div_geq]) 1);
 qed "div_self";
 
@@ -193,12 +193,12 @@
 by (asm_simp_tac (simpset() addsimps [add_commute, div_add_self2]) 1);
 qed "div_add_self1";
 
-Goal "!!n. 0<n ==> (m + k*n) div n = k + m div n";
+Goal "!!n::nat. 0<n ==> (m + k*n) div n = k + m div n";
 by (induct_tac "k" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [div_add_self1])));
 qed "div_mult_self1";
 
-Goal "0<n ==> (m + n*k) div n = k + m div n";
+Goal "0<n ==> (m + n*k) div n = k + m div (n::nat)";
 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self1]) 1);
 qed "div_mult_self2";
 
@@ -206,12 +206,12 @@
 
 (** A dividend of zero **)
 
-Goal "0 div m = 0";
+Goal "0 div m = (0::nat)";
 by (div_undefined_case_tac "m=0" 1);
 by (Asm_simp_tac 1);
 qed "div_0"; 
 
-Goal "0 mod m = 0";
+Goal "0 mod m = (0::nat)";
 by (div_undefined_case_tac "m=0" 1);
 by (Asm_simp_tac 1);
 qed "mod_0"; 
@@ -234,7 +234,7 @@
 qed_spec_mp "div_le_mono";
 
 (* Antimonotonicity of div in second argument *)
-Goal "[| 0<m; m<=n |] ==> (k div n) <= (k div m)";
+Goal "!!m::nat. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
 by (subgoal_tac "0<n" 1);
  by (Asm_simp_tac 2);
 by (res_inst_tac [("n","k")] less_induct 1);
@@ -261,7 +261,7 @@
 Addsimps [div_le_dividend];
 
 (* Similar for "less than" *)
-Goal "1<n ==> (0 < m) --> (m div n < m)";
+Goal "!!n::nat. 1<n ==> (0 < m) --> (m div n < m)";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (rename_tac "m" 1);
 by (case_tac "m<n" 1);
@@ -296,7 +296,7 @@
 	      simpset() addsimps [Suc_diff_le, diff_less, le_mod_geq]));
 qed "mod_Suc";
 
-Goal "0<n ==> m mod n < n";
+Goal "0<n ==> m mod n < (n::nat)";
 by (res_inst_tac [("n","m")] less_induct 1);
 by (case_tac "na<n" 1);
 (*case n le na*)
@@ -308,18 +308,18 @@
 
 (*** More division laws ***)
 
-Goal "0<n ==> (m*n) div n = m";
+Goal "0<n ==> (m*n) div n = (m::nat)";
 by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
 by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
 qed "div_mult_self_is_m";
 
-Goal "0<n ==> (n*m) div n = m";
+Goal "0<n ==> (n*m) div n = (m::nat)";
 by (asm_simp_tac (simpset() addsimps [mult_commute, div_mult_self_is_m]) 1);
 qed "div_mult_self1_is_m";
 Addsimps [div_mult_self_is_m, div_mult_self1_is_m];
 
 (*Cancellation law for division*)
-Goal "0<k ==> (k*m) div (k*n) = m div n";
+Goal "0<k ==> (k*m) div (k*n) = m div (n::nat)";
 by (div_undefined_case_tac "n=0" 1);
 by (res_inst_tac [("n","m")] less_induct 1);
 by (case_tac "na<n" 1);
@@ -340,16 +340,16 @@
 (** Divides Relation                           **)
 (************************************************)
 
-Goalw [dvd_def] "m dvd 0";
+Goalw [dvd_def] "m dvd (0::nat)";
 by (blast_tac (claset() addIs [mult_0_right RS sym]) 1);
 qed "dvd_0_right";
 AddIffs [dvd_0_right];
 
-Goalw [dvd_def] "0 dvd m ==> m = 0";
+Goalw [dvd_def] "0 dvd m ==> m = (0::nat)";
 by Auto_tac;
 qed "dvd_0_left";
 
-Goalw [dvd_def] "1 dvd k";
+Goalw [dvd_def] "1 dvd (k::nat)";
 by (Simp_tac 1);
 qed "dvd_1_left";
 AddIffs [dvd_1_left];
@@ -404,7 +404,7 @@
 by (rtac dvd_refl 1);
 qed "dvd_reduce";
 
-Goalw [dvd_def] "[| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
+Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
 by (Clarify_tac 1);
 by (Full_simp_tac 1);
 by (res_inst_tac 
@@ -438,7 +438,7 @@
 by (Blast_tac 1);
 qed "dvd_mult_left";
 
-Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= n";
+Goalw [dvd_def] "[| k dvd n; 0 < n |] ==> k <= (n::nat)";
 by (Clarify_tac 1);
 by (ALLGOALS (full_simp_tac (simpset() addsimps [zero_less_mult_iff])));
 by (etac conjE 1);
@@ -448,7 +448,7 @@
 by (Simp_tac 1);
 qed "dvd_imp_le";
 
-Goalw [dvd_def] "(k dvd n) = (n mod k = 0)";
+Goalw [dvd_def] "!!k::nat. (k dvd n) = (n mod k = 0)";
 by (div_undefined_case_tac "k=0" 1);
 by Safe_tac;
 by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/Induct/Multiset0.ML
--- a/src/HOL/Induct/Multiset0.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/Induct/Multiset0.ML	Tue May 23 18:06:22 2000 +0200
@@ -6,6 +6,6 @@
 This theory merely proves that the representation of multisets is nonempty.
 *)
 
-Goal "(%x.0) : {f. finite {x. 0 < f x}}";
+Goal "(%x. (0::nat)) : {f. finite {x. 0 < f x}}";
 by (Simp_tac 1);
 qed "multiset_witness";
diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML	Tue May 23 18:06:22 2000 +0200
@@ -6,8 +6,6 @@
 Binary arithmetic for the natural numbers
 *)
 
-val zcompare_rls = [];
-
 (** nat (coercion from int to nat) **)
 
 Goal "nat (number_of w) = number_of w";
@@ -17,15 +15,15 @@
 
 (*These rewrites should one day be re-oriented...*)
 
-Goal "#0 = 0";
+Goal "#0 = (0::nat)";
 by (simp_tac (simpset_of Int.thy addsimps [nat_0, nat_number_of_def]) 1);
 qed "numeral_0_eq_0";
 
-Goal "#1 = 1";
+Goal "#1 = (1::nat)";
 by (simp_tac (simpset_of Int.thy addsimps [nat_1, nat_number_of_def]) 1);
 qed "numeral_1_eq_1";
 
-Goal "#2 = 2";
+Goal "#2 = (2::nat)";
 by (simp_tac (simpset_of Int.thy addsimps [nat_2, nat_number_of_def]) 1);
 qed "numeral_2_eq_2";
 
@@ -402,26 +400,26 @@
 
 Addsimps [rename_numerals thy card_Pow];
 
-(*** Comparisons involving 0 ***)
+(*** Comparisons involving (0::nat) ***)
 
-Goal "(number_of v = 0) = \
+Goal "(number_of v = (0::nat)) = \
 \     (if neg (number_of v) then True else iszero (number_of v))";
 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
 qed "eq_number_of_0";
 
-Goal "(0 = number_of v) = \
+Goal "((0::nat) = number_of v) = \
 \     (if neg (number_of v) then True else iszero (number_of v))";
 by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
 qed "eq_0_number_of";
 
-Goal "(0 < number_of v) = neg (number_of (bin_minus v))";
+Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
 by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
 qed "less_0_number_of";
 
 (*Simplification already handles n<0, n<=0 and 0<=n.*)
 Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
 
-Goal "neg (number_of v) ==> number_of v = 0";
+Goal "neg (number_of v) ==> number_of v = (0::nat)";
 by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
 qed "neg_imp_number_of_eq_0";
 
diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Tue May 23 18:06:22 2000 +0200
@@ -380,7 +380,7 @@
 (*Now just instantiating n to (number_of v) does the right simplification,
   but with some redundant inequality tests.*)
 
-Goal "neg (number_of (bin_pred v)) = (number_of v = 0)";
+Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
 by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
 by (Asm_simp_tac 1);
 by (stac less_number_of_Suc 1);
@@ -471,7 +471,7 @@
 qed "mod2_Suc_Suc";
 Addsimps [mod2_Suc_Suc];
 
-Goal "(0 < m mod #2) = (m mod #2 = #1)";
+Goal "!!m::nat. (0 < m mod #2) = (m mod #2 = #1)";
 by (subgoal_tac "m mod #2 < #2" 1);
 by (Asm_simp_tac 2);
 by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/Isar_examples/Fibonacci.thy
--- a/src/HOL/Isar_examples/Fibonacci.thy	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy	Tue May 23 18:06:22 2000 +0200
@@ -152,7 +152,7 @@
 theorem fib_gcd: "fib (gcd (m, n)) = gcd (fib m, fib n)" (is "?P m n");
 proof (induct ?P m n rule: gcd_induct);
   fix m; show "fib (gcd (m, 0)) = gcd (fib m, fib 0)"; by simp;
-  fix n; assume n: "0 < n";
+  fix n :: nat; assume n: "0 < n";
   hence "gcd (m, n) = gcd (n, m mod n)"; by (rule gcd_non_0);
   also; assume hyp: "fib ... = gcd (fib n, fib (m mod n))";
   also; from n; have "... = gcd (fib n, fib m)"; by (rule gcd_fib_mod);
diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/Lambda/ListApplication.ML
--- a/src/HOL/Lambda/ListApplication.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.ML	Tue May 23 18:06:22 2000 +0200
@@ -87,9 +87,9 @@
 qed "size_apps";
 Addsimps [size_apps];
 
-Goal "[| 0 < k; m <= n |] ==> m < n+k";
+Goal "[| (0::nat) < k; m <= n |] ==> m < n+k";
 by (fast_arith_tac 1);
-val lemma = result();
+val lemma0 = result();
 
 (* a customized induction schema for $$ *)
 
@@ -107,7 +107,7 @@
  by (Clarify_tac 1);
  by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
  by (Simp_tac 1);
- by (rtac lemma 1);
+ by (rtac lemma0 1);
   by (Force_tac 1);
  by (rtac elem_le_sum 1);
  by (Force_tac 1);
diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/List.ML
--- a/src/HOL/List.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/List.ML	Tue May 23 18:06:22 2000 +0200
@@ -1151,12 +1151,12 @@
 by Auto_tac;
 qed_spec_mp "start_le_sum";
 
-Goal "n : set ns ==> n <= foldl op+ 0 ns";
+Goal "!!n::nat. n : set ns ==> n <= foldl op+ 0 ns";
 by (force_tac (claset() addIs [start_le_sum],
               simpset() addsimps [in_set_conv_decomp]) 1);
 qed "elem_le_sum";
 
-Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
+Goal "!m::nat. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
 by (induct_tac "ns" 1);
 by Auto_tac;
 qed_spec_mp "sum_eq_0_conv";
diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/Power.ML
--- a/src/HOL/Power.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/Power.ML	Tue May 23 18:06:22 2000 +0200
@@ -19,9 +19,9 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [power_add])));
 qed "power_mult";
 
-Goal "0 < i ==> 0 < i^n";
+Goal "!!i::nat. 0 < i ==> 0 < i^n";
 by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff])));
+by (ALLGOALS Asm_simp_tac);
 qed "zero_less_power";
 Addsimps [zero_less_power];
 
@@ -31,13 +31,13 @@
 qed "one_le_power";
 Addsimps [one_le_power];
 
-Goalw [dvd_def] "!!(m::nat) (i::nat). m<=n ==> i^m dvd i^n";
+Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n";
 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
 by (asm_simp_tac (simpset() addsimps [power_add]) 1);
 by (Blast_tac 1);
 qed "le_imp_power_dvd";
 
-Goal "[| 0 < i; i^m < i^n |] ==> m<n";
+Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";
 by (rtac ccontr 1);
 by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
 by (etac zero_less_power 1);
diff -r 39d0cc787d47 -r 548901d05a0e src/HOL/ex/Factorization.ML
--- a/src/HOL/ex/Factorization.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOL/ex/Factorization.ML	Tue May 23 18:06:22 2000 +0200
@@ -9,26 +9,26 @@
 
 (* --- Arithmetic --- *)
 
-Goal "[| m ~= m*k; m ~= 1 |] ==> 1<m";
+Goal "!!m::nat. [| m ~= m*k; m ~= 1 |] ==> 1<m";
 by (case_tac "m" 1);
 by Auto_tac;
 qed "one_less_m";
 
-Goal "[| m ~= m*k; 1<m*k |] ==> 1<k";
+Goal "!!m::nat. [| m ~= m*k; 1<m*k |] ==> 1<k";
 by (case_tac "k" 1);
 by Auto_tac;
 qed "one_less_k";
 
-Goal "[| 0<k; k*n=k*m |] ==> n=m";
+Goal "!!m::nat. [| 0<k; k*n=k*m |] ==> n=m";
 by Auto_tac;
 qed "mult_left_cancel";
 
-Goal "[| 0<m; m*n = m |] ==> n=1";
+Goal "!!m::nat. [| 0<m; m*n = m |] ==> n=1";
 by (case_tac "n" 1);
 by Auto_tac;
 qed "mn_eq_m_one";
 
-Goal "[| 0<n; 0<k |] ==> 1<m --> m*n = k --> n<k";
+Goal "!!m::nat. [| 0<n; 0<k |] ==> 1<m --> m*n = k --> n<k";
 by (induct_tac "m" 1);
 by Auto_tac;
 qed_spec_mp "prod_mn_less_k";
diff -r 39d0cc787d47 -r 548901d05a0e src/HOLCF/Cont.ML
--- a/src/HOLCF/Cont.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOLCF/Cont.ML	Tue May 23 18:06:22 2000 +0200
@@ -3,11 +3,9 @@
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
 
-Lemmas for Cont.thy 
+Results about continuity and monotonicity
 *)
 
-open Cont;
-
 (* ------------------------------------------------------------------------ *)
 (* access to definition                                                     *)
 (* ------------------------------------------------------------------------ *)
@@ -121,7 +119,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "binchain_cont" thy
-"[| cont(f); x << y |]  ==> range(%i. f(if i = 0 then x else y)) <<| f(y)"
+"[| cont(f); x << y |]  ==> range(%i::nat. f(if i = 0 then x else y)) <<| f(y)"
 (fn prems => 
         [
         (cut_facts_tac prems 1),
diff -r 39d0cc787d47 -r 548901d05a0e src/HOLCF/Porder.ML
--- a/src/HOLCF/Porder.ML	Tue May 23 12:44:03 2000 +0200
+++ b/src/HOLCF/Porder.ML	Tue May 23 18:06:22 2000 +0200
@@ -6,8 +6,6 @@
 Lemmas for theory Porder.thy 
 *)
 
-open Porder;
-
 (* ------------------------------------------------------------------------ *)
 (* lubs are unique                                                          *)
 (* ------------------------------------------------------------------------ *)
@@ -241,7 +239,7 @@
         ]);
 
 qed_goal "lub_bin_chain" thy 
-        "x << y ==> range(%i. if (i=0) then x else y) <<| y"
+        "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y"
 (fn prems=>
         [ (cut_facts_tac prems 1),
         (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1),