isabelle: src/CTT/Arith.thy@df77edc4f5d0 (annotated)

1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	1	(* Title: CTT/arith
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1991 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Arithmetic operators and their definitions
a5a9c433f639 Initial revision clasohm parents: diff changeset	7
a5a9c433f639 Initial revision clasohm parents: diff changeset	8	Proves about elementary arithmetic: addition, multiplication, etc.
a5a9c433f639 Initial revision clasohm parents: diff changeset	9	Tests definitions and simplifier.
a5a9c433f639 Initial revision clasohm parents: diff changeset	10	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	11
a5a9c433f639 Initial revision clasohm parents: diff changeset	12	Arith = CTT +
a5a9c433f639 Initial revision clasohm parents: diff changeset	13
1474 3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	14	consts "#+","-","\|-\|" :: "[i,i]=>i" (infixr 65)
3f7d67927fe2 expanded tabs clasohm parents: 0 diff changeset	15	"#*",div,mod :: "[i,i]=>i" (infixr 70)
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	16
12110 f8b4b11cd79d eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 10467 diff changeset	17	syntax (xsymbols)
10467 e6e7205e9e91 x-symbol support for Pi, Sigma, -->, : (membership) paulson parents: 3837 diff changeset	18	"op #*" :: [i, i] => i (infixr "#\\<times>" 70)
e6e7205e9e91 x-symbol support for Pi, Sigma, -->, : (membership) paulson parents: 3837 diff changeset	19
e6e7205e9e91 x-symbol support for Pi, Sigma, -->, : (membership) paulson parents: 3837 diff changeset	20	syntax (HTML output)
e6e7205e9e91 x-symbol support for Pi, Sigma, -->, : (membership) paulson parents: 3837 diff changeset	21	"op #*" :: [i, i] => i (infixr "#\\<times>" 70)
e6e7205e9e91 x-symbol support for Pi, Sigma, -->, : (membership) paulson parents: 3837 diff changeset	22
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	23	rules
3837 d7f033c74b38 fixed dots; wenzelm parents: 1474 diff changeset	24	add_def "a#+b == rec(a, b, %u v. succ(v))"
d7f033c74b38 fixed dots; wenzelm parents: 1474 diff changeset	25	diff_def "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	26	absdiff_def "a\|-\|b == (a-b) #+ (b-a)"
a5a9c433f639 Initial revision clasohm parents: diff changeset	27	mult_def "a#*b == rec(a, 0, %u v. b #+ v)"
3837 d7f033c74b38 fixed dots; wenzelm parents: 1474 diff changeset	28	mod_def "a mod b == rec(a, 0, %u v. rec(succ(v) \|-\| b, 0, %x y. succ(v)))"
d7f033c74b38 fixed dots; wenzelm parents: 1474 diff changeset	29	div_def "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	30	end

author	obua
	Fri, 16 Sep 2005 21:02:15 +0200
changeset 17440	df77edc4f5d0
parent 12110	f8b4b11cd79d
child 17441	5b5feca0344a
permissions	-rw-r--r--