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