src/HOL/Divides.thy
author wenzelm
Sat, 27 Oct 2001 00:00:05 +0200
changeset 11954 3d1780208bf3
parent 10789 260fa2c67e3e
child 12338 de0f4a63baa5
permissions -rw-r--r--
made new-style theory; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Divides.thy
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     2
    ID:         $Id$
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
     4
    Copyright   1999  University of Cambridge
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     5
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     6
The division operators div, mod and the divides relation "dvd"
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     7
*)
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     8
10214
77349ed89f45 *** empty log message ***
nipkow
parents: 10212
diff changeset
     9
Divides = NatArith +
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    10
8902
a705822f4e2a replaced {{ }} by { };
wenzelm
parents: 7029
diff changeset
    11
(*We use the same class for div and mod;
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    12
  moreover, dvd is defined whenever multiplication is*)
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    13
axclass
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    14
  div < term
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    15
8961
b547482dd127 installing plus_ac0 for nat
paulson
parents: 8902
diff changeset
    16
instance  nat :: div
b547482dd127 installing plus_ac0 for nat
paulson
parents: 8902
diff changeset
    17
instance  nat :: plus_ac0 (add_commute,add_assoc,add_0)
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    18
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    19
consts
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    20
  div  :: ['a::div, 'a]  => 'a          (infixl 70)
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    21
  mod  :: ['a::div, 'a]  => 'a          (infixl 70)
10789
260fa2c67e3e Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents: 10559
diff changeset
    22
  dvd  :: ['a::times, 'a] => bool       (infixl 50) 
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    23
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    24
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    25
(*Remainder and quotient are defined here by algorithms and later proved to
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    26
  satisfy the traditional definition (theorem mod_div_equality)
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    27
*)
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    28
defs
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    29
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    30
  mod_def   "m mod n == wfrec (trancl pred_nat)
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 6865
diff changeset
    31
                          (%f j. if j<n | n=0 then j else f (j-n)) m"
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    32
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    33
  div_def   "m div n == wfrec (trancl pred_nat) 
7029
08d4eb8500dd new division laws taking advantage of (m div 0) = 0 and (m mod 0) = m
paulson
parents: 6865
diff changeset
    34
                          (%f j. if j<n | n=0 then 0 else Suc (f (j-n))) m"
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    35
6865
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    36
(*The definition of dvd is polymorphic!*)
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    37
  dvd_def   "m dvd n == EX k. n = m*k"
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    38
10559
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10214
diff changeset
    39
(*This definition helps prove the harder properties of div and mod.
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10214
diff changeset
    40
  It is copied from IntDiv.thy; should it be overloaded?*)
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10214
diff changeset
    41
constdefs
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10214
diff changeset
    42
  quorem :: "(nat*nat) * (nat*nat) => bool"
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10214
diff changeset
    43
    "quorem == %((a,b), (q,r)).
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10214
diff changeset
    44
                      a = b*q + r &
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10214
diff changeset
    45
                      (if 0<b then 0<=r & r<b else b<r & r <=0)"
d3fd54fc659b many new div and mod properties (borrowed from Integ/IntDiv)
paulson
parents: 10214
diff changeset
    46
3366
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    47
end