--- a/src/ZF/IsaMakefile Tue Jul 02 17:44:13 2002 +0200
+++ b/src/ZF/IsaMakefile Tue Jul 02 22:46:23 2002 +0200
@@ -39,7 +39,7 @@
Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \
Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \
OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy \
- QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML \
+ QPair.thy QUniv.thy ROOT.ML \
Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \
Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \
Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \
--- a/src/ZF/QPair.ML Tue Jul 02 17:44:13 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,357 +0,0 @@
-(* Title: ZF/QPair.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-Quine-inspired ordered pairs and disjoint sums, for non-well-founded data
-structures in ZF. Does not precisely follow Quine's construction. Thanks
-to Thomas Forster for suggesting this approach!
-
-W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
-1966.
-
-Many proofs are borrowed from pair.ML and sum.ML
-
-Do we EVER have rank(a) < rank(<a;b>) ? Perhaps if the latter rank
- is not a limit ordinal?
-*)
-
-(**** Quine ordered pairing ****)
-
-(** Lemmas for showing that <a;b> uniquely determines a and b **)
-
-Goalw [QPair_def] "<0;0> = 0";
-by (Simp_tac 1);
-qed "QPair_empty";
-
-Goalw [QPair_def] "<a;b> = <c;d> <-> a=c & b=d";
-by (rtac sum_equal_iff 1);
-qed "QPair_iff";
-
-bind_thm ("QPair_inject", QPair_iff RS iffD1 RS conjE);
-
-Addsimps [QPair_empty, QPair_iff];
-AddSEs [QPair_inject];
-
-Goal "<a;b> = <c;d> ==> a=c";
-by (Blast_tac 1) ;
-qed "QPair_inject1";
-
-Goal "<a;b> = <c;d> ==> b=d";
-by (Blast_tac 1) ;
-qed "QPair_inject2";
-
-
-(*** QSigma: Disjoint union of a family of sets
- Generalizes Cartesian product ***)
-
-Goalw [QSigma_def] "[| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)";
-by (Blast_tac 1) ;
-qed "QSigmaI";
-
-AddSIs [QSigmaI];
-
-(*The general elimination rule*)
-val major::prems= Goalw [QSigma_def]
- "[| c: QSigma(A,B); \
-\ !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P \
-\ |] ==> P";
-by (cut_facts_tac [major] 1);
-by (REPEAT (eresolve_tac [UN_E, singletonE] 1 ORELSE ares_tac prems 1)) ;
-qed "QSigmaE";
-
-(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
-
-bind_thm ("QSigmaE2",
- rule_by_tactic (REPEAT_FIRST (etac QPair_inject ORELSE' bound_hyp_subst_tac)
- THEN prune_params_tac)
- (inst "c" "<a;b>" QSigmaE));
-
-AddSEs [QSigmaE2, QSigmaE];
-
-Goal "<a;b> : QSigma(A,B) ==> a : A";
-by (Blast_tac 1) ;
-qed "QSigmaD1";
-
-Goal "<a;b> : QSigma(A,B) ==> b : B(a)";
-by (Blast_tac 1) ;
-qed "QSigmaD2";
-
-
-val prems= Goalw [QSigma_def]
- "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==> \
-\ QSigma(A,B) = QSigma(A',B')";
-by (simp_tac (simpset() addsimps prems) 1) ;
-qed "QSigma_cong";
-
-Goal "QSigma(0,B) = 0";
-by (Blast_tac 1) ;
-qed "QSigma_empty1";
-
-Goal "A <*> 0 = 0";
-by (Blast_tac 1) ;
-qed "QSigma_empty2";
-
-Addsimps [QSigma_empty1, QSigma_empty2];
-
-
-(*** Projections: qfst, qsnd ***)
-
-Goalw [qfst_def] "qfst(<a;b>) = a";
-by (Blast_tac 1) ;
-qed "qfst_conv";
-
-Goalw [qsnd_def] "qsnd(<a;b>) = b";
-by (Blast_tac 1) ;
-qed "qsnd_conv";
-
-Addsimps [qfst_conv, qsnd_conv];
-
-Goal "p:QSigma(A,B) ==> qfst(p) : A";
-by (Auto_tac) ;
-qed "qfst_type";
-AddTCs [qfst_type];
-
-Goal "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))";
-by (Auto_tac) ;
-qed "qsnd_type";
-AddTCs [qsnd_type];
-
-Goal "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a";
-by Auto_tac;
-qed "QPair_qfst_qsnd_eq";
-
-
-(*** Eliminator - qsplit ***)
-
-(*A META-equality, so that it applies to higher types as well...*)
-Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)";
-by (Simp_tac 1);
-qed "qsplit";
-Addsimps [qsplit];
-
-val major::prems= Goal
- "[| p:QSigma(A,B); \
-\ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>) \
-\ |] ==> qsplit(%x y. c(x,y), p) : C(p)";
-by (rtac (major RS QSigmaE) 1);
-by (asm_simp_tac (simpset() addsimps prems) 1) ;
-qed "qsplit_type";
-
-Goalw [qsplit_def]
- "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))";
-by Auto_tac;
-qed "expand_qsplit";
-
-
-(*** qsplit for predicates: result type o ***)
-
-Goalw [qsplit_def] "R(a,b) ==> qsplit(R, <a;b>)";
-by (Asm_simp_tac 1);
-qed "qsplitI";
-
-val major::sigma::prems = Goalw [qsplit_def]
- "[| qsplit(R,z); z:QSigma(A,B); \
-\ !!x y. [| z = <x;y>; R(x,y) |] ==> P \
-\ |] ==> P";
-by (rtac (sigma RS QSigmaE) 1);
-by (cut_facts_tac [major] 1);
-by (REPEAT (ares_tac prems 1));
-by (Asm_full_simp_tac 1);
-qed "qsplitE";
-
-Goalw [qsplit_def] "qsplit(R,<a;b>) ==> R(a,b)";
-by (Asm_full_simp_tac 1);
-qed "qsplitD";
-
-
-(*** qconverse ***)
-
-Goalw [qconverse_def] "<a;b>:r ==> <b;a>:qconverse(r)";
-by (Blast_tac 1) ;
-qed "qconverseI";
-
-Goalw [qconverse_def] "<a;b> : qconverse(r) ==> <b;a> : r";
-by (Blast_tac 1) ;
-qed "qconverseD";
-
-val [major,minor]= Goalw [qconverse_def]
- "[| yx : qconverse(r); \
-\ !!x y. [| yx=<y;x>; <x;y>:r |] ==> P \
-\ |] ==> P";
-by (rtac (major RS ReplaceE) 1);
-by (REPEAT (eresolve_tac [exE, conjE, minor] 1));
-by (hyp_subst_tac 1);
-by (assume_tac 1) ;
-qed "qconverseE";
-
-AddSIs [qconverseI];
-AddSEs [qconverseD, qconverseE];
-
-Goal "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r";
-by (Blast_tac 1) ;
-qed "qconverse_qconverse";
-
-Goal "r <= A <*> B ==> qconverse(r) <= B <*> A";
-by (Blast_tac 1) ;
-qed "qconverse_type";
-
-Goal "qconverse(A <*> B) = B <*> A";
-by (Blast_tac 1) ;
-qed "qconverse_prod";
-
-Goal "qconverse(0) = 0";
-by (Blast_tac 1) ;
-qed "qconverse_empty";
-
-
-(**** The Quine-inspired notion of disjoint sum ****)
-
-bind_thms ("qsum_defs", [qsum_def,QInl_def,QInr_def,qcase_def]);
-
-(** Introduction rules for the injections **)
-
-Goalw qsum_defs "a : A ==> QInl(a) : A <+> B";
-by (Blast_tac 1);
-qed "QInlI";
-
-Goalw qsum_defs "b : B ==> QInr(b) : A <+> B";
-by (Blast_tac 1);
-qed "QInrI";
-
-(** Elimination rules **)
-
-val major::prems = Goalw qsum_defs
- "[| u: A <+> B; \
-\ !!x. [| x:A; u=QInl(x) |] ==> P; \
-\ !!y. [| y:B; u=QInr(y) |] ==> P \
-\ |] ==> P";
-by (rtac (major RS UnE) 1);
-by (REPEAT (rtac refl 1
- ORELSE eresolve_tac (prems@[QSigmaE,singletonE,ssubst]) 1));
-qed "qsumE";
-
-AddSIs [QInlI, QInrI];
-
-(** Injection and freeness equivalences, for rewriting **)
-
-Goalw qsum_defs "QInl(a)=QInl(b) <-> a=b";
-by (Simp_tac 1);
-qed "QInl_iff";
-
-Goalw qsum_defs "QInr(a)=QInr(b) <-> a=b";
-by (Simp_tac 1);
-qed "QInr_iff";
-
-Goalw qsum_defs "QInl(a)=QInr(b) <-> False";
-by (Simp_tac 1);
-qed "QInl_QInr_iff";
-
-Goalw qsum_defs "QInr(b)=QInl(a) <-> False";
-by (Simp_tac 1);
-qed "QInr_QInl_iff";
-
-Goalw qsum_defs "0<+>0 = 0";
-by (Simp_tac 1);
-qed "qsum_empty";
-
-(*Injection and freeness rules*)
-
-bind_thm ("QInl_inject", (QInl_iff RS iffD1));
-bind_thm ("QInr_inject", (QInr_iff RS iffD1));
-bind_thm ("QInl_neq_QInr", (QInl_QInr_iff RS iffD1 RS FalseE));
-bind_thm ("QInr_neq_QInl", (QInr_QInl_iff RS iffD1 RS FalseE));
-
-AddSEs [qsumE, QInl_neq_QInr, QInr_neq_QInl];
-AddSDs [QInl_inject, QInr_inject];
-Addsimps [QInl_iff, QInr_iff, QInl_QInr_iff, QInr_QInl_iff, qsum_empty];
-
-Goal "QInl(a): A<+>B ==> a: A";
-by (Blast_tac 1);
-qed "QInlD";
-
-Goal "QInr(b): A<+>B ==> b: B";
-by (Blast_tac 1);
-qed "QInrD";
-
-(** <+> is itself injective... who cares?? **)
-
-Goal "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))";
-by (Blast_tac 1);
-qed "qsum_iff";
-
-Goal "A <+> B <= C <+> D <-> A<=C & B<=D";
-by (Blast_tac 1);
-qed "qsum_subset_iff";
-
-Goal "A <+> B = C <+> D <-> A=C & B=D";
-by (simp_tac (simpset() addsimps [extension,qsum_subset_iff]) 1);
-by (Blast_tac 1);
-qed "qsum_equal_iff";
-
-(*** Eliminator -- qcase ***)
-
-Goalw qsum_defs "qcase(c, d, QInl(a)) = c(a)";
-by (Simp_tac 1);
-qed "qcase_QInl";
-
-Goalw qsum_defs "qcase(c, d, QInr(b)) = d(b)";
-by (Simp_tac 1);
-qed "qcase_QInr";
-
-Addsimps [qcase_QInl, qcase_QInr];
-
-val major::prems = Goal
- "[| u: A <+> B; \
-\ !!x. x: A ==> c(x): C(QInl(x)); \
-\ !!y. y: B ==> d(y): C(QInr(y)) \
-\ |] ==> qcase(c,d,u) : C(u)";
-by (rtac (major RS qsumE) 1);
-by (ALLGOALS (etac ssubst));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
-qed "qcase_type";
-
-(** Rules for the Part primitive **)
-
-Goal "Part(A <+> B,QInl) = {QInl(x). x: A}";
-by (Blast_tac 1);
-qed "Part_QInl";
-
-Goal "Part(A <+> B,QInr) = {QInr(y). y: B}";
-by (Blast_tac 1);
-qed "Part_QInr";
-
-Goal "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}";
-by (Blast_tac 1);
-qed "Part_QInr2";
-
-Goal "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C";
-by (Blast_tac 1);
-qed "Part_qsum_equality";
-
-
-(*** Monotonicity ***)
-
-Goalw [QPair_def] "[| a<=c; b<=d |] ==> <a;b> <= <c;d>";
-by (REPEAT (ares_tac [sum_mono] 1));
-qed "QPair_mono";
-
-Goal "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> \
-\ QSigma(A,B) <= QSigma(C,D)";
-by (Blast_tac 1);
-qed "QSigma_mono_lemma";
-bind_thm ("QSigma_mono", ballI RSN (2,QSigma_mono_lemma));
-
-Goalw [QInl_def] "a<=b ==> QInl(a) <= QInl(b)";
-by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
-qed "QInl_mono";
-
-Goalw [QInr_def] "a<=b ==> QInr(a) <= QInr(b)";
-by (REPEAT (ares_tac [subset_refl RS QPair_mono] 1));
-qed "QInr_mono";
-
-Goal "[| A<=C; B<=D |] ==> A <+> B <= C <+> D";
-by (Blast_tac 1);
-qed "qsum_mono";
-
-
--- a/src/ZF/QPair.thy Tue Jul 02 17:44:13 2002 +0200
+++ b/src/ZF/QPair.thy Tue Jul 02 22:46:23 2002 +0200
@@ -9,20 +9,33 @@
W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
1966.
+
+Many proofs are borrowed from pair.thy and sum.thy
+
+Do we EVER have rank(a) < rank(<a;b>) ? Perhaps if the latter rank
+ is not a limit ordinal?
*)
-QPair = Sum + mono +
+theory QPair = Sum + mono:
+
+constdefs
+ QPair :: "[i, i] => i" ("<(_;/ _)>")
+ "<a;b> == a+b"
-consts
- QPair :: "[i, i] => i" ("<(_;/ _)>")
- qfst,qsnd :: "i => i"
+ qfst :: "i => i"
+ "qfst(p) == THE a. EX b. p=<a;b>"
+
+ qsnd :: "i => i"
+ "qsnd(p) == THE b. EX a. p=<a;b>"
+
qsplit :: "[[i, i] => 'a, i] => 'a::logic" (*for pattern-matching*)
- qconverse :: "i => i"
- QSigma :: "[i, i => i] => i"
+ "qsplit(c,p) == c(qfst(p), qsnd(p))"
- "<+>" :: "[i,i]=>i" (infixr 65)
- QInl,QInr :: "i=>i"
- qcase :: "[i=>i, i=>i, i]=>i"
+ qconverse :: "i => i"
+ "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
+
+ QSigma :: "[i, i => i] => i"
+ "QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}"
syntax
"@QSUM" :: "[idt, i, i] => i" ("(3QSUM _:_./ _)" 10)
@@ -32,23 +45,356 @@
"QSUM x:A. B" => "QSigma(A, %x. B)"
"A <*> B" => "QSigma(A, _K(B))"
+constdefs
+ qsum :: "[i,i]=>i" (infixr "<+>" 65)
+ "A <+> B == ({0} <*> A) Un ({1} <*> B)"
-defs
- QPair_def "<a;b> == a+b"
- qfst_def "qfst(p) == THE a. EX b. p=<a;b>"
- qsnd_def "qsnd(p) == THE b. EX a. p=<a;b>"
- qsplit_def "qsplit(c,p) == c(qfst(p), qsnd(p))"
+ QInl :: "i=>i"
+ "QInl(a) == <0;a>"
+
+ QInr :: "i=>i"
+ "QInr(b) == <1;b>"
+
+ qcase :: "[i=>i, i=>i, i]=>i"
+ "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))"
+
+
+print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
+
+
+(**** Quine ordered pairing ****)
+
+(** Lemmas for showing that <a;b> uniquely determines a and b **)
+
+lemma QPair_empty [simp]: "<0;0> = 0"
+by (simp add: QPair_def)
+
+lemma QPair_iff [simp]: "<a;b> = <c;d> <-> a=c & b=d"
+apply (simp add: QPair_def)
+apply (rule sum_equal_iff)
+done
+
+lemmas QPair_inject = QPair_iff [THEN iffD1, THEN conjE, standard, elim!]
+
+lemma QPair_inject1: "<a;b> = <c;d> ==> a=c"
+by blast
+
+lemma QPair_inject2: "<a;b> = <c;d> ==> b=d"
+by blast
+
+
+(*** QSigma: Disjoint union of a family of sets
+ Generalizes Cartesian product ***)
+
+lemma QSigmaI [intro!]: "[| a:A; b:B(a) |] ==> <a;b> : QSigma(A,B)"
+by (simp add: QSigma_def)
+
+
+(*The general elimination rule*)
+lemma QSigmaE:
+ "[| c: QSigma(A,B);
+ !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P
+ |] ==> P"
+apply (simp add: QSigma_def, blast)
+done
+
+(** Elimination rules for <a;b>:A*B -- introducing no eigenvariables **)
+
+lemma QSigmaE [elim!]:
+ "[| c: QSigma(A,B);
+ !!x y.[| x:A; y:B(x); c=<x;y> |] ==> P
+ |] ==> P"
+apply (simp add: QSigma_def, blast)
+done
+
+lemma QSigmaE2 [elim!]:
+ "[| <a;b>: QSigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P"
+by (simp add: QSigma_def)
+
+lemma QSigmaD1: "<a;b> : QSigma(A,B) ==> a : A"
+by blast
+
+lemma QSigmaD2: "<a;b> : QSigma(A,B) ==> b : B(a)"
+by blast
+
+lemma QSigma_cong:
+ "[| A=A'; !!x. x:A' ==> B(x)=B'(x) |] ==>
+ QSigma(A,B) = QSigma(A',B')"
+by (simp add: QSigma_def)
+
+lemma QSigma_empty1 [simp]: "QSigma(0,B) = 0"
+by blast
+
+lemma QSigma_empty2 [simp]: "A <*> 0 = 0"
+by blast
+
+
+(*** Projections: qfst, qsnd ***)
+
+lemma qfst_conv [simp]: "qfst(<a;b>) = a"
+by (simp add: qfst_def, blast)
+
+lemma qsnd_conv [simp]: "qsnd(<a;b>) = b"
+by (simp add: qsnd_def, blast)
+
+lemma qfst_type [TC]: "p:QSigma(A,B) ==> qfst(p) : A"
+by auto
+
+lemma qsnd_type [TC]: "p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
+by auto
+
+lemma QPair_qfst_qsnd_eq: "a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a"
+by auto
+
+
+(*** Eliminator - qsplit ***)
+
+(*A META-equality, so that it applies to higher types as well...*)
+lemma qsplit [simp]: "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
+by (simp add: qsplit_def)
+
+
+lemma qsplit_type [elim!]:
+ "[| p:QSigma(A,B);
+ !!x y.[| x:A; y:B(x) |] ==> c(x,y):C(<x;y>)
+ |] ==> qsplit(%x y. c(x,y), p) : C(p)"
+by auto
+
+lemma expand_qsplit:
+ "u: A<*>B ==> R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))"
+apply (simp add: qsplit_def, auto)
+done
+
+
+(*** qsplit for predicates: result type o ***)
+
+lemma qsplitI: "R(a,b) ==> qsplit(R, <a;b>)"
+by (simp add: qsplit_def)
+
+
+lemma qsplitE:
+ "[| qsplit(R,z); z:QSigma(A,B);
+ !!x y. [| z = <x;y>; R(x,y) |] ==> P
+ |] ==> P"
+apply (simp add: qsplit_def, auto)
+done
+
+lemma qsplitD: "qsplit(R,<a;b>) ==> R(a,b)"
+by (simp add: qsplit_def)
+
+
+(*** qconverse ***)
+
+lemma qconverseI [intro!]: "<a;b>:r ==> <b;a>:qconverse(r)"
+by (simp add: qconverse_def, blast)
+
+lemma qconverseD [elim!]: "<a;b> : qconverse(r) ==> <b;a> : r"
+by (simp add: qconverse_def, blast)
+
+lemma qconverseE [elim!]:
+ "[| yx : qconverse(r);
+ !!x y. [| yx=<y;x>; <x;y>:r |] ==> P
+ |] ==> P"
+apply (simp add: qconverse_def, blast)
+done
+
+lemma qconverse_qconverse: "r<=QSigma(A,B) ==> qconverse(qconverse(r)) = r"
+by blast
+
+lemma qconverse_type: "r <= A <*> B ==> qconverse(r) <= B <*> A"
+by blast
+
+lemma qconverse_prod: "qconverse(A <*> B) = B <*> A"
+by blast
+
+lemma qconverse_empty: "qconverse(0) = 0"
+by blast
+
+
+(**** The Quine-inspired notion of disjoint sum ****)
+
+lemmas qsum_defs = qsum_def QInl_def QInr_def qcase_def
+
+(** Introduction rules for the injections **)
+
+lemma QInlI [intro!]: "a : A ==> QInl(a) : A <+> B"
+by (simp add: qsum_defs, blast)
- qconverse_def "qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}"
- QSigma_def "QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>}"
+lemma QInrI [intro!]: "b : B ==> QInr(b) : A <+> B"
+by (simp add: qsum_defs, blast)
+
+(** Elimination rules **)
+
+lemma qsumE [elim!]:
+ "[| u: A <+> B;
+ !!x. [| x:A; u=QInl(x) |] ==> P;
+ !!y. [| y:B; u=QInr(y) |] ==> P
+ |] ==> P"
+apply (simp add: qsum_defs, blast)
+done
+
+
+(** Injection and freeness equivalences, for rewriting **)
+
+lemma QInl_iff [iff]: "QInl(a)=QInl(b) <-> a=b"
+by (simp add: qsum_defs )
+
+lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
+by (simp add: qsum_defs )
+
+lemma QInl_QInr_iff [iff]: "QInl(a)=QInr(b) <-> False"
+by (simp add: qsum_defs )
+
+lemma QInr_QInl_iff [iff]: "QInr(b)=QInl(a) <-> False"
+by (simp add: qsum_defs )
+
+lemma qsum_empty [simp]: "0<+>0 = 0"
+by (simp add: qsum_defs )
+
+(*Injection and freeness rules*)
+
+lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
+lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
+lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE]
+lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE]
+
+lemma QInlD: "QInl(a): A<+>B ==> a: A"
+by blast
+
+lemma QInrD: "QInr(b): A<+>B ==> b: B"
+by blast
+
+(** <+> is itself injective... who cares?? **)
+
+lemma qsum_iff:
+ "u: A <+> B <-> (EX x. x:A & u=QInl(x)) | (EX y. y:B & u=QInr(y))"
+apply blast
+done
+
+lemma qsum_subset_iff: "A <+> B <= C <+> D <-> A<=C & B<=D"
+by blast
+
+lemma qsum_equal_iff: "A <+> B = C <+> D <-> A=C & B=D"
+apply (simp (no_asm) add: extension qsum_subset_iff)
+apply blast
+done
+
+(*** Eliminator -- qcase ***)
+
+lemma qcase_QInl [simp]: "qcase(c, d, QInl(a)) = c(a)"
+by (simp add: qsum_defs )
+
+
+lemma qcase_QInr [simp]: "qcase(c, d, QInr(b)) = d(b)"
+by (simp add: qsum_defs )
+
+lemma qcase_type:
+ "[| u: A <+> B;
+ !!x. x: A ==> c(x): C(QInl(x));
+ !!y. y: B ==> d(y): C(QInr(y))
+ |] ==> qcase(c,d,u) : C(u)"
+apply (simp add: qsum_defs , auto)
+done
+
+(** Rules for the Part primitive **)
+
+lemma Part_QInl: "Part(A <+> B,QInl) = {QInl(x). x: A}"
+by blast
+
+lemma Part_QInr: "Part(A <+> B,QInr) = {QInr(y). y: B}"
+by blast
+
+lemma Part_QInr2: "Part(A <+> B, %x. QInr(h(x))) = {QInr(y). y: Part(B,h)}"
+by blast
- qsum_def "A <+> B == ({0} <*> A) Un ({1} <*> B)"
- QInl_def "QInl(a) == <0;a>"
- QInr_def "QInr(b) == <1;b>"
- qcase_def "qcase(c,d) == qsplit(%y z. cond(y, d(z), c(z)))"
+lemma Part_qsum_equality: "C <= A <+> B ==> Part(C,QInl) Un Part(C,QInr) = C"
+by blast
+
+
+(*** Monotonicity ***)
+
+lemma QPair_mono: "[| a<=c; b<=d |] ==> <a;b> <= <c;d>"
+by (simp add: QPair_def sum_mono)
+
+lemma QSigma_mono [rule_format]:
+ "[| A<=C; ALL x:A. B(x) <= D(x) |] ==> QSigma(A,B) <= QSigma(C,D)"
+by blast
+
+lemma QInl_mono: "a<=b ==> QInl(a) <= QInl(b)"
+by (simp add: QInl_def subset_refl [THEN QPair_mono])
+
+lemma QInr_mono: "a<=b ==> QInr(a) <= QInr(b)"
+by (simp add: QInr_def subset_refl [THEN QPair_mono])
+
+lemma qsum_mono: "[| A<=C; B<=D |] ==> A <+> B <= C <+> D"
+by blast
+
+ML
+{*
+val qsum_defs = thms "qsum_defs";
+
+val QPair_empty = thm "QPair_empty";
+val QPair_iff = thm "QPair_iff";
+val QPair_inject = thm "QPair_inject";
+val QPair_inject1 = thm "QPair_inject1";
+val QPair_inject2 = thm "QPair_inject2";
+val QSigmaI = thm "QSigmaI";
+val QSigmaE = thm "QSigmaE";
+val QSigmaE = thm "QSigmaE";
+val QSigmaE2 = thm "QSigmaE2";
+val QSigmaD1 = thm "QSigmaD1";
+val QSigmaD2 = thm "QSigmaD2";
+val QSigma_cong = thm "QSigma_cong";
+val QSigma_empty1 = thm "QSigma_empty1";
+val QSigma_empty2 = thm "QSigma_empty2";
+val qfst_conv = thm "qfst_conv";
+val qsnd_conv = thm "qsnd_conv";
+val qfst_type = thm "qfst_type";
+val qsnd_type = thm "qsnd_type";
+val QPair_qfst_qsnd_eq = thm "QPair_qfst_qsnd_eq";
+val qsplit = thm "qsplit";
+val qsplit_type = thm "qsplit_type";
+val expand_qsplit = thm "expand_qsplit";
+val qsplitI = thm "qsplitI";
+val qsplitE = thm "qsplitE";
+val qsplitD = thm "qsplitD";
+val qconverseI = thm "qconverseI";
+val qconverseD = thm "qconverseD";
+val qconverseE = thm "qconverseE";
+val qconverse_qconverse = thm "qconverse_qconverse";
+val qconverse_type = thm "qconverse_type";
+val qconverse_prod = thm "qconverse_prod";
+val qconverse_empty = thm "qconverse_empty";
+val QInlI = thm "QInlI";
+val QInrI = thm "QInrI";
+val qsumE = thm "qsumE";
+val QInl_iff = thm "QInl_iff";
+val QInr_iff = thm "QInr_iff";
+val QInl_QInr_iff = thm "QInl_QInr_iff";
+val QInr_QInl_iff = thm "QInr_QInl_iff";
+val qsum_empty = thm "qsum_empty";
+val QInl_inject = thm "QInl_inject";
+val QInr_inject = thm "QInr_inject";
+val QInl_neq_QInr = thm "QInl_neq_QInr";
+val QInr_neq_QInl = thm "QInr_neq_QInl";
+val QInlD = thm "QInlD";
+val QInrD = thm "QInrD";
+val qsum_iff = thm "qsum_iff";
+val qsum_subset_iff = thm "qsum_subset_iff";
+val qsum_equal_iff = thm "qsum_equal_iff";
+val qcase_QInl = thm "qcase_QInl";
+val qcase_QInr = thm "qcase_QInr";
+val qcase_type = thm "qcase_type";
+val Part_QInl = thm "Part_QInl";
+val Part_QInr = thm "Part_QInr";
+val Part_QInr2 = thm "Part_QInr2";
+val Part_qsum_equality = thm "Part_qsum_equality";
+val QPair_mono = thm "QPair_mono";
+val QSigma_mono = thm "QSigma_mono";
+val QInl_mono = thm "QInl_mono";
+val QInr_mono = thm "QInr_mono";
+val qsum_mono = thm "qsum_mono";
+*}
+
end
-ML
-
-val print_translation =
- [("QSigma", dependent_tr' ("@QSUM", "op <*>"))];
--- a/src/ZF/QUniv.thy Tue Jul 02 17:44:13 2002 +0200
+++ b/src/ZF/QUniv.thy Tue Jul 02 22:46:23 2002 +0200
@@ -3,25 +3,242 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-A small universe for lazy recursive types.
+A small universe for lazy recursive types
*)
-QUniv = Univ + QPair + mono + equalities +
+(** Properties involving Transset and Sum **)
+
+theory QUniv = Univ + QPair + mono + equalities:
(*Disjoint sums as a datatype*)
rep_datatype
- elim sumE
- induct TrueI
- case_eqns case_Inl, case_Inr
+ elimination sumE
+ induction TrueI
+ case_eqns case_Inl case_Inr
(*Variant disjoint sums as a datatype*)
rep_datatype
- elim qsumE
- induct TrueI
- case_eqns qcase_QInl, qcase_QInr
+ elimination qsumE
+ induction TrueI
+ case_eqns qcase_QInl qcase_QInr
constdefs
quniv :: "i => i"
"quniv(A) == Pow(univ(eclose(A)))"
+
+lemma Transset_includes_summands:
+ "[| Transset(C); A+B <= C |] ==> A <= C & B <= C"
+apply (simp add: sum_def Un_subset_iff)
+apply (blast dest: Transset_includes_range)
+done
+
+lemma Transset_sum_Int_subset:
+ "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"
+apply (simp add: sum_def Int_Un_distrib2)
+apply (blast dest: Transset_Pair_D)
+done
+
+(** Introduction and elimination rules avoid tiresome folding/unfolding **)
+
+lemma qunivI: "X <= univ(eclose(A)) ==> X : quniv(A)"
+by (simp add: quniv_def)
+
+lemma qunivD: "X : quniv(A) ==> X <= univ(eclose(A))"
+by (simp add: quniv_def)
+
+lemma quniv_mono: "A<=B ==> quniv(A) <= quniv(B)"
+apply (unfold quniv_def)
+apply (erule eclose_mono [THEN univ_mono, THEN Pow_mono])
+done
+
+(*** Closure properties ***)
+
+lemma univ_eclose_subset_quniv: "univ(eclose(A)) <= quniv(A)"
+apply (simp add: quniv_def Transset_iff_Pow [symmetric])
+apply (rule Transset_eclose [THEN Transset_univ])
+done
+
+(*Key property for proving A_subset_quniv; requires eclose in def of quniv*)
+lemma univ_subset_quniv: "univ(A) <= quniv(A)"
+apply (rule arg_subset_eclose [THEN univ_mono, THEN subset_trans])
+apply (rule univ_eclose_subset_quniv)
+done
+
+lemmas univ_into_quniv = univ_subset_quniv [THEN subsetD, standard]
+
+lemma Pow_univ_subset_quniv: "Pow(univ(A)) <= quniv(A)"
+apply (unfold quniv_def)
+apply (rule arg_subset_eclose [THEN univ_mono, THEN Pow_mono])
+done
+
+lemmas univ_subset_into_quniv =
+ PowI [THEN Pow_univ_subset_quniv [THEN subsetD], standard]
+
+lemmas zero_in_quniv = zero_in_univ [THEN univ_into_quniv, standard]
+lemmas one_in_quniv = one_in_univ [THEN univ_into_quniv, standard]
+lemmas two_in_quniv = two_in_univ [THEN univ_into_quniv, standard]
+
+lemmas A_subset_quniv = subset_trans [OF A_subset_univ univ_subset_quniv]
+
+lemmas A_into_quniv = A_subset_quniv [THEN subsetD, standard]
+
+(*** univ(A) closure for Quine-inspired pairs and injections ***)
+
+(*Quine ordered pairs*)
+lemma QPair_subset_univ:
+ "[| a <= univ(A); b <= univ(A) |] ==> <a;b> <= univ(A)"
+by (simp add: QPair_def sum_subset_univ)
+
+(** Quine disjoint sum **)
+
+lemma QInl_subset_univ: "a <= univ(A) ==> QInl(a) <= univ(A)"
+apply (unfold QInl_def)
+apply (erule empty_subsetI [THEN QPair_subset_univ])
+done
+
+lemmas naturals_subset_nat =
+ Ord_nat [THEN Ord_is_Transset, unfolded Transset_def, THEN bspec, standard]
+
+lemmas naturals_subset_univ =
+ subset_trans [OF naturals_subset_nat nat_subset_univ]
+
+lemma QInr_subset_univ: "a <= univ(A) ==> QInr(a) <= univ(A)"
+apply (unfold QInr_def)
+apply (erule nat_1I [THEN naturals_subset_univ, THEN QPair_subset_univ])
+done
+
+(*** Closure for Quine-inspired products and sums ***)
+
+(*Quine ordered pairs*)
+lemma QPair_in_quniv:
+ "[| a: quniv(A); b: quniv(A) |] ==> <a;b> : quniv(A)"
+by (simp add: quniv_def QPair_def sum_subset_univ)
+
+lemma QSigma_quniv: "quniv(A) <*> quniv(A) <= quniv(A)"
+by (blast intro: QPair_in_quniv)
+
+lemmas QSigma_subset_quniv = subset_trans [OF QSigma_mono QSigma_quniv]
+
+(*The opposite inclusion*)
+lemma quniv_QPair_D:
+ "<a;b> : quniv(A) ==> a: quniv(A) & b: quniv(A)"
+apply (unfold quniv_def QPair_def)
+apply (rule Transset_includes_summands [THEN conjE])
+apply (rule Transset_eclose [THEN Transset_univ])
+apply (erule PowD, blast)
+done
+
+lemmas quniv_QPair_E = quniv_QPair_D [THEN conjE, standard]
+
+lemma quniv_QPair_iff: "<a;b> : quniv(A) <-> a: quniv(A) & b: quniv(A)"
+by (blast intro: QPair_in_quniv dest: quniv_QPair_D)
+
+
+(** Quine disjoint sum **)
+
+lemma QInl_in_quniv: "a: quniv(A) ==> QInl(a) : quniv(A)"
+by (simp add: QInl_def zero_in_quniv QPair_in_quniv)
+
+lemma QInr_in_quniv: "b: quniv(A) ==> QInr(b) : quniv(A)"
+by (simp add: QInr_def one_in_quniv QPair_in_quniv)
+
+lemma qsum_quniv: "quniv(C) <+> quniv(C) <= quniv(C)"
+by (blast intro: QInl_in_quniv QInr_in_quniv)
+
+lemmas qsum_subset_quniv = subset_trans [OF qsum_mono qsum_quniv]
+
+
+(*** The natural numbers ***)
+
+lemmas nat_subset_quniv = subset_trans [OF nat_subset_univ univ_subset_quniv]
+
+(* n:nat ==> n:quniv(A) *)
+lemmas nat_into_quniv = nat_subset_quniv [THEN subsetD, standard]
+
+lemmas bool_subset_quniv = subset_trans [OF bool_subset_univ univ_subset_quniv]
+
+lemmas bool_into_quniv = bool_subset_quniv [THEN subsetD, standard]
+
+
+(*** Intersecting <a;b> with Vfrom... ***)
+
+lemma QPair_Int_Vfrom_succ_subset:
+ "Transset(X) ==>
+ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"
+by (simp add: QPair_def sum_def Int_Un_distrib2 Un_mono
+ product_Int_Vfrom_subset [THEN subset_trans]
+ Sigma_mono [OF Int_lower1 subset_refl])
+
+(**** "Take-lemma" rules for proving a=b by coinduction and c: quniv(A) ****)
+
+(*Rule for level i -- preserving the level, not decreasing it*)
+
+lemma QPair_Int_Vfrom_subset:
+ "Transset(X) ==>
+ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>"
+apply (unfold QPair_def)
+apply (erule Transset_Vfrom [THEN Transset_sum_Int_subset])
+done
+
+(*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> <a;b> Int Vset(i) <= <c;d>*)
+lemmas QPair_Int_Vset_subset_trans =
+ subset_trans [OF Transset_0 [THEN QPair_Int_Vfrom_subset] QPair_mono]
+
+lemma QPair_Int_Vset_subset_UN:
+ "Ord(i) ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)"
+apply (erule Ord_cases)
+(*0 case*)
+apply (simp add: Vfrom_0)
+(*succ(j) case*)
+apply (erule ssubst)
+apply (rule Transset_0 [THEN QPair_Int_Vfrom_succ_subset, THEN subset_trans])
+apply (rule succI1 [THEN UN_upper])
+(*Limit(i) case*)
+apply (simp del: UN_simps
+ add: Limit_Vfrom_eq Int_UN_distrib UN_mono QPair_Int_Vset_subset_trans)
+done
+
+ML
+{*
+val Transset_includes_summands = thm "Transset_includes_summands";
+val Transset_sum_Int_subset = thm "Transset_sum_Int_subset";
+val qunivI = thm "qunivI";
+val qunivD = thm "qunivD";
+val quniv_mono = thm "quniv_mono";
+val univ_eclose_subset_quniv = thm "univ_eclose_subset_quniv";
+val univ_subset_quniv = thm "univ_subset_quniv";
+val univ_into_quniv = thm "univ_into_quniv";
+val Pow_univ_subset_quniv = thm "Pow_univ_subset_quniv";
+val univ_subset_into_quniv = thm "univ_subset_into_quniv";
+val zero_in_quniv = thm "zero_in_quniv";
+val one_in_quniv = thm "one_in_quniv";
+val two_in_quniv = thm "two_in_quniv";
+val A_subset_quniv = thm "A_subset_quniv";
+val A_into_quniv = thm "A_into_quniv";
+val QPair_subset_univ = thm "QPair_subset_univ";
+val QInl_subset_univ = thm "QInl_subset_univ";
+val naturals_subset_nat = thm "naturals_subset_nat";
+val naturals_subset_univ = thm "naturals_subset_univ";
+val QInr_subset_univ = thm "QInr_subset_univ";
+val QPair_in_quniv = thm "QPair_in_quniv";
+val QSigma_quniv = thm "QSigma_quniv";
+val QSigma_subset_quniv = thm "QSigma_subset_quniv";
+val quniv_QPair_D = thm "quniv_QPair_D";
+val quniv_QPair_E = thm "quniv_QPair_E";
+val quniv_QPair_iff = thm "quniv_QPair_iff";
+val QInl_in_quniv = thm "QInl_in_quniv";
+val QInr_in_quniv = thm "QInr_in_quniv";
+val qsum_quniv = thm "qsum_quniv";
+val qsum_subset_quniv = thm "qsum_subset_quniv";
+val nat_subset_quniv = thm "nat_subset_quniv";
+val nat_into_quniv = thm "nat_into_quniv";
+val bool_subset_quniv = thm "bool_subset_quniv";
+val bool_into_quniv = thm "bool_into_quniv";
+val QPair_Int_Vfrom_succ_subset = thm "QPair_Int_Vfrom_succ_subset";
+val QPair_Int_Vfrom_subset = thm "QPair_Int_Vfrom_subset";
+val QPair_Int_Vset_subset_trans = thm "QPair_Int_Vset_subset_trans";
+val QPair_Int_Vset_subset_UN = thm "QPair_Int_Vset_subset_UN";
+*}
+
end