# HG changeset patch # User lcp # Date 787597632 -3600 # Node ID 4c8333ab3eaea368cc98acc401c85d76ba6e15d4 # Parent 2f2fbf0a7e4fe93f7aa19edf6a2e2296063daa0c changed useless "qed" calls for lemmas back to uses of "result", and/or used "bind_thm" to declare the real results. diff -r 2f2fbf0a7e4f -r 4c8333ab3eae src/ZF/Cardinal.ML --- a/src/ZF/Cardinal.ML Fri Dec 16 17:46:02 1994 +0100 +++ b/src/ZF/Cardinal.ML Fri Dec 16 18:07:12 1994 +0100 @@ -185,8 +185,7 @@ by (etac (ordermap_bij RS bij_converse_bij) 1); qed "well_ord_cardinal_eqpoll"; -val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll - |> standard; +bind_thm ("Ord_cardinal_eqpoll", well_ord_Memrel RS well_ord_cardinal_eqpoll); goal Cardinal.thy "!!X Y. [| well_ord(X,r); well_ord(Y,s); |X| = |Y| |] ==> X eqpoll Y"; @@ -341,8 +340,9 @@ by (eres_inst_tac [("n","n")] natE 1); by (asm_simp_tac (ZF_ss addsimps [inj_def, succI1 RS Pi_empty2]) 1); by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [inj_succ_succD]) 1); -qed "nat_lepoll_imp_le_lemma"; -val nat_lepoll_imp_le = nat_lepoll_imp_le_lemma RS bspec RS mp |> standard; +val nat_lepoll_imp_le_lemma = result(); + +bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp); goal Cardinal.thy "!!m n. [| m:nat; n: nat |] ==> m eqpoll n <-> m = n"; diff -r 2f2fbf0a7e4f -r 4c8333ab3eae src/ZF/Finite.ML --- a/src/ZF/Finite.ML Fri Dec 16 17:46:02 1994 +0100 +++ b/src/ZF/Finite.ML Fri Dec 16 18:07:12 1994 +0100 @@ -122,7 +122,7 @@ by (asm_simp_tac (Fin_ss addsimps [domain_cons]) 1); qed "FiniteFun_domain_Fin"; -val FiniteFun_apply_type = FiniteFun_is_fun RS apply_type |> standard; +bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type); (*Every subset of a finite function is a finite function.*) goal Finite.thy "!!b A. b: A-||>B ==> ALL z. z<=b --> z: A-||>B"; diff -r 2f2fbf0a7e4f -r 4c8333ab3eae src/ZF/OrderType.ML --- a/src/ZF/OrderType.ML Fri Dec 16 17:46:02 1994 +0100 +++ b/src/ZF/OrderType.ML Fri Dec 16 18:07:12 1994 +0100 @@ -94,10 +94,9 @@ by (assume_tac 1); qed "converse_ordermap_mono"; -val ordermap_surj = - (ordermap_type RS surj_image) |> - rewrite_rule [symmetric ordertype_def] |> - standard; +bind_thm ("ordermap_surj", + rewrite_rule [symmetric ordertype_def] + (ordermap_type RS surj_image)); goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def] "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; diff -r 2f2fbf0a7e4f -r 4c8333ab3eae src/ZF/QUniv.ML --- a/src/ZF/QUniv.ML Fri Dec 16 17:46:02 1994 +0100 +++ b/src/ZF/QUniv.ML Fri Dec 16 18:07:12 1994 +0100 @@ -37,21 +37,21 @@ by (rtac univ_eclose_subset_quniv 1); qed "univ_subset_quniv"; -bind_thm ("univ_into_quniv", (univ_subset_quniv RS subsetD)); +bind_thm ("univ_into_quniv", univ_subset_quniv RS subsetD); goalw QUniv.thy [quniv_def] "Pow(univ(A)) <= quniv(A)"; by (rtac (arg_subset_eclose RS univ_mono RS Pow_mono) 1); qed "Pow_univ_subset_quniv"; -val univ_subset_into_quniv = standard - (PowI RS (Pow_univ_subset_quniv RS subsetD)); +bind_thm ("univ_subset_into_quniv", + PowI RS (Pow_univ_subset_quniv RS subsetD)); -bind_thm ("zero_in_quniv", (zero_in_univ RS univ_into_quniv)); -bind_thm ("one_in_quniv", (one_in_univ RS univ_into_quniv)); -bind_thm ("two_in_quniv", (two_in_univ RS univ_into_quniv)); +bind_thm ("zero_in_quniv", zero_in_univ RS univ_into_quniv); +bind_thm ("one_in_quniv", one_in_univ RS univ_into_quniv); +bind_thm ("two_in_quniv", two_in_univ RS univ_into_quniv); -val A_subset_quniv = standard - ([A_subset_univ, univ_subset_quniv] MRS subset_trans); +bind_thm ("A_subset_quniv", + [A_subset_univ, univ_subset_quniv] MRS subset_trans); val A_into_quniv = A_subset_quniv RS subsetD; @@ -94,8 +94,8 @@ ORELSE eresolve_tac [QSigmaE, ssubst] 1)); qed "QSigma_quniv"; -val QSigma_subset_quniv = standard - (QSigma_mono RS (QSigma_quniv RSN (2,subset_trans))); +bind_thm ("QSigma_subset_quniv", + [QSigma_mono, QSigma_quniv] MRS subset_trans); (*The opposite inclusion*) goalw QUniv.thy [quniv_def,QPair_def] @@ -105,7 +105,7 @@ by (REPEAT (ares_tac [conjI,PowI] 1)); qed "quniv_QPair_D"; -bind_thm ("quniv_QPair_E", (quniv_QPair_D RS conjE)); +bind_thm ("quniv_QPair_E", quniv_QPair_D RS conjE); goal QUniv.thy " : quniv(A) <-> a: quniv(A) & b: quniv(A)"; by (REPEAT (ares_tac [iffI, QPair_in_quniv, quniv_QPair_D] 1 @@ -128,21 +128,21 @@ ORELSE eresolve_tac [qsumE, ssubst] 1)); qed "qsum_quniv"; -val qsum_subset_quniv = standard - (qsum_mono RS (qsum_quniv RSN (2,subset_trans))); +bind_thm ("qsum_subset_quniv", [qsum_mono, qsum_quniv] MRS subset_trans); + (*** The natural numbers ***) -val nat_subset_quniv = standard - ([nat_subset_univ, univ_subset_quniv] MRS subset_trans); +bind_thm ("nat_subset_quniv", + [nat_subset_univ, univ_subset_quniv] MRS subset_trans); (* n:nat ==> n:quniv(A) *) bind_thm ("nat_into_quniv", (nat_subset_quniv RS subsetD)); -val bool_subset_quniv = standard - ([bool_subset_univ, univ_subset_quniv] MRS subset_trans); +bind_thm ("bool_subset_quniv", + [bool_subset_univ, univ_subset_quniv] MRS subset_trans); -bind_thm ("bool_into_quniv", (bool_subset_quniv RS subsetD)); +bind_thm ("bool_into_quniv", bool_subset_quniv RS subsetD); (**** Properties of Vfrom analogous to the "take-lemma" ****) @@ -159,7 +159,7 @@ qed "doubleton_in_Vfrom_D"; (*This weaker version says a, b exist at the same level*) -bind_thm ("Vfrom_doubleton_D", (Transset_Vfrom RS Transset_doubleton_D)); +bind_thm ("Vfrom_doubleton_D", Transset_Vfrom RS Transset_doubleton_D); (** Using only the weaker theorem would prove : Vfrom(X,i) implies a, b : Vfrom(X,i), which is useless for induction. @@ -203,8 +203,8 @@ qed "QPair_Int_Vfrom_subset"; (*[| a Int Vset(i) <= c; b Int Vset(i) <= d |] ==> Int Vset(i) <= *) -val QPair_Int_Vset_subset_trans = standard - ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans); +bind_thm ("QPair_Int_Vset_subset_trans", + [Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] MRS subset_trans); goal QUniv.thy "!!i. [| Ord(i) \ diff -r 2f2fbf0a7e4f -r 4c8333ab3eae src/ZF/ROOT.ML --- a/src/ZF/ROOT.ML Fri Dec 16 17:46:02 1994 +0100 +++ b/src/ZF/ROOT.ML Fri Dec 16 18:07:12 1994 +0100 @@ -30,16 +30,7 @@ (*Add user sections for inductive/datatype definitions*) use "../Pure/section_utils.ML"; -use_thy "Datatype"; -structure ThySyn = ThySynFun - (val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", - "and", "|", "<=", "domains", "intrs", "monos", - "con_defs", "type_intrs", "type_elims"] - and user_sections = [("inductive", inductive_decl ""), - ("coinductive", inductive_decl "Co"), - ("datatype", datatype_decl ""), - ("codatatype", datatype_decl "Co")]); -init_thy_reader (); +use "thy_syntax.ML"; use_thy "InfDatatype"; use_thy "List"; diff -r 2f2fbf0a7e4f -r 4c8333ab3eae src/ZF/Sum.ML --- a/src/ZF/Sum.ML Fri Dec 16 17:46:02 1994 +0100 +++ b/src/ZF/Sum.ML Fri Dec 16 18:07:12 1994 +0100 @@ -165,8 +165,7 @@ by (fast_tac (sum_cs addSIs [equalityI]) 1); qed "Part_Collect"; -val Part_CollectE = - Part_Collect RS equalityD1 RS subsetD RS CollectE |> standard; +bind_thm ("Part_CollectE", Part_Collect RS equalityD1 RS subsetD RS CollectE); goal Sum.thy "Part(A+B,Inl) = {Inl(x). x: A}"; by (fast_tac (sum_cs addIs [equalityI]) 1); diff -r 2f2fbf0a7e4f -r 4c8333ab3eae src/ZF/Univ.ML --- a/src/ZF/Univ.ML Fri Dec 16 17:46:02 1994 +0100 +++ b/src/ZF/Univ.ML Fri Dec 16 18:07:12 1994 +0100 @@ -85,7 +85,7 @@ by (rtac Un_upper1 1); qed "A_subset_Vfrom"; -val A_into_Vfrom = A_subset_Vfrom RS subsetD |> standard; +bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD); goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))"; by (rtac (Vfrom RS ssubst) 1); @@ -244,12 +244,11 @@ ORELSE eresolve_tac [SigmaE, ssubst] 1)); qed "product_VLimit"; -val Sigma_subset_VLimit = - [Sigma_mono, product_VLimit] MRS subset_trans |> standard; +bind_thm ("Sigma_subset_VLimit", + [Sigma_mono, product_VLimit] MRS subset_trans); -val nat_subset_VLimit = - [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans - |> standard; +bind_thm ("nat_subset_VLimit", + [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans); goal Univ.thy "!!i. [| n: nat; Limit(i) |] ==> n : Vfrom(A,i)"; by (REPEAT (ares_tac [nat_subset_VLimit RS subsetD] 1)); @@ -257,7 +256,7 @@ (** Closure under disjoint union **) -val zero_in_VLimit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard; +bind_thm ("zero_in_VLimit", Limit_has_0 RS ltD RS zero_in_Vfrom); goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)"; by (REPEAT (ares_tac [nat_into_VLimit, nat_0I, nat_succI] 1)); @@ -277,8 +276,7 @@ by (fast_tac (sum_cs addSIs [Inl_in_VLimit, Inr_in_VLimit]) 1); qed "sum_VLimit"; -val sum_subset_VLimit = - [sum_mono, sum_VLimit] MRS subset_trans |> standard; +bind_thm ("sum_subset_VLimit", [sum_mono, sum_VLimit] MRS subset_trans); @@ -618,9 +616,92 @@ by (rtac (Limit_nat RS sum_VLimit) 1); qed "sum_univ"; -val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard; +bind_thm ("sum_subset_univ", [sum_mono, sum_univ] MRS subset_trans); (** Closure under binary union -- use Un_least **) (** Closure under Collect -- use (Collect_subset RS subset_trans) **) (** Closure under RepFun -- use RepFun_subset **) + + +(*** Finite Branching Closure Properties ***) + +(** Closure under finite powerset **) + +goal Univ.thy + "!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j Fin(Vfrom(A,i)) <= Vfrom(A,i)"; +by (rtac subsetI 1); +by (dresolve_tac [Fin_Vfrom_lemma] 1); +by (safe_tac ZF_cs); +by (resolve_tac [Vfrom RS ssubst] 1); +by (fast_tac (ZF_cs addSDs [ltD]) 1); +val Fin_VLimit = result(); + +bind_thm ("Fin_subset_VLimit", [Fin_mono, Fin_VLimit] MRS subset_trans); + +goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)"; +by (rtac (Limit_nat RS Fin_VLimit) 1); +val Fin_univ = result(); + +(** Closure under finite powers (functions from a fixed natural number) **) + +goal Univ.thy + "!!i. [| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"; +by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1); +by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, + nat_subset_VLimit, subset_refl] 1)); +val nat_fun_VLimit = result(); + +bind_thm ("nat_fun_subset_VLimit", [Pi_mono, nat_fun_VLimit] MRS subset_trans); + +goalw Univ.thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)"; +by (etac (Limit_nat RSN (2,nat_fun_VLimit)) 1); +val nat_fun_univ = result(); + + +(** Closure under finite function space **) + +(*General but seldom-used version; normally the domain is fixed*) +goal Univ.thy + "!!i. Limit(i) ==> Vfrom(A,i) -||> Vfrom(A,i) <= Vfrom(A,i)"; +by (resolve_tac [FiniteFun.dom_subset RS subset_trans] 1); +by (REPEAT (ares_tac [Fin_subset_VLimit, Sigma_subset_VLimit, subset_refl] 1)); +val FiniteFun_VLimit1 = result(); + +goalw Univ.thy [univ_def] "univ(A) -||> univ(A) <= univ(A)"; +by (rtac (Limit_nat RS FiniteFun_VLimit1) 1); +val FiniteFun_univ1 = result(); + +(*Version for a fixed domain*) +goal Univ.thy + "!!i. [| W <= Vfrom(A,i); Limit(i) |] ==> W -||> Vfrom(A,i) <= Vfrom(A,i)"; +by (eresolve_tac [subset_refl RSN (2, FiniteFun_mono) RS subset_trans] 1); +by (eresolve_tac [FiniteFun_VLimit1] 1); +val FiniteFun_VLimit = result(); + +goalw Univ.thy [univ_def] + "!!W. W <= univ(A) ==> W -||> univ(A) <= univ(A)"; +by (etac (Limit_nat RSN (2, FiniteFun_VLimit)) 1); +val FiniteFun_univ = result(); + +goal Univ.thy + "!!W. [| f: W -||> univ(A); W <= univ(A) |] ==> f : univ(A)"; +by (eresolve_tac [FiniteFun_univ RS subsetD] 1); +by (assume_tac 1); +val FiniteFun_in_univ = result(); + +(*Remove <= from the rule above*) +val FiniteFun_in_univ' = subsetI RSN (2, FiniteFun_in_univ); + + diff -r 2f2fbf0a7e4f -r 4c8333ab3eae src/ZF/Zorn.ML --- a/src/ZF/Zorn.ML Fri Dec 16 17:46:02 1994 +0100 +++ b/src/ZF/Zorn.ML Fri Dec 16 18:07:12 1994 +0100 @@ -63,8 +63,8 @@ (*** Section 3. Some Properties of the Transfinite Construction ***) -val increasing_trans = - TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans)) |> standard; +bind_thm ("increasing_trans", + TFin_is_subset RSN (3, increasingD2 RSN (2,subset_trans))); (*Lemma 1 of section 3.1*) val major::prems = goal Zorn.thy