src/HOLCF/IOA/meta_theory/Sequence.ML
changeset 4477 b3e5857d8d99
parent 4098 71e05eb27fb6
child 4681 a331c1f5a23e
     1.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -432,7 +432,7 @@
     1.4  by (etac (FiniteConc_2 RS spec RS spec RS mp) 1);
     1.5  by (rtac refl 1);
     1.6  by (rtac (FiniteConc_1 RS mp) 1);
     1.7 -by (Auto_tac());
     1.8 +by Auto_tac;
     1.9  qed"FiniteConc";
    1.10  
    1.11  Addsimps [FiniteConc];
    1.12 @@ -448,13 +448,13 @@
    1.13  by (Seq_case_simp_tac "t" 1);
    1.14  by (Asm_full_simp_tac 1);
    1.15  (* main case *)
    1.16 -by (Auto_tac());
    1.17 +by Auto_tac;
    1.18  by (Seq_case_simp_tac "t" 1);
    1.19  by (Asm_full_simp_tac 1);
    1.20  qed"FiniteMap2";
    1.21  
    1.22  goal thy "Finite (Map f`s) = Finite s";
    1.23 -by (Auto_tac());
    1.24 +by Auto_tac;
    1.25  by (etac (FiniteMap2 RS spec RS mp) 1);
    1.26  by (rtac refl 1);
    1.27  by (etac FiniteMap1 1);
    1.28 @@ -482,9 +482,9 @@
    1.29  by (etac conjE 1);
    1.30  by (etac nil_less_is_nil 1);
    1.31  (* main case *)
    1.32 -by (Auto_tac());
    1.33 +by Auto_tac;
    1.34  by (Seq_case_simp_tac "y" 1);
    1.35 -by (Auto_tac());
    1.36 +by Auto_tac;
    1.37  qed_spec_mp"Finite_flat";
    1.38  
    1.39  
    1.40 @@ -499,7 +499,7 @@
    1.41  by (eres_inst_tac [("x","j")] allE 1);
    1.42  by (cut_inst_tac [("x","Y 0"),("y","Y j")] Finite_flat 1);
    1.43  (* Generates a contradiction in subgoal 3 *)
    1.44 -by (Auto_tac());
    1.45 +by Auto_tac;
    1.46  qed"adm_Finite";
    1.47  
    1.48  Addsimps [adm_Finite];
    1.49 @@ -530,12 +530,12 @@
    1.50  (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
    1.51  goal thy "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
    1.52  by (Seq_case_simp_tac "x" 1);
    1.53 -by (Auto_tac());
    1.54 +by Auto_tac;
    1.55  qed"nil_is_Conc";
    1.56  
    1.57  goal thy "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
    1.58  by (Seq_case_simp_tac "x" 1);
    1.59 -by (Auto_tac());
    1.60 +by Auto_tac;
    1.61  qed"nil_is_Conc2";
    1.62  
    1.63  
    1.64 @@ -642,14 +642,14 @@
    1.65  by (strip_tac 1); 
    1.66  by (Seq_case_simp_tac "sa" 1);
    1.67  by (Asm_full_simp_tac 1);
    1.68 -by (Auto_tac());
    1.69 +by Auto_tac;
    1.70  qed"Forall_prefix";
    1.71   
    1.72  bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
    1.73  
    1.74  
    1.75  goal thy "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
    1.76 -by (Auto_tac());
    1.77 +by Auto_tac;
    1.78  qed"Forall_postfixclosed";
    1.79  
    1.80  
    1.81 @@ -728,7 +728,7 @@
    1.82  \                (Forall (%x. ~P x) ys  & ~Finite ys)";
    1.83  by (rtac conjI 1);
    1.84  by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
    1.85 -by (Auto_tac());
    1.86 +by Auto_tac;
    1.87  by (blast_tac (claset() addSDs [FilterUU_nFinite_lemma1]) 1);
    1.88  qed"FilternPUUForallP";
    1.89  
    1.90 @@ -737,14 +737,14 @@
    1.91  \   ==> Filter P`ys = nil";
    1.92  by (etac ForallnPFilterPnil 1);
    1.93  by (etac ForallPForallQ 1);
    1.94 -by (Auto_tac());
    1.95 +by Auto_tac;
    1.96  qed"ForallQFilterPnil";
    1.97  
    1.98  goal thy "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
    1.99  \   ==> Filter P`ys = UU ";
   1.100  by (etac ForallnPFilterPUU 1);
   1.101  by (etac ForallPForallQ 1);
   1.102 -by (Auto_tac());
   1.103 +by Auto_tac;
   1.104  qed"ForallQFilterPUU";
   1.105  
   1.106  
   1.107 @@ -762,7 +762,7 @@
   1.108  goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
   1.109  by (rtac ForallPForallQ 1);
   1.110  by (rtac ForallPTakewhileP 1);
   1.111 -by (Auto_tac());
   1.112 +by Auto_tac;
   1.113  qed"ForallPTakewhileQ";
   1.114  
   1.115  
   1.116 @@ -771,7 +771,7 @@
   1.117  by (etac ForallnPFilterPnil 1);
   1.118  by (rtac ForallPForallQ 1);
   1.119  by (rtac ForallPTakewhileP 1);
   1.120 -by (Auto_tac());
   1.121 +by Auto_tac;
   1.122  qed"FilterPTakewhileQnil";
   1.123  
   1.124  goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
   1.125 @@ -779,7 +779,7 @@
   1.126  by (rtac ForallPFilterPid 1);
   1.127  by (rtac ForallPForallQ 1);
   1.128  by (rtac ForallPTakewhileP 1);
   1.129 -by (Auto_tac());
   1.130 +by Auto_tac;
   1.131  qed"FilterPTakewhileQid";
   1.132  
   1.133  Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
   1.134 @@ -864,14 +864,15 @@
   1.135  by (safe_tac set_cs);
   1.136  by (res_inst_tac [("x","x")] exI 1);
   1.137  by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
   1.138 -by (Auto_tac());
   1.139 +by Auto_tac;
   1.140  qed"divide_Seq2";
   1.141  
   1.142  
   1.143  goal thy  "!! y. ~Forall P y \
   1.144  \  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
   1.145  by (cut_inst_tac [] divide_Seq2 1);
   1.146 -by (Auto_tac());
   1.147 +(*Auto_tac no longer proves it*)
   1.148 +by (REPEAT (fast_tac (claset() addss (simpset())) 1));
   1.149  qed"divide_Seq3";
   1.150  
   1.151  Addsimps [FilterPQ,FilterConc,Conc_cong];
   1.152 @@ -885,7 +886,7 @@
   1.153  goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
   1.154  by (rtac iffI 1);
   1.155  by (resolve_tac seq.take_lemmas 1);
   1.156 -by (Auto_tac());
   1.157 +by Auto_tac;
   1.158  qed"seq_take_lemma";
   1.159  
   1.160  goal thy 
   1.161 @@ -894,9 +895,9 @@
   1.162  by (Seq_induct_tac "x" [] 1);
   1.163  by (strip_tac 1);
   1.164  by (res_inst_tac [("n","n")] natE 1);
   1.165 -by (Auto_tac());
   1.166 +by Auto_tac;
   1.167  by (res_inst_tac [("n","n")] natE 1);
   1.168 -by (Auto_tac());
   1.169 +by Auto_tac;
   1.170  qed"take_reduction1";
   1.171  
   1.172  
   1.173 @@ -916,9 +917,9 @@
   1.174  by (Seq_induct_tac "x" [] 1);
   1.175  by (strip_tac 1);
   1.176  by (res_inst_tac [("n","n")] natE 1);
   1.177 -by (Auto_tac());
   1.178 +by Auto_tac;
   1.179  by (res_inst_tac [("n","n")] natE 1);
   1.180 -by (Auto_tac());
   1.181 +by Auto_tac;
   1.182  qed"take_reduction_less1";
   1.183  
   1.184  
   1.185 @@ -949,7 +950,7 @@
   1.186  goal thy "(!n. seq_take n`x << seq_take n`x') = (x << x')";
   1.187  by (rtac iffI 1);
   1.188  by (rtac take_lemma_less1 1);
   1.189 -by (Auto_tac());
   1.190 +by Auto_tac;
   1.191  by (etac monofun_cfun_arg 1);
   1.192  qed"take_lemma_less";
   1.193  
   1.194 @@ -973,7 +974,7 @@
   1.195  by (case_tac "Forall Q x" 1);
   1.196  by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
   1.197  by (resolve_tac seq.take_lemmas 1);
   1.198 -by (Auto_tac());
   1.199 +by Auto_tac;
   1.200  qed"take_lemma_principle2";
   1.201  
   1.202  
   1.203 @@ -1190,8 +1191,9 @@
   1.204  
   1.205  
   1.206  goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
   1.207 -by (res_inst_tac [("A1","%x. True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
   1.208 -by (Auto_tac());
   1.209 +by (res_inst_tac [("A1","%x. True"), ("x1","x")]
   1.210 +    (take_lemma_in_eq_out RS mp) 1);
   1.211 +by Auto_tac;
   1.212  qed"MapConc_takelemma";
   1.213  
   1.214