src/ZF/Sum.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4091 771b1f6422a8
child 5067 62b6288e6005
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
clasohm@1461
     1
(*  Title:      ZF/Sum
clasohm@0
     2
    ID:         $Id$
clasohm@1461
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Disjoint sums in Zermelo-Fraenkel Set Theory 
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open Sum;
clasohm@0
    10
lcp@744
    11
(*** Rules for the Part primitive ***)
lcp@744
    12
lcp@744
    13
goalw Sum.thy [Part_def]
lcp@744
    14
    "a : Part(A,h) <-> a:A & (EX y. a=h(y))";
lcp@744
    15
by (rtac separation 1);
clasohm@760
    16
qed "Part_iff";
lcp@744
    17
lcp@744
    18
goalw Sum.thy [Part_def]
lcp@744
    19
    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
paulson@2925
    20
by (Blast_tac 1);
clasohm@760
    21
qed "Part_eqI";
lcp@744
    22
lcp@744
    23
val PartI = refl RSN (2,Part_eqI);
lcp@744
    24
lcp@744
    25
val major::prems = goalw Sum.thy [Part_def]
lcp@744
    26
    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
lcp@744
    27
\    |] ==> P";
lcp@744
    28
by (rtac (major RS CollectE) 1);
lcp@744
    29
by (etac exE 1);
lcp@744
    30
by (REPEAT (ares_tac prems 1));
clasohm@760
    31
qed "PartE";
lcp@744
    32
paulson@2925
    33
AddIs  [Part_eqI];
paulson@2469
    34
AddSEs [PartE];
paulson@2469
    35
lcp@744
    36
goalw Sum.thy [Part_def] "Part(A,h) <= A";
lcp@744
    37
by (rtac Collect_subset 1);
clasohm@760
    38
qed "Part_subset";
lcp@744
    39
lcp@744
    40
lcp@744
    41
(*** Rules for Disjoint Sums ***)
lcp@744
    42
clasohm@0
    43
val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
clasohm@0
    44
lcp@521
    45
goalw Sum.thy (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
paulson@2925
    46
by (Blast_tac 1);
clasohm@760
    47
qed "Sigma_bool";
lcp@521
    48
clasohm@0
    49
(** Introduction rules for the injections **)
clasohm@0
    50
clasohm@0
    51
goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";
paulson@2925
    52
by (Blast_tac 1);
clasohm@760
    53
qed "InlI";
clasohm@0
    54
clasohm@0
    55
goalw Sum.thy sum_defs "!!b A B. b : B ==> Inr(b) : A+B";
paulson@2925
    56
by (Blast_tac 1);
clasohm@760
    57
qed "InrI";
clasohm@0
    58
clasohm@0
    59
(** Elimination rules **)
clasohm@0
    60
clasohm@0
    61
val major::prems = goalw Sum.thy sum_defs
clasohm@0
    62
    "[| u: A+B;  \
clasohm@0
    63
\       !!x. [| x:A;  u=Inl(x) |] ==> P; \
clasohm@0
    64
\       !!y. [| y:B;  u=Inr(y) |] ==> P \
clasohm@0
    65
\    |] ==> P";
clasohm@0
    66
by (rtac (major RS UnE) 1);
clasohm@0
    67
by (REPEAT (rtac refl 1
clasohm@0
    68
     ORELSE eresolve_tac (prems@[SigmaE,singletonE,ssubst]) 1));
clasohm@760
    69
qed "sumE";
clasohm@0
    70
clasohm@0
    71
(** Injection and freeness equivalences, for rewriting **)
clasohm@0
    72
lcp@55
    73
goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b";
paulson@2469
    74
by (Simp_tac 1);
clasohm@760
    75
qed "Inl_iff";
clasohm@0
    76
lcp@55
    77
goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b";
paulson@2469
    78
by (Simp_tac 1);
clasohm@760
    79
qed "Inr_iff";
clasohm@0
    80
lcp@55
    81
goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False";
paulson@2469
    82
by (Simp_tac 1);
clasohm@760
    83
qed "Inl_Inr_iff";
clasohm@0
    84
lcp@55
    85
goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False";
paulson@2469
    86
by (Simp_tac 1);
clasohm@760
    87
qed "Inr_Inl_iff";
clasohm@0
    88
paulson@2469
    89
goalw Sum.thy sum_defs "0+0 = 0";
paulson@2469
    90
by (Simp_tac 1);
paulson@2469
    91
qed "sum_empty";
paulson@2469
    92
lcp@55
    93
(*Injection and freeness rules*)
lcp@55
    94
clasohm@782
    95
bind_thm ("Inl_inject", (Inl_iff RS iffD1));
clasohm@782
    96
bind_thm ("Inr_inject", (Inr_iff RS iffD1));
clasohm@782
    97
bind_thm ("Inl_neq_Inr", (Inl_Inr_iff RS iffD1 RS FalseE));
clasohm@782
    98
bind_thm ("Inr_neq_Inl", (Inr_Inl_iff RS iffD1 RS FalseE));
lcp@55
    99
paulson@2469
   100
AddSIs [InlI, InrI];
paulson@2469
   101
AddSEs [sumE, Inl_neq_Inr, Inr_neq_Inl];
paulson@2469
   102
AddSDs [Inl_inject, Inr_inject];
paulson@2469
   103
paulson@2469
   104
Addsimps [InlI, InrI, Inl_iff, Inr_iff, Inl_Inr_iff, Inr_Inl_iff, sum_empty];
paulson@2469
   105
lcp@55
   106
goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
paulson@2925
   107
by (Blast_tac 1);
clasohm@760
   108
qed "InlD";
lcp@55
   109
lcp@55
   110
goal Sum.thy "!!A B. Inr(b): A+B ==> b: B";
paulson@2925
   111
by (Blast_tac 1);
clasohm@760
   112
qed "InrD";
lcp@55
   113
clasohm@0
   114
goal Sum.thy "u: A+B <-> (EX x. x:A & u=Inl(x)) | (EX y. y:B & u=Inr(y))";
paulson@2925
   115
by (Blast_tac 1);
clasohm@760
   116
qed "sum_iff";
clasohm@0
   117
clasohm@0
   118
goal Sum.thy "A+B <= C+D <-> A<=C & B<=D";
paulson@2925
   119
by (Blast_tac 1);
clasohm@760
   120
qed "sum_subset_iff";
clasohm@0
   121
clasohm@0
   122
goal Sum.thy "A+B = C+D <-> A=C & B=D";
wenzelm@4091
   123
by (simp_tac (simpset() addsimps [extension,sum_subset_iff]) 1);
paulson@2925
   124
by (Blast_tac 1);
clasohm@760
   125
qed "sum_equal_iff";
clasohm@0
   126
paulson@1611
   127
goalw Sum.thy [sum_def] "A+A = 2*A";
paulson@2925
   128
by (Blast_tac 1);
paulson@1611
   129
qed "sum_eq_2_times";
paulson@1611
   130
lcp@521
   131
clasohm@0
   132
(*** Eliminator -- case ***)
clasohm@0
   133
clasohm@0
   134
goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";
wenzelm@4091
   135
by (simp_tac (simpset() addsimps [cond_0]) 1);
clasohm@760
   136
qed "case_Inl";
clasohm@0
   137
clasohm@0
   138
goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)";
wenzelm@4091
   139
by (simp_tac (simpset() addsimps [cond_1]) 1);
clasohm@760
   140
qed "case_Inr";
clasohm@0
   141
paulson@2469
   142
Addsimps [case_Inl, case_Inr];
paulson@2469
   143
clasohm@0
   144
val major::prems = goal Sum.thy
clasohm@0
   145
    "[| u: A+B; \
clasohm@0
   146
\       !!x. x: A ==> c(x): C(Inl(x));   \
clasohm@0
   147
\       !!y. y: B ==> d(y): C(Inr(y)) \
clasohm@0
   148
\    |] ==> case(c,d,u) : C(u)";
clasohm@0
   149
by (rtac (major RS sumE) 1);
clasohm@0
   150
by (ALLGOALS (etac ssubst));
wenzelm@4091
   151
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
clasohm@760
   152
qed "case_type";
clasohm@0
   153
lcp@435
   154
goal Sum.thy
lcp@435
   155
  "!!u. u: A+B ==>   \
lcp@435
   156
\       R(case(c,d,u)) <-> \
lcp@435
   157
\       ((ALL x:A. u = Inl(x) --> R(c(x))) & \
lcp@435
   158
\       (ALL y:B. u = Inr(y) --> R(d(y))))";
paulson@4477
   159
by Auto_tac;
clasohm@760
   160
qed "expand_case";
lcp@435
   161
lcp@858
   162
val major::prems = goal Sum.thy
clasohm@1461
   163
  "[| z: A+B;   \
clasohm@1461
   164
\     !!x. x:A ==> c(x)=c'(x);  \
clasohm@1461
   165
\     !!y. y:B ==> d(y)=d'(y)   \
lcp@858
   166
\  |] ==> case(c,d,z) = case(c',d',z)";
lcp@858
   167
by (resolve_tac [major RS sumE] 1);
wenzelm@4091
   168
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
lcp@858
   169
qed "case_cong";
lcp@858
   170
paulson@2469
   171
goal Sum.thy
paulson@2469
   172
  "!!z. z: A+B ==>   \
paulson@2469
   173
\       case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \
paulson@2469
   174
\       case(%x. c(c'(x)), %y. d(d'(y)), z)";
paulson@4477
   175
by Auto_tac;
lcp@858
   176
qed "case_case";
lcp@858
   177
lcp@773
   178
lcp@773
   179
(*** More rules for Part(A,h) ***)
lcp@773
   180
clasohm@0
   181
goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
paulson@2925
   182
by (Blast_tac 1);
clasohm@760
   183
qed "Part_mono";
clasohm@0
   184
lcp@744
   185
goal Sum.thy "Part(Collect(A,P), h) = Collect(Part(A,h), P)";
paulson@2925
   186
by (Blast_tac 1);
clasohm@760
   187
qed "Part_Collect";
lcp@744
   188
lcp@803
   189
bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE);
lcp@744
   190
clasohm@0
   191
goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
paulson@2925
   192
by (Blast_tac 1);
clasohm@760
   193
qed "Part_Inl";
clasohm@0
   194
clasohm@0
   195
goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
paulson@2925
   196
by (Blast_tac 1);
clasohm@760
   197
qed "Part_Inr";
clasohm@0
   198
clasohm@0
   199
goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
clasohm@0
   200
by (etac CollectD1 1);
clasohm@760
   201
qed "PartD1";
clasohm@0
   202
wenzelm@3840
   203
goal Sum.thy "Part(A,%x. x) = A";
paulson@2925
   204
by (Blast_tac 1);
clasohm@760
   205
qed "Part_id";
clasohm@0
   206
wenzelm@3840
   207
goal Sum.thy "Part(A+B, %x. Inr(h(x))) = {Inr(y). y: Part(B,h)}";
paulson@2925
   208
by (Blast_tac 1);
clasohm@760
   209
qed "Part_Inr2";
clasohm@0
   210
clasohm@0
   211
goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
paulson@2925
   212
by (Blast_tac 1);
clasohm@760
   213
qed "Part_sum_equality";