src/HOL/Lex/RegExp2NA.ML
changeset 6162 484adda70b65
parent 5758 27a2b36efd95
child 7958 f531589c9fc1
     1.1 --- a/src/HOL/Lex/RegExp2NA.ML	Fri Jan 29 16:23:56 1999 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Fri Jan 29 16:26:12 1999 +0100
     1.3 @@ -9,37 +9,37 @@
     1.4  (******************************************************)
     1.5  
     1.6  Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
     1.7 -by(Simp_tac 1);
     1.8 +by (Simp_tac 1);
     1.9  qed "fin_atom";
    1.10  
    1.11  Goalw [atom_def] "start (atom a) = [True]";
    1.12 -by(Simp_tac 1);
    1.13 +by (Simp_tac 1);
    1.14  qed "start_atom";
    1.15  
    1.16  Goalw [atom_def,step_def]
    1.17   "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)";
    1.18 -by(Simp_tac 1);
    1.19 +by (Simp_tac 1);
    1.20  qed "in_step_atom_Some";
    1.21  Addsimps [in_step_atom_Some];
    1.22  
    1.23  Goal
    1.24   "([False],[False]) : steps (atom a) w = (w = [])";
    1.25  by (induct_tac "w" 1);
    1.26 - by(Simp_tac 1);
    1.27 -by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
    1.28 + by (Simp_tac 1);
    1.29 +by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
    1.30  qed "False_False_in_steps_atom";
    1.31  
    1.32  Goal
    1.33   "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
    1.34  by (induct_tac "w" 1);
    1.35 - by(asm_simp_tac (simpset() addsimps [start_atom]) 1);
    1.36 -by(asm_full_simp_tac (simpset()
    1.37 + by (asm_simp_tac (simpset() addsimps [start_atom]) 1);
    1.38 +by (asm_full_simp_tac (simpset()
    1.39       addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
    1.40  qed "start_fin_in_steps_atom";
    1.41  
    1.42  Goal
    1.43   "accepts (atom a) w = (w = [a])";
    1.44 -by(simp_tac(simpset() addsimps
    1.45 +by (simp_tac(simpset() addsimps
    1.46         [accepts_conv_steps,start_fin_in_steps_atom,fin_atom]) 1);
    1.47  qed "accepts_atom";
    1.48  
    1.49 @@ -67,13 +67,13 @@
    1.50  Goalw [union_def,step_def]
    1.51  "!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
    1.52  by (Simp_tac 1);
    1.53 -by(Blast_tac 1);
    1.54 +by (Blast_tac 1);
    1.55  qed_spec_mp "True_in_step_union";
    1.56  
    1.57  Goalw [union_def,step_def]
    1.58  "!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
    1.59  by (Simp_tac 1);
    1.60 -by(Blast_tac 1);
    1.61 +by (Blast_tac 1);
    1.62  qed_spec_mp "False_in_step_union";
    1.63  
    1.64  AddIffs [True_in_step_union,False_in_step_union];
    1.65 @@ -102,8 +102,8 @@
    1.66   "!L R. (start(union L R),q) : step(union L R) a = \
    1.67  \       (? p. (q = True#p & (start L,p) : step L a) | \
    1.68  \             (q = False#p & (start R,p) : step R a))";
    1.69 -by(Simp_tac 1);
    1.70 -by(Blast_tac 1);
    1.71 +by (Simp_tac 1);
    1.72 +by (Blast_tac 1);
    1.73  qed_spec_mp "start_step_union";
    1.74  AddIffs [start_step_union];
    1.75  
    1.76 @@ -112,17 +112,17 @@
    1.77  \ ( (w = [] & q = start(union L R)) | \
    1.78  \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
    1.79  \                     q = False # p & (start R,p) : steps R w)))";
    1.80 -by(exhaust_tac "w" 1);
    1.81 +by (exhaust_tac "w" 1);
    1.82   by (Asm_simp_tac 1);
    1.83 - by(Blast_tac 1);
    1.84 + by (Blast_tac 1);
    1.85  by (Asm_simp_tac 1);
    1.86 -by(Blast_tac 1);
    1.87 +by (Blast_tac 1);
    1.88  qed "steps_union";
    1.89  
    1.90  Goalw [union_def]
    1.91   "!L R. fin (union L R) (start(union L R)) = \
    1.92  \       (fin L (start L) | fin R (start R))";
    1.93 -by(Simp_tac 1);
    1.94 +by (Simp_tac 1);
    1.95  qed_spec_mp "fin_start_union";
    1.96  AddIffs [fin_start_union];
    1.97  
    1.98 @@ -130,8 +130,8 @@
    1.99   "accepts (union L R) w = (accepts L w | accepts R w)";
   1.100  by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
   1.101  (* get rid of case_tac: *)
   1.102 -by(case_tac "w = []" 1);
   1.103 -by(Auto_tac);
   1.104 +by (case_tac "w = []" 1);
   1.105 +by (Auto_tac);
   1.106  qed "accepts_union";
   1.107  AddIffs [accepts_union];
   1.108  
   1.109 @@ -160,14 +160,14 @@
   1.110  \       ((? r. q=True#r & (p,r): step L a) | \
   1.111  \        (fin L p & (? r. q=False#r & (start R,r) : step R a)))";
   1.112  by (Simp_tac 1);
   1.113 -by(Blast_tac 1);
   1.114 +by (Blast_tac 1);
   1.115  qed_spec_mp "True_step_conc";
   1.116  
   1.117  Goalw [conc_def,step_def]
   1.118   "!L R. (False#p,q) : step (conc L R) a = \
   1.119  \       (? r. q = False#r & (p,r) : step R a)";
   1.120  by (Simp_tac 1);
   1.121 -by(Blast_tac 1);
   1.122 +by (Blast_tac 1);
   1.123  qed_spec_mp "False_step_conc";
   1.124  
   1.125  AddIffs [True_step_conc, False_step_conc];
   1.126 @@ -185,16 +185,16 @@
   1.127  
   1.128  Goal
   1.129   "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
   1.130 -by(induct_tac "w" 1);
   1.131 +by (induct_tac "w" 1);
   1.132   by (Simp_tac 1);
   1.133  by (Simp_tac 1);
   1.134 -by(Blast_tac 1);
   1.135 +by (Blast_tac 1);
   1.136  qed_spec_mp "True_True_steps_concI";
   1.137  
   1.138  Goal
   1.139   "!L R. (True#p,False#q) : step (conc L R) a = \
   1.140  \       (fin L p & (start R,q) : step R a)";
   1.141 -by(Simp_tac 1);
   1.142 +by (Simp_tac 1);
   1.143  qed "True_False_step_conc";
   1.144  AddIffs [True_False_step_conc];
   1.145  
   1.146 @@ -205,26 +205,26 @@
   1.147  \            (? r. (p,r) : steps L u & fin L r & \
   1.148  \            (? s. (start R,s) : step R a & \
   1.149  \            (? t. (s,t) : steps R v & q = False#t)))))";
   1.150 -by(induct_tac "w" 1);
   1.151 - by(Simp_tac 1);
   1.152 -by(Simp_tac 1);
   1.153 -by(clarify_tac (claset() delrules [disjCI]) 1);
   1.154 -be disjE 1;
   1.155 - by(clarify_tac (claset() delrules [disjCI]) 1);
   1.156 - by(etac allE 1 THEN mp_tac 1);
   1.157 - be disjE 1;
   1.158 +by (induct_tac "w" 1);
   1.159 + by (Simp_tac 1);
   1.160 +by (Simp_tac 1);
   1.161 +by (clarify_tac (claset() delrules [disjCI]) 1);
   1.162 +by (etac disjE 1);
   1.163 + by (clarify_tac (claset() delrules [disjCI]) 1);
   1.164 + by (etac allE 1 THEN mp_tac 1);
   1.165 + by (etac disjE 1);
   1.166    by (Blast_tac 1);
   1.167 - br disjI2 1;
   1.168 + by (rtac disjI2 1);
   1.169   by (Clarify_tac 1);
   1.170 - by(Simp_tac 1);
   1.171 - by(res_inst_tac[("x","a#u")] exI 1);
   1.172 - by(Simp_tac 1);
   1.173 + by (Simp_tac 1);
   1.174 + by (res_inst_tac[("x","a#u")] exI 1);
   1.175 + by (Simp_tac 1);
   1.176   by (Blast_tac 1);
   1.177 -br disjI2 1;
   1.178 +by (rtac disjI2 1);
   1.179  by (Clarify_tac 1);
   1.180 -by(Simp_tac 1);
   1.181 -by(res_inst_tac[("x","[]")] exI 1);
   1.182 -by(Simp_tac 1);
   1.183 +by (Simp_tac 1);
   1.184 +by (res_inst_tac[("x","[]")] exI 1);
   1.185 +by (Simp_tac 1);
   1.186  by (Blast_tac 1);
   1.187  qed_spec_mp "True_steps_concD";
   1.188  
   1.189 @@ -235,7 +235,7 @@
   1.190  \            (? r. (p,r) : steps L u & fin L r & \
   1.191  \            (? s. (start R,s) : step R a & \
   1.192  \            (? t. (s,t) : steps R v & q = False#t)))))";
   1.193 -by(force_tac (claset() addDs [True_steps_concD]
   1.194 +by (force_tac (claset() addDs [True_steps_concD]
   1.195       addIs [True_True_steps_concI],simpset()) 1);
   1.196  qed "True_steps_conc";
   1.197  
   1.198 @@ -243,7 +243,7 @@
   1.199  
   1.200  Goalw [conc_def]
   1.201    "!L R. start(conc L R) = True#start L";
   1.202 -by(Simp_tac 1);
   1.203 +by (Simp_tac 1);
   1.204  qed_spec_mp "start_conc";
   1.205  
   1.206  Goalw [conc_def]
   1.207 @@ -257,27 +257,27 @@
   1.208   "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
   1.209  by (simp_tac (simpset() addsimps
   1.210       [accepts_conv_steps,True_steps_conc,final_conc,start_conc]) 1);
   1.211 -br iffI 1;
   1.212 +by (rtac iffI 1);
   1.213   by (Clarify_tac 1);
   1.214 - be disjE 1;
   1.215 + by (etac disjE 1);
   1.216    by (Clarify_tac 1);
   1.217 -  be disjE 1;
   1.218 -   by(res_inst_tac [("x","w")] exI 1);
   1.219 -   by(Simp_tac 1);
   1.220 -   by(Blast_tac 1);
   1.221 -  by(Blast_tac 1);
   1.222 - be disjE 1;
   1.223 -  by(Blast_tac 1);
   1.224 +  by (etac disjE 1);
   1.225 +   by (res_inst_tac [("x","w")] exI 1);
   1.226 +   by (Simp_tac 1);
   1.227 +   by (Blast_tac 1);
   1.228 +  by (Blast_tac 1);
   1.229 + by (etac disjE 1);
   1.230 +  by (Blast_tac 1);
   1.231   by (Clarify_tac 1);
   1.232 - by(res_inst_tac [("x","u")] exI 1);
   1.233 - by(Simp_tac 1);
   1.234 - by(Blast_tac 1);
   1.235 + by (res_inst_tac [("x","u")] exI 1);
   1.236 + by (Simp_tac 1);
   1.237 + by (Blast_tac 1);
   1.238  by (Clarify_tac 1);
   1.239 -by(exhaust_tac "v" 1);
   1.240 - by(Asm_full_simp_tac 1);
   1.241 - by(Blast_tac 1);
   1.242 -by(Asm_full_simp_tac 1);
   1.243 -by(Blast_tac 1);
   1.244 +by (exhaust_tac "v" 1);
   1.245 + by (Asm_full_simp_tac 1);
   1.246 + by (Blast_tac 1);
   1.247 +by (Asm_full_simp_tac 1);
   1.248 +by (Blast_tac 1);
   1.249  qed "accepts_conc";
   1.250  
   1.251  (******************************************************)
   1.252 @@ -285,19 +285,19 @@
   1.253  (******************************************************)
   1.254  
   1.255  Goalw [epsilon_def,step_def] "step epsilon a = {}";
   1.256 -by(Simp_tac 1);
   1.257 -by(Blast_tac 1);
   1.258 +by (Simp_tac 1);
   1.259 +by (Blast_tac 1);
   1.260  qed "step_epsilon";
   1.261  Addsimps [step_epsilon];
   1.262  
   1.263  Goal "((p,q) : steps epsilon w) = (w=[] & p=q)";
   1.264 -by(induct_tac "w" 1);
   1.265 -by(Auto_tac);
   1.266 +by (induct_tac "w" 1);
   1.267 +by (Auto_tac);
   1.268  qed "steps_epsilon";
   1.269  
   1.270  Goal "accepts epsilon w = (w = [])";
   1.271 -by(simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
   1.272 -by(simp_tac (simpset() addsimps [epsilon_def]) 1);
   1.273 +by (simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
   1.274 +by (simp_tac (simpset() addsimps [epsilon_def]) 1);
   1.275  qed "accepts_epsilon";
   1.276  AddIffs [accepts_epsilon];
   1.277  
   1.278 @@ -306,41 +306,41 @@
   1.279  (******************************************************)
   1.280  
   1.281  Goalw [plus_def] "!A. start (plus A) = start A";
   1.282 -by(Simp_tac 1);
   1.283 +by (Simp_tac 1);
   1.284  qed_spec_mp "start_plus";
   1.285  Addsimps [start_plus];
   1.286  
   1.287  Goalw [plus_def] "!A. fin (plus A) = fin A";
   1.288 -by(Simp_tac 1);
   1.289 +by (Simp_tac 1);
   1.290  qed_spec_mp "fin_plus";
   1.291  AddIffs [fin_plus];
   1.292  
   1.293  Goalw [plus_def,step_def]
   1.294    "!A. (p,q) : step A a --> (p,q) : step (plus A) a";
   1.295 -by(Simp_tac 1);
   1.296 +by (Simp_tac 1);
   1.297  qed_spec_mp "step_plusI";
   1.298  
   1.299  Goal "!p. (p,q) : steps A w --> (p,q) : steps (plus A) w";
   1.300 -by(induct_tac "w" 1);
   1.301 - by(Simp_tac 1);
   1.302 -by(Simp_tac 1);
   1.303 -by(blast_tac (claset() addIs [step_plusI]) 1);
   1.304 +by (induct_tac "w" 1);
   1.305 + by (Simp_tac 1);
   1.306 +by (Simp_tac 1);
   1.307 +by (blast_tac (claset() addIs [step_plusI]) 1);
   1.308  qed_spec_mp "steps_plusI";
   1.309  
   1.310  Goalw [plus_def,step_def]
   1.311   "!A. (p,r): step (plus A) a = \
   1.312  \     ( (p,r): step A a | fin A p & (start A,r) : step A a )";
   1.313 -by(Simp_tac 1);
   1.314 +by (Simp_tac 1);
   1.315  qed_spec_mp "step_plus_conv";
   1.316  AddIffs [step_plus_conv];
   1.317  
   1.318  Goal
   1.319   "[| (start A,q) : steps A u; u ~= []; fin A p |] \
   1.320  \ ==> (p,q) : steps (plus A) u";
   1.321 -by(exhaust_tac "u" 1);
   1.322 - by(Blast_tac 1);
   1.323 -by(Asm_full_simp_tac 1);
   1.324 -by(blast_tac (claset() addIs [steps_plusI]) 1);
   1.325 +by (exhaust_tac "u" 1);
   1.326 + by (Blast_tac 1);
   1.327 +by (Asm_full_simp_tac 1);
   1.328 +by (blast_tac (claset() addIs [steps_plusI]) 1);
   1.329  qed "fin_steps_plusI";
   1.330  
   1.331  (* reverse list induction! Complicates matters for conc? *)
   1.332 @@ -349,24 +349,24 @@
   1.333  \     (? us v. w = concat us @ v & \
   1.334  \              (!u:set us. u ~= [] & accepts A u) & \
   1.335  \              (start A,r) : steps A v)";
   1.336 -by(rev_induct_tac "w" 1);
   1.337 +by (rev_induct_tac "w" 1);
   1.338   by (Simp_tac 1);
   1.339 - by(res_inst_tac [("x","[]")] exI 1);
   1.340 + by (res_inst_tac [("x","[]")] exI 1);
   1.341   by (Simp_tac 1);
   1.342  by (Simp_tac 1);
   1.343  by (Clarify_tac 1);
   1.344 -by(etac allE 1 THEN mp_tac 1);
   1.345 +by (etac allE 1 THEN mp_tac 1);
   1.346  by (Clarify_tac 1);
   1.347 -be disjE 1;
   1.348 - by(res_inst_tac [("x","us")] exI 1);
   1.349 - by(Asm_simp_tac 1);
   1.350 - by(Blast_tac 1);
   1.351 -by(exhaust_tac "v" 1);
   1.352 - by(res_inst_tac [("x","us")] exI 1);
   1.353 - by(Asm_full_simp_tac 1);
   1.354 -by(res_inst_tac [("x","us@[v]")] exI 1);
   1.355 -by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.356 -by(Blast_tac 1);
   1.357 +by (etac disjE 1);
   1.358 + by (res_inst_tac [("x","us")] exI 1);
   1.359 + by (Asm_simp_tac 1);
   1.360 + by (Blast_tac 1);
   1.361 +by (exhaust_tac "v" 1);
   1.362 + by (res_inst_tac [("x","us")] exI 1);
   1.363 + by (Asm_full_simp_tac 1);
   1.364 +by (res_inst_tac [("x","us@[v]")] exI 1);
   1.365 +by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.366 +by (Blast_tac 1);
   1.367  qed_spec_mp "start_steps_plusD";
   1.368  
   1.369  Goal
   1.370 @@ -374,54 +374,54 @@
   1.371  \     (? us v. w = concat us @ v & \
   1.372  \              (!u:set us. accepts A u) & \
   1.373  \              (start A,r) : steps A v)";
   1.374 -by(rev_induct_tac "w" 1);
   1.375 +by (rev_induct_tac "w" 1);
   1.376   by (Simp_tac 1);
   1.377 - by(res_inst_tac [("x","[]")] exI 1);
   1.378 + by (res_inst_tac [("x","[]")] exI 1);
   1.379   by (Simp_tac 1);
   1.380  by (Simp_tac 1);
   1.381  by (Clarify_tac 1);
   1.382 -by(etac allE 1 THEN mp_tac 1);
   1.383 +by (etac allE 1 THEN mp_tac 1);
   1.384  by (Clarify_tac 1);
   1.385 -be disjE 1;
   1.386 - by(res_inst_tac [("x","us")] exI 1);
   1.387 - by(Asm_simp_tac 1);
   1.388 - by(Blast_tac 1);
   1.389 -by(res_inst_tac [("x","us@[v]")] exI 1);
   1.390 -by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.391 -by(Blast_tac 1);
   1.392 +by (etac disjE 1);
   1.393 + by (res_inst_tac [("x","us")] exI 1);
   1.394 + by (Asm_simp_tac 1);
   1.395 + by (Blast_tac 1);
   1.396 +by (res_inst_tac [("x","us@[v]")] exI 1);
   1.397 +by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.398 +by (Blast_tac 1);
   1.399  qed_spec_mp "start_steps_plusD";
   1.400  
   1.401  Goal
   1.402   "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
   1.403 -by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.404 -by(rev_induct_tac "us" 1);
   1.405 - by(Simp_tac 1);
   1.406 -by(rename_tac "u us" 1);
   1.407 -by(Simp_tac 1);
   1.408 +by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.409 +by (rev_induct_tac "us" 1);
   1.410 + by (Simp_tac 1);
   1.411 +by (rename_tac "u us" 1);
   1.412 +by (Simp_tac 1);
   1.413  by (Clarify_tac 1);
   1.414 -by(case_tac "us = []" 1);
   1.415 - by(Asm_full_simp_tac 1);
   1.416 - by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   1.417 +by (case_tac "us = []" 1);
   1.418 + by (Asm_full_simp_tac 1);
   1.419 + by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   1.420  by (Clarify_tac 1);
   1.421 -by(case_tac "u = []" 1);
   1.422 - by(Asm_full_simp_tac 1);
   1.423 - by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   1.424 -by(Asm_full_simp_tac 1);
   1.425 -by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   1.426 +by (case_tac "u = []" 1);
   1.427 + by (Asm_full_simp_tac 1);
   1.428 + by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   1.429 +by (Asm_full_simp_tac 1);
   1.430 +by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   1.431  qed_spec_mp "steps_star_cycle";
   1.432  
   1.433  Goal
   1.434   "accepts (plus A) w = \
   1.435  \ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))";
   1.436 -br iffI 1;
   1.437 - by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.438 +by (rtac iffI 1);
   1.439 + by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.440   by (Clarify_tac 1);
   1.441 - bd start_steps_plusD 1;
   1.442 + by (dtac start_steps_plusD 1);
   1.443   by (Clarify_tac 1);
   1.444 - by(res_inst_tac [("x","us@[v]")] exI 1);
   1.445 - by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.446 - by(Blast_tac 1);
   1.447 -by(blast_tac (claset() addIs [steps_star_cycle]) 1);
   1.448 + by (res_inst_tac [("x","us@[v]")] exI 1);
   1.449 + by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.450 + by (Blast_tac 1);
   1.451 +by (blast_tac (claset() addIs [steps_star_cycle]) 1);
   1.452  qed "accepts_plus";
   1.453  AddIffs [accepts_plus];
   1.454  
   1.455 @@ -432,24 +432,24 @@
   1.456  Goalw [star_def]
   1.457  "accepts (star A) w = \
   1.458  \ (? us. (!u : set us. accepts A u) & w = concat us)";
   1.459 -br iffI 1;
   1.460 +by (rtac iffI 1);
   1.461   by (Clarify_tac 1);
   1.462 - be disjE 1;
   1.463 -  by(res_inst_tac [("x","[]")] exI 1);
   1.464 -  by(Simp_tac 1);
   1.465 -  by(Blast_tac 1);
   1.466 - by(Blast_tac 1);
   1.467 -by(Force_tac 1);
   1.468 + by (etac disjE 1);
   1.469 +  by (res_inst_tac [("x","[]")] exI 1);
   1.470 +  by (Simp_tac 1);
   1.471 +  by (Blast_tac 1);
   1.472 + by (Blast_tac 1);
   1.473 +by (Force_tac 1);
   1.474  qed "accepts_star";
   1.475  
   1.476  (***** Correctness of r2n *****)
   1.477  
   1.478  Goal
   1.479   "!w. accepts (rexp2na r) w = (w : lang r)";
   1.480 -by(induct_tac "r" 1);
   1.481 -    by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.482 -   by(simp_tac(simpset() addsimps [accepts_atom]) 1);
   1.483 -  by(Asm_simp_tac 1);
   1.484 - by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
   1.485 -by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
   1.486 +by (induct_tac "r" 1);
   1.487 +    by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   1.488 +   by (simp_tac(simpset() addsimps [accepts_atom]) 1);
   1.489 +  by (Asm_simp_tac 1);
   1.490 + by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
   1.491 +by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
   1.492  qed_spec_mp "accepts_rexp2na";