# HG changeset patch # User paulson # Date 1025642783 -7200 # Node ID 28d1823ce0f2f25aa9c7d21f35cd347e7c49e471 # Parent 20c818c966e6575c3d552bb60c158d6452e6272c conversion of QPair to Isar diff -r 20c818c966e6 -r 28d1823ce0f2 src/ZF/IsaMakefile --- 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 \ diff -r 20c818c966e6 -r 28d1823ce0f2 src/ZF/QPair.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() ? Perhaps if the latter rank - is not a limit ordinal? -*) - -(**** Quine ordered pairing ****) - -(** Lemmas for showing that uniquely determines a and b **) - -Goalw [QPair_def] "<0;0> = 0"; -by (Simp_tac 1); -qed "QPair_empty"; - -Goalw [QPair_def] " = <-> 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=c"; -by (Blast_tac 1) ; -qed "QPair_inject1"; - -Goal " = ==> 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) |] ==> : 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= |] ==> 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 -- 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" "" QSigmaE)); - -AddSEs [QSigmaE2, QSigmaE]; - -Goal " : QSigma(A,B) ==> a : A"; -by (Blast_tac 1) ; -qed "QSigmaD1"; - -Goal " : 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"; -by (Blast_tac 1) ; -qed "qfst_conv"; - -Goalw [qsnd_def] "qsnd() = 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) ==> = 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), ) == 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() \ -\ |] ==> 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 = --> R(c(x,y)))"; -by Auto_tac; -qed "expand_qsplit"; - - -(*** qsplit for predicates: result type o ***) - -Goalw [qsplit_def] "R(a,b) ==> qsplit(R, )"; -by (Asm_simp_tac 1); -qed "qsplitI"; - -val major::sigma::prems = Goalw [qsplit_def] - "[| qsplit(R,z); z:QSigma(A,B); \ -\ !!x y. [| z = ; 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,) ==> R(a,b)"; -by (Asm_full_simp_tac 1); -qed "qsplitD"; - - -(*** qconverse ***) - -Goalw [qconverse_def] ":r ==> :qconverse(r)"; -by (Blast_tac 1) ; -qed "qconverseI"; - -Goalw [qconverse_def] " : qconverse(r) ==> : r"; -by (Blast_tac 1) ; -qed "qconverseD"; - -val [major,minor]= Goalw [qconverse_def] - "[| yx : qconverse(r); \ -\ !!x y. [| yx=; :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 |] ==> <= "; -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"; - - diff -r 20c818c966e6 -r 28d1823ce0f2 src/ZF/QPair.thy --- 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() ? Perhaps if the latter rank + is not a limit ordinal? *) -QPair = Sum + mono + +theory QPair = Sum + mono: + +constdefs + QPair :: "[i, i] => i" ("<(_;/ _)>") + " == a+b" -consts - QPair :: "[i, i] => i" ("<(_;/ _)>") - qfst,qsnd :: "i => i" + qfst :: "i => i" + "qfst(p) == THE a. EX b. p=" + + qsnd :: "i => i" + "qsnd(p) == THE b. EX a. p=" + 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= & z=}" + + QSigma :: "[i, i => i] => i" + "QSigma(A,B) == UN x:A. UN y:B(x). {}" 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" - qfst_def "qfst(p) == THE a. EX b. p=" - qsnd_def "qsnd(p) == THE b. EX a. p=" - 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 uniquely determines a and b **) + +lemma QPair_empty [simp]: "<0;0> = 0" +by (simp add: QPair_def) + +lemma QPair_iff [simp]: " = <-> 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=c" +by blast + +lemma QPair_inject2: " = ==> b=d" +by blast + + +(*** QSigma: Disjoint union of a family of sets + Generalizes Cartesian product ***) + +lemma QSigmaI [intro!]: "[| a:A; b:B(a) |] ==> : 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= |] ==> P + |] ==> P" +apply (simp add: QSigma_def, blast) +done + +(** Elimination rules for :A*B -- introducing no eigenvariables **) + +lemma QSigmaE [elim!]: + "[| c: QSigma(A,B); + !!x y.[| x:A; y:B(x); c= |] ==> P + |] ==> P" +apply (simp add: QSigma_def, blast) +done + +lemma QSigmaE2 [elim!]: + "[| : QSigma(A,B); [| a:A; b:B(a) |] ==> P |] ==> P" +by (simp add: QSigma_def) + +lemma QSigmaD1: " : QSigma(A,B) ==> a : A" +by blast + +lemma QSigmaD2: " : 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" +by (simp add: qfst_def, blast) + +lemma qsnd_conv [simp]: "qsnd() = 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) ==> = 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), ) == 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() + |] ==> 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 = --> R(c(x,y)))" +apply (simp add: qsplit_def, auto) +done + + +(*** qsplit for predicates: result type o ***) + +lemma qsplitI: "R(a,b) ==> qsplit(R, )" +by (simp add: qsplit_def) + + +lemma qsplitE: + "[| qsplit(R,z); z:QSigma(A,B); + !!x y. [| z = ; R(x,y) |] ==> P + |] ==> P" +apply (simp add: qsplit_def, auto) +done + +lemma qsplitD: "qsplit(R,) ==> R(a,b)" +by (simp add: qsplit_def) + + +(*** qconverse ***) + +lemma qconverseI [intro!]: ":r ==> :qconverse(r)" +by (simp add: qconverse_def, blast) + +lemma qconverseD [elim!]: " : qconverse(r) ==> : r" +by (simp add: qconverse_def, blast) + +lemma qconverseE [elim!]: + "[| yx : qconverse(r); + !!x y. [| yx=; :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= & z=}" - QSigma_def "QSigma(A,B) == UN x:A. UN y:B(x). {}" +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 |] ==> <= " +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 <*>"))]; diff -r 20c818c966e6 -r 28d1823ce0f2 src/ZF/QUniv.thy --- 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) |] ==> <= 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) |] ==> : 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: + " : 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: " : 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 with Vfrom... ***) + +lemma QPair_Int_Vfrom_succ_subset: + "Transset(X) ==> + Int Vfrom(X, succ(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) ==> + 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 |] ==> Int Vset(i) <= *) +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) ==> Int Vset(i) <= (UN j:i. )" +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