new theorems, tidying
authorpaulson
Fri Jun 28 17:36:22 2002 +0200 (2002-06-28 ago)
changeset 13255407ad9c3036d
parent 13254 5146ccaedf42
child 13256 cf85c4f7dcf2
new theorems, tidying
src/ZF/Sum.thy
src/ZF/Univ.thy
     1.1 --- a/src/ZF/Sum.thy	Fri Jun 28 11:25:46 2002 +0200
     1.2 +++ b/src/ZF/Sum.thy	Fri Jun 28 17:36:22 2002 +0200
     1.3 @@ -40,17 +40,14 @@
     1.4  
     1.5  lemma Part_eqI [intro]: 
     1.6      "[| a : A;  a=h(b) |] ==> a : Part(A,h)"
     1.7 -apply (unfold Part_def)
     1.8 -apply blast
     1.9 -done
    1.10 +by (unfold Part_def, blast)
    1.11  
    1.12  lemmas PartI = refl [THEN [2] Part_eqI]
    1.13  
    1.14  lemma PartE [elim!]: 
    1.15      "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P   
    1.16       |] ==> P"
    1.17 -apply (unfold Part_def)
    1.18 -apply blast
    1.19 +apply (unfold Part_def, blast)
    1.20  done
    1.21  
    1.22  lemma Part_subset: "Part(A,h) <= A"
    1.23 @@ -64,21 +61,15 @@
    1.24  lemmas sum_defs = sum_def Inl_def Inr_def case_def
    1.25  
    1.26  lemma Sigma_bool: "Sigma(bool,C) = C(0) + C(1)"
    1.27 -apply (unfold bool_def sum_def)
    1.28 -apply blast
    1.29 -done
    1.30 +by (unfold bool_def sum_def, blast)
    1.31  
    1.32  (** Introduction rules for the injections **)
    1.33  
    1.34  lemma InlI [intro!,simp,TC]: "a : A ==> Inl(a) : A+B"
    1.35 -apply (unfold sum_defs)
    1.36 -apply blast
    1.37 -done
    1.38 +by (unfold sum_defs, blast)
    1.39  
    1.40  lemma InrI [intro!,simp,TC]: "b : B ==> Inr(b) : A+B"
    1.41 -apply (unfold sum_defs)
    1.42 -apply blast
    1.43 -done
    1.44 +by (unfold sum_defs, blast)
    1.45  
    1.46  (** Elimination rules **)
    1.47  
    1.48 @@ -87,31 +78,24 @@
    1.49          !!x. [| x:A;  u=Inl(x) |] ==> P;  
    1.50          !!y. [| y:B;  u=Inr(y) |] ==> P  
    1.51       |] ==> P"
    1.52 -apply (unfold sum_defs)
    1.53 -apply (blast intro: elim:); 
    1.54 -done
    1.55 +by (unfold sum_defs, blast) 
    1.56  
    1.57  (** Injection and freeness equivalences, for rewriting **)
    1.58  
    1.59  lemma Inl_iff [iff]: "Inl(a)=Inl(b) <-> a=b"
    1.60 -apply (simp add: sum_defs)
    1.61 -done
    1.62 +by (simp add: sum_defs)
    1.63  
    1.64  lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
    1.65 -apply (simp add: sum_defs)
    1.66 -done
    1.67 +by (simp add: sum_defs)
    1.68  
    1.69  lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) <-> False"
    1.70 -apply (simp add: sum_defs)
    1.71 -done
    1.72 +by (simp add: sum_defs)
    1.73  
    1.74  lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) <-> False"
    1.75 -apply (simp add: sum_defs)
    1.76 -done
    1.77 +by (simp add: sum_defs)
    1.78  
    1.79  lemma sum_empty [simp]: "0+0 = 0"
    1.80 -apply (simp add: sum_defs)
    1.81 -done
    1.82 +by (simp add: sum_defs)
    1.83  
    1.84  (*Injection and freeness rules*)
    1.85  
    1.86 @@ -122,49 +106,44 @@
    1.87  
    1.88  
    1.89  lemma InlD: "Inl(a): A+B ==> a: A"
    1.90 -apply blast
    1.91 -done
    1.92 +by blast
    1.93  
    1.94  lemma InrD: "Inr(b): A+B ==> b: B"
    1.95 -apply blast
    1.96 -done
    1.97 +by blast
    1.98  
    1.99  lemma sum_iff: "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))"
   1.100 -apply blast
   1.101 -done
   1.102 +by blast
   1.103 +
   1.104 +lemma Inl_in_sum_iff [simp]: "(Inl(x) \<in> A+B) <-> (x \<in> A)";
   1.105 +by auto
   1.106 +
   1.107 +lemma Inr_in_sum_iff [simp]: "(Inr(y) \<in> A+B) <-> (y \<in> B)";
   1.108 +by auto
   1.109  
   1.110  lemma sum_subset_iff: "A+B <= C+D <-> A<=C & B<=D"
   1.111 -apply blast
   1.112 -done
   1.113 +by blast
   1.114  
   1.115  lemma sum_equal_iff: "A+B = C+D <-> A=C & B=D"
   1.116 -apply (simp add: extension sum_subset_iff)
   1.117 -apply blast
   1.118 -done
   1.119 +by (simp add: extension sum_subset_iff, blast)
   1.120  
   1.121  lemma sum_eq_2_times: "A+A = 2*A"
   1.122 -apply (simp add: sum_def)
   1.123 -apply blast
   1.124 -done
   1.125 +by (simp add: sum_def, blast)
   1.126  
   1.127  
   1.128  (*** Eliminator -- case ***)
   1.129  
   1.130  lemma case_Inl [simp]: "case(c, d, Inl(a)) = c(a)"
   1.131 -apply (simp add: sum_defs)
   1.132 -done
   1.133 +by (simp add: sum_defs)
   1.134  
   1.135  lemma case_Inr [simp]: "case(c, d, Inr(b)) = d(b)"
   1.136 -apply (simp add: sum_defs)
   1.137 -done
   1.138 +by (simp add: sum_defs)
   1.139  
   1.140  lemma case_type [TC]:
   1.141      "[| u: A+B;  
   1.142          !!x. x: A ==> c(x): C(Inl(x));    
   1.143          !!y. y: B ==> d(y): C(Inr(y))  
   1.144       |] ==> case(c,d,u) : C(u)"
   1.145 -apply (auto );  
   1.146 -done
   1.147 +by auto
   1.148  
   1.149  lemma expand_case: "u: A+B ==>    
   1.150          R(case(c,d,u)) <->  
   1.151 @@ -177,10 +156,11 @@
   1.152        !!x. x:A ==> c(x)=c'(x);   
   1.153        !!y. y:B ==> d(y)=d'(y)    
   1.154     |] ==> case(c,d,z) = case(c',d',z)"
   1.155 -by (auto ); 
   1.156 +by auto 
   1.157  
   1.158  lemma case_case: "z: A+B ==>    
   1.159 -        case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =  
   1.160 +        
   1.161 +	case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) =  
   1.162          case(%x. c(c'(x)), %y. d(d'(y)), z)"
   1.163  by auto
   1.164  
   1.165 @@ -188,39 +168,31 @@
   1.166  (*** More rules for Part(A,h) ***)
   1.167  
   1.168  lemma Part_mono: "A<=B ==> Part(A,h)<=Part(B,h)"
   1.169 -apply blast
   1.170 -done
   1.171 +by blast
   1.172  
   1.173  lemma Part_Collect: "Part(Collect(A,P), h) = Collect(Part(A,h), P)"
   1.174 -apply blast
   1.175 -done
   1.176 +by blast
   1.177  
   1.178  lemmas Part_CollectE =
   1.179       Part_Collect [THEN equalityD1, THEN subsetD, THEN CollectE, standard]
   1.180  
   1.181  lemma Part_Inl: "Part(A+B,Inl) = {Inl(x). x: A}"
   1.182 -apply blast
   1.183 -done
   1.184 +by blast
   1.185  
   1.186  lemma Part_Inr: "Part(A+B,Inr) = {Inr(y). y: B}"
   1.187 -apply blast
   1.188 -done
   1.189 +by blast
   1.190  
   1.191  lemma PartD1: "a : Part(A,h) ==> a : A"
   1.192 -apply (simp add: Part_def)
   1.193 -done
   1.194 +by (simp add: Part_def)
   1.195  
   1.196  lemma Part_id: "Part(A,%x. x) = A"
   1.197 -apply blast
   1.198 -done
   1.199 +by blast
   1.200  
   1.201  lemma Part_Inr2: "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}"
   1.202 -apply blast
   1.203 -done
   1.204 +by blast
   1.205  
   1.206  lemma Part_sum_equality: "C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C"
   1.207 -apply blast
   1.208 -done
   1.209 +by blast
   1.210  
   1.211  ML
   1.212  {*
     2.1 --- a/src/ZF/Univ.thy	Fri Jun 28 11:25:46 2002 +0200
     2.2 +++ b/src/ZF/Univ.thy	Fri Jun 28 17:36:22 2002 +0200
     2.3 @@ -563,6 +563,9 @@
     2.4  apply (rule nat_0I [THEN zero_in_Vfrom])
     2.5  done
     2.6  
     2.7 +lemma zero_subset_univ: "{0} <= univ(A)"
     2.8 +by (blast intro: zero_in_univ)
     2.9 +
    2.10  lemma A_subset_univ: "A <= univ(A)"
    2.11  apply (unfold univ_def)
    2.12  apply (rule A_subset_Vfrom)
    2.13 @@ -649,10 +652,16 @@
    2.14  
    2.15  lemmas sum_subset_univ = subset_trans [OF sum_mono sum_univ]
    2.16  
    2.17 +lemma Sigma_subset_univ:
    2.18 +  "[|A \<subseteq> univ(D); \<And>x. x \<in> A \<Longrightarrow> B(x) \<subseteq> univ(D)|] ==> Sigma(A,B) \<subseteq> univ(D)"
    2.19 +apply (simp add: univ_def)
    2.20 +apply (blast intro: Sigma_subset_VLimit del: subsetI) 
    2.21 +done
    2.22  
    2.23 -subsubsection{* Closure under binary union -- use Un_least *}
    2.24 -subsubsection{* Closure under Collect -- use  (Collect_subset RS subset_trans)  *}
    2.25 -subsubsection{* Closure under RepFun -- use   RepFun_subset  *}
    2.26 +
    2.27 +(*Closure under binary union -- use Un_least
    2.28 +  Closure under Collect -- use  Collect_subset [THEN subset_trans]
    2.29 +  Closure under RepFun -- use   RepFun_subset *)
    2.30  
    2.31  
    2.32  subsection{* Finite Branching Closure Properties *}