--- a/src/HOL/Arith.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Arith.ML Mon Jun 23 10:42:03 1997 +0200
@@ -12,11 +12,11 @@
(*** Basic rewrite rules for the arithmetic operators ***)
goalw Arith.thy [pred_def] "pred 0 = 0";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "pred_0";
goalw Arith.thy [pred_def] "pred(Suc n) = n";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "pred_Suc";
Addsimps [pred_0,pred_Suc];
@@ -175,8 +175,8 @@
qed "add_lessD1";
goal Arith.thy "!!i::nat. ~ (i+j < i)";
-br notI 1;
-be (add_lessD1 RS less_irrefl) 1;
+by (rtac notI 1);
+by (etac (add_lessD1 RS less_irrefl) 1);
qed "not_add_less1";
goal Arith.thy "!!i::nat. ~ (j+i < i)";
@@ -506,7 +506,7 @@
qed "mult_less_mono2";
goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
-bd mult_less_mono2 1;
+by (dtac mult_less_mono2 1);
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [mult_commute])));
qed "mult_less_mono1";
@@ -531,21 +531,21 @@
qed "mult_less_cancel2";
goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";
-bd mult_less_cancel2 1;
+by (dtac mult_less_cancel2 1);
by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
qed "mult_less_cancel1";
Addsimps [mult_less_cancel1, mult_less_cancel2];
goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
by (cut_facts_tac [less_linear] 1);
-by(Step_tac 1);
-ba 2;
+by (Step_tac 1);
+by (assume_tac 2);
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
by (ALLGOALS Asm_full_simp_tac);
qed "mult_cancel2";
goal Arith.thy "!!k. 0<k ==> (k*m = k*n) = (m=n)";
-bd mult_cancel2 1;
+by (dtac mult_cancel2 1);
by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
qed "mult_cancel1";
Addsimps [mult_cancel1, mult_cancel2];
@@ -574,13 +574,13 @@
qed "diff_less_mono";
goal Arith.thy "!! a b c::nat. a+b < c ==> a < c-b";
-bd diff_less_mono 1;
-br le_add2 1;
+by (dtac diff_less_mono 1);
+by (rtac le_add2 1);
by (Asm_full_simp_tac 1);
qed "add_less_imp_less_diff";
goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)";
-br Suc_diff_n 1;
+by (rtac Suc_diff_n 1);
by (asm_full_simp_tac (!simpset addsimps [le_eq_less_Suc]) 1);
qed "Suc_diff_le";
@@ -597,7 +597,7 @@
Addsimps [diff_diff_cancel];
goal Arith.thy "!!k::nat. k <= n ==> m <= n + m - k";
-be rev_mp 1;
+by (etac rev_mp 1);
by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
by (Simp_tac 1);
by (simp_tac (!simpset addsimps [less_add_Suc2, less_imp_le]) 1);
--- a/src/HOL/Divides.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Divides.ML Mon Jun 23 10:42:03 1997 +0200
@@ -189,7 +189,7 @@
goal thy "!!n. 0<n ==> m*n div n = m";
by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [mod_mult_self_is_0]) 1);
qed "div_mult_self_is_m";
Addsimps [div_mult_self_is_m];
@@ -264,7 +264,7 @@
qed "dvd_diff";
goal thy "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
-be (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1;
+by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
by (blast_tac (!claset addIs [dvd_add]) 1);
qed "dvd_diffD";
@@ -316,9 +316,9 @@
goalw thy [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
by (Step_tac 1);
by (ALLGOALS (full_simp_tac (!simpset addsimps [zero_less_mult_iff])));
-be conjE 1;
-br le_trans 1;
-br (le_refl RS mult_le_mono) 2;
+by (etac conjE 1);
+by (rtac le_trans 1);
+by (rtac (le_refl RS mult_le_mono) 2);
by (etac Suc_leI 2);
by (Simp_tac 1);
qed "dvd_imp_le";
--- a/src/HOL/Finite.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Finite.ML Mon Jun 23 10:42:03 1997 +0200
@@ -41,7 +41,7 @@
\ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \
\ |] ==> F <= A --> P(F)";
by (rtac (major RS finite_induct) 1);
-by(ALLGOALS (blast_tac (!claset addIs prems)));
+by (ALLGOALS (blast_tac (!claset addIs prems)));
val lemma = result();
val prems = goal Finite.thy
@@ -49,7 +49,7 @@
\ P({}); \
\ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \
\ |] ==> P(F)";
-by(blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
+by (blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
qed "finite_subset_induct";
Addsimps Finites.intrs;
@@ -122,7 +122,7 @@
goal Finite.thy "finite(A-{a}) = finite(A)";
by (case_tac "a:A" 1);
-br (finite_insert RS sym RS trans) 1;
+by (rtac (finite_insert RS sym RS trans) 1);
by (stac insert_Diff 1);
by (ALLGOALS Asm_simp_tac);
qed "finite_Diff_singleton";
@@ -134,21 +134,21 @@
by (Step_tac 1);
by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
by (Step_tac 1);
- bw inj_onto_def;
+ by (rewtac inj_onto_def);
by (Blast_tac 1);
by (thin_tac "ALL A. ?PP(A)" 1);
by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
by (Step_tac 1);
by (res_inst_tac [("x","xa")] bexI 1);
by (ALLGOALS Asm_simp_tac);
-be equalityE 1;
-br equalityI 1;
+by (etac equalityE 1);
+by (rtac equalityI 1);
by (Blast_tac 2);
by (Best_tac 1);
val lemma = result();
goal Finite.thy "!!A. [| finite(f``A); inj_onto f A |] ==> finite A";
-bd lemma 1;
+by (dtac lemma 1);
by (Blast_tac 1);
qed "finite_imageD";
@@ -157,15 +157,15 @@
goal Finite.thy "!!A. finite(Pow A) ==> finite A";
by (subgoal_tac "finite ((%x.{x})``A)" 1);
-br finite_subset 2;
-ba 3;
+by (rtac finite_subset 2);
+by (assume_tac 3);
by (ALLGOALS
(fast_tac (!claset addSDs [rewrite_rule [inj_onto_def] finite_imageD])));
val lemma = result();
goal Finite.thy "finite(Pow A) = finite A";
-br iffI 1;
-be lemma 1;
+by (rtac iffI 1);
+by (etac lemma 1);
(*Opposite inclusion: finite A ==> finite (Pow A) *)
by (etac finite_induct 1);
by (ALLGOALS
@@ -175,19 +175,19 @@
AddIffs [finite_Pow_iff];
goal Finite.thy "finite(r^-1) = finite r";
-by(subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
- by(Asm_simp_tac 1);
- br iffI 1;
- be (rewrite_rule [inj_onto_def] finite_imageD) 1;
- by(simp_tac (!simpset setloop (split_tac[expand_split])) 1);
- be finite_imageI 1;
-by(simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
-by(Auto_tac());
- br bexI 1;
- ba 2;
- by(Simp_tac 1);
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
+by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
+ by (Asm_simp_tac 1);
+ by (rtac iffI 1);
+ by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
+ by (simp_tac (!simpset setloop (split_tac[expand_split])) 1);
+ by (etac finite_imageI 1);
+by (simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
+by (Auto_tac());
+ by (rtac bexI 1);
+ by (assume_tac 2);
+ by (Simp_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
qed "finite_inverse";
AddIffs [finite_inverse];
@@ -249,7 +249,7 @@
by (Asm_simp_tac 1);
by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
by (Blast_tac 1);
- bd sym 1;
+ by (dtac sym 1);
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
@@ -282,21 +282,21 @@
goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
\ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
by (rtac Least_equality 1);
- bd finite_has_card 1;
- be exE 1;
+ by (dtac finite_has_card 1);
+ by (etac exE 1);
by (dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
- be exE 1;
+ by (etac exE 1);
by (res_inst_tac
[("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
by (simp_tac
(!simpset addsimps [Collect_conv_insert, less_Suc_eq]
addcongs [rev_conj_cong]) 1);
- be subst 1;
- br refl 1;
+ by (etac subst 1);
+ by (rtac refl 1);
by (rtac notI 1);
by (etac exE 1);
by (dtac lemma 1);
- ba 1;
+ by (assume_tac 1);
by (etac exE 1);
by (etac conjE 1);
by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
@@ -339,9 +339,9 @@
goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
by (subgoal_tac "(A-B) Un B = A" 1);
by (Blast_tac 2);
-br (add_right_cancel RS iffD1) 1;
-br (card_Un_disjoint RS subst) 1;
-be ssubst 4;
+by (rtac (add_right_cancel RS iffD1) 1);
+by (rtac (card_Un_disjoint RS subst) 1);
+by (etac ssubst 4);
by (Blast_tac 3);
by (ALLGOALS
(asm_simp_tac
@@ -382,7 +382,7 @@
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by (Step_tac 1);
-bw inj_onto_def;
+by (rewtac inj_onto_def);
by (Blast_tac 1);
by (stac card_insert_disjoint 1);
by (etac finite_imageI 1);
@@ -397,7 +397,7 @@
by (EVERY (map (blast_tac (!claset addIs [finite_imageI])) [3,2,1]));
by (subgoal_tac "inj_onto (insert x) (Pow F)" 1);
by (asm_simp_tac (!simpset addsimps [card_image, Pow_insert]) 1);
-bw inj_onto_def;
+by (rewtac inj_onto_def);
by (blast_tac (!claset addSEs [equalityE]) 1);
qed "card_Pow";
Addsimps [card_Pow];
--- a/src/HOL/IMP/Denotation.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/IMP/Denotation.ML Mon Jun 23 10:42:03 1997 +0200
@@ -29,7 +29,7 @@
(* start with rule induction *)
by (etac evalc.induct 1);
-auto();
+by (Auto_tac());
(* while *)
by (rewtac Gamma_def);
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
--- a/src/HOL/Induct/Com.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Induct/Com.ML Mon Jun 23 10:42:03 1997 +0200
@@ -52,7 +52,7 @@
qed "assign_different";
goalw thy [assign_def] "s[s x/x] = s";
-br ext 1;
+by (rtac ext 1);
by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
qed "assign_triv";
--- a/src/HOL/Integ/Equiv.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Integ/Equiv.ML Mon Jun 23 10:42:03 1997 +0200
@@ -263,14 +263,14 @@
goal thy "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";
by (rtac finite_subset 1);
by (etac (finite_Pow_iff RS iffD2) 2);
-by (rewrite_goals_tac [quotient_def]);
+by (rewtac quotient_def);
by (Blast_tac 1);
qed "finite_quotient";
goalw thy [quotient_def]
"!!A. [| finite A; r <= A Times A; X : A/r |] ==> finite X";
by (rtac finite_subset 1);
-ba 2;
+by (assume_tac 2);
by (Blast_tac 1);
qed "finite_equiv_class";
--- a/src/HOL/List.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/List.ML Mon Jun 23 10:42:03 1997 +0200
@@ -38,8 +38,8 @@
qed "expand_list_case";
val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
-by(induct_tac "xs" 1);
-by(REPEAT(resolve_tac prems 1));
+by (induct_tac "xs" 1);
+by (REPEAT(resolve_tac prems 1));
qed "list_cases";
goal thy "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
@@ -73,7 +73,7 @@
goal thy "([] = xs@ys) = (xs=[] & ys=[])";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "Nil_is_append_conv";
AddIffs [Nil_is_append_conv];
@@ -84,19 +84,19 @@
AddIffs [same_append_eq];
goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)";
-by(induct_tac "xs" 1);
- br allI 1;
- by(induct_tac "ys" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(induct_tac "ys" 1);
- by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+ by (rtac allI 1);
+ by (induct_tac "ys" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (induct_tac "ys" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "append1_eq_conv";
AddIffs [append1_eq_conv];
goal thy "xs ~= [] --> hd xs # tl xs = xs";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed_spec_mp "hd_Cons_tl";
Addsimps [hd_Cons_tl];
@@ -106,15 +106,15 @@
qed "hd_append";
goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
-by(simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
+by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
qed "tl_append";
(** map **)
goal thy
"(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
goal thy "map (%x.x) = (%xs.xs)";
@@ -190,20 +190,20 @@
qed "set_of_list_subset_Cons";
goal thy "(set_of_list xs = {}) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "set_of_list_empty";
Addsimps [set_of_list_empty];
goal thy "set_of_list(rev xs) = set_of_list(xs)";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "set_of_list_rev";
Addsimps [set_of_list_rev];
goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "set_of_list_map";
Addsimps [set_of_list_map];
@@ -232,14 +232,14 @@
(** filter **)
goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
-by(induct_tac "xs" 1);
- by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (induct_tac "xs" 1);
+ by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "filter_append";
Addsimps [filter_append];
goal thy "size (filter P xs) <= size xs";
-by(induct_tac "xs" 1);
- by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (induct_tac "xs" 1);
+ by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "filter_size";
@@ -277,14 +277,14 @@
Addsimps [length_rev];
goal thy "(length xs = 0) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "length_0_conv";
AddIffs [length_0_conv];
goal thy "(0 < length xs) = (xs ~= [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "length_greater_0_conv";
AddIffs [length_greater_0_conv];
@@ -294,14 +294,14 @@
goal thy
"!xs. nth n (xs@ys) = \
\ (if n < length xs then nth n xs else nth (n - length xs) ys)";
-by(nat_ind_tac "n" 1);
- by(Asm_simp_tac 1);
- br allI 1;
- by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (Asm_simp_tac 1);
+ by (rtac allI 1);
+ by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "nth_append";
goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
@@ -365,118 +365,118 @@
Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
goal thy "!xs. length(take n xs) = min (length xs) n";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "length_take";
Addsimps [length_take];
goal thy "!xs. length(drop n xs) = (length xs - n)";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "length_drop";
Addsimps [length_drop];
goal thy "!xs. length xs <= n --> take n xs = xs";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "take_all";
goal thy "!xs. length xs <= n --> drop n xs = []";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "drop_all";
goal thy
"!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "take_append";
Addsimps [take_append];
goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "drop_append";
Addsimps [drop_append];
goal thy "!xs n. take n (take m xs) = take (min n m) xs";
-by(nat_ind_tac "m" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "m" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "take_take";
goal thy "!xs. drop n (drop m xs) = drop (n + m) xs";
-by(nat_ind_tac "m" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "m" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "drop_drop";
goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)";
-by(nat_ind_tac "m" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "m" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "take_drop";
goal thy "!xs. take n (map f xs) = map f (take n xs)";
-by(nat_ind_tac "n" 1);
-by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed_spec_mp "take_map";
goal thy "!xs. drop n (map f xs) = map f (drop n xs)";
-by(nat_ind_tac "n" 1);
-by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed_spec_mp "drop_map";
goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
-by(induct_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
-by(strip_tac 1);
-by(exhaust_tac "n" 1);
- by(Blast_tac 1);
-by(exhaust_tac "i" 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (induct_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (strip_tac 1);
+by (exhaust_tac "n" 1);
+ by (Blast_tac 1);
+by (exhaust_tac "i" 1);
+by (ALLGOALS Asm_full_simp_tac);
qed_spec_mp "nth_take";
Addsimps [nth_take];
goal thy "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
qed_spec_mp "nth_drop";
Addsimps [nth_drop];
@@ -484,41 +484,41 @@
goal thy
"x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Blast_tac 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (Blast_tac 1);
bind_thm("takeWhile_append1", conjI RS (result() RS mp));
Addsimps [takeWhile_append1];
goal thy
"(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
bind_thm("takeWhile_append2", ballI RS (result() RS mp));
Addsimps [takeWhile_append2];
goal thy
"x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Blast_tac 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (Blast_tac 1);
bind_thm("dropWhile_append1", conjI RS (result() RS mp));
Addsimps [dropWhile_append1];
goal thy
"(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
bind_thm("dropWhile_append2", ballI RS (result() RS mp));
Addsimps [dropWhile_append2];
goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
qed_spec_mp"set_of_list_take_whileD";
--- a/src/HOL/Modelcheck/MCSyn.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Modelcheck/MCSyn.ML Mon Jun 23 10:42:03 1997 +0200
@@ -19,16 +19,16 @@
goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
-auto();
+by (Auto_tac());
by (split_all_tac 1);
-auto();
+by (Auto_tac());
qed "split_paired_Ex";
goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
- br ext 1;
+ by (rtac ext 1);
by (stac (surjective_pairing RS sym) 1);
- br refl 1;
+ by (rtac refl 1);
qed "pair_eta_expand";
local
--- a/src/HOL/NatDef.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/NatDef.ML Mon Jun 23 10:42:03 1997 +0200
@@ -135,7 +135,7 @@
bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
goal thy "!!n. n ~= 0 ==> EX m. n = Suc m";
-br natE 1;
+by (rtac natE 1);
by (REPEAT (Blast_tac 1));
qed "not0_implies_Suc";
@@ -567,15 +567,15 @@
(** LEAST -- the least number operator **)
goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";
-by(blast_tac (!claset addIs [leI] addEs [leE]) 1);
+by (blast_tac (!claset addIs [leI] addEs [leE]) 1);
val lemma = result();
(* This is an old def of Least for nat, which is derived for compatibility *)
goalw thy [Least_def]
"(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
-by(simp_tac (!simpset addsimps [lemma]) 1);
-br eq_reflection 1;
-br refl 1;
+by (simp_tac (!simpset addsimps [lemma]) 1);
+by (rtac eq_reflection 1);
+by (rtac refl 1);
qed "Least_nat_def";
val [prem1,prem2] = goalw thy [Least_nat_def]
--- a/src/HOL/Power.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Power.ML Mon Jun 23 10:42:03 1997 +0200
@@ -28,15 +28,15 @@
qed "zero_less_power";
goalw thy [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n";
-be (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1;
+by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
by (asm_simp_tac (!simpset addsimps [power_add]) 1);
by (Blast_tac 1);
qed "le_imp_power_dvd";
goal thy "!! i r. [| 0 < i; i^m < i^n |] ==> m<n";
-br ccontr 1;
-bd (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1;
-be zero_less_power 1;
+by (rtac ccontr 1);
+by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
+by (etac zero_less_power 1);
by (contr_tac 1);
qed "power_less_imp_less";
--- a/src/HOL/Quot/HQUOT.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Quot/HQUOT.ML Mon Jun 23 10:42:03 1997 +0200
@@ -14,7 +14,7 @@
val prems = goal thy "Rep_quot a = Rep_quot b ==> a=b";
by (cut_facts_tac prems 1);
-br (Rep_quot_inverse RS subst) 1;
+by (rtac (Rep_quot_inverse RS subst) 1);
by (res_inst_tac [("t","a")] (Rep_quot_inverse RS subst) 1);
by (Asm_simp_tac 1);
qed "quot_eq";
@@ -22,8 +22,8 @@
(* prepare induction and exhaustiveness *)
val prems = goal thy "!s.s:quot --> P (Abs_quot s) ==> P x";
by (cut_facts_tac prems 1);
-br (Abs_quot_inverse RS subst) 1;
-br Rep_quot 1;
+by (rtac (Abs_quot_inverse RS subst) 1);
+by (rtac Rep_quot 1);
by (dres_inst_tac [("x","Rep_quot x")] spec 1);
by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
qed "all_q";
@@ -39,90 +39,90 @@
val prems = goalw thy [peclass_def] "x===y==><[x]>=<[y]>";
by (cut_facts_tac prems 1);
by (res_inst_tac [("f","Abs_quot")] arg_cong 1);
-br Collect_cong 1;
-br iffI 1;
-be per_trans 1;ba 1;
-be per_trans 1;
-be per_sym 1;
+by (rtac Collect_cong 1);
+by (rtac iffI 1);
+by (etac per_trans 1);by (assume_tac 1);
+by (etac per_trans 1);
+by (etac per_sym 1);
qed "per_class_eqI";
val prems = goalw thy [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y";
by (cut_facts_tac prems 1);
by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
-by (dres_inst_tac [("c","x")] equalityCE 1);ba 3;
+by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
by (safe_tac set_cs);
by (fast_tac (set_cs addIs [er_refl]) 1);
qed "er_class_eqE";
val prems = goalw thy [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y";
by (cut_facts_tac prems 1);
-bd DomainD 1;
+by (dtac DomainD 1);
by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
-by (dres_inst_tac [("c","x")] equalityCE 1);ba 3;
+by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
by (safe_tac set_cs);
qed "per_class_eqE";
goal thy "<[(x::'a::er)]>=<[y]>=x===y";
-br iffI 1;
-be er_class_eqE 1;
-be per_class_eqI 1;
+by (rtac iffI 1);
+by (etac er_class_eqE 1);
+by (etac per_class_eqI 1);
qed "er_class_eq";
val prems = goal thy "x:D==><[x]>=<[y]>=x===y";
by (cut_facts_tac prems 1);
-br iffI 1;
-be per_class_eqE 1;ba 1;
-be per_class_eqI 1;
+by (rtac iffI 1);
+by (etac per_class_eqE 1);by (assume_tac 1);
+by (etac per_class_eqI 1);
qed "per_class_eq";
(* inequality *)
val prems = goal thy "[|x:D;~x===y|]==><[x]>~=<[y]>";
by (cut_facts_tac prems 1);
-br notI 1;
-bd per_class_eqE 1;
-auto();
+by (rtac notI 1);
+by (dtac per_class_eqE 1);
+by (Auto_tac());
qed "per_class_neqI";
val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>";
by (cut_facts_tac prems 1);
-br notI 1;
-bd er_class_eqE 1;
-auto();
+by (rtac notI 1);
+by (dtac er_class_eqE 1);
+by (Auto_tac());
qed "er_class_neqI";
val prems = goal thy "<[x]>~=<[y]>==>~x===y";
by (cut_facts_tac prems 1);
-br notI 1;
-be notE 1;
-be per_class_eqI 1;
+by (rtac notI 1);
+by (etac notE 1);
+by (etac per_class_eqI 1);
qed "per_class_neqE";
val prems = goal thy "x:D==><[x]>~=<[y]>=(~x===y)";
by (cut_facts_tac prems 1);
-br iffI 1;
-be per_class_neqE 1;
-be per_class_neqI 1;ba 1;
+by (rtac iffI 1);
+by (etac per_class_neqE 1);
+by (etac per_class_neqI 1);by (assume_tac 1);
qed "per_class_not";
goal thy "<[(x::'a::er)]>~=<[y]>=(~x===y)";
-br iffI 1;
-be per_class_neqE 1;
-be er_class_neqI 1;
+by (rtac iffI 1);
+by (etac per_class_neqE 1);
+by (etac er_class_neqI 1);
qed "er_class_not";
(* exhaustiveness and induction *)
goalw thy [peclass_def] "? s.x=<[s]>";
-br all_q 1;
+by (rtac all_q 1);
by (strip_tac 1);
by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
-be exE 1;
+by (etac exE 1);
by (res_inst_tac [("x","r")] exI 1);
-br quot_eq 1;
+by (rtac quot_eq 1);
by (subgoal_tac "s:quot" 1);
by (asm_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
-br set_ext 1;
+by (rtac set_ext 1);
by (fast_tac set_cs 1);
by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
by (fast_tac set_cs 1);
--- a/src/HOL/Quot/NPAIR.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Quot/NPAIR.ML Mon Jun 23 10:42:03 1997 +0200
@@ -7,13 +7,13 @@
open NPAIR;
goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
-auto();
+by (Auto_tac());
qed "rep_abs_NP";
Addsimps [rep_abs_NP];
val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
by (cut_facts_tac prems 1);
-auto();
+by (Auto_tac());
qed "per_sym_NP";
--- a/src/HOL/Quot/PER.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Quot/PER.ML Mon Jun 23 10:42:03 1997 +0200
@@ -7,13 +7,13 @@
open PER;
goalw thy [fun_per_def,per_def] "f===g=(!x y.x:D&y:D&x===y-->f x===g y)";
-br refl 1;
+by (rtac refl 1);
qed "inst_fun_per";
(* Witness that quot is not empty *)
goal thy "?z:{s.? r.!y.y:s=y===r}";
fr CollectI;
by (res_inst_tac [("x","x")] exI 1);
-br allI 1;
-br mem_Collect_eq 1;
+by (rtac allI 1);
+by (rtac mem_Collect_eq 1);
qed "quotNE";
--- a/src/HOL/Quot/PER0.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Quot/PER0.ML Mon Jun 23 10:42:03 1997 +0200
@@ -9,37 +9,37 @@
(* derive the characteristic axioms *)
val prems = goalw thy [per_def] "x === y ==> y === x";
by (cut_facts_tac prems 1);
-be ax_per_sym 1;
+by (etac ax_per_sym 1);
qed "per_sym";
val prems = goalw thy [per_def] "[| x === y; y === z |] ==> x === z";
by (cut_facts_tac prems 1);
-be ax_per_trans 1;
-ba 1;
+by (etac ax_per_trans 1);
+by (assume_tac 1);
qed "per_trans";
goalw thy [per_def] "(x::'a::er) === x";
-br ax_er_refl 1;
+by (rtac ax_er_refl 1);
qed "er_refl";
(* now everything works without axclasses *)
goal thy "x===y=y===x";
-br iffI 1;
-be per_sym 1;
-be per_sym 1;
+by (rtac iffI 1);
+by (etac per_sym 1);
+by (etac per_sym 1);
qed "per_sym2";
val prems = goal thy "x===y ==> x===x";
by (cut_facts_tac prems 1);
-br per_trans 1;ba 1;
-be per_sym 1;
+by (rtac per_trans 1);by (assume_tac 1);
+by (etac per_sym 1);
qed "sym2refl1";
val prems = goal thy "x===y ==> y===y";
by (cut_facts_tac prems 1);
-br per_trans 1;ba 2;
-be per_sym 1;
+by (rtac per_trans 1);by (assume_tac 2);
+by (etac per_sym 1);
qed "sym2refl2";
val prems = goalw thy [Dom] "x:D ==> x === x";
@@ -53,44 +53,44 @@
qed "DomainI";
goal thy "x:D = x===x";
-br iffI 1;
-be DomainD 1;
-be DomainI 1;
+by (rtac iffI 1);
+by (etac DomainD 1);
+by (etac DomainI 1);
qed "DomainEq";
goal thy "(~ x === y) = (~ y === x)";
-br (per_sym2 RS arg_cong) 1;
+by (rtac (per_sym2 RS arg_cong) 1);
qed "per_not_sym";
(* show that PER work only on D *)
val prems = goal thy "x===y ==> x:D";
by (cut_facts_tac prems 1);
-be (sym2refl1 RS DomainI) 1;
+by (etac (sym2refl1 RS DomainI) 1);
qed "DomainI_left";
val prems = goal thy "x===y ==> y:D";
by (cut_facts_tac prems 1);
-be (sym2refl2 RS DomainI) 1;
+by (etac (sym2refl2 RS DomainI) 1);
qed "DomainI_right";
val prems = goalw thy [Dom] "x~:D ==> ~x===y";
by (cut_facts_tac prems 1);
-by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);ba 1;
-bd sym2refl1 1;
+by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);by (assume_tac 1);
+by (dtac sym2refl1 1);
by (fast_tac set_cs 1);
qed "notDomainE1";
val prems = goalw thy [Dom] "x~:D ==> ~y===x";
by (cut_facts_tac prems 1);
-by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);ba 1;
-bd sym2refl2 1;
+by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);by (assume_tac 1);
+by (dtac sym2refl2 1);
by (fast_tac set_cs 1);
qed "notDomainE2";
(* theorems for equivalence relations *)
goal thy "(x::'a::er) : D";
-br DomainI 1;
-br er_refl 1;
+by (rtac DomainI 1);
+by (rtac er_refl 1);
qed "er_Domain";
(* witnesses for "=>" ::(per,per)per *)
@@ -106,9 +106,9 @@
by (safe_tac HOL_cs);
by (REPEAT (dtac spec 1));
by (res_inst_tac [("y","g y")] per_trans 1);
-br mp 1;ba 1;
+by (rtac mp 1);by (assume_tac 1);
by (Asm_simp_tac 1);
-br mp 1;ba 1;
+by (rtac mp 1);by (assume_tac 1);
by (asm_simp_tac (!simpset addsimps [sym2refl2]) 1);
qed "per_trans_fun";
--- a/src/HOL/Subst/Subst.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Subst/Subst.ML Mon Jun 23 10:42:03 1997 +0200
@@ -25,7 +25,7 @@
goal Subst.thy "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s";
by (case_tac "t = Var(v)" 1);
-be rev_mp 2;
+by (etac rev_mp 2);
by (res_inst_tac [("P",
"%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")]
uterm.induct 2);
@@ -41,7 +41,7 @@
qed "agreement";
goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
-by(simp_tac (!simpset addsimps [agreement]
+by (simp_tac (!simpset addsimps [agreement]
setloop (split_tac [expand_if])) 1);
qed_spec_mp"repl_invariance";
--- a/src/HOL/Subst/Unifier.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Subst/Unifier.ML Mon Jun 23 10:42:03 1997 +0200
@@ -56,7 +56,7 @@
by (simp_tac(!simpset addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
delsimps [subst_Var]) 1);
by (Step_tac 1);
-br exI 1;
+by (rtac exI 1);
by (etac subst 1 THEN rtac (Cons_trivial RS subst_sym) 1);
by (etac ssubst_subst2 1);
by (asm_simp_tac (!simpset addsimps [Var_not_occs]) 1);
--- a/src/HOL/Trancl.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Trancl.ML Mon Jun 23 10:42:03 1997 +0200
@@ -195,16 +195,16 @@
qed "rtranclE2";
goal Trancl.thy "r O r^* = r^* O r";
-by(Step_tac 1);
- by(blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
-by(blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
+by (Step_tac 1);
+ by (blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
+by (blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
qed "r_comp_rtrancl_eq";
(**** The relation trancl ****)
goalw Trancl.thy [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+";
-by(blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1);
+by (blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1);
qed "trancl_mono";
(** Conversions between trancl and rtrancl **)
@@ -279,7 +279,7 @@
goalw Trancl.thy [trancl_def]
"!!r. [| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
-by(blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1);
+by (blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1);
qed "rtrancl_trancl_trancl";
val prems = goal Trancl.thy
@@ -291,22 +291,22 @@
(* primitive recursion for trancl over finite relations: *)
goal Trancl.thy "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
-br equalityI 1;
- br subsetI 1;
- by(split_all_tac 1);
- be trancl_induct 1;
- by(blast_tac (!claset addIs [r_into_trancl]) 1);
- by(blast_tac (!claset addIs
+by (rtac equalityI 1);
+ by (rtac subsetI 1);
+ by (split_all_tac 1);
+ by (etac trancl_induct 1);
+ by (blast_tac (!claset addIs [r_into_trancl]) 1);
+ by (blast_tac (!claset addIs
[rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
-br subsetI 1;
-by(blast_tac (!claset addIs
+by (rtac subsetI 1);
+by (blast_tac (!claset addIs
[rtrancl_into_trancl2, rtrancl_trancl_trancl,
impOfSubs rtrancl_mono, trancl_mono]) 1);
qed "trancl_insert";
goalw Trancl.thy [trancl_def] "(r^-1)^+ = (r^+)^-1";
-by(simp_tac (!simpset addsimps [rtrancl_inverse,inverse_comp]) 1);
-by(simp_tac (!simpset addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
+by (simp_tac (!simpset addsimps [rtrancl_inverse,inverse_comp]) 1);
+by (simp_tac (!simpset addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
qed "trancl_inverse";
--- a/src/HOL/WF.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/WF.ML Mon Jun 23 10:42:03 1997 +0200
@@ -107,23 +107,23 @@
*---------------------------------------------------------------------------*)
goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
-br iffI 1;
- by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
+by (rtac iffI 1);
+ by (blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
[rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
-by(asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
-by(safe_tac (!claset));
-by(EVERY1[rtac allE, atac, etac impE, Blast_tac]);
-be bexE 1;
-by(rename_tac "a" 1);
-by(case_tac "a = x" 1);
- by(res_inst_tac [("x","a")]bexI 2);
- ba 3;
- by(Blast_tac 2);
-by(case_tac "y:Q" 1);
- by(Blast_tac 2);
-by(res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
- ba 1;
-by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
+by (asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
+by (safe_tac (!claset));
+by (EVERY1[rtac allE, atac, etac impE, Blast_tac]);
+by (etac bexE 1);
+by (rename_tac "a" 1);
+by (case_tac "a = x" 1);
+ by (res_inst_tac [("x","a")]bexI 2);
+ by (assume_tac 3);
+ by (Blast_tac 2);
+by (case_tac "y:Q" 1);
+ by (Blast_tac 2);
+by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
+ by (assume_tac 1);
+by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
qed "wf_insert";
AddIffs [wf_insert];
@@ -131,18 +131,18 @@
goalw WF.thy [acyclic_def]
"!!r. wf r ==> acyclic r";
-by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
+by (blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
qed "wf_acyclic";
goalw WF.thy [acyclic_def]
"acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
-by(simp_tac (!simpset addsimps [trancl_insert]) 1);
-by(blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
+by (simp_tac (!simpset addsimps [trancl_insert]) 1);
+by (blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
qed "acyclic_insert";
AddIffs [acyclic_insert];
goalw WF.thy [acyclic_def] "acyclic(r^-1) = acyclic r";
-by(simp_tac (!simpset addsimps [trancl_inverse]) 1);
+by (simp_tac (!simpset addsimps [trancl_inverse]) 1);
qed "acyclic_inverse";
(** cut **)
--- a/src/HOL/WF_Rel.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/WF_Rel.ML Mon Jun 23 10:42:03 1997 +0200
@@ -106,14 +106,14 @@
*---------------------------------------------------------------------------*)
goal thy "!!r. finite r ==> acyclic r --> wf r";
-be finite_induct 1;
- by(Blast_tac 1);
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
+by (etac finite_induct 1);
+ by (Blast_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
qed_spec_mp "finite_acyclic_wf";
goal thy "!!r. finite r ==> wf r = acyclic r";
-by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
+by (blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
qed "wf_iff_acyclic_if_finite";
@@ -123,26 +123,26 @@
goalw thy [wf_eq_minimal RS eq_reflection]
"wf r = (~(? f. !i. (f(Suc i),f i) : r))";
-br iffI 1;
- br notI 1;
- be exE 1;
- by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
- by(Blast_tac 1);
-be swap 1;
+by (rtac iffI 1);
+ by (rtac notI 1);
+ by (etac exE 1);
+ by (eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
+ by (Blast_tac 1);
+by (etac swap 1);
by (Asm_full_simp_tac 1);
by (Step_tac 1);
-by(subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
+by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
- br allI 1;
- by(Simp_tac 1);
- br selectI2EX 1;
- by(Blast_tac 1);
- by(Blast_tac 1);
-br allI 1;
-by(induct_tac "n" 1);
- by(Asm_simp_tac 1);
-by(Simp_tac 1);
-br selectI2EX 1;
- by(Blast_tac 1);
-by(Blast_tac 1);
+ by (rtac allI 1);
+ by (Simp_tac 1);
+ by (rtac selectI2EX 1);
+ by (Blast_tac 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (rtac selectI2EX 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
qed "wf_iff_no_infinite_down_chain";
--- a/src/HOL/equalities.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/equalities.ML Mon Jun 23 10:42:03 1997 +0200
@@ -100,7 +100,7 @@
qed "image_id";
goal Set.thy "f``(range g) = range (%x. f (g x))";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "image_range";
qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
@@ -379,7 +379,7 @@
Addsimps[UN_empty];
goal Set.thy "(UN x:A. {}) = {}";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "UN_empty2";
Addsimps[UN_empty2];
@@ -635,7 +635,7 @@
goal Set.thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
by (Step_tac 1);
-be swap 1;
+by (etac swap 1);
by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
by (ALLGOALS Blast_tac);
qed "Pow_insert";
--- a/src/HOL/ex/Primes.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/ex/Primes.ML Mon Jun 23 10:42:03 1997 +0200
@@ -89,8 +89,8 @@
goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
by (Step_tac 1);
by (subgoal_tac "m = gcd(m*p, m*n)" 1);
-be ssubst 1;
-br gcd_greatest 1;
+by (etac ssubst 1);
+by (rtac gcd_greatest 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [gcd_mult_distrib2 RS sym])));
(*Now deduce gcd(p,n)=1 to finish the proof*)
by (cut_inst_tac [("m","p"),("n","n")] gcd_divides_both 1);
--- a/src/HOL/ex/Primrec.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/ex/Primrec.ML Mon Jun 23 10:42:03 1997 +0200
@@ -128,7 +128,7 @@
val lemma = result();
goal thy "!!i j k. i<j ==> ack(i,k) < ack(j,k)";
-be less_natE 1;
+by (etac less_natE 1);
by (blast_tac (!claset addSIs [lemma]) 1);
qed "ack_less_mono1";
@@ -248,8 +248,8 @@
"!!f g. [| ALL l. f l < ack(kf, list_add l); \
\ ALL l. g l < ack(kg, list_add l) \
\ |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";
-br exI 1;
-br allI 1;
+by (rtac exI 1);
+by (rtac allI 1);
by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1);
by (REPEAT (blast_tac (!claset addIs [ack_add_bound2]) 1));
qed "PREC_case";
--- a/src/HOLCF/IMP/Denotational.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IMP/Denotational.ML Mon Jun 23 10:42:03 1997 +0200
@@ -7,25 +7,25 @@
*)
goalw thy [dlift_def] "dlift f`(Def x) = f`(Discr x)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "dlift_Def";
Addsimps [dlift_Def];
goalw thy [dlift_def] "cont(%f. dlift f)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "cont_dlift";
AddIffs [cont_dlift];
goalw thy [dlift_def]
"(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
-by(simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
+by (simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
qed "dlift_is_Def";
Addsimps [dlift_is_Def];
goal thy "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
-be evalc.induct 1;
+by (etac evalc.induct 1);
by (ALLGOALS Asm_simp_tac);
- by (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
+ by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
qed_spec_mp "eval_implies_D";
goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
@@ -36,8 +36,8 @@
by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
by (Simp_tac 1);
-br fix_ind 1;
- by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
+by (rtac fix_ind 1);
+ by (fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
by (Simp_tac 1);
by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
by (safe_tac HOL_cs);
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Mon Jun 23 10:42:03 1997 +0200
@@ -32,7 +32,7 @@
goal thy
"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
- by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+ by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
qed "starts_of_par";
@@ -43,14 +43,14 @@
goal thy
"actions(asig_comp a b) = actions(a) Un actions(b)";
- by(simp_tac (!simpset addsimps
+ by (simp_tac (!simpset addsimps
([actions_def,asig_comp_def]@asig_projections)) 1);
by (fast_tac (set_cs addSIs [equalityI]) 1);
qed "actions_asig_comp";
goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
- by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+ by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
qed "asig_of_par";
@@ -90,7 +90,7 @@
goal thy"compatible A B = compatible B A";
by (asm_full_simp_tac (!simpset addsimps [compatible_def,Int_commute]) 1);
-auto();
+by (Auto_tac());
qed"compat_commute";
goalw thy [externals_def,actions_def,compatible_def]
@@ -167,21 +167,21 @@
goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
\ trans_of(restrict ioa acts) = trans_of(ioa)";
-by(simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
+by (simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
qed "cancel_restrict_a";
goal thy "reachable (restrict ioa acts) s = reachable ioa s";
by (rtac iffI 1);
-be reachable.induct 1;
-by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
+by (etac reachable.induct 1);
+by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
by (etac reachable_n 1);
-by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
(* <-- *)
-be reachable.induct 1;
+by (etac reachable.induct 1);
by (rtac reachable_0 1);
-by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
by (etac reachable_n 1);
-by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
qed "cancel_restrict_b";
goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
@@ -202,14 +202,14 @@
goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
-be reachable.induct 1;
-br reachable_0 1;
-by(asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
-bd trans_rename 1;
-be exE 1;
-be conjE 1;
-be reachable_n 1;
-ba 1;
+by (etac reachable.induct 1);
+by (rtac reachable_0 1);
+by (asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
+by (dtac trans_rename 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (etac reachable_n 1);
+by (assume_tac 1);
qed"reachable_rename";
@@ -282,7 +282,7 @@
\ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D) \
\ else snd(snd(snd(t)))=snd(snd(snd(s)))))";
- by(simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
+ by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
ioa_projections)
setloop (split_tac [expand_if])) 1);
qed "trans_of_par4";
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Mon Jun 23 10:42:03 1997 +0200
@@ -89,9 +89,9 @@
\ `x) \
\ ))";
by (rtac trans 1);
-br fix_eq2 1;
-br stutter2_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac stutter2_def 1);
+by (rtac beta_cfun 1);
by (simp_tac (!simpset addsimps [flift1_def]) 1);
qed"stutter2_unfold";
@@ -108,7 +108,7 @@
goal thy "(stutter2 A`(at>>xs)) s = \
\ ((if (fst at)~:act A then Def (s=snd at) else TT) \
\ andalso (stutter2 A`xs) (snd at))";
-br trans 1;
+by (rtac trans 1);
by (stac stutter2_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1);
by (Simp_tac 1);
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Mon Jun 23 10:42:03 1997 +0200
@@ -69,7 +69,7 @@
goal thy "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \
\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
\ (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
-br trans 1;
+by (rtac trans 1);
by (stac mkex2_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -78,7 +78,7 @@
goal thy "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
\ (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
-br trans 1;
+by (rtac trans 1);
by (stac mkex2_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -88,7 +88,7 @@
\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
\ (x,snd a,snd b) >> \
\ (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
-br trans 1;
+by (rtac trans 1);
by (stac mkex2_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -115,7 +115,7 @@
by (simp_tac (!simpset addsimps [mkex_def]
setloop (split_tac [expand_if]) ) 1);
by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
-auto();
+by (Auto_tac());
qed"mkex_cons_1";
goal thy "!!x.[| x~:act A; x:act B |] \
@@ -124,7 +124,7 @@
by (simp_tac (!simpset addsimps [mkex_def]
setloop (split_tac [expand_if]) ) 1);
by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
-auto();
+by (Auto_tac());
qed"mkex_cons_2";
goal thy "!!x.[| x:act A; x:act B |] \
@@ -133,7 +133,7 @@
by (simp_tac (!simpset addsimps [mkex_def]
setloop (split_tac [expand_if]) ) 1);
by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
-auto();
+by (Auto_tac());
qed"mkex_cons_3";
Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
@@ -289,8 +289,8 @@
by (cut_facts_tac [stutterA_mkex] 1);
by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
by (REPEAT (etac allE 1));
-bd mp 1;
-ba 2;
+by (dtac mp 1);
+by (assume_tac 2);
by (Asm_full_simp_tac 1);
qed"stutter_mkex_on_A";
@@ -320,8 +320,8 @@
by (cut_facts_tac [stutterB_mkex] 1);
by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
by (REPEAT (etac allE 1));
-bd mp 1;
-ba 2;
+by (dtac mp 1);
+by (assume_tac 2);
by (Asm_full_simp_tac 1);
qed"stutter_mkex_on_B";
@@ -380,11 +380,11 @@
by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
by (pair_tac "exA" 1);
by (pair_tac "exB" 1);
-br conjI 1;
+by (rtac conjI 1);
by (simp_tac (!simpset addsimps [mkex_def]) 1);
by (stac trick_against_eq_in_ass 1);
back();
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exA_tmp]) 1);
qed"filter_mkex_is_exA";
@@ -424,11 +424,11 @@
by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
by (pair_tac "exA" 1);
by (pair_tac "exB" 1);
-br conjI 1;
+by (rtac conjI 1);
by (simp_tac (!simpset addsimps [mkex_def]) 1);
by (stac trick_against_eq_in_ass 1);
back();
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exB_tmp]) 1);
qed"filter_mkex_is_exB";
@@ -473,7 +473,7 @@
lemma_2_1a,lemma_2_1b]) 1);
by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
by (pair_tac "ex" 1);
-be conjE 1;
+by (etac conjE 1);
by (asm_full_simp_tac (!simpset addsimps [sch_actions_in_AorB]) 1);
(* <== *)
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Jun 23 10:42:03 1997 +0200
@@ -65,7 +65,7 @@
\ (Takewhile (%a.a:int A)`schA) \
\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
\ `schB))";
-br trans 1;
+by (rtac trans 1);
by (stac mksch_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -76,7 +76,7 @@
\ (Takewhile (%a.a:int B)`schB) \
\ @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a.a:int B)`schB)) \
\ ))";
-br trans 1;
+by (rtac trans 1);
by (stac mksch_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -89,7 +89,7 @@
\ @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
\ `(TL`(Dropwhile (%a.a:int B)`schB)))) \
\ )";
-br trans 1;
+by (rtac trans 1);
by (stac mksch_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -136,13 +136,13 @@
(* Lemma for substitution of looping assumption in another specific assumption *)
val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
by (cut_facts_tac [p1] 1);
-be (p2 RS subst) 1;
+by (etac (p2 RS subst) 1);
qed"subst_lemma1";
(* Lemma for substitution of looping assumption in another specific assumption *)
val [p1,p2] = goal thy "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g";
by (cut_facts_tac [p1] 1);
-be (p2 RS subst) 1;
+by (etac (p2 RS subst) 1);
qed"subst_lemma2";
@@ -156,21 +156,21 @@
by (case_tac "a:act B" 1);
(* a:A, a:B *)
by (Asm_full_simp_tac 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
(* a:A,a~:B *)
by (Asm_full_simp_tac 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
by (case_tac "a:act B" 1);
(* a~:A, a:B *)
by (Asm_full_simp_tac 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
(* a~:A,a~:B *)
-auto();
+by (Auto_tac());
qed"ForallAorB_mksch1";
bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp);
@@ -181,7 +181,7 @@
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
by (safe_tac set_cs);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
intA_is_not_actB,int_is_act]) 1);
qed"ForallBnA_mksch";
@@ -196,7 +196,7 @@
by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
by (safe_tac set_cs);
by (Asm_full_simp_tac 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
intA_is_not_actB,int_is_act]) 1);
qed"ForallAnB_mksch";
@@ -214,7 +214,7 @@
\ Forall (%x. x:ext (A||B)) tr \
\ --> Finite (mksch A B`tr`x`y)";
-be Seq_Finite_ind 1;
+by (etac Seq_Finite_ind 1);
by (Asm_full_simp_tac 1);
(* main case *)
by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
@@ -231,10 +231,10 @@
(* now for conclusion IH applicable, but assumptions have to be transformed *)
by (dres_inst_tac [("x","x"),
("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
by (dres_inst_tac [("x","y"),
("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
(* IH *)
by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
@@ -249,7 +249,7 @@
(* now for conclusion IH applicable, but assumptions have to be transformed *)
by (dres_inst_tac [("x","y"),
("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
(* IH *)
by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
@@ -264,7 +264,7 @@
(* now for conclusion IH applicable, but assumptions have to be transformed *)
by (dres_inst_tac [("x","x"),
("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
(* IH *)
by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
@@ -290,7 +290,7 @@
\ Finite y1 & y = (y1 @@ y2) & \
\ Filter (%a. a:ext B)`y1 = bs)";
by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
-be Seq_Finite_ind 1;
+by (etac Seq_Finite_ind 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
by (res_inst_tac [("x","nil")] exI 1);
@@ -308,7 +308,7 @@
(* transform assumption f eB y = f B (s@z) *)
by (dres_inst_tac [("x","y"),
("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
Addsimps [FilterConc];
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
(* apply IH *)
@@ -345,7 +345,7 @@
\ Finite x1 & x = (x1 @@ x2) & \
\ Filter (%a. a:ext A)`x1 = as)";
by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
-be Seq_Finite_ind 1;
+by (etac Seq_Finite_ind 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
by (res_inst_tac [("x","nil")] exI 1);
@@ -363,7 +363,7 @@
(* transform assumption f eA x = f A (s@z) *)
by (dres_inst_tac [("x","x"),
("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
Addsimps [FilterConc];
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
(* apply IH *)
@@ -394,13 +394,13 @@
goal thy "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
\ y = z @@ mksch A B`tr`a`b\
\ --> Finite tr";
-be Seq_Finite_ind 1;
-auto();
+by (etac Seq_Finite_ind 1);
+by (Auto_tac());
by (Seq_case_simp_tac "tr" 1);
(* tr = UU *)
by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc]) 1);
(* tr = nil *)
-auto();
+by (Auto_tac());
(* tr = Conc *)
ren "s ss" 1;
@@ -419,7 +419,7 @@
by (Seq_case_simp_tac "tr" 1);
(* tr = UU *)
by (asm_full_simp_tac (!simpset addsimps [Conc_Conc_eq]) 1);
-auto();
+by (Auto_tac());
(* tr = nil ok *)
(* tr = Conc *)
by (Seq_case_simp_tac "z" 1);
@@ -452,19 +452,19 @@
goal thy "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))";
by (Seq_case_simp_tac "y" 1);
-auto();
+by (Auto_tac());
qed"Conc_Conc_eq";
goal thy "!! (y::'a Seq).Finite y ==> ~ y= x@@UU";
-be Seq_Finite_ind 1;
+by (etac Seq_Finite_ind 1);
by (Seq_case_simp_tac "x" 1);
by (Seq_case_simp_tac "x" 1);
-auto();
+by (Auto_tac());
qed"FiniteConcUU1";
goal thy "~ Finite ((x::'a Seq)@@UU)";
-br (FiniteConcUU1 COMP rev_contrapos) 1;
-auto();
+by (rtac (FiniteConcUU1 COMP rev_contrapos) 1);
+by (Auto_tac());
qed"FiniteConcUU";
finiteR_mksch
@@ -505,9 +505,9 @@
externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
(* conclusion of IH ok, but assumptions of IH have to be transformed *)
by (dres_inst_tac [("x","schA")] subst_lemma1 1);
-ba 1;
+by (assume_tac 1);
by (dres_inst_tac [("x","schB")] subst_lemma1 1);
-ba 1;
+by (assume_tac 1);
(* IH *)
by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
@@ -521,7 +521,7 @@
externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
by (dres_inst_tac [("x","schB")] subst_lemma1 1);
back();
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
(* Case a:A, a~:B *)
@@ -533,7 +533,7 @@
[FilterPTakewhileQnil,not_ext_is_int_or_not_act,
externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
by (dres_inst_tac [("x","schA")] subst_lemma1 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
(* Case a~:A, a~:B *)
@@ -614,8 +614,8 @@
(* eliminate the B-only prefix *)
by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
by (Fast_tac 2);
(* Now real recursive step follows (in y) *)
@@ -630,8 +630,8 @@
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
(* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
by (Fast_tac 2);
(* bring in divide Seq for s *)
@@ -643,15 +643,15 @@
back();
back();
back();
-ba 1;
+by (assume_tac 1);
(* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
+by (rtac take_reduction 1);
(* f A (tw iA) = tw ~eA *)
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
not_ext_is_int_or_not_act]) 1);
-br refl 1;
+by (rtac refl 1);
(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
(*
@@ -665,12 +665,12 @@
(* assumption schA *)
by (dres_inst_tac [("x","schA"),
("g","Filter (%a. a:act A)`s2")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil]) 1);
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
by (dres_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
FIX: problem: schA and schB are not quantified in the new take lemma version !!!
@@ -699,15 +699,15 @@
\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
by (strip_tac 1);
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
back();back();back();back();
by (res_inst_tac [("x","schA")] spec 1);
by (res_inst_tac [("x","schB")] spec 1);
by (res_inst_tac [("x","tr")] spec 1);
by (thin_tac' 5 1);
-br less_induct 1;
+by (rtac less_induct 1);
by (REPEAT (rtac allI 1));
ren "tr schB schA" 1;
by (strip_tac 1);
@@ -715,7 +715,7 @@
by (case_tac "Forall (%x. x:act B & x~:act A) tr" 1);
-br (seq_take_lemma RS iffD2 RS spec) 1;
+by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
by (thin_tac' 5 1);
@@ -731,7 +731,7 @@
by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
by (Asm_simp_tac 1);
by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPnil 1);
-ba 1;
+by (assume_tac 1);
by (Fast_tac 1);
(* case ~ Finite s *)
@@ -748,12 +748,12 @@
by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
by (Asm_simp_tac 1);
by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPUU 1);
-ba 1;
+by (assume_tac 1);
by (Fast_tac 1);
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
-bd divide_Seq3 1;
+by (dtac divide_Seq3 1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
@@ -772,8 +772,8 @@
(* eliminate the B-only prefix *)
by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
by (Fast_tac 2);
(* Now real recursive step follows (in y) *)
@@ -788,8 +788,8 @@
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
(* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
by (Fast_tac 2);
(* bring in divide Seq for s *)
@@ -801,15 +801,15 @@
back();
back();
back();
-ba 1;
+by (assume_tac 1);
(* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
+by (rtac take_reduction 1);
(* f A (tw iA) = tw ~eA *)
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
not_ext_is_int_or_not_act]) 1);
-br refl 1;
+by (rtac refl 1);
by (asm_full_simp_tac (!simpset addsimps [int_is_act,
not_ext_is_int_or_not_act]) 1);
by (rotate_tac ~11 1);
@@ -824,17 +824,17 @@
(* assumption schA *)
by (dres_inst_tac [("x","schA"),
("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
by (forw_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
(* assumption Forall schA *)
by (dres_inst_tac [("s","schA"),
("P","Forall (%x.x:act A)")] subst 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
@@ -847,8 +847,8 @@
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
(* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
by (Fast_tac 2);
(* bring in divide Seq for s *)
@@ -860,7 +860,7 @@
back();
back();
back();
-ba 1;
+by (assume_tac 1);
(* f A (tw iA) = tw ~eA *)
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
@@ -876,7 +876,7 @@
(* assumption schA *)
by (dres_inst_tac [("x","schA"),
("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
(* f A (tw iB schB2) = nil *)
@@ -885,22 +885,22 @@
(* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
-br refl 1;
-br refl 1;
+by (rtac take_reduction 1);
+by (rtac refl 1);
+by (rtac refl 1);
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
(* assumption schB *)
by (dres_inst_tac [("x","y2"),
("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
by (forw_inst_tac [("sch1.0","y1")] LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1);
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
@@ -941,15 +941,15 @@
\ --> Filter (%a.a:act B)`(mksch A B`tr`schA`schB) = schB";
by (strip_tac 1);
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
back();back();back();back();
by (res_inst_tac [("x","schA")] spec 1);
by (res_inst_tac [("x","schB")] spec 1);
by (res_inst_tac [("x","tr")] spec 1);
by (thin_tac' 5 1);
-br less_induct 1;
+by (rtac less_induct 1);
by (REPEAT (rtac allI 1));
ren "tr schB schA" 1;
by (strip_tac 1);
@@ -957,7 +957,7 @@
by (case_tac "Forall (%x. x:act A & x~:act B) tr" 1);
-br (seq_take_lemma RS iffD2 RS spec) 1;
+by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
by (thin_tac' 5 1);
@@ -973,7 +973,7 @@
by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
by (Asm_simp_tac 1);
by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPnil 1);
-ba 1;
+by (assume_tac 1);
by (Fast_tac 1);
(* case ~ Finite tr *)
@@ -990,12 +990,12 @@
by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
by (Asm_simp_tac 1);
by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPUU 1);
-ba 1;
+by (assume_tac 1);
by (Fast_tac 1);
(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
-bd divide_Seq3 1;
+by (dtac divide_Seq3 1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
@@ -1014,8 +1014,8 @@
(* eliminate the A-only prefix *)
by (subgoal_tac "(Filter (%a.a :act B)`x1) = nil" 1);
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
by (Fast_tac 2);
(* Now real recursive step follows (in x) *)
@@ -1030,8 +1030,8 @@
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
(* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
by (Fast_tac 2);
(* bring in divide Seq for s *)
@@ -1043,15 +1043,15 @@
back();
back();
back();
-ba 1;
+by (assume_tac 1);
(* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
+by (rtac take_reduction 1);
(* f B (tw iB) = tw ~eB *)
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
not_ext_is_int_or_not_act]) 1);
-br refl 1;
+by (rtac refl 1);
by (asm_full_simp_tac (!simpset addsimps [int_is_act,
not_ext_is_int_or_not_act]) 1);
by (rotate_tac ~11 1);
@@ -1066,17 +1066,17 @@
(* assumption schB *)
by (dres_inst_tac [("x","schB"),
("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
by (forw_inst_tac [("sch1.0","x1")] LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
(* assumption Forall schB *)
by (dres_inst_tac [("s","schB"),
("P","Forall (%x.x:act B)")] subst 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
(* case x:actions(asig_of A) & x: actions(asig_of B) *)
@@ -1089,8 +1089,8 @@
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
(* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
by (Fast_tac 2);
(* bring in divide Seq for s *)
@@ -1102,7 +1102,7 @@
back();
back();
back();
-ba 1;
+by (assume_tac 1);
(* f B (tw iB) = tw ~eB *)
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
@@ -1118,7 +1118,7 @@
(* assumption schA *)
by (dres_inst_tac [("x","schB"),
("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
(* f B (tw iA schA2) = nil *)
@@ -1127,22 +1127,22 @@
(* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
-br refl 1;
-br refl 1;
+by (rtac take_reduction 1);
+by (rtac refl 1);
+by (rtac refl 1);
(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
(* assumption schA *)
by (dres_inst_tac [("x","x2"),
("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *)
by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
by (forw_inst_tac [("sch1.0","x1")] LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1);
(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
@@ -1192,22 +1192,22 @@
by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
externals_of_par,ext1_ext2_is_not_act2]) 1);
(* Traces of A||B have only external actions from A or B *)
-br ForallPFilterP 1;
+by (rtac ForallPFilterP 1);
(* <== *)
(* replace schA and schB by Cut(schA) and Cut(schB) *)
by (dtac exists_LastActExtsch 1);
-ba 1;
+by (assume_tac 1);
by (dtac exists_LastActExtsch 1);
-ba 1;
+by (assume_tac 1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
(* Schedules of A(B) have only actions of A(B) *)
-bd scheds_in_sig 1;
-ba 1;
-bd scheds_in_sig 1;
-ba 1;
+by (dtac scheds_in_sig 1);
+by (assume_tac 1);
+by (dtac scheds_in_sig 1);
+by (assume_tac 1);
ren "h1 h2 schA schB" 1;
(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
@@ -1220,9 +1220,9 @@
(* mksch is a schedule -- use compositionality on sch-level *)
by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1);
by (asm_full_simp_tac (!simpset addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
-be ForallAorB_mksch 1;
-be ForallPForallQ 1;
-be ext_is_act 1;
+by (etac ForallAorB_mksch 1);
+by (etac ForallPForallQ 1);
+by (etac ext_is_act 1);
qed"compositionality_tr";
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Mon Jun 23 10:42:03 1997 +0200
@@ -9,16 +9,16 @@
goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
-auto();
+by (Auto_tac());
qed"compatibility_consequence3";
goal thy
"!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
-br ForallPFilterQR 1;
-ba 2;
-br compatibility_consequence3 1;
+by (rtac ForallPFilterQR 1);
+by (assume_tac 2);
+by (rtac compatibility_consequence3 1);
by (REPEAT (asm_full_simp_tac (!simpset
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
qed"Filter_actAisFilter_extA";
@@ -28,15 +28,15 @@
or even better A||B= B||A, FIX *)
goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
-auto();
+by (Auto_tac());
qed"compatibility_consequence4";
goal thy
"!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
-br ForallPFilterQR 1;
-ba 2;
-br compatibility_consequence4 1;
+by (rtac ForallPFilterQR 1);
+by (assume_tac 2);
+by (rtac compatibility_consequence4 1);
by (REPEAT (asm_full_simp_tac (!simpset
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
qed"Filter_actAisFilter_extA2";
@@ -73,11 +73,11 @@
(* 2 goals, the 3rd has been solved automatically *)
(* 1: Filter A2 x : traces A2 *)
by (dres_inst_tac [("A","traces A1")] subsetD 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA]) 1);
(* 2: Filter B2 x : traces B2 *)
by (dres_inst_tac [("A","traces B1")] subsetD 1);
-ba 1;
+by (assume_tac 1);
by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA2]) 1);
qed"compositionality";
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Mon Jun 23 10:42:03 1997 +0200
@@ -20,28 +20,28 @@
ren "sch s ex" 1;
by (subgoal_tac "Finite ex" 1);
by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 2);
-br (Map2Finite RS iffD1) 2;
+by (rtac (Map2Finite RS iffD1) 2);
by (res_inst_tac [("t","Map fst`ex")] subst 2);
-ba 2;
-be FiniteFilter 2;
+by (assume_tac 2);
+by (etac FiniteFilter 2);
(* subgoal 1 *)
by (forward_tac [exists_laststate] 1);
-be allE 1;
-be exE 1;
+by (etac allE 1);
+by (etac exE 1);
(* using input-enabledness *)
by (asm_full_simp_tac (!simpset addsimps [ioa_def,input_enabled_def]) 1);
by (REPEAT (etac conjE 1));
by (eres_inst_tac [("x","a")] allE 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","u")] allE 1);
-be exE 1;
+by (etac exE 1);
(* instantiate execution *)
by (res_inst_tac [("x","(s,ex @@ (a,s2)>>nil)")] exI 1);
by (asm_full_simp_tac (!simpset addsimps [filter_act_def,MapConc]) 1);
by (eres_inst_tac [("t","u")] lemma_2_1 1);
by (Asm_full_simp_tac 1);
-br sym 1;
-ba 1;
+by (rtac sym 1);
+by (assume_tac 1);
qed"scheds_input_enabled";
(********************************************************************************
@@ -56,18 +56,18 @@
\ ==> (sch @@ a>>nil) : schedules (A||B)";
by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
-br conjI 1;
+by (rtac conjI 1);
(* a : act (A||B) *)
by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 2);
-br disjI1 2;
-be disjE 2;
-be int_is_act 2;
-be out_is_act 2;
+by (rtac disjI1 2);
+by (etac disjE 2);
+by (etac int_is_act 2);
+by (etac out_is_act 2);
(* Filter B (sch@@[a]) : schedules B *)
by (case_tac "a:int A" 1);
-bd intA_is_not_actB 1;
-ba 1; (* --> a~:act B *)
+by (dtac intA_is_not_actB 1);
+by (assume_tac 1); (* --> a~:act B *)
by (Asm_full_simp_tac 1);
(* case a~:int A , i.e. a:out A *)
@@ -77,10 +77,10 @@
by (Asm_full_simp_tac 1);
by (subgoal_tac "a:out A" 1);
by (Fast_tac 2);
-bd outAactB_is_inpB 1;
-ba 1;
-ba 1;
-br scheds_input_enabled 1;
+by (dtac outAactB_is_inpB 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac scheds_input_enabled 1);
by (Asm_full_simp_tac 1);
by (REPEAT (atac 1));
qed"IOA_deadlock_free";
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Jun 23 10:42:03 1997 +0200
@@ -24,9 +24,9 @@
\ @@ ((corresp_exC A f `xs) (snd pr))) \
\ `x) ))";
by (rtac trans 1);
-br fix_eq2 1;
-br corresp_exC_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac corresp_exC_def 1);
+by (rtac beta_cfun 1);
by (simp_tac (!simpset addsimps [flift1_def]) 1);
qed"corresp_exC_unfold";
@@ -43,7 +43,7 @@
goal thy "(corresp_exC A f`(at>>xs)) s = \
\ (@cex. move A cex (f s) (fst at) (f (snd at))) \
\ @@ ((corresp_exC A f`xs) (snd at))";
-br trans 1;
+by (rtac trans 1);
by (stac corresp_exC_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
by (Simp_tac 1);
@@ -140,7 +140,7 @@
by (safe_tac set_cs);
by (asm_full_simp_tac (!simpset addsimps [mk_traceConc]) 1);
by (forward_tac [reachable.reachable_n] 1);
-ba 1;
+by (assume_tac 1);
by (eres_inst_tac [("x","y")] allE 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (!simpset addsimps [move_subprop4]
@@ -165,7 +165,7 @@
\ t = laststate (s,xs) \
\ --> is_exec_frag A (s,xs @@ ys))";
-br impI 1;
+by (rtac impI 1);
by (Seq_Finite_induct_tac 1);
(* base_case *)
by (fast_tac HOL_cs 1);
@@ -193,12 +193,12 @@
by (res_inst_tac [("t","f y")] lemma_2_1 1);
(* Finite *)
-be move_subprop2 1;
+by (etac move_subprop2 1);
by (REPEAT (atac 1));
by (rtac conjI 1);
(* is_exec_frag *)
-be move_subprop1 1;
+by (etac move_subprop1 1);
by (REPEAT (atac 1));
by (rtac conjI 1);
@@ -207,10 +207,10 @@
by (eres_inst_tac [("x","y")] allE 1);
by (Asm_full_simp_tac 1);
by (forward_tac [reachable.reachable_n] 1);
-ba 1;
+by (assume_tac 1);
by (Asm_full_simp_tac 1);
(* laststate *)
-be (move_subprop3 RS sym) 1;
+by (etac (move_subprop3 RS sym) 1);
by (REPEAT (atac 1));
qed"lemma_2";
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Jun 23 10:42:03 1997 +0200
@@ -25,8 +25,8 @@
by (case_tac "ex=nil" 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
-bd (Finite_Last1 RS mp) 1;
-ba 1;
+by (dtac (Finite_Last1 RS mp) 1);
+by (assume_tac 1);
by (def_tac 1);
qed"laststate_cons";
@@ -92,7 +92,7 @@
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by(fast_tac (!claset addDs prems) 1);
+ by (fast_tac (!claset addDs prems) 1);
qed "imp_conj_lemma";
goal thy "!!f.[| is_weak_ref_map f C A |]\
@@ -108,7 +108,7 @@
by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
asig_outputs_def,asig_of_def,trans_of_def]) 1);
by (safe_tac (!claset));
-by (rtac (expand_if RS ssubst) 1);
+by (stac expand_if 1);
by (rtac conjI 1);
by (rtac impI 1);
by (etac disjE 1);
--- a/src/HOLCF/IOA/meta_theory/Seq.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Mon Jun 23 10:42:03 1997 +0200
@@ -48,10 +48,10 @@
goal thy
"!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs";
-br trans 1;
+by (rtac trans 1);
by (stac smap_unfold 1);
by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
qed"smap_cons";
(* ----------------------------------------------------------- *)
@@ -76,10 +76,10 @@
goal thy
"!!x.x~=UU ==> sfilter`P`(x##xs)= \
\ (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
-br trans 1;
+by (rtac trans 1);
by (stac sfilter_unfold 1);
by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
qed"sfilter_cons";
(* ----------------------------------------------------------- *)
@@ -103,10 +103,10 @@
goal thy
"!!x.x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
-br trans 1;
+by (rtac trans 1);
by (stac sforall2_unfold 1);
by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
qed"sforall2_cons";
@@ -133,10 +133,10 @@
goal thy
"!!x.x~=UU ==> stakewhile`P`(x##xs) = \
\ (If P`x then x##(stakewhile`P`xs) else nil fi)";
-br trans 1;
+by (rtac trans 1);
by (stac stakewhile_unfold 1);
by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
qed"stakewhile_cons";
(* ----------------------------------------------------------- *)
@@ -162,10 +162,10 @@
goal thy
"!!x.x~=UU ==> sdropwhile`P`(x##xs) = \
\ (If P`x then sdropwhile`P`xs else x##xs fi)";
-br trans 1;
+by (rtac trans 1);
by (stac sdropwhile_unfold 1);
by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
qed"sdropwhile_cons";
@@ -192,10 +192,10 @@
goal thy
"!!x.x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
-br trans 1;
+by (rtac trans 1);
by (stac slast_unfold 1);
by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
qed"slast_cons";
@@ -220,7 +220,7 @@
qed"sconc_UU";
goal thy "(x##xs) @@ y=x##(xs @@ y)";
-br trans 1;
+by (rtac trans 1);
by (stac sconc_unfold 1);
by (Asm_full_simp_tac 1);
by (case_tac "x=UU" 1);
@@ -250,7 +250,7 @@
qed"sflat_UU";
goal thy "sflat`(x##xs)= x@@(sflat`xs)";
-br trans 1;
+by (rtac trans 1);
by (stac sflat_unfold 1);
by (Asm_full_simp_tac 1);
by (case_tac "x=UU" 1);
@@ -289,13 +289,13 @@
qed"szip_UU2";
goal thy "!!x.x~=UU ==> szip`(x##xs)`nil=UU";
-br trans 1;
+by (rtac trans 1);
by (stac szip_unfold 1);
by (REPEAT (Asm_full_simp_tac 1));
qed"szip_cons_nil";
goal thy "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
-br trans 1;
+by (rtac trans 1);
by (stac szip_unfold 1);
by (REPEAT (Asm_full_simp_tac 1));
qed"szip_cons";
@@ -320,7 +320,7 @@
"!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
by (rtac iffI 1);
by (etac (hd seq.injects) 1);
-auto();
+by (Auto_tac());
qed"scons_inject_eq";
goal thy "!!x. nil<<x ==> nil=x";
@@ -399,8 +399,8 @@
(* ---------------------------------------------------- *)
goal thy "Finite x --> x~=UU";
-br impI 1;
-be sfinite.induct 1;
+by (rtac impI 1);
+by (etac sfinite.induct 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed"Finite_UU_a";
@@ -412,7 +412,7 @@
goal thy "Finite x --> a~=UU --> x=a##xs --> Finite xs";
by (strip_tac 1);
-be sfinite.elim 1;
+by (etac sfinite.elim 1);
by (fast_tac (HOL_cs addss !simpset) 1);
by (fast_tac (HOL_cs addSDs seq.injects) 1);
qed"Finite_cons_a";
@@ -454,8 +454,8 @@
\ !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
\ |] ==> seq_finite(s) --> P(s)";
by (rtac seq_finite_ind_lemma 1);
-be seq.finite_ind 1;
- ba 1;
+by (etac seq.finite_ind 1);
+ by (assume_tac 1);
by (Asm_full_simp_tac 1);
qed"seq_finite_ind";
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Jun 23 10:42:03 1997 +0200
@@ -13,8 +13,8 @@
\ ==> adm (%x. P x = Q x)";
by (res_inst_tac [("P2","(%x.(P x --> Q x) & (Q x --> P x))")] (adm_cong RS iffD1) 1);
by (Fast_tac 1);
-be adm_conj 1;
-ba 1;
+by (etac adm_conj 1);
+by (assume_tac 1);
qed"adm_iff";
Addsimps [adm_iff];
@@ -169,9 +169,9 @@
\ Undef => UU \
\ | Def b => Def (a,b)##(Zip`xs`ys)))))";
by (rtac trans 1);
-br fix_eq2 1;
-br Zip_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac Zip_def 1);
+by (rtac beta_cfun 1);
by (Simp_tac 1);
qed"Zip_unfold";
@@ -198,7 +198,7 @@
qed"Zip_cons_nil";
goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys";
-br trans 1;
+by (rtac trans 1);
by (stac Zip_unfold 1);
by (Simp_tac 1);
(* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not
@@ -236,9 +236,9 @@
\ | x##xs => (case x of Undef => UU | Def y => \
\ (if P y then y>>(Filter2 P`xs) else Filter2 P`xs)))";
by (rtac trans 1);
-br fix_eq2 1;
-br Filter2_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac Filter2_def 1);
+by (rtac beta_cfun 1);
by (Simp_tac 1);
is also possible, if then else has to be proven continuous and it would be nice if a case for
@@ -265,9 +265,9 @@
goal thy "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s ==> P |] ==> P";
by (cut_inst_tac [("x","x")] Seq_exhaust 1);
-be disjE 1;
+by (etac disjE 1);
by (Asm_full_simp_tac 1);
-be disjE 1;
+by (etac disjE 1);
by (Asm_full_simp_tac 1);
by (REPEAT (etac exE 1));
by (Asm_full_simp_tac 1);
@@ -284,7 +284,7 @@
goal thy "a>>s ~= UU";
by (stac Cons_def2 1);
by (resolve_tac seq.con_rews 1);
-br Def_not_UU 1;
+by (rtac Def_not_UU 1);
qed"Cons_not_UU";
@@ -298,7 +298,7 @@
goal thy "~a>>s << nil";
by (stac Cons_def2 1);
by (resolve_tac seq.rews 1);
-br Def_not_UU 1;
+by (rtac Def_not_UU 1);
qed"Cons_not_less_nil";
goal thy "a>>s ~= nil";
@@ -353,7 +353,7 @@
section "induction";
goal thy "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
-be seq.ind 1;
+by (etac seq.ind 1);
by (REPEAT (atac 1));
by (def_tac 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -361,15 +361,15 @@
goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |] \
\ ==> seq_finite x --> P x";
-be seq_finite_ind 1;
+by (etac seq_finite_ind 1);
by (REPEAT (atac 1));
by (def_tac 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
qed"Seq_FinitePartial_ind";
goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
-be sfinite.induct 1;
-ba 1;
+by (etac sfinite.induct 1);
+by (assume_tac 1);
by (def_tac 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
qed"Seq_Finite_ind";
@@ -442,10 +442,10 @@
goal thy "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
by (rtac iffI 1);
-be (FiniteConc_2 RS spec RS spec RS mp) 1;
-br refl 1;
-br (FiniteConc_1 RS mp) 1;
-auto();
+by (etac (FiniteConc_2 RS spec RS spec RS mp) 1);
+by (rtac refl 1);
+by (rtac (FiniteConc_1 RS mp) 1);
+by (Auto_tac());
qed"FiniteConc";
Addsimps [FiniteConc];
@@ -461,16 +461,16 @@
by (Seq_case_simp_tac "t" 1);
by (Asm_full_simp_tac 1);
(* main case *)
-auto();
+by (Auto_tac());
by (Seq_case_simp_tac "t" 1);
by (Asm_full_simp_tac 1);
qed"FiniteMap2";
goal thy "Finite (Map f`s) = Finite s";
-auto();
-be (FiniteMap2 RS spec RS mp) 1;
-br refl 1;
-be FiniteMap1 1;
+by (Auto_tac());
+by (etac (FiniteMap2 RS spec RS mp) 1);
+by (rtac refl 1);
+by (etac FiniteMap1 1);
qed"Map2Finite";
@@ -492,27 +492,27 @@
goal thy "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y";
by (Seq_Finite_induct_tac 1);
by (strip_tac 1);
-be conjE 1;
-be nil_less_is_nil 1;
+by (etac conjE 1);
+by (etac nil_less_is_nil 1);
(* main case *)
-auto();
+by (Auto_tac());
by (Seq_case_simp_tac "y" 1);
-auto();
+by (Auto_tac());
qed_spec_mp"Finite_flat";
goal thy "adm(%(x:: 'a Seq).Finite x)";
-br admI 1;
+by (rtac admI 1);
by (eres_inst_tac [("x","0")] allE 1);
back();
-be exE 1;
+by (etac exE 1);
by (REPEAT (etac conjE 1));
by (res_inst_tac [("x","0")] allE 1);
-ba 1;
+by (assume_tac 1);
by (eres_inst_tac [("x","j")] allE 1);
by (cut_inst_tac [("x","Y 0"),("y","Y j")] Finite_flat 1);
(* Generates a contradiction in subgoal 3 *)
-auto();
+by (Auto_tac());
qed"adm_Finite";
Addsimps [adm_Finite];
@@ -543,12 +543,12 @@
(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
goal thy "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
by (Seq_case_simp_tac "x" 1);
-auto();
+by (Auto_tac());
qed"nil_is_Conc";
goal thy "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
by (Seq_case_simp_tac "x" 1);
-auto();
+by (Auto_tac());
qed"nil_is_Conc2";
@@ -655,14 +655,14 @@
by (strip_tac 1);
by (Seq_case_simp_tac "sa" 1);
by (Asm_full_simp_tac 1);
-auto();
+by (Auto_tac());
qed"Forall_prefix";
bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
goal thy "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
-auto();
+by (Auto_tac());
qed"Forall_postfixclosed";
@@ -715,7 +715,7 @@
by (res_inst_tac[("x","ys")] Seq_induct 1);
(* adm *)
(* FIX: not admissible, search other proof!! *)
-br adm_all 1;
+by (rtac adm_all 1);
(* base cases *)
by (Simp_tac 1);
by (Simp_tac 1);
@@ -741,23 +741,23 @@
\ (Forall (%x. ~P x) ys & ~Finite ys)";
by (rtac conjI 1);
by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
-auto();
+by (Auto_tac());
by (blast_tac (!claset addSDs [FilterUU_nFinite_lemma1]) 1);
qed"FilternPUUForallP";
goal thy "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
\ ==> Filter P`ys = nil";
-be ForallnPFilterPnil 1;
-be ForallPForallQ 1;
-auto();
+by (etac ForallnPFilterPnil 1);
+by (etac ForallPForallQ 1);
+by (Auto_tac());
qed"ForallQFilterPnil";
goal thy "!! Q P. [| ~Finite ys; Forall Q ys; !!x. Q x ==> ~P x|] \
\ ==> Filter P`ys = UU ";
-be ForallnPFilterPUU 1;
-be ForallPForallQ 1;
-auto();
+by (etac ForallnPFilterPUU 1);
+by (etac ForallPForallQ 1);
+by (Auto_tac());
qed"ForallQFilterPUU";
@@ -773,26 +773,26 @@
goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
-br ForallPForallQ 1;
-br ForallPTakewhileP 1;
-auto();
+by (rtac ForallPForallQ 1);
+by (rtac ForallPTakewhileP 1);
+by (Auto_tac());
qed"ForallPTakewhileQ";
goal thy "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
\ ==> Filter P`(Takewhile Q`ys) = nil";
-be ForallnPFilterPnil 1;
-br ForallPForallQ 1;
-br ForallPTakewhileP 1;
-auto();
+by (etac ForallnPFilterPnil 1);
+by (rtac ForallPForallQ 1);
+by (rtac ForallPTakewhileP 1);
+by (Auto_tac());
qed"FilterPTakewhileQnil";
goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
\ Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)";
-br ForallPFilterPid 1;
-br ForallPForallQ 1;
-br ForallPTakewhileP 1;
-auto();
+by (rtac ForallPFilterPid 1);
+by (rtac ForallPForallQ 1);
+by (rtac ForallPTakewhileP 1);
+by (Auto_tac());
qed"FilterPTakewhileQid";
Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
@@ -840,26 +840,26 @@
(* FIX: pay attention: is only admissible with chain-finite package to be added to
adm test *)
by (Seq_induct_tac "y" [] 1);
-br adm_all 1;
+by (rtac adm_all 1);
by (Asm_full_simp_tac 1);
by (case_tac "P a" 1);
by (Asm_full_simp_tac 1);
-br impI 1;
+by (rtac impI 1);
by (hyp_subst_tac 1);
by (Asm_full_simp_tac 1);
(* ~ P a *)
by (Asm_full_simp_tac 1);
-br impI 1;
+by (rtac impI 1);
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
by (REPEAT (etac conjE 1));
-ba 1;
+by (assume_tac 1);
qed"divide_Seq_lemma";
goal thy "!! x. (x>>xs) << Filter P`y \
\ ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
\ & Finite (Takewhile (%a. ~ P a)`y) & P x";
-br (divide_Seq_lemma RS mp) 1;
+by (rtac (divide_Seq_lemma RS mp) 1);
by (dres_inst_tac [("fo","HD"),("xa","x>>xs")] monofun_cfun_arg 1);
by (Asm_full_simp_tac 1);
qed"divide_Seq";
@@ -869,7 +869,7 @@
(* FIX: pay attention: is only admissible with chain-finite package to be added to
adm test *)
by (Seq_induct_tac "y" [] 1);
-br adm_all 1;
+by (rtac adm_all 1);
by (case_tac "P a" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
@@ -879,18 +879,18 @@
goal thy "!!y. ~Forall P y \
\ ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
\ Finite (Takewhile P`y) & (~ P x)";
-bd (nForall_HDFilter RS mp) 1;
+by (dtac (nForall_HDFilter RS mp) 1);
by (safe_tac set_cs);
by (res_inst_tac [("x","x")] exI 1);
by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
-auto();
+by (Auto_tac());
qed"divide_Seq2";
goal thy "!! y. ~Forall P y \
\ ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
by (cut_inst_tac [] divide_Seq2 1);
-auto();
+by (Auto_tac());
qed"divide_Seq3";
Addsimps [FilterPQ,FilterConc,Conc_cong];
@@ -903,8 +903,8 @@
goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
by (rtac iffI 1);
-br seq.take_lemma 1;
-auto();
+by (rtac seq.take_lemma 1);
+by (Auto_tac());
qed"seq_take_lemma";
goal thy
@@ -913,9 +913,9 @@
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
by (res_inst_tac [("n","n")] natE 1);
-auto();
+by (Auto_tac());
by (res_inst_tac [("n","n")] natE 1);
-auto();
+by (Auto_tac());
qed"take_reduction1";
@@ -935,9 +935,9 @@
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
by (res_inst_tac [("n","n")] natE 1);
-auto();
+by (Auto_tac());
by (res_inst_tac [("n","n")] natE 1);
-auto();
+by (Auto_tac());
qed"take_reduction_less1";
@@ -953,9 +953,9 @@
by (res_inst_tac [("t","s1")] (seq.reach RS subst) 1);
by (res_inst_tac [("t","s2")] (seq.reach RS subst) 1);
by (rtac (fix_def2 RS ssubst ) 1);
-by (rtac (contlub_cfun_fun RS ssubst) 1);
+by (stac contlub_cfun_fun 1);
by (rtac is_chain_iterate 1);
-by (rtac (contlub_cfun_fun RS ssubst) 1);
+by (stac contlub_cfun_fun 1);
by (rtac is_chain_iterate 1);
by (rtac lub_mono 1);
by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
@@ -967,9 +967,9 @@
goal thy "(!n. seq_take n`x << seq_take n`x') = (x << x')";
by (rtac iffI 1);
-br take_lemma_less1 1;
-auto();
-be monofun_cfun_arg 1;
+by (rtac take_lemma_less1 1);
+by (Auto_tac());
+by (etac monofun_cfun_arg 1);
qed"take_lemma_less";
(* ------------------------------------------------------------------
@@ -991,8 +991,8 @@
\ ==> A x --> (f x)=(g x)";
by (case_tac "Forall Q x" 1);
by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
-br seq.take_lemma 1;
-auto();
+by (rtac seq.take_lemma 1);
+by (Auto_tac());
qed"take_lemma_principle2";
@@ -1011,14 +1011,14 @@
\ ==> seq_take (Suc n)`(f (s1 @@ y>>s2)) \
\ = seq_take (Suc n)`(g (s1 @@ y>>s2)) |] \
\ ==> A x --> (f x)=(g x)";
-br impI 1;
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac impI 1);
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
by (res_inst_tac [("x","x")] spec 1);
-br nat_induct 1;
+by (rtac nat_induct 1);
by (Simp_tac 1);
-br allI 1;
+by (rtac allI 1);
by (case_tac "Forall Q xa" 1);
by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
!simpset)) 1);
@@ -1033,13 +1033,13 @@
\ ==> seq_take n`(f (s1 @@ y>>s2)) \
\ = seq_take n`(g (s1 @@ y>>s2)) |] \
\ ==> A x --> (f x)=(g x)";
-br impI 1;
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac impI 1);
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
by (res_inst_tac [("x","x")] spec 1);
-br less_induct 1;
-br allI 1;
+by (rtac less_induct 1);
+by (rtac allI 1);
by (case_tac "Forall Q xa" 1);
by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
!simpset)) 1);
@@ -1057,14 +1057,14 @@
\ = seq_take n`(g (s1 @@ y>>s2) h1 h2) |] \
\ ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
by (strip_tac 1);
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
by (res_inst_tac [("x","h2a")] spec 1);
by (res_inst_tac [("x","h1a")] spec 1);
by (res_inst_tac [("x","x")] spec 1);
-br less_induct 1;
-br allI 1;
+by (rtac less_induct 1);
+by (rtac allI 1);
by (case_tac "Forall Q xa" 1);
by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
!simpset)) 1);
@@ -1083,15 +1083,15 @@
by (res_inst_tac [("t","f x = g x"),
("s","!n. seq_take n`(f x) = seq_take n`(g x)")] subst 1);
-br seq_take_lemma 1;
+by (rtac seq_take_lemma 1);
wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden.....
FIX
-br less_induct 1;
-br allI 1;
+by (rtac less_induct 1);
+by (rtac allI 1);
by (case_tac "Forall Q xa" 1);
by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
!simpset)) 1);
@@ -1110,14 +1110,14 @@
\ ==> seq_take (Suc n)`(f (y>>s)) \
\ = seq_take (Suc n)`(g (y>>s)) |] \
\ ==> A x --> (f x)=(g x)";
-br impI 1;
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac impI 1);
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
by (res_inst_tac [("x","x")] spec 1);
-br nat_induct 1;
+by (rtac nat_induct 1);
by (Simp_tac 1);
-br allI 1;
+by (rtac allI 1);
by (Seq_case_simp_tac "xa" 1);
qed"take_lemma_in_eq_out";
@@ -1181,7 +1181,7 @@
goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
-auto();
+by (Auto_tac());
qed"MapConc_takelemma";
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Mon Jun 23 10:42:03 1997 +0200
@@ -47,7 +47,7 @@
goal thy "oraclebuild P`s`(x>>t) = \
\ (Takewhile (%a.~ P a)`s) \
\ @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";
-br trans 1;
+by (rtac trans 1);
by (stac oraclebuild_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -65,7 +65,7 @@
\ ==> Cut P s =nil";
by (subgoal_tac "Filter P`s = nil" 1);
by (asm_simp_tac (!simpset addsimps [oraclebuild_nil]) 1);
-br ForallQFilterPnil 1;
+by (rtac ForallQFilterPnil 1);
by (REPEAT (atac 1));
qed"Cut_nil";
@@ -74,7 +74,7 @@
\ ==> Cut P s =UU";
by (subgoal_tac "Filter P`s= UU" 1);
by (asm_simp_tac (!simpset addsimps [oraclebuild_UU]) 1);
-br ForallQFilterPUU 1;
+by (rtac ForallQFilterPUU 1);
by (REPEAT (atac 1));
qed"Cut_UU";
@@ -106,7 +106,7 @@
ForallQFilterPUU]) 1);
(* main case *)
by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
-auto();
+by (Auto_tac());
qed"FilterCut";
@@ -123,8 +123,8 @@
ForallQFilterPUU]) 1);
(* main case *)
by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
-br take_reduction 1;
-auto();
+by (rtac take_reduction 1);
+by (Auto_tac());
qed"Cut_idemp";
@@ -136,45 +136,45 @@
by (Fast_tac 3);
by (case_tac "Finite s" 1);
by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1);
-br (Cut_nil RS sym) 1;
+by (rtac (Cut_nil RS sym) 1);
by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1);
by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
(* csae ~ Finite s *)
by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
-br (Cut_UU RS sym) 1;
+by (rtac (Cut_UU RS sym) 1);
by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1);
by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
(* main case *)
by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,MapConc,
ForallMap,FiniteMap1,o_def]) 1);
-br take_reduction 1;
-auto();
+by (rtac take_reduction 1);
+by (Auto_tac());
qed"MapCut";
goal thy "~Finite s --> Cut P s << s";
by (strip_tac 1);
-br (take_lemma_less RS iffD1) 1;
+by (rtac (take_lemma_less RS iffD1) 1);
by (strip_tac 1);
-br mp 1;
-ba 2;
+by (rtac mp 1);
+by (assume_tac 2);
by (thin_tac' 1 1);
by (res_inst_tac [("x","s")] spec 1);
-br less_induct 1;
+by (rtac less_induct 1);
by (strip_tac 1);
ren "na n s" 1;
by (case_tac "Forall (%x. ~ P x) s" 1);
-br (take_lemma_less RS iffD2 RS spec) 1;
+by (rtac (take_lemma_less RS iffD2 RS spec) 1);
by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
(* main case *)
-bd divide_Seq3 1;
+by (dtac divide_Seq3 1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
by (hyp_subst_tac 1);
by (asm_full_simp_tac (!simpset addsimps [Cut_Cons]) 1);
-br take_reduction_less 1;
+by (rtac take_reduction_less 1);
(* auto makes also reasoning about Finiteness of parts of s ! *)
-auto();
+by (Auto_tac());
qed_spec_mp"Cut_prefixcl_nFinite";
@@ -184,24 +184,24 @@
goal thy "Finite s --> (? y. s = Cut P s @@ y)";
by (strip_tac 1);
by (rtac exI 1);
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
by (thin_tac' 1 1);
by (res_inst_tac [("x","s")] spec 1);
-br less_induct 1;
+by (rtac less_induct 1);
by (strip_tac 1);
ren "na n s" 1;
by (case_tac "Forall (%x. ~ P x) s" 1);
-br (seq_take_lemma RS iffD2 RS spec) 1;
+by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1);
(* main case *)
-bd divide_Seq3 1;
+by (dtac divide_Seq3 1);
by (REPEAT (etac exE 1));
by (REPEAT (etac conjE 1));
by (hyp_subst_tac 1);
by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,Conc_assoc]) 1);
-br take_reduction 1;
+by (rtac take_reduction 1);
qed_spec_mp"Cut_prefixcl_Finite";
@@ -212,13 +212,13 @@
goal thy "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)";
by (case_tac "Finite ex" 1);
by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1);
-ba 1;
-be exE 1;
-br exec_prefix2closed 1;
+by (assume_tac 1);
+by (etac exE 1);
+by (rtac exec_prefix2closed 1);
by (eres_inst_tac [("s","ex"),("t","Cut P ex @@ y")] subst 1);
-ba 1;
-be exec_prefixclosed 1;
-be Cut_prefixcl_nFinite 1;
+by (assume_tac 1);
+by (etac exec_prefixclosed 1);
+by (etac Cut_prefixcl_nFinite 1);
qed"execThruCut";
@@ -251,14 +251,14 @@
by (simp_tac (!simpset addsimps [filter_act_def]) 1);
by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
-br (rewrite_rule [o_def] MapCut) 2;
+by (rtac (rewrite_rule [o_def] MapCut) 2);
by (asm_full_simp_tac (!simpset addsimps [FilterCut RS sym]) 1);
(* Subgoal 3: Lemma: Cut idempotent *)
by (simp_tac (!simpset addsimps [LastActExtsch_def,filter_act_def]) 1);
by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
-br (rewrite_rule [o_def] MapCut) 2;
+by (rtac (rewrite_rule [o_def] MapCut) 2);
by (asm_full_simp_tac (!simpset addsimps [Cut_idemp]) 1);
qed"exists_LastActExtsch";
@@ -270,19 +270,19 @@
goalw thy [LastActExtsch_def]
"!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = nil |] \
\ ==> sch=nil";
-bd FilternPnilForallP 1;
-be conjE 1;
-bd Cut_nil 1;
-ba 1;
+by (dtac FilternPnilForallP 1);
+by (etac conjE 1);
+by (dtac Cut_nil 1);
+by (assume_tac 1);
by (Asm_full_simp_tac 1);
qed"LastActExtimplnil";
goalw thy [LastActExtsch_def]
"!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = UU |] \
\ ==> sch=UU";
-bd FilternPUUForallP 1;
-be conjE 1;
-bd Cut_UU 1;
-ba 1;
+by (dtac FilternPUUForallP 1);
+by (etac conjE 1);
+by (dtac Cut_UU 1);
+by (assume_tac 1);
by (Asm_full_simp_tac 1);
qed"LastActExtimplUU";
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Mon Jun 23 10:42:03 1997 +0200
@@ -71,9 +71,9 @@
\ `x) \
\ ))";
by (rtac trans 1);
-br fix_eq2 1;
-br is_exec_fragC_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac is_exec_fragC_def 1);
+by (rtac beta_cfun 1);
by (simp_tac (!simpset addsimps [flift1_def]) 1);
qed"is_exec_fragC_unfold";
@@ -90,7 +90,7 @@
goal thy "(is_exec_fragC A`(pr>>xs)) s = \
\ (Def ((s,pr):trans_of A) \
\ andalso (is_exec_fragC A`xs)(snd pr))";
-br trans 1;
+by (rtac trans 1);
by (stac is_exec_fragC_unfold 1);
by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
by (Simp_tac 1);
@@ -178,8 +178,8 @@
by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
by (pair_tac "x" 1);
-br (execfrag_in_sig RS spec RS mp) 1;
-auto();
+by (rtac (execfrag_in_sig RS spec RS mp) 1);
+by (Auto_tac());
qed"exec_in_sig";
goalw thy [schedules_def,has_schedule_def]
@@ -200,7 +200,7 @@
by (strip_tac 1);
by (Seq_case_simp_tac "xa" 1);
by (pair_tac "a" 1);
-auto();
+by (Auto_tac());
qed"execfrag_prefixclosed";
bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
@@ -213,6 +213,6 @@
by (strip_tac 1);
by (Seq_case_simp_tac "s" 1);
by (pair_tac "a" 1);
-auto();
+by (Auto_tac());
qed_spec_mp"exec_prefix2closed";
--- a/src/HOLCF/Lift.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/Lift.ML Mon Jun 23 10:42:03 1997 +0200
@@ -8,7 +8,7 @@
(* flift1 is continuous in its argument itself*)
goal thy "cont (lift_case UU f)";
-br flatdom_strict2cont 1;
+by (rtac flatdom_strict2cont 1);
by (Simp_tac 1);
qed"cont_flift1_arg";
@@ -17,7 +17,7 @@
goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
\ cont (%y. lift_case UU (f y))";
-br cont2cont_CF1L_rev 1;
+by (rtac cont2cont_CF1L_rev 1);
by (strip_tac 1);
by (res_inst_tac [("x","y")] Lift_cases 1);
by (Asm_simp_tac 1);
@@ -29,18 +29,18 @@
goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
\ cont (%y. lift_case UU (f y) (g y))";
-br cont2cont_app 1;
+by (rtac cont2cont_app 1);
back();
by (safe_tac set_cs);
-br cont_flift1_not_arg 1;
-auto();
-br cont_flift1_arg 1;
+by (rtac cont_flift1_not_arg 1);
+by (Auto_tac());
+by (rtac cont_flift1_arg 1);
qed"cont_flift1_arg_and_not_arg";
(* flift2 is continuous in its argument itself *)
goal thy "cont (lift_case UU (%y. Def (f y)))";
-br flatdom_strict2cont 1;
+by (rtac flatdom_strict2cont 1);
by (Simp_tac 1);
qed"cont_flift2_arg";
--- a/src/HOLCF/Lift3.ML Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/Lift3.ML Mon Jun 23 10:42:03 1997 +0200
@@ -71,7 +71,7 @@
(* --------------------------------------------------------*)
goal thy "(x::'a lift) << y = (x=y | x=UU)";
-br (inst_lift_po RS ssubst) 1;
+by (stac inst_lift_po 1);
by (Simp_tac 1);
qed"less_lift";
@@ -96,13 +96,13 @@
goal thy
"P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))";
-by(lift.induct_tac "x" 1);
-by(ALLGOALS Asm_simp_tac);
+by (lift.induct_tac "x" 1);
+by (ALLGOALS Asm_simp_tac);
qed "expand_lift_case";
goal thy "(x~=UU)=(? y.x=Def y)";
-br iffI 1;
-br Lift_cases 1;
+by (rtac iffI 1);
+by (rtac Lift_cases 1);
by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
qed"not_Undef_is_Def";
@@ -126,7 +126,7 @@
back();
by (rtac iffI 1);
by (asm_full_simp_tac (!simpset addsimps [inst_lift_po] ) 1);
-be (antisym_less_inverse RS conjunct1) 1;
+by (etac (antisym_less_inverse RS conjunct1) 1);
qed"Def_inject_less_eq";
goal thy "Def x << y = (Def x = y)";
@@ -146,15 +146,15 @@
(* Two specific lemmas for the combination of LCF and HOL terms *)
goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
-br cont2cont_CF1L 1;
+by (rtac cont2cont_CF1L 1);
by (REPEAT (resolve_tac cont_lemmas1 1));
-auto();
+by (Auto_tac());
qed"cont_fapp_app";
goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
-br cont2cont_CF1L 1;
-be cont_fapp_app 1;
-ba 1;
+by (rtac cont2cont_CF1L 1);
+by (etac cont_fapp_app 1);
+by (assume_tac 1);
qed"cont_fapp_app_app";