src/ZF/QPair.thy
author paulson
Thu Mar 15 16:35:02 2012 +0000 (2012-03-15)
changeset 46953 2b6e55924af3
parent 46821 ff6b0c1087f2
child 58871 c399ae4b836f
permissions -rw-r--r--
replacing ":" by "\<in>"
wenzelm@35762
     1
(*  Title:      ZF/QPair.thy
clasohm@1478
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     3
    Copyright   1993  University of Cambridge
clasohm@0
     4
paulson@13285
     5
Many proofs are borrowed from pair.thy and sum.thy
paulson@13285
     6
paulson@13285
     7
Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
paulson@46953
     8
is not a limit ordinal?
clasohm@0
     9
*)
clasohm@0
    10
paulson@13356
    11
header{*Quine-Inspired Ordered Pairs and Disjoint Sums*}
paulson@13356
    12
haftmann@16417
    13
theory QPair imports Sum func begin
paulson@13285
    14
paulson@13356
    15
text{*For non-well-founded data
paulson@13356
    16
structures in ZF.  Does not precisely follow Quine's construction.  Thanks
paulson@13356
    17
to Thomas Forster for suggesting this approach!
paulson@13356
    18
paulson@13356
    19
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
paulson@13356
    20
1966.
paulson@13356
    21
*}
paulson@13356
    22
wenzelm@24893
    23
definition
wenzelm@24893
    24
  QPair     :: "[i, i] => i"                      ("<(_;/ _)>")  where
paulson@13285
    25
    "<a;b> == a+b"
wenzelm@3923
    26
wenzelm@24893
    27
definition
wenzelm@24893
    28
  qfst :: "i => i"  where
paulson@46820
    29
    "qfst(p) == THE a. \<exists>b. p=<a;b>"
paulson@13285
    30
wenzelm@24893
    31
definition
wenzelm@24893
    32
  qsnd :: "i => i"  where
paulson@46820
    33
    "qsnd(p) == THE b. \<exists>a. p=<a;b>"
paulson@13285
    34
wenzelm@24893
    35
definition
wenzelm@24893
    36
  qsplit    :: "[[i, i] => 'a, i] => 'a::{}"  (*for pattern-matching*)  where
paulson@13285
    37
    "qsplit(c,p) == c(qfst(p), qsnd(p))"
clasohm@0
    38
wenzelm@24893
    39
definition
wenzelm@24893
    40
  qconverse :: "i => i"  where
paulson@46953
    41
    "qconverse(r) == {z. w \<in> r, \<exists>x y. w=<x;y> & z=<y;x>}"
paulson@13285
    42
wenzelm@24893
    43
definition
wenzelm@24893
    44
  QSigma    :: "[i, i => i] => i"  where
paulson@13615
    45
    "QSigma(A,B)  ==  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
clasohm@0
    46
lcp@929
    47
syntax
paulson@46953
    48
  "_QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _ \<in> _./ _)" 10)
clasohm@0
    49
translations
paulson@46953
    50
  "QSUM x \<in> A. B"  => "CONST QSigma(A, %x. B)"
wenzelm@22808
    51
wenzelm@22808
    52
abbreviation
wenzelm@22808
    53
  qprod  (infixr "<*>" 80) where
wenzelm@22808
    54
  "A <*> B == QSigma(A, %_. B)"
clasohm@0
    55
wenzelm@24893
    56
definition
wenzelm@24893
    57
  qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)  where
paulson@46820
    58
    "A <+> B      == ({0} <*> A) \<union> ({1} <*> B)"
wenzelm@3923
    59
wenzelm@24893
    60
definition
wenzelm@24893
    61
  QInl :: "i=>i"  where
paulson@13285
    62
    "QInl(a)      == <0;a>"
paulson@13285
    63
wenzelm@24893
    64
definition
wenzelm@24893
    65
  QInr :: "i=>i"  where
paulson@13285
    66
    "QInr(b)      == <1;b>"
paulson@13285
    67
wenzelm@24893
    68
definition
wenzelm@24893
    69
  qcase     :: "[i=>i, i=>i, i]=>i"  where
paulson@13285
    70
    "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
paulson@13285
    71
paulson@13285
    72
paulson@13356
    73
subsection{*Quine ordered pairing*}
paulson@13285
    74
paulson@13285
    75
(** Lemmas for showing that <a;b> uniquely determines a and b **)
paulson@13285
    76
paulson@13285
    77
lemma QPair_empty [simp]: "<0;0> = 0"
paulson@13285
    78
by (simp add: QPair_def)
paulson@13285
    79
paulson@46821
    80
lemma QPair_iff [simp]: "<a;b> = <c;d> \<longleftrightarrow> a=c & b=d"
paulson@13285
    81
apply (simp add: QPair_def)
paulson@13285
    82
apply (rule sum_equal_iff)
paulson@13285
    83
done
paulson@13285
    84
wenzelm@45602
    85
lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, elim!]
paulson@13285
    86
paulson@13285
    87
lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
paulson@13285
    88
by blast
paulson@13285
    89
paulson@13285
    90
lemma QPair_inject2: "<a;b> = <c;d> ==> b=d"
paulson@13285
    91
by blast
paulson@13285
    92
paulson@13285
    93
paulson@13356
    94
subsubsection{*QSigma: Disjoint union of a family of sets
paulson@13356
    95
     Generalizes Cartesian product*}
paulson@13285
    96
paulson@46953
    97
lemma QSigmaI [intro!]: "[| a \<in> A;  b \<in> B(a) |] ==> <a;b> \<in> QSigma(A,B)"
paulson@13285
    98
by (simp add: QSigma_def)
paulson@13285
    99
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@46953
   104
    "[| c \<in> QSigma(A,B);
paulson@46953
   105
        !!x y.[| x \<in> A;  y \<in> B(x);  c=<x;y> |] ==> P
paulson@13285
   106
     |] ==> P"
paulson@46953
   107
by (simp add: QSigma_def, blast)
paulson@13285
   108
paulson@13285
   109
lemma QSigmaE2 [elim!]:
paulson@46953
   110
    "[| <a;b>: QSigma(A,B); [| a \<in> A;  b \<in> B(a) |] ==> P |] ==> P"
paulson@46953
   111
by (simp add: QSigma_def)
paulson@13285
   112
paulson@46820
   113
lemma QSigmaD1: "<a;b> \<in> QSigma(A,B) ==> a \<in> A"
paulson@13285
   114
by blast
paulson@13285
   115
paulson@46820
   116
lemma QSigmaD2: "<a;b> \<in> QSigma(A,B) ==> b \<in> B(a)"
paulson@13285
   117
by blast
paulson@13285
   118
paulson@13285
   119
lemma QSigma_cong:
paulson@46953
   120
    "[| A=A';  !!x. x \<in> A' ==> B(x)=B'(x) |] ==>
paulson@13285
   121
     QSigma(A,B) = QSigma(A',B')"
paulson@46953
   122
by (simp add: QSigma_def)
paulson@13285
   123
paulson@13285
   124
lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0"
paulson@13285
   125
by blast
paulson@13285
   126
paulson@13285
   127
lemma QSigma_empty2 [simp]: "A <*> 0 = 0"
paulson@13285
   128
by blast
paulson@13285
   129
paulson@13285
   130
paulson@13356
   131
subsubsection{*Projections: qfst, qsnd*}
paulson@13285
   132
paulson@13285
   133
lemma qfst_conv [simp]: "qfst(<a;b>) = a"
paulson@13544
   134
by (simp add: qfst_def)
paulson@13285
   135
paulson@13285
   136
lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
paulson@13544
   137
by (simp add: qsnd_def)
paulson@13285
   138
paulson@46953
   139
lemma qfst_type [TC]: "p \<in> QSigma(A,B) ==> qfst(p) \<in> A"
paulson@13285
   140
by auto
paulson@13285
   141
paulson@46953
   142
lemma qsnd_type [TC]: "p \<in> QSigma(A,B) ==> qsnd(p) \<in> B(qfst(p))"
paulson@13285
   143
by auto
paulson@13285
   144
paulson@46953
   145
lemma QPair_qfst_qsnd_eq: "a \<in> QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
paulson@13285
   146
by auto
paulson@13285
   147
paulson@13285
   148
paulson@13356
   149
subsubsection{*Eliminator: qsplit*}
paulson@13285
   150
paulson@13285
   151
(*A META-equality, so that it applies to higher types as well...*)
paulson@13285
   152
lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
paulson@13285
   153
by (simp add: qsplit_def)
paulson@13285
   154
paulson@13285
   155
paulson@13285
   156
lemma qsplit_type [elim!]:
paulson@46953
   157
    "[|  p \<in> QSigma(A,B);
paulson@46953
   158
         !!x y.[| x \<in> A; y \<in> B(x) |] ==> c(x,y):C(<x;y>)
paulson@46820
   159
     |] ==> qsplit(%x y. c(x,y), p) \<in> C(p)"
paulson@46953
   160
by auto
paulson@13285
   161
paulson@46953
   162
lemma expand_qsplit:
paulson@46953
   163
 "u \<in> A<*>B ==> R(qsplit(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x;y> \<longrightarrow> R(c(x,y)))"
paulson@13285
   164
apply (simp add: qsplit_def, auto)
paulson@13285
   165
done
paulson@13285
   166
paulson@13285
   167
paulson@13356
   168
subsubsection{*qsplit for predicates: result type o*}
paulson@13285
   169
paulson@13285
   170
lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
paulson@13285
   171
by (simp add: qsplit_def)
paulson@13285
   172
paulson@13285
   173
paulson@13285
   174
lemma qsplitE:
paulson@46953
   175
    "[| qsplit(R,z);  z \<in> QSigma(A,B);
paulson@46953
   176
        !!x y. [| z = <x;y>;  R(x,y) |] ==> P
paulson@13285
   177
    |] ==> P"
paulson@46953
   178
by (simp add: qsplit_def, auto)
paulson@13285
   179
paulson@13285
   180
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
paulson@13285
   181
by (simp add: qsplit_def)
paulson@13285
   182
paulson@13285
   183
paulson@13356
   184
subsubsection{*qconverse*}
paulson@13285
   185
paulson@13285
   186
lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
paulson@13285
   187
by (simp add: qconverse_def, blast)
paulson@13285
   188
paulson@46820
   189
lemma qconverseD [elim!]: "<a;b> \<in> qconverse(r) ==> <b;a> \<in> r"
paulson@13285
   190
by (simp add: qconverse_def, blast)
paulson@13285
   191
paulson@13285
   192
lemma qconverseE [elim!]:
paulson@46953
   193
    "[| yx \<in> qconverse(r);
paulson@46953
   194
        !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P
paulson@13285
   195
     |] ==> P"
paulson@46953
   196
by (simp add: qconverse_def, blast)
paulson@13285
   197
paulson@13285
   198
lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
paulson@13285
   199
by blast
paulson@13285
   200
paulson@46820
   201
lemma qconverse_type: "r \<subseteq> A <*> B ==> qconverse(r) \<subseteq> B <*> A"
paulson@13285
   202
by blast
paulson@13285
   203
paulson@13285
   204
lemma qconverse_prod: "qconverse(A <*> B) = B <*> A"
paulson@13285
   205
by blast
paulson@13285
   206
paulson@13285
   207
lemma qconverse_empty: "qconverse(0) = 0"
paulson@13285
   208
by blast
paulson@13285
   209
paulson@13285
   210
paulson@13356
   211
subsection{*The Quine-inspired notion of disjoint sum*}
paulson@13285
   212
paulson@13285
   213
lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
paulson@13285
   214
paulson@13285
   215
(** Introduction rules for the injections **)
paulson@13285
   216
paulson@46820
   217
lemma QInlI [intro!]: "a \<in> A ==> QInl(a) \<in> A <+> B"
paulson@13285
   218
by (simp add: qsum_defs, blast)
lcp@1097
   219
paulson@46820
   220
lemma QInrI [intro!]: "b \<in> B ==> QInr(b) \<in> A <+> B"
paulson@13285
   221
by (simp add: qsum_defs, blast)
paulson@13285
   222
paulson@13285
   223
(** Elimination rules **)
paulson@13285
   224
paulson@13285
   225
lemma qsumE [elim!]:
paulson@46953
   226
    "[| u \<in> A <+> B;
paulson@46953
   227
        !!x. [| x \<in> A;  u=QInl(x) |] ==> P;
paulson@46953
   228
        !!y. [| y \<in> B;  u=QInr(y) |] ==> P
paulson@13285
   229
     |] ==> P"
paulson@46953
   230
by (simp add: qsum_defs, blast)
paulson@13285
   231
paulson@13285
   232
paulson@13285
   233
(** Injection and freeness equivalences, for rewriting **)
paulson@13285
   234
paulson@46821
   235
lemma QInl_iff [iff]: "QInl(a)=QInl(b) \<longleftrightarrow> a=b"
paulson@13285
   236
by (simp add: qsum_defs )
paulson@13285
   237
paulson@46821
   238
lemma QInr_iff [iff]: "QInr(a)=QInr(b) \<longleftrightarrow> a=b"
paulson@13285
   239
by (simp add: qsum_defs )
paulson@13285
   240
paulson@46821
   241
lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) \<longleftrightarrow> False"
paulson@13285
   242
by (simp add: qsum_defs )
paulson@13285
   243
paulson@46821
   244
lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) \<longleftrightarrow> False"
paulson@13285
   245
by (simp add: qsum_defs )
paulson@13285
   246
paulson@13285
   247
lemma qsum_empty [simp]: "0<+>0 = 0"
paulson@13285
   248
by (simp add: qsum_defs )
paulson@13285
   249
paulson@13285
   250
(*Injection and freeness rules*)
paulson@13285
   251
wenzelm@45602
   252
lemmas QInl_inject = QInl_iff [THEN iffD1]
wenzelm@45602
   253
lemmas QInr_inject = QInr_iff [THEN iffD1]
paulson@13823
   254
lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!]
paulson@13823
   255
lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
paulson@13285
   256
paulson@46953
   257
lemma QInlD: "QInl(a): A<+>B ==> a \<in> A"
paulson@13285
   258
by blast
paulson@13285
   259
paulson@46953
   260
lemma QInrD: "QInr(b): A<+>B ==> b \<in> B"
paulson@13285
   261
by blast
paulson@13285
   262
paulson@13285
   263
(** <+> is itself injective... who cares?? **)
paulson@13285
   264
paulson@13285
   265
lemma qsum_iff:
paulson@46953
   266
     "u \<in> A <+> B \<longleftrightarrow> (\<exists>x. x \<in> A & u=QInl(x)) | (\<exists>y. y \<in> B & u=QInr(y))"
paulson@13356
   267
by blast
paulson@13285
   268
paulson@46821
   269
lemma qsum_subset_iff: "A <+> B \<subseteq> C <+> D \<longleftrightarrow> A<=C & B<=D"
paulson@13285
   270
by blast
paulson@13285
   271
paulson@46821
   272
lemma qsum_equal_iff: "A <+> B = C <+> D \<longleftrightarrow> A=C & B=D"
paulson@13285
   273
apply (simp (no_asm) add: extension qsum_subset_iff)
paulson@13285
   274
apply blast
paulson@13285
   275
done
paulson@13285
   276
paulson@13356
   277
subsubsection{*Eliminator -- qcase*}
paulson@13285
   278
paulson@13285
   279
lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
paulson@13285
   280
by (simp add: qsum_defs )
paulson@13285
   281
paulson@13285
   282
paulson@13285
   283
lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)"
paulson@13285
   284
by (simp add: qsum_defs )
paulson@13285
   285
paulson@13285
   286
lemma qcase_type:
paulson@46953
   287
    "[| u \<in> A <+> B;
paulson@46953
   288
        !!x. x \<in> A ==> c(x): C(QInl(x));
paulson@46953
   289
        !!y. y \<in> B ==> d(y): C(QInr(y))
paulson@46820
   290
     |] ==> qcase(c,d,u) \<in> C(u)"
paulson@46953
   291
by (simp add: qsum_defs, auto)
paulson@13285
   292
paulson@13285
   293
(** Rules for the Part primitive **)
paulson@13285
   294
paulson@46953
   295
lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x \<in> A}"
paulson@13285
   296
by blast
paulson@13285
   297
paulson@46953
   298
lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y \<in> B}"
paulson@13285
   299
by blast
paulson@13285
   300
paulson@46953
   301
lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y \<in> Part(B,h)}"
paulson@13285
   302
by blast
clasohm@0
   303
paulson@46820
   304
lemma Part_qsum_equality: "C \<subseteq> A <+> B ==> Part(C,QInl) \<union> Part(C,QInr) = C"
paulson@13285
   305
by blast
paulson@13285
   306
paulson@13285
   307
paulson@13356
   308
subsubsection{*Monotonicity*}
paulson@13285
   309
paulson@46820
   310
lemma QPair_mono: "[| a<=c;  b<=d |] ==> <a;b> \<subseteq> <c;d>"
paulson@13285
   311
by (simp add: QPair_def sum_mono)
paulson@13285
   312
paulson@13285
   313
lemma QSigma_mono [rule_format]:
paulson@46820
   314
     "[| A<=C;  \<forall>x\<in>A. B(x) \<subseteq> D(x) |] ==> QSigma(A,B) \<subseteq> QSigma(C,D)"
paulson@13285
   315
by blast
paulson@13285
   316
paulson@46820
   317
lemma QInl_mono: "a<=b ==> QInl(a) \<subseteq> QInl(b)"
paulson@13285
   318
by (simp add: QInl_def subset_refl [THEN QPair_mono])
paulson@13285
   319
paulson@46820
   320
lemma QInr_mono: "a<=b ==> QInr(a) \<subseteq> QInr(b)"
paulson@13285
   321
by (simp add: QInr_def subset_refl [THEN QPair_mono])
paulson@13285
   322
paulson@46820
   323
lemma qsum_mono: "[| A<=C;  B<=D |] ==> A <+> B \<subseteq> C <+> D"
paulson@13285
   324
by blast
paulson@13285
   325
clasohm@0
   326
end