src/ZF/Sum.thy
 author paulson Fri Jan 03 15:01:55 1997 +0100 (1997-01-03 ago) changeset 2469 b50b8c0eec01 parent 1478 2b8c2a7547ab child 3923 c257b82a1200 permissions -rw-r--r--
Implicit simpsets and clasets for FOL and ZF
 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` paulson@2469 ` 10` ```Sum = Bool + pair + ``` 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 ```