isabelle: src/HOL/Arith.thy@8c937127fd8c (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
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4711 diff changeset	17	primrec
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
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4711 diff changeset	21	primrec
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
5183 89f162de39cf Adapted to new datatype package. berghofe parents: 4711 diff changeset	25	primrec
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	paulson
	Tue, 03 Aug 1999 13:15:54 +0200
changeset 7165	8c937127fd8c
parent 5183	89f162de39cf
child 8929	4829556a56f8
permissions	-rw-r--r--