isabelle: src/HOL/Arith.thy@2402c6ab1561 (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
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	14	consts
1370 7361ac9b024d removed quotes from types in consts and syntax sections clasohm parents: 972 diff changeset	15	pred :: nat => nat
3308 da002cef7090 Added overloaded function `size' for all datatypes. nipkow parents: 3235 diff changeset	16	(* size of a datatype value; overloaded *)
da002cef7090 Added overloaded function `size' for all datatypes. nipkow parents: 3235 diff changeset	17	size :: 'a => nat
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	18
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	19	defs
2099 c5f004bfcbab Defined pred using nat_case rather than nat_rec. nipkow parents: 1824 diff changeset	20	pred_def "pred(m) == case m of 0 => 0 \| Suc n => n"
1796 c42db9ab8728 Tidied spacing paulson parents: 1475 diff changeset	21
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	22	primrec "op +" nat
3366 2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	23	add_0 "0 + n = n"
2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	24	add_Suc "Suc m + n = Suc(m + n)"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	25
93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	26	primrec "op -" nat
3235 351565b7321b The diff laws must be named: we do "Delsimps [diff_Suc];" paulson parents: 2887 diff changeset	27	diff_0 "m - 0 = m"
351565b7321b The diff laws must be named: we do "Delsimps [diff_Suc];" paulson parents: 2887 diff changeset	28	diff_Suc "m - Suc n = pred(m - n)"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	29
93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	30	primrec "op *" nat
3366 2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	31	mult_0 "0 * n = 0"
2402c6ab1561 Moving div and mod from Arith to Divides paulson parents: 3308 diff changeset	32	mult_Suc "Suc m * n = n + (m * n)"
2681 93ed51a91622 definitions of +,-,* replaced by primrec definitions pusch parents: 2099 diff changeset	33
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	34	end

author	paulson
	Fri, 30 May 1997 15:15:57 +0200
changeset 3366	2402c6ab1561
parent 3308	da002cef7090
child 4360	40e5c97e988d
permissions	-rw-r--r--