src/ZF/Sum.thy
 author lcp Thu May 04 02:01:49 1995 +0200 (1995-05-04 ago) changeset 1108 22b256c8c9fb parent 753 ec86863e87c8 child 1401 0c439768f45c permissions -rw-r--r--
case is defined using pattern-matching
 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` 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 ```