src/ZF/qpair.ML
author lcp
Fri, 17 Sep 1993 16:16:38 +0200
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
child 55 331d93292ee0
permissions -rw-r--r--
Installation of new simplifier for ZF. Deleted all congruence rules not involving local assumptions. NB the congruence rules for Sigma and Pi (dependent type constructions) cause difficulties and are not used by default.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	ZF/qpair.ML
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   1993  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
For qpair.thy.  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
structures in ZF.  Does not precisely follow Quine's construction.  Thanks
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
to Thomas Forster for suggesting this approach!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
1966.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
Many proofs are borrowed from pair.ML and sum.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
    is not a limit ordinal? 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
open QPair;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
(**** Quine ordered pairing ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
(** Lemmas for showing that <a;b> uniquely determines a and b **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
val QPair_iff = prove_goalw QPair.thy [QPair_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
    "<a;b> = <c;d> <-> a=c & b=d"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
 (fn _=> [rtac sum_equal_iff 1]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
val QPair_inject = standard (QPair_iff RS iffD1 RS conjE);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
val QPair_inject1 = prove_goal QPair.thy "<a;b> = <c;d> ==> a=c"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
  [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
val QPair_inject2 = prove_goal QPair.thy "<a;b> = <c;d> ==> b=d"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  [ (rtac (major RS QPair_inject) 1), (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
(*** QSigma: Disjoint union of a family of sets
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
     Generalizes Cartesian product ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
val QSigmaI = prove_goalw QPair.thy [QSigma_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
    "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
 (fn prems=> [ (REPEAT (resolve_tac (prems@[singletonI,UN_I]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
(*The general elimination rule*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
val QSigmaE = prove_goalw QPair.thy [QSigma_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
    "[| c: QSigma(A,B);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
\       !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
  [ (cut_facts_tac [major] 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
    (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
val QSigmaE2 = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
		  THEN prune_params_tac)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
      (read_instantiate [("c","<a;b>")] QSigmaE);  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
val QSigmaD1 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> a : A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
val QSigmaD2 = prove_goal QPair.thy "<a;b> : QSigma(A,B) ==> b : B(a)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
 (fn [major]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
  [ (rtac (major RS QSigmaE2) 1), (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
val QSigma_cong = prove_goalw QPair.thy [QSigma_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
\    QSigma(A,B) = QSigma(A',B')"
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
    77
 (fn prems=> [ (simp_tac (ZF_ss addsimps prems) 1) ]);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
val QSigma_empty1 = prove_goal QPair.thy "QSigma(0,B) = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
 (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
val QSigma_empty2 = prove_goal QPair.thy "A <*> 0 = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
 (fn _ => [ (fast_tac (ZF_cs addIs [equalityI] addSEs [QSigmaE]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
(*** Eliminator - qsplit ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
val qsplit = prove_goalw QPair.thy [qsplit_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
    "qsplit(%x y.c(x,y), <a;b>) = c(a,b)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
 (fn _ => [ (fast_tac (ZF_cs addIs [the_equality] addEs [QPair_inject]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
val qsplit_type = prove_goal QPair.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
    "[|  p:QSigma(A,B);   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
\        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
\    |] ==> qsplit(%x y.c(x,y), p) : C(p)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
 (fn major::prems=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  [ (rtac (major RS QSigmaE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
    (etac ssubst 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
    (REPEAT (ares_tac (prems @ [qsplit RS ssubst]) 1)) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
val qpair_cs = ZF_cs addSIs [QSigmaI] addSEs [QSigmaE2, QSigmaE, QPair_inject];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
(*** qconverse ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
val qconverseI = prove_goalw QPair.thy [qconverse_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
    "!!a b r. <a;b>:r ==> <b;a>:qconverse(r)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
 (fn _ => [ (fast_tac qpair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
val qconverseD = prove_goalw QPair.thy [qconverse_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
    "!!a b r. <a;b> : qconverse(r) ==> <b;a> : r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
 (fn _ => [ (fast_tac qpair_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
val qconverseE = prove_goalw QPair.thy [qconverse_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
    "[| yx : qconverse(r);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
\       !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
\    |] ==> P"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
 (fn [major,minor]=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
  [ (rtac (major RS ReplaceE) 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
    (REPEAT (eresolve_tac [exE, conjE, minor] 1)),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
    (hyp_subst_tac 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
    (assume_tac 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
val qconverse_cs = qpair_cs addSIs [qconverseI] 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
			    addSEs [qconverseD,qconverseE];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
val qconverse_of_qconverse = prove_goal QPair.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
    "!!A B r. r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
 (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
val qconverse_type = prove_goal QPair.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
    "!!A B r. r <= A <*> B ==> qconverse(r) <= B <*> A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
 (fn _ => [ (fast_tac qconverse_cs 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
val qconverse_of_prod = prove_goal QPair.thy "qconverse(A <*> B) = B <*> A"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
 (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
val qconverse_empty = prove_goal QPair.thy "qconverse(0) = 0"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
 (fn _ => [ (fast_tac (qconverse_cs addSIs [equalityI]) 1) ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
(*** qsplit for predicates: result type o ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
goalw QPair.thy [qfsplit_def] "!!R a b. R(a,b) ==> qfsplit(R, <a;b>)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
by (REPEAT (ares_tac [refl,exI,conjI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
val qfsplitI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
val major::prems = goalw QPair.thy [qfsplit_def]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
    "[| qfsplit(R,z);  !!x y. [| z = <x;y>;  R(x,y) |] ==> P |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
by (cut_facts_tac [major] 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
by (REPEAT (eresolve_tac (prems@[asm_rl,exE,conjE]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
val qfsplitE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
goal QPair.thy "!!R a b. qfsplit(R,<a;b>) ==> R(a,b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
by (REPEAT (eresolve_tac [asm_rl,qfsplitE,QPair_inject,ssubst] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
val qfsplitD = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   159
(**** The Quine-inspired notion of disjoint sum ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   160
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   161
val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   162
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   163
(** Introduction rules for the injections **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
goalw QPair.thy qsum_defs "!!a A B. a : A ==> QInl(a) : A <+> B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
by (REPEAT (ares_tac [UnI1,QSigmaI,singletonI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
val QInlI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
goalw QPair.thy qsum_defs "!!b A B. b : B ==> QInr(b) : A <+> B";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
by (REPEAT (ares_tac [UnI2,QSigmaI,singletonI] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
val QInrI = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
(** Elimination rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
val major::prems = goalw QPair.thy qsum_defs
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
    "[| u: A <+> B;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
\       !!x. [| x:A;  u=QInl(x) |] ==> P; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
\       !!y. [| y:B;  u=QInr(y) |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
by (rtac (major RS UnE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   181
by (REPEAT (rtac refl 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   182
     ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
val qsumE = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   184
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
(** QInjection and freeness rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInl(b) ==> a=b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
val QInl_inject = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   191
val [major] = goalw QPair.thy qsum_defs "QInr(a)=QInr(b) ==> a=b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   192
by (EVERY1 [rtac (major RS QPair_inject), assume_tac]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
val QInr_inject = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   195
val [major] = goalw QPair.thy qsum_defs "QInl(a)=QInr(b) ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
by (rtac (major RS QPair_inject) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
by (etac (sym RS one_neq_0) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
val QInl_neq_QInr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   199
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
val QInr_neq_QInl = sym RS QInl_neq_QInr;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
(** Injection and freeness equivalences, for rewriting **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   203
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
goal QPair.thy "QInl(a)=QInl(b) <-> a=b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
by (REPEAT (eresolve_tac [QInl_inject,subst_context] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
val QInl_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
goal QPair.thy "QInr(a)=QInr(b) <-> a=b";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
by (REPEAT (eresolve_tac [QInr_inject,subst_context] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
val QInr_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   214
goal QPair.thy "QInl(a)=QInr(b) <-> False";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   216
by (REPEAT (eresolve_tac [QInl_neq_QInr,FalseE] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   217
val QInl_QInr_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
goal QPair.thy "QInr(b)=QInl(a) <-> False";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
by (rtac iffI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
by (REPEAT (eresolve_tac [QInr_neq_QInl,FalseE] 1));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
val QInr_QInl_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
val qsum_cs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
    ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
          addSDs [QInl_inject,QInr_inject];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
(** <+> is itself injective... who cares?? **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
goal QPair.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
    "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
by (fast_tac qsum_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
val qsum_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
goal QPair.thy "A <+> B <= C <+> D <-> A<=C & B<=D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
by (fast_tac qsum_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
val qsum_subset_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
goal QPair.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
   240
by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
val qsum_equal_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
(*** Eliminator -- qcase ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
goalw QPair.thy qsum_defs "qcase(c, d, QInl(a)) = c(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
by (rtac (qsplit RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
by (rtac cond_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
val qcase_QInl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
by (rtac (qsplit RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
by (rtac cond_1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
val qcase_QInr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
val major::prems = goal QPair.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   257
    "[| u: A <+> B; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
\       !!x. x: A ==> c(x): C(QInl(x));   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
\       !!y. y: B ==> d(y): C(QInr(y)) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
\    |] ==> qcase(c,d,u) : C(u)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
by (rtac (major RS qsumE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
by (ALLGOALS (etac ssubst));
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   263
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
			    (prems@[qcase_QInl,qcase_QInr]))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
val qcase_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
(** Rules for the Part primitive **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
val Part_QInl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
val Part_QInr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
val Part_QInr2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
by (rtac Un_least 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   286
by (fast_tac (ZF_cs addIs [PartI] addSEs [qsumE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
val Part_qsum_equality = result();