equal
deleted
inserted
replaced
|
1 (* Title: HOL/Divides.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 The division operators div, mod and the divides relation "dvd" |
|
7 *) |
|
8 |
|
9 Divides = Arith + |
|
10 |
|
11 consts |
|
12 div, mod :: [nat, nat] => nat (infixl 70) |
|
13 dvd :: [nat,nat]=>bool (infixl 70) |
|
14 |
|
15 |
|
16 defs |
|
17 mod_def "m mod n == wfrec (trancl pred_nat) |
|
18 (%f j. if j<n then j else f (j-n)) m" |
|
19 div_def "m div n == wfrec (trancl pred_nat) |
|
20 (%f j. if j<n then 0 else Suc (f (j-n))) m" |
|
21 |
|
22 dvd_def "m dvd n == EX k. n = m*k" |
|
23 |
|
24 end |