src/ZF/Sum.ML
author clasohm
Thu, 16 Sep 1993 12:20:38 +0200
changeset 0 a5a9c433f639
child 6 8ce8c4d13d4d
permissions -rw-r--r--
Initial revision
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/sum
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1992  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Disjoint sums in Zermelo-Fraenkel Set Theory 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open Sum;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
(** Introduction rules for the injections **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
by (REPEAT (ares_tac [UnI1,SigmaI,singletonI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
val InlI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
by (REPEAT (ares_tac [UnI2,SigmaI,singletonI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
val InrI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
(** Elimination rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
val major::prems = goalw Sum.thy sum_defs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
    "[| u: A+B;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
\       !!x. [| x:A;  u=Inl(x) |] ==> P; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
\       !!y. [| y:B;  u=Inr(y) |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
by (rtac (major RS UnE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
by (REPEAT (rtac refl 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
     ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
val sumE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
(** Injection and freeness rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val [major] = goalw Sum.thy sum_defs "Inl(a)=Inl(b) ==> a=b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val Inl_inject = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
val [major] = goalw Sum.thy sum_defs "Inr(a)=Inr(b) ==> a=b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
by (EVERY1 [rtac (major RS Pair_inject), assume_tac]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val Inr_inject = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
val [major] = goalw Sum.thy sum_defs "Inl(a)=Inr(b) ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
by (rtac (major RS Pair_inject) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
by (etac (sym RS one_neq_0) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
val Inl_neq_Inr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
val Inr_neq_Inl = sym RS Inl_neq_Inr;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
(** Injection and freeness equivalences, for rewriting **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
goal Sum.thy "Inl(a)=Inl(b) <-> a=b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
by (REPEAT (eresolve_tac [Inl_inject,subst_context] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
val Inl_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
goal Sum.thy "Inr(a)=Inr(b) <-> a=b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
by (REPEAT (eresolve_tac [Inr_inject,subst_context] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
val Inr_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
goal Sum.thy "Inl(a)=Inr(b) <-> False";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
by (REPEAT (eresolve_tac [Inl_neq_Inr,FalseE] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
val Inl_Inr_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
goal Sum.thy "Inr(b)=Inl(a) <-> False";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
by (REPEAT (eresolve_tac [Inr_neq_Inl,FalseE] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
val Inr_Inl_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
val sum_cs = ZF_cs addIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
                   addSDs [Inl_inject,Inr_inject];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
by (fast_tac sum_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
val sum_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
goal Sum.thy "A+B <= C+D <-> A<=C & B<=D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
by (fast_tac sum_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
val sum_subset_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
goal Sum.thy "A+B = C+D <-> A=C & B=D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
by (SIMP_TAC (ZF_ss addrews [extension,sum_subset_iff]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val sum_equal_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
(*** Eliminator -- case ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
by (rtac (split RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
by (rtac cond_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
val case_Inl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
by (rtac (split RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
by (rtac cond_1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
val case_Inr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
val prems = goalw Sum.thy [case_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
    "[| u=u'; !!x. c(x)=c'(x);  !!y. d(y)=d'(y) |] ==>    \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
\    case(c,d,u)=case(c',d',u')";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
by (REPEAT (resolve_tac ([refl,split_cong,cond_cong] @ prems) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val case_cong = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
val major::prems = goal Sum.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
    "[| u: A+B; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
\       !!x. x: A ==> c(x): C(Inl(x));   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
\       !!y. y: B ==> d(y): C(Inr(y)) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
\    |] ==> case(c,d,u) : C(u)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
by (rtac (major RS sumE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
by (ALLGOALS (etac ssubst));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
by (ALLGOALS (ASM_SIMP_TAC (ZF_ss addrews
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
			    (prems@[case_Inl,case_Inr]))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
val case_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
(** Rules for the Part primitive **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
goalw Sum.thy [Part_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
by (REPEAT (ares_tac [exI,CollectI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
val Part_eqI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
val PartI = refl RSN (2,Part_eqI);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
val major::prems = goalw Sum.thy [Part_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
by (rtac (major RS CollectE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
by (etac exE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
val PartE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
goalw Sum.thy [Part_def] "Part(A,h) <= A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (rtac Collect_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val Part_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
by (fast_tac (ZF_cs addIs [PartI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
val Part_mono = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
val Part_Inl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
val Part_Inr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (etac CollectD1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
val PartD1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
goal Sum.thy "Part(A,%x.x) = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
by (fast_tac (ZF_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
val Part_id = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
val Part_Inr2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
by (rtac Un_least 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
by (fast_tac (ZF_cs addIs [PartI] addSEs [sumE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
val Part_sum_equality = result();