src/HOL/Lex/RegExp2NAe.ML
changeset 4907 0eb6730de30f
child 4936 e67949e15255
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Fri May 08 18:33:29 1998 +0200
     1.3 @@ -0,0 +1,671 @@
     1.4 +(*  Title:      HOL/Lex/RegExp2NAe.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow
     1.7 +    Copyright   1998 TUM
     1.8 +*)
     1.9 +
    1.10 +(******************************************************)
    1.11 +(*                       atom                         *)
    1.12 +(******************************************************)
    1.13 +
    1.14 +goalw thy [atom_def] "(fin (atom a) q) = (q = [False])";
    1.15 +by(Simp_tac 1);
    1.16 +qed "fin_atom";
    1.17 +
    1.18 +goalw thy [atom_def] "start (atom a) = [True]";
    1.19 +by(Simp_tac 1);
    1.20 +qed "start_atom";
    1.21 +
    1.22 +(* Use {x. False} = {}? *)
    1.23 +
    1.24 +goalw thy [atom_def,step_def]
    1.25 + "eps(atom a) = {}";
    1.26 +by(Simp_tac 1);
    1.27 +by (Blast_tac 1);
    1.28 +qed "eps_atom";
    1.29 +Addsimps [eps_atom];
    1.30 +
    1.31 +goalw thy [atom_def,step_def]
    1.32 + "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)";
    1.33 +by(Simp_tac 1);
    1.34 +qed "in_step_atom_Some";
    1.35 +Addsimps [in_step_atom_Some];
    1.36 +
    1.37 +goal thy
    1.38 + "([False],[False]) : steps (atom a) w = (w = [])";
    1.39 +by (induct_tac "w" 1);
    1.40 + by(Simp_tac 1);
    1.41 +by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
    1.42 +qed "False_False_in_steps_atom";
    1.43 +
    1.44 +goal thy
    1.45 + "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
    1.46 +by (induct_tac "w" 1);
    1.47 + by(asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
    1.48 +by(asm_full_simp_tac (simpset()
    1.49 +     addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
    1.50 +qed "start_fin_in_steps_atom";
    1.51 +
    1.52 +goal thy
    1.53 + "accepts (atom a) w = (w = [a])";
    1.54 +by(simp_tac(simpset() addsimps
    1.55 +       [accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
    1.56 +qed "accepts_atom";
    1.57 +
    1.58 +
    1.59 +(******************************************************)
    1.60 +(*                      union                         *)
    1.61 +(******************************************************)
    1.62 +
    1.63 +(***** True/False ueber fin anheben *****)
    1.64 +
    1.65 +goalw thy [union_def] 
    1.66 + "!L R. fin (union L R) (True#p) = fin L p";
    1.67 +by (Simp_tac 1);
    1.68 +qed_spec_mp "fin_union_True";
    1.69 +
    1.70 +goalw thy [union_def] 
    1.71 + "!L R. fin (union L R) (False#p) = fin R p";
    1.72 +by (Simp_tac 1);
    1.73 +qed_spec_mp "fin_union_False";
    1.74 +
    1.75 +AddIffs [fin_union_True,fin_union_False];
    1.76 +
    1.77 +(***** True/False ueber step anheben *****)
    1.78 +
    1.79 +goalw thy [union_def,step_def]
    1.80 +"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
    1.81 +by (Simp_tac 1);
    1.82 +by(Blast_tac 1);
    1.83 +qed_spec_mp "True_in_step_union";
    1.84 +
    1.85 +goalw thy [union_def,step_def]
    1.86 +"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
    1.87 +by (Simp_tac 1);
    1.88 +by(Blast_tac 1);
    1.89 +qed_spec_mp "False_in_step_union";
    1.90 +
    1.91 +AddIffs [True_in_step_union,False_in_step_union];
    1.92 +
    1.93 +(***** True/False ueber epsclosure anheben *****)
    1.94 +
    1.95 +goal thy
    1.96 + "!!d. (tp,tq) : (eps(union L R))^* ==> \
    1.97 +\ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
    1.98 +be rtrancl_induct 1;
    1.99 + by(Blast_tac 1);
   1.100 +by(Clarify_tac 1);
   1.101 +by(Asm_full_simp_tac 1);
   1.102 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.103 +val lemma1a = result();
   1.104 +
   1.105 +goal thy
   1.106 + "!!d. (tp,tq) : (eps(union L R))^* ==> \
   1.107 +\ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
   1.108 +be rtrancl_induct 1;
   1.109 + by(Blast_tac 1);
   1.110 +by(Clarify_tac 1);
   1.111 +by(Asm_full_simp_tac 1);
   1.112 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.113 +val lemma1b = result();
   1.114 +
   1.115 +goal thy
   1.116 + "!!p. (p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(union L R))^*";
   1.117 +be rtrancl_induct 1;
   1.118 + by(Blast_tac 1);
   1.119 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.120 +val lemma2a = result();
   1.121 +
   1.122 +goal thy
   1.123 + "!!p. (p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(union L R))^*";
   1.124 +be rtrancl_induct 1;
   1.125 + by(Blast_tac 1);
   1.126 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.127 +val lemma2b = result();
   1.128 +
   1.129 +goal thy
   1.130 + "(True#p,q) : (eps(union L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
   1.131 +by(blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
   1.132 +qed "True_epsclosure_union";
   1.133 +
   1.134 +goal thy
   1.135 + "(False#p,q) : (eps(union L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
   1.136 +by(blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
   1.137 +qed "False_epsclosure_union";
   1.138 +
   1.139 +AddIffs [True_epsclosure_union,False_epsclosure_union];
   1.140 +
   1.141 +(***** True/False ueber steps anheben *****)
   1.142 +
   1.143 +goal thy
   1.144 + "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
   1.145 +by (induct_tac "w" 1);
   1.146 +by (ALLGOALS Asm_simp_tac);
   1.147 +(* Blast_tac produces PROOF FAILED for depth 8 *)
   1.148 +by(Fast_tac 1);
   1.149 +qed_spec_mp "lift_True_over_steps_union";
   1.150 +
   1.151 +goal thy 
   1.152 + "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
   1.153 +by (induct_tac "w" 1);
   1.154 +by (ALLGOALS Asm_simp_tac);
   1.155 +(* Blast_tac produces PROOF FAILED for depth 8 *)
   1.156 +by(Fast_tac 1);
   1.157 +qed_spec_mp "lift_False_over_steps_union";
   1.158 +
   1.159 +AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
   1.160 +
   1.161 +
   1.162 +(***** Epsilonhuelle des Startzustands  *****)
   1.163 +
   1.164 +goal thy
   1.165 + "R^* = id Un (R^* O R)";
   1.166 +by(rtac set_ext 1);
   1.167 +by(split_all_tac 1);
   1.168 +by(rtac iffI 1);
   1.169 + be rtrancl_induct 1;
   1.170 +  by(Blast_tac 1);
   1.171 + by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.172 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
   1.173 +qed "unfold_rtrancl2";
   1.174 +
   1.175 +goal thy
   1.176 + "(p,q) : R^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))";
   1.177 +by(rtac (unfold_rtrancl2 RS equalityE) 1);
   1.178 +by(Blast_tac 1);
   1.179 +qed "in_unfold_rtrancl2";
   1.180 +
   1.181 +val epsclosure_start_step_union =
   1.182 +  read_instantiate [("p","start(union L R)")] in_unfold_rtrancl2;
   1.183 +AddIffs [epsclosure_start_step_union];
   1.184 +
   1.185 +goalw thy [union_def,step_def]
   1.186 + "!L R. (start(union L R),q) : eps(union L R) = \
   1.187 +\       (q = True#start L | q = False#start R)";
   1.188 +by(Simp_tac 1);
   1.189 +qed_spec_mp "start_eps_union";
   1.190 +AddIffs [start_eps_union];
   1.191 +
   1.192 +goalw thy [union_def,step_def]
   1.193 + "!L R. (start(union L R),q) ~: step (union L R) (Some a)";
   1.194 +by(Simp_tac 1);
   1.195 +qed_spec_mp "not_start_step_union_Some";
   1.196 +AddIffs [not_start_step_union_Some];
   1.197 +
   1.198 +goal thy
   1.199 + "(start(union L R), q) : steps (union L R) w = \
   1.200 +\ ( (w = [] & q = start(union L R)) | \
   1.201 +\   (? p.  q = True  # p & (start L,p) : steps L w | \
   1.202 +\          q = False # p & (start R,p) : steps R w) )";
   1.203 +by (exhaust_tac "w" 1);
   1.204 + by (Asm_simp_tac 1);
   1.205 + (* Blast_tac produces PROOF FAILED! *)
   1.206 + by(Fast_tac 1);
   1.207 +by (Asm_simp_tac 1);
   1.208 +(* The goal is now completely dual to the first one.
   1.209 +   Fast/Best_tac don't return. Blast_tac produces PROOF FAILED!
   1.210 +   The lemmas used in the explicit proof are part of the claset already!
   1.211 +*)
   1.212 +br iffI 1;
   1.213 + by(Blast_tac 1);
   1.214 +by(Clarify_tac 1);
   1.215 +be disjE 1;
   1.216 + by(Blast_tac 1);
   1.217 +by(Clarify_tac 1);
   1.218 +br compI 1;
   1.219 +br compI 1;
   1.220 +br (epsclosure_start_step_union RS iffD2) 1;
   1.221 +br disjI2 1;
   1.222 +br exI 1;
   1.223 +br conjI 1;
   1.224 +br (start_eps_union RS iffD2) 1;
   1.225 +br disjI2 1;
   1.226 +br refl 1;
   1.227 +by(Clarify_tac 1);
   1.228 +br exI 1;
   1.229 +br conjI 1;
   1.230 +br refl 1;
   1.231 +ba 1;
   1.232 +by(Clarify_tac 1);
   1.233 +br exI 1;
   1.234 +br conjI 1;
   1.235 +br refl 1;
   1.236 +ba 1;
   1.237 +by(Clarify_tac 1);
   1.238 +br exI 1;
   1.239 +br conjI 1;
   1.240 +br refl 1;
   1.241 +ba 1;
   1.242 +qed "steps_union";
   1.243 +
   1.244 +goalw thy [union_def]
   1.245 + "!L R. ~ fin (union L R) (start(union L R))";
   1.246 +by(Simp_tac 1);
   1.247 +qed_spec_mp "start_union_not_final";
   1.248 +AddIffs [start_union_not_final];
   1.249 +
   1.250 +goalw thy [accepts_def]
   1.251 + "accepts (union L R) w = (accepts L w | accepts R w)";
   1.252 +by (simp_tac (simpset() addsimps [steps_union]) 1);
   1.253 +auto();
   1.254 +qed "accepts_union";
   1.255 +
   1.256 +
   1.257 +(******************************************************)
   1.258 +(*                      conc                        *)
   1.259 +(******************************************************)
   1.260 +
   1.261 +(** True/False in fin **)
   1.262 +
   1.263 +goalw thy [conc_def]
   1.264 + "!L R. fin (conc L R) (True#p) = False";
   1.265 +by (Simp_tac 1);
   1.266 +qed_spec_mp "fin_conc_True";
   1.267 +
   1.268 +goalw thy [conc_def] 
   1.269 + "!L R. fin (conc L R) (False#p) = fin R p";
   1.270 +by (Simp_tac 1);
   1.271 +qed "fin_conc_False";
   1.272 +
   1.273 +AddIffs [fin_conc_True,fin_conc_False];
   1.274 +
   1.275 +(** True/False in step **)
   1.276 +
   1.277 +goalw thy [conc_def,step_def]
   1.278 + "!L R. (True#p,q) : step (conc L R) a = \
   1.279 +\       ((? r. q=True#r & (p,r): step L a) | \
   1.280 +\        (fin L p & a=None & q=False#start R))";
   1.281 +by (Simp_tac 1);
   1.282 +by(Blast_tac 1);
   1.283 +qed_spec_mp "True_step_conc";
   1.284 +
   1.285 +goalw thy [conc_def,step_def]
   1.286 + "!L R. (False#p,q) : step (conc L R) a = \
   1.287 +\       (? r. q = False#r & (p,r) : step R a)";
   1.288 +by (Simp_tac 1);
   1.289 +by(Blast_tac 1);
   1.290 +qed_spec_mp "False_step_conc";
   1.291 +
   1.292 +AddIffs [True_step_conc, False_step_conc];
   1.293 +
   1.294 +(** False in epsclosure **)
   1.295 +
   1.296 +goal thy
   1.297 + "!!d. (tp,tq) : (eps(conc L R))^* ==> \
   1.298 +\ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
   1.299 +by(etac rtrancl_induct 1);
   1.300 + by(Blast_tac 1);
   1.301 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.302 +qed "lemma1b";
   1.303 +
   1.304 +goal thy
   1.305 + "!!p. (p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
   1.306 +by(etac rtrancl_induct 1);
   1.307 + by(Blast_tac 1);
   1.308 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.309 +val lemma2b = result();
   1.310 +
   1.311 +goal thy
   1.312 + "((False # p, q) : (eps (conc L R))^*) = \
   1.313 +\ (? r. q = False # r & (p, r) : (eps R)^*)";
   1.314 +by (rtac iffI 1);
   1.315 + by(blast_tac (claset() addDs [lemma1b]) 1);
   1.316 +by(blast_tac (claset() addDs [lemma2b]) 1);
   1.317 +qed "False_epsclosure_conc";
   1.318 +AddIffs [False_epsclosure_conc];
   1.319 +
   1.320 +(** False in steps **)
   1.321 +
   1.322 +goal thy
   1.323 + "!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
   1.324 +by (induct_tac "w" 1);
   1.325 + by (Simp_tac 1);
   1.326 +by (Simp_tac 1);
   1.327 +(* Blast_tac produces PROOF FAILED for depth 8 *)
   1.328 +by(Fast_tac 1);
   1.329 +qed_spec_mp "False_steps_conc";
   1.330 +AddIffs [False_steps_conc];
   1.331 +
   1.332 +(** True in epsclosure **)
   1.333 +
   1.334 +goal thy
   1.335 + "!!L R. (p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*";
   1.336 +be rtrancl_induct 1;
   1.337 + by(Blast_tac 1);
   1.338 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.339 +qed "True_True_eps_concI";
   1.340 +
   1.341 +goal thy
   1.342 + "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
   1.343 +by(induct_tac "w" 1);
   1.344 + by (simp_tac (simpset() addsimps [True_True_eps_concI]) 1);
   1.345 +by (Simp_tac 1);
   1.346 +by(blast_tac (claset() addIs [True_True_eps_concI]) 1);
   1.347 +qed_spec_mp "True_True_steps_concI";
   1.348 +
   1.349 +goal thy
   1.350 + "!!d. (tp,tq) : (eps(conc L R))^* ==> \
   1.351 +\ !p. tp = True#p --> \
   1.352 +\ (? q. tq = True#q & (p,q) : (eps L)^*) | \
   1.353 +\ (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*)";
   1.354 +by(etac rtrancl_induct 1);
   1.355 + by(Blast_tac 1);
   1.356 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.357 +val lemma1a = result();
   1.358 +
   1.359 +goal thy
   1.360 + "!!p. (p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*";
   1.361 +by(etac rtrancl_induct 1);
   1.362 + by(Blast_tac 1);
   1.363 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.364 +val lemma2a = result();
   1.365 +
   1.366 +goalw thy [conc_def,step_def]
   1.367 + "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None";
   1.368 +by(split_all_tac 1);
   1.369 +by (Asm_full_simp_tac 1);
   1.370 +val lemma = result();
   1.371 +
   1.372 +goal thy
   1.373 + "!!L R. (p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
   1.374 +by(etac rtrancl_induct 1);
   1.375 + by(Blast_tac 1);
   1.376 +by (dtac lemma 1);
   1.377 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.378 +val lemma2b = result();
   1.379 +
   1.380 +goalw thy [conc_def,step_def]
   1.381 + "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)";
   1.382 +by(split_all_tac 1);
   1.383 +by(Asm_full_simp_tac 1);
   1.384 +qed "True_False_eps_concI";
   1.385 +
   1.386 +goal thy
   1.387 + "((True#p,q) : (eps(conc L R))^*) = \
   1.388 +\ ((? r. (p,r) : (eps L)^* & q = True#r) | \
   1.389 +\  (? r. (p,r) : (eps L)^* & fin L r & \
   1.390 +\        (? s. (start R, s) : (eps R)^* & q = False#s)))";
   1.391 +by(rtac iffI 1);
   1.392 + by(blast_tac (claset() addDs [lemma1a]) 1);
   1.393 +be disjE 1;
   1.394 + by(blast_tac (claset() addIs [lemma2a]) 1);
   1.395 +by(Clarify_tac 1);
   1.396 +br (rtrancl_trans) 1;
   1.397 +be lemma2a 1;
   1.398 +br (rtrancl_into_rtrancl2) 1;
   1.399 +be True_False_eps_concI 1;
   1.400 +be lemma2b 1;
   1.401 +qed "True_epsclosure_conc";
   1.402 +AddIffs [True_epsclosure_conc];
   1.403 +
   1.404 +(** True in steps **)
   1.405 +
   1.406 +goal thy
   1.407 + "!p. (True#p,q) : steps (conc L R) w --> \
   1.408 +\     ((? r. (p,r) : steps L w & q = True#r)  | \
   1.409 +\      (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
   1.410 +\              (? s. (start R,s) : steps R v & q = False#s))))";
   1.411 +by(induct_tac "w" 1);
   1.412 + by(Simp_tac 1);
   1.413 +by(Simp_tac 1);
   1.414 +by(clarify_tac (claset() delrules [disjCI]) 1);
   1.415 + be disjE 1;
   1.416 + by(clarify_tac (claset() delrules [disjCI]) 1);
   1.417 + be disjE 1;
   1.418 +  by(clarify_tac (claset() delrules [disjCI]) 1);
   1.419 +  by(etac allE 1 THEN mp_tac 1);
   1.420 +  be disjE 1;
   1.421 +   by (Blast_tac 1);
   1.422 +  br disjI2 1;
   1.423 +  by (Clarify_tac 1);
   1.424 +  by(Simp_tac 1);
   1.425 +  by(res_inst_tac[("x","a#u")] exI 1);
   1.426 +  by(Simp_tac 1);
   1.427 +  by (Blast_tac 1);
   1.428 + by (Blast_tac 1);
   1.429 +br disjI2 1;
   1.430 +by (Clarify_tac 1);
   1.431 +by(Simp_tac 1);
   1.432 +by(res_inst_tac[("x","[]")] exI 1);
   1.433 +by(Simp_tac 1);
   1.434 +by (Blast_tac 1);
   1.435 +qed_spec_mp "True_steps_concD";
   1.436 +
   1.437 +goal thy
   1.438 + "(True#p,q) : steps (conc L R) w = \
   1.439 +\ ((? r. (p,r) : steps L w & q = True#r)  | \
   1.440 +\  (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
   1.441 +\          (? s. (start R,s) : steps R v & q = False#s))))";
   1.442 +by(blast_tac (claset() addDs [True_steps_concD]
   1.443 +     addIs [True_True_steps_concI,in_steps_epsclosure,r_into_rtrancl]) 1);
   1.444 +qed "True_steps_conc";
   1.445 +
   1.446 +(** starting from the start **)
   1.447 +
   1.448 +goalw thy [conc_def]
   1.449 +  "!L R. start(conc L R) = True#start L";
   1.450 +by(Simp_tac 1);
   1.451 +qed_spec_mp "start_conc";
   1.452 +
   1.453 +goalw thy [conc_def]
   1.454 + "!L R. fin(conc L R) p = (? s. p = False#s & fin R s)";
   1.455 +by (simp_tac (simpset() addsplits [split_list_case]) 1);
   1.456 +qed_spec_mp "final_conc";
   1.457 +
   1.458 +goal thy
   1.459 + "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
   1.460 +by (simp_tac (simpset() addsimps
   1.461 +     [accepts_def,True_steps_conc,final_conc,start_conc]) 1);
   1.462 +by(Blast_tac 1);
   1.463 +qed "accepts_conc";
   1.464 +
   1.465 +(******************************************************)
   1.466 +(*                       star                         *)
   1.467 +(******************************************************)
   1.468 +
   1.469 +goalw thy [star_def,step_def]
   1.470 + "!A. (True#p,q) : eps(star A) = \
   1.471 +\     ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )";
   1.472 +by(Simp_tac 1);
   1.473 +by(Blast_tac 1);
   1.474 +qed_spec_mp "True_in_eps_star";
   1.475 +AddIffs [True_in_eps_star];
   1.476 +
   1.477 +goalw thy [star_def,step_def]
   1.478 +  "!A. (p,q) : step A a --> (True#p, True#q) : step (star A) a";
   1.479 +by(Simp_tac 1);
   1.480 +qed_spec_mp "True_True_step_starI";
   1.481 +
   1.482 +goal thy
   1.483 +  "!!A. (p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
   1.484 +be rtrancl_induct 1;
   1.485 + by(Blast_tac 1);
   1.486 +by(blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
   1.487 +qed_spec_mp "True_True_eps_starI";
   1.488 +
   1.489 +goalw thy [star_def,step_def]
   1.490 + "!A. fin A p --> (True#p,True#start A) : eps(star A)";
   1.491 +by(Simp_tac 1);
   1.492 +qed_spec_mp "True_start_eps_starI";
   1.493 +
   1.494 +goal thy
   1.495 + "!!dummy. (tp,s) : (eps(star A))^* ==> (! p. tp = True#p --> \
   1.496 +\ (? r. ((p,r) : (eps A)^* | \
   1.497 +\        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
   1.498 +\       s = True#r))";
   1.499 +be rtrancl_induct 1;
   1.500 + by(Simp_tac 1);
   1.501 +by (Clarify_tac 1);
   1.502 +by (Asm_full_simp_tac 1);
   1.503 +by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   1.504 +val lemma = result();
   1.505 +
   1.506 +goal thy
   1.507 + "((True#p,s) : (eps(star A))^*) = \
   1.508 +\ (? r. ((p,r) : (eps A)^* | \
   1.509 +\        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
   1.510 +\       s = True#r)";
   1.511 +br iffI 1;
   1.512 + bd lemma 1;
   1.513 + by(Blast_tac 1);
   1.514 +(* Why can't blast_tac do the rest? *)
   1.515 +by (Clarify_tac 1);
   1.516 +be disjE 1;
   1.517 +be True_True_eps_starI 1;
   1.518 +by (Clarify_tac 1);
   1.519 +br rtrancl_trans 1;
   1.520 +be True_True_eps_starI 1;
   1.521 +br rtrancl_trans 1;
   1.522 +br r_into_rtrancl 1;
   1.523 +be True_start_eps_starI 1;
   1.524 +be True_True_eps_starI 1;
   1.525 +qed "True_eps_star";
   1.526 +AddIffs [True_eps_star];
   1.527 +
   1.528 +(** True in step Some **)
   1.529 +
   1.530 +goalw thy [star_def,step_def]
   1.531 + "!A. (True#p,r): step (star A) (Some a) = \
   1.532 +\     (? q. (p,q): step A (Some a) & r=True#q)";
   1.533 +by(Simp_tac 1);
   1.534 +by(Blast_tac 1);
   1.535 +qed_spec_mp "True_step_star";
   1.536 +AddIffs [True_step_star];
   1.537 +
   1.538 +
   1.539 +(** True in steps **)
   1.540 +
   1.541 +(* reverse list induction! Complicates matters for conc? *)
   1.542 +goal thy
   1.543 + "!rr. (True#start A,rr) : steps (star A) w --> \
   1.544 +\ (? us v. w = concat us @ v & \
   1.545 +\             (!u:set us. accepts A u) & \
   1.546 +\             (? r. (start A,r) : steps A v & rr = True#r))";
   1.547 +by(res_inst_tac [("xs","w")] snoc_induct 1);
   1.548 + by (Asm_full_simp_tac 1);
   1.549 + by (Clarify_tac 1);
   1.550 + by(res_inst_tac [("x","[]")] exI 1);
   1.551 + be disjE 1;
   1.552 +  by (Asm_simp_tac 1);
   1.553 + by (Clarify_tac 1);
   1.554 + by (Asm_simp_tac 1);
   1.555 +by(simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
   1.556 +by (Clarify_tac 1);
   1.557 +by(etac allE 1 THEN mp_tac 1);
   1.558 +by (Clarify_tac 1);
   1.559 +be disjE 1;
   1.560 + by(res_inst_tac [("x","us")] exI 1);
   1.561 + by(res_inst_tac [("x","v@[x]")] exI 1);
   1.562 + by(asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
   1.563 + by(Blast_tac 1);
   1.564 +by (Clarify_tac 1);
   1.565 +by(res_inst_tac [("x","us@[v@[x]]")] exI 1);
   1.566 +by(res_inst_tac [("x","[]")] exI 1);
   1.567 +by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
   1.568 +by(Blast_tac 1);
   1.569 +qed_spec_mp "True_start_steps_starD";
   1.570 +
   1.571 +goal thy "!p. (p,q) : steps A w --> (True#p,True#q) : steps (star A) w";
   1.572 +by(induct_tac "w" 1);
   1.573 + by(Simp_tac 1);
   1.574 +by(Simp_tac 1);
   1.575 +by(blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
   1.576 +qed_spec_mp "True_True_steps_starI";
   1.577 +
   1.578 +goalw thy [accepts_def]
   1.579 + "(!u : set us. accepts A u) --> \
   1.580 +\ (True#start A,True#start A) : steps (star A) (concat us)";
   1.581 +by(induct_tac "us" 1);
   1.582 + by(Simp_tac 1);
   1.583 +by(Simp_tac 1);
   1.584 +by(blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
   1.585 +qed_spec_mp "steps_star_cycle";
   1.586 +
   1.587 +(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
   1.588 +goal thy
   1.589 + "(True#start A,rr) : steps (star A) w = \
   1.590 +\ (? us v. w = concat us @ v & \
   1.591 +\             (!u:set us. accepts A u) & \
   1.592 +\             (? r. (start A,r) : steps A v & rr = True#r))";
   1.593 +br iffI 1;
   1.594 + be True_start_steps_starD 1;
   1.595 +by (Clarify_tac 1);
   1.596 +by(Asm_simp_tac 1);
   1.597 +by(blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
   1.598 +qed "True_start_steps_star";
   1.599 +
   1.600 +(** the start state **)
   1.601 +
   1.602 +goalw thy [star_def,step_def]
   1.603 +  "!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)";
   1.604 +by(Simp_tac 1);
   1.605 +qed_spec_mp "start_step_star";
   1.606 +AddIffs [start_step_star];
   1.607 +
   1.608 +val epsclosure_start_step_star =
   1.609 +  read_instantiate [("p","start(star A)")] in_unfold_rtrancl2;
   1.610 +
   1.611 +goal thy
   1.612 + "(start(star A),r) : steps (star A) w = \
   1.613 +\ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
   1.614 +br iffI 1;
   1.615 + by(exhaust_tac "w" 1);
   1.616 +  by(asm_full_simp_tac (simpset() addsimps
   1.617 +    [epsclosure_start_step_star]) 1);
   1.618 + by(Asm_full_simp_tac 1);
   1.619 + by (Clarify_tac 1);
   1.620 + by(asm_full_simp_tac (simpset() addsimps
   1.621 +    [epsclosure_start_step_star]) 1);
   1.622 + by(Blast_tac 1);
   1.623 +be disjE 1;
   1.624 + by(Asm_simp_tac 1);
   1.625 +by(blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
   1.626 +qed "start_steps_star";
   1.627 +
   1.628 +goalw thy [star_def] "!A. fin (star A) (True#p) = fin A p";
   1.629 +by(Simp_tac 1);
   1.630 +qed_spec_mp "fin_star_True";
   1.631 +AddIffs [fin_star_True];
   1.632 +
   1.633 +goalw thy [star_def] "!A. fin (star A) (start(star A))";
   1.634 +by(Simp_tac 1);
   1.635 +qed_spec_mp "fin_star_start";
   1.636 +AddIffs [fin_star_start];
   1.637 +
   1.638 +(* too complex! Simpler if loop back to start(star A)? *)
   1.639 +goalw thy [accepts_def]
   1.640 + "accepts (star A) w = \
   1.641 +\ (? us. (!u : set(us). accepts A u) & (w = concat us) )";
   1.642 +by(simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
   1.643 +br iffI 1;
   1.644 + by (Clarify_tac 1);
   1.645 + be disjE 1;
   1.646 +  by (Clarify_tac 1);
   1.647 +  by(Simp_tac 1);
   1.648 +  by(res_inst_tac [("x","[]")] exI 1);
   1.649 +  by(Simp_tac 1);
   1.650 + by (Clarify_tac 1);
   1.651 + by(res_inst_tac [("x","us@[v]")] exI 1);
   1.652 + by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
   1.653 + by(Blast_tac 1);
   1.654 +by (Clarify_tac 1);
   1.655 +by(res_inst_tac [("xs","us")] snoc_exhaust 1);
   1.656 + by(Asm_simp_tac 1);
   1.657 + by(Blast_tac 1);
   1.658 +by (Clarify_tac 1);
   1.659 +by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
   1.660 +by(Blast_tac 1);
   1.661 +qed "accepts_star";
   1.662 +
   1.663 +
   1.664 +(***** Correctness of r2n *****)
   1.665 +
   1.666 +goal thy
   1.667 + "!w. accepts (rexp2nae r) w = (w : lang r)";
   1.668 +by(induct_tac "r" 1);
   1.669 +    by(simp_tac (simpset() addsimps [accepts_def]) 1);
   1.670 +   by(simp_tac(simpset() addsimps [accepts_atom]) 1);
   1.671 +  by(asm_simp_tac (simpset() addsimps [accepts_union]) 1);
   1.672 + by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
   1.673 +by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
   1.674 +qed "accepts_rexp2nae";