--- a/src/HOL/Divides.ML Thu Jul 01 10:32:57 1999 +0200
+++ b/src/HOL/Divides.ML Thu Jul 01 10:33:50 1999 +0200
@@ -19,7 +19,7 @@
by (simp_tac (simpset() addsimps [mod_def]) 1);
qed "mod_eq";
-Goal "m<n ==> m mod n = m";
+Goal "m<n ==> m mod n = (m::nat)";
by (rtac (mod_eq RS wf_less_trans) 1);
by (Asm_simp_tac 1);
qed "mod_less";
@@ -352,7 +352,7 @@
Addsimps [dvd_0_right];
Goalw [dvd_def] "0 dvd m ==> m = 0";
-by (fast_tac (claset() addss simpset()) 1);
+by Auto_tac;
qed "dvd_0_left";
Goalw [dvd_def] "1 dvd k";
@@ -360,38 +360,38 @@
qed "dvd_1_left";
AddIffs [dvd_1_left];
-Goalw [dvd_def] "m dvd m";
+Goalw [dvd_def] "m dvd (m::nat)";
by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
qed "dvd_refl";
Addsimps [dvd_refl];
-Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
+Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)";
by (blast_tac (claset() addIs [mult_assoc] ) 1);
qed "dvd_trans";
-Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
-by (fast_tac (claset() addDs [mult_eq_self_implies_10]
- addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
+Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m = (n::nat)";
+by (force_tac (claset() addDs [mult_eq_self_implies_10],
+ simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1);
qed "dvd_anti_sym";
-Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m + n)";
+Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)";
by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
qed "dvd_add";
-Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n)";
+Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)";
by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
qed "dvd_diff";
-Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
+Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd (m::nat)";
by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
by (blast_tac (claset() addIs [dvd_add]) 1);
qed "dvd_diffD";
-Goalw [dvd_def] "k dvd n ==> k dvd (m*n)";
+Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)";
by (blast_tac (claset() addIs [mult_left_commute]) 1);
qed "dvd_mult";
-Goal "k dvd m ==> k dvd (m*n)";
+Goal "k dvd m ==> k dvd (m*n :: nat)";
by (stac mult_commute 1);
by (etac dvd_mult 1);
qed "dvd_mult2";
@@ -415,19 +415,19 @@
by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
qed "dvd_mod_imp_dvd";
-Goalw [dvd_def] "!!k. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
+Goalw [dvd_def] "!!k::nat. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
by (etac exE 1);
by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
by (Blast_tac 1);
qed "dvd_mult_cancel";
-Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
+Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n :: nat)";
by (Clarify_tac 1);
by (res_inst_tac [("x","k*ka")] exI 1);
by (asm_simp_tac (simpset() addsimps mult_ac) 1);
qed "mult_dvd_mono";
-Goalw [dvd_def] "(i*j) dvd k ==> i dvd k";
+Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k";
by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
by (Blast_tac 1);
qed "dvd_mult_left";
--- a/src/HOL/Divides.thy Thu Jul 01 10:32:57 1999 +0200
+++ b/src/HOL/Divides.thy Thu Jul 01 10:33:50 1999 +0200
@@ -1,24 +1,39 @@
(* Title: HOL/Divides.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1999 University of Cambridge
The division operators div, mod and the divides relation "dvd"
*)
Divides = Arith +
+(*We use the same sort for div and mod;
+ moreover, dvd is defined whenever multiplication is*)
+axclass
+ div < term
+
+instance
+ nat :: {div}
+
consts
- div, mod :: [nat, nat] => nat (infixl 70)
- dvd :: [nat,nat]=>bool (infixl 70)
+ div :: ['a::div, 'a] => 'a (infixl 70)
+ mod :: ['a::div, 'a] => 'a (infixl 70)
+ dvd :: ['a::times, 'a] => bool (infixl 70)
+(*Remainder and quotient are defined here by algorithms and later proved to
+ satisfy the traditional definition (theorem mod_div_equality)
+*)
defs
+
mod_def "m mod n == wfrec (trancl pred_nat)
(%f j. if j<n then j else f (j-n)) m"
+
div_def "m div n == wfrec (trancl pred_nat)
(%f j. if j<n then 0 else Suc (f (j-n))) m"
+(*The definition of dvd is polymorphic!*)
dvd_def "m dvd n == EX k. n = m*k"
end
--- a/src/HOL/Power.ML Thu Jul 01 10:32:57 1999 +0200
+++ b/src/HOL/Power.ML Thu Jul 01 10:33:50 1999 +0200
@@ -7,9 +7,6 @@
Also binomial coefficents
*)
-
-open Power;
-
(*** Simple laws about Power ***)
Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
@@ -27,7 +24,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff])));
qed "zero_less_power";
-Goalw [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n";
+Goalw [dvd_def] "!!(m::nat) (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);
@@ -40,7 +37,7 @@
by (contr_tac 1);
qed "power_less_imp_less";
-Goal "k^j dvd n --> i<j --> k^i dvd n";
+Goal "k^j dvd n --> i<j --> k^i dvd (n::nat)";
by (induct_tac "j" 1);
by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
by (stac mult_commute 1);