# HG changeset patch
# User paulson
# Date 1025278582 -7200
# Node ID 407ad9c3036d04e07650684e5b263cdd7eed5ce8
# Parent  5146ccaedf42f0fd3fc48ba7f64c1cef0b102413
new theorems, tidying

diff -r 5146ccaedf42 -r 407ad9c3036d src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Fri Jun 28 11:25:46 2002 +0200
+++ b/src/ZF/Sum.thy	Fri Jun 28 17:36:22 2002 +0200
@@ -40,17 +40,14 @@
 
 lemma Part_eqI [intro]: 
     "[| a : A;  a=h(b) |] ==> a : Part(A,h)"
-apply (unfold Part_def)
-apply blast
-done
+by (unfold Part_def, blast)
 
 lemmas PartI = refl [THEN [2] Part_eqI]
 
 lemma PartE [elim!]: 
     "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P   
      |] ==> P"
-apply (unfold Part_def)
-apply blast
+apply (unfold Part_def, blast)
 done
 
 lemma Part_subset: "Part(A,h) <= A"
@@ -64,21 +61,15 @@
 lemmas sum_defs = sum_def Inl_def Inr_def case_def
 
 lemma Sigma_bool: "Sigma(bool,C) = C(0) + C(1)"
-apply (unfold bool_def sum_def)
-apply blast
-done
+by (unfold bool_def sum_def, blast)
 
 (** Introduction rules for the injections **)
 
 lemma InlI [intro!,simp,TC]: "a : A ==> Inl(a) : A+B"
-apply (unfold sum_defs)
-apply blast
-done
+by (unfold sum_defs, blast)
 
 lemma InrI [intro!,simp,TC]: "b : B ==> Inr(b) : A+B"
-apply (unfold sum_defs)
-apply blast
-done
+by (unfold sum_defs, blast)
 
 (** Elimination rules **)
 
@@ -87,31 +78,24 @@
         !!x. [| x:A;  u=Inl(x) |] ==> P;  
         !!y. [| y:B;  u=Inr(y) |] ==> P  
      |] ==> P"
-apply (unfold sum_defs)
-apply (blast intro: elim:); 
-done
+by (unfold sum_defs, blast) 
 
 (** Injection and freeness equivalences, for rewriting **)
 
 lemma Inl_iff [iff]: "Inl(a)=Inl(b) <-> a=b"
-apply (simp add: sum_defs)
-done
+by (simp add: sum_defs)
 
 lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
-apply (simp add: sum_defs)
-done
+by (simp add: sum_defs)
 
 lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) <-> False"
-apply (simp add: sum_defs)
-done
+by (simp add: sum_defs)
 
 lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) <-> False"
-apply (simp add: sum_defs)
-done
+by (simp add: sum_defs)
 
 lemma sum_empty [simp]: "0+0 = 0"
-apply (simp add: sum_defs)
-done
+by (simp add: sum_defs)
 
 (*Injection and freeness rules*)
 
@@ -122,49 +106,44 @@
 
 
 lemma InlD: "Inl(a): A+B ==> a: A"
-apply blast
-done
+by blast
 
 lemma InrD: "Inr(b): A+B ==> b: B"
-apply blast
-done
+by blast
 
 lemma sum_iff: "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"
-apply blast
-done
+by blast
+
+lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) <-> (x \<in> A)";
+by auto
+
+lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) <-> (y \<in> B)";
+by auto
 
 lemma sum_subset_iff: "A+B <= C+D <-> A<=C & B<=D"
-apply blast
-done
+by blast
 
 lemma sum_equal_iff: "A+B = C+D <-> A=C & B=D"
-apply (simp add: extension sum_subset_iff)
-apply blast
-done
+by (simp add: extension sum_subset_iff, blast)
 
 lemma sum_eq_2_times: "A+A = 2*A"
-apply (simp add: sum_def)
-apply blast
-done
+by (simp add: sum_def, blast)
 
 
 (*** Eliminator -- case ***)
 
 lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)"
-apply (simp add: sum_defs)
-done
+by (simp add: sum_defs)
 
 lemma case_Inr [simp]: "case(c, d, Inr(b)) = d(b)"
-apply (simp add: sum_defs)
-done
+by (simp add: sum_defs)
 
 lemma case_type [TC]:
     "[| u: A+B;  
         !!x. x: A ==> c(x): C(Inl(x));    
         !!y. y: B ==> d(y): C(Inr(y))  
      |] ==> case(c,d,u) : C(u)"
-apply (auto );  
-done
+by auto
 
 lemma expand_case: "u: A+B ==>    
         R(case(c,d,u)) <->  
@@ -177,10 +156,11 @@
       !!x. x:A ==> c(x)=c'(x);   
       !!y. y:B ==> d(y)=d'(y)    
    |] ==> case(c,d,z) = case(c',d',z)"
-by (auto ); 
+by auto 
 
 lemma case_case: "z: A+B ==>    
-        case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =  
+        
+	case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =  
         case(%x. c(c'(x)), %y. d(d'(y)), z)"
 by auto
 
@@ -188,39 +168,31 @@
 (*** More rules for Part(A,h) ***)
 
 lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)"
-apply blast
-done
+by blast
 
 lemma Part_Collect: "Part(Collect(A,P), h) = Collect(Part(A,h), P)"
-apply blast
-done
+by blast
 
 lemmas Part_CollectE =
      Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE, standard]
 
 lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x: A}"
-apply blast
-done
+by blast
 
 lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y: B}"
-apply blast
-done
+by blast
 
 lemma PartD1: "a : Part(A,h) ==> a : A"
-apply (simp add: Part_def)
-done
+by (simp add: Part_def)
 
 lemma Part_id: "Part(A,%x. x) = A"
-apply blast
-done
+by blast
 
 lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}"
-apply blast
-done
+by blast
 
 lemma Part_sum_equality: "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"
-apply blast
-done
+by blast
 
 ML
 {*
diff -r 5146ccaedf42 -r 407ad9c3036d src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Fri Jun 28 11:25:46 2002 +0200
+++ b/src/ZF/Univ.thy	Fri Jun 28 17:36:22 2002 +0200
@@ -563,6 +563,9 @@
 apply (rule nat_0I [THEN zero_in_Vfrom])
 done
 
+lemma zero_subset_univ: "{0} <= univ(A)"
+by (blast intro: zero_in_univ)
+
 lemma A_subset_univ: "A <= univ(A)"
 apply (unfold univ_def)
 apply (rule A_subset_Vfrom)
@@ -649,10 +652,16 @@
 
 lemmas sum_subset_univ = subset_trans [OF sum_mono sum_univ]
 
+lemma Sigma_subset_univ:
+  "[|A \<subseteq> univ(D); \<And>x. x \<in> A \<Longrightarrow> B(x) \<subseteq> univ(D)|] ==> Sigma(A,B) \<subseteq> univ(D)"
+apply (simp add: univ_def)
+apply (blast intro: Sigma_subset_VLimit del: subsetI) 
+done
 
-subsubsection{* Closure under binary union -- use Un_least *}
-subsubsection{* Closure under Collect -- use  (Collect_subset RS subset_trans)  *}
-subsubsection{* Closure under RepFun -- use   RepFun_subset  *}
+
+(*Closure under binary union -- use Un_least
+  Closure under Collect -- use  Collect_subset [THEN subset_trans]
+  Closure under RepFun -- use   RepFun_subset *)
 
 
 subsection{* Finite Branching Closure Properties *}