isabelle: src/HOL/NatDef.thy@fc5773ae2790 (annotated)

2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	1	(* Title: HOL/NatDef.thy
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	2	ID: $Id$
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	3	Author: Tobias Nipkow, Cambridge University Computer Laboratory
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	4	Copyright 1991 University of Cambridge
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	5
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	6	Definition of types ind and nat.
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	7
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	8	Type nat is defined as a set Nat over type ind.
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	9	*)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	10
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	11	NatDef = WF +
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	12
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	13	( type ind )
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	14
3947 eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	15	global
eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	16
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	17	types
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	18	ind
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	19
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	20	arities
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	21	ind :: term
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	22
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	23	consts
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	24	Zero_Rep :: ind
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	25	Suc_Rep :: ind => ind
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	26
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	27	rules
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	28	(the axiom of infinity in 2 parts)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	29	inj_Suc_Rep "inj(Suc_Rep)"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	30	Suc_Rep_not_Zero_Rep "Suc_Rep(x) ~= Zero_Rep"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	31
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	32
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	33
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	34	( type nat )
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	35
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	36	(* type definition *)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	37
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	38	typedef (Nat)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	39	nat = "lfp(%X. {Zero_Rep} Un (Suc_Rep``X))" (lfp_def)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	40
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	41	instance
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	42	nat :: ord
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	43
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	44
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	45	(* abstract constants and syntax *)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	46
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	47	consts
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	48	"0" :: nat ("0")
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	49	Suc :: nat => nat
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	50	nat_case :: ['a, nat => 'a, nat] => 'a
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	51	pred_nat :: "(nat * nat) set"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	52	nat_rec :: ['a, [nat, 'a] => 'a, nat] => 'a
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	53
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	54	syntax
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	55	"1" :: nat ("1")
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	56	"2" :: nat ("2")
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	57
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	58	translations
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	59	"1" == "Suc 0"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	60	"2" == "Suc 1"
3842 b55686a7b22c fixed dots; wenzelm parents: 3236 diff changeset	61	"case p of 0 => a \| Suc y => b" == "nat_case a (%y. b) p"
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	62
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	63
3947 eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	64	local
eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	65
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	66	defs
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	67	Zero_def "0 == Abs_Nat(Zero_Rep)"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	68	Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	69
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	70	(nat operations and recursion)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	71	nat_case_def "nat_case a f n == @z. (n=0 --> z=a)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	72	& (!x. n=Suc x --> z=f(x))"
3236 882e125ed7da New pattern-matching definition of pred_nat paulson parents: 2608 diff changeset	73	pred_nat_def "pred_nat == {(m,n). n = Suc m}"
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	74
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	75	less_def "m<n == (m,n):trancl(pred_nat)"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	76
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	77	le_def "m<=(n::nat) == ~(n<m)"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	78
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	79	nat_rec_def "nat_rec c d ==
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	80	wfrec pred_nat (%f. nat_case c (%m. d m (f m)))"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	81	end

author	oheimb
	Mon, 27 Apr 1998 19:29:19 +0200
changeset 4836	fc5773ae2790
parent 3947	eb707467f8c5
child 5187	55f07169cf5f
permissions	-rw-r--r--