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
--- 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(<x,y>) \
-\ |] ==> 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 **)
--- 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";
--- 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
--- 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));
--- 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));
--- 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) ==> \
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,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. <a,b> : quniv(X) ==> <a,b> : 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 "<a;b> 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) \
\ |] ==> <a;b> 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) ==> \
\ <a;b> Int Vfrom(X,i) <= <a Int Vfrom(X,i); b 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) \
\ |] ==> <a;b> 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 \
\ |] ==> <a;b> Int Vset(succ(i)) <= <c;d>";
-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 \
\ |] ==> <a;b> Int Vset(i) <= <c;d>";
-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();
--- 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.[| <a,b> <= Vfrom(A,i); Transset(A); Limit(i) |] ==> \
\ <a,b> : 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.[| <a,b> <= univ(A); Transset(A) |] ==> <a,b> : 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();