src/ZF/Sum.thy
 author clasohm Tue Nov 16 14:24:21 1993 +0100 (1993-11-16) changeset 124 858ab9a9b047 parent 0 a5a9c433f639 child 753 ec86863e87c8 permissions -rw-r--r--
made pseudo theories for all ML files;
documented dependencies between all thy and ML files
 clasohm@0 ` 1` ```(* Title: ZF/sum.thy ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```Disjoint sums in Zermelo-Fraenkel Set Theory ``` clasohm@0 ` 7` ```"Part" primitive for simultaneous recursive type definitions ``` clasohm@0 ` 8` ```*) ``` clasohm@0 ` 9` clasohm@124 ` 10` ```Sum = Bool + "simpdata" + ``` clasohm@0 ` 11` ```consts ``` clasohm@0 ` 12` ``` "+" :: "[i,i]=>i" (infixr 65) ``` clasohm@0 ` 13` ``` Inl,Inr :: "i=>i" ``` clasohm@0 ` 14` ``` case :: "[i=>i, i=>i, i]=>i" ``` clasohm@0 ` 15` ``` Part :: "[i,i=>i] => i" ``` clasohm@0 ` 16` clasohm@0 ` 17` ```rules ``` clasohm@0 ` 18` ``` sum_def "A+B == {0}*A Un {1}*B" ``` clasohm@0 ` 19` ``` Inl_def "Inl(a) == <0,a>" ``` clasohm@0 ` 20` ``` Inr_def "Inr(b) == <1,b>" ``` clasohm@0 ` 21` ``` case_def "case(c,d) == split(%y z. cond(y, d(z), c(z)))" ``` clasohm@0 ` 22` clasohm@0 ` 23` ``` (*operator for selecting out the various summands*) ``` clasohm@0 ` 24` ``` Part_def "Part(A,h) == {x: A. EX z. x = h(z)}" ``` clasohm@0 ` 25` ```end ```