isabelle: src/Sequents/LK/Nat.thy@11d447d5d68c (annotated)

17481 75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	1	(* Title: Sequents/LK/Nat.thy
7091 b76a26835a5c Sequents/LK/Nat: new example of simplification in LK paulson parents: diff changeset	2	ID: $Id$
b76a26835a5c Sequents/LK/Nat: new example of simplification in LK paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
7095 cfc11af6174a fixed the comments... paulson parents: 7091 diff changeset	4	Copyright 1999 University of Cambridge
7091 b76a26835a5c Sequents/LK/Nat: new example of simplification in LK paulson parents: diff changeset	5	*)
b76a26835a5c Sequents/LK/Nat: new example of simplification in LK paulson parents: diff changeset	6
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	7	header {* Theory of the natural numbers: Peano's axioms, primitive recursion *}
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	8
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	9	theory Nat
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	10	imports LK
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	11	begin
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	12
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	13	typedecl nat
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	14	arities nat :: "term"
7091 b76a26835a5c Sequents/LK/Nat: new example of simplification in LK paulson parents: diff changeset	15	consts "0" :: nat ("0")
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	16	Suc :: "nat=>nat"
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	17	rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	18	"+" :: "[nat, nat] => nat" (infixl 60)
7091 b76a26835a5c Sequents/LK/Nat: new example of simplification in LK paulson parents: diff changeset	19
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	20	axioms
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	21	induct: "[\| $H \|- $E, P(0), $F;
7123 4ab38de3fd20 congruence rule for \|-, etc. paulson parents: 7095 diff changeset	22	!!x. $H, P(x) \|- $E, P(Suc(x)), $F \|] ==> $H \|- $E, P(n), $F"
7095 cfc11af6174a fixed the comments... paulson parents: 7091 diff changeset	23
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	24	Suc_inject: "\|- Suc(m)=Suc(n) --> m=n"
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	25	Suc_neq_0: "\|- Suc(m) ~= 0"
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	26	rec_0: "\|- rec(0,a,f) = a"
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	27	rec_Suc: "\|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	28	add_def: "m+n == rec(m, n, %x y. Suc(y))"
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	29
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	30	ML {* use_legacy_bindings (the_context ()) *}
75166ebb619b converted to Isar theory format; wenzelm parents: 7123 diff changeset	31
7091 b76a26835a5c Sequents/LK/Nat: new example of simplification in LK paulson parents: diff changeset	32	end

author	wenzelm
	Tue, 13 Jun 2006 23:41:39 +0200
changeset 19876	11d447d5d68c
parent 17481	75166ebb619b
child 21426	87ac12bed1ab
permissions	-rw-r--r--