src/ZF/sum.ML
author paulson
Fri, 11 Aug 2000 13:26:40 +0200
changeset 9577 9e66e8ed8237
parent 55 331d93292ee0
permissions -rw-r--r--
ZF arith
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 equivalences, for rewriting **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    37
goalw Sum.thy sum_defs "Inl(a)=Inl(b) <-> a=b";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    38
by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
val Inl_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    41
goalw Sum.thy sum_defs "Inr(a)=Inr(b) <-> a=b";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    42
by (simp_tac (ZF_ss addsimps [Pair_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
val Inr_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    45
goalw Sum.thy sum_defs "Inl(a)=Inr(b) <-> False";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    46
by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0 RS not_sym]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
val Inl_Inr_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    49
goalw Sum.thy sum_defs "Inr(b)=Inl(a) <-> False";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    50
by (simp_tac (ZF_ss addsimps [Pair_iff, one_not_0]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
val Inr_Inl_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    53
(*Injection and freeness rules*)
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    54
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    55
val Inl_inject = standard (Inl_iff RS iffD1);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    56
val Inr_inject = standard (Inr_iff RS iffD1);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    57
val Inl_neq_Inr = standard (Inl_Inr_iff RS iffD1 RS FalseE);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    58
val Inr_neq_Inl = standard (Inr_Inl_iff RS iffD1 RS FalseE);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    59
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    60
val sum_cs = ZF_cs addSIs [InlI,InrI] addSEs [sumE,Inl_neq_Inr,Inr_neq_Inl]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
                   addSDs [Inl_inject,Inr_inject];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    63
goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    64
by (fast_tac sum_cs 1);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    65
val InlD = result();
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    66
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    67
goal Sum.thy "!!A B. Inr(b): A+B ==> b: B";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    68
by (fast_tac sum_cs 1);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    69
val InrD = result();
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
    70
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
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
    72
by (fast_tac sum_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
val sum_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
goal Sum.thy "A+B <= C+D <-> A<=C & B<=D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
by (fast_tac sum_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
val sum_subset_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
goal Sum.thy "A+B = C+D <-> A=C & B=D";
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    80
by (simp_tac (ZF_ss addsimps [extension,sum_subset_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val sum_equal_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
(*** Eliminator -- case ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
by (rtac (split RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
by (rtac cond_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
val case_Inl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
goalw Sum.thy sum_defs "case(c, d, Inr(b)) = d(b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
by (rtac (split RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
by (rtac cond_1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
val case_Inr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
val major::prems = goal Sum.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
    "[| u: A+B; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
\       !!x. x: A ==> c(x): C(Inl(x));   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
\       !!y. y: B ==> d(y): C(Inr(y)) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
\    |] ==> case(c,d,u) : C(u)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
by (rtac (major RS sumE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
by (ALLGOALS (etac ssubst));
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   103
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
			    (prems@[case_Inl,case_Inr]))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
val case_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
(** Rules for the Part primitive **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
goalw Sum.thy [Part_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
    "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part(A,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
by (REPEAT (ares_tac [exI,CollectI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
val Part_eqI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
val PartI = refl RSN (2,Part_eqI);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
val major::prems = goalw Sum.thy [Part_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    "[| a : Part(A,h);  !!z. [| a : A;  a=h(z) |] ==> P  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
by (rtac (major RS CollectE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
by (etac exE 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
by (REPEAT (ares_tac prems 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
val PartE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
goalw Sum.thy [Part_def] "Part(A,h) <= A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
by (rtac Collect_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
val Part_subset = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
by (fast_tac (ZF_cs addIs [PartI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
val Part_mono = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
val Part_Inl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
goal Sum.thy "Part(A+B,Inr) = {Inr(y). y: B}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
by (fast_tac (sum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val Part_Inr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
goalw Sum.thy [Part_def] "!!a. a : Part(A,h) ==> a : A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
by (etac CollectD1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
val PartD1 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
goal Sum.thy "Part(A,%x.x) = A";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
by (fast_tac (ZF_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
val Part_id = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
goal Sum.thy "Part(A+B, %x.Inr(h(x))) = {Inr(y). y: Part(B,h)}";
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_Inr2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
goal Sum.thy "!!A B C. C <= A+B ==> Part(C,Inl) Un Part(C,Inr) = C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
by (rtac Un_least 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
by (fast_tac (ZF_cs addIs [PartI] addSEs [sumE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
val Part_sum_equality = result();