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