isabelle: src/HOL/Hoare/Arith2.thy@47c7490c74fe (annotated)

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	1	(* Title: HOL/Hoare/Arith2.thy
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	3	Author: Norbert Galm
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	4	Copyright 1995 TUM
5e1c0540f285 New directory. nipkow parents: diff changeset	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 5e1c0540f285 New directory. nipkow parents: diff changeset	7	*)
5e1c0540f285 New directory. nipkow parents: diff changeset	8
3372 6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs paulson parents: 1824 diff changeset	9	Arith2 = Divides +
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	10
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	11	constdefs
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	12	cd :: [nat, nat, nat] => bool
3372 6e472c8f0011 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs paulson parents: 1824 diff changeset	13	"cd x m n == x dvd m & x dvd n"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	14
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	15	gcd :: [nat, nat] => nat
9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	16	"gcd m n == @x.(cd x m n) & (!y.(cd y m n) --> y<=x)"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	17
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	18	pow :: [nat, nat] => nat (infixl 75)
3842 b55686a7b22c fixed dots; wenzelm parents: 3372 diff changeset	19	"m pow n == nat_rec (Suc 0) (%u v. m*v) n"
1558 9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	20
9c6ebfab4e05 added constdefs section clasohm parents: 1476 diff changeset	21	fac :: nat => nat
1824 44254696843a Changed argument order of nat_rec. berghofe parents: 1558 diff changeset	22	"fac m == nat_rec (Suc 0) (%u v.(Suc u)*v) m"
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	23
5e1c0540f285 New directory. nipkow parents: diff changeset	24	end

author	paulson
	Wed, 05 Nov 1997 13:29:47 +0100
changeset 4158	47c7490c74fe
parent 3842	b55686a7b22c
child 4359	6f2986464280
permissions	-rw-r--r--