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 ```