src/ZF/quniv.ML

 
 (** Introduction and elimination rules avoid tiresome folding/unfolding **)
 
 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)";
 by (etac (eclose_mono RS univ_mono RS Pow_mono) 1);
 val quniv_mono = result();

 
 (*This version says a, b exist one level down, in the smaller set Vfrom(X,i)*)
 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();
 
 (*This weaker version says a, b exist at the same level*)
 val Vfrom_doubleton_D = standard (Transset_Vfrom RS Transset_doubleton_D);

 (*** Intersecting <a;b> with Vfrom... ***)
 
 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();
 
 (** 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();
 
 goalw QUniv.thy [QPair_def,sum_def]
     "<a;b> Int quniv(A) = <a;b> Int univ(eclose(A))";

 val QPair_Int_quniv_eq = result();
 
 (**** "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 
  "!!X. a Int X : quniv(A) ==> a Int Vfrom(X, 0) : quniv(A)";
 by (etac (Vfrom_0 RS ssubst) 1);

 goal QUniv.thy 
  "!!X. [| a Int Vfrom(X,i) : quniv(A);	\
 \         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();
 
 val zero_Int_in_quniv = standard
     ([Int_lower1,empty_subsetI] MRS subset_trans RS qunivI);

 
 (*Unused; kept as an example.  QInr rule is similar*)
 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();
 
 (** Rules for level i -- preserving the level, not decreasing it **)
 
 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 
  "!!X. [| a Int Vfrom(X,i) : quniv(A);	\
 \         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();
 
 
 (**** "Take-lemma" rules for proving a=b by co-induction ****)

 (*Rule for level succ(i), decreasing it to i*)
 goal QUniv.thy 
  "!!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*)
 goal QUniv.thy 
  "!!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();