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