src/ZF/Sum.thy
changeset 13356 c9cfe1638bf2
parent 13255 407ad9c3036d
child 13823 d49ffd9f9662
     1.1 --- a/src/ZF/Sum.thy	Sun Jul 14 15:11:21 2002 +0200
     1.2 +++ b/src/ZF/Sum.thy	Sun Jul 14 15:14:43 2002 +0200
     1.3 @@ -3,12 +3,14 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1993  University of Cambridge
     1.6  
     1.7 -Disjoint sums in Zermelo-Fraenkel Set Theory 
     1.8 -"Part" primitive for simultaneous recursive type definitions
     1.9  *)
    1.10  
    1.11 +header{*Disjoint Sums*}
    1.12 +
    1.13  theory Sum = Bool + equalities:
    1.14  
    1.15 +text{*And the "Part" primitive for simultaneous recursive type definitions*}
    1.16 +
    1.17  global
    1.18  
    1.19  constdefs
    1.20 @@ -30,7 +32,7 @@
    1.21  
    1.22  local
    1.23  
    1.24 -(*** Rules for the Part primitive ***)
    1.25 +subsection{*Rules for the @{term Part} Primitive*}
    1.26  
    1.27  lemma Part_iff: 
    1.28      "a : Part(A,h) <-> a:A & (EX y. a=h(y))"
    1.29 @@ -56,7 +58,7 @@
    1.30  done
    1.31  
    1.32  
    1.33 -(*** Rules for Disjoint Sums ***)
    1.34 +subsection{*Rules for Disjoint Sums*}
    1.35  
    1.36  lemmas sum_defs = sum_def Inl_def Inr_def case_def
    1.37  
    1.38 @@ -130,7 +132,7 @@
    1.39  by (simp add: sum_def, blast)
    1.40  
    1.41  
    1.42 -(*** Eliminator -- case ***)
    1.43 +subsection{*The Eliminator: @{term case}*}
    1.44  
    1.45  lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)"
    1.46  by (simp add: sum_defs)
    1.47 @@ -165,7 +167,7 @@
    1.48  by auto
    1.49  
    1.50  
    1.51 -(*** More rules for Part(A,h) ***)
    1.52 +subsection{*More Rules for @{term "Part(A,h)"}*}
    1.53  
    1.54  lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)"
    1.55  by blast