src/ZF/nat.thy
author lcp
Fri Sep 17 16:16:38 1993 +0200 (1993-09-17)
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 124 858ab9a9b047
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not
involving local assumptions. NB the congruence rules for Sigma and Pi
(dependent type constructions) cause difficulties and are not used by
default.
clasohm@0
     1
(*  Title: 	ZF/nat.thy
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Natural numbers in Zermelo-Fraenkel Set Theory 
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
Nat = Ord + Bool + 
clasohm@0
    10
consts
clasohm@0
    11
    nat 	::      "i"
lcp@6
    12
    nat_case    ::      "[i, i=>i, i]=>i"
clasohm@0
    13
    nat_rec     ::      "[i, i, [i,i]=>i]=>i"
clasohm@0
    14
clasohm@0
    15
rules
clasohm@0
    16
clasohm@0
    17
    nat_def     "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
clasohm@0
    18
clasohm@0
    19
    nat_case_def
lcp@6
    20
	"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
clasohm@0
    21
clasohm@0
    22
    nat_rec_def
clasohm@0
    23
	"nat_rec(k,a,b) ==   \
lcp@6
    24
\   	  wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
clasohm@0
    25
clasohm@0
    26
end