isabelle: src/ZF/Integ/IntDiv.thy@e8c774c12105 (annotated)

9578 ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	1	(* Title: ZF/IntDiv.thy
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	2	ID: $Id$
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	4	Copyright 1999 University of Cambridge
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	5
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	6	The division operators div, mod
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	7	*)
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	8
9955 6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	9	IntDiv = IntArith + OrderArith +
9578 ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	10
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	11	constdefs
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	12	quorem :: "[i,i] => o"
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	13	"quorem == %<a,b> <q,r>.
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	14	a = b$*q $+ r &
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	15	(#0$<b & #0$<=r & r$<b \| ~(#0$<b) & b$<r & r $<= #0)"
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	16
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	17	adjust :: "[i,i,i] => i"
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	18	"adjust(a,b) == %<q,r>. if #0 $<= r$-b then <#2$*q $+ #1,r$-b>
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	19	else <#2$*q,r>"
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	20
ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	21
9955 6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	22	( the division algorithm )
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	23
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	24	constdefs posDivAlg :: "i => i"
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	25	(for the case a>=0, b>0)
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	26	(recdef posDivAlg "inv_image less_than (%(a,b). nat_of(a $- b $+ #1))")
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	27	"posDivAlg(ab) ==
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	28	wfrec(measure(int*int, %<a,b>. nat_of (a $- b $+ #1)),
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	29	ab,
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	30	%<a,b> f. if (a$<b \| b$<=#0) then <#0,a>
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	31	else adjust(a, b, f ` <a,#2$*b>))"
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	32
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	33	(TO BE COMPLETED)
6ed42bcba707 a bit more of division paulson parents: 9883 diff changeset	34
9578 ab26d6c8ebfe new theory Integ/IntDiv and many more monotonicity laws, etc., for the integers paulson parents: diff changeset	35	end

author	wenzelm
	Thu, 30 Nov 2000 20:04:16 +0100
changeset 10548	e8c774c12105
parent 9955	6ed42bcba707
child 11321	01cbbf33779b
permissions	-rw-r--r--