isabelle: src/FOL/ex/Nat.thy@a8c8ed1c85e0 (annotated)

3115 24ed05500380 tuned comments; wenzelm parents: 1473 diff changeset	1	(* Title: FOL/ex/Nat.thy
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1473 e8d4606e6502 expanded tabs clasohm parents: 1322 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1992 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	6
17245 1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	7	header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	8
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	9	theory Nat
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	10	imports FOL
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	11	begin
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	12
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	13	typedecl nat
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	14	arities nat :: "term"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	15
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	16	consts
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	17	0 :: nat ("0")
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	18	Suc :: "nat => nat"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	19	rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	20	add :: "[nat, nat] => nat" (infixl "+" 60)
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	21
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	22	axioms
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	23	induct: "[\| P(0); !!x. P(x) ==> P(Suc(x)) \|] ==> P(n)"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	24	Suc_inject: "Suc(m)=Suc(n) ==> m=n"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	25	Suc_neq_0: "Suc(m)=0 ==> R"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	26	rec_0: "rec(0,a,f) = a"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	27	rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	28	add_def: "m+n == rec(m, n, %x y. Suc(y))"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	29
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	30	ML {* use_legacy_bindings (the_context ()) *}
1c519a3cca59 converted to Isar theory format; wenzelm parents: 3115 diff changeset	31
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	32	end

author	haftmann
	Wed, 07 Jun 2006 16:54:30 +0200
changeset 19816	a8c8ed1c85e0
parent 17245	1c519a3cca59
child 19819	14de4d05d275
permissions	-rw-r--r--