diff -r c9cfe1638bf2 -r 6f54e992777e src/ZF/pair.thy --- a/src/ZF/pair.thy Sun Jul 14 15:14:43 2002 +0200 +++ b/src/ZF/pair.thy Sun Jul 14 19:59:55 2002 +0200 @@ -3,9 +3,10 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -Ordered pairs in Zermelo-Fraenkel Set Theory *) +header{*Ordered Pairs*} + theory pair = upair files "simpdata.ML": @@ -49,8 +50,9 @@ done -(*** Sigma: Disjoint union of a family of sets - Generalizes Cartesian product ***) +subsection{*Sigma: Disjoint Union of a Family of Sets*} + +text{*Generalizes Cartesian product*} lemma Sigma_iff [simp]: ": Sigma(A,B) <-> a:A & b:B(a)" by (simp add: Sigma_def) @@ -66,15 +68,13 @@ "[| c: Sigma(A,B); !!x y.[| x:A; y:B(x); c= |] ==> P |] ==> P" -apply (unfold Sigma_def, blast) -done +by (unfold Sigma_def, blast) lemma SigmaE2 [elim!]: "[| : Sigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P" -apply (unfold Sigma_def, blast) -done +by (unfold Sigma_def, blast) lemma Sigma_cong: "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> @@ -95,7 +95,7 @@ by blast -(*** Projections: fst, snd ***) +subsection{*Projections @{term fst} and @{term snd}*} lemma fst_conv [simp]: "fst() = a" by (simp add: fst_def, blast) @@ -113,7 +113,7 @@ by auto -(*** Eliminator - split ***) +subsection{*The Eliminator, @{term split}*} (*A META-equality, so that it applies to higher types as well...*) lemma split [simp]: "split(%x y. c(x,y), ) == c(a,b)" @@ -133,7 +133,7 @@ done -(*** split for predicates: result type o ***) +subsection{*A version of @{term split} for Formulae: Result Type @{typ o}*} lemma splitI: "R(a,b) ==> split(R, )" by (simp add: split_def)