isabelle: src/HOL/Nat.thy@a528a716a312 (annotated)

923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	1	(* Title: HOL/Nat.thy
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2	ID: $Id$
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	3	Author: Tobias Nipkow and Lawrence C Paulson
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	5	Type "nat" is a linear order, and a datatype; arithmetic operators + -
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	6	and * (for div, mod and dvd, see theory 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
11451 8abfb4f7bd02 partial restructuring to reduce dependence on Axiom of Choice paulson parents: 11325 diff changeset	9	Nat = NatDef +
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10
11134 8bc06c4202cd added nat as instance of new wellorder axclass oheimb parents: 10435 diff changeset	11	(* type "nat" is a wellfounded linear order, and a datatype *)
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	12
5188 633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	13	rep_datatype nat
5714 b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5499 diff changeset	14	distinct Suc_not_Zero, Zero_not_Suc
b4f2e281a907 Changed syntax of rep_datatype. berghofe parents: 5499 diff changeset	15	inject Suc_Suc_eq
5188 633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	16	induct nat_induct
4104 84433b1ab826 nat datatype_info moved to Nat.thy; wenzelm parents: 3370 diff changeset	17
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: 2541 diff changeset	18	instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
4640 ac6cf9f18653 Congruence rules use == in premises now. nipkow parents: 4613 diff changeset	19	instance nat :: linorder (nat_le_linear)
11134 8bc06c4202cd added nat as instance of new wellorder axclass oheimb parents: 10435 diff changeset	20	instance nat :: wellorder (wf_less)
1660 8cb42cd97579 * empty log message * oheimb parents: 1625 diff changeset	21
10435 b100e8d2c355 added axclass power (from HOL.thy); wenzelm parents: 9436 diff changeset	22	axclass power < term
b100e8d2c355 added axclass power (from HOL.thy); wenzelm parents: 9436 diff changeset	23
3370 5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	24	consts
10435 b100e8d2c355 added axclass power (from HOL.thy); wenzelm parents: 9436 diff changeset	25	power :: ['a::power, nat] => 'a (infixr "^" 80)
3370 5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	26
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	27
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	28	(* arithmetic operators + - and * *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	29
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	30	instance
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	31	nat :: {plus, minus, times, power}
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	32
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	33	(* size of a datatype value; overloaded *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	34	consts size :: 'a => nat
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	35
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	36	primrec
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	37	add_0 "0 + n = n"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	38	add_Suc "Suc m + n = Suc(m + n)"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	39
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	40	primrec
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	41	diff_0 "m - 0 = m"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	42	diff_Suc "m - Suc n = (case m - n of 0 => 0 \| Suc k => k)"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	43
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	44	primrec
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	45	mult_0 "0 * n = 0"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	46	mult_Suc "Suc m * n = n + (m * n)"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	47
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	48	end

author	wenzelm
	Sat, 20 Oct 2001 20:20:41 +0200
changeset 11852	a528a716a312
parent 11451	8abfb4f7bd02
child 12338	de0f4a63baa5
permissions	-rw-r--r--