ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
the keyword "inductive" making the theory file fail
ZF/Makefile: now has Inductive.thy,.ML
ZF/Datatype,Finite,Zorn: depend upon Inductive
ZF/intr_elim: now checks that the inductive name does not clash with
existing theory names
ZF/ind_section: deleted things replicated in Pure/section_utils.ML
ZF/ROOT: now loads Pure/section_utils
(* Title: ZF/sum.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Disjoint sums in Zermelo-Fraenkel Set Theory
"Part" primitive for simultaneous recursive type definitions
*)
Sum = Bool + "simpdata" +
consts
"+" :: "[i,i]=>i" (infixr 65)
Inl,Inr :: "i=>i"
case :: "[i=>i, i=>i, i]=>i"
Part :: "[i,i=>i] => i"
rules
sum_def "A+B == {0}*A Un {1}*B"
Inl_def "Inl(a) == <0,a>"
Inr_def "Inr(b) == <1,b>"
case_def "case(c,d) == split(%y z. cond(y, d(z), c(z)))"
(*operator for selecting out the various summands*)
Part_def "Part(A,h) == {x: A. EX z. x = h(z)}"
end