conversion of QPair to Isar
authorpaulson
Tue Jul 02 22:46:23 2002 +0200 (2002-07-02)
changeset 1328528d1823ce0f2
parent 13284 20c818c966e6
child 13286 a7f0f8869b54
conversion of QPair to Isar
src/ZF/IsaMakefile
src/ZF/QPair.ML
src/ZF/QPair.thy
src/ZF/QUniv.thy
     1.1 --- a/src/ZF/IsaMakefile	Tue Jul 02 17:44:13 2002 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Tue Jul 02 22:46:23 2002 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
     1.5    Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy	\
     1.6    OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy	\
     1.7 -  QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML	\
     1.8 +  QPair.thy QUniv.thy ROOT.ML	\
     1.9    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
    1.10    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
    1.11    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
     2.1 --- a/src/ZF/QPair.ML	Tue Jul 02 17:44:13 2002 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,357 +0,0 @@
     2.4 -(*  Title:      ZF/QPair.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1993  University of Cambridge
     2.8 -
     2.9 -Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
    2.10 -structures in ZF.  Does not precisely follow Quine's construction.  Thanks
    2.11 -to Thomas Forster for suggesting this approach!
    2.12 -
    2.13 -W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
    2.14 -1966.
    2.15 -
    2.16 -Many proofs are borrowed from pair.ML and sum.ML
    2.17 -
    2.18 -Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
    2.19 -    is not a limit ordinal? 
    2.20 -*)
    2.21 -
    2.22 -(**** Quine ordered pairing ****)
    2.23 -
    2.24 -(** Lemmas for showing that <a;b> uniquely determines a and b **)
    2.25 -
    2.26 -Goalw [QPair_def] "<0;0> = 0";
    2.27 -by (Simp_tac 1);
    2.28 -qed "QPair_empty";
    2.29 -
    2.30 -Goalw [QPair_def] "<a;b> = <c;d> <-> a=c & b=d";
    2.31 -by (rtac sum_equal_iff 1);
    2.32 -qed "QPair_iff";
    2.33 -
    2.34 -bind_thm ("QPair_inject", QPair_iff RS iffD1 RS conjE);
    2.35 -
    2.36 -Addsimps [QPair_empty, QPair_iff];
    2.37 -AddSEs   [QPair_inject];
    2.38 -
    2.39 -Goal "<a;b> = <c;d> ==> a=c";
    2.40 -by (Blast_tac 1) ;
    2.41 -qed "QPair_inject1";
    2.42 -
    2.43 -Goal "<a;b> = <c;d> ==> b=d";
    2.44 -by (Blast_tac 1) ;
    2.45 -qed "QPair_inject2";
    2.46 -
    2.47 -
    2.48 -(*** QSigma: Disjoint union of a family of sets
    2.49 -     Generalizes Cartesian product ***)
    2.50 -
    2.51 -Goalw [QSigma_def] "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)";
    2.52 -by (Blast_tac 1) ;
    2.53 -qed "QSigmaI";
    2.54 -
    2.55 -AddSIs [QSigmaI];
    2.56 -
    2.57 -(*The general elimination rule*)
    2.58 -val major::prems= Goalw [QSigma_def] 
    2.59 -    "[| c: QSigma(A,B);  \
    2.60 -\       !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P \
    2.61 -\    |] ==> P";
    2.62 -by (cut_facts_tac [major] 1);
    2.63 -by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
    2.64 -qed "QSigmaE";
    2.65 -
    2.66 -(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
    2.67 -
    2.68 -bind_thm ("QSigmaE2",
    2.69 -  rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
    2.70 -                  THEN prune_params_tac)
    2.71 -      (inst "c" "<a;b>" QSigmaE));
    2.72 -
    2.73 -AddSEs [QSigmaE2, QSigmaE];
    2.74 -
    2.75 -Goal "<a;b> : QSigma(A,B) ==> a : A";
    2.76 -by (Blast_tac 1) ;
    2.77 -qed "QSigmaD1";
    2.78 -
    2.79 -Goal "<a;b> : QSigma(A,B) ==> b : B(a)";
    2.80 -by (Blast_tac 1) ;
    2.81 -qed "QSigmaD2";
    2.82 -
    2.83 -
    2.84 -val prems= Goalw [QSigma_def] 
    2.85 -    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    2.86 -\    QSigma(A,B) = QSigma(A',B')";
    2.87 -by (simp_tac (simpset() addsimps prems) 1) ;
    2.88 -qed "QSigma_cong";
    2.89 -
    2.90 -Goal "QSigma(0,B) = 0";
    2.91 -by (Blast_tac 1) ;
    2.92 -qed "QSigma_empty1";
    2.93 -
    2.94 -Goal "A <*> 0 = 0";
    2.95 -by (Blast_tac 1) ;
    2.96 -qed "QSigma_empty2";
    2.97 -
    2.98 -Addsimps [QSigma_empty1, QSigma_empty2];
    2.99 -
   2.100 -
   2.101 -(*** Projections: qfst, qsnd ***)
   2.102 -
   2.103 -Goalw [qfst_def]  "qfst(<a;b>) = a";
   2.104 -by (Blast_tac 1) ;
   2.105 -qed "qfst_conv";
   2.106 -
   2.107 -Goalw [qsnd_def]  "qsnd(<a;b>) = b";
   2.108 -by (Blast_tac 1) ;
   2.109 -qed "qsnd_conv";
   2.110 -
   2.111 -Addsimps [qfst_conv, qsnd_conv];
   2.112 -
   2.113 -Goal "p:QSigma(A,B) ==> qfst(p) : A";
   2.114 -by (Auto_tac) ;
   2.115 -qed "qfst_type";
   2.116 -AddTCs [qfst_type];
   2.117 -
   2.118 -Goal "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))";
   2.119 -by (Auto_tac) ;
   2.120 -qed "qsnd_type";
   2.121 -AddTCs [qsnd_type];
   2.122 -
   2.123 -Goal "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a";
   2.124 -by Auto_tac;
   2.125 -qed "QPair_qfst_qsnd_eq";
   2.126 -
   2.127 -
   2.128 -(*** Eliminator - qsplit ***)
   2.129 -
   2.130 -(*A META-equality, so that it applies to higher types as well...*)
   2.131 -Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)";
   2.132 -by (Simp_tac 1);
   2.133 -qed "qsplit";
   2.134 -Addsimps [qsplit];
   2.135 -
   2.136 -val major::prems= Goal
   2.137 -    "[|  p:QSigma(A,B);   \
   2.138 -\        !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
   2.139 -\    |] ==> qsplit(%x y. c(x,y), p) : C(p)";
   2.140 -by (rtac (major RS QSigmaE) 1);
   2.141 -by (asm_simp_tac (simpset() addsimps prems) 1) ;
   2.142 -qed "qsplit_type";
   2.143 -
   2.144 -Goalw [qsplit_def]
   2.145 - "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))";
   2.146 -by Auto_tac;
   2.147 -qed "expand_qsplit";
   2.148 -
   2.149 -
   2.150 -(*** qsplit for predicates: result type o ***)
   2.151 -
   2.152 -Goalw [qsplit_def] "R(a,b) ==> qsplit(R, <a;b>)";
   2.153 -by (Asm_simp_tac 1);
   2.154 -qed "qsplitI";
   2.155 -
   2.156 -val major::sigma::prems = Goalw [qsplit_def]
   2.157 -    "[| qsplit(R,z);  z:QSigma(A,B);                    \
   2.158 -\       !!x y. [| z = <x;y>;  R(x,y) |] ==> P           \
   2.159 -\   |] ==> P";
   2.160 -by (rtac (sigma RS QSigmaE) 1);
   2.161 -by (cut_facts_tac [major] 1);
   2.162 -by (REPEAT (ares_tac prems 1));
   2.163 -by (Asm_full_simp_tac 1);
   2.164 -qed "qsplitE";
   2.165 -
   2.166 -Goalw [qsplit_def] "qsplit(R,<a;b>) ==> R(a,b)";
   2.167 -by (Asm_full_simp_tac 1);
   2.168 -qed "qsplitD";
   2.169 -
   2.170 -
   2.171 -(*** qconverse ***)
   2.172 -
   2.173 -Goalw [qconverse_def] "<a;b>:r ==> <b;a>:qconverse(r)";
   2.174 -by (Blast_tac 1) ;
   2.175 -qed "qconverseI";
   2.176 -
   2.177 -Goalw [qconverse_def] "<a;b> : qconverse(r) ==> <b;a> : r";
   2.178 -by (Blast_tac 1) ;
   2.179 -qed "qconverseD";
   2.180 -
   2.181 -val [major,minor]= Goalw [qconverse_def] 
   2.182 -    "[| yx : qconverse(r);  \
   2.183 -\       !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P \
   2.184 -\    |] ==> P";
   2.185 -by (rtac (major RS ReplaceE) 1);
   2.186 -by (REPEAT (eresolve_tac [exE, conjE, minor] 1));
   2.187 -by (hyp_subst_tac 1);
   2.188 -by (assume_tac 1) ;
   2.189 -qed "qconverseE";
   2.190 -
   2.191 -AddSIs [qconverseI];
   2.192 -AddSEs [qconverseD, qconverseE];
   2.193 -
   2.194 -Goal "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r";
   2.195 -by (Blast_tac 1) ;
   2.196 -qed "qconverse_qconverse";
   2.197 -
   2.198 -Goal "r <= A <*> B ==> qconverse(r) <= B <*> A";
   2.199 -by (Blast_tac 1) ;
   2.200 -qed "qconverse_type";
   2.201 -
   2.202 -Goal "qconverse(A <*> B) = B <*> A";
   2.203 -by (Blast_tac 1) ;
   2.204 -qed "qconverse_prod";
   2.205 -
   2.206 -Goal "qconverse(0) = 0";
   2.207 -by (Blast_tac 1) ;
   2.208 -qed "qconverse_empty";
   2.209 -
   2.210 -
   2.211 -(**** The Quine-inspired notion of disjoint sum ****)
   2.212 -
   2.213 -bind_thms ("qsum_defs", [qsum_def,QInl_def,QInr_def,qcase_def]);
   2.214 -
   2.215 -(** Introduction rules for the injections **)
   2.216 -
   2.217 -Goalw qsum_defs "a : A ==> QInl(a) : A <+> B";
   2.218 -by (Blast_tac 1);
   2.219 -qed "QInlI";
   2.220 -
   2.221 -Goalw qsum_defs "b : B ==> QInr(b) : A <+> B";
   2.222 -by (Blast_tac 1);
   2.223 -qed "QInrI";
   2.224 -
   2.225 -(** Elimination rules **)
   2.226 -
   2.227 -val major::prems = Goalw qsum_defs
   2.228 -    "[| u: A <+> B;  \
   2.229 -\       !!x. [| x:A;  u=QInl(x) |] ==> P; \
   2.230 -\       !!y. [| y:B;  u=QInr(y) |] ==> P \
   2.231 -\    |] ==> P";
   2.232 -by (rtac (major RS UnE) 1);
   2.233 -by (REPEAT (rtac refl 1
   2.234 -     ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
   2.235 -qed "qsumE";
   2.236 -
   2.237 -AddSIs [QInlI, QInrI];
   2.238 -
   2.239 -(** Injection and freeness equivalences, for rewriting **)
   2.240 -
   2.241 -Goalw qsum_defs "QInl(a)=QInl(b) <-> a=b";
   2.242 -by (Simp_tac 1);
   2.243 -qed "QInl_iff";
   2.244 -
   2.245 -Goalw qsum_defs "QInr(a)=QInr(b) <-> a=b";
   2.246 -by (Simp_tac 1);
   2.247 -qed "QInr_iff";
   2.248 -
   2.249 -Goalw qsum_defs "QInl(a)=QInr(b) <-> False";
   2.250 -by (Simp_tac 1);
   2.251 -qed "QInl_QInr_iff";
   2.252 -
   2.253 -Goalw qsum_defs "QInr(b)=QInl(a) <-> False";
   2.254 -by (Simp_tac 1);
   2.255 -qed "QInr_QInl_iff";
   2.256 -
   2.257 -Goalw qsum_defs "0<+>0 = 0";
   2.258 -by (Simp_tac 1);
   2.259 -qed "qsum_empty";
   2.260 -
   2.261 -(*Injection and freeness rules*)
   2.262 -
   2.263 -bind_thm ("QInl_inject", (QInl_iff RS iffD1));
   2.264 -bind_thm ("QInr_inject", (QInr_iff RS iffD1));
   2.265 -bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE));
   2.266 -bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE));
   2.267 -
   2.268 -AddSEs [qsumE, QInl_neq_QInr, QInr_neq_QInl];
   2.269 -AddSDs [QInl_inject, QInr_inject];
   2.270 -Addsimps [QInl_iff, QInr_iff, QInl_QInr_iff, QInr_QInl_iff, qsum_empty];
   2.271 -
   2.272 -Goal "QInl(a): A<+>B ==> a: A";
   2.273 -by (Blast_tac 1);
   2.274 -qed "QInlD";
   2.275 -
   2.276 -Goal "QInr(b): A<+>B ==> b: B";
   2.277 -by (Blast_tac 1);
   2.278 -qed "QInrD";
   2.279 -
   2.280 -(** <+> is itself injective... who cares?? **)
   2.281 -
   2.282 -Goal "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
   2.283 -by (Blast_tac 1);
   2.284 -qed "qsum_iff";
   2.285 -
   2.286 -Goal "A <+> B <= C <+> D <-> A<=C & B<=D";
   2.287 -by (Blast_tac 1);
   2.288 -qed "qsum_subset_iff";
   2.289 -
   2.290 -Goal "A <+> B = C <+> D <-> A=C & B=D";
   2.291 -by (simp_tac (simpset() addsimps [extension,qsum_subset_iff]) 1);
   2.292 -by (Blast_tac 1);
   2.293 -qed "qsum_equal_iff";
   2.294 -
   2.295 -(*** Eliminator -- qcase ***)
   2.296 -
   2.297 -Goalw qsum_defs "qcase(c, d, QInl(a)) = c(a)";
   2.298 -by (Simp_tac 1);
   2.299 -qed "qcase_QInl";
   2.300 -
   2.301 -Goalw qsum_defs "qcase(c, d, QInr(b)) = d(b)";
   2.302 -by (Simp_tac 1);
   2.303 -qed "qcase_QInr";
   2.304 -
   2.305 -Addsimps [qcase_QInl, qcase_QInr];
   2.306 -
   2.307 -val major::prems = Goal
   2.308 -    "[| u: A <+> B; \
   2.309 -\       !!x. x: A ==> c(x): C(QInl(x));   \
   2.310 -\       !!y. y: B ==> d(y): C(QInr(y)) \
   2.311 -\    |] ==> qcase(c,d,u) : C(u)";
   2.312 -by (rtac (major RS qsumE) 1);
   2.313 -by (ALLGOALS (etac ssubst));
   2.314 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   2.315 -qed "qcase_type";
   2.316 -
   2.317 -(** Rules for the Part primitive **)
   2.318 -
   2.319 -Goal "Part(A <+> B,QInl) = {QInl(x). x: A}";
   2.320 -by (Blast_tac 1);
   2.321 -qed "Part_QInl";
   2.322 -
   2.323 -Goal "Part(A <+> B,QInr) = {QInr(y). y: B}";
   2.324 -by (Blast_tac 1);
   2.325 -qed "Part_QInr";
   2.326 -
   2.327 -Goal "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}";
   2.328 -by (Blast_tac 1);
   2.329 -qed "Part_QInr2";
   2.330 -
   2.331 -Goal "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
   2.332 -by (Blast_tac 1);
   2.333 -qed "Part_qsum_equality";
   2.334 -
   2.335 -
   2.336 -(*** Monotonicity ***)
   2.337 -
   2.338 -Goalw [QPair_def] "[| a<=c;  b<=d |] ==> <a;b> <= <c;d>";
   2.339 -by (REPEAT (ares_tac [sum_mono] 1));
   2.340 -qed "QPair_mono";
   2.341 -
   2.342 -Goal "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==>  \
   2.343 -\                          QSigma(A,B) <= QSigma(C,D)";
   2.344 -by (Blast_tac 1);
   2.345 -qed "QSigma_mono_lemma";
   2.346 -bind_thm ("QSigma_mono", ballI RSN (2,QSigma_mono_lemma));
   2.347 -
   2.348 -Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)";
   2.349 -by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
   2.350 -qed "QInl_mono";
   2.351 -
   2.352 -Goalw [QInr_def] "a<=b ==> QInr(a) <= QInr(b)";
   2.353 -by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
   2.354 -qed "QInr_mono";
   2.355 -
   2.356 -Goal "[| A<=C;  B<=D |] ==> A <+> B <= C <+> D";
   2.357 -by (Blast_tac 1);
   2.358 -qed "qsum_mono";
   2.359 -
   2.360 -
     3.1 --- a/src/ZF/QPair.thy	Tue Jul 02 17:44:13 2002 +0200
     3.2 +++ b/src/ZF/QPair.thy	Tue Jul 02 22:46:23 2002 +0200
     3.3 @@ -9,20 +9,33 @@
     3.4  
     3.5  W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
     3.6  1966.
     3.7 +
     3.8 +Many proofs are borrowed from pair.thy and sum.thy
     3.9 +
    3.10 +Do we EVER have rank(a) < rank(<a;b>) ?  Perhaps if the latter rank
    3.11 +    is not a limit ordinal? 
    3.12  *)
    3.13  
    3.14 -QPair = Sum + mono +
    3.15 +theory QPair = Sum + mono:
    3.16 +
    3.17 +constdefs
    3.18 +  QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
    3.19 +    "<a;b> == a+b"
    3.20  
    3.21 -consts
    3.22 -  QPair     :: "[i, i] => i"                      ("<(_;/ _)>")
    3.23 -  qfst,qsnd :: "i => i"
    3.24 +  qfst :: "i => i"
    3.25 +    "qfst(p) == THE a. EX b. p=<a;b>"
    3.26 +
    3.27 +  qsnd :: "i => i"
    3.28 +    "qsnd(p) == THE b. EX a. p=<a;b>"
    3.29 +
    3.30    qsplit    :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
    3.31 -  qconverse :: "i => i"
    3.32 -  QSigma    :: "[i, i => i] => i"
    3.33 +    "qsplit(c,p) == c(qfst(p), qsnd(p))"
    3.34  
    3.35 -  "<+>"     :: "[i,i]=>i"                         (infixr 65)
    3.36 -  QInl,QInr :: "i=>i"
    3.37 -  qcase     :: "[i=>i, i=>i, i]=>i"
    3.38 +  qconverse :: "i => i"
    3.39 +    "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
    3.40 +
    3.41 +  QSigma    :: "[i, i => i] => i"
    3.42 +    "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
    3.43  
    3.44  syntax
    3.45    "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
    3.46 @@ -32,23 +45,356 @@
    3.47    "QSUM x:A. B"  => "QSigma(A, %x. B)"
    3.48    "A <*> B"      => "QSigma(A, _K(B))"
    3.49  
    3.50 +constdefs
    3.51 +  qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)
    3.52 +    "A <+> B      == ({0} <*> A) Un ({1} <*> B)"
    3.53  
    3.54 -defs
    3.55 -  QPair_def       "<a;b> == a+b"
    3.56 -  qfst_def        "qfst(p) == THE a. EX b. p=<a;b>"
    3.57 -  qsnd_def        "qsnd(p) == THE b. EX a. p=<a;b>"
    3.58 -  qsplit_def      "qsplit(c,p) == c(qfst(p), qsnd(p))"
    3.59 +  QInl :: "i=>i"
    3.60 +    "QInl(a)      == <0;a>"
    3.61 +
    3.62 +  QInr :: "i=>i"
    3.63 +    "QInr(b)      == <1;b>"
    3.64 +
    3.65 +  qcase     :: "[i=>i, i=>i, i]=>i"
    3.66 +    "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
    3.67 +
    3.68 +
    3.69 +print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
    3.70 +
    3.71 +
    3.72 +(**** Quine ordered pairing ****)
    3.73 +
    3.74 +(** Lemmas for showing that <a;b> uniquely determines a and b **)
    3.75 +
    3.76 +lemma QPair_empty [simp]: "<0;0> = 0"
    3.77 +by (simp add: QPair_def)
    3.78 +
    3.79 +lemma QPair_iff [simp]: "<a;b> = <c;d> <-> a=c & b=d"
    3.80 +apply (simp add: QPair_def)
    3.81 +apply (rule sum_equal_iff)
    3.82 +done
    3.83 +
    3.84 +lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!]
    3.85 +
    3.86 +lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
    3.87 +by blast
    3.88 +
    3.89 +lemma QPair_inject2: "<a;b> = <c;d> ==> b=d"
    3.90 +by blast
    3.91 +
    3.92 +
    3.93 +(*** QSigma: Disjoint union of a family of sets
    3.94 +     Generalizes Cartesian product ***)
    3.95 +
    3.96 +lemma QSigmaI [intro!]: "[| a:A;  b:B(a) |] ==> <a;b> : QSigma(A,B)"
    3.97 +by (simp add: QSigma_def)
    3.98 +
    3.99 +
   3.100 +(*The general elimination rule*)
   3.101 +lemma QSigmaE:
   3.102 +    "[| c: QSigma(A,B);   
   3.103 +        !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
   3.104 +     |] ==> P"
   3.105 +apply (simp add: QSigma_def, blast) 
   3.106 +done
   3.107 +
   3.108 +(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
   3.109 +
   3.110 +lemma QSigmaE [elim!]:
   3.111 +    "[| c: QSigma(A,B);   
   3.112 +        !!x y.[| x:A;  y:B(x);  c=<x;y> |] ==> P  
   3.113 +     |] ==> P"
   3.114 +apply (simp add: QSigma_def, blast) 
   3.115 +done
   3.116 +
   3.117 +lemma QSigmaE2 [elim!]:
   3.118 +    "[| <a;b>: QSigma(A,B); [| a:A;  b:B(a) |] ==> P |] ==> P"
   3.119 +by (simp add: QSigma_def) 
   3.120 +
   3.121 +lemma QSigmaD1: "<a;b> : QSigma(A,B) ==> a : A"
   3.122 +by blast
   3.123 +
   3.124 +lemma QSigmaD2: "<a;b> : QSigma(A,B) ==> b : B(a)"
   3.125 +by blast
   3.126 +
   3.127 +lemma QSigma_cong:
   3.128 +    "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==>  
   3.129 +     QSigma(A,B) = QSigma(A',B')"
   3.130 +by (simp add: QSigma_def) 
   3.131 +
   3.132 +lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0"
   3.133 +by blast
   3.134 +
   3.135 +lemma QSigma_empty2 [simp]: "A <*> 0 = 0"
   3.136 +by blast
   3.137 +
   3.138 +
   3.139 +(*** Projections: qfst, qsnd ***)
   3.140 +
   3.141 +lemma qfst_conv [simp]: "qfst(<a;b>) = a"
   3.142 +by (simp add: qfst_def, blast)
   3.143 +
   3.144 +lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
   3.145 +by (simp add: qsnd_def, blast)
   3.146 +
   3.147 +lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A"
   3.148 +by auto
   3.149 +
   3.150 +lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
   3.151 +by auto
   3.152 +
   3.153 +lemma QPair_qfst_qsnd_eq: "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
   3.154 +by auto
   3.155 +
   3.156 +
   3.157 +(*** Eliminator - qsplit ***)
   3.158 +
   3.159 +(*A META-equality, so that it applies to higher types as well...*)
   3.160 +lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
   3.161 +by (simp add: qsplit_def)
   3.162 +
   3.163 +
   3.164 +lemma qsplit_type [elim!]:
   3.165 +    "[|  p:QSigma(A,B);    
   3.166 +         !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>)  
   3.167 +     |] ==> qsplit(%x y. c(x,y), p) : C(p)"
   3.168 +by auto 
   3.169 +
   3.170 +lemma expand_qsplit: 
   3.171 + "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))"
   3.172 +apply (simp add: qsplit_def, auto)
   3.173 +done
   3.174 +
   3.175 +
   3.176 +(*** qsplit for predicates: result type o ***)
   3.177 +
   3.178 +lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
   3.179 +by (simp add: qsplit_def)
   3.180 +
   3.181 +
   3.182 +lemma qsplitE:
   3.183 +    "[| qsplit(R,z);  z:QSigma(A,B);                     
   3.184 +        !!x y. [| z = <x;y>;  R(x,y) |] ==> P            
   3.185 +    |] ==> P"
   3.186 +apply (simp add: qsplit_def, auto) 
   3.187 +done
   3.188 +
   3.189 +lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
   3.190 +by (simp add: qsplit_def)
   3.191 +
   3.192 +
   3.193 +(*** qconverse ***)
   3.194 +
   3.195 +lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
   3.196 +by (simp add: qconverse_def, blast)
   3.197 +
   3.198 +lemma qconverseD [elim!]: "<a;b> : qconverse(r) ==> <b;a> : r"
   3.199 +by (simp add: qconverse_def, blast)
   3.200 +
   3.201 +lemma qconverseE [elim!]:
   3.202 +    "[| yx : qconverse(r);   
   3.203 +        !!x y. [| yx=<y;x>;  <x;y>:r |] ==> P  
   3.204 +     |] ==> P"
   3.205 +apply (simp add: qconverse_def, blast) 
   3.206 +done
   3.207 +
   3.208 +lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
   3.209 +by blast
   3.210 +
   3.211 +lemma qconverse_type: "r <= A <*> B ==> qconverse(r) <= B <*> A"
   3.212 +by blast
   3.213 +
   3.214 +lemma qconverse_prod: "qconverse(A <*> B) = B <*> A"
   3.215 +by blast
   3.216 +
   3.217 +lemma qconverse_empty: "qconverse(0) = 0"
   3.218 +by blast
   3.219 +
   3.220 +
   3.221 +(**** The Quine-inspired notion of disjoint sum ****)
   3.222 +
   3.223 +lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
   3.224 +
   3.225 +(** Introduction rules for the injections **)
   3.226 +
   3.227 +lemma QInlI [intro!]: "a : A ==> QInl(a) : A <+> B"
   3.228 +by (simp add: qsum_defs, blast)
   3.229  
   3.230 -  qconverse_def   "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
   3.231 -  QSigma_def      "QSigma(A,B)  ==  UN x:A. UN y:B(x). {<x;y>}"
   3.232 +lemma QInrI [intro!]: "b : B ==> QInr(b) : A <+> B"
   3.233 +by (simp add: qsum_defs, blast)
   3.234 +
   3.235 +(** Elimination rules **)
   3.236 +
   3.237 +lemma qsumE [elim!]:
   3.238 +    "[| u: A <+> B;   
   3.239 +        !!x. [| x:A;  u=QInl(x) |] ==> P;  
   3.240 +        !!y. [| y:B;  u=QInr(y) |] ==> P  
   3.241 +     |] ==> P"
   3.242 +apply (simp add: qsum_defs, blast) 
   3.243 +done
   3.244 +
   3.245 +
   3.246 +(** Injection and freeness equivalences, for rewriting **)
   3.247 +
   3.248 +lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b"
   3.249 +by (simp add: qsum_defs )
   3.250 +
   3.251 +lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
   3.252 +by (simp add: qsum_defs )
   3.253 +
   3.254 +lemma QInl_QInr_iff [iff]: "QInl(a)=QInr(b) <-> False"
   3.255 +by (simp add: qsum_defs )
   3.256 +
   3.257 +lemma QInr_QInl_iff [iff]: "QInr(b)=QInl(a) <-> False"
   3.258 +by (simp add: qsum_defs )
   3.259 +
   3.260 +lemma qsum_empty [simp]: "0<+>0 = 0"
   3.261 +by (simp add: qsum_defs )
   3.262 +
   3.263 +(*Injection and freeness rules*)
   3.264 +
   3.265 +lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
   3.266 +lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
   3.267 +lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE]
   3.268 +lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE]
   3.269 +
   3.270 +lemma QInlD: "QInl(a): A<+>B ==> a: A"
   3.271 +by blast
   3.272 +
   3.273 +lemma QInrD: "QInr(b): A<+>B ==> b: B"
   3.274 +by blast
   3.275 +
   3.276 +(** <+> is itself injective... who cares?? **)
   3.277 +
   3.278 +lemma qsum_iff:
   3.279 +     "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"
   3.280 +apply blast
   3.281 +done
   3.282 +
   3.283 +lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D"
   3.284 +by blast
   3.285 +
   3.286 +lemma qsum_equal_iff: "A <+> B = C <+> D <-> A=C & B=D"
   3.287 +apply (simp (no_asm) add: extension qsum_subset_iff)
   3.288 +apply blast
   3.289 +done
   3.290 +
   3.291 +(*** Eliminator -- qcase ***)
   3.292 +
   3.293 +lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
   3.294 +by (simp add: qsum_defs )
   3.295 +
   3.296 +
   3.297 +lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)"
   3.298 +by (simp add: qsum_defs )
   3.299 +
   3.300 +lemma qcase_type:
   3.301 +    "[| u: A <+> B;  
   3.302 +        !!x. x: A ==> c(x): C(QInl(x));    
   3.303 +        !!y. y: B ==> d(y): C(QInr(y))  
   3.304 +     |] ==> qcase(c,d,u) : C(u)"
   3.305 +apply (simp add: qsum_defs , auto) 
   3.306 +done
   3.307 +
   3.308 +(** Rules for the Part primitive **)
   3.309 +
   3.310 +lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x: A}"
   3.311 +by blast
   3.312 +
   3.313 +lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y: B}"
   3.314 +by blast
   3.315 +
   3.316 +lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}"
   3.317 +by blast
   3.318  
   3.319 -  qsum_def        "A <+> B      == ({0} <*> A) Un ({1} <*> B)"
   3.320 -  QInl_def        "QInl(a)      == <0;a>"
   3.321 -  QInr_def        "QInr(b)      == <1;b>"
   3.322 -  qcase_def       "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
   3.323 +lemma Part_qsum_equality: "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"
   3.324 +by blast
   3.325 +
   3.326 +
   3.327 +(*** Monotonicity ***)
   3.328 +
   3.329 +lemma QPair_mono: "[| a<=c;  b<=d |] ==> <a;b> <= <c;d>"
   3.330 +by (simp add: QPair_def sum_mono)
   3.331 +
   3.332 +lemma QSigma_mono [rule_format]:
   3.333 +     "[| A<=C;  ALL x:A. B(x) <= D(x) |] ==> QSigma(A,B) <= QSigma(C,D)"
   3.334 +by blast
   3.335 +
   3.336 +lemma QInl_mono: "a<=b ==> QInl(a) <= QInl(b)"
   3.337 +by (simp add: QInl_def subset_refl [THEN QPair_mono])
   3.338 +
   3.339 +lemma QInr_mono: "a<=b ==> QInr(a) <= QInr(b)"
   3.340 +by (simp add: QInr_def subset_refl [THEN QPair_mono])
   3.341 +
   3.342 +lemma qsum_mono: "[| A<=C;  B<=D |] ==> A <+> B <= C <+> D"
   3.343 +by blast
   3.344 +
   3.345 +ML
   3.346 +{*
   3.347 +val qsum_defs = thms "qsum_defs";
   3.348 +
   3.349 +val QPair_empty = thm "QPair_empty";
   3.350 +val QPair_iff = thm "QPair_iff";
   3.351 +val QPair_inject = thm "QPair_inject";
   3.352 +val QPair_inject1 = thm "QPair_inject1";
   3.353 +val QPair_inject2 = thm "QPair_inject2";
   3.354 +val QSigmaI = thm "QSigmaI";
   3.355 +val QSigmaE = thm "QSigmaE";
   3.356 +val QSigmaE = thm "QSigmaE";
   3.357 +val QSigmaE2 = thm "QSigmaE2";
   3.358 +val QSigmaD1 = thm "QSigmaD1";
   3.359 +val QSigmaD2 = thm "QSigmaD2";
   3.360 +val QSigma_cong = thm "QSigma_cong";
   3.361 +val QSigma_empty1 = thm "QSigma_empty1";
   3.362 +val QSigma_empty2 = thm "QSigma_empty2";
   3.363 +val qfst_conv = thm "qfst_conv";
   3.364 +val qsnd_conv = thm "qsnd_conv";
   3.365 +val qfst_type = thm "qfst_type";
   3.366 +val qsnd_type = thm "qsnd_type";
   3.367 +val QPair_qfst_qsnd_eq = thm "QPair_qfst_qsnd_eq";
   3.368 +val qsplit = thm "qsplit";
   3.369 +val qsplit_type = thm "qsplit_type";
   3.370 +val expand_qsplit = thm "expand_qsplit";
   3.371 +val qsplitI = thm "qsplitI";
   3.372 +val qsplitE = thm "qsplitE";
   3.373 +val qsplitD = thm "qsplitD";
   3.374 +val qconverseI = thm "qconverseI";
   3.375 +val qconverseD = thm "qconverseD";
   3.376 +val qconverseE = thm "qconverseE";
   3.377 +val qconverse_qconverse = thm "qconverse_qconverse";
   3.378 +val qconverse_type = thm "qconverse_type";
   3.379 +val qconverse_prod = thm "qconverse_prod";
   3.380 +val qconverse_empty = thm "qconverse_empty";
   3.381 +val QInlI = thm "QInlI";
   3.382 +val QInrI = thm "QInrI";
   3.383 +val qsumE = thm "qsumE";
   3.384 +val QInl_iff = thm "QInl_iff";
   3.385 +val QInr_iff = thm "QInr_iff";
   3.386 +val QInl_QInr_iff = thm "QInl_QInr_iff";
   3.387 +val QInr_QInl_iff = thm "QInr_QInl_iff";
   3.388 +val qsum_empty = thm "qsum_empty";
   3.389 +val QInl_inject = thm "QInl_inject";
   3.390 +val QInr_inject = thm "QInr_inject";
   3.391 +val QInl_neq_QInr = thm "QInl_neq_QInr";
   3.392 +val QInr_neq_QInl = thm "QInr_neq_QInl";
   3.393 +val QInlD = thm "QInlD";
   3.394 +val QInrD = thm "QInrD";
   3.395 +val qsum_iff = thm "qsum_iff";
   3.396 +val qsum_subset_iff = thm "qsum_subset_iff";
   3.397 +val qsum_equal_iff = thm "qsum_equal_iff";
   3.398 +val qcase_QInl = thm "qcase_QInl";
   3.399 +val qcase_QInr = thm "qcase_QInr";
   3.400 +val qcase_type = thm "qcase_type";
   3.401 +val Part_QInl = thm "Part_QInl";
   3.402 +val Part_QInr = thm "Part_QInr";
   3.403 +val Part_QInr2 = thm "Part_QInr2";
   3.404 +val Part_qsum_equality = thm "Part_qsum_equality";
   3.405 +val QPair_mono = thm "QPair_mono";
   3.406 +val QSigma_mono = thm "QSigma_mono";
   3.407 +val QInl_mono = thm "QInl_mono";
   3.408 +val QInr_mono = thm "QInr_mono";
   3.409 +val qsum_mono = thm "qsum_mono";
   3.410 +*}
   3.411 +
   3.412  end
   3.413  
   3.414 -ML
   3.415 -
   3.416 -val print_translation =
   3.417 -  [("QSigma", dependent_tr' ("@QSUM", "op <*>"))];
     4.1 --- a/src/ZF/QUniv.thy	Tue Jul 02 17:44:13 2002 +0200
     4.2 +++ b/src/ZF/QUniv.thy	Tue Jul 02 22:46:23 2002 +0200
     4.3 @@ -3,25 +3,242 @@
     4.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.5      Copyright   1993  University of Cambridge
     4.6  
     4.7 -A small universe for lazy recursive types.
     4.8 +A small universe for lazy recursive types
     4.9  *)
    4.10  
    4.11 -QUniv = Univ + QPair + mono + equalities +
    4.12 +(** Properties involving Transset and Sum **)
    4.13 +
    4.14 +theory QUniv = Univ + QPair + mono + equalities:
    4.15  
    4.16  (*Disjoint sums as a datatype*)
    4.17  rep_datatype 
    4.18 -  elim		sumE
    4.19 -  induct	TrueI
    4.20 -  case_eqns	case_Inl, case_Inr
    4.21 +  elimination	sumE
    4.22 +  induction	TrueI
    4.23 +  case_eqns	case_Inl case_Inr
    4.24  
    4.25  (*Variant disjoint sums as a datatype*)
    4.26  rep_datatype 
    4.27 -  elim		qsumE
    4.28 -  induct	TrueI
    4.29 -  case_eqns	qcase_QInl, qcase_QInr
    4.30 +  elimination	qsumE
    4.31 +  induction	TrueI
    4.32 +  case_eqns	qcase_QInl qcase_QInr
    4.33  
    4.34  constdefs
    4.35    quniv :: "i => i"
    4.36     "quniv(A) == Pow(univ(eclose(A)))"
    4.37  
    4.38 +
    4.39 +lemma Transset_includes_summands:
    4.40 +     "[| Transset(C); A+B <= C |] ==> A <= C & B <= C"
    4.41 +apply (simp add: sum_def Un_subset_iff) 
    4.42 +apply (blast dest: Transset_includes_range)
    4.43 +done
    4.44 +
    4.45 +lemma Transset_sum_Int_subset:
    4.46 +     "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"
    4.47 +apply (simp add: sum_def Int_Un_distrib2) 
    4.48 +apply (blast dest: Transset_Pair_D)
    4.49 +done
    4.50 +
    4.51 +(** Introduction and elimination rules avoid tiresome folding/unfolding **)
    4.52 +
    4.53 +lemma qunivI: "X <= univ(eclose(A)) ==> X : quniv(A)"
    4.54 +by (simp add: quniv_def)
    4.55 +
    4.56 +lemma qunivD: "X : quniv(A) ==> X <= univ(eclose(A))"
    4.57 +by (simp add: quniv_def)
    4.58 +
    4.59 +lemma quniv_mono: "A<=B ==> quniv(A) <= quniv(B)"
    4.60 +apply (unfold quniv_def)
    4.61 +apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
    4.62 +done
    4.63 +
    4.64 +(*** Closure properties ***)
    4.65 +
    4.66 +lemma univ_eclose_subset_quniv: "univ(eclose(A)) <= quniv(A)"
    4.67 +apply (simp add: quniv_def Transset_iff_Pow [symmetric]) 
    4.68 +apply (rule Transset_eclose [THEN Transset_univ])
    4.69 +done
    4.70 +
    4.71 +(*Key property for proving A_subset_quniv; requires eclose in def of quniv*)
    4.72 +lemma univ_subset_quniv: "univ(A) <= quniv(A)"
    4.73 +apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans])
    4.74 +apply (rule univ_eclose_subset_quniv)
    4.75 +done
    4.76 +
    4.77 +lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD, standard]
    4.78 +
    4.79 +lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)"
    4.80 +apply (unfold quniv_def)
    4.81 +apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono])
    4.82 +done
    4.83 +
    4.84 +lemmas univ_subset_into_quniv =
    4.85 +    PowI [THEN Pow_univ_subset_quniv [THEN subsetD], standard]
    4.86 +
    4.87 +lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv, standard]
    4.88 +lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv, standard]
    4.89 +lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv, standard]
    4.90 +
    4.91 +lemmas A_subset_quniv =  subset_trans [OF A_subset_univ univ_subset_quniv]
    4.92 +
    4.93 +lemmas A_into_quniv = A_subset_quniv [THEN subsetD, standard]
    4.94 +
    4.95 +(*** univ(A) closure for Quine-inspired pairs and injections ***)
    4.96 +
    4.97 +(*Quine ordered pairs*)
    4.98 +lemma QPair_subset_univ: 
    4.99 +    "[| a <= univ(A);  b <= univ(A) |] ==> <a;b> <= univ(A)"
   4.100 +by (simp add: QPair_def sum_subset_univ)
   4.101 +
   4.102 +(** Quine disjoint sum **)
   4.103 +
   4.104 +lemma QInl_subset_univ: "a <= univ(A) ==> QInl(a) <= univ(A)"
   4.105 +apply (unfold QInl_def)
   4.106 +apply (erule empty_subsetI [THEN QPair_subset_univ])
   4.107 +done
   4.108 +
   4.109 +lemmas naturals_subset_nat = 
   4.110 +    Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec, standard]
   4.111 +
   4.112 +lemmas naturals_subset_univ =
   4.113 +    subset_trans [OF naturals_subset_nat nat_subset_univ]
   4.114 +
   4.115 +lemma QInr_subset_univ: "a <= univ(A) ==> QInr(a) <= univ(A)"
   4.116 +apply (unfold QInr_def)
   4.117 +apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ])
   4.118 +done
   4.119 +
   4.120 +(*** Closure for Quine-inspired products and sums ***)
   4.121 +
   4.122 +(*Quine ordered pairs*)
   4.123 +lemma QPair_in_quniv: 
   4.124 +    "[| a: quniv(A);  b: quniv(A) |] ==> <a;b> : quniv(A)"
   4.125 +by (simp add: quniv_def QPair_def sum_subset_univ) 
   4.126 +
   4.127 +lemma QSigma_quniv: "quniv(A) <*> quniv(A) <= quniv(A)" 
   4.128 +by (blast intro: QPair_in_quniv)
   4.129 +
   4.130 +lemmas QSigma_subset_quniv =  subset_trans [OF QSigma_mono QSigma_quniv]
   4.131 +
   4.132 +(*The opposite inclusion*)
   4.133 +lemma quniv_QPair_D: 
   4.134 +    "<a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)"
   4.135 +apply (unfold quniv_def QPair_def)
   4.136 +apply (rule Transset_includes_summands [THEN conjE]) 
   4.137 +apply (rule Transset_eclose [THEN Transset_univ])
   4.138 +apply (erule PowD, blast) 
   4.139 +done
   4.140 +
   4.141 +lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE, standard]
   4.142 +
   4.143 +lemma quniv_QPair_iff: "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"
   4.144 +by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
   4.145 +
   4.146 +
   4.147 +(** Quine disjoint sum **)
   4.148 +
   4.149 +lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) : quniv(A)"
   4.150 +by (simp add: QInl_def zero_in_quniv QPair_in_quniv)
   4.151 +
   4.152 +lemma QInr_in_quniv: "b: quniv(A) ==> QInr(b) : quniv(A)"
   4.153 +by (simp add: QInr_def one_in_quniv QPair_in_quniv)
   4.154 +
   4.155 +lemma qsum_quniv: "quniv(C) <+> quniv(C) <= quniv(C)"
   4.156 +by (blast intro: QInl_in_quniv QInr_in_quniv)
   4.157 +
   4.158 +lemmas qsum_subset_quniv = subset_trans [OF qsum_mono qsum_quniv]
   4.159 +
   4.160 +
   4.161 +(*** The natural numbers ***)
   4.162 +
   4.163 +lemmas nat_subset_quniv =  subset_trans [OF nat_subset_univ univ_subset_quniv]
   4.164 +
   4.165 +(* n:nat ==> n:quniv(A) *)
   4.166 +lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD, standard]
   4.167 +
   4.168 +lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv]
   4.169 +
   4.170 +lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard]
   4.171 +
   4.172 +
   4.173 +(*** Intersecting <a;b> with Vfrom... ***)
   4.174 +
   4.175 +lemma QPair_Int_Vfrom_succ_subset: 
   4.176 + "Transset(X) ==>           
   4.177 +       <a;b> Int Vfrom(X, succ(i))  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>"
   4.178 +by (simp add: QPair_def sum_def Int_Un_distrib2 Un_mono
   4.179 +              product_Int_Vfrom_subset [THEN subset_trans]
   4.180 +              Sigma_mono [OF Int_lower1 subset_refl])
   4.181 +
   4.182 +(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****)
   4.183 +
   4.184 +(*Rule for level i -- preserving the level, not decreasing it*)
   4.185 +
   4.186 +lemma QPair_Int_Vfrom_subset: 
   4.187 + "Transset(X) ==>           
   4.188 +       <a;b> Int Vfrom(X,i)  <=  <a Int Vfrom(X,i);  b Int Vfrom(X,i)>"
   4.189 +apply (unfold QPair_def)
   4.190 +apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset])
   4.191 +done
   4.192 +
   4.193 +(*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*)
   4.194 +lemmas QPair_Int_Vset_subset_trans =
   4.195 +     subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono]
   4.196 +
   4.197 +lemma QPair_Int_Vset_subset_UN:
   4.198 +     "Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"
   4.199 +apply (erule Ord_cases)
   4.200 +(*0 case*)
   4.201 +apply (simp add: Vfrom_0)
   4.202 +(*succ(j) case*)
   4.203 +apply (erule ssubst) 
   4.204 +apply (rule Transset_0 [THEN QPair_Int_Vfrom_succ_subset, THEN subset_trans])
   4.205 +apply (rule succI1 [THEN UN_upper])
   4.206 +(*Limit(i) case*)
   4.207 +apply (simp del: UN_simps 
   4.208 +        add: Limit_Vfrom_eq Int_UN_distrib UN_mono QPair_Int_Vset_subset_trans)
   4.209 +done
   4.210 +
   4.211 +ML
   4.212 +{*
   4.213 +val Transset_includes_summands = thm "Transset_includes_summands";
   4.214 +val Transset_sum_Int_subset = thm "Transset_sum_Int_subset";
   4.215 +val qunivI = thm "qunivI";
   4.216 +val qunivD = thm "qunivD";
   4.217 +val quniv_mono = thm "quniv_mono";
   4.218 +val univ_eclose_subset_quniv = thm "univ_eclose_subset_quniv";
   4.219 +val univ_subset_quniv = thm "univ_subset_quniv";
   4.220 +val univ_into_quniv = thm "univ_into_quniv";
   4.221 +val Pow_univ_subset_quniv = thm "Pow_univ_subset_quniv";
   4.222 +val univ_subset_into_quniv = thm "univ_subset_into_quniv";
   4.223 +val zero_in_quniv = thm "zero_in_quniv";
   4.224 +val one_in_quniv = thm "one_in_quniv";
   4.225 +val two_in_quniv = thm "two_in_quniv";
   4.226 +val A_subset_quniv = thm "A_subset_quniv";
   4.227 +val A_into_quniv = thm "A_into_quniv";
   4.228 +val QPair_subset_univ = thm "QPair_subset_univ";
   4.229 +val QInl_subset_univ = thm "QInl_subset_univ";
   4.230 +val naturals_subset_nat = thm "naturals_subset_nat";
   4.231 +val naturals_subset_univ = thm "naturals_subset_univ";
   4.232 +val QInr_subset_univ = thm "QInr_subset_univ";
   4.233 +val QPair_in_quniv = thm "QPair_in_quniv";
   4.234 +val QSigma_quniv = thm "QSigma_quniv";
   4.235 +val QSigma_subset_quniv = thm "QSigma_subset_quniv";
   4.236 +val quniv_QPair_D = thm "quniv_QPair_D";
   4.237 +val quniv_QPair_E = thm "quniv_QPair_E";
   4.238 +val quniv_QPair_iff = thm "quniv_QPair_iff";
   4.239 +val QInl_in_quniv = thm "QInl_in_quniv";
   4.240 +val QInr_in_quniv = thm "QInr_in_quniv";
   4.241 +val qsum_quniv = thm "qsum_quniv";
   4.242 +val qsum_subset_quniv = thm "qsum_subset_quniv";
   4.243 +val nat_subset_quniv = thm "nat_subset_quniv";
   4.244 +val nat_into_quniv = thm "nat_into_quniv";
   4.245 +val bool_subset_quniv = thm "bool_subset_quniv";
   4.246 +val bool_into_quniv = thm "bool_into_quniv";
   4.247 +val QPair_Int_Vfrom_succ_subset = thm "QPair_Int_Vfrom_succ_subset";
   4.248 +val QPair_Int_Vfrom_subset = thm "QPair_Int_Vfrom_subset";
   4.249 +val QPair_Int_Vset_subset_trans = thm "QPair_Int_Vset_subset_trans";
   4.250 +val QPair_Int_Vset_subset_UN = thm "QPair_Int_Vset_subset_UN";
   4.251 +*}
   4.252 +
   4.253  end