--- 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";
--- 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);
--- 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";
--- 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";
--- 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]));
--- 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);
--- 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);
--- 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";
--- 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);
--- 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";
--- 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),
--- 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),