--- a/src/HOL/IOA/IOA.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/IOA/IOA.ML Sun Jul 12 11:49:17 1998 +0200
@@ -56,7 +56,7 @@
"!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
by (asm_full_simp_tac (simpset() delsimps bex_simps) 1);
by (split_all_tac 1);
- by (Safe_tac);
+ by Safe_tac;
by (rename_tac "ex1 ex2 n" 1);
by (res_inst_tac [("x","(%i. if i<n then ex1 i \
\ else (if i=n then Some a else None), \
@@ -79,7 +79,7 @@
\ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
\ ==> invariant A P";
by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
- by (Safe_tac);
+ by Safe_tac;
by (rename_tac "ex1 ex2 n" 1);
by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1);
by (Asm_full_simp_tac 1);
--- a/src/HOL/IOA/Solve.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/IOA/Solve.ML Sun Jul 12 11:49:17 1998 +0200
@@ -15,7 +15,7 @@
\ is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
by (simp_tac(simpset() addsimps [has_trace_def])1);
- by (Safe_tac);
+ by Safe_tac;
by (rename_tac "ex1 ex2" 1);
(* choose same trace, therefore same NF *)
--- a/src/HOL/Lex/AutoMaxChop.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/AutoMaxChop.ML Sun Jul 12 11:49:17 1998 +0200
@@ -5,33 +5,33 @@
*)
Goal "delta A (xs@[y]) q = next A y (delta A xs q)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "delta_snoc";
Goal
"!q ps res. auto_split A (delta A ps q) res ps xs = \
\ maxsplit (%ys. fin A (delta A ys q)) res ps xs";
-by(induct_tac "xs" 1);
-by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
+by (induct_tac "xs" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
delsimps [delta_append]) 1);
qed_spec_mp "auto_split_lemma";
Goalw [accepts_def]
"auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs";
-by(stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
-by(stac auto_split_lemma 1);
-by(Simp_tac 1);
+by (stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
+by (stac auto_split_lemma 1);
+by (Simp_tac 1);
qed_spec_mp "auto_split_is_maxsplit";
Goal
"is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)";
-by(simp_tac (simpset() addsimps
+by (simp_tac (simpset() addsimps
[auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1);
qed "is_maxsplitter_auto_split";
Goalw [auto_chop_def]
"is_maxchopper (accepts A) (auto_chop A)";
-br is_maxchopper_chop 1;
-br is_maxsplitter_auto_split 1;
+by (rtac is_maxchopper_chop 1);
+by (rtac is_maxsplitter_auto_split 1);
qed "is_maxchopper_auto_chop";
--- a/src/HOL/Lex/AutoProj.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/AutoProj.ML Sun Jul 12 11:49:17 1998 +0200
@@ -5,15 +5,15 @@
*)
Goalw [start_def] "start(q,d,f) = q";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "start_conv";
Goalw [next_def] "next(q,d,f) = d";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "next_conv";
Goalw [fin_def] "fin(q,d,f) = f";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "fin_conv";
Addsimps [start_conv,next_conv,fin_conv];
--- a/src/HOL/Lex/Automata.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/Automata.ML Sun Jul 12 11:49:17 1998 +0200
@@ -8,35 +8,35 @@
Goalw [na2da_def]
"!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
-by(induct_tac "w" 1);
- by(ALLGOALS Asm_simp_tac);
- by(ALLGOALS Blast_tac);
+by (induct_tac "w" 1);
+ by (ALLGOALS Asm_simp_tac);
+ by (ALLGOALS Blast_tac);
qed_spec_mp "DA_delta_is_lift_NA_delta";
Goalw [DA.accepts_def,NA.accepts_def]
"NA.accepts A w = DA.accepts (na2da A) w";
-by(simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
-by(simp_tac (simpset() addsimps [na2da_def]) 1);
+by (simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
+by (simp_tac (simpset() addsimps [na2da_def]) 1);
qed "NA_DA_equiv";
(*** Direct equivalence of NAe and DA ***)
Goalw [nae2da_def]
"!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
-by(induct_tac "w" 1);
+by (induct_tac "w" 1);
by (Simp_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [step_def]) 1);
-by(Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
+by (Blast_tac 1);
qed_spec_mp "espclosure_DA_delta_is_steps";
Goalw [nae2da_def]
"fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
-by(Simp_tac 1);
+by (Simp_tac 1);
val lemma = result();
Goalw [NAe.accepts_def,DA.accepts_def]
"DA.accepts (nae2da A) w = NAe.accepts A w";
-by(simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
-by(simp_tac (simpset() addsimps [nae2da_def]) 1);
-by(Blast_tac 1);
+by (simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
+by (simp_tac (simpset() addsimps [nae2da_def]) 1);
+by (Blast_tac 1);
qed "NAe_DA_equiv";
--- a/src/HOL/Lex/DA.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/DA.ML Sun Jul 12 11:49:17 1998 +0200
@@ -5,27 +5,27 @@
*)
Goalw [foldl2_def] "foldl2 f [] a = a";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "foldl2_Nil";
Goalw [foldl2_def] "foldl2 f (x#xs) a = foldl2 f xs (f x a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "foldl2_Cons";
Addsimps [foldl2_Nil,foldl2_Cons];
Goalw [delta_def] "delta A [] s = s";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "delta_Nil";
Goalw [delta_def] "delta A (a#w) s = delta A w (next A a s)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "delta_Cons";
Addsimps [delta_Nil,delta_Cons];
Goal "!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)";
-by(induct_tac "xs" 1);
+by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "delta_append";
Addsimps [delta_append];
--- a/src/HOL/Lex/MaxChop.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML Sun Jul 12 11:49:17 1998 +0200
@@ -7,12 +7,12 @@
(* Termination of chop *)
Goalw [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)";
-by(asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1);
qed "reducing_maxsplit";
val [tc] = chopr.tcs;
goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
-by(blast_tac (claset() addDs [sym]) 1);
+by (blast_tac (claset() addDs [sym]) 1);
val lemma = result();
val chopr_rule = let val [chopr_rule] = chopr.rules in lemma RS chopr_rule end;
@@ -22,85 +22,85 @@
\ in if pre=[] then ([],xs) \
\ else let (xss,zs) = chop splitf post \
\ in (pre#xss,zs))";
-by(asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1);
-by(simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
+by (asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1);
+by (simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
qed "chop_rule";
Goalw [is_maxsplitter_def,reducing_def]
"is_maxsplitter P splitf ==> reducing splitf";
-by(Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
qed "is_maxsplitter_reducing";
Goal "is_maxsplitter P splitf ==> \
\ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
-by(res_inst_tac [("xs","xs")] length_induct 1);
-by(asm_simp_tac (simpset() delsplits [split_if]
+by (res_inst_tac [("xs","xs")] length_induct 1);
+by (asm_simp_tac (simpset() delsplits [split_if]
addsimps [chop_rule,is_maxsplitter_reducing]
addcongs [if_weak_cong]) 1);
-by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
+by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
addsplits [split_split]) 1);
qed_spec_mp "chop_concat";
Goal "is_maxsplitter P splitf ==> \
\ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
-by(res_inst_tac [("xs","xs")] length_induct 1);
-by(asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
+by (res_inst_tac [("xs","xs")] length_induct 1);
+by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
addcongs [if_weak_cong]) 1);
-by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
+by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
addsplits [split_split]) 1);
-by(simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
+by (simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
addsplits [split_split]) 1);
-be thin_rl 1;
-by(strip_tac 1);
-br ballI 1;
-be exE 1;
-be allE 1;
-auto();
+by (etac thin_rl 1);
+by (strip_tac 1);
+by (rtac ballI 1);
+by (etac exE 1);
+by (etac allE 1);
+by Auto_tac;
qed_spec_mp "chop_nonempty";
val [prem] = goalw thy [is_maxchopper_def]
"is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)";
-by(Clarify_tac 1);
-br iffI 1;
- br conjI 1;
- be (prem RS chop_concat) 1;
- br conjI 1;
- be (prem RS chop_nonempty) 1;
- be rev_mp 1;
- by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
- by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
+by (Clarify_tac 1);
+by (rtac iffI 1);
+ by (rtac conjI 1);
+ by (etac (prem RS chop_concat) 1);
+ by (rtac conjI 1);
+ by (etac (prem RS chop_nonempty) 1);
+ by (etac rev_mp 1);
+ by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
+ by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
addsplits [split_split]) 1);
- by(Clarify_tac 1);
- br conjI 1;
- by(Clarify_tac 1);
- by(Asm_full_simp_tac 1);
- by(Clarify_tac 1);
- by(Asm_full_simp_tac 1);
- by(forward_tac [prem RS chop_concat] 1);
- by(Clarify_tac 1);
- ba 1;
-by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
- by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
+ by (Clarify_tac 1);
+ by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (Clarify_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (forward_tac [prem RS chop_concat] 1);
+ by (Clarify_tac 1);
+ by (assume_tac 1);
+by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
+ by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
addsplits [split_split]) 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(exhaust_tac "yss" 1);
- by(Asm_simp_tac 1);
- by(Asm_full_simp_tac 1);
- by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
- by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
-by(exhaust_tac "yss" 1);
- by(Asm_full_simp_tac 1);
- by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
- by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(subgoal_tac "x=a" 1);
- by(Clarify_tac 1);
- by(Asm_full_simp_tac 1);
-by(rotate_tac ~2 1);
-by(Asm_full_simp_tac 1);
-by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
-by(blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (exhaust_tac "yss" 1);
+ by (Asm_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
+ by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
+by (exhaust_tac "yss" 1);
+ by (Asm_full_simp_tac 1);
+ by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
+ by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "x=a" 1);
+ by (Clarify_tac 1);
+ by (Asm_full_simp_tac 1);
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac 1);
+by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
+by (blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);
qed "is_maxchopper_chop";
--- a/src/HOL/Lex/MaxPrefix.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/MaxPrefix.ML Sun Jul 12 11:49:17 1998 +0200
@@ -9,56 +9,56 @@
\ (maxsplit P res ps qs = (xs,ys)) = \
\ (if ? us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \
\ else (xs,ys)=res)";
-by(induct_tac "qs" 1);
- by(simp_tac (simpset() addsplits [split_if]) 1);
- by(Blast_tac 1);
-by(Asm_simp_tac 1);
-be thin_rl 1;
-by(Clarify_tac 1);
-by(case_tac "? us. us <= list & P (ps @ a # us)" 1);
- by(Asm_simp_tac 1);
- by(subgoal_tac "? us. us <= a # list & P (ps @ us)" 1);
- by(Asm_simp_tac 1);
- by(blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1);
-by(subgoal_tac "~P(ps@[a])" 1);
- by(Blast_tac 2);
-by(Asm_simp_tac 1);
-by(case_tac "? us. us <= a#list & P (ps @ us)" 1);
- by(Asm_simp_tac 1);
- by(Clarify_tac 1);
- by(exhaust_tac "us" 1);
- br iffI 1;
- by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
- by(Blast_tac 1);
- by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
- by(Clarify_tac 1);
- be disjE 1;
- by(fast_tac (claset() addDs [prefix_antisym]) 1);
- by(Clarify_tac 1);
- be disjE 1;
- by(Clarify_tac 1);
- by(Asm_full_simp_tac 1);
- be disjE 1;
- by(Clarify_tac 1);
- by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
- by(Asm_full_simp_tac 1);
-by(subgoal_tac "~P(ps)" 1);
-by(Asm_simp_tac 1);
-by(fast_tac (claset() addss simpset()) 1);
+by (induct_tac "qs" 1);
+ by (simp_tac (simpset() addsplits [split_if]) 1);
+ by (Blast_tac 1);
+by (Asm_simp_tac 1);
+by (etac thin_rl 1);
+by (Clarify_tac 1);
+by (case_tac "? us. us <= list & P (ps @ a # us)" 1);
+ by (Asm_simp_tac 1);
+ by (subgoal_tac "? us. us <= a # list & P (ps @ us)" 1);
+ by (Asm_simp_tac 1);
+ by (blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1);
+by (subgoal_tac "~P(ps@[a])" 1);
+ by (Blast_tac 2);
+by (Asm_simp_tac 1);
+by (case_tac "? us. us <= a#list & P (ps @ us)" 1);
+ by (Asm_simp_tac 1);
+ by (Clarify_tac 1);
+ by (exhaust_tac "us" 1);
+ by (rtac iffI 1);
+ by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
+ by (Blast_tac 1);
+ by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
+ by (Clarify_tac 1);
+ by (etac disjE 1);
+ by (fast_tac (claset() addDs [prefix_antisym]) 1);
+ by (Clarify_tac 1);
+ by (etac disjE 1);
+ by (Clarify_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (etac disjE 1);
+ by (Clarify_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
+ by (Asm_full_simp_tac 1);
+by (subgoal_tac "~P(ps)" 1);
+by (Asm_simp_tac 1);
+by (fast_tac (claset() addss simpset()) 1);
qed_spec_mp "maxsplit_lemma";
Addsplits [split_if];
Goalw [is_maxpref_def]
"~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "is_maxpref_Nil";
Addsimps [is_maxpref_Nil];
Goalw [is_maxsplitter_def]
"is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)";
-by(simp_tac (simpset() addsimps [maxsplit_lemma]) 1);
-by(fast_tac (claset() addss simpset()) 1);
+by (simp_tac (simpset() addsimps [maxsplit_lemma]) 1);
+by (fast_tac (claset() addss simpset()) 1);
qed "is_maxsplitter_maxsplit";
val maxsplit_eq = rewrite_rule [is_maxsplitter_def] is_maxsplitter_maxsplit;
--- a/src/HOL/Lex/NAe.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/NAe.ML Sun Jul 12 11:49:17 1998 +0200
@@ -6,13 +6,13 @@
Goal "steps A w O (eps A)^* = steps A w";
by (exhaust_tac "w" 1);
-by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
qed_spec_mp "steps_epsclosure";
Addsimps [steps_epsclosure];
Goal "[| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w";
-by(rtac (steps_epsclosure RS equalityE) 1);
-by(Blast_tac 1);
+by (rtac (steps_epsclosure RS equalityE) 1);
+by (Blast_tac 1);
qed "in_steps_epsclosure";
Goal "(eps A)^* O steps A w = steps A w";
@@ -22,19 +22,19 @@
qed "epsclosure_steps";
Goal "[| (p,q) : steps A w; (q,r) : (eps A)^* |] ==> (p,r) : steps A w";
-by(rtac (epsclosure_steps RS equalityE) 1);
-by(Blast_tac 1);
+by (rtac (epsclosure_steps RS equalityE) 1);
+by (Blast_tac 1);
qed "in_epsclosure_steps";
Goal "steps A (v@w) = steps A w O steps A v";
by (induct_tac "v" 1);
-by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
qed "steps_append";
Addsimps [steps_append];
Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
-by(rtac (steps_append RS equalityE) 1);
-by(Blast_tac 1);
+by (rtac (steps_append RS equalityE) 1);
+by (Blast_tac 1);
qed "in_steps_append";
AddIffs [in_steps_append];
@@ -44,6 +44,6 @@
by (induct_tac "w" 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "steps_equiv_delta";
*)
--- a/src/HOL/Lex/Prefix.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML Sun Jul 12 11:49:17 1998 +0200
@@ -15,18 +15,18 @@
(** <= is a partial order: **)
Goalw [prefix_def] "xs <= (xs::'a list)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "prefix_refl";
AddIffs[prefix_refl];
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
-by(Clarify_tac 1);
-by(Simp_tac 1);
+by (Clarify_tac 1);
+by (Simp_tac 1);
qed "prefix_trans";
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
qed "prefix_antisym";
(** recursion equations **)
@@ -44,17 +44,17 @@
Addsimps [prefix_Nil];
Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
-br iffI 1;
- be exE 1;
- by(rename_tac "zs" 1);
- by(res_inst_tac [("xs","zs")] rev_exhaust 1);
- by(Asm_full_simp_tac 1);
- by(hyp_subst_tac 1);
- by(asm_full_simp_tac (simpset() delsimps [append_assoc]
+by (rtac iffI 1);
+ by (etac exE 1);
+ by (rename_tac "zs" 1);
+ by (res_inst_tac [("xs","zs")] rev_exhaust 1);
+ by (Asm_full_simp_tac 1);
+ by (hyp_subst_tac 1);
+ by (asm_full_simp_tac (simpset() delsimps [append_assoc]
addsimps [append_assoc RS sym])1);
-be disjE 1;
- by(Asm_simp_tac 1);
-by(Clarify_tac 1);
+by (etac disjE 1);
+ by (Asm_simp_tac 1);
+by (Clarify_tac 1);
by (Simp_tac 1);
qed "prefix_snoc";
Addsimps [prefix_snoc];
@@ -67,7 +67,7 @@
Goal "(xs@ys <= xs@zs) = (ys <= zs)";
by (induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (ALLGOALS Asm_simp_tac);
qed "same_prefix_prefix";
Addsimps [same_prefix_prefix];
@@ -75,7 +75,7 @@
[simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
-by(Clarify_tac 1);
+by (Clarify_tac 1);
by (Simp_tac 1);
qed "prefix_prefix";
Addsimps [prefix_prefix];
@@ -90,11 +90,11 @@
qed "prefix_Cons";
Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by(res_inst_tac [("xs","zs")] rev_induct 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
-by(asm_full_simp_tac (simpset() delsimps [append_assoc]
+by (res_inst_tac [("xs","zs")] rev_induct 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [append_assoc]
addsimps [append_assoc RS sym])1);
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
qed "prefix_append";
--- a/src/HOL/Lex/RegExp2NAe.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML Sun Jul 12 11:49:17 1998 +0200
@@ -9,43 +9,43 @@
(******************************************************)
Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "fin_atom";
Goalw [atom_def] "start (atom a) = [True]";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "start_atom";
(* Use {x. False} = {}? *)
Goalw [atom_def,step_def]
"eps(atom a) = {}";
-by(Simp_tac 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed "eps_atom";
Addsimps [eps_atom];
Goalw [atom_def,step_def]
"(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "in_step_atom_Some";
Addsimps [in_step_atom_Some];
Goal "([False],[False]) : steps (atom a) w = (w = [])";
by (induct_tac "w" 1);
- by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
qed "False_False_in_steps_atom";
Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
by (induct_tac "w" 1);
- by(asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
-by(asm_full_simp_tac (simpset()
+ by (asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
+by (asm_full_simp_tac (simpset()
addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
qed "start_fin_in_steps_atom";
Goal "accepts (atom a) w = (w = [a])";
-by(simp_tac(simpset() addsimps
+by (simp_tac(simpset() addsimps
[accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
qed "accepts_atom";
@@ -73,13 +73,13 @@
Goalw [union_def,step_def]
"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "True_in_step_union";
Goalw [union_def,step_def]
"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "False_in_step_union";
AddIffs [True_in_step_union,False_in_step_union];
@@ -89,45 +89,45 @@
Goal
"(tp,tq) : (eps(union L R))^* ==> \
\ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
val lemma1a = result();
Goal
"(tp,tq) : (eps(union L R))^* ==> \
\ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
val lemma1b = result();
Goal
"(p,q) : (eps L)^* ==> (True#p, True#q) : (eps(union L R))^*";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
val lemma2a = result();
Goal
"(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(union L R))^*";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
val lemma2b = result();
Goal
"(True#p,q) : (eps(union L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
-by(blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
+by (blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
qed "True_epsclosure_union";
Goal
"(False#p,q) : (eps(union L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
-by(blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
+by (blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
qed "False_epsclosure_union";
AddIffs [True_epsclosure_union,False_epsclosure_union];
@@ -139,7 +139,7 @@
by (induct_tac "w" 1);
by (ALLGOALS Asm_simp_tac);
(* Blast_tac produces PROOF FAILED for depth 8 *)
-by(Fast_tac 1);
+by (Fast_tac 1);
qed_spec_mp "lift_True_over_steps_union";
Goal
@@ -147,7 +147,7 @@
by (induct_tac "w" 1);
by (ALLGOALS Asm_simp_tac);
(* Blast_tac produces PROOF FAILED for depth 8 *)
-by(Fast_tac 1);
+by (Fast_tac 1);
qed_spec_mp "lift_False_over_steps_union";
AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
@@ -157,19 +157,19 @@
Goal
"R^* = id Un (R^* O R)";
-by(rtac set_ext 1);
-by(split_all_tac 1);
-by(rtac iffI 1);
- be rtrancl_induct 1;
- by(Blast_tac 1);
- by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+by (rtac set_ext 1);
+by (split_all_tac 1);
+by (rtac iffI 1);
+ by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+ by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
qed "unfold_rtrancl2";
Goal
"(p,q) : R^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))";
-by(rtac (unfold_rtrancl2 RS equalityE) 1);
-by(Blast_tac 1);
+by (rtac (unfold_rtrancl2 RS equalityE) 1);
+by (Blast_tac 1);
qed "in_unfold_rtrancl2";
val epsclosure_start_step_union =
@@ -179,13 +179,13 @@
Goalw [union_def,step_def]
"!L R. (start(union L R),q) : eps(union L R) = \
\ (q = True#start L | q = False#start R)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "start_eps_union";
AddIffs [start_eps_union];
Goalw [union_def,step_def]
"!L R. (start(union L R),q) ~: step (union L R) (Some a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "not_start_step_union_Some";
AddIffs [not_start_step_union_Some];
@@ -197,54 +197,54 @@
by (exhaust_tac "w" 1);
by (Asm_simp_tac 1);
(* Blast_tac produces PROOF FAILED! *)
- by(Fast_tac 1);
+ by (Fast_tac 1);
by (Asm_simp_tac 1);
(* The goal is now completely dual to the first one.
Fast/Best_tac don't return. Blast_tac produces PROOF FAILED!
The lemmas used in the explicit proof are part of the claset already!
*)
-br iffI 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-be disjE 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-br compI 1;
-br compI 1;
-br (epsclosure_start_step_union RS iffD2) 1;
-br disjI2 1;
-br exI 1;
-br conjI 1;
-br (start_eps_union RS iffD2) 1;
-br disjI2 1;
-br refl 1;
-by(Clarify_tac 1);
-br exI 1;
-br conjI 1;
-br refl 1;
-ba 1;
-by(Clarify_tac 1);
-br exI 1;
-br conjI 1;
-br refl 1;
-ba 1;
-by(Clarify_tac 1);
-br exI 1;
-br conjI 1;
-br refl 1;
-ba 1;
+by (rtac iffI 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (etac disjE 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (rtac compI 1);
+by (rtac compI 1);
+by (rtac (epsclosure_start_step_union RS iffD2) 1);
+by (rtac disjI2 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac (start_eps_union RS iffD2) 1);
+by (rtac disjI2 1);
+by (rtac refl 1);
+by (Clarify_tac 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (assume_tac 1);
+by (Clarify_tac 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (assume_tac 1);
+by (Clarify_tac 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (assume_tac 1);
qed "steps_union";
Goalw [union_def]
"!L R. ~ fin (union L R) (start(union L R))";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "start_union_not_final";
AddIffs [start_union_not_final];
Goalw [accepts_def]
"accepts (union L R) w = (accepts L w | accepts R w)";
by (simp_tac (simpset() addsimps [steps_union]) 1);
-auto();
+by Auto_tac;
qed "accepts_union";
@@ -273,14 +273,14 @@
\ ((? r. q=True#r & (p,r): step L a) | \
\ (fin L p & a=None & q=False#start R))";
by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "True_step_conc";
Goalw [conc_def,step_def]
"!L R. (False#p,q) : step (conc L R) a = \
\ (? r. q = False#r & (p,r) : step R a)";
by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed_spec_mp "False_step_conc";
AddIffs [True_step_conc, False_step_conc];
@@ -290,24 +290,24 @@
Goal
"(tp,tq) : (eps(conc L R))^* ==> \
\ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
qed "lemma1b";
Goal
"(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
val lemma2b = result();
Goal
"((False # p, q) : (eps (conc L R))^*) = \
\ (? r. q = False # r & (p, r) : (eps R)^*)";
by (rtac iffI 1);
- by(blast_tac (claset() addDs [lemma1b]) 1);
-by(blast_tac (claset() addDs [lemma2b]) 1);
+ by (blast_tac (claset() addDs [lemma1b]) 1);
+by (blast_tac (claset() addDs [lemma2b]) 1);
qed "False_epsclosure_conc";
AddIffs [False_epsclosure_conc];
@@ -319,7 +319,7 @@
by (Simp_tac 1);
by (Simp_tac 1);
(* Blast_tac produces PROOF FAILED for depth 8 *)
-by(Fast_tac 1);
+by (Fast_tac 1);
qed_spec_mp "False_steps_conc";
AddIffs [False_steps_conc];
@@ -327,17 +327,17 @@
Goal
"(p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
qed "True_True_eps_concI";
Goal
"!p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
-by(induct_tac "w" 1);
+by (induct_tac "w" 1);
by (simp_tac (simpset() addsimps [True_True_eps_concI]) 1);
by (Simp_tac 1);
-by(blast_tac (claset() addIs [True_True_eps_concI]) 1);
+by (blast_tac (claset() addIs [True_True_eps_concI]) 1);
qed_spec_mp "True_True_steps_concI";
Goal
@@ -345,36 +345,36 @@
\ !p. tp = True#p --> \
\ (? q. tq = True#q & (p,q) : (eps L)^*) | \
\ (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*)";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
val lemma1a = result();
Goal
"(p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
val lemma2a = result();
Goalw [conc_def,step_def]
"!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None";
-by(split_all_tac 1);
+by (split_all_tac 1);
by (Asm_full_simp_tac 1);
val lemma = result();
Goal
"(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
by (dtac lemma 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
val lemma2b = result();
Goalw [conc_def,step_def]
"!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)";
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
qed "True_False_eps_concI";
Goal
@@ -382,16 +382,16 @@
\ ((? r. (p,r) : (eps L)^* & q = True#r) | \
\ (? r. (p,r) : (eps L)^* & fin L r & \
\ (? s. (start R, s) : (eps R)^* & q = False#s)))";
-by(rtac iffI 1);
- by(blast_tac (claset() addDs [lemma1a]) 1);
-be disjE 1;
- by(blast_tac (claset() addIs [lemma2a]) 1);
-by(Clarify_tac 1);
-br (rtrancl_trans) 1;
-be lemma2a 1;
-br (rtrancl_into_rtrancl2) 1;
-be True_False_eps_concI 1;
-be lemma2b 1;
+by (rtac iffI 1);
+ by (blast_tac (claset() addDs [lemma1a]) 1);
+by (etac disjE 1);
+ by (blast_tac (claset() addIs [lemma2a]) 1);
+by (Clarify_tac 1);
+by (rtac (rtrancl_trans) 1);
+by (etac lemma2a 1);
+by (rtac (rtrancl_into_rtrancl2) 1);
+by (etac True_False_eps_concI 1);
+by (etac lemma2b 1);
qed "True_epsclosure_conc";
AddIffs [True_epsclosure_conc];
@@ -402,29 +402,29 @@
\ ((? r. (p,r) : steps L w & q = True#r) | \
\ (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
\ (? s. (start R,s) : steps R v & q = False#s))))";
-by(induct_tac "w" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(clarify_tac (claset() delrules [disjCI]) 1);
- be disjE 1;
- by(clarify_tac (claset() delrules [disjCI]) 1);
- be disjE 1;
- by(clarify_tac (claset() delrules [disjCI]) 1);
- by(etac allE 1 THEN mp_tac 1);
- be disjE 1;
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (etac disjE 1);
+ by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (etac disjE 1);
+ by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (etac allE 1 THEN mp_tac 1);
+ by (etac disjE 1);
by (Blast_tac 1);
- br disjI2 1;
+ by (rtac disjI2 1);
by (Clarify_tac 1);
- by(Simp_tac 1);
- by(res_inst_tac[("x","a#u")] exI 1);
- by(Simp_tac 1);
+ by (Simp_tac 1);
+ by (res_inst_tac[("x","a#u")] exI 1);
+ by (Simp_tac 1);
by (Blast_tac 1);
by (Blast_tac 1);
-br disjI2 1;
+by (rtac disjI2 1);
by (Clarify_tac 1);
-by(Simp_tac 1);
-by(res_inst_tac[("x","[]")] exI 1);
-by(Simp_tac 1);
+by (Simp_tac 1);
+by (res_inst_tac[("x","[]")] exI 1);
+by (Simp_tac 1);
by (Blast_tac 1);
qed_spec_mp "True_steps_concD";
@@ -433,7 +433,7 @@
\ ((? r. (p,r) : steps L w & q = True#r) | \
\ (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
\ (? s. (start R,s) : steps R v & q = False#s))))";
-by(blast_tac (claset() addDs [True_steps_concD]
+by (blast_tac (claset() addDs [True_steps_concD]
addIs [True_True_steps_concI,in_steps_epsclosure,r_into_rtrancl]) 1);
qed "True_steps_conc";
@@ -441,7 +441,7 @@
Goalw [conc_def]
"!L R. start(conc L R) = True#start L";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "start_conc";
Goalw [conc_def]
@@ -453,7 +453,7 @@
"accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
by (simp_tac (simpset() addsimps
[accepts_def,True_steps_conc,final_conc,start_conc]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "accepts_conc";
(******************************************************)
@@ -463,26 +463,26 @@
Goalw [star_def,step_def]
"!A. (True#p,q) : eps(star A) = \
\ ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
qed_spec_mp "True_in_eps_star";
AddIffs [True_in_eps_star];
Goalw [star_def,step_def]
"!A. (p,q) : step A a --> (True#p, True#q) : step (star A) a";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "True_True_step_starI";
Goal
"(p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
qed_spec_mp "True_True_eps_starI";
Goalw [star_def,step_def]
"!A. fin A p --> (True#p,True#start A) : eps(star A)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "True_start_eps_starI";
Goal
@@ -490,11 +490,11 @@
\ (? r. ((p,r) : (eps A)^* | \
\ (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
\ s = True#r))";
-be rtrancl_induct 1;
- by(Simp_tac 1);
+by (etac rtrancl_induct 1);
+ by (Simp_tac 1);
by (Clarify_tac 1);
by (Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
val lemma = result();
Goal
@@ -502,20 +502,20 @@
\ (? r. ((p,r) : (eps A)^* | \
\ (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
\ s = True#r)";
-br iffI 1;
- bd lemma 1;
- by(Blast_tac 1);
+by (rtac iffI 1);
+ by (dtac lemma 1);
+ by (Blast_tac 1);
(* Why can't blast_tac do the rest? *)
by (Clarify_tac 1);
-be disjE 1;
-be True_True_eps_starI 1;
+by (etac disjE 1);
+by (etac True_True_eps_starI 1);
by (Clarify_tac 1);
-br rtrancl_trans 1;
-be True_True_eps_starI 1;
-br rtrancl_trans 1;
-br r_into_rtrancl 1;
-be True_start_eps_starI 1;
-be True_True_eps_starI 1;
+by (rtac rtrancl_trans 1);
+by (etac True_True_eps_starI 1);
+by (rtac rtrancl_trans 1);
+by (rtac r_into_rtrancl 1);
+by (etac True_start_eps_starI 1);
+by (etac True_True_eps_starI 1);
qed "True_eps_star";
AddIffs [True_eps_star];
@@ -524,8 +524,8 @@
Goalw [star_def,step_def]
"!A. (True#p,r): step (star A) (Some a) = \
\ (? q. (p,q): step A (Some a) & r=True#q)";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
qed_spec_mp "True_step_star";
AddIffs [True_step_star];
@@ -538,44 +538,44 @@
\ (? us v. w = concat us @ v & \
\ (!u:set us. accepts A u) & \
\ (? r. (start A,r) : steps A v & rr = True#r))";
-by(res_inst_tac [("xs","w")] rev_induct 1);
+by (res_inst_tac [("xs","w")] rev_induct 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
- by(res_inst_tac [("x","[]")] exI 1);
- be disjE 1;
+ by (res_inst_tac [("x","[]")] exI 1);
+ by (etac disjE 1);
by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (Asm_simp_tac 1);
-by(simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
+by (simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
by (Clarify_tac 1);
-by(etac allE 1 THEN mp_tac 1);
+by (etac allE 1 THEN mp_tac 1);
by (Clarify_tac 1);
-be disjE 1;
- by(res_inst_tac [("x","us")] exI 1);
- by(res_inst_tac [("x","v@[x]")] exI 1);
- by(asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
- by(Blast_tac 1);
+by (etac disjE 1);
+ by (res_inst_tac [("x","us")] exI 1);
+ by (res_inst_tac [("x","v@[x]")] exI 1);
+ by (asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
+ by (Blast_tac 1);
by (Clarify_tac 1);
-by(res_inst_tac [("x","us@[v@[x]]")] exI 1);
-by(res_inst_tac [("x","[]")] exI 1);
-by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
-by(Blast_tac 1);
+by (res_inst_tac [("x","us@[v@[x]]")] exI 1);
+by (res_inst_tac [("x","[]")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+by (Blast_tac 1);
qed_spec_mp "True_start_steps_starD";
Goal "!p. (p,q) : steps A w --> (True#p,True#q) : steps (star A) w";
-by(induct_tac "w" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
qed_spec_mp "True_True_steps_starI";
Goalw [accepts_def]
"(!u : set us. accepts A u) --> \
\ (True#start A,True#start A) : steps (star A) (concat us)";
-by(induct_tac "us" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
+by (induct_tac "us" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
qed_spec_mp "steps_star_cycle";
(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
@@ -584,18 +584,18 @@
\ (? us v. w = concat us @ v & \
\ (!u:set us. accepts A u) & \
\ (? r. (start A,r) : steps A v & rr = True#r))";
-br iffI 1;
- be True_start_steps_starD 1;
+by (rtac iffI 1);
+ by (etac True_start_steps_starD 1);
by (Clarify_tac 1);
-by(Asm_simp_tac 1);
-by(blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
+by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
qed "True_start_steps_star";
(** the start state **)
Goalw [star_def,step_def]
"!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "start_step_star";
AddIffs [start_step_star];
@@ -605,27 +605,27 @@
Goal
"(start(star A),r) : steps (star A) w = \
\ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
-br iffI 1;
- by(exhaust_tac "w" 1);
- by(asm_full_simp_tac (simpset() addsimps
+by (rtac iffI 1);
+ by (exhaust_tac "w" 1);
+ by (asm_full_simp_tac (simpset() addsimps
[epsclosure_start_step_star]) 1);
- by(Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
- by(asm_full_simp_tac (simpset() addsimps
+ by (asm_full_simp_tac (simpset() addsimps
[epsclosure_start_step_star]) 1);
- by(Blast_tac 1);
-be disjE 1;
- by(Asm_simp_tac 1);
-by(blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
+ by (Blast_tac 1);
+by (etac disjE 1);
+ by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
qed "start_steps_star";
Goalw [star_def] "!A. fin (star A) (True#p) = fin A p";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "fin_star_True";
AddIffs [fin_star_True];
Goalw [star_def] "!A. fin (star A) (start(star A))";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed_spec_mp "fin_star_start";
AddIffs [fin_star_start];
@@ -633,25 +633,25 @@
Goalw [accepts_def]
"accepts (star A) w = \
\ (? us. (!u : set(us). accepts A u) & (w = concat us) )";
-by(simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
-br iffI 1;
+by (simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
+by (rtac iffI 1);
by (Clarify_tac 1);
- be disjE 1;
+ by (etac disjE 1);
by (Clarify_tac 1);
- by(Simp_tac 1);
- by(res_inst_tac [("x","[]")] exI 1);
- by(Simp_tac 1);
+ by (Simp_tac 1);
+ by (res_inst_tac [("x","[]")] exI 1);
+ by (Simp_tac 1);
by (Clarify_tac 1);
- by(res_inst_tac [("x","us@[v]")] exI 1);
- by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
- by(Blast_tac 1);
+ by (res_inst_tac [("x","us@[v]")] exI 1);
+ by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+ by (Blast_tac 1);
by (Clarify_tac 1);
-by(res_inst_tac [("xs","us")] rev_exhaust 1);
- by(Asm_simp_tac 1);
- by(Blast_tac 1);
+by (res_inst_tac [("xs","us")] rev_exhaust 1);
+ by (Asm_simp_tac 1);
+ by (Blast_tac 1);
by (Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
-by(Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+by (Blast_tac 1);
qed "accepts_star";
@@ -659,10 +659,10 @@
Goal
"!w. accepts (rexp2nae r) w = (w : lang r)";
-by(induct_tac "r" 1);
- by(simp_tac (simpset() addsimps [accepts_def]) 1);
- by(simp_tac(simpset() addsimps [accepts_atom]) 1);
- by(asm_simp_tac (simpset() addsimps [accepts_union]) 1);
- by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
-by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
+by (induct_tac "r" 1);
+ by (simp_tac (simpset() addsimps [accepts_def]) 1);
+ by (simp_tac(simpset() addsimps [accepts_atom]) 1);
+ by (asm_simp_tac (simpset() addsimps [accepts_union]) 1);
+ by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
+by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
qed "accepts_rexp2nae";
--- a/src/HOL/Lex/RegSet.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/RegSet.ML Sun Jul 12 11:49:17 1998 +0200
@@ -15,7 +15,7 @@
Goal
"w : star U = (? us. (!u : set(us). u : U) & (w = concat us))";
-br iffI 1;
+by (rtac iffI 1);
be star.induct 1;
by (res_inst_tac [("x","[]")] exI 1);
by (Simp_tac 1);
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML Sun Jul 12 11:49:17 1998 +0200
@@ -210,6 +210,6 @@
Goalw [regset_of_DA_def]
"[| bounded (next A) k; start A < k; j < k |] ==> \
\ w : regset_of_DA A k = accepts A w";
-by(asm_simp_tac (simpset() addcongs [conj_cong] addsimps
+by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps
[regset_below,deltas_below,accepts_def,delta_def]) 1);
qed "regset_DA_equiv";
--- a/src/HOL/Lex/Scanner.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/Scanner.ML Sun Jul 12 11:49:17 1998 +0200
@@ -6,5 +6,5 @@
Goal
"DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)";
-by(simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
+by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
qed "accepts_nae2da_rexp2nae";
--- a/src/HOL/List.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/List.ML Sun Jul 12 11:49:17 1998 +0200
@@ -21,7 +21,7 @@
(* Induction over the length of a list: *)
val [prem] = Goal
"(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
-by(rtac measure_induct 1 THEN etac prem 1);
+by (rtac measure_induct 1 THEN etac prem 1);
qed "length_induct";
@@ -184,14 +184,14 @@
[same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
Goal "(xs @ ys = ys) = (xs=[])";
-by(cut_inst_tac [("zs","[]")] append_same_eq 1);
+by (cut_inst_tac [("zs","[]")] append_same_eq 1);
by (Auto_tac);
qed "append_self_conv2";
Goal "(ys = xs @ ys) = (xs=[])";
-by(simp_tac (simpset() addsimps
+by (simp_tac (simpset() addsimps
[simplify (simpset()) (read_instantiate[("ys","[]")]append_same_eq)]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "self_append_conv2";
AddIffs [append_self_conv2,self_append_conv2];
@@ -309,16 +309,16 @@
AddIffs [Nil_is_rev_conv];
val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
-by(stac (rev_rev_ident RS sym) 1);
+by (stac (rev_rev_ident RS sym) 1);
br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
-by(ALLGOALS Simp_tac);
-brs prems 1;
-bes prems 1;
+by (ALLGOALS Simp_tac);
+by (resolve_tac prems 1);
+by (eresolve_tac prems 1);
qed "rev_induct";
Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P";
-by(res_inst_tac [("xs","xs")] rev_induct 1);
-by(Auto_tac);
+by (res_inst_tac [("xs","xs")] rev_induct 1);
+by (Auto_tac);
bind_thm ("rev_exhaust",
impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
--- a/src/HOL/NatDef.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/NatDef.ML Sun Jul 12 11:49:17 1998 +0200
@@ -601,7 +601,7 @@
Goal "(m::nat) <= n | n <= m";
by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
by (cut_facts_tac [less_linear] 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "nat_le_linear";
--- a/src/HOL/Ord.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Ord.ML Sun Jul 12 11:49:17 1998 +0200
@@ -58,31 +58,31 @@
Goal "!!x::'a::linorder. x<y | x=y | y<x";
by (simp_tac (simpset() addsimps [order_less_le]) 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
by (Blast_tac 1);
qed "linorder_less_linear";
Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
by (Simp_tac 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "le_max_iff_disj";
Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
by (Simp_tac 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "max_le_iff_conj";
Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
by (Simp_tac 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "le_min_iff_conj";
Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
by (Simp_tac 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
by (blast_tac (claset() addIs [order_trans]) 1);
qed "min_le_iff_disj";
--- a/src/HOL/Prod.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Prod.ML Sun Jul 12 11:49:17 1998 +0200
@@ -156,7 +156,7 @@
Addsimps split_etas; (* pragmatic solution *)
Goal "(%(x,y,z).f(x,y,z)) = t";
-by(simp_tac (simpset() addsimps [cond_split_eta]) 1);
+by (simp_tac (simpset() addsimps [cond_split_eta]) 1);
qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
--- a/src/HOL/Trancl.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Trancl.ML Sun Jul 12 11:49:17 1998 +0200
@@ -114,9 +114,9 @@
Addsimps [rtrancl_idemp];
Goal "R^* O R^* = R^*";
-br set_ext 1;
-by(split_all_tac 1);
-by(blast_tac (claset() addIs [rtrancl_trans]) 1);
+by (rtac set_ext 1);
+by (split_all_tac 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
qed "rtrancl_idemp_self_comp";
Addsimps [rtrancl_idemp_self_comp];
@@ -341,7 +341,7 @@
by (etac rtranclE 1);
by (Auto_tac );
by (etac rtrancl_into_trancl1 1);
-ba 1;
+by (assume_tac 1);
qed "reflcl_trancl";
Addsimps[reflcl_trancl];
--- a/src/HOL/UNITY/Traces.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Sun Jul 12 11:49:17 1998 +0200
@@ -53,7 +53,7 @@
\ ==> P s' |] \
\ ==> P za";
by (cut_facts_tac [major] 1);
-auto();
+by Auto_tac;
be traces.induct 1;
by (ALLGOALS (blast_tac (claset() addIs prems)));
qed "reachable_induct";
--- a/src/HOL/WF.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/WF.ML Sun Jul 12 11:49:17 1998 +0200
@@ -232,7 +232,7 @@
by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
by (Clarify_tac 1);
by (stac cut_apply 1);
- by(fast_tac (claset() addDs [transD]) 1);
+ by (fast_tac (claset() addDs [transD]) 1);
by (rtac (refl RSN (2,H_cong)) 1);
by (fold_tac [is_recfun_def]);
by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1);
--- a/src/HOL/arith_data.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/arith_data.ML Sun Jul 12 11:49:17 1998 +0200
@@ -226,7 +226,7 @@
by (induct_tac "l" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
-be less_SucE 1;
+by (etac less_SucE 1);
by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
Suc_diff_n]) 1);
by (Clarify_tac 1);
--- a/src/HOLCF/IOA/NTP/Multiset.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.ML Sun Jul 12 11:49:17 1998 +0200
@@ -38,7 +38,7 @@
by (res_inst_tac [("M","M")] Multiset.induction 1);
by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
-auto();
+by Auto_tac;
qed "countm_props";
Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Sun Jul 12 11:49:17 1998 +0200
@@ -39,13 +39,13 @@
Goal "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))";
by (simp_tac (simpset() addsimps [temp_weakening_def,temp_strengthening_def,
NOT_def,temp_sat_def,satisfies_def]) 1);
-auto();
+by Auto_tac;
qed"temp_weakening_def2";
Goal "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))";
by (simp_tac (simpset() addsimps [state_weakening_def,state_strengthening_def,
NOT_def]) 1);
-auto();
+by Auto_tac;
qed"state_weakening_def2";
@@ -74,7 +74,7 @@
Goal "!!A. is_abstraction h C A ==> weakeningIOA A C h";
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
-auto();
+by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
(* start state *)
by (rtac conjI 1);
@@ -87,7 +87,7 @@
Goal "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
\ ==> validIOA C P";
-bd abs_is_weakening 1;
+by (dtac abs_is_weakening 1);
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def,
validIOA_def, temp_strengthening_def])1);
by (safe_tac set_cs);
@@ -120,8 +120,8 @@
"!!A. [|is_live_abstraction h (C,L) (A,M); \
\ validLIOA (A,M) Q; temp_strengthening Q P h |] \
\ ==> validLIOA (C,L) P";
-auto();
-bd abs_is_weakening 1;
+by Auto_tac;
+by (dtac abs_is_weakening 1);
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
validLIOA_def, validIOA_def, temp_strengthening_def])1);
by (safe_tac set_cs);
@@ -134,8 +134,8 @@
\ validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h; \
\ temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
\ ==> validLIOA (C,L) P";
-auto();
-bd abs_is_weakening 1;
+by Auto_tac;
+by (dtac abs_is_weakening 1);
by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
validLIOA_def, validIOA_def, temp_strengthening_def])1);
by (safe_tac set_cs);
@@ -162,10 +162,10 @@
\ is_abstraction h C A |] \
\ ==> C =<| A";
by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
-br trace_inclusion 1;
+by (rtac trace_inclusion 1);
by (simp_tac (simpset() addsimps [externals_def])1);
by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
-be abstraction_is_ref_map 1;
+by (etac abstraction_is_ref_map 1);
qed"abs_safety";
@@ -244,7 +244,7 @@
Goalw [ioa_implements_def]
"!! A. [| A =<| B; B =<| C|] ==> A =<| C";
-auto();
+by Auto_tac;
qed"implements_trans";
@@ -260,13 +260,13 @@
\ A =<| Q ; \
\ is_abstraction h2 Q P |] \
\ ==> C =<| P";
-bd abs_safety 1;
+by (dtac abs_safety 1);
by (REPEAT (atac 1));
-bd abs_safety 1;
+by (dtac abs_safety 1);
by (REPEAT (atac 1));
-be implements_trans 1;
-be implements_trans 1;
-ba 1;
+by (etac implements_trans 1);
+by (etac implements_trans 1);
+by (assume_tac 1);
qed"AbsRuleA1";
@@ -276,13 +276,13 @@
\ live_implements (A,LA) (Q,LQ) ; \
\ is_live_abstraction h2 (Q,LQ) (P,LP) |] \
\ ==> live_implements (C,LC) (P,LP)";
-bd abs_liveness 1;
+by (dtac abs_liveness 1);
by (REPEAT (atac 1));
-bd abs_liveness 1;
+by (dtac abs_liveness 1);
by (REPEAT (atac 1));
-be live_implements_trans 1;
-be live_implements_trans 1;
-ba 1;
+by (etac live_implements_trans 1);
+by (etac live_implements_trans 1);
+by (assume_tac 1);
qed"AbsRuleA2";
@@ -299,21 +299,21 @@
"!! h. [| temp_strengthening P1 Q1 h; \
\ temp_strengthening P2 Q2 h |] \
\ ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
-auto();
+by Auto_tac;
qed"strength_AND";
Goalw [temp_strengthening_def]
"!! h. [| temp_strengthening P1 Q1 h; \
\ temp_strengthening P2 Q2 h |] \
\ ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
-auto();
+by Auto_tac;
qed"strength_OR";
Goalw [temp_strengthening_def]
"!! h. [| temp_weakening P Q h |] \
\ ==> temp_strengthening (.~ P) (.~ Q) h";
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
-auto();
+by Auto_tac;
qed"strength_NOT";
Goalw [temp_strengthening_def]
@@ -347,7 +347,7 @@
"!! h. [| temp_strengthening P Q h |] \
\ ==> temp_weakening (.~ P) (.~ Q) h";
by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
-auto();
+by Auto_tac;
qed"weak_NOT";
Goalw [temp_strengthening_def]
@@ -387,16 +387,16 @@
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
(* cons case *)
by (pair_tac "aa" 1);
-auto();
+by Auto_tac;
qed_spec_mp"ex2seqConc";
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
Goalw [tsuffix_def,suffix_def]
"!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
-auto();
-bd ex2seqConc 1;
-auto();
+by Auto_tac;
+by (dtac ex2seqConc 1);
+by Auto_tac;
qed"ex2seq_tsuffix";
@@ -414,7 +414,7 @@
Goalw [tsuffix_def,suffix_def,cex_absSeq_def]
"!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
-auto();
+by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1);
@@ -486,7 +486,7 @@
by (pair_tac "ex" 1);
by (Seq_case_simp_tac "y" 1);
by (pair_tac "a" 1);
-auto();
+by Auto_tac;
qed"TLex2seq";
@@ -520,9 +520,9 @@
(* cons case *)
by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqUUTL,ex2seqnilTL])1);
-bd TLex2seq 1;
-ba 1;
-auto();
+by (dtac TLex2seq 1);
+by (assume_tac 1);
+by Auto_tac;
qed"strength_Next";
@@ -572,18 +572,18 @@
Goalw [Diamond_def]
"!! h. [| temp_strengthening P Q h |]\
\ ==> temp_strengthening (<> P) (<> Q) h";
-br strength_NOT 1;
-br weak_Box 1;
-be weak_NOT 1;
+by (rtac strength_NOT 1);
+by (rtac weak_Box 1);
+by (etac weak_NOT 1);
qed"strength_Diamond";
Goalw [Leadsto_def]
"!! h. [| temp_weakening P1 P2 h;\
\ temp_strengthening Q1 Q2 h |]\
\ ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
-br strength_Box 1;
-be strength_IMPLIES 1;
-be strength_Diamond 1;
+by (rtac strength_Box 1);
+by (etac strength_IMPLIES 1);
+by (etac strength_Diamond 1);
qed"strength_Leadsto";
@@ -595,30 +595,30 @@
Goalw [Diamond_def]
"!! h. [| temp_weakening P Q h |]\
\ ==> temp_weakening (<> P) (<> Q) h";
-br weak_NOT 1;
-br strength_Box 1;
-be strength_NOT 1;
+by (rtac weak_NOT 1);
+by (rtac strength_Box 1);
+by (etac strength_NOT 1);
qed"weak_Diamond";
Goalw [Leadsto_def]
"!! h. [| temp_strengthening P1 P2 h;\
\ temp_weakening Q1 Q2 h |]\
\ ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
-br weak_Box 1;
-be weak_IMPLIES 1;
-be weak_Diamond 1;
+by (rtac weak_Box 1);
+by (etac weak_IMPLIES 1);
+by (etac weak_Diamond 1);
qed"weak_Leadsto";
Goalw [WF_def]
" !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \
\ ==> temp_weakening (WF A acts) (WF C acts) h";
-br weak_IMPLIES 1;
-br strength_Diamond 1;
-br strength_Box 1;
-br strength_Init 1;
-br weak_Box 2;
-br weak_Diamond 2;
-br weak_Init 2;
+by (rtac weak_IMPLIES 1);
+by (rtac strength_Diamond 1);
+by (rtac strength_Box 1);
+by (rtac strength_Init 1);
+by (rtac weak_Box 2);
+by (rtac weak_Diamond 2);
+by (rtac weak_Init 2);
by (auto_tac (claset(),
simpset() addsimps [state_weakening_def,state_strengthening_def,
xt2_def,plift_def,option_lift_def,NOT_def]));
@@ -627,13 +627,13 @@
Goalw [SF_def]
" !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \
\ ==> temp_weakening (SF A acts) (SF C acts) h";
-br weak_IMPLIES 1;
-br strength_Box 1;
-br strength_Diamond 1;
-br strength_Init 1;
-br weak_Box 2;
-br weak_Diamond 2;
-br weak_Init 2;
+by (rtac weak_IMPLIES 1);
+by (rtac strength_Box 1);
+by (rtac strength_Diamond 1);
+by (rtac strength_Init 1);
+by (rtac weak_Box 2);
+by (rtac weak_Diamond 2);
+by (rtac weak_Init 2);
by (auto_tac (claset(),
simpset() addsimps [state_weakening_def,state_strengthening_def,
xt2_def,plift_def,option_lift_def,NOT_def]));
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Sun Jul 12 11:49:17 1998 +0200
@@ -59,7 +59,7 @@
by (rtac conjI 1);
(* a : act (A||B) *)
by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 2);
-by(blast_tac (claset() addDs [int_is_act,out_is_act]) 2);
+by (blast_tac (claset() addDs [int_is_act,out_is_act]) 2);
(* Filter B (sch@@[a]) : schedules B *)
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML Sun Jul 12 11:49:17 1998 +0200
@@ -12,7 +12,7 @@
Goalw [live_implements_def]
"!! A. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
\ ==> live_implements (A,LA) (C,LC)";
-auto();
+by Auto_tac;
qed"live_implements_trans";
@@ -51,7 +51,7 @@
by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
(* Liveness *)
-auto();
+by Auto_tac;
qed"live_implements";
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Sun Jul 12 11:49:17 1998 +0200
@@ -256,7 +256,7 @@
Goalw [fin_often_def] "(~inf_often P s) = fin_often P s";
-auto();
+by Auto_tac;
qed"fininf";
@@ -264,17 +264,17 @@
"is_wfair A W (s,ex) = \
\ (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)";
by (asm_full_simp_tac (simpset() addsimps [is_wfair_def,fin_often_def])1);
-auto();
+by Auto_tac;
qed"WF_alt";
Goal
"!! ex. [|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
\ en_persistent A W|] \
\ ==> inf_often (%x. fst x :W) ex";
-bd persistent 1;
-ba 1;
+by (dtac persistent 1);
+by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [WF_alt])1);
-auto();
+by Auto_tac;
qed"WF_persistent";
@@ -305,7 +305,7 @@
by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
(* Fairness *)
-auto();
+by Auto_tac;
qed"fair_trace_inclusion";
Goal "!! C A. \
@@ -335,7 +335,7 @@
by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
(* Fairness *)
-auto();
+by Auto_tac;
qed"fair_trace_inclusion2";
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Sun Jul 12 11:49:17 1998 +0200
@@ -27,9 +27,9 @@
\ @@ ((corresp_ex_simC A R `xs) T')) \
\ `x) ))";
by (rtac trans 1);
-br fix_eq2 1;
-br corresp_ex_simC_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac corresp_ex_simC_def 1);
+by (rtac beta_cfun 1);
by (simp_tac (simpset() addsimps [flift1_def]) 1);
qed"corresp_ex_simC_unfold";
@@ -48,7 +48,7 @@
\ in \
\ (@cex. move A cex s a T') \
\ @@ ((corresp_ex_simC A R`xs) T'))";
-br trans 1;
+by (rtac trans 1);
by (stac corresp_ex_simC_unfold 1);
by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
by (Simp_tac 1);
@@ -84,15 +84,15 @@
by (eres_inst_tac [("x","a")] allE 2);
by (Asm_full_simp_tac 2);
(* Go on as usual *)
-be exE 1;
+by (etac exE 1);
by (dres_inst_tac [("x","t'"),
("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] selectI 1);
-be exE 1;
-be conjE 1;
+by (etac exE 1);
+by (etac conjE 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def]) 1);
by (res_inst_tac [("x","ex")] selectI 1);
-be conjE 1;
-ba 1;
+by (etac conjE 1);
+by (assume_tac 1);
qed"move_is_move_sim";
@@ -168,7 +168,7 @@
ren "ex a t s s'" 1;
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","t")] allE 1);
by (eres_inst_tac [("x",
"@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")]
@@ -202,12 +202,12 @@
lemma_2_1 1);
(* Finite *)
-be (rewrite_rule [Let_def] move_subprop2_sim) 1;
+by (etac (rewrite_rule [Let_def] move_subprop2_sim) 1);
by (REPEAT (atac 1));
by (rtac conjI 1);
(* is_exec_frag *)
-be (rewrite_rule [Let_def] move_subprop1_sim) 1;
+by (etac (rewrite_rule [Let_def] move_subprop1_sim) 1);
by (REPEAT (atac 1));
by (rtac conjI 1);
@@ -219,11 +219,11 @@
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 (simpset() addsimps
[rewrite_rule [Let_def] move_subprop5_sim]) 1);
(* laststate *)
-be ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1;
+by (etac ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1);
by (REPEAT (atac 1));
qed_spec_mp"correspsim_is_execution";
@@ -246,11 +246,11 @@
by (asm_full_simp_tac (simpset() addsimps [is_simulation_def,
corresp_ex_sim_def, Int_non_empty,Image_def]) 1);
by (REPEAT (etac conjE 1));
- be ballE 1;
+ by (etac ballE 1);
by (Blast_tac 2);
- be exE 1;
- br selectI2 1;
- ba 1;
+ by (etac exE 1);
+ by (rtac selectI2 1);
+ by (assume_tac 1);
by (Blast_tac 1);
qed"simulation_starts";
@@ -290,7 +290,7 @@
(* is-execution-fragment *)
by (asm_full_simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1);
by (res_inst_tac [("s","s")] correspsim_is_execution 1);
- ba 1;
+ by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0,sim_starts1]) 1);
qed"trace_inclusion_for_simulations";
--- a/src/HOLCF/IOA/meta_theory/Simulations.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Simulations.ML Sun Jul 12 11:49:17 1998 +0200
@@ -10,7 +10,7 @@
Goal "(A~={}) = (? x. x:A)";
by (safe_tac set_cs);
-auto();
+by Auto_tac;
qed"set_non_empty";
Goal "(A Int B ~= {}) = (? x. x: A & x:B)";
--- a/src/HOLCF/IOA/meta_theory/TL.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.ML Sun Jul 12 11:49:17 1998 +0200
@@ -8,9 +8,9 @@
Goal "[] <> (.~ P) = (.~ <> [] P)";
-br ext 1;
+by (rtac ext 1);
by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
-auto();
+by Auto_tac;
qed"simple_try";
Goal "nil |= [] P";
@@ -39,7 +39,7 @@
Goal "suffix s s";
by (simp_tac (simpset() addsimps [suffix_def])1);
by (res_inst_tac [("x","nil")] exI 1);
-auto();
+by Auto_tac;
qed"suffix_refl";
Goal "s~=UU & s~=nil --> (s |= [] F .--> F)";
@@ -52,19 +52,19 @@
Goal "!!x. [| suffix y x ; suffix z y |] ==> suffix z x";
by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
-auto();
+by Auto_tac;
by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
-auto();
+by Auto_tac;
by (simp_tac (simpset() addsimps [Conc_assoc]) 1);
qed"suffix_trans";
Goal "s |= [] F .--> [] [] F";
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def,tsuffix_def])1);
-auto();
-bd suffix_trans 1;
-ba 1;
+by Auto_tac;
+by (dtac suffix_trans 1);
+by (assume_tac 1);
by (eres_inst_tac [("x","s2a")] allE 1);
-auto();
+by Auto_tac;
qed"transT";
@@ -76,13 +76,13 @@
(*
Goal "s |= <> F .& <> G .--> (<> (F .& <> G) .| <> (G .& <> F))";
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,AND_def,OR_def,Diamond_def2])1);
-br impI 1;
-be conjE 1;
-be exE 1;
-be exE 1;
+by (rtac impI 1);
+by (etac conjE 1);
+by (etac exE 1);
+by (etac exE 1);
-br disjI1 1;
+by (rtac disjI1 1);
Goal "!!s. [| tsuffix s1 s ; tsuffix s2 s|] ==> tsuffix s2 s1 | tsuffix s1 s2";
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
@@ -109,8 +109,8 @@
qed"STL1b";
Goal "!! P. valid P ==> validT ([] (Init P))";
-br STL1a 1;
-be STL1b 1;
+by (rtac STL1a 1);
+by (etac STL1b 1);
qed"STL1";
@@ -130,10 +130,10 @@
Goalw [tsuffix_def,suffix_def]
"s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s";
-auto();
+by Auto_tac;
by (Seq_case_simp_tac "s" 1);
by (res_inst_tac [("x","a>>s1")] exI 1);
-auto();
+by Auto_tac;
qed_spec_mp"tsuffix_TL";
val tsuffix_TL2 = conjI RS tsuffix_TL;
@@ -141,16 +141,16 @@
Delsplits[split_if];
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def]
"s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
-auto();
+by Auto_tac;
(* []F .--> F *)
by (eres_inst_tac [("x","s")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
(* []F .--> Next [] F *)
by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
-auto();
-bd tsuffix_TL2 1;
+by Auto_tac;
+by (dtac tsuffix_TL2 1);
by (REPEAT (atac 1));
-auto();
+by Auto_tac;
qed"LTL1";
Addsplits[split_if];
@@ -173,11 +173,11 @@
Goalw [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def]
"s |= [] (F .--> Next F) .--> F .--> []F";
by (Asm_full_simp_tac 1);
-auto();
+by Auto_tac;
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
-auto();
+by Auto_tac;
--- a/src/HOLCF/IOA/meta_theory/TrivEx.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx.ML Sun Jul 12 11:49:17 1998 +0200
@@ -7,7 +7,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";
@@ -24,14 +24,14 @@
C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
by (simp_tac (simpset() addsimps [h_abs_def]) 1);
by (action.induct_tac "a" 1);
-auto();
+by Auto_tac;
qed"h_abs_is_abstraction";
Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
-br AbsRuleT1 1;
-br h_abs_is_abstraction 1;
-br MC_result 1;
+by (rtac AbsRuleT1 1);
+by (rtac h_abs_is_abstraction 1);
+by (rtac MC_result 1);
by (abstraction_tac 1);
by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
qed"TrivEx_abstraction";
--- a/src/HOLCF/IOA/meta_theory/TrivEx2.ML Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML Sun Jul 12 11:49:17 1998 +0200
@@ -7,7 +7,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";
@@ -24,7 +24,7 @@
C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
by (simp_tac (simpset() addsimps [h_abs_def]) 1);
by (action.induct_tac "a" 1);
-auto();
+by Auto_tac;
qed"h_abs_is_abstraction";
@@ -39,26 +39,26 @@
Goalw [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def,
C_trans_def,trans_of_def]
"!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s";
-auto();
+by Auto_tac;
qed"Enabled_implication";
Goalw [is_live_abstraction_def]
"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";
-auto();
+by Auto_tac;
(* is_abstraction *)
-br h_abs_is_abstraction 1;
+by (rtac h_abs_is_abstraction 1);
(* temp_weakening *)
by (abstraction_tac 1);
-be Enabled_implication 1;
+by (etac Enabled_implication 1);
qed"h_abs_is_liveabstraction";
Goalw [C_live_ioa_def]
"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
-br AbsRuleT2 1;
-br h_abs_is_liveabstraction 1;
-br MC_result 1;
+by (rtac AbsRuleT2 1);
+by (rtac h_abs_is_liveabstraction 1);
+by (rtac MC_result 1);
by (abstraction_tac 1);
by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
qed"TrivEx2_abstraction";