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

1473 e8d4606e6502 expanded tabs clasohm parents: 1322 diff changeset	1	(* Title: FOL/ex/nat2.thy
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1473 e8d4606e6502 expanded tabs clasohm parents: 1322 diff changeset	3	Author: Tobias Nipkow
352 fd3ab8bcb69d removal of obsolete type-declaration syntax lcp parents: 0 diff changeset	4	Copyright 1994 University of Cambridge
0 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: 1473 diff changeset	7	header {* Theory for examples of simplification and induction on the natural numbers *}
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	8
17245 1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	9	theory Nat2
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	10	imports FOL
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	11	begin
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	12
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	13	typedecl nat
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	14	arities nat :: "term"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	15
352 fd3ab8bcb69d removal of obsolete type-declaration syntax lcp parents: 0 diff changeset	16	consts
17245 1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	17	succ :: "nat => nat"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	18	pred :: "nat => nat"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	19	0 :: nat ("0")
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	20	add :: "[nat,nat] => nat" (infixr "+" 90)
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	21	lt :: "[nat,nat] => o" (infixr "<" 70)
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	22	leq :: "[nat,nat] => o" (infixr "<=" 70)
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	23
17245 1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	24	axioms
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	25	pred_0: "pred(0) = 0"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	26	pred_succ: "pred(succ(m)) = m"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	27
17245 1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	28	plus_0: "0+n = n"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	29	plus_succ: "succ(m)+n = succ(m+n)"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	30
17245 1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	31	nat_distinct1: "~ 0=succ(n)"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	32	nat_distinct2: "~ succ(m)=0"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	33	succ_inject: "succ(m)=succ(n) <-> m=n"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	34
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	35	leq_0: "0 <= n"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	36	leq_succ_succ: "succ(m)<=succ(n) <-> m<=n"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	37	leq_succ_0: "~ succ(m) <= 0"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	38
17245 1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	39	lt_0_succ: "0 < succ(n)"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	40	lt_succ_succ: "succ(m)<succ(n) <-> m<n"
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	41	lt_0: "~ m < 0"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	42
17245 1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	43	nat_ind: "[\| P(0); ALL n. P(n)-->P(succ(n)) \|] ==> All(P)"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	44
17245 1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	45	ML {* use_legacy_bindings (the_context ()) *}
1c519a3cca59 converted to Isar theory format; wenzelm parents: 1473 diff changeset	46
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	47	end

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