# HG changeset patch # User lcp # Date 749381198 -3600 # Node ID 6c6d2f6e318590ded5fb0b3606b91fc97d2f627f # Parent 1c0926788772bb93adabd6431ee91782135b8850 ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext domrange/image_subset,vimage_subset: deleted needless premise! misc: This slightly simplifies two proofs in Schroeder-Bernstein Theorem ind-syntax/rule_concl: recoded to avoid exceptions intr-elim: now checks conclusions of introduction rules func/fun_disjoint_Un: now uses ex_ex1I list-fn/hd,tl,drop: new simpdata/bquant_simps: new list/list_case_type: restored! bool.thy: changed 1 from a "def" to a translation Removed occurreces of one_def in bool.ML, nat.ML, univ.ML, ex/integ.ML nat/succ_less_induct: new induction principle arith/add_mono: new results about monotonicity simpdata/mem_simps: removed the ones for succ and cons; added succI1, consI2 to ZF_ss upair/succ_iff: new, for use with simp_tac (cons_iff already existed) ordinal/Ord_0_in_succ: renamed from Ord_0_mem_succ nat/nat_0_in_succ: new ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed diff -r 1c0926788772 -r 6c6d2f6e3185 src/ZF/List.ML --- a/src/ZF/List.ML Thu Sep 30 10:10:21 1993 +0100 +++ b/src/ZF/List.ML Thu Sep 30 10:26:38 1993 +0100 @@ -55,17 +55,14 @@ val list_subset_univ = standard (list_mono RS (list_univ RSN (2,subset_trans))); -(***** val major::prems = goal List.thy "[| l: list(A); \ -\ c: C(0); \ -\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C() \ -\ |] ==> list_case(l,c,h) : C(l)"; -by (rtac (major RS list_induct) 1); -by (ALLGOALS (asm_simp_tac (ZF_ss addsimps - ([list_case_0,list_case_Pair]@prems)))); +\ c: C(Nil); \ +\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \ +\ |] ==> list_case(c,h,l) : C(l)"; +by (rtac (major RS List.induct) 1); +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.case_eqns @ prems)))); val list_case_type = result(); -****) (** For recursion **) diff -r 1c0926788772 -r 6c6d2f6e3185 src/ZF/ListFn.ML --- a/src/ZF/ListFn.ML Thu Sep 30 10:10:21 1993 +0100 +++ b/src/ZF/ListFn.ML Thu Sep 30 10:26:38 1993 +0100 @@ -8,6 +8,47 @@ open ListFn; +(** hd and tl **) + +goalw ListFn.thy [hd_def] "hd(Cons(a,l)) = a"; +by (resolve_tac List.case_eqns 1); +val hd_Cons = result(); + +goalw ListFn.thy [tl_def] "tl(Nil) = Nil"; +by (resolve_tac List.case_eqns 1); +val tl_Nil = result(); + +goalw ListFn.thy [tl_def] "tl(Cons(a,l)) = l"; +by (resolve_tac List.case_eqns 1); +val tl_Cons = result(); + +goal ListFn.thy "!!l. l: list(A) ==> tl(l) : list(A)"; +by (etac List.elim 1); +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (List.intrs @ [tl_Nil,tl_Cons])))); +val tl_type = result(); + +(** drop **) + +goalw ListFn.thy [drop_def] "drop(0, l) = l"; +by (rtac rec_0 1); +val drop_0 = result(); + +goalw ListFn.thy [drop_def] "!!i. i:nat ==> drop(i, Nil) = Nil"; +by (etac nat_induct 1); +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Nil]))); +val drop_Nil = result(); + +goalw ListFn.thy [drop_def] + "!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"; +by (etac nat_induct 1); +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_Cons]))); +val drop_succ_Cons = result(); + +goalw ListFn.thy [drop_def] + "!!i l. [| i:nat; l: list(A) |] ==> drop(i,l) : list(A)"; +by (etac nat_induct 1); +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [tl_type]))); +val drop_type = result(); (** list_rec -- by Vset recursion **) @@ -67,18 +108,18 @@ val [length_Nil,length_Cons] = list_recs length_def; -val prems = goalw ListFn.thy [length_def] - "l: list(A) ==> length(l) : nat"; -by (REPEAT (ares_tac (prems @ [list_rec_type, nat_0I, nat_succI]) 1)); +goalw ListFn.thy [length_def] + "!!l. l: list(A) ==> length(l) : nat"; +by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1)); val length_type = result(); (** app **) val [app_Nil,app_Cons] = list_recs app_def; -val prems = goalw ListFn.thy [app_def] - "[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)"; -by (REPEAT (ares_tac (prems @ [list_rec_type, ConsI]) 1)); +goalw ListFn.thy [app_def] + "!!xs ys. [| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)"; +by (REPEAT (ares_tac [list_rec_type, ConsI] 1)); val app_type = result(); (** rev **) @@ -204,6 +245,38 @@ by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_app]))); val length_flat = result(); +(** Length and drop **) + +(*Lemma for the inductive step of drop_length*) +goal ListFn.thy + "!!xs. xs: list(A) ==> \ +\ ALL x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"; +by (etac List.induct 1); +by (ALLGOALS (asm_simp_tac (list_ss addsimps [drop_0,drop_succ_Cons]))); +by (fast_tac ZF_cs 1); +val drop_length_Cons_lemma = result(); +val drop_length_Cons = standard (drop_length_Cons_lemma RS spec); + +goal ListFn.thy + "!!l. l: list(A) ==> ALL i: length(l). EX z zs. drop(i,l) = Cons(z,zs)"; +by (etac List.induct 1); +by (ALLGOALS (asm_simp_tac (list_ss addsimps bquant_simps))); +by (rtac conjI 1); +by (etac drop_length_Cons 1); +by (rtac ballI 1); +by (rtac natE 1); +by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1); +by (assume_tac 1); +by (asm_simp_tac (list_ss addsimps [drop_0]) 1); +by (fast_tac ZF_cs 1); +by (asm_simp_tac (list_ss addsimps [drop_succ_Cons]) 1); +by (dtac bspec 1); +by (fast_tac ZF_cs 2); +by (fast_tac (ZF_cs addEs [succ_in_naturalD,length_type]) 1); +val drop_length_lemma = result(); +val drop_length = standard (drop_length_lemma RS bspec); + + (*** theorems about app ***) val [major] = goal ListFn.thy "xs: list(A) ==> xs@Nil=xs"; diff -r 1c0926788772 -r 6c6d2f6e3185 src/ZF/ListFn.thy --- a/src/ZF/ListFn.thy Thu Sep 30 10:10:21 1993 +0100 +++ b/src/ZF/ListFn.thy Thu Sep 30 10:26:38 1993 +0100 @@ -18,6 +18,8 @@ length,rev :: "i=>i" flat :: "i=>i" list_add :: "i=>i" + hd,tl :: "i=>i" + drop :: "[i,i]=>i" (* List Enumeration *) "[]" :: "i" ("[]") @@ -31,6 +33,11 @@ rules + + hd_def "hd(l) == list_case(0, %x xs.x, l)" + tl_def "tl(l) == list_case(Nil, %x xs.xs, l)" + drop_def "drop(i,l) == rec(i, l, %j r. tl(r))" + list_rec_def "list_rec(l,c,h) == Vrec(l, %l g.list_case(c, %x xs. h(x, xs, g`xs), l))" @@ -40,5 +47,4 @@ rev_def "rev(l) == list_rec(l, Nil, %x xs r. r @ [x])" flat_def "flat(ls) == list_rec(ls, Nil, %l ls r. l @ r)" list_add_def "list_add(l) == list_rec(l, 0, %x xs r. x#+r)" - end diff -r 1c0926788772 -r 6c6d2f6e3185 src/ZF/Nat.ML --- a/src/ZF/Nat.ML Thu Sep 30 10:10:21 1993 +0100 +++ b/src/ZF/Nat.ML Thu Sep 30 10:26:38 1993 +0100 @@ -31,7 +31,7 @@ by (resolve_tac prems 1); val nat_succI = result(); -goalw Nat.thy [one_def] "1 : nat"; +goal Nat.thy "1 : nat"; by (rtac (nat_0I RS nat_succI) 1); val nat_1I = result(); @@ -59,7 +59,7 @@ val major::prems = goal Nat.thy "[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"; -br (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1; +by (rtac (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1); by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1 ORELSE ares_tac prems 1)); val natE = result(); @@ -69,10 +69,13 @@ by (REPEAT (ares_tac [Ord_0, Ord_succ] 1)); val naturals_are_ordinals = result(); +(* i: nat ==> 0: succ(i) *) +val nat_0_in_succ = naturals_are_ordinals RS Ord_0_in_succ; + goal Nat.thy "!!n. n: nat ==> n=0 | 0:n"; by (etac nat_induct 1); by (fast_tac ZF_cs 1); -by (fast_tac (ZF_cs addIs [naturals_are_ordinals RS Ord_0_mem_succ]) 1); +by (fast_tac (ZF_cs addIs [nat_0_in_succ]) 1); val natE0 = result(); goal Nat.thy "Ord(nat)"; @@ -84,6 +87,12 @@ by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1)); val Ord_nat = result(); +(* succ(i): nat ==> i: nat *) +val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans; + +(* [| succ(i): k; k: nat |] ==> i: k *) +val succ_in_naturalD = [succI1, asm_rl, naturals_are_ordinals] MRS Ord_trans; + (** Variations on mathematical induction **) (*complete induction*) @@ -97,7 +106,7 @@ by (ALLGOALS (asm_simp_tac (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, - Ord_nat RS Ord_in_Ord])))); + naturals_are_ordinals])))); val nat_induct_from_lemma = result(); (*Induction starting from m rather than 0*) @@ -125,6 +134,28 @@ by (REPEAT (ares_tac (prems@[ballI]) 1 ORELSE etac bspec 1)); val diff_induct = result(); +(** Induction principle analogous to trancl_induct **) + +goal Nat.thy + "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \ +\ (ALL n:nat. m:n --> P(m,n))"; +by (etac nat_induct 1); +by (ALLGOALS + (EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac, + fast_tac ZF_cs, fast_tac ZF_cs])); +val succ_less_induct_lemma = result(); + +val prems = goal Nat.thy + "[| m: n; n: nat; \ +\ P(m,succ(m)); \ +\ !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) \ +\ |] ==> P(m,n)"; +by (res_inst_tac [("P4","P")] + (succ_less_induct_lemma RS mp RS mp RS bspec RS mp) 1); +by (rtac (Ord_nat RSN (3,Ord_trans)) 1); +by (REPEAT (ares_tac (prems @ [ballI,impI]) 1)); +val succ_less_induct = result(); + (** nat_case **) goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a"; @@ -157,18 +188,16 @@ val [prem] = goal Nat.thy "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"; -val nat_rec_ss = ZF_ss - addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, - vimage_singleton_iff]; by (rtac nat_rec_trans 1); -by (simp_tac nat_rec_ss 1); +by (simp_tac (ZF_ss addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, + vimage_singleton_iff]) 1); val nat_rec_succ = result(); (** The union of two natural numbers is a natural number -- their maximum **) -(* [| ?i : nat; ?j : nat |] ==> ?i Un ?j : nat *) +(* [| i : nat; j : nat |] ==> i Un j : nat *) val Un_nat_type = standard (Ord_nat RSN (3,Ord_member_UnI)); -(* [| ?i : nat; ?j : nat |] ==> ?i Int ?j : nat *) +(* [| i : nat; j : nat |] ==> i Int j : nat *) val Int_nat_type = standard (Ord_nat RSN (3,Ord_member_IntI)); diff -r 1c0926788772 -r 6c6d2f6e3185 src/ZF/Ord.ML --- a/src/ZF/Ord.ML Thu Sep 30 10:10:21 1993 +0100 +++ b/src/ZF/Ord.ML Thu Sep 30 10:26:38 1993 +0100 @@ -47,14 +47,14 @@ val [prem1,prem2] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def] "[| Transset(C); A+B <= C |] ==> A <= C & B <= C"; -br (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1; +by (rtac (prem2 RS (Un_subset_iff RS iffD1) RS conjE) 1); by (REPEAT (etac (prem1 RS Transset_includes_range) 1 ORELSE resolve_tac [conjI, singletonI] 1)); val Transset_includes_summands = result(); val [prem] = goalw (merge_theories(Ord.thy,Sum.thy)) [sum_def] "Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)"; -br (Int_Un_distrib RS ssubst) 1; +by (rtac (Int_Un_distrib RS ssubst) 1); by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1); val Transset_sum_Int_subset = result(); @@ -281,7 +281,7 @@ by (fast_tac ZF_cs 1); by (rtac (prem RS Ord_succ) 1); by (rtac Ord_0 1); -val Ord_0_mem_succ = result(); +val Ord_0_in_succ = result(); goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j:i <-> j<=i & ~(i<=j)"; by (rtac iffI 1); @@ -293,7 +293,7 @@ val Ord_member_iff = result(); goal Ord.thy "!!i. Ord(i) ==> 0:i <-> ~ i=0"; -be (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1; +by (etac (Ord_0 RSN (2,Ord_member_iff) RS iff_trans) 1); by (fast_tac eq_cs 1); val Ord_0_member_iff = result(); @@ -307,6 +307,7 @@ by (ALLGOALS (fast_tac ZF_cs)); val member_succI = result(); +(*Recall Ord_succ_subsetI, namely [| i:j; Ord(j) |] ==> succ(i) <= j *) goalw Ord.thy [Transset_def,Ord_def] "!!i j. [| i : succ(j); Ord(j) |] ==> i<=j"; by (fast_tac ZF_cs 1); @@ -353,6 +354,8 @@ by (REPEAT (ares_tac [Ord_succ] 1)); val Ord_succ_mono = result(); +(** Union and Intersection **) + goal Ord.thy "!!i j k. [| i:k; j:k; Ord(k) |] ==> i Un j : k"; by (res_inst_tac [("i","i"),("j","j")] Ord_subset 1); by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); diff -r 1c0926788772 -r 6c6d2f6e3185 src/ZF/QUniv.ML --- a/src/ZF/QUniv.ML Thu Sep 30 10:10:21 1993 +0100 +++ b/src/ZF/QUniv.ML Thu Sep 30 10:26:38 1993 +0100 @@ -12,12 +12,12 @@ goalw QUniv.thy [quniv_def] "!!X A. X <= univ(eclose(A)) ==> X : quniv(A)"; -be PowI 1; +by (etac PowI 1); val qunivI = result(); goalw QUniv.thy [quniv_def] "!!X A. X : quniv(A) ==> X <= univ(eclose(A))"; -be PowD 1; +by (etac PowD 1); val qunivD = result(); goalw QUniv.thy [quniv_def] "!!A B. A<=B ==> quniv(A) <= quniv(B)"; @@ -152,8 +152,8 @@ goal Univ.thy "!!X. [| {a,b} : Vfrom(X,succ(i)); Transset(X) |] ==> \ \ a: Vfrom(X,i) & b: Vfrom(X,i)"; -bd (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1; -ba 1; +by (dtac (Transset_Vfrom_succ RS equalityD1 RS subsetD RS PowD) 1); +by (assume_tac 1); by (fast_tac ZF_cs 1); val doubleton_in_Vfrom_D = result(); @@ -185,8 +185,8 @@ goalw QUniv.thy [QPair_def,sum_def] "!!X. Transset(X) ==> \ \ Int Vfrom(X, succ(i)) <= "; -br (Int_Un_distrib RS ssubst) 1; -br Un_mono 1; +by (rtac (Int_Un_distrib RS ssubst) 1); +by (rtac Un_mono 1); by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans, [Int_lower1, subset_refl] MRS Sigma_mono] 1)); val QPair_Int_Vfrom_succ_subset = result(); @@ -194,12 +194,12 @@ (** Pairs in quniv -- for handling the base case **) goal QUniv.thy "!!X. : quniv(X) ==> : univ(eclose(X))"; -be ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1; +by (etac ([qunivD, Transset_eclose] MRS Transset_Pair_subset_univ) 1); val Pair_in_quniv_D = result(); goal QUniv.thy "a*b Int quniv(A) = a*b Int univ(eclose(A))"; -br equalityI 1; -br ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2; +by (rtac equalityI 1); +by (rtac ([subset_refl, univ_eclose_subset_quniv] MRS Int_mono) 2); by (fast_tac (ZF_cs addSEs [Pair_in_quniv_D]) 1); val product_Int_quniv_eq = result(); @@ -211,33 +211,33 @@ (**** "Take-lemma" rules for proving c: quniv(A) ****) goalw QUniv.thy [quniv_def] "Transset(quniv(A))"; -br (Transset_eclose RS Transset_univ RS Transset_Pow) 1; +by (rtac (Transset_eclose RS Transset_univ RS Transset_Pow) 1); val Transset_quniv = result(); val [aprem, iprem] = goal QUniv.thy "[| a: quniv(quniv(X)); \ \ !!i. i:nat ==> a Int Vfrom(quniv(X),i) : quniv(A) \ \ |] ==> a : quniv(A)"; -br (univ_Int_Vfrom_subset RS qunivI) 1; -br (aprem RS qunivD) 1; +by (rtac (univ_Int_Vfrom_subset RS qunivI) 1); +by (rtac (aprem RS qunivD) 1); by (rtac (Transset_quniv RS Transset_eclose_eq_arg RS ssubst) 1); -be (iprem RS qunivD) 1; +by (etac (iprem RS qunivD) 1); val quniv_Int_Vfrom = result(); (** Rules for level 0 **) goal QUniv.thy " Int quniv(A) : quniv(A)"; -br (QPair_Int_quniv_eq RS ssubst) 1; -br (Int_lower2 RS qunivI) 1; +by (rtac (QPair_Int_quniv_eq RS ssubst) 1); +by (rtac (Int_lower2 RS qunivI) 1); val QPair_Int_quniv_in_quniv = result(); (*Unused; kept as an example. QInr rule is similar*) goalw QUniv.thy [QInl_def] "QInl(a) Int quniv(A) : quniv(A)"; -br QPair_Int_quniv_in_quniv 1; +by (rtac QPair_Int_quniv_in_quniv 1); val QInl_Int_quniv_in_quniv = result(); goal QUniv.thy "!!a A X. a : quniv(A) ==> a Int X : quniv(A)"; -be ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1; +by (etac ([Int_lower1, qunivD] MRS subset_trans RS qunivI) 1); val Int_quniv_in_quniv = result(); goal QUniv.thy @@ -252,8 +252,8 @@ \ b Int Vfrom(X,i) : quniv(A); \ \ Transset(X) \ \ |] ==> Int Vfrom(X, succ(i)) : quniv(A)"; -br (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1; -br (QPair_in_quniv RS qunivD) 2; +by (rtac (QPair_Int_Vfrom_succ_subset RS subset_trans RS qunivI) 1); +by (rtac (QPair_in_quniv RS qunivD) 2); by (REPEAT (assume_tac 1)); val QPair_Int_Vfrom_succ_in_quniv = result(); @@ -267,7 +267,7 @@ goalw QUniv.thy [QInl_def] "!!X. [| a Int Vfrom(X,i) : quniv(A); Transset(X) \ \ |] ==> QInl(a) Int Vfrom(X, succ(i)) : quniv(A)"; -br QPair_Int_Vfrom_succ_in_quniv 1; +by (rtac QPair_Int_Vfrom_succ_in_quniv 1); by (REPEAT (ares_tac [zero_Int_in_quniv] 1)); val QInl_Int_Vfrom_succ_in_quniv = result(); @@ -276,7 +276,7 @@ goalw QUniv.thy [QPair_def] "!!X. Transset(X) ==> \ \ Int Vfrom(X,i) <= "; -be (Transset_Vfrom RS Transset_sum_Int_subset) 1; +by (etac (Transset_Vfrom RS Transset_sum_Int_subset) 1); val QPair_Int_Vfrom_subset = result(); goal QUniv.thy @@ -284,8 +284,8 @@ \ b Int Vfrom(X,i) : quniv(A); \ \ Transset(X) \ \ |] ==> Int Vfrom(X,i) : quniv(A)"; -br (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1; -br (QPair_in_quniv RS qunivD) 2; +by (rtac (QPair_Int_Vfrom_subset RS subset_trans RS qunivI) 1); +by (rtac (QPair_in_quniv RS qunivD) 2); by (REPEAT (assume_tac 1)); val QPair_Int_Vfrom_in_quniv = result(); @@ -309,15 +309,15 @@ "!!i. [| a Int Vset(i) <= c; \ \ b Int Vset(i) <= d \ \ |] ==> Int Vset(succ(i)) <= "; -br ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] - MRS subset_trans) 1; +by (rtac ([Transset_0 RS QPair_Int_Vfrom_succ_subset, QPair_mono] + MRS subset_trans) 1); by (REPEAT (assume_tac 1)); val QPair_Int_Vset_succ_subset_trans = result(); (*Unused; kept as an example. QInr rule is similar*) goalw QUniv.thy [QInl_def] "!!i. a Int Vset(i) <= b ==> QInl(a) Int Vset(succ(i)) <= QInl(b)"; -be (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1; +by (etac (Int_lower1 RS QPair_Int_Vset_succ_subset_trans) 1); val QInl_Int_Vset_succ_subset_trans = result(); (*Rule for level i -- preserving the level, not decreasing it*) @@ -325,8 +325,8 @@ "!!i. [| a Int Vset(i) <= c; \ \ b Int Vset(i) <= d \ \ |] ==> Int Vset(i) <= "; -br ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] - MRS subset_trans) 1; +by (rtac ([Transset_0 RS QPair_Int_Vfrom_subset, QPair_mono] + MRS subset_trans) 1); by (REPEAT (assume_tac 1)); val QPair_Int_Vset_subset_trans = result(); diff -r 1c0926788772 -r 6c6d2f6e3185 src/ZF/Univ.ML --- a/src/ZF/Univ.ML Thu Sep 30 10:10:21 1993 +0100 +++ b/src/ZF/Univ.ML Thu Sep 30 10:26:38 1993 +0100 @@ -47,11 +47,11 @@ by (eps_ind_tac "x" 1); by (rtac (Vfrom RS ssubst) 1); by (rtac (Vfrom RS ssubst) 1); -br (subset_refl RS Un_mono) 1; -br UN_least 1; +by (rtac (subset_refl RS Un_mono) 1); +by (rtac UN_least 1); by (etac (rank_implies_mem RS bexE) 1); -br subset_trans 1; -be UN_upper 2; +by (rtac subset_trans 1); +by (etac UN_upper 2); by (etac (subset_refl RS Vfrom_mono RS subset_trans RS Pow_mono) 1); by (etac bspec 1); by (assume_tac 1); @@ -144,16 +144,16 @@ by (rtac equalityI 1); (*first inclusion*) by (rtac Un_least 1); -br (A_subset_Vfrom RS subset_trans) 1; -br (prem RS UN_upper) 1; -br UN_least 1; -be UnionE 1; -br subset_trans 1; -be UN_upper 2; +by (rtac (A_subset_Vfrom RS subset_trans) 1); +by (rtac (prem RS UN_upper) 1); +by (rtac UN_least 1); +by (etac UnionE 1); +by (rtac subset_trans 1); +by (etac UN_upper 2); by (rtac (Vfrom RS ssubst) 1); -be ([UN_upper, Un_upper2] MRS subset_trans) 1; +by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1); (*opposite inclusion*) -br UN_least 1; +by (rtac UN_least 1); by (rtac (Vfrom RS ssubst) 1); by (fast_tac ZF_cs 1); val Vfrom_Union = result(); @@ -183,9 +183,9 @@ goalw Univ.thy [Limit_def] "!!i. [| Ord(i); 0:i; ALL y. ~ succ(y)=i |] ==> Limit(i)"; by (safe_tac subset_cs); -br Ord_member 1; +by (rtac Ord_member 1); by (REPEAT_FIRST (eresolve_tac [asm_rl, Ord_in_Ord RS Ord_succ] - ORELSE' dresolve_tac [Ord_succ_subsetI])); + ORELSE' dtac Ord_succ_subsetI )); by (fast_tac (subset_cs addSIs [equalityI]) 1); val non_succ_LimitI = result(); @@ -271,10 +271,10 @@ goal Univ.thy "!!A i. Transset(A) ==> Vfrom(A, succ(i)) = Pow(Vfrom(A,i))"; by (rtac (Vfrom_succ RS trans) 1); -br (Un_upper2 RSN (2,equalityI)) 1;; -br (subset_refl RSN (2,Un_least)) 1;; -br (A_subset_Vfrom RS subset_trans) 1; -be (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1; +by (rtac (Un_upper2 RSN (2,equalityI)) 1); +by (rtac (subset_refl RSN (2,Un_least)) 1); +by (rtac (A_subset_Vfrom RS subset_trans) 1); +by (etac (Transset_Vfrom RS (Transset_iff_Pow RS iffD1)) 1); val Transset_Vfrom_succ = result(); goalw Ord.thy [Pair_def,Transset_def] @@ -285,8 +285,8 @@ goal Univ.thy "!!a b.[| <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \ \ : Vfrom(A,i)"; -be (Transset_Pair_subset RS conjE) 1; -be Transset_Vfrom 1; +by (etac (Transset_Pair_subset RS conjE) 1); +by (etac Transset_Vfrom 1); by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1)); val Transset_Pair_subset_Vfrom_limit = result(); @@ -346,7 +346,7 @@ by (rtac (bprem RS (limiti RS Limit_VfromE)) 1); by (rtac (limiti RS Limit_Vfrom_eq RS ssubst) 1); by (rtac UN_I 1); -by (rtac (rewrite_rule [one_def] sum_in_Vfrom) 2); +by (rtac sum_in_Vfrom 2); by (rtac (succI1 RS UnI1) 5); (*Infer that succ(succ(succ(x Un xa))) < i *) by (etac (Vfrom_UnI1 RS Vfrom_UnI2) 2); @@ -456,14 +456,14 @@ val Vset_rankI = Ord_rank RS VsetI; goal Univ.thy "a <= Vset(rank(a))"; -br subsetI 1; -be (rank_lt RS Vset_rankI) 1; +by (rtac subsetI 1); +by (etac (rank_lt RS Vset_rankI) 1); val arg_subset_Vset_rank = result(); val [iprem] = goal Univ.thy "[| !!i. Ord(i) ==> a Int Vset(i) <= b |] ==> a <= b"; -br ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1; -br (Ord_rank RS iprem) 1; +by (rtac ([subset_refl, arg_subset_Vset_rank] MRS Int_greatest RS subset_trans) 1); +by (rtac (Ord_rank RS iprem) 1); val Int_Vset_subset = result(); (** Set up an environment for simplification **) @@ -507,28 +507,28 @@ (** univ(A) as a limit **) goalw Univ.thy [univ_def] "univ(A) = (UN i:nat. Vfrom(A,i))"; -br (Limit_nat RS Limit_Vfrom_eq) 1; +by (rtac (Limit_nat RS Limit_Vfrom_eq) 1); val univ_eq_UN = result(); goal Univ.thy "!!c. c <= univ(A) ==> c = (UN i:nat. c Int Vfrom(A,i))"; -br (subset_UN_iff_eq RS iffD1) 1; -be (univ_eq_UN RS subst) 1; +by (rtac (subset_UN_iff_eq RS iffD1) 1); +by (etac (univ_eq_UN RS subst) 1); val subset_univ_eq_Int = result(); val [aprem, iprem] = goal Univ.thy "[| a <= univ(X); \ \ !!i. i:nat ==> a Int Vfrom(X,i) <= b \ \ |] ==> a <= b"; -br (aprem RS subset_univ_eq_Int RS ssubst) 1; -br UN_least 1; -be iprem 1; +by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1); +by (rtac UN_least 1); +by (etac iprem 1); val univ_Int_Vfrom_subset = result(); val prems = goal Univ.thy "[| a <= univ(X); b <= univ(X); \ \ !!i. i:nat ==> a Int Vfrom(X,i) = b Int Vfrom(X,i) \ \ |] ==> a = b"; -br equalityI 1; +by (rtac equalityI 1); by (ALLGOALS (resolve_tac (prems RL [univ_Int_Vfrom_subset]) THEN' eresolve_tac (prems RL [equalityD1,equalityD2] RL [subset_trans]) THEN' @@ -576,7 +576,7 @@ goalw Univ.thy [univ_def] "!!a b.[| <= univ(A); Transset(A) |] ==> : univ(A)"; -be Transset_Pair_subset_Vfrom_limit 1; +by (etac Transset_Pair_subset_Vfrom_limit 1); by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); val Transset_Pair_subset_univ = result(); @@ -592,7 +592,7 @@ (** instances for 1 and 2 **) -goalw Univ.thy [one_def] "1 : univ(A)"; +goal Univ.thy "1 : univ(A)"; by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); val one_in_univ = result();