Old_HOL: Arith.thy@fd1be45b64bf (annotated)

145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	1	(* Title: HOL/Arith.thy
0 7949f97df77a Initial revision clasohm parents: diff changeset	2	ID: $Id$
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 7949f97df77a Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
7949f97df77a Initial revision clasohm parents: diff changeset	5
7949f97df77a Initial revision clasohm parents: diff changeset	6	Arithmetic operators and their definitions
7949f97df77a Initial revision clasohm parents: diff changeset	7	*)
7949f97df77a Initial revision clasohm parents: diff changeset	8
7949f97df77a Initial revision clasohm parents: diff changeset	9	Arith = Nat +
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	10
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	11	instance
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	12	nat :: {plus, minus, times}
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	13
0 7949f97df77a Initial revision clasohm parents: diff changeset	14	consts
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	15	pred :: "nat => nat"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	16	div, mod :: "[nat, nat] => nat" (infixl 70)
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	17
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	18	defs
21 803ccc4a83bb added pred: nat=>nat nipkow parents: 0 diff changeset	19	pred_def "pred(m) == nat_rec(m, 0, %n r.n)"
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	20	add_def "m+n == nat_rec(m, n, %u v. Suc(v))"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	21	diff_def "m-n == nat_rec(n, m, %u v. pred(v))"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	22	mult_def "m*n == nat_rec(m, 0, %u v. n + v)"
a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	23	mod_def "m mod n == wfrec(trancl(pred_nat), m, %j f. if(j<n, j, f(j-n)))"
0 7949f97df77a Initial revision clasohm parents: diff changeset	24	div_def "m div n == wfrec(trancl(pred_nat), m, %j f. if(j<n, 0, Suc(f(j-n))))"
7949f97df77a Initial revision clasohm parents: diff changeset	25	end
7949f97df77a Initial revision clasohm parents: diff changeset	26
7949f97df77a Initial revision clasohm parents: diff changeset	27	(*"Difference" is subtraction of natural numbers.
7949f97df77a Initial revision clasohm parents: diff changeset	28	There are no negative numbers; we have
7949f97df77a Initial revision clasohm parents: diff changeset	29	m - n = 0 iff m<=n and m - n = Suc(k) iff m>n.
7949f97df77a Initial revision clasohm parents: diff changeset	30	Also, nat_rec(m, 0, %z w.z) is pred(m). *)
145 a9f7ff3a464c minor cleanup, added 'axclass', 'instance', 'syntax', 'defs' sections; wenzelm parents: 77 diff changeset	31

author	clasohm
	Wed, 02 Nov 1994 11:50:09 +0100
changeset 156	fd1be45b64bf
parent 145	a9f7ff3a464c
permissions	-rw-r--r--