src/ZF/QPair.ML
author paulson
Fri, 11 Aug 2000 13:26:40 +0200
changeset 9577 9e66e8ed8237
parent 9211 6236c5285bd8
child 9907 473a6604da94
permissions -rw-r--r--
ZF arith
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1096
diff changeset
     1
(*  Title:      ZF/QPair.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1096
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
0
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
Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
structures in ZF.  Does not precisely follow Quine's construction.  Thanks
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
to Thomas Forster for suggesting this approach!
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
1966.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
Many proofs are borrowed from pair.ML and sum.ML
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
    is not a limit ordinal? 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
(**** Quine ordered pairing ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
(** Lemmas for showing that <a;b> uniquely determines a and b **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    23
Goalw [QPair_def] "<0;0> = 0";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    24
by (Simp_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    25
qed "QPair_empty";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    26
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    27
Goalw [QPair_def] "<a;b> = <c;d> <-> a=c & b=d";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    28
by (rtac sum_equal_iff 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    29
qed "QPair_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    31
bind_thm ("QPair_inject", QPair_iff RS iffD1 RS conjE);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    33
Addsimps [QPair_empty, QPair_iff];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    34
AddSEs   [QPair_inject];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    35
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    36
Goal "<a;b> = <c;d> ==> a=c";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    37
by (Blast_tac 1) ;
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    38
qed "QPair_inject1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    40
Goal "<a;b> = <c;d> ==> b=d";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    41
by (Blast_tac 1) ;
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    42
qed "QPair_inject2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
(*** QSigma: Disjoint union of a family of sets
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
     Generalizes Cartesian product ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    48
Goalw [QSigma_def] "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    49
by (Blast_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    50
qed "QSigmaI";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    51
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    52
AddSIs [QSigmaI];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
(*The general elimination rule*)
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    55
val major::prems= Goalw [QSigma_def] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
    "[| c: QSigma(A,B);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
\       !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P \
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    58
\    |] ==> P";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    59
by (cut_facts_tac [major] 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    60
by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    61
qed "QSigmaE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
val QSigmaE2 = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
  rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1096
diff changeset
    67
                  THEN prune_params_tac)
8551
5c22595bc599 tidied using new "inst" rule
paulson
parents: 6112
diff changeset
    68
      (inst "c" "<a;b>" QSigmaE);  
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    70
AddSEs [QSigmaE2, QSigmaE];
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    71
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    72
Goal "<a;b> : QSigma(A,B) ==> a : A";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    73
by (Blast_tac 1) ;
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    74
qed "QSigmaD1";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    76
Goal "<a;b> : QSigma(A,B) ==> b : B(a)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    77
by (Blast_tac 1) ;
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    78
qed "QSigmaD2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
744
2054fa3c8d76 tidied proofs, using fast_tac etc. as much as possible
lcp
parents: 516
diff changeset
    80
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    81
val prems= Goalw [QSigma_def] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    83
\    QSigma(A,B) = QSigma(A',B')";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    84
by (simp_tac (simpset() addsimps prems) 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
    85
qed "QSigma_cong";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    87
Goal "QSigma(0,B) = 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    88
by (Blast_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    89
qed "QSigma_empty1";
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
    90
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    91
Goal "A <*> 0 = 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    92
by (Blast_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
    93
qed "QSigma_empty2";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    94
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
    95
Addsimps [QSigma_empty1, QSigma_empty2];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
    97
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
    98
(*** Projections: qfst, qsnd ***)
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
    99
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   100
Goalw [qfst_def]  "qfst(<a;b>) = a";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   101
by (Blast_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   102
qed "qfst_conv";
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   103
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   104
Goalw [qsnd_def]  "qsnd(<a;b>) = b";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   105
by (Blast_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   106
qed "qsnd_conv";
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   107
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   108
Addsimps [qfst_conv, qsnd_conv];
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   109
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   110
Goal "p:QSigma(A,B) ==> qfst(p) : A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   111
by (Auto_tac) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   112
qed "qfst_type";
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   113
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   114
Goal "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   115
by (Auto_tac) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   116
qed "qsnd_type";
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   117
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
   118
Goal "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a";
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4091
diff changeset
   119
by Auto_tac;
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   120
qed "QPair_qfst_qsnd_eq";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
(*** Eliminator - qsplit ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   125
(*A META-equality, so that it applies to higher types as well...*)
6112
5e4871c5136b datatype package improvements
paulson
parents: 5505
diff changeset
   126
Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)";
5e4871c5136b datatype package improvements
paulson
parents: 5505
diff changeset
   127
by (Simp_tac 1);
5e4871c5136b datatype package improvements
paulson
parents: 5505
diff changeset
   128
qed "qsplit";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   129
Addsimps [qsplit];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   130
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   131
val major::prems= Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
    "[|  p:QSigma(A,B);   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
\        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   134
\    |] ==> qsplit(%x y. c(x,y), p) : C(p)";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   135
by (rtac (major RS QSigmaE) 1);
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   136
by (asm_simp_tac (simpset() addsimps prems) 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   137
qed "qsplit_type";
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   138
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   139
Goalw [qsplit_def]
5147
825877190618 More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5137
diff changeset
   140
 "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))";
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4091
diff changeset
   141
by Auto_tac;
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   142
qed "expand_qsplit";
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   143
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   144
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   145
(*** qsplit for predicates: result type o ***)
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   146
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
   147
Goalw [qsplit_def] "R(a,b) ==> qsplit(R, <a;b>)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   148
by (Asm_simp_tac 1);
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   149
qed "qsplitI";
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   150
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   151
val major::sigma::prems = Goalw [qsplit_def]
1461
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1096
diff changeset
   152
    "[| qsplit(R,z);  z:QSigma(A,B);                    \
6bcb44e4d6e5 expanded tabs
clasohm
parents: 1096
diff changeset
   153
\       !!x y. [| z = <x;y>;  R(x,y) |] ==> P           \
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   154
\   |] ==> P";
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   155
by (rtac (sigma RS QSigmaE) 1);
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   156
by (cut_facts_tac [major] 1);
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   157
by (REPEAT (ares_tac prems 1));
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   158
by (Asm_full_simp_tac 1);
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   159
qed "qsplitE";
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   160
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
   161
Goalw [qsplit_def] "qsplit(R,<a;b>) ==> R(a,b)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   162
by (Asm_full_simp_tac 1);
1096
6c177c4c2127 Modified proofs for (q)split, fst, snd for new
lcp
parents: 790
diff changeset
   163
qed "qsplitD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   164
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(*** qconverse ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   168
Goalw [qconverse_def] "<a;b>:r ==> <b;a>:qconverse(r)";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   169
by (Blast_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   170
qed "qconverseI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   172
Goalw [qconverse_def] "<a;b> : qconverse(r) ==> <b;a> : r";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   173
by (Blast_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   174
qed "qconverseD";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   176
val [major,minor]= Goalw [qconverse_def] 
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
    "[| yx : qconverse(r);  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   178
\       !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P \
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   179
\    |] ==> P";
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   180
by (rtac (major RS ReplaceE) 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   181
by (REPEAT (eresolve_tac [exE, conjE, minor] 1));
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   182
by (hyp_subst_tac 1);
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   183
by (assume_tac 1) ;
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   184
qed "qconverseE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   185
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   186
AddSIs [qconverseI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   187
AddSEs [qconverseD, qconverseE];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   189
Goal "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   190
by (Blast_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   191
qed "qconverse_qconverse";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   192
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   193
Goal "r <= A <*> B ==> qconverse(r) <= B <*> A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   194
by (Blast_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   195
qed "qconverse_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   197
Goal "qconverse(A <*> B) = B <*> A";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   198
by (Blast_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   199
qed "qconverse_prod";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
9180
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   201
Goal "qconverse(0) = 0";
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   202
by (Blast_tac 1) ;
3bda56c0d70d tidying and unbatchifying
paulson
parents: 8551
diff changeset
   203
qed "qconverse_empty";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   204
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   205
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
(**** The Quine-inspired notion of disjoint sum ****)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   208
val qsum_defs = [qsum_def,QInl_def,QInr_def,qcase_def];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
(** Introduction rules for the injections **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
   212
Goalw qsum_defs "a : A ==> QInl(a) : A <+> B";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   213
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   214
qed "QInlI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
   216
Goalw qsum_defs "b : B ==> QInr(b) : A <+> B";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   217
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   218
qed "QInrI";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   219
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   220
(** Elimination rules **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   221
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   222
val major::prems = Goalw qsum_defs
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
    "[| u: A <+> B;  \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
\       !!x. [| x:A;  u=QInl(x) |] ==> P; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
\       !!y. [| y:B;  u=QInr(y) |] ==> P \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
\    |] ==> P";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
by (rtac (major RS UnE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
by (REPEAT (rtac refl 1
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
     ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   230
qed "qsumE";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   231
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   232
AddSIs [QInlI, QInrI];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   233
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   234
(** Injection and freeness equivalences, for rewriting **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   235
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   236
Goalw qsum_defs "QInl(a)=QInl(b) <-> a=b";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   237
by (Simp_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   238
qed "QInl_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   239
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   240
Goalw qsum_defs "QInr(a)=QInr(b) <-> a=b";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   241
by (Simp_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   242
qed "QInr_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   243
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   244
Goalw qsum_defs "QInl(a)=QInr(b) <-> False";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   245
by (Simp_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   246
qed "QInl_QInr_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   247
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   248
Goalw qsum_defs "QInr(b)=QInl(a) <-> False";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   249
by (Simp_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   250
qed "QInr_QInl_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   251
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   252
Goalw qsum_defs "0<+>0 = 0";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   253
by (Simp_tac 1);
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   254
qed "qsum_empty";
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   255
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   256
(*Injection and freeness rules*)
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   257
782
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   258
bind_thm ("QInl_inject", (QInl_iff RS iffD1));
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   259
bind_thm ("QInr_inject", (QInr_iff RS iffD1));
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   260
bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE));
200a16083201 added bind_thm for theorems defined by "standard ..."
clasohm
parents: 760
diff changeset
   261
bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE));
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   262
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   263
AddSEs [qsumE, QInl_neq_QInr, QInr_neq_QInl];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   264
AddSDs [QInl_inject, QInr_inject];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   265
Addsimps [QInl_iff, QInr_iff, QInl_QInr_iff, QInr_QInl_iff, qsum_empty];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
   267
Goal "QInl(a): A<+>B ==> a: A";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   268
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   269
qed "QInlD";
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   270
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
   271
Goal "QInr(b): A<+>B ==> b: B";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   272
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   273
qed "QInrD";
55
331d93292ee0 ZF/ind-syntax/refl_thin: new
lcp
parents: 6
diff changeset
   274
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   275
(** <+> is itself injective... who cares?? **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
5268
59ef39008514 even more tidying of Goal commands
paulson
parents: 5147
diff changeset
   277
Goal "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   278
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   279
qed "qsum_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   281
Goal "A <+> B <= C <+> D <-> A<=C & B<=D";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   282
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   283
qed "qsum_subset_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   285
Goal "A <+> B = C <+> D <-> A=C & B=D";
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   286
by (simp_tac (simpset() addsimps [extension,qsum_subset_iff]) 1);
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   287
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   288
qed "qsum_equal_iff";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
(*** Eliminator -- qcase ***)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   292
Goalw qsum_defs "qcase(c, d, QInl(a)) = c(a)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   293
by (Simp_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   294
qed "qcase_QInl";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   296
Goalw qsum_defs "qcase(c, d, QInr(b)) = d(b)";
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   297
by (Simp_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   298
qed "qcase_QInr";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   300
Addsimps [qcase_QInl, qcase_QInr];
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 1461
diff changeset
   301
9211
6236c5285bd8 removal of batch-style proofs
paulson
parents: 9180
diff changeset
   302
val major::prems = Goal
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
    "[| u: A <+> B; \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   304
\       !!x. x: A ==> c(x): C(QInl(x));   \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   305
\       !!y. y: B ==> d(y): C(QInr(y)) \
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   306
\    |] ==> qcase(c,d,u) : C(u)";
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
by (rtac (major RS qsumE) 1);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
by (ALLGOALS (etac ssubst));
4091
771b1f6422a8 isatool fixclasimp;
wenzelm
parents: 3840
diff changeset
   309
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   310
qed "qcase_type";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
(** Rules for the Part primitive **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   314
Goal "Part(A <+> B,QInl) = {QInl(x). x: A}";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   315
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   316
qed "Part_QInl";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   318
Goal "Part(A <+> B,QInr) = {QInr(y). y: B}";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   319
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   320
qed "Part_QInr";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
5067
62b6288e6005 isatool fixgoal;
wenzelm
parents: 4477
diff changeset
   322
Goal "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   323
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   324
qed "Part_QInr2";
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
5137
60205b0de9b9 Huge tidy-up: removal of leading \!\!
paulson
parents: 5067
diff changeset
   326
Goal "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
3016
15763781afb0 Conversion to use blast_tac
paulson
parents: 2493
diff changeset
   327
by (Blast_tac 1);
760
f0200e91b272 added qed and qed_goal[w]
clasohm
parents: 744
diff changeset
   328
qed "Part_qsum_equality";