isabelle: src/HOL/Nat.thy@c97dba47e504 (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
5188 633ec5f6c155 Declaration of type 'nat' as a datatype (this allows usage of berghofe parents: 4640 diff changeset	9	Nat = NatDef + Inductive +
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	10
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	11	(* type "nat" is a linear order, and a datatype *)
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)
1660 8cb42cd97579 * empty log message * oheimb parents: 1625 diff changeset	20
3370 5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	21	consts
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	22	"^" :: ['a::power,nat] => 'a (infixr 80)
5c5fdce3a4e4 Overloading of "^" requires new type class "power", with types "nat" and paulson parents: 2608 diff changeset	23
9436 62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	24
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	25	(* arithmetic operators + - and * *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	26
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	27	instance
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	28	nat :: {plus, minus, times, power}
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	(* size of a datatype value; overloaded *)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	31	consts size :: 'a => nat
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	primrec
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	34	add_0 "0 + n = n"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	35	add_Suc "Suc m + n = Suc(m + n)"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	36
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	37	primrec
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	38	diff_0 "m - 0 = m"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	39	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	40
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	41	primrec
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	42	mult_0 "0 * n = 0"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	43	mult_Suc "Suc m * n = n + (m * n)"
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values; wenzelm parents: 7702 diff changeset	44
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	45	end

author	wenzelm
	Thu, 27 Jul 2000 18:23:12 +0200
changeset 9450	c97dba47e504
parent 9436	62bb04ab4b01
child 10435	b100e8d2c355
permissions	-rw-r--r--