src/ZF/QPair.thy
author wenzelm
Thu, 26 Apr 2007 14:24:08 +0200
changeset 22808 a7daa74e2980
parent 17782 b3846df9d643
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
eliminated unnamed infixes, tuned syntax;
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
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    24
constdefs
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    25
  QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
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
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    28
  qfst :: "i => i"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    29
    "qfst(p) == THE a. EX b. p=<a;b>"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    30
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    31
  qsnd :: "i => i"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    32
    "qsnd(p) == THE b. EX a. p=<a;b>"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    33
14854
61bdf2ae4dc5 removed obsolete sort 'logic';
wenzelm
parents: 13823
diff changeset
    34
  qsplit    :: "[[i, i] => 'a, i] => 'a::{}"  (*for pattern-matching*)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    35
    "qsplit(c,p) == c(qfst(p), qsnd(p))"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    37
  qconverse :: "i => i"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    38
    "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
    39
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    40
  QSigma    :: "[i, i => i] => i"
13615
449a70d88b38 Numerous cosmetic changes, prompted by the new simplifier
paulson
parents: 13544
diff changeset
    41
    "QSigma(A,B)  ==  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
929
137035296ad6 Moved declarations of @QSUM and <*> to a syntax section.
lcp
parents: 753
diff changeset
    43
syntax
22808
a7daa74e2980 eliminated unnamed infixes, tuned syntax;
wenzelm
parents: 17782
diff changeset
    44
  "_QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
translations
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
  "QSUM x:A. B"  => "QSigma(A, %x. B)"
22808
a7daa74e2980 eliminated unnamed infixes, tuned syntax;
wenzelm
parents: 17782
diff changeset
    47
a7daa74e2980 eliminated unnamed infixes, tuned syntax;
wenzelm
parents: 17782
diff changeset
    48
abbreviation
a7daa74e2980 eliminated unnamed infixes, tuned syntax;
wenzelm
parents: 17782
diff changeset
    49
  qprod  (infixr "<*>" 80) where
a7daa74e2980 eliminated unnamed infixes, tuned syntax;
wenzelm
parents: 17782
diff changeset
    50
  "A <*> B == QSigma(A, %_. B)"
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    52
constdefs
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    53
  qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    54
    "A <+> B      == ({0} <*> A) Un ({1} <*> B)"
3923
c257b82a1200 global;
wenzelm
parents: 2469
diff changeset
    55
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    56
  QInl :: "i=>i"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    57
    "QInl(a)      == <0;a>"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    58
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    59
  QInr :: "i=>i"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    60
    "QInr(b)      == <1;b>"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    61
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    62
  qcase     :: "[i=>i, i=>i, i]=>i"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    63
    "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    64
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    65
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
    66
subsection{*Quine ordered pairing*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    67
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    68
(** Lemmas for showing that <a;b> uniquely determines a and b **)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    69
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    70
lemma QPair_empty [simp]: "<0;0> = 0"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    71
by (simp add: QPair_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    72
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    73
lemma QPair_iff [simp]: "<a;b> = <c;d> <-> a=c & b=d"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    74
apply (simp add: QPair_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    75
apply (rule sum_equal_iff)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    76
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    77
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    78
lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    79
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    80
lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    81
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    82
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    83
lemma QPair_inject2: "<a;b> = <c;d> ==> b=d"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    84
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    85
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    86
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
    87
subsubsection{*QSigma: Disjoint union of a family of sets
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
    88
     Generalizes Cartesian product*}
13285
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 QSigmaI [intro!]: "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    91
by (simp add: QSigma_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    92
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    93
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    94
(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    95
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    96
lemma QSigmaE [elim!]:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    97
    "[| c: QSigma(A,B);   
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    98
        !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
    99
     |] ==> P"
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   100
by (simp add: QSigma_def, blast) 
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   101
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   102
lemma QSigmaE2 [elim!]:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   103
    "[| <a;b>: QSigma(A,B); [| a:A;  b:B(a) |] ==> P |] ==> P"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   104
by (simp add: QSigma_def) 
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   105
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   106
lemma QSigmaD1: "<a;b> : QSigma(A,B) ==> a : A"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   107
by blast
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 QSigmaD2: "<a;b> : QSigma(A,B) ==> b : B(a)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   110
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   111
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   112
lemma QSigma_cong:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   113
    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   114
     QSigma(A,B) = QSigma(A',B')"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   115
by (simp add: QSigma_def) 
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 QSigma_empty1 [simp]: "QSigma(0,B) = 0"
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_empty2 [simp]: "A <*> 0 = 0"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   121
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   122
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   123
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   124
subsubsection{*Projections: qfst, qsnd*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   125
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   126
lemma qfst_conv [simp]: "qfst(<a;b>) = a"
13544
895994073bdf various new lemmas for Constructible
paulson
parents: 13534
diff changeset
   127
by (simp add: qfst_def)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   128
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   129
lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
13544
895994073bdf various new lemmas for Constructible
paulson
parents: 13534
diff changeset
   130
by (simp add: qsnd_def)
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   131
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   132
lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   133
by auto
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   134
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   135
lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   136
by auto
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   137
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   138
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
   139
by auto
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   140
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   141
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   142
subsubsection{*Eliminator: qsplit*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   143
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   144
(*A META-equality, so that it applies to higher types as well...*)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   145
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
   146
by (simp add: qsplit_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   147
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   148
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   149
lemma qsplit_type [elim!]:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   150
    "[|  p:QSigma(A,B);    
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   151
         !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>)  
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   152
     |] ==> qsplit(%x y. c(x,y), p) : C(p)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   153
by auto 
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   154
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   155
lemma expand_qsplit: 
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   156
 "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
   157
apply (simp add: qsplit_def, auto)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   158
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   159
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   160
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   161
subsubsection{*qsplit for predicates: result type o*}
13285
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 qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   164
by (simp add: qsplit_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   165
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   166
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   167
lemma qsplitE:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   168
    "[| qsplit(R,z);  z:QSigma(A,B);                     
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   169
        !!x y. [| z = <x;y>;  R(x,y) |] ==> P            
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   170
    |] ==> P"
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   171
by (simp add: qsplit_def, auto) 
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   172
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   173
lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   174
by (simp add: qsplit_def)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   175
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   176
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   177
subsubsection{*qconverse*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   178
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   179
lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   180
by (simp add: qconverse_def, blast)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   181
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   182
lemma qconverseD [elim!]: "<a;b> : qconverse(r) ==> <b;a> : r"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   183
by (simp add: qconverse_def, blast)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   184
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   185
lemma qconverseE [elim!]:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   186
    "[| yx : qconverse(r);   
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   187
        !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P  
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   188
     |] ==> P"
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   189
by (simp add: qconverse_def, blast) 
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   190
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   191
lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   192
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   193
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   194
lemma qconverse_type: "r <= A <*> B ==> qconverse(r) <= B <*> A"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   195
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   196
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   197
lemma qconverse_prod: "qconverse(A <*> B) = B <*> A"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   198
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   199
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   200
lemma qconverse_empty: "qconverse(0) = 0"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   201
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   202
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   203
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   204
subsection{*The Quine-inspired notion of disjoint sum*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   205
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   206
lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   207
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   208
(** Introduction rules for the injections **)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   209
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   210
lemma QInlI [intro!]: "a : A ==> QInl(a) : A <+> B"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   211
by (simp add: qsum_defs, blast)
1097
01379c46ad2d Changed definitions so that qsplit is now defined in terms of
lcp
parents: 929
diff changeset
   212
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   213
lemma QInrI [intro!]: "b : B ==> QInr(b) : A <+> B"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   214
by (simp add: qsum_defs, blast)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   215
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   216
(** Elimination rules **)
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 qsumE [elim!]:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   219
    "[| u: A <+> B;   
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   220
        !!x. [| x:A;  u=QInl(x) |] ==> P;  
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   221
        !!y. [| y:B;  u=QInr(y) |] ==> P  
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   222
     |] ==> P"
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   223
by (simp add: qsum_defs, blast) 
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   224
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   225
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   226
(** Injection and freeness equivalences, for rewriting **)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   227
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   228
lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   229
by (simp add: qsum_defs )
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   230
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   231
lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   232
by (simp add: qsum_defs )
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   233
13823
d49ffd9f9662 fixed anomalies in the installed classical rules
paulson
parents: 13784
diff changeset
   234
lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   235
by (simp add: qsum_defs )
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   236
13823
d49ffd9f9662 fixed anomalies in the installed classical rules
paulson
parents: 13784
diff changeset
   237
lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False"
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   238
by (simp add: qsum_defs )
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   239
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   240
lemma qsum_empty [simp]: "0<+>0 = 0"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   241
by (simp add: qsum_defs )
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   242
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   243
(*Injection and freeness rules*)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   244
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   245
lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   246
lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
13823
d49ffd9f9662 fixed anomalies in the installed classical rules
paulson
parents: 13784
diff changeset
   247
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
   248
lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   249
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   250
lemma QInlD: "QInl(a): A<+>B ==> a: A"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   251
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   252
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   253
lemma QInrD: "QInr(b): A<+>B ==> b: B"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   254
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   255
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   256
(** <+> is itself injective... who cares?? **)
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 qsum_iff:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   259
     "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
   260
by blast
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   261
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   262
lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   263
by blast
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_equal_iff: "A <+> B = C <+> D <-> A=C & B=D"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   266
apply (simp (no_asm) add: extension qsum_subset_iff)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   267
apply blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   268
done
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   269
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   270
subsubsection{*Eliminator -- qcase*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   271
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   272
lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   273
by (simp add: qsum_defs )
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   274
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   275
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   276
lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   277
by (simp add: qsum_defs )
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_type:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   280
    "[| u: A <+> B;  
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   281
        !!x. x: A ==> c(x): C(QInl(x));    
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   282
        !!y. y: B ==> d(y): C(QInr(y))  
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   283
     |] ==> qcase(c,d,u) : C(u)"
13784
b9f6154427a4 tidying (by script)
paulson
parents: 13615
diff changeset
   284
by (simp add: qsum_defs, auto) 
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   286
(** Rules for the Part primitive **)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   287
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   288
lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x: A}"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   289
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   290
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   291
lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y: B}"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   292
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   293
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   294
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
   295
by blast
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   297
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
   298
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   299
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   300
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13285
diff changeset
   301
subsubsection{*Monotonicity*}
13285
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   302
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   303
lemma QPair_mono: "[| a<=c;  b<=d |] ==> <a;b> <= <c;d>"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   304
by (simp add: QPair_def sum_mono)
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   305
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   306
lemma QSigma_mono [rule_format]:
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   307
     "[| 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
   308
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   309
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   310
lemma QInl_mono: "a<=b ==> QInl(a) <= QInl(b)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   311
by (simp add: QInl_def subset_refl [THEN QPair_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 QInr_mono: "a<=b ==> QInr(a) <= QInr(b)"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   314
by (simp add: QInr_def subset_refl [THEN QPair_mono])
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   315
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   316
lemma qsum_mono: "[| A<=C;  B<=D |] ==> A <+> B <= C <+> D"
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   317
by blast
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   318
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   319
ML
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   320
{*
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   321
val qsum_defs = thms "qsum_defs";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   322
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   323
val QPair_empty = thm "QPair_empty";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   324
val QPair_iff = thm "QPair_iff";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   325
val QPair_inject = thm "QPair_inject";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   326
val QPair_inject1 = thm "QPair_inject1";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   327
val QPair_inject2 = thm "QPair_inject2";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   328
val QSigmaI = thm "QSigmaI";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   329
val QSigmaE = thm "QSigmaE";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   330
val QSigmaE = thm "QSigmaE";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   331
val QSigmaE2 = thm "QSigmaE2";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   332
val QSigmaD1 = thm "QSigmaD1";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   333
val QSigmaD2 = thm "QSigmaD2";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   334
val QSigma_cong = thm "QSigma_cong";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   335
val QSigma_empty1 = thm "QSigma_empty1";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   336
val QSigma_empty2 = thm "QSigma_empty2";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   337
val qfst_conv = thm "qfst_conv";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   338
val qsnd_conv = thm "qsnd_conv";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   339
val qfst_type = thm "qfst_type";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   340
val qsnd_type = thm "qsnd_type";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   341
val QPair_qfst_qsnd_eq = thm "QPair_qfst_qsnd_eq";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   342
val qsplit = thm "qsplit";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   343
val qsplit_type = thm "qsplit_type";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   344
val expand_qsplit = thm "expand_qsplit";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   345
val qsplitI = thm "qsplitI";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   346
val qsplitE = thm "qsplitE";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   347
val qsplitD = thm "qsplitD";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   348
val qconverseI = thm "qconverseI";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   349
val qconverseD = thm "qconverseD";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   350
val qconverseE = thm "qconverseE";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   351
val qconverse_qconverse = thm "qconverse_qconverse";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   352
val qconverse_type = thm "qconverse_type";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   353
val qconverse_prod = thm "qconverse_prod";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   354
val qconverse_empty = thm "qconverse_empty";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   355
val QInlI = thm "QInlI";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   356
val QInrI = thm "QInrI";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   357
val qsumE = thm "qsumE";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   358
val QInl_iff = thm "QInl_iff";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   359
val QInr_iff = thm "QInr_iff";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   360
val QInl_QInr_iff = thm "QInl_QInr_iff";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   361
val QInr_QInl_iff = thm "QInr_QInl_iff";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   362
val qsum_empty = thm "qsum_empty";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   363
val QInl_inject = thm "QInl_inject";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   364
val QInr_inject = thm "QInr_inject";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   365
val QInl_neq_QInr = thm "QInl_neq_QInr";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   366
val QInr_neq_QInl = thm "QInr_neq_QInl";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   367
val QInlD = thm "QInlD";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   368
val QInrD = thm "QInrD";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   369
val qsum_iff = thm "qsum_iff";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   370
val qsum_subset_iff = thm "qsum_subset_iff";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   371
val qsum_equal_iff = thm "qsum_equal_iff";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   372
val qcase_QInl = thm "qcase_QInl";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   373
val qcase_QInr = thm "qcase_QInr";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   374
val qcase_type = thm "qcase_type";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   375
val Part_QInl = thm "Part_QInl";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   376
val Part_QInr = thm "Part_QInr";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   377
val Part_QInr2 = thm "Part_QInr2";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   378
val Part_qsum_equality = thm "Part_qsum_equality";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   379
val QPair_mono = thm "QPair_mono";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   380
val QSigma_mono = thm "QSigma_mono";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   381
val QInl_mono = thm "QInl_mono";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   382
val QInr_mono = thm "QInr_mono";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   383
val qsum_mono = thm "qsum_mono";
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   384
*}
28d1823ce0f2 conversion of QPair to Isar
paulson
parents: 13259
diff changeset
   385
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   386
end