src/HOL/Lex/RegExp2NAe.ML
author nipkow
Fri May 08 18:33:29 1998 +0200 (1998-05-08)
changeset 4907 0eb6730de30f
child 4936 e67949e15255
permissions -rw-r--r--
Reshuffeling, renaming and a few simple corollaries.
     1 (*  Title:      HOL/Lex/RegExp2NAe.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1998 TUM
     5 *)
     6 
     7 (******************************************************)
     8 (*                       atom                         *)
     9 (******************************************************)
    10 
    11 goalw thy [atom_def] "(fin (atom a) q) = (q = [False])";
    12 by(Simp_tac 1);
    13 qed "fin_atom";
    14 
    15 goalw thy [atom_def] "start (atom a) = [True]";
    16 by(Simp_tac 1);
    17 qed "start_atom";
    18 
    19 (* Use {x. False} = {}? *)
    20 
    21 goalw thy [atom_def,step_def]
    22  "eps(atom a) = {}";
    23 by(Simp_tac 1);
    24 by (Blast_tac 1);
    25 qed "eps_atom";
    26 Addsimps [eps_atom];
    27 
    28 goalw thy [atom_def,step_def]
    29  "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)";
    30 by(Simp_tac 1);
    31 qed "in_step_atom_Some";
    32 Addsimps [in_step_atom_Some];
    33 
    34 goal thy
    35  "([False],[False]) : steps (atom a) w = (w = [])";
    36 by (induct_tac "w" 1);
    37  by(Simp_tac 1);
    38 by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
    39 qed "False_False_in_steps_atom";
    40 
    41 goal thy
    42  "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
    43 by (induct_tac "w" 1);
    44  by(asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
    45 by(asm_full_simp_tac (simpset()
    46      addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
    47 qed "start_fin_in_steps_atom";
    48 
    49 goal thy
    50  "accepts (atom a) w = (w = [a])";
    51 by(simp_tac(simpset() addsimps
    52        [accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
    53 qed "accepts_atom";
    54 
    55 
    56 (******************************************************)
    57 (*                      union                         *)
    58 (******************************************************)
    59 
    60 (***** True/False ueber fin anheben *****)
    61 
    62 goalw thy [union_def] 
    63  "!L R. fin (union L R) (True#p) = fin L p";
    64 by (Simp_tac 1);
    65 qed_spec_mp "fin_union_True";
    66 
    67 goalw thy [union_def] 
    68  "!L R. fin (union L R) (False#p) = fin R p";
    69 by (Simp_tac 1);
    70 qed_spec_mp "fin_union_False";
    71 
    72 AddIffs [fin_union_True,fin_union_False];
    73 
    74 (***** True/False ueber step anheben *****)
    75 
    76 goalw thy [union_def,step_def]
    77 "!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
    78 by (Simp_tac 1);
    79 by(Blast_tac 1);
    80 qed_spec_mp "True_in_step_union";
    81 
    82 goalw thy [union_def,step_def]
    83 "!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
    84 by (Simp_tac 1);
    85 by(Blast_tac 1);
    86 qed_spec_mp "False_in_step_union";
    87 
    88 AddIffs [True_in_step_union,False_in_step_union];
    89 
    90 (***** True/False ueber epsclosure anheben *****)
    91 
    92 goal thy
    93  "!!d. (tp,tq) : (eps(union L R))^* ==> \
    94 \ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
    95 be rtrancl_induct 1;
    96  by(Blast_tac 1);
    97 by(Clarify_tac 1);
    98 by(Asm_full_simp_tac 1);
    99 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   100 val lemma1a = result();
   101 
   102 goal thy
   103  "!!d. (tp,tq) : (eps(union L R))^* ==> \
   104 \ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
   105 be rtrancl_induct 1;
   106  by(Blast_tac 1);
   107 by(Clarify_tac 1);
   108 by(Asm_full_simp_tac 1);
   109 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   110 val lemma1b = result();
   111 
   112 goal thy
   113  "!!p. (p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(union L R))^*";
   114 be rtrancl_induct 1;
   115  by(Blast_tac 1);
   116 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   117 val lemma2a = result();
   118 
   119 goal thy
   120  "!!p. (p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(union L R))^*";
   121 be rtrancl_induct 1;
   122  by(Blast_tac 1);
   123 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   124 val lemma2b = result();
   125 
   126 goal thy
   127  "(True#p,q) : (eps(union L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
   128 by(blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
   129 qed "True_epsclosure_union";
   130 
   131 goal thy
   132  "(False#p,q) : (eps(union L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
   133 by(blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
   134 qed "False_epsclosure_union";
   135 
   136 AddIffs [True_epsclosure_union,False_epsclosure_union];
   137 
   138 (***** True/False ueber steps anheben *****)
   139 
   140 goal thy
   141  "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
   142 by (induct_tac "w" 1);
   143 by (ALLGOALS Asm_simp_tac);
   144 (* Blast_tac produces PROOF FAILED for depth 8 *)
   145 by(Fast_tac 1);
   146 qed_spec_mp "lift_True_over_steps_union";
   147 
   148 goal thy 
   149  "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
   150 by (induct_tac "w" 1);
   151 by (ALLGOALS Asm_simp_tac);
   152 (* Blast_tac produces PROOF FAILED for depth 8 *)
   153 by(Fast_tac 1);
   154 qed_spec_mp "lift_False_over_steps_union";
   155 
   156 AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
   157 
   158 
   159 (***** Epsilonhuelle des Startzustands  *****)
   160 
   161 goal thy
   162  "R^* = id Un (R^* O R)";
   163 by(rtac set_ext 1);
   164 by(split_all_tac 1);
   165 by(rtac iffI 1);
   166  be rtrancl_induct 1;
   167   by(Blast_tac 1);
   168  by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   169 by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
   170 qed "unfold_rtrancl2";
   171 
   172 goal thy
   173  "(p,q) : R^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))";
   174 by(rtac (unfold_rtrancl2 RS equalityE) 1);
   175 by(Blast_tac 1);
   176 qed "in_unfold_rtrancl2";
   177 
   178 val epsclosure_start_step_union =
   179   read_instantiate [("p","start(union L R)")] in_unfold_rtrancl2;
   180 AddIffs [epsclosure_start_step_union];
   181 
   182 goalw thy [union_def,step_def]
   183  "!L R. (start(union L R),q) : eps(union L R) = \
   184 \       (q = True#start L | q = False#start R)";
   185 by(Simp_tac 1);
   186 qed_spec_mp "start_eps_union";
   187 AddIffs [start_eps_union];
   188 
   189 goalw thy [union_def,step_def]
   190  "!L R. (start(union L R),q) ~: step (union L R) (Some a)";
   191 by(Simp_tac 1);
   192 qed_spec_mp "not_start_step_union_Some";
   193 AddIffs [not_start_step_union_Some];
   194 
   195 goal thy
   196  "(start(union L R), q) : steps (union L R) w = \
   197 \ ( (w = [] & q = start(union L R)) | \
   198 \   (? p.  q = True  # p & (start L,p) : steps L w | \
   199 \          q = False # p & (start R,p) : steps R w) )";
   200 by (exhaust_tac "w" 1);
   201  by (Asm_simp_tac 1);
   202  (* Blast_tac produces PROOF FAILED! *)
   203  by(Fast_tac 1);
   204 by (Asm_simp_tac 1);
   205 (* The goal is now completely dual to the first one.
   206    Fast/Best_tac don't return. Blast_tac produces PROOF FAILED!
   207    The lemmas used in the explicit proof are part of the claset already!
   208 *)
   209 br iffI 1;
   210  by(Blast_tac 1);
   211 by(Clarify_tac 1);
   212 be disjE 1;
   213  by(Blast_tac 1);
   214 by(Clarify_tac 1);
   215 br compI 1;
   216 br compI 1;
   217 br (epsclosure_start_step_union RS iffD2) 1;
   218 br disjI2 1;
   219 br exI 1;
   220 br conjI 1;
   221 br (start_eps_union RS iffD2) 1;
   222 br disjI2 1;
   223 br refl 1;
   224 by(Clarify_tac 1);
   225 br exI 1;
   226 br conjI 1;
   227 br refl 1;
   228 ba 1;
   229 by(Clarify_tac 1);
   230 br exI 1;
   231 br conjI 1;
   232 br refl 1;
   233 ba 1;
   234 by(Clarify_tac 1);
   235 br exI 1;
   236 br conjI 1;
   237 br refl 1;
   238 ba 1;
   239 qed "steps_union";
   240 
   241 goalw thy [union_def]
   242  "!L R. ~ fin (union L R) (start(union L R))";
   243 by(Simp_tac 1);
   244 qed_spec_mp "start_union_not_final";
   245 AddIffs [start_union_not_final];
   246 
   247 goalw thy [accepts_def]
   248  "accepts (union L R) w = (accepts L w | accepts R w)";
   249 by (simp_tac (simpset() addsimps [steps_union]) 1);
   250 auto();
   251 qed "accepts_union";
   252 
   253 
   254 (******************************************************)
   255 (*                      conc                        *)
   256 (******************************************************)
   257 
   258 (** True/False in fin **)
   259 
   260 goalw thy [conc_def]
   261  "!L R. fin (conc L R) (True#p) = False";
   262 by (Simp_tac 1);
   263 qed_spec_mp "fin_conc_True";
   264 
   265 goalw thy [conc_def] 
   266  "!L R. fin (conc L R) (False#p) = fin R p";
   267 by (Simp_tac 1);
   268 qed "fin_conc_False";
   269 
   270 AddIffs [fin_conc_True,fin_conc_False];
   271 
   272 (** True/False in step **)
   273 
   274 goalw thy [conc_def,step_def]
   275  "!L R. (True#p,q) : step (conc L R) a = \
   276 \       ((? r. q=True#r & (p,r): step L a) | \
   277 \        (fin L p & a=None & q=False#start R))";
   278 by (Simp_tac 1);
   279 by(Blast_tac 1);
   280 qed_spec_mp "True_step_conc";
   281 
   282 goalw thy [conc_def,step_def]
   283  "!L R. (False#p,q) : step (conc L R) a = \
   284 \       (? r. q = False#r & (p,r) : step R a)";
   285 by (Simp_tac 1);
   286 by(Blast_tac 1);
   287 qed_spec_mp "False_step_conc";
   288 
   289 AddIffs [True_step_conc, False_step_conc];
   290 
   291 (** False in epsclosure **)
   292 
   293 goal thy
   294  "!!d. (tp,tq) : (eps(conc L R))^* ==> \
   295 \ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
   296 by(etac rtrancl_induct 1);
   297  by(Blast_tac 1);
   298 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   299 qed "lemma1b";
   300 
   301 goal thy
   302  "!!p. (p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
   303 by(etac rtrancl_induct 1);
   304  by(Blast_tac 1);
   305 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   306 val lemma2b = result();
   307 
   308 goal thy
   309  "((False # p, q) : (eps (conc L R))^*) = \
   310 \ (? r. q = False # r & (p, r) : (eps R)^*)";
   311 by (rtac iffI 1);
   312  by(blast_tac (claset() addDs [lemma1b]) 1);
   313 by(blast_tac (claset() addDs [lemma2b]) 1);
   314 qed "False_epsclosure_conc";
   315 AddIffs [False_epsclosure_conc];
   316 
   317 (** False in steps **)
   318 
   319 goal thy
   320  "!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
   321 by (induct_tac "w" 1);
   322  by (Simp_tac 1);
   323 by (Simp_tac 1);
   324 (* Blast_tac produces PROOF FAILED for depth 8 *)
   325 by(Fast_tac 1);
   326 qed_spec_mp "False_steps_conc";
   327 AddIffs [False_steps_conc];
   328 
   329 (** True in epsclosure **)
   330 
   331 goal thy
   332  "!!L R. (p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*";
   333 be rtrancl_induct 1;
   334  by(Blast_tac 1);
   335 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   336 qed "True_True_eps_concI";
   337 
   338 goal thy
   339  "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
   340 by(induct_tac "w" 1);
   341  by (simp_tac (simpset() addsimps [True_True_eps_concI]) 1);
   342 by (Simp_tac 1);
   343 by(blast_tac (claset() addIs [True_True_eps_concI]) 1);
   344 qed_spec_mp "True_True_steps_concI";
   345 
   346 goal thy
   347  "!!d. (tp,tq) : (eps(conc L R))^* ==> \
   348 \ !p. tp = True#p --> \
   349 \ (? q. tq = True#q & (p,q) : (eps L)^*) | \
   350 \ (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*)";
   351 by(etac rtrancl_induct 1);
   352  by(Blast_tac 1);
   353 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   354 val lemma1a = result();
   355 
   356 goal thy
   357  "!!p. (p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*";
   358 by(etac rtrancl_induct 1);
   359  by(Blast_tac 1);
   360 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   361 val lemma2a = result();
   362 
   363 goalw thy [conc_def,step_def]
   364  "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None";
   365 by(split_all_tac 1);
   366 by (Asm_full_simp_tac 1);
   367 val lemma = result();
   368 
   369 goal thy
   370  "!!L R. (p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
   371 by(etac rtrancl_induct 1);
   372  by(Blast_tac 1);
   373 by (dtac lemma 1);
   374 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   375 val lemma2b = result();
   376 
   377 goalw thy [conc_def,step_def]
   378  "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)";
   379 by(split_all_tac 1);
   380 by(Asm_full_simp_tac 1);
   381 qed "True_False_eps_concI";
   382 
   383 goal thy
   384  "((True#p,q) : (eps(conc L R))^*) = \
   385 \ ((? r. (p,r) : (eps L)^* & q = True#r) | \
   386 \  (? r. (p,r) : (eps L)^* & fin L r & \
   387 \        (? s. (start R, s) : (eps R)^* & q = False#s)))";
   388 by(rtac iffI 1);
   389  by(blast_tac (claset() addDs [lemma1a]) 1);
   390 be disjE 1;
   391  by(blast_tac (claset() addIs [lemma2a]) 1);
   392 by(Clarify_tac 1);
   393 br (rtrancl_trans) 1;
   394 be lemma2a 1;
   395 br (rtrancl_into_rtrancl2) 1;
   396 be True_False_eps_concI 1;
   397 be lemma2b 1;
   398 qed "True_epsclosure_conc";
   399 AddIffs [True_epsclosure_conc];
   400 
   401 (** True in steps **)
   402 
   403 goal thy
   404  "!p. (True#p,q) : steps (conc L R) w --> \
   405 \     ((? r. (p,r) : steps L w & q = True#r)  | \
   406 \      (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
   407 \              (? s. (start R,s) : steps R v & q = False#s))))";
   408 by(induct_tac "w" 1);
   409  by(Simp_tac 1);
   410 by(Simp_tac 1);
   411 by(clarify_tac (claset() delrules [disjCI]) 1);
   412  be disjE 1;
   413  by(clarify_tac (claset() delrules [disjCI]) 1);
   414  be disjE 1;
   415   by(clarify_tac (claset() delrules [disjCI]) 1);
   416   by(etac allE 1 THEN mp_tac 1);
   417   be disjE 1;
   418    by (Blast_tac 1);
   419   br disjI2 1;
   420   by (Clarify_tac 1);
   421   by(Simp_tac 1);
   422   by(res_inst_tac[("x","a#u")] exI 1);
   423   by(Simp_tac 1);
   424   by (Blast_tac 1);
   425  by (Blast_tac 1);
   426 br disjI2 1;
   427 by (Clarify_tac 1);
   428 by(Simp_tac 1);
   429 by(res_inst_tac[("x","[]")] exI 1);
   430 by(Simp_tac 1);
   431 by (Blast_tac 1);
   432 qed_spec_mp "True_steps_concD";
   433 
   434 goal thy
   435  "(True#p,q) : steps (conc L R) w = \
   436 \ ((? r. (p,r) : steps L w & q = True#r)  | \
   437 \  (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
   438 \          (? s. (start R,s) : steps R v & q = False#s))))";
   439 by(blast_tac (claset() addDs [True_steps_concD]
   440      addIs [True_True_steps_concI,in_steps_epsclosure,r_into_rtrancl]) 1);
   441 qed "True_steps_conc";
   442 
   443 (** starting from the start **)
   444 
   445 goalw thy [conc_def]
   446   "!L R. start(conc L R) = True#start L";
   447 by(Simp_tac 1);
   448 qed_spec_mp "start_conc";
   449 
   450 goalw thy [conc_def]
   451  "!L R. fin(conc L R) p = (? s. p = False#s & fin R s)";
   452 by (simp_tac (simpset() addsplits [split_list_case]) 1);
   453 qed_spec_mp "final_conc";
   454 
   455 goal thy
   456  "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
   457 by (simp_tac (simpset() addsimps
   458      [accepts_def,True_steps_conc,final_conc,start_conc]) 1);
   459 by(Blast_tac 1);
   460 qed "accepts_conc";
   461 
   462 (******************************************************)
   463 (*                       star                         *)
   464 (******************************************************)
   465 
   466 goalw thy [star_def,step_def]
   467  "!A. (True#p,q) : eps(star A) = \
   468 \     ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )";
   469 by(Simp_tac 1);
   470 by(Blast_tac 1);
   471 qed_spec_mp "True_in_eps_star";
   472 AddIffs [True_in_eps_star];
   473 
   474 goalw thy [star_def,step_def]
   475   "!A. (p,q) : step A a --> (True#p, True#q) : step (star A) a";
   476 by(Simp_tac 1);
   477 qed_spec_mp "True_True_step_starI";
   478 
   479 goal thy
   480   "!!A. (p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
   481 be rtrancl_induct 1;
   482  by(Blast_tac 1);
   483 by(blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
   484 qed_spec_mp "True_True_eps_starI";
   485 
   486 goalw thy [star_def,step_def]
   487  "!A. fin A p --> (True#p,True#start A) : eps(star A)";
   488 by(Simp_tac 1);
   489 qed_spec_mp "True_start_eps_starI";
   490 
   491 goal thy
   492  "!!dummy. (tp,s) : (eps(star A))^* ==> (! p. tp = True#p --> \
   493 \ (? r. ((p,r) : (eps A)^* | \
   494 \        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
   495 \       s = True#r))";
   496 be rtrancl_induct 1;
   497  by(Simp_tac 1);
   498 by (Clarify_tac 1);
   499 by (Asm_full_simp_tac 1);
   500 by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   501 val lemma = result();
   502 
   503 goal thy
   504  "((True#p,s) : (eps(star A))^*) = \
   505 \ (? r. ((p,r) : (eps A)^* | \
   506 \        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
   507 \       s = True#r)";
   508 br iffI 1;
   509  bd lemma 1;
   510  by(Blast_tac 1);
   511 (* Why can't blast_tac do the rest? *)
   512 by (Clarify_tac 1);
   513 be disjE 1;
   514 be True_True_eps_starI 1;
   515 by (Clarify_tac 1);
   516 br rtrancl_trans 1;
   517 be True_True_eps_starI 1;
   518 br rtrancl_trans 1;
   519 br r_into_rtrancl 1;
   520 be True_start_eps_starI 1;
   521 be True_True_eps_starI 1;
   522 qed "True_eps_star";
   523 AddIffs [True_eps_star];
   524 
   525 (** True in step Some **)
   526 
   527 goalw thy [star_def,step_def]
   528  "!A. (True#p,r): step (star A) (Some a) = \
   529 \     (? q. (p,q): step A (Some a) & r=True#q)";
   530 by(Simp_tac 1);
   531 by(Blast_tac 1);
   532 qed_spec_mp "True_step_star";
   533 AddIffs [True_step_star];
   534 
   535 
   536 (** True in steps **)
   537 
   538 (* reverse list induction! Complicates matters for conc? *)
   539 goal thy
   540  "!rr. (True#start A,rr) : steps (star A) w --> \
   541 \ (? us v. w = concat us @ v & \
   542 \             (!u:set us. accepts A u) & \
   543 \             (? r. (start A,r) : steps A v & rr = True#r))";
   544 by(res_inst_tac [("xs","w")] snoc_induct 1);
   545  by (Asm_full_simp_tac 1);
   546  by (Clarify_tac 1);
   547  by(res_inst_tac [("x","[]")] exI 1);
   548  be disjE 1;
   549   by (Asm_simp_tac 1);
   550  by (Clarify_tac 1);
   551  by (Asm_simp_tac 1);
   552 by(simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
   553 by (Clarify_tac 1);
   554 by(etac allE 1 THEN mp_tac 1);
   555 by (Clarify_tac 1);
   556 be disjE 1;
   557  by(res_inst_tac [("x","us")] exI 1);
   558  by(res_inst_tac [("x","v@[x]")] exI 1);
   559  by(asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
   560  by(Blast_tac 1);
   561 by (Clarify_tac 1);
   562 by(res_inst_tac [("x","us@[v@[x]]")] exI 1);
   563 by(res_inst_tac [("x","[]")] exI 1);
   564 by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
   565 by(Blast_tac 1);
   566 qed_spec_mp "True_start_steps_starD";
   567 
   568 goal thy "!p. (p,q) : steps A w --> (True#p,True#q) : steps (star A) w";
   569 by(induct_tac "w" 1);
   570  by(Simp_tac 1);
   571 by(Simp_tac 1);
   572 by(blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
   573 qed_spec_mp "True_True_steps_starI";
   574 
   575 goalw thy [accepts_def]
   576  "(!u : set us. accepts A u) --> \
   577 \ (True#start A,True#start A) : steps (star A) (concat us)";
   578 by(induct_tac "us" 1);
   579  by(Simp_tac 1);
   580 by(Simp_tac 1);
   581 by(blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
   582 qed_spec_mp "steps_star_cycle";
   583 
   584 (* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
   585 goal thy
   586  "(True#start A,rr) : steps (star A) w = \
   587 \ (? us v. w = concat us @ v & \
   588 \             (!u:set us. accepts A u) & \
   589 \             (? r. (start A,r) : steps A v & rr = True#r))";
   590 br iffI 1;
   591  be True_start_steps_starD 1;
   592 by (Clarify_tac 1);
   593 by(Asm_simp_tac 1);
   594 by(blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
   595 qed "True_start_steps_star";
   596 
   597 (** the start state **)
   598 
   599 goalw thy [star_def,step_def]
   600   "!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)";
   601 by(Simp_tac 1);
   602 qed_spec_mp "start_step_star";
   603 AddIffs [start_step_star];
   604 
   605 val epsclosure_start_step_star =
   606   read_instantiate [("p","start(star A)")] in_unfold_rtrancl2;
   607 
   608 goal thy
   609  "(start(star A),r) : steps (star A) w = \
   610 \ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
   611 br iffI 1;
   612  by(exhaust_tac "w" 1);
   613   by(asm_full_simp_tac (simpset() addsimps
   614     [epsclosure_start_step_star]) 1);
   615  by(Asm_full_simp_tac 1);
   616  by (Clarify_tac 1);
   617  by(asm_full_simp_tac (simpset() addsimps
   618     [epsclosure_start_step_star]) 1);
   619  by(Blast_tac 1);
   620 be disjE 1;
   621  by(Asm_simp_tac 1);
   622 by(blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
   623 qed "start_steps_star";
   624 
   625 goalw thy [star_def] "!A. fin (star A) (True#p) = fin A p";
   626 by(Simp_tac 1);
   627 qed_spec_mp "fin_star_True";
   628 AddIffs [fin_star_True];
   629 
   630 goalw thy [star_def] "!A. fin (star A) (start(star A))";
   631 by(Simp_tac 1);
   632 qed_spec_mp "fin_star_start";
   633 AddIffs [fin_star_start];
   634 
   635 (* too complex! Simpler if loop back to start(star A)? *)
   636 goalw thy [accepts_def]
   637  "accepts (star A) w = \
   638 \ (? us. (!u : set(us). accepts A u) & (w = concat us) )";
   639 by(simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
   640 br iffI 1;
   641  by (Clarify_tac 1);
   642  be disjE 1;
   643   by (Clarify_tac 1);
   644   by(Simp_tac 1);
   645   by(res_inst_tac [("x","[]")] exI 1);
   646   by(Simp_tac 1);
   647  by (Clarify_tac 1);
   648  by(res_inst_tac [("x","us@[v]")] exI 1);
   649  by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
   650  by(Blast_tac 1);
   651 by (Clarify_tac 1);
   652 by(res_inst_tac [("xs","us")] snoc_exhaust 1);
   653  by(Asm_simp_tac 1);
   654  by(Blast_tac 1);
   655 by (Clarify_tac 1);
   656 by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
   657 by(Blast_tac 1);
   658 qed "accepts_star";
   659 
   660 
   661 (***** Correctness of r2n *****)
   662 
   663 goal thy
   664  "!w. accepts (rexp2nae r) w = (w : lang r)";
   665 by(induct_tac "r" 1);
   666     by(simp_tac (simpset() addsimps [accepts_def]) 1);
   667    by(simp_tac(simpset() addsimps [accepts_atom]) 1);
   668   by(asm_simp_tac (simpset() addsimps [accepts_union]) 1);
   669  by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
   670 by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
   671 qed "accepts_rexp2nae";