src/ZF/Sum.thy
 changeset 13255 407ad9c3036d parent 13240 bb5f4faea1f3 child 13356 c9cfe1638bf2
```     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.61 -done
1.63
1.64  lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
1.66 -done
1.68
1.69  lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) <-> False"
1.71 -done
1.73
1.74  lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) <-> False"
1.76 -done
1.78
1.79  lemma sum_empty [simp]: "0+0 = 0"
1.81 -done
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.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.132 -done
1.134
1.135  lemma case_Inr [simp]: "case(c, d, Inr(b)) = d(b)"
1.137 -done
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.193 -done
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  {*
```