isabelle: src/HOL/Arith.thy@c7f56322a84b (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
40e5c97e988d pred n -> n-1 nipkow parents: 3366 diff changeset	25	syntax pred :: nat => nat
40e5c97e988d pred n -> n-1 nipkow parents: 3366 diff changeset	26	translations "pred m" => "m - 1"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	27
93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	28	primrec "op *" nat
3366 2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	29	mult_0 "0 * n = 0"
2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	30	mult_Suc "Suc m * n = n + (m * n)"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	31
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	32	end

author	paulson
	Thu, 08 Jan 1998 11:21:45 +0100
changeset 4521	c7f56322a84b
parent 4360	40e5c97e988d
child 4711	75a9ef36b1fe
permissions	-rw-r--r--