src/ZF/pair.thy
changeset 13357 6f54e992777e
parent 13240 bb5f4faea1f3
child 13544 895994073bdf
     1.1 --- a/src/ZF/pair.thy	Sun Jul 14 15:14:43 2002 +0200
     1.2 +++ b/src/ZF/pair.thy	Sun Jul 14 19:59:55 2002 +0200
     1.3 @@ -3,9 +3,10 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1992  University of Cambridge
     1.6  
     1.7 -Ordered pairs in Zermelo-Fraenkel Set Theory 
     1.8  *)
     1.9  
    1.10 +header{*Ordered Pairs*}
    1.11 +
    1.12  theory pair = upair
    1.13  files "simpdata.ML":
    1.14  
    1.15 @@ -49,8 +50,9 @@
    1.16  done
    1.17  
    1.18  
    1.19 -(*** Sigma: Disjoint union of a family of sets
    1.20 -     Generalizes Cartesian product ***)
    1.21 +subsection{*Sigma: Disjoint Union of a Family of Sets*}
    1.22 +
    1.23 +text{*Generalizes Cartesian product*}
    1.24  
    1.25  lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) <-> a:A & b:B(a)"
    1.26  by (simp add: Sigma_def)
    1.27 @@ -66,15 +68,13 @@
    1.28      "[| c: Sigma(A,B);   
    1.29          !!x y.[| x:A;  y:B(x);  c=<x,y> |] ==> P  
    1.30       |] ==> P"
    1.31 -apply (unfold Sigma_def, blast) 
    1.32 -done
    1.33 +by (unfold Sigma_def, blast) 
    1.34  
    1.35  lemma SigmaE2 [elim!]:
    1.36      "[| <a,b> : Sigma(A,B);     
    1.37          [| a:A;  b:B(a) |] ==> P    
    1.38       |] ==> P"
    1.39 -apply (unfold Sigma_def, blast) 
    1.40 -done
    1.41 +by (unfold Sigma_def, blast) 
    1.42  
    1.43  lemma Sigma_cong:
    1.44      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
    1.45 @@ -95,7 +95,7 @@
    1.46  by blast
    1.47  
    1.48  
    1.49 -(*** Projections: fst, snd ***)
    1.50 +subsection{*Projections @{term fst} and @{term snd}*}
    1.51  
    1.52  lemma fst_conv [simp]: "fst(<a,b>) = a"
    1.53  by (simp add: fst_def, blast)
    1.54 @@ -113,7 +113,7 @@
    1.55  by auto
    1.56  
    1.57  
    1.58 -(*** Eliminator - split ***)
    1.59 +subsection{*The Eliminator, @{term split}*}
    1.60  
    1.61  (*A META-equality, so that it applies to higher types as well...*)
    1.62  lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)"
    1.63 @@ -133,7 +133,7 @@
    1.64  done
    1.65  
    1.66  
    1.67 -(*** split for predicates: result type o ***)
    1.68 +subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*}
    1.69  
    1.70  lemma splitI: "R(a,b) ==> split(R, <a,b>)"
    1.71  by (simp add: split_def)