now div and mod are overloaded; dvd is polymorphic
authorpaulson
Thu Jul 01 10:33:50 1999 +0200 (1999-07-01)
changeset 68655577ffe4c2f1
parent 6864 32b5d68196d2
child 6866 f795b63139ec
now div and mod are overloaded; dvd is polymorphic
src/HOL/Divides.ML
src/HOL/Divides.thy
src/HOL/Power.ML
     1.1 --- a/src/HOL/Divides.ML	Thu Jul 01 10:32:57 1999 +0200
     1.2 +++ b/src/HOL/Divides.ML	Thu Jul 01 10:33:50 1999 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  by (simp_tac (simpset() addsimps [mod_def]) 1);
     1.5  qed "mod_eq";
     1.6  
     1.7 -Goal "m<n ==> m mod n = m";
     1.8 +Goal "m<n ==> m mod n = (m::nat)";
     1.9  by (rtac (mod_eq RS wf_less_trans) 1);
    1.10  by (Asm_simp_tac 1);
    1.11  qed "mod_less";
    1.12 @@ -352,7 +352,7 @@
    1.13  Addsimps [dvd_0_right];
    1.14  
    1.15  Goalw [dvd_def] "0 dvd m ==> m = 0";
    1.16 -by (fast_tac (claset() addss simpset()) 1);
    1.17 +by Auto_tac;
    1.18  qed "dvd_0_left";
    1.19  
    1.20  Goalw [dvd_def] "1 dvd k";
    1.21 @@ -360,38 +360,38 @@
    1.22  qed "dvd_1_left";
    1.23  AddIffs [dvd_1_left];
    1.24  
    1.25 -Goalw [dvd_def] "m dvd m";
    1.26 +Goalw [dvd_def] "m dvd (m::nat)";
    1.27  by (blast_tac (claset() addIs [mult_1_right RS sym]) 1);
    1.28  qed "dvd_refl";
    1.29  Addsimps [dvd_refl];
    1.30  
    1.31 -Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
    1.32 +Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd (p::nat)";
    1.33  by (blast_tac (claset() addIs [mult_assoc] ) 1);
    1.34  qed "dvd_trans";
    1.35  
    1.36 -Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m=n";
    1.37 -by (fast_tac (claset() addDs [mult_eq_self_implies_10]
    1.38 -                     addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
    1.39 +Goalw [dvd_def] "[| m dvd n; n dvd m |] ==> m = (n::nat)";
    1.40 +by (force_tac (claset() addDs [mult_eq_self_implies_10],
    1.41 +	       simpset() addsimps [mult_assoc, mult_eq_1_iff]) 1);
    1.42  qed "dvd_anti_sym";
    1.43  
    1.44 -Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m + n)";
    1.45 +Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m+n :: nat)";
    1.46  by (blast_tac (claset() addIs [add_mult_distrib2 RS sym]) 1);
    1.47  qed "dvd_add";
    1.48  
    1.49 -Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n)";
    1.50 +Goalw [dvd_def] "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)";
    1.51  by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
    1.52  qed "dvd_diff";
    1.53  
    1.54 -Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
    1.55 +Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd (m::nat)";
    1.56  by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
    1.57  by (blast_tac (claset() addIs [dvd_add]) 1);
    1.58  qed "dvd_diffD";
    1.59  
    1.60 -Goalw [dvd_def] "k dvd n ==> k dvd (m*n)";
    1.61 +Goalw [dvd_def] "k dvd n ==> k dvd (m*n :: nat)";
    1.62  by (blast_tac (claset() addIs [mult_left_commute]) 1);
    1.63  qed "dvd_mult";
    1.64  
    1.65 -Goal "k dvd m ==> k dvd (m*n)";
    1.66 +Goal "k dvd m ==> k dvd (m*n :: nat)";
    1.67  by (stac mult_commute 1);
    1.68  by (etac dvd_mult 1);
    1.69  qed "dvd_mult2";
    1.70 @@ -415,19 +415,19 @@
    1.71  by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
    1.72  qed "dvd_mod_imp_dvd";
    1.73  
    1.74 -Goalw [dvd_def]  "!!k. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
    1.75 +Goalw [dvd_def]  "!!k::nat. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
    1.76  by (etac exE 1);
    1.77  by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
    1.78  by (Blast_tac 1);
    1.79  qed "dvd_mult_cancel";
    1.80  
    1.81 -Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
    1.82 +Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n :: nat)";
    1.83  by (Clarify_tac 1);
    1.84  by (res_inst_tac [("x","k*ka")] exI 1);
    1.85  by (asm_simp_tac (simpset() addsimps mult_ac) 1);
    1.86  qed "mult_dvd_mono";
    1.87  
    1.88 -Goalw [dvd_def] "(i*j) dvd k ==> i dvd k";
    1.89 +Goalw [dvd_def] "(i*j :: nat) dvd k ==> i dvd k";
    1.90  by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
    1.91  by (Blast_tac 1);
    1.92  qed "dvd_mult_left";
     2.1 --- a/src/HOL/Divides.thy	Thu Jul 01 10:32:57 1999 +0200
     2.2 +++ b/src/HOL/Divides.thy	Thu Jul 01 10:33:50 1999 +0200
     2.3 @@ -1,24 +1,39 @@
     2.4  (*  Title:      HOL/Divides.thy
     2.5      ID:         $Id$
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1993  University of Cambridge
     2.8 +    Copyright   1999  University of Cambridge
     2.9  
    2.10  The division operators div, mod and the divides relation "dvd"
    2.11  *)
    2.12  
    2.13  Divides = Arith +
    2.14  
    2.15 +(*We use the same sort for div and mod;
    2.16 +  moreover, dvd is defined whenever multiplication is*)
    2.17 +axclass
    2.18 +  div < term
    2.19 +
    2.20 +instance
    2.21 +  nat :: {div}
    2.22 +
    2.23  consts
    2.24 -  div, mod  :: [nat, nat] => nat          (infixl 70)
    2.25 -  dvd     :: [nat,nat]=>bool              (infixl 70) 
    2.26 +  div  :: ['a::div, 'a]  => 'a          (infixl 70)
    2.27 +  mod  :: ['a::div, 'a]  => 'a          (infixl 70)
    2.28 +  dvd  :: ['a::times, 'a] => bool       (infixl 70) 
    2.29  
    2.30  
    2.31 +(*Remainder and quotient are defined here by algorithms and later proved to
    2.32 +  satisfy the traditional definition (theorem mod_div_equality)
    2.33 +*)
    2.34  defs
    2.35 +
    2.36    mod_def   "m mod n == wfrec (trancl pred_nat)
    2.37                            (%f j. if j<n then j else f (j-n)) m"
    2.38 +
    2.39    div_def   "m div n == wfrec (trancl pred_nat) 
    2.40                            (%f j. if j<n then 0 else Suc (f (j-n))) m"
    2.41  
    2.42 +(*The definition of dvd is polymorphic!*)
    2.43    dvd_def   "m dvd n == EX k. n = m*k"
    2.44  
    2.45  end
     3.1 --- a/src/HOL/Power.ML	Thu Jul 01 10:32:57 1999 +0200
     3.2 +++ b/src/HOL/Power.ML	Thu Jul 01 10:33:50 1999 +0200
     3.3 @@ -7,9 +7,6 @@
     3.4  Also binomial coefficents
     3.5  *)
     3.6  
     3.7 -
     3.8 -open Power;
     3.9 -
    3.10  (*** Simple laws about Power ***)
    3.11  
    3.12  Goal "!!i::nat. i ^ (j+k) = (i^j) * (i^k)";
    3.13 @@ -27,7 +24,7 @@
    3.14  by (ALLGOALS (asm_simp_tac (simpset() addsimps [zero_less_mult_iff])));
    3.15  qed "zero_less_power";
    3.16  
    3.17 -Goalw [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n";
    3.18 +Goalw [dvd_def] "!!(m::nat) (i::nat). m<=n ==> i^m dvd i^n";
    3.19  by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
    3.20  by (asm_simp_tac (simpset() addsimps [power_add]) 1);
    3.21  by (Blast_tac 1);
    3.22 @@ -40,7 +37,7 @@
    3.23  by (contr_tac 1);
    3.24  qed "power_less_imp_less";
    3.25  
    3.26 -Goal "k^j dvd n --> i<j --> k^i dvd n";
    3.27 +Goal "k^j dvd n --> i<j --> k^i dvd (n::nat)";
    3.28  by (induct_tac "j" 1);
    3.29  by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
    3.30  by (stac mult_commute 1);