# HG changeset patch
# User paulson
# Date 930818030 -7200
# Node ID 5577ffe4c2f1900fe073fac867a1ba66bbfafc8d
# Parent  32b5d68196d27f165a4fdc287b42e8335af0d170
now div and mod are overloaded; dvd is polymorphic

diff -r 32b5d68196d2 -r 5577ffe4c2f1 src/HOL/Divides.ML
--- 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";
diff -r 32b5d68196d2 -r 5577ffe4c2f1 src/HOL/Divides.thy
--- 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
diff -r 32b5d68196d2 -r 5577ffe4c2f1 src/HOL/Power.ML
--- 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);