src/ZF/Sum.thy
 author clasohm Tue Feb 06 12:27:17 1996 +0100 (1996-02-06 ago) changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 2469 b50b8c0eec01 permissions -rw-r--r--
expanded tabs
 clasohm@1478 ` 1` ```(* Title: ZF/sum.thy ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@1478 ` 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@1478 ` 12` ``` "+" :: [i,i]=>i (infixr 65) ``` clasohm@1401 ` 13` ``` Inl,Inr :: i=>i ``` clasohm@1401 ` 14` ``` case :: [i=>i, i=>i, i]=>i ``` clasohm@1401 ` 15` ``` Part :: [i,i=>i] => i ``` clasohm@0 ` 16` lcp@753 ` 17` ```defs ``` 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>" ``` lcp@1108 ` 21` ``` case_def "case(c,d) == (%. cond(y, d(z), c(z)))" ``` clasohm@0 ` 22` clasohm@0 ` 23` ``` (*operator for selecting out the various summands*) ``` clasohm@1478 ` 24` ``` Part_def "Part(A,h) == {x: A. EX z. x = h(z)}" ``` clasohm@0 ` 25` ```end ```