isabelle: src/ZF/Nat_ZF.thy@fd0d6de380c6 (annotated)

32960 69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width; wenzelm parents: 26056 diff changeset	1	(* Title: ZF/Nat_ZF.thy
26056 6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	2	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	3	Copyright 1994 University of Cambridge
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	4	*)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	5
60770 240563fbf41d isabelle update_cartouches; wenzelm parents: 58871 diff changeset	6	section\<open>The Natural numbers As a Least Fixed Point\<close>
26056 6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	7
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	8	theory Nat_ZF imports OrdQuant Bool begin
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	9
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	10	definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	11	nat :: i where
46953 2b6e55924af3 replacing ":" by "\<in>" paulson parents: 46935 diff changeset	12	"nat == lfp(Inf, %X. {0} \<union> {succ(i). i \<in> X})"
26056 6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	13
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	14	definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	15	quasinat :: "i => o" where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	16	"quasinat(n) == n=0 \| (\<exists>m. n = succ(m))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	17
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	18	definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	19	(Has an unconditional succ case, which is used in "recursor" below.)
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	20	nat_case :: "[i, i=>i, i]=>i" where
46820 c656222c4dc1 mathematical symbols instead of ASCII paulson parents: 45602 diff changeset	21	"nat_case(a,b,k) == THE y. k=0 & y=a \| (\<exists>x. k=succ(x) & y=b(x))"
26056 6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	22
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	23	definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	24	nat_rec :: "[i, i, [i,i]=>i]=>i" where
46820 c656222c4dc1 mathematical symbols instead of ASCII paulson parents: 45602 diff changeset	25	"nat_rec(k,a,b) ==
26056 6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	26	wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	27
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	28	(Internalized relations on the naturals)
46820 c656222c4dc1 mathematical symbols instead of ASCII paulson parents: 45602 diff changeset	29
26056 6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	30	definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	31	Le :: i where
46820 c656222c4dc1 mathematical symbols instead of ASCII paulson parents: 45602 diff changeset	32	"Le == {<x,y>:nat*nat. x \<le> y}"
26056 6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	33
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	34	definition
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	35	Lt :: i where
6a0801279f4c Made theory names in ZF disjoint from HOL theory names to allow loading both developments krauss parents: diff changeset	36	"Lt == {<x, y>:nat*nat. x < y}"
46820 c656222c4dc1 mathematical symbols instead of ASCII paulson parents: 45602 diff changeset	37
26056

author	wenzelm
	Tue, 20 Dec 2016 10:44:36 +0100
changeset 64615	fd0d6de380c6
parent 60770	240563fbf41d
permissions	-rw-r--r--