src/HOL/Divides.thy
author berghofe
Tue, 30 May 2000 18:02:49 +0200
changeset 9001 93af64f54bf2
parent 8961 b547482dd127
child 10212 33fe2d701ddd
permissions -rw-r--r--
the is now defined using primrec, avoiding explicit use of arbitrary.
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
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
     9
Divides = Arith +
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)
5577ffe4c2f1 now div and mod are overloaded; dvd is polymorphic
paulson
parents: 3366
diff changeset
    22
  dvd  :: ['a::times, 'a] => bool       (infixl 70) 
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
2402c6ab1561 Moving div and mod from Arith to Divides
paulson
parents:
diff changeset
    39
end