isabelle: src/HOL/NatDef.thy@6766aa05e4eb (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
10212 33fe2d701ddd * empty log message * nipkow parents: 8943 diff changeset	11	NatDef = Wellfounded_Recursion +
2608 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
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 11701 diff changeset	15	types ind
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 11701 diff changeset	16	arities ind :: type
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	17
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	18	consts
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	19	Zero_Rep :: ind
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	20	Suc_Rep :: ind => ind
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	21
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	22	rules
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	23	(the axiom of infinity in 2 parts)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	24	inj_Suc_Rep "inj(Suc_Rep)"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	25	Suc_Rep_not_Zero_Rep "Suc_Rep(x) ~= Zero_Rep"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	26
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	27
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	28
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	29	( type nat )
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	30
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	31	(* type definition *)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	32
11326 680ebd093cfe Representing set for type nat is now defined via "inductive". berghofe parents: 10832 diff changeset	33	consts
680ebd093cfe Representing set for type nat is now defined via "inductive". berghofe parents: 10832 diff changeset	34	Nat' :: "ind set"
680ebd093cfe Representing set for type nat is now defined via "inductive". berghofe parents: 10832 diff changeset	35
680ebd093cfe Representing set for type nat is now defined via "inductive". berghofe parents: 10832 diff changeset	36	inductive Nat'
680ebd093cfe Representing set for type nat is now defined via "inductive". berghofe parents: 10832 diff changeset	37	intrs
680ebd093cfe Representing set for type nat is now defined via "inductive". berghofe parents: 10832 diff changeset	38	Zero_RepI "Zero_Rep : Nat'"
680ebd093cfe Representing set for type nat is now defined via "inductive". berghofe parents: 10832 diff changeset	39	Suc_RepI "i : Nat' ==> Suc_Rep i : Nat'"
680ebd093cfe Representing set for type nat is now defined via "inductive". berghofe parents: 10832 diff changeset	40
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 11701 diff changeset	41	global
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 11701 diff changeset	42
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	43	typedef (Nat)
11326 680ebd093cfe Representing set for type nat is now defined via "inductive". berghofe parents: 10832 diff changeset	44	nat = "Nat'" (Nat'.Zero_RepI)
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	45
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	46	instance
11701 3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, wenzelm parents: 11464 diff changeset	47	nat :: {ord, zero, one}
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	48
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	49
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	50	(* abstract constants and syntax *)
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	51
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	52	consts
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	53	Suc :: nat => nat
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	54	pred_nat :: "(nat * nat) set"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	55
3947 eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	56	local
eb707467f8c5 adapted to qualified names; wenzelm parents: 3842 diff changeset	57
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	58	defs
11701 3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, wenzelm parents: 11464 diff changeset	59	Zero_nat_def "0 == Abs_Nat(Zero_Rep)"
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	60	Suc_def "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
11701 3d51fbf81c17 sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, wenzelm parents: 11464 diff changeset	61	One_nat_def "1 == Suc 0"
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	62
7872 2e2d7e80fb07 Removed obsolete comment. berghofe parents: 5187 diff changeset	63	(nat operations)
3236 882e125ed7da New pattern-matching definition of pred_nat paulson parents: 2608 diff changeset	64	pred_nat_def "pred_nat == {(m,n). n = Suc m}"
2608 450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	65
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	66	less_def "m<n == (m,n):trancl(pred_nat)"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	67
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	68	le_def "m<=(n::nat) == ~(n<m)"
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	69
450c9b682a92 New class "order" and accompanying changes. nipkow parents: diff changeset	70	end

author	wenzelm
	Thu, 06 Dec 2001 00:39:40 +0100
changeset 12397	6766aa05e4eb
parent 12338	de0f4a63baa5
permissions	-rw-r--r--