src/HOLCF/IOA/meta_theory/Sequence.ML

 goal thy "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
 by (rtac iffI 1);
 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());
+by Auto_tac;
 qed"FiniteConc";
 
 Addsimps [FiniteConc];
 
 

 by (Seq_Finite_induct_tac 1);
 by (strip_tac 1);
 by (Seq_case_simp_tac "t" 1);
 by (Asm_full_simp_tac 1);
 (* main case *)
-by (Auto_tac());
+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";
-by (Auto_tac());
+by Auto_tac;
 by (etac (FiniteMap2 RS spec RS mp) 1);
 by (rtac refl 1);
 by (etac FiniteMap1 1);
 qed"Map2Finite";
 

 by (Seq_Finite_induct_tac 1);
 by (strip_tac 1);
 by (etac conjE 1);
 by (etac nil_less_is_nil 1);
 (* main case *)
-by (Auto_tac());
+by Auto_tac;
 by (Seq_case_simp_tac "y" 1);
-by (Auto_tac());
+by Auto_tac;
 qed_spec_mp"Finite_flat";
 
 
 goal thy "adm(%(x:: 'a Seq).Finite x)";
 by (rtac admI2 1);

 by (res_inst_tac [("x","0")] allE 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 *)
-by (Auto_tac());
+by Auto_tac;
 qed"adm_Finite";
 
 Addsimps [adm_Finite];
 
 

 Addsimps [nilConc];
 
 (* 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);
-by (Auto_tac());
+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);
-by (Auto_tac());
+by Auto_tac;
 qed"nil_is_Conc2";
 
 
 (* ------------------------------------------------------------------------------------ *)
 

 goal thy "! s. Forall P s --> t<<s --> Forall P t";
 by (Seq_induct_tac "t" [Forall_def,sforall_def] 1);
 by (strip_tac 1); 
 by (Seq_case_simp_tac "sa" 1);
 by (Asm_full_simp_tac 1);
-by (Auto_tac());
+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";
-by (Auto_tac());
+by Auto_tac;
 qed"Forall_postfixclosed";
 
 
 goal thy "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q`tr = Filter R`tr";
 by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1);

 
 goal thy   "!! P. Filter P`ys = UU ==> \
 \                (Forall (%x. ~P x) ys  & ~Finite ys)";
 by (rtac conjI 1);
 by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
-by (Auto_tac());
+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";
 by (etac ForallnPFilterPnil 1);
 by (etac ForallPForallQ 1);
-by (Auto_tac());
+by Auto_tac;
 qed"ForallQFilterPnil";
 
 goal thy "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
 \   ==> Filter P`ys = UU ";
 by (etac ForallnPFilterPUU 1);
 by (etac ForallPForallQ 1);
-by (Auto_tac());
+by Auto_tac;
 qed"ForallQFilterPUU";
 
 
 
 (* ------------------------------------------------------------------------------------- *)

 
 
 goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
 by (rtac ForallPForallQ 1);
 by (rtac ForallPTakewhileP 1);
-by (Auto_tac());
+by Auto_tac;
 qed"ForallPTakewhileQ";
 
 
 goal thy  "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
 \   ==> Filter P`(Takewhile Q`ys) = nil";
 by (etac ForallnPFilterPnil 1);
 by (rtac ForallPForallQ 1);
 by (rtac ForallPTakewhileP 1);
-by (Auto_tac());
+by Auto_tac;
 qed"FilterPTakewhileQnil";
 
 goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
 \            Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)";
 by (rtac ForallPFilterPid 1);
 by (rtac ForallPForallQ 1);
 by (rtac ForallPTakewhileP 1);
-by (Auto_tac());
+by Auto_tac;
 qed"FilterPTakewhileQid";
 
 Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
           FilterPTakewhileQnil,FilterPTakewhileQid];
 

 \      Finite (Takewhile P`y) & (~ P x)";
 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);
-by (Auto_tac());
+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);
-by (Auto_tac());
+(*Auto_tac no longer proves it*)
+by (REPEAT (fast_tac (claset() addss (simpset())) 1));
 qed"divide_Seq3";
 
 Addsimps [FilterPQ,FilterConc,Conc_cong];
 
 

 section "take_lemma";
 
 goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
 by (rtac iffI 1);
 by (resolve_tac seq.take_lemmas 1);
-by (Auto_tac());
+by Auto_tac;
 qed"seq_take_lemma";
 
 goal thy 
 "  ! n. ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
 \   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2)))";
 by (Seq_induct_tac "x" [] 1);
 by (strip_tac 1);
 by (res_inst_tac [("n","n")] natE 1);
-by (Auto_tac());
+by Auto_tac;
 by (res_inst_tac [("n","n")] natE 1);
-by (Auto_tac());
+by Auto_tac;
 qed"take_reduction1";
 
 
 goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 = seq_take k`y2|] \
 \ ==> seq_take n`(x @@ (s>>y1)) =  seq_take n`(y @@ (t>>y2))";

 "  ! n. ((! k. k < n --> seq_take k`y1 << seq_take k`y2) \
 \   --> seq_take n`(x @@ (t>>y1)) <<  seq_take n`(x @@ (t>>y2)))";
 by (Seq_induct_tac "x" [] 1);
 by (strip_tac 1);
 by (res_inst_tac [("n","n")] natE 1);
-by (Auto_tac());
+by Auto_tac;
 by (res_inst_tac [("n","n")] natE 1);
-by (Auto_tac());
+by Auto_tac;
 qed"take_reduction_less1";
 
 
 goal thy "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k`y1 << seq_take k`y2|] \
 \ ==> seq_take n`(x @@ (s>>y1)) <<  seq_take n`(y @@ (t>>y2))";

 
 
 goal thy "(!n. seq_take n`x << seq_take n`x') = (x << x')";
 by (rtac iffI 1);
 by (rtac take_lemma_less1 1);
-by (Auto_tac());
+by Auto_tac;
 by (etac monofun_cfun_arg 1);
 qed"take_lemma_less";
 
 (* ------------------------------------------------------------------
           take-lemma proof principles

 \                                = seq_take n`(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
 by (case_tac "Forall Q x" 1);
 by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
 by (resolve_tac seq.take_lemmas 1);
-by (Auto_tac());
+by Auto_tac;
 qed"take_lemma_principle2";
 
 
 (* Note: in the following proofs the ordering of proof steps is very 
          important, as otherwise either (Forall Q s1) would be in the IH as

 (* --------------------------------------------------------------- *)
 
 
 
 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);
-by (Auto_tac());
+by (res_inst_tac [("A1","%x. True"), ("x1","x")]
+    (take_lemma_in_eq_out RS mp) 1);
+by Auto_tac;
 qed"MapConc_takelemma";