src/ZF/qpair.ML
author paulson
Fri, 16 Feb 1996 18:00:47 +0100
changeset 1512 ce37c64244c0
parent 55 331d93292ee0
permissions -rw-r--r--
Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
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
(** Injection and freeness equivalences, for rewriting **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   186
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   187
goalw QPair.thy qsum_defs "QInl(a)=QInl(b) <-> a=b";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   188
by (simp_tac (ZF_ss addsimps [QPair_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   189
val QInl_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   190
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   191
goalw QPair.thy qsum_defs "QInr(a)=QInr(b) <-> a=b";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   192
by (simp_tac (ZF_ss addsimps [QPair_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   193
val QInr_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   194
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   195
goalw QPair.thy qsum_defs "QInl(a)=QInr(b) <-> False";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   196
by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0 RS not_sym]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
val QInl_QInr_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   199
goalw QPair.thy qsum_defs "QInr(b)=QInl(a) <-> False";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   200
by (simp_tac (ZF_ss addsimps [QPair_iff, one_not_0]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   201
val QInr_QInl_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   203
(*Injection and freeness rules*)
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   204
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   205
val QInl_inject = standard (QInl_iff RS iffD1);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   206
val QInr_inject = standard (QInr_iff RS iffD1);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   207
val QInl_neq_QInr = standard (QInl_QInr_iff RS iffD1 RS FalseE);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   208
val QInr_neq_QInl = standard (QInr_QInl_iff RS iffD1 RS FalseE);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   209
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
val qsum_cs = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
    ZF_cs addIs [QInlI,QInrI] addSEs [qsumE,QInl_neq_QInr,QInr_neq_QInl]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
          addSDs [QInl_inject,QInr_inject];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   214
goal QPair.thy "!!A B. QInl(a): A<+>B ==> a: A";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   215
by (fast_tac qsum_cs 1);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   216
val QInlD = result();
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   217
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   218
goal QPair.thy "!!A B. QInr(b): A<+>B ==> b: B";
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   219
by (fast_tac qsum_cs 1);
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   220
val QInrD = result();
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   221
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   222
(** <+> is itself injective... who cares?? **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
goal QPair.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
    "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
by (fast_tac qsum_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
val qsum_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
goal QPair.thy "A <+> B <= C <+> D <-> A<=C & B<=D";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
by (fast_tac qsum_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
val qsum_subset_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   232
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   233
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
   234
by (simp_tac (ZF_ss addsimps [extension,qsum_subset_iff]) 1);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
by (fast_tac ZF_cs 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   236
val qsum_equal_iff = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   237
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   238
(*** Eliminator -- qcase ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   240
goalw QPair.thy qsum_defs "qcase(c, d, QInl(a)) = c(a)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   241
by (rtac (qsplit RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   242
by (rtac cond_0 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
val qcase_QInl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   244
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   245
goalw QPair.thy qsum_defs "qcase(c, d, QInr(b)) = d(b)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   246
by (rtac (qsplit RS trans) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
by (rtac cond_1 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   248
val qcase_QInr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   249
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   250
val major::prems = goal QPair.thy
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
    "[| u: A <+> B; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   252
\       !!x. x: A ==> c(x): C(QInl(x));   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   253
\       !!y. y: B ==> d(y): C(QInr(y)) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   254
\    |] ==> qcase(c,d,u) : C(u)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   255
by (rtac (major RS qsumE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
by (ALLGOALS (etac ssubst));
6
8ce8c4d13d4d Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents: 0
diff changeset
   257
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
			    (prems@[qcase_QInl,qcase_QInr]))));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
val qcase_type = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
(** Rules for the Part primitive **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
goal QPair.thy "Part(A <+> B,QInl) = {QInl(x). x: A}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   265
val Part_QInl = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
goal QPair.thy "Part(A <+> B,QInr) = {QInr(y). y: B}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   269
val Part_QInr = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   270
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
goal QPair.thy "Part(A <+> B, %x.QInr(h(x))) = {QInr(y). y: Part(B,h)}";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
by (fast_tac (qsum_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
val Part_QInr2 = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
goal QPair.thy "!!A B C. C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
by (rtac equalityI 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
by (rtac Un_least 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
by (rtac Part_subset 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
by (fast_tac (ZF_cs addIs [PartI] addSEs [qsumE]) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
val Part_qsum_equality = result();