src/HOL/BCV/Kildall.ML

--- a/src/HOL/BCV/Kildall.ML	Mon Oct 09 10:18:21 2000 +0200
+++ b/src/HOL/BCV/Kildall.ML	Mon Oct 09 12:23:45 2000 +0200
@@ -34,8 +34,8 @@
  "[| semilat(A,r,f) |] ==> \
 \ !xs. xs : list n A --> x : A --> (!p : set ps. p<n) \
 \      --> merges f x ps xs : list n A";
-by(ftac semilatDclosedI 1);
-by(rewtac closed_def);
+by (ftac semilatDclosedI 1);
+by (rewtac closed_def);
 by (induct_tac "ps" 1);
 by (Auto_tac);
 qed_spec_mp "merges_preserves_type";
@@ -49,9 +49,9 @@
 by (Asm_full_simp_tac 1);
 by (Clarify_tac 1);
 by (rtac order_trans 1);
-  by(Asm_simp_tac 1);
+  by (Asm_simp_tac 1);
  by (etac list_update_incr 1);
-   ba 1;
+   by (assume_tac 1);
   by (Asm_simp_tac 1);
  by (Asm_simp_tac 1);
 by (blast_tac (claset() addSIs [listE_set]
@@ -70,13 +70,13 @@
  by (rtac context_conjI 1);
   by (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs" 1);
    by (EVERY[etac subst 2, rtac merges_incr 2]);
-      by(force_tac (claset() addSDs [le_listD],
+      by (force_tac (claset() addSDs [le_listD],
                     simpset() addsimps [nth_list_update]) 1);
      by (assume_tac 1);
     by (blast_tac (claset() addSIs [listE_set]
                    addIs [closedD,listE_length RS nth_in]) 1);
-   ba 1;
-  by(Asm_simp_tac 1);
+   by (assume_tac 1);
+  by (Asm_simp_tac 1);
  by (Clarify_tac 1);
  by (rotate_tac ~2 1);
  by (asm_full_simp_tac (simpset() addsimps
@@ -108,7 +108,7 @@
 by (Clarify_tac 1);
 by (rotate_tac ~2 1);
 by (Asm_full_simp_tac 1);
-by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
+by (EVERY[etac allE 1, etac impE 1, etac mp 2]);
  by (asm_simp_tac (simpset() addsimps [closedD]) 1);
 by (asm_full_simp_tac (simpset() addsimps [list_update_le_listI]) 1);
 val lemma = result();
@@ -125,9 +125,9 @@
 Goal "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A --> \
 \     (!p:set ps. p<n) --> \
 \     (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)";
-by(induct_tac "ps" 1);
+by (induct_tac "ps" 1);
  by (Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [nth_list_update,closedD,listE_nth_in]) 1);
+by (asm_simp_tac (simpset() addsimps [nth_list_update,closedD,listE_nth_in]) 1);
 qed_spec_mp "nth_merges";
 
 
@@ -137,14 +137,14 @@
 \ propa f qs t ss w = \
 \ (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)";
 by (induct_tac "qs" 1);
- by(Simp_tac 1);
+ by (Simp_tac 1);
 by (Simp_tac 1);
-by(Clarify_tac 1);
-br conjI 1;
+by (Clarify_tac 1);
+by (rtac conjI 1);
  by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
- by(Blast_tac 1);
+ by (Blast_tac 1);
 by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "decomp_propa";
 
 (** iter **)
@@ -152,17 +152,17 @@
 val [iter_wf,iter_tc] = iter.tcs;
 
 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
-by(REPEAT(rtac wf_same_fstI 1));
-by(split_all_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1);
-by(REPEAT(rtac wf_same_fstI 1));
-br wf_lex_prod 1;
- br wf_finite_psubset 2; (* FIXME *)
-by(Clarify_tac 1);
-bd (semilatDorderI RS acc_le_listI) 1;
- ba 1;
-by(rewrite_goals_tac [acc_def,lesssub_def]);
-ba 1;
+by (REPEAT(rtac wf_same_fstI 1));
+by (split_all_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1);
+by (REPEAT(rtac wf_same_fstI 1));
+by (rtac wf_lex_prod 1);
+ by (rtac wf_finite_psubset 2); (* FIXME *)
+by (Clarify_tac 1);
+by (dtac (semilatDorderI RS acc_le_listI) 1);
+ by (assume_tac 1);
+by (rewrite_goals_tac [acc_def,lesssub_def]);
+by (assume_tac 1);
 qed "iter_wf";
 
 Goalw [lesssub_def]
@@ -170,28 +170,28 @@
 \ ss <[r] merges f t qs ss | \
 \ merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w";
 by (asm_simp_tac (simpset() addsimps [merges_incr]) 1);
-br impI 1;
-bd (sym RS (rotate_prems 4 (merges_same_conv RS iffD1))) 1;
-    ba 1;
-   ba 1;
-  ba 1;
- by(Asm_simp_tac 1);
+by (rtac impI 1);
+by (dtac (sym RS (rotate_prems 4 (merges_same_conv RS iffD1))) 1);
+    by (assume_tac 1);
+   by (assume_tac 1);
+  by (assume_tac 1);
+ by (Asm_simp_tac 1);
 by (asm_simp_tac (simpset() addcongs [conj_cong]
                             addsimps [le_iff_plus_unchanged RS sym]) 1);
 by (blast_tac (claset() addSIs [psubsetI] addEs [equalityE]) 1);
 qed "inter_tc_lemma";
 
 goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc));
-by(asm_simp_tac (simpset() addsimps [same_fst_def,pres_type_def]) 1);
-by(clarify_tac (claset() delrules [disjCI]) 1);
-by(subgoal_tac "(@p. p:w) : w" 1);
+by (asm_simp_tac (simpset() addsimps [same_fst_def,pres_type_def]) 1);
+by (clarify_tac (claset() delrules [disjCI]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
  by (fast_tac (claset() addIs [someI]) 2);
-by(subgoal_tac "ss : list (size ss) A" 1);
+by (subgoal_tac "ss : list (size ss) A" 1);
  by (blast_tac (claset() addSIs [listI]) 2);
-by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
  by (blast_tac (claset() addDs [boundedD]) 2);
-by(rotate_tac 1 1);
-by(asm_full_simp_tac (simpset() delsimps [listE_length]
+by (rotate_tac 1 1);
+by (asm_full_simp_tac (simpset() delsimps [listE_length]
       addsimps [decomp_propa,finite_psubset_def,inter_tc_lemma,
                 bounded_nat_set_is_finite]) 1);
 qed "iter_tc";
@@ -204,15 +204,15 @@
 \     --> P A r f step succs (merges f (step p (ss!p)) (succs p) ss) \
 \           ({q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))\
 \    ==> P A r f step succs ss w) ==> P A r f step succs ss w";
-by(res_inst_tac [("P","P")] (iter_tc RS (iter_wf RS iter.induct)) 1);
-by(rename_tac "w" 1);
-brs prems 1;
-by(Clarify_tac 1);
-by(asm_full_simp_tac (simpset()) 1);
-by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
- by(rotate_tac ~1 1);
- by(asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1);
-by(subgoal_tac "(@p. p:w) : w" 1);
+by (res_inst_tac [("P","P")] (iter_tc RS (iter_wf RS iter.induct)) 1);
+by (rename_tac "w" 1);
+by (resolve_tac prems 1);
+by (Clarify_tac 1);
+by (asm_full_simp_tac (simpset()) 1);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+ by (rotate_tac ~1 1);
+ by (asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
  by (fast_tac (claset() addIs [someI]) 2);
 by (blast_tac (claset() addDs [boundedD]) 1);
 qed "iter_induct";
@@ -227,9 +227,9 @@
 \        {q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))";
 by (rtac ((iter_tc RS (iter_wf RS (hd iter.simps))) RS trans) 1);
 by (Asm_simp_tac 1);
-br impI 1;
-by(stac decomp_propa 1);
- by(subgoal_tac "(@p. p:w) : w" 1);
+by (rtac impI 1);
+by (stac decomp_propa 1);
+ by (subgoal_tac "(@p. p:w) : w" 1);
   by (fast_tac (claset() addIs [someI]) 2);
  by (blast_tac (claset() addDs [boundedD]) 1);
 by (Simp_tac 1);
@@ -242,26 +242,26 @@
 \    q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q; \
 \    q ~: w | q = p  |] ==> \
 \      stable r step succs (merges f (step p (ss!p)) (succs p) ss) q";
-by(subgoal_tac "step p (ss!p) : A" 1);
+by (subgoal_tac "step p (ss!p) : A" 1);
  by (blast_tac (claset() addIs [listE_nth_in,pres_typeD]) 2);
 by (Simp_tac 1);
-by(Clarify_tac 1);
-by(stac nth_merges 1);
-     ba 1;
-    ba 1;
-   ba 2;
+by (Clarify_tac 1);
+by (stac nth_merges 1);
+     by (assume_tac 1);
+    by (assume_tac 1);
+   by (assume_tac 2);
   by (blast_tac (claset() addDs [boundedD]) 1);
  by (blast_tac (claset() addDs [boundedD]) 1);
-by(stac nth_merges 1);
-     ba 1;
-    ba 1;
-   ba 2;
+by (stac nth_merges 1);
+     by (assume_tac 1);
+    by (assume_tac 1);
+   by (assume_tac 2);
   by (blast_tac (claset() addDs [boundedD]) 1);
  by (blast_tac (claset() addDs [boundedD]) 1);
 by (Simp_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
  by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1);
 by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1);
 qed "stable_pres_lemma";
@@ -289,43 +289,43 @@
 \     (! ts:list n A. \
 \          ss <=[r] ts & stables r step succs ts --> \
 \          iter(((A,r,f),step,succs),ss,w) <=[r] ts)";
-by(res_inst_tac [("A","A"),("r","r"),("f","f"),("step","step"),("ss","ss"),("w","w")]iter_induct 1);
-by(Clarify_tac 1);
-by(ftac listE_length 1);
-by(hyp_subst_tac 1);
-by(stac iter_unfold 1);
-      ba 1;
-     ba 1;
+by (res_inst_tac [("A","A"),("r","r"),("f","f"),("step","step"),("ss","ss"),("w","w")]iter_induct 1);
+by (Clarify_tac 1);
+by (ftac listE_length 1);
+by (hyp_subst_tac 1);
+by (stac iter_unfold 1);
+      by (assume_tac 1);
+     by (assume_tac 1);
     by (Asm_simp_tac 1);
-   ba 1;
-  ba 1;
- ba 1;
-by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
-br impI 1;
-be allE 1;
-be impE 1;
- by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
-by(subgoal_tac "(@p. p:w) : w" 1);
+   by (assume_tac 1);
+  by (assume_tac 1);
+ by (assume_tac 1);
+by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (rtac impI 1);
+by (etac allE 1);
+by (etac impE 1);
+ by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
  by (fast_tac (claset() addIs [someI]) 2);
-by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
+by (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
  by (blast_tac (claset() addIs [pres_typeD,listE_nth_in]) 2);
-be impE 1;
- by(asm_simp_tac (simpset() delsimps [listE_length,le_iff_plus_unchanged RS sym]) 1);
- br conjI 1;
+by (etac impE 1);
+ by (asm_simp_tac (simpset() delsimps [listE_length,le_iff_plus_unchanged RS sym]) 1);
+ by (rtac conjI 1);
   by (blast_tac (claset() addDs [boundedD]) 1);
- br conjI 1;
-  by(blast_tac (claset() addIs[merges_preserves_type]addDs[boundedD]) 1);
+ by (rtac conjI 1);
+  by (blast_tac (claset() addIs[merges_preserves_type]addDs[boundedD]) 1);
  by (blast_tac (claset() addSIs [stable_pres_lemma]) 1);
-by(asm_simp_tac (simpset() delsimps [listE_length]) 1);
-by(subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+by (asm_simp_tac (simpset() delsimps [listE_length]) 1);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
  by (blast_tac (claset() addDs [boundedD]) 2);
-by(subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
+by (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1);
  by (blast_tac (claset() addIs [pres_typeD]) 2);
-br conjI 1;
+by (rtac conjI 1);
  by (blast_tac (claset() addSIs [merges_incr] addIs [le_list_trans]) 1);
-by(Clarify_tac 1);
-by(EVERY1[dtac bspec, atac, etac mp]);
-by(asm_full_simp_tac (simpset() delsimps [listE_length]) 1);
+by (Clarify_tac 1);
+by (EVERY1[dtac bspec, atac, etac mp]);
+by (asm_full_simp_tac (simpset() delsimps [listE_length]) 1);
 by (blast_tac (claset() addIs [merges_bounded_lemma]) 1);
 qed_spec_mp "iter_properties";
 
@@ -334,11 +334,11 @@
  "[| semilat(A,r,f); acc r; pres_type step n A; \
 \    mono r step n A; bounded succs n|] ==> \
 \ is_dfa r (kildall (A,r,f) step succs) step succs n A";
-by(Clarify_tac 1);
-by(Simp_tac 1);
-br iter_properties 1;
-by(asm_simp_tac (simpset() addsimps [unstables_def,stable_def]) 1);
-by(blast_tac (claset() addSIs [le_iff_plus_unchanged RS iffD2,listE_nth_in]
+by (Clarify_tac 1);
+by (Simp_tac 1);
+by (rtac iter_properties 1);
+by (asm_simp_tac (simpset() addsimps [unstables_def,stable_def]) 1);
+by (blast_tac (claset() addSIs [le_iff_plus_unchanged RS iffD2,listE_nth_in]
               addDs [boundedD,pres_typeD]) 1);
 qed "is_dfa_kildall";