# HG changeset patch # User lcp # Date 772208794 -7200 # Node ID 89d45187f04dbddcb46f4a6650af7e137e0e5dd5 # Parent 1e4f420523ae1fd299f0767c32184698d8c4f891 Various updates and tidying diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/Acc.ML --- a/src/ZF/ex/Acc.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/Acc.ML Tue Jun 21 16:26:34 1994 +0200 @@ -18,37 +18,34 @@ val type_intrs = [] val type_elims = []); +(*The introduction rule must require a:field(r) + Otherwise acc(r) would be a proper class! *) + goal Acc.thy "!!a b r. [| b: acc(r); : r |] ==> a: acc(r)"; by (etac Acc.elim 1); by (fast_tac ZF_cs 1); val acc_downward = result(); -val [major] = goal Acc.thy "field(r) <= acc(r) ==> wf(r)"; -by (rtac (major RS wfI2) 1); -by (rtac subsetI 1); -by (etac Acc.induct 1); -by (etac (bspec RS mp) 1); +val [major,indhyp] = goal Acc.thy + "[| a : acc(r); \ +\ !!x. [| x: acc(r); ALL y. :r --> P(y) |] ==> P(x) \ +\ |] ==> P(a)"; +br (major RS Acc.induct) 1; +br indhyp 1; +by (fast_tac ZF_cs 2); by (resolve_tac Acc.intrs 1); -by (assume_tac 2); -by (ALLGOALS (fast_tac ZF_cs)); -val acc_wfI = result(); - -goal ZF.thy "!!r A. field(r Int A*A) <= field(r) Int A"; +ba 2; by (fast_tac ZF_cs 1); -val field_Int_prodself = result(); +val acc_induct = result(); -goal Acc.thy "wf(r Int (acc(r)*acc(r)))"; -by (rtac (field_Int_prodself RS wfI2) 1); -by (rtac subsetI 1); -by (etac IntE 1); -by (etac Acc.induct 1); -by (etac (bspec RS mp) 1); -by (rtac IntI 1); -by (assume_tac 1); -by (resolve_tac Acc.intrs 1); -by (assume_tac 2); -by (ALLGOALS (fast_tac ZF_cs)); -val wf_acc_Int = result(); +goal Acc.thy "wf[acc(r)](r)"; +br wf_onI2 1; +be acc_induct 1; +by (fast_tac ZF_cs 1); +val wf_on_acc = result(); + +(* field(r) <= acc(r) ==> wf(r) *) +val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf; val [major] = goal Acc.thy "wf(r) ==> field(r) <= acc(r)"; by (rtac subsetI 1); diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/Bin.ML --- a/src/ZF/ex/Bin.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/Bin.ML Tue Jun 21 16:26:34 1994 +0200 @@ -14,7 +14,8 @@ [(["Plus", "Minus"], "i"), (["op $$"], "[i,i]=>i")])]; val rec_styp = "i"; - val ext = Some (Syntax.simple_sext [OldMixfix.Infixl("$$", "[i,i] => i", 60)]); + val ext = Some (Syntax.simple_sext + [OldMixfix.Infixl("$$", "[i,i] => i", 60)]); val sintrs = ["Plus : bin", "Minus : bin", diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/Comb.ML --- a/src/ZF/ex/Comb.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/Comb.ML Tue Jun 21 16:26:34 1994 +0200 @@ -19,7 +19,8 @@ [(["K","S"], "i"), (["op #"], "[i,i]=>i")])]; val rec_styp = "i"; - val ext = Some (Syntax.simple_sext [OldMixfix.Infixl("#", "[i,i] => i", 90)]); + val ext = Some (Syntax.simple_sext + [OldMixfix.Infixl("#", "[i,i] => i", 90)]); val sintrs = ["K : comb", "S : comb", diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/Equiv.ML --- a/src/ZF/ex/Equiv.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/Equiv.ML Tue Jun 21 16:26:34 1994 +0200 @@ -1,9 +1,9 @@ -(* Title: ZF/ex/equiv.ML +(* Title: ZF/ex/Equiv.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge + Copyright 1994 University of Cambridge -For equiv.thy. Equivalence relations in Zermelo-Fraenkel Set Theory +For Equiv.thy. Equivalence relations in Zermelo-Fraenkel Set Theory *) val RSLIST = curry (op MRS); @@ -20,7 +20,7 @@ val sym_trans_comp_subset = result(); goalw Equiv.thy [refl_def] - "!!A r. refl(A,r) ==> r <= converse(r) O r"; + "!!A r. [| refl(A,r); r <= A*A |] ==> r <= converse(r) O r"; by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 1); val refl_comp_subset = result(); @@ -80,9 +80,8 @@ by (fast_tac ZF_cs 1); val equiv_class_nondisjoint = result(); -val [major] = goalw Equiv.thy [equiv_def,refl_def] - "equiv(A,r) ==> r <= A*A"; -by (rtac (major RS conjunct1 RS conjunct1) 1); +goalw Equiv.thy [equiv_def] "!!A r. equiv(A,r) ==> r <= A*A"; +by (safe_tac ZF_cs); val equiv_type = result(); goal Equiv.thy @@ -137,9 +136,9 @@ val prems as [equivA,bcong,_] = goal Equiv.thy "[| equiv(A,r); congruent(r,b); a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"; by (cut_facts_tac prems 1); -by (rtac UN_singleton 1); -by (etac equiv_class_self 1); -by (assume_tac 1); +by (rtac ([refl RS UN_cong, UN_constant] MRS trans) 1); +by (etac equiv_class_self 2); +by (assume_tac 2); by (rewrite_goals_tac [equiv_def,sym_def,congruent_def]); by (fast_tac ZF_cs 1); val UN_equiv_class = result(); diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/Equiv.thy --- a/src/ZF/ex/Equiv.thy Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/Equiv.thy Tue Jun 21 16:26:34 1994 +0200 @@ -1,23 +1,18 @@ -(* Title: ZF/ex/equiv.thy +(* Title: ZF/ex/Equiv.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge + Copyright 1994 University of Cambridge Equivalence relations in Zermelo-Fraenkel Set Theory *) -Equiv = Trancl + +Equiv = Rel + Perm + consts - refl,equiv :: "[i,i]=>o" - sym :: "i=>o" "'/" :: "[i,i]=>i" (infixl 90) (*set of equiv classes*) congruent :: "[i,i=>i]=>o" congruent2 :: "[i,[i,i]=>i]=>o" rules - refl_def "refl(A,r) == r <= (A*A) & (ALL x: A. : r)" - sym_def "sym(r) == ALL x y. : r --> : r" - equiv_def "equiv(A,r) == refl(A,r) & sym(r) & trans(r)" quotient_def "A/r == {r``{x} . x:A}" congruent_def "congruent(r,b) == ALL y z. :r --> b(y)=b(z)" diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/LList.ML --- a/src/ZF/ex/LList.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/LList.ML Tue Jun 21 16:26:34 1994 +0200 @@ -28,6 +28,15 @@ val LCons_iff = LList.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'"; val LNil_LCons_iff = LList.mk_free "~ LNil=LCons(a,l)"; +goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))"; +by (rtac (LList.unfold RS trans) 1); +bws LList.con_defs; +by (fast_tac (qsum_cs addIs ([equalityI] @ codatatype_intrs) + addDs [LList.dom_subset RS subsetD] + addEs [A_into_quniv] + addSEs [QSigmaE]) 1); +val llist_unfold = result(); + (*** Lemmas to justify using "llist" in other recursive type definitions ***) goalw LList.thy LList.defs "!!A B. A<=B ==> llist(A) <= llist(B)"; diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/ParContract.ML --- a/src/ZF/ex/ParContract.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/ParContract.ML Tue Jun 21 16:26:34 1994 +0200 @@ -22,7 +22,8 @@ val type_intrs = Comb.intrs@[SigmaI]; val type_elims = [SigmaE2]); -val [parcontract_refl,K_parcontract,S_parcontract,Ap_parcontract] = ParContract.intrs; +val [parcontract_refl,K_parcontract,S_parcontract,Ap_parcontract] = + ParContract.intrs; val parcontract_induct = standard (ParContract.mutual_induct RS spec RS spec RSN (2,rev_mp)); diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/Primrec0.ML --- a/src/ZF/ex/Primrec0.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/Primrec0.ML Tue Jun 21 16:26:34 1994 +0200 @@ -92,7 +92,7 @@ val ack_typechecks = [ACK_in_primrec, primrec_into_fun RS apply_type, - add_type, list_add_type, naturals_are_ordinals] @ + add_type, list_add_type, nat_into_Ord] @ nat_typechecks @ List.intrs @ Primrec.intrs; (*strict typechecking for the Ackermann proof; instantiates no vars*) @@ -127,7 +127,7 @@ val ack_ss = pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ, - ack_type, naturals_are_ordinals]; + ack_type, nat_into_Ord]; (*PROPERTY A 4*) goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j < ack(i,j)"; @@ -161,7 +161,7 @@ goal Primrec.thy "!!i j k. [| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)"; by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1); -by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS naturals_are_ordinals] 1)); +by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1)); val ack_le_mono2 = result(); (*PROPERTY A 6*) @@ -194,7 +194,7 @@ goal Primrec.thy "!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)"; by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1); -by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS naturals_are_ordinals] 1)); +by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1)); val ack_le_mono1 = result(); (*PROPERTY A 8*) @@ -247,8 +247,7 @@ (*** MAIN RESULT ***) val ack2_ss = - ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, - naturals_are_ordinals]; + ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, nat_into_Ord]; goalw Primrec.thy [SC_def] "!!l. l: list(nat) ==> SC ` l < ack(1, list_add(l))"; diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/TF.ML --- a/src/ZF/ex/TF.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/TF.ML Tue Jun 21 16:26:34 1994 +0200 @@ -47,19 +47,27 @@ addDs [TF.dom_subset RS subsetD] addSEs ([PartE] @ datatype_elims @ TF.free_SEs); -goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}"; -by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1); +goalw TF.thy (tl TF.defs) + "tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))"; +by (rtac (TF.unfold RS trans) 1); by (rewrite_goals_tac TF.con_defs); by (rtac equalityI 1); by (fast_tac unfold_cs 1); by (fast_tac unfold_cs 1); +val tree_forest_unfold = result(); + +val tree_forest_unfold' = rewrite_rule (tl TF.defs) tree_forest_unfold; + + +goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}"; +br (Part_Inl RS subst) 1; +br (tree_forest_unfold' RS subst_context) 1; val tree_unfold = result(); goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}"; -by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (TF.unfold RS ssubst) 1); -by (rewrite_goals_tac TF.con_defs); -by (rtac equalityI 1); -by (fast_tac unfold_cs 1); -by (fast_tac unfold_cs 1); +br (Part_Inr RS subst) 1; +br (tree_forest_unfold' RS subst_context) 1; val forest_unfold = result(); + + diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/Term.ML --- a/src/ZF/ex/Term.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/Term.ML Tue Jun 21 16:26:34 1994 +0200 @@ -21,6 +21,15 @@ val [ApplyI] = Term.intrs; +(*Note that Apply is the identity function*) +goal Term.thy "term(A) = A * list(term(A))"; +by (rtac (Term.unfold RS trans) 1); +bws Term.con_defs; +by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs) + addDs [Term.dom_subset RS subsetD] + addEs [A_into_univ, list_into_univ]) 1); +val term_unfold = result(); + (*Induction on term(A) followed by induction on List *) val major::prems = goal Term.thy "[| t: term(A); \ @@ -61,6 +70,9 @@ by (REPEAT (ares_tac [Pair_in_univ, list_univ RS subsetD] 1)); val term_univ = result(); -val term_subset_univ = standard - (term_mono RS (term_univ RSN (2,subset_trans))); +val term_subset_univ = + term_mono RS (term_univ RSN (2,subset_trans)) |> standard; +goal Term.thy "!!t A B. [| t: term(A); A <= univ(B) |] ==> t: univ(B)"; +by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1)); +val term_into_univ = result(); diff -r 1e4f420523ae -r 89d45187f04d src/ZF/ex/misc.ML --- a/src/ZF/ex/misc.ML Tue Jun 21 11:55:36 1994 +0200 +++ b/src/ZF/ex/misc.ML Tue Jun 21 16:26:34 1994 +0200 @@ -45,50 +45,6 @@ result(); -(**** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ****) - -val SB_thy = merge_theories (Fixedpt.thy, Perm.thy); - -(** Lemma: Banach's Decomposition Theorem **) - -goal SB_thy "bnd_mono(X, %W. X - g``(Y - f``W))"; -by (rtac bnd_monoI 1); -by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1)); -val decomp_bnd_mono = result(); - -val [gfun] = goal SB_thy - "g: Y->X ==> \ -\ g``(Y - f`` lfp(X, %W. X - g``(Y - f``W))) = \ -\ X - lfp(X, %W. X - g``(Y - f``W)) "; -by (res_inst_tac [("P", "%u. ?v = X-u")] - (decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); -by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, - gfun RS fun_is_rel RS image_subset]) 1); -val Banach_last_equation = result(); - -val prems = goal SB_thy - "[| f: X->Y; g: Y->X |] ==> \ -\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \ -\ (YA Int YB = 0) & (YA Un YB = Y) & \ -\ f``XA=YA & g``YB=XB"; -by (REPEAT - (FIRSTGOAL - (resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition]))); -by (rtac Banach_last_equation 3); -by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1)); -val decomposition = result(); - -val prems = goal SB_thy - "[| f: inj(X,Y); g: inj(Y,X) |] ==> EX h. h: bij(X,Y)"; -by (cut_facts_tac prems 1); -by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1); -by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un] - addIs [bij_converse_bij]) 1); -(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))" - is forced by the context!! *) -val schroeder_bernstein = result(); - - (*** Composition of homomorphisms is a homomorphism ***) (*Given as a challenge problem in @@ -98,9 +54,9 @@ *) (*collecting the relevant lemmas*) -val hom_ss = ZF_ss addsimps [comp_func,comp_func_apply,SigmaI,apply_funtype]; +val hom_ss = ZF_ss addsimps [comp_fun,comp_fun_apply,SigmaI,apply_funtype]; -(*The problem below is proving conditions of rewrites such as comp_func_apply; +(*The problem below is proving conditions of rewrites such as comp_fun_apply; rewriting does not instantiate Vars; we must prove the conditions explicitly.*) fun hom_tac hyps = @@ -166,7 +122,7 @@ [comp_mem_injD1, comp_mem_surjD1, comp_mem_injD2, comp_mem_surjD2]; fun pastre_facts (fact1::fact2::fact3::prems) = - forw_iterate (prems @ [comp_surj, comp_inj, comp_func]) + forw_iterate (prems @ [comp_surj, comp_inj, comp_fun]) pastre_rls [fact1,fact2,fact3] 4; val prems = goalw Perm.thy [bij_def]