src/ZF/sum.ML
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/sum.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,170 @@
     1.4 +(*  Title: 	ZF/sum
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +Disjoint sums in Zermelo-Fraenkel Set Theory 
    1.10 +*)
    1.11 +
    1.12 +open Sum;
    1.13 +
    1.14 +val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
    1.15 +
    1.16 +(** Introduction rules for the injections **)
    1.17 +
    1.18 +goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";
    1.19 +by (REPEAT (ares_tac [UnI1,SigmaI,singletonI] 1));
    1.20 +val InlI = result();
    1.21 +
    1.22 +goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B";
    1.23 +by (REPEAT (ares_tac [UnI2,SigmaI,singletonI] 1));
    1.24 +val InrI = result();
    1.25 +
    1.26 +(** Elimination rules **)
    1.27 +
    1.28 +val major::prems = goalw Sum.thy sum_defs
    1.29 +    "[| u: A+B;  \
    1.30 +\       !!x. [| x:A;  u=Inl(x) |] ==> P; \
    1.31 +\       !!y. [| y:B;  u=Inr(y) |] ==> P \
    1.32 +\    |] ==> P";
    1.33 +by (rtac (major RS UnE) 1);
    1.34 +by (REPEAT (rtac refl 1
    1.35 +     ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1));
    1.36 +val sumE = result();
    1.37 +
    1.38 +(** Injection and freeness rules **)
    1.39 +
    1.40 +val [major] = goalw Sum.thy sum_defs "Inl(a)=Inl(b) ==> a=b";
    1.41 +by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
    1.42 +val Inl_inject = result();
    1.43 +
    1.44 +val [major] = goalw Sum.thy sum_defs "Inr(a)=Inr(b) ==> a=b";
    1.45 +by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
    1.46 +val Inr_inject = result();
    1.47 +
    1.48 +val [major] = goalw Sum.thy sum_defs "Inl(a)=Inr(b) ==> P";
    1.49 +by (rtac (major RS Pair_inject) 1);
    1.50 +by (etac (sym RS one_neq_0) 1);
    1.51 +val Inl_neq_Inr = result();
    1.52 +
    1.53 +val Inr_neq_Inl = sym RS Inl_neq_Inr;
    1.54 +
    1.55 +(** Injection and freeness equivalences, for rewriting **)
    1.56 +
    1.57 +goal Sum.thy "Inl(a)=Inl(b) <-> a=b";
    1.58 +by (rtac iffI 1);
    1.59 +by (REPEAT (eresolve_tac [Inl_inject,subst_context] 1));
    1.60 +val Inl_iff = result();
    1.61 +
    1.62 +goal Sum.thy "Inr(a)=Inr(b) <-> a=b";
    1.63 +by (rtac iffI 1);
    1.64 +by (REPEAT (eresolve_tac [Inr_inject,subst_context] 1));
    1.65 +val Inr_iff = result();
    1.66 +
    1.67 +goal Sum.thy "Inl(a)=Inr(b) <-> False";
    1.68 +by (rtac iffI 1);
    1.69 +by (REPEAT (eresolve_tac [Inl_neq_Inr,FalseE] 1));
    1.70 +val Inl_Inr_iff = result();
    1.71 +
    1.72 +goal Sum.thy "Inr(b)=Inl(a) <-> False";
    1.73 +by (rtac iffI 1);
    1.74 +by (REPEAT (eresolve_tac [Inr_neq_Inl,FalseE] 1));
    1.75 +val Inr_Inl_iff = result();
    1.76 +
    1.77 +val sum_cs = ZF_cs addIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
    1.78 +                   addSDs [Inl_inject,Inr_inject];
    1.79 +
    1.80 +goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
    1.81 +by (fast_tac sum_cs 1);
    1.82 +val sum_iff = result();
    1.83 +
    1.84 +goal Sum.thy "A+B <= C+D <-> A<=C & B<=D";
    1.85 +by (fast_tac sum_cs 1);
    1.86 +val sum_subset_iff = result();
    1.87 +
    1.88 +goal Sum.thy "A+B = C+D <-> A=C & B=D";
    1.89 +by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);
    1.90 +by (fast_tac ZF_cs 1);
    1.91 +val sum_equal_iff = result();
    1.92 +
    1.93 +(*** Eliminator -- case ***)
    1.94 +
    1.95 +goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";
    1.96 +by (rtac (split RS trans) 1);
    1.97 +by (rtac cond_0 1);
    1.98 +val case_Inl = result();
    1.99 +
   1.100 +goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)";
   1.101 +by (rtac (split RS trans) 1);
   1.102 +by (rtac cond_1 1);
   1.103 +val case_Inr = result();
   1.104 +
   1.105 +val prems = goalw Sum.thy [case_def]
   1.106 +    "[| u=u'; !!x. c(x)=c'(x);  !!y. d(y)=d'(y) |] ==>    \
   1.107 +\    case(c,d,u)=case(c',d',u')";
   1.108 +by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));
   1.109 +val case_cong = result();
   1.110 +
   1.111 +val major::prems = goal Sum.thy
   1.112 +    "[| u: A+B; \
   1.113 +\       !!x. x: A ==> c(x): C(Inl(x));   \
   1.114 +\       !!y. y: B ==> d(y): C(Inr(y)) \
   1.115 +\    |] ==> case(c,d,u) : C(u)";
   1.116 +by (rtac (major RS sumE) 1);
   1.117 +by (ALLGOALS (etac ssubst));
   1.118 +by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
   1.119 +			    (prems@[case_Inl,case_Inr]))));
   1.120 +val case_type = result();
   1.121 +
   1.122 +(** Rules for the Part primitive **)
   1.123 +
   1.124 +goalw Sum.thy [Part_def]
   1.125 +    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
   1.126 +by (REPEAT (ares_tac [exI,CollectI] 1));
   1.127 +val Part_eqI = result();
   1.128 +
   1.129 +val PartI = refl RSN (2,Part_eqI);
   1.130 +
   1.131 +val major::prems = goalw Sum.thy [Part_def]
   1.132 +    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
   1.133 +\    |] ==> P";
   1.134 +by (rtac (major RS CollectE) 1);
   1.135 +by (etac exE 1);
   1.136 +by (REPEAT (ares_tac prems 1));
   1.137 +val PartE = result();
   1.138 +
   1.139 +goalw Sum.thy [Part_def] "Part(A,h) <= A";
   1.140 +by (rtac Collect_subset 1);
   1.141 +val Part_subset = result();
   1.142 +
   1.143 +goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
   1.144 +by (fast_tac (ZF_cs addIs [PartI] addSEs [PartE]) 1);
   1.145 +val Part_mono = result();
   1.146 +
   1.147 +goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
   1.148 +by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.149 +val Part_Inl = result();
   1.150 +
   1.151 +goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
   1.152 +by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.153 +val Part_Inr = result();
   1.154 +
   1.155 +goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
   1.156 +by (etac CollectD1 1);
   1.157 +val PartD1 = result();
   1.158 +
   1.159 +goal Sum.thy "Part(A,%x.x) = A";
   1.160 +by (fast_tac (ZF_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.161 +val Part_id = result();
   1.162 +
   1.163 +goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
   1.164 +by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
   1.165 +val Part_Inr2 = result();
   1.166 +
   1.167 +goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
   1.168 +by (rtac equalityI 1);
   1.169 +by (rtac Un_least 1);
   1.170 +by (rtac Part_subset 1);
   1.171 +by (rtac Part_subset 1);
   1.172 +by (fast_tac (ZF_cs addIs [PartI] addSEs [sumE]) 1);
   1.173 +val Part_sum_equality = result();