src/ZF/QPair.thy
author paulson
Tue Jul 02 22:46:23 2002 +0200 (2002-07-02)
changeset 13285 28d1823ce0f2
parent 13259 01fa0c8dbc92
child 13356 c9cfe1638bf2
permissions -rw-r--r--
conversion of QPair to Isar
clasohm@1478
     1
(*  Title:      ZF/qpair.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
clasohm@0
     7
structures in ZF.  Does not precisely follow Quine's construction.  Thanks
clasohm@0
     8
to Thomas Forster for suggesting this approach!
clasohm@0
     9
clasohm@0
    10
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
clasohm@0
    11
1966.
paulson@13285
    12
paulson@13285
    13
Many proofs are borrowed from pair.thy and sum.thy
paulson@13285
    14
paulson@13285
    15
Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
paulson@13285
    16
    is not a limit ordinal? 
clasohm@0
    17
*)
clasohm@0
    18
paulson@13285
    19
theory QPair = Sum + mono:
paulson@13285
    20
paulson@13285
    21
constdefs
paulson@13285
    22
  QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
paulson@13285
    23
    "<a;b> == a+b"
wenzelm@3923
    24
paulson@13285
    25
  qfst :: "i => i"
paulson@13285
    26
    "qfst(p) == THE a. EX b. p=<a;b>"
paulson@13285
    27
paulson@13285
    28
  qsnd :: "i => i"
paulson@13285
    29
    "qsnd(p) == THE b. EX a. p=<a;b>"
paulson@13285
    30
paulson@13220
    31
  qsplit    :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
paulson@13285
    32
    "qsplit(c,p) == c(qfst(p), qsnd(p))"
clasohm@0
    33
paulson@13285
    34
  qconverse :: "i => i"
paulson@13285
    35
    "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
paulson@13285
    36
paulson@13285
    37
  QSigma    :: "[i, i => i] => i"
paulson@13285
    38
    "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
clasohm@0
    39
lcp@929
    40
syntax
paulson@13220
    41
  "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
paulson@13220
    42
  "<*>"     :: "[i, i] => i"                      (infixr 80)
lcp@929
    43
clasohm@0
    44
translations
clasohm@0
    45
  "QSUM x:A. B"  => "QSigma(A, %x. B)"
wenzelm@44
    46
  "A <*> B"      => "QSigma(A, _K(B))"
clasohm@0
    47
paulson@13285
    48
constdefs
paulson@13285
    49
  qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)
paulson@13285
    50
    "A <+> B      == ({0} <*> A) Un ({1} <*> B)"
wenzelm@3923
    51
paulson@13285
    52
  QInl :: "i=>i"
paulson@13285
    53
    "QInl(a)      == <0;a>"
paulson@13285
    54
paulson@13285
    55
  QInr :: "i=>i"
paulson@13285
    56
    "QInr(b)      == <1;b>"
paulson@13285
    57
paulson@13285
    58
  qcase     :: "[i=>i, i=>i, i]=>i"
paulson@13285
    59
    "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
paulson@13285
    60
paulson@13285
    61
paulson@13285
    62
print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
paulson@13285
    63
paulson@13285
    64
paulson@13285
    65
(**** Quine ordered pairing ****)
paulson@13285
    66
paulson@13285
    67
(** Lemmas for showing that <a;b> uniquely determines a and b **)
paulson@13285
    68
paulson@13285
    69
lemma QPair_empty [simp]: "<0;0> = 0"
paulson@13285
    70
by (simp add: QPair_def)
paulson@13285
    71
paulson@13285
    72
lemma QPair_iff [simp]: "<a;b> = <c;d> <-> a=c & b=d"
paulson@13285
    73
apply (simp add: QPair_def)
paulson@13285
    74
apply (rule sum_equal_iff)
paulson@13285
    75
done
paulson@13285
    76
paulson@13285
    77
lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!]
paulson@13285
    78
paulson@13285
    79
lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
paulson@13285
    80
by blast
paulson@13285
    81
paulson@13285
    82
lemma QPair_inject2: "<a;b> = <c;d> ==> b=d"
paulson@13285
    83
by blast
paulson@13285
    84
paulson@13285
    85
paulson@13285
    86
(*** QSigma: Disjoint union of a family of sets
paulson@13285
    87
     Generalizes Cartesian product ***)
paulson@13285
    88
paulson@13285
    89
lemma QSigmaI [intro!]: "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
paulson@13285
    90
by (simp add: QSigma_def)
paulson@13285
    91
paulson@13285
    92
paulson@13285
    93
(*The general elimination rule*)
paulson@13285
    94
lemma QSigmaE:
paulson@13285
    95
    "[| c: QSigma(A,B);   
paulson@13285
    96
        !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
paulson@13285
    97
     |] ==> P"
paulson@13285
    98
apply (simp add: QSigma_def, blast) 
paulson@13285
    99
done
paulson@13285
   100
paulson@13285
   101
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
paulson@13285
   102
paulson@13285
   103
lemma QSigmaE [elim!]:
paulson@13285
   104
    "[| c: QSigma(A,B);   
paulson@13285
   105
        !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
paulson@13285
   106
     |] ==> P"
paulson@13285
   107
apply (simp add: QSigma_def, blast) 
paulson@13285
   108
done
paulson@13285
   109
paulson@13285
   110
lemma QSigmaE2 [elim!]:
paulson@13285
   111
    "[| <a;b>: QSigma(A,B); [| a:A;  b:B(a) |] ==> P |] ==> P"
paulson@13285
   112
by (simp add: QSigma_def) 
paulson@13285
   113
paulson@13285
   114
lemma QSigmaD1: "<a;b> : QSigma(A,B) ==> a : A"
paulson@13285
   115
by blast
paulson@13285
   116
paulson@13285
   117
lemma QSigmaD2: "<a;b> : QSigma(A,B) ==> b : B(a)"
paulson@13285
   118
by blast
paulson@13285
   119
paulson@13285
   120
lemma QSigma_cong:
paulson@13285
   121
    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
paulson@13285
   122
     QSigma(A,B) = QSigma(A',B')"
paulson@13285
   123
by (simp add: QSigma_def) 
paulson@13285
   124
paulson@13285
   125
lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0"
paulson@13285
   126
by blast
paulson@13285
   127
paulson@13285
   128
lemma QSigma_empty2 [simp]: "A <*> 0 = 0"
paulson@13285
   129
by blast
paulson@13285
   130
paulson@13285
   131
paulson@13285
   132
(*** Projections: qfst, qsnd ***)
paulson@13285
   133
paulson@13285
   134
lemma qfst_conv [simp]: "qfst(<a;b>) = a"
paulson@13285
   135
by (simp add: qfst_def, blast)
paulson@13285
   136
paulson@13285
   137
lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
paulson@13285
   138
by (simp add: qsnd_def, blast)
paulson@13285
   139
paulson@13285
   140
lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A"
paulson@13285
   141
by auto
paulson@13285
   142
paulson@13285
   143
lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
paulson@13285
   144
by auto
paulson@13285
   145
paulson@13285
   146
lemma QPair_qfst_qsnd_eq: "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
paulson@13285
   147
by auto
paulson@13285
   148
paulson@13285
   149
paulson@13285
   150
(*** Eliminator - qsplit ***)
paulson@13285
   151
paulson@13285
   152
(*A META-equality, so that it applies to higher types as well...*)
paulson@13285
   153
lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
paulson@13285
   154
by (simp add: qsplit_def)
paulson@13285
   155
paulson@13285
   156
paulson@13285
   157
lemma qsplit_type [elim!]:
paulson@13285
   158
    "[|  p:QSigma(A,B);    
paulson@13285
   159
         !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>)  
paulson@13285
   160
     |] ==> qsplit(%x y. c(x,y), p) : C(p)"
paulson@13285
   161
by auto 
paulson@13285
   162
paulson@13285
   163
lemma expand_qsplit: 
paulson@13285
   164
 "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))"
paulson@13285
   165
apply (simp add: qsplit_def, auto)
paulson@13285
   166
done
paulson@13285
   167
paulson@13285
   168
paulson@13285
   169
(*** qsplit for predicates: result type o ***)
paulson@13285
   170
paulson@13285
   171
lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
paulson@13285
   172
by (simp add: qsplit_def)
paulson@13285
   173
paulson@13285
   174
paulson@13285
   175
lemma qsplitE:
paulson@13285
   176
    "[| qsplit(R,z);  z:QSigma(A,B);                     
paulson@13285
   177
        !!x y. [| z = <x;y>;  R(x,y) |] ==> P            
paulson@13285
   178
    |] ==> P"
paulson@13285
   179
apply (simp add: qsplit_def, auto) 
paulson@13285
   180
done
paulson@13285
   181
paulson@13285
   182
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
paulson@13285
   183
by (simp add: qsplit_def)
paulson@13285
   184
paulson@13285
   185
paulson@13285
   186
(*** qconverse ***)
paulson@13285
   187
paulson@13285
   188
lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
paulson@13285
   189
by (simp add: qconverse_def, blast)
paulson@13285
   190
paulson@13285
   191
lemma qconverseD [elim!]: "<a;b> : qconverse(r) ==> <b;a> : r"
paulson@13285
   192
by (simp add: qconverse_def, blast)
paulson@13285
   193
paulson@13285
   194
lemma qconverseE [elim!]:
paulson@13285
   195
    "[| yx : qconverse(r);   
paulson@13285
   196
        !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P  
paulson@13285
   197
     |] ==> P"
paulson@13285
   198
apply (simp add: qconverse_def, blast) 
paulson@13285
   199
done
paulson@13285
   200
paulson@13285
   201
lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
paulson@13285
   202
by blast
paulson@13285
   203
paulson@13285
   204
lemma qconverse_type: "r <= A <*> B ==> qconverse(r) <= B <*> A"
paulson@13285
   205
by blast
paulson@13285
   206
paulson@13285
   207
lemma qconverse_prod: "qconverse(A <*> B) = B <*> A"
paulson@13285
   208
by blast
paulson@13285
   209
paulson@13285
   210
lemma qconverse_empty: "qconverse(0) = 0"
paulson@13285
   211
by blast
paulson@13285
   212
paulson@13285
   213
paulson@13285
   214
(**** The Quine-inspired notion of disjoint sum ****)
paulson@13285
   215
paulson@13285
   216
lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
paulson@13285
   217
paulson@13285
   218
(** Introduction rules for the injections **)
paulson@13285
   219
paulson@13285
   220
lemma QInlI [intro!]: "a : A ==> QInl(a) : A <+> B"
paulson@13285
   221
by (simp add: qsum_defs, blast)
lcp@1097
   222
paulson@13285
   223
lemma QInrI [intro!]: "b : B ==> QInr(b) : A <+> B"
paulson@13285
   224
by (simp add: qsum_defs, blast)
paulson@13285
   225
paulson@13285
   226
(** Elimination rules **)
paulson@13285
   227
paulson@13285
   228
lemma qsumE [elim!]:
paulson@13285
   229
    "[| u: A <+> B;   
paulson@13285
   230
        !!x. [| x:A;  u=QInl(x) |] ==> P;  
paulson@13285
   231
        !!y. [| y:B;  u=QInr(y) |] ==> P  
paulson@13285
   232
     |] ==> P"
paulson@13285
   233
apply (simp add: qsum_defs, blast) 
paulson@13285
   234
done
paulson@13285
   235
paulson@13285
   236
paulson@13285
   237
(** Injection and freeness equivalences, for rewriting **)
paulson@13285
   238
paulson@13285
   239
lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b"
paulson@13285
   240
by (simp add: qsum_defs )
paulson@13285
   241
paulson@13285
   242
lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
paulson@13285
   243
by (simp add: qsum_defs )
paulson@13285
   244
paulson@13285
   245
lemma QInl_QInr_iff [iff]: "QInl(a)=QInr(b) <-> False"
paulson@13285
   246
by (simp add: qsum_defs )
paulson@13285
   247
paulson@13285
   248
lemma QInr_QInl_iff [iff]: "QInr(b)=QInl(a) <-> False"
paulson@13285
   249
by (simp add: qsum_defs )
paulson@13285
   250
paulson@13285
   251
lemma qsum_empty [simp]: "0<+>0 = 0"
paulson@13285
   252
by (simp add: qsum_defs )
paulson@13285
   253
paulson@13285
   254
(*Injection and freeness rules*)
paulson@13285
   255
paulson@13285
   256
lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
paulson@13285
   257
lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
paulson@13285
   258
lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE]
paulson@13285
   259
lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE]
paulson@13285
   260
paulson@13285
   261
lemma QInlD: "QInl(a): A<+>B ==> a: A"
paulson@13285
   262
by blast
paulson@13285
   263
paulson@13285
   264
lemma QInrD: "QInr(b): A<+>B ==> b: B"
paulson@13285
   265
by blast
paulson@13285
   266
paulson@13285
   267
(** <+> is itself injective... who cares?? **)
paulson@13285
   268
paulson@13285
   269
lemma qsum_iff:
paulson@13285
   270
     "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"
paulson@13285
   271
apply blast
paulson@13285
   272
done
paulson@13285
   273
paulson@13285
   274
lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D"
paulson@13285
   275
by blast
paulson@13285
   276
paulson@13285
   277
lemma qsum_equal_iff: "A <+> B = C <+> D <-> A=C & B=D"
paulson@13285
   278
apply (simp (no_asm) add: extension qsum_subset_iff)
paulson@13285
   279
apply blast
paulson@13285
   280
done
paulson@13285
   281
paulson@13285
   282
(*** Eliminator -- qcase ***)
paulson@13285
   283
paulson@13285
   284
lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
paulson@13285
   285
by (simp add: qsum_defs )
paulson@13285
   286
paulson@13285
   287
paulson@13285
   288
lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)"
paulson@13285
   289
by (simp add: qsum_defs )
paulson@13285
   290
paulson@13285
   291
lemma qcase_type:
paulson@13285
   292
    "[| u: A <+> B;  
paulson@13285
   293
        !!x. x: A ==> c(x): C(QInl(x));    
paulson@13285
   294
        !!y. y: B ==> d(y): C(QInr(y))  
paulson@13285
   295
     |] ==> qcase(c,d,u) : C(u)"
paulson@13285
   296
apply (simp add: qsum_defs , auto) 
paulson@13285
   297
done
paulson@13285
   298
paulson@13285
   299
(** Rules for the Part primitive **)
paulson@13285
   300
paulson@13285
   301
lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x: A}"
paulson@13285
   302
by blast
paulson@13285
   303
paulson@13285
   304
lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y: B}"
paulson@13285
   305
by blast
paulson@13285
   306
paulson@13285
   307
lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}"
paulson@13285
   308
by blast
clasohm@0
   309
paulson@13285
   310
lemma Part_qsum_equality: "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"
paulson@13285
   311
by blast
paulson@13285
   312
paulson@13285
   313
paulson@13285
   314
(*** Monotonicity ***)
paulson@13285
   315
paulson@13285
   316
lemma QPair_mono: "[| a<=c;  b<=d |] ==> <a;b> <= <c;d>"
paulson@13285
   317
by (simp add: QPair_def sum_mono)
paulson@13285
   318
paulson@13285
   319
lemma QSigma_mono [rule_format]:
paulson@13285
   320
     "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==> QSigma(A,B) <= QSigma(C,D)"
paulson@13285
   321
by blast
paulson@13285
   322
paulson@13285
   323
lemma QInl_mono: "a<=b ==> QInl(a) <= QInl(b)"
paulson@13285
   324
by (simp add: QInl_def subset_refl [THEN QPair_mono])
paulson@13285
   325
paulson@13285
   326
lemma QInr_mono: "a<=b ==> QInr(a) <= QInr(b)"
paulson@13285
   327
by (simp add: QInr_def subset_refl [THEN QPair_mono])
paulson@13285
   328
paulson@13285
   329
lemma qsum_mono: "[| A<=C;  B<=D |] ==> A <+> B <= C <+> D"
paulson@13285
   330
by blast
paulson@13285
   331
paulson@13285
   332
ML
paulson@13285
   333
{*
paulson@13285
   334
val qsum_defs = thms "qsum_defs";
paulson@13285
   335
paulson@13285
   336
val QPair_empty = thm "QPair_empty";
paulson@13285
   337
val QPair_iff = thm "QPair_iff";
paulson@13285
   338
val QPair_inject = thm "QPair_inject";
paulson@13285
   339
val QPair_inject1 = thm "QPair_inject1";
paulson@13285
   340
val QPair_inject2 = thm "QPair_inject2";
paulson@13285
   341
val QSigmaI = thm "QSigmaI";
paulson@13285
   342
val QSigmaE = thm "QSigmaE";
paulson@13285
   343
val QSigmaE = thm "QSigmaE";
paulson@13285
   344
val QSigmaE2 = thm "QSigmaE2";
paulson@13285
   345
val QSigmaD1 = thm "QSigmaD1";
paulson@13285
   346
val QSigmaD2 = thm "QSigmaD2";
paulson@13285
   347
val QSigma_cong = thm "QSigma_cong";
paulson@13285
   348
val QSigma_empty1 = thm "QSigma_empty1";
paulson@13285
   349
val QSigma_empty2 = thm "QSigma_empty2";
paulson@13285
   350
val qfst_conv = thm "qfst_conv";
paulson@13285
   351
val qsnd_conv = thm "qsnd_conv";
paulson@13285
   352
val qfst_type = thm "qfst_type";
paulson@13285
   353
val qsnd_type = thm "qsnd_type";
paulson@13285
   354
val QPair_qfst_qsnd_eq = thm "QPair_qfst_qsnd_eq";
paulson@13285
   355
val qsplit = thm "qsplit";
paulson@13285
   356
val qsplit_type = thm "qsplit_type";
paulson@13285
   357
val expand_qsplit = thm "expand_qsplit";
paulson@13285
   358
val qsplitI = thm "qsplitI";
paulson@13285
   359
val qsplitE = thm "qsplitE";
paulson@13285
   360
val qsplitD = thm "qsplitD";
paulson@13285
   361
val qconverseI = thm "qconverseI";
paulson@13285
   362
val qconverseD = thm "qconverseD";
paulson@13285
   363
val qconverseE = thm "qconverseE";
paulson@13285
   364
val qconverse_qconverse = thm "qconverse_qconverse";
paulson@13285
   365
val qconverse_type = thm "qconverse_type";
paulson@13285
   366
val qconverse_prod = thm "qconverse_prod";
paulson@13285
   367
val qconverse_empty = thm "qconverse_empty";
paulson@13285
   368
val QInlI = thm "QInlI";
paulson@13285
   369
val QInrI = thm "QInrI";
paulson@13285
   370
val qsumE = thm "qsumE";
paulson@13285
   371
val QInl_iff = thm "QInl_iff";
paulson@13285
   372
val QInr_iff = thm "QInr_iff";
paulson@13285
   373
val QInl_QInr_iff = thm "QInl_QInr_iff";
paulson@13285
   374
val QInr_QInl_iff = thm "QInr_QInl_iff";
paulson@13285
   375
val qsum_empty = thm "qsum_empty";
paulson@13285
   376
val QInl_inject = thm "QInl_inject";
paulson@13285
   377
val QInr_inject = thm "QInr_inject";
paulson@13285
   378
val QInl_neq_QInr = thm "QInl_neq_QInr";
paulson@13285
   379
val QInr_neq_QInl = thm "QInr_neq_QInl";
paulson@13285
   380
val QInlD = thm "QInlD";
paulson@13285
   381
val QInrD = thm "QInrD";
paulson@13285
   382
val qsum_iff = thm "qsum_iff";
paulson@13285
   383
val qsum_subset_iff = thm "qsum_subset_iff";
paulson@13285
   384
val qsum_equal_iff = thm "qsum_equal_iff";
paulson@13285
   385
val qcase_QInl = thm "qcase_QInl";
paulson@13285
   386
val qcase_QInr = thm "qcase_QInr";
paulson@13285
   387
val qcase_type = thm "qcase_type";
paulson@13285
   388
val Part_QInl = thm "Part_QInl";
paulson@13285
   389
val Part_QInr = thm "Part_QInr";
paulson@13285
   390
val Part_QInr2 = thm "Part_QInr2";
paulson@13285
   391
val Part_qsum_equality = thm "Part_qsum_equality";
paulson@13285
   392
val QPair_mono = thm "QPair_mono";
paulson@13285
   393
val QSigma_mono = thm "QSigma_mono";
paulson@13285
   394
val QInl_mono = thm "QInl_mono";
paulson@13285
   395
val QInr_mono = thm "QInr_mono";
paulson@13285
   396
val qsum_mono = thm "qsum_mono";
paulson@13285
   397
*}
paulson@13285
   398
clasohm@0
   399
end
clasohm@0
   400