isabelle: src/HOL/Arith.thy@585fa380df1a (annotated)

923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	1	(* Title: HOL/Arith.thy
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
3366 2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	6	Arithmetic operators + - and * (for div, mod and dvd, see Divides)
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	7	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	8
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	9	Arith = Nat +
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	11	instance
3366 2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	12	nat :: {plus, minus, times, power}
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	13
4360 40e5c97e988d pred n -> n-1 nipkow parents: 3366 diff changeset	14	(* size of a datatype value; overloaded *)
40e5c97e988d pred n -> n-1 nipkow parents: 3366 diff changeset	15	consts size :: 'a => nat
1796 c42db9ab8728 Tidied spacing paulson parents: 1475 diff changeset	16
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	17	primrec "op +" nat
3366 2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	18	add_0 "0 + n = n"
2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	19	add_Suc "Suc m + n = Suc(m + n)"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	20
93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	21	primrec "op -" nat
3235 351565b7321b The diff laws must be named: we do "Delsimps [diff_Suc];" paulson parents: 2887 diff changeset	22	diff_0 "m - 0 = m"
4360 40e5c97e988d pred n -> n-1 nipkow parents: 3366 diff changeset	23	diff_Suc "m - Suc n = (case m - n of 0 => 0 \| Suc k => k)"
40e5c97e988d pred n -> n-1 nipkow parents: 3366 diff changeset	24
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	25	primrec "op *" nat
3366 2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	26	mult_0 "0 * n = 0"
2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	27	mult_Suc "Suc m * n = n + (m * n)"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	28
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	29	end

author	wenzelm
	Thu, 18 Jun 1998 10:52:34 +0200
changeset 5047	585fa380df1a
parent 4711	75a9ef36b1fe
child 5183	89f162de39cf
permissions	-rw-r--r--