src/ZF/Sum.thy
 author clasohm Sat Dec 09 13:36:11 1995 +0100 (1995-12-09) changeset 1401 0c439768f45c parent 1108 22b256c8c9fb child 1478 2b8c2a7547ab permissions -rw-r--r--
removed quotes from consts and syntax sections
 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@1401 ` 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@0 ` 24` ``` Part_def "Part(A,h) == {x: A. EX z. x = h(z)}" ``` clasohm@0 ` 25` ```end ```