author  wenzelm 
Tue, 06 Sep 2005 16:59:53 +0200  
changeset 17278  f27456a2a975 
parent 8791  50b650d19641 
child 19802  c2860c37e574 
permissions  rwrr 
1476  1 
(* Title: HOL/Hoare/Arith2.thy 
1335  2 
ID: $Id$ 
1476  3 
Author: Norbert Galm 
1335  4 
Copyright 1995 TUM 
5 

3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
1824
diff
changeset

6 
More arithmetic. Much of this duplicates ex/Primes. 
1335  7 
*) 
8 

17278  9 
theory Arith2 
10 
imports Main 

11 
begin 

1335  12 

1558  13 
constdefs 
17278  14 
"cd" :: "[nat, nat, nat] => bool" 
3372
6e472c8f0011
Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
paulson
parents:
1824
diff
changeset

15 
"cd x m n == x dvd m & x dvd n" 
1335  16 

17278  17 
gcd :: "[nat, nat] => nat" 
1558  18 
"gcd m n == @x.(cd x m n) & (!y.(cd y m n) > y<=x)" 
1335  19 

17278  20 
consts fac :: "nat => nat" 
5183  21 

22 
primrec 

23 
"fac 0 = Suc 0" 

24 
"fac(Suc n) = (Suc n)*fac(n)" 

1335  25 

17278  26 
ML {* use_legacy_bindings (the_context ()) *} 
27 

1335  28 
end 