1.1 --- a/src/HOL/Lex/Automata.ML Mon Aug 17 11:00:27 1998 +0200
1.2 +++ b/src/HOL/Lex/Automata.ML Mon Aug 17 11:00:57 1998 +0200
1.3 @@ -4,7 +4,7 @@
1.4 Copyright 1998 TUM
1.5 *)
1.6
1.7 -(*** Equivalence of NA and DA --- redundant ***)
1.8 +(*** Equivalence of NA and DA ***)
1.9
1.10 Goalw [na2da_def]
1.11 "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Lex/NA.ML Mon Aug 17 11:00:57 1998 +0200
2.3 @@ -0,0 +1,29 @@
2.4 +(* Title: HOL/Lex/NA.ML
2.5 + ID: $Id$
2.6 + Author: Tobias Nipkow
2.7 + Copyright 1998 TUM
2.8 +*)
2.9 +
2.10 +Goal
2.11 + "steps A (v@w) = steps A w O steps A v";
2.12 +by (induct_tac "v" 1);
2.13 +by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
2.14 +qed "steps_append";
2.15 +Addsimps [steps_append];
2.16 +
2.17 +Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
2.18 +by(rtac (steps_append RS equalityE) 1);
2.19 +by(Blast_tac 1);
2.20 +qed "in_steps_append";
2.21 +AddIffs [in_steps_append];
2.22 +
2.23 +Goal
2.24 + "!p. delta A w p = {q. (p,q) : steps A w}";
2.25 +by(induct_tac "w" 1);
2.26 +by(auto_tac (claset(), simpset() addsimps [step_def]));
2.27 +qed_spec_mp "delta_conv_steps";
2.28 +
2.29 +Goalw [accepts_def]
2.30 + "accepts A w = (? q. (start A,q) : steps A w & fin A q)";
2.31 +by(simp_tac (simpset() addsimps [delta_conv_steps]) 1);
2.32 +qed "accepts_conv_steps";
3.1 --- a/src/HOL/Lex/NA.thy Mon Aug 17 11:00:27 1998 +0200
3.2 +++ b/src/HOL/Lex/NA.thy Mon Aug 17 11:00:57 1998 +0200
3.3 @@ -19,4 +19,13 @@
3.4 accepts :: ('a,'s)na => 'a list => bool
3.5 "accepts A w == ? q : delta A w (start A). fin A q"
3.6
3.7 +constdefs
3.8 + step :: "('a,'s)na => 'a => ('s * 's)set"
3.9 +"step A a == {(p,q) . q : next A a p}"
3.10 +
3.11 +consts steps :: "('a,'s)na => 'a list => ('s * 's)set"
3.12 +primrec
3.13 +"steps A [] = id"
3.14 +"steps A (a#w) = steps A w O step A a"
3.15 +
3.16 end
4.1 --- a/src/HOL/Lex/ROOT.ML Mon Aug 17 11:00:27 1998 +0200
4.2 +++ b/src/HOL/Lex/ROOT.ML Mon Aug 17 11:00:57 1998 +0200
4.3 @@ -14,5 +14,6 @@
4.4 Or via ML-bound names of axioms that are overwritten?
4.5 *)
4.6 use_thy"RegSet_of_nat_DA";
4.7 +use_thy"RegExp2NA";
4.8 use_thy"RegExp2NAe";
4.9 use_thy"Scanner";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Lex/RegExp2NA.ML Mon Aug 17 11:00:57 1998 +0200
5.3 @@ -0,0 +1,463 @@
5.4 +(* Title: HOL/Lex/RegExp2NA.ML
5.5 + ID: $Id$
5.6 + Author: Tobias Nipkow
5.7 + Copyright 1998 TUM
5.8 +*)
5.9 +
5.10 +(******************************************************)
5.11 +(* atom *)
5.12 +(******************************************************)
5.13 +
5.14 +Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
5.15 +by(Simp_tac 1);
5.16 +qed "fin_atom";
5.17 +
5.18 +Goalw [atom_def] "start (atom a) = [True]";
5.19 +by(Simp_tac 1);
5.20 +qed "start_atom";
5.21 +
5.22 +Goalw [atom_def,step_def]
5.23 + "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)";
5.24 +by(Simp_tac 1);
5.25 +qed "in_step_atom_Some";
5.26 +Addsimps [in_step_atom_Some];
5.27 +
5.28 +Goal
5.29 + "([False],[False]) : steps (atom a) w = (w = [])";
5.30 +by (induct_tac "w" 1);
5.31 + by(Simp_tac 1);
5.32 +by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
5.33 +qed "False_False_in_steps_atom";
5.34 +
5.35 +Goal
5.36 + "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
5.37 +by (induct_tac "w" 1);
5.38 + by(asm_simp_tac (simpset() addsimps [start_atom]) 1);
5.39 +by(asm_full_simp_tac (simpset()
5.40 + addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
5.41 +qed "start_fin_in_steps_atom";
5.42 +
5.43 +Goal
5.44 + "accepts (atom a) w = (w = [a])";
5.45 +by(simp_tac(simpset() addsimps
5.46 + [accepts_conv_steps,start_fin_in_steps_atom,fin_atom]) 1);
5.47 +qed "accepts_atom";
5.48 +
5.49 +
5.50 +(******************************************************)
5.51 +(* union *)
5.52 +(******************************************************)
5.53 +
5.54 +(***** True/False ueber fin anheben *****)
5.55 +
5.56 +Goalw [union_def]
5.57 + "!L R. fin (union L R) (True#p) = fin L p";
5.58 +by (Simp_tac 1);
5.59 +qed_spec_mp "fin_union_True";
5.60 +
5.61 +Goalw [union_def]
5.62 + "!L R. fin (union L R) (False#p) = fin R p";
5.63 +by (Simp_tac 1);
5.64 +qed_spec_mp "fin_union_False";
5.65 +
5.66 +AddIffs [fin_union_True,fin_union_False];
5.67 +
5.68 +(***** True/False ueber step anheben *****)
5.69 +
5.70 +Goalw [union_def,step_def]
5.71 +"!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
5.72 +by (Simp_tac 1);
5.73 +by(Blast_tac 1);
5.74 +qed_spec_mp "True_in_step_union";
5.75 +
5.76 +Goalw [union_def,step_def]
5.77 +"!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
5.78 +by (Simp_tac 1);
5.79 +by(Blast_tac 1);
5.80 +qed_spec_mp "False_in_step_union";
5.81 +
5.82 +AddIffs [True_in_step_union,False_in_step_union];
5.83 +
5.84 +
5.85 +(***** True/False ueber steps anheben *****)
5.86 +
5.87 +Goal
5.88 + "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
5.89 +by (induct_tac "w" 1);
5.90 +by (ALLGOALS Asm_simp_tac);
5.91 +(* Blast_tac produces PROOF FAILED for depth 8 *)
5.92 +by(ALLGOALS Fast_tac);
5.93 +qed_spec_mp "lift_True_over_steps_union";
5.94 +
5.95 +Goal
5.96 + "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
5.97 +by (induct_tac "w" 1);
5.98 +by (ALLGOALS Asm_simp_tac);
5.99 +(* Blast_tac produces PROOF FAILED for depth 8 *)
5.100 +by(ALLGOALS Fast_tac);
5.101 +qed_spec_mp "lift_False_over_steps_union";
5.102 +
5.103 +AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
5.104 +
5.105 +
5.106 +(** From the start **)
5.107 +
5.108 +Goalw [union_def,step_def]
5.109 + "!L R. (start(union L R),q) : step(union L R) a = \
5.110 +\ (? p. (q = True#p & (start L,p) : step L a) | \
5.111 +\ (q = False#p & (start R,p) : step R a))";
5.112 +by(Simp_tac 1);
5.113 +by(Blast_tac 1);
5.114 +qed_spec_mp "start_step_union";
5.115 +AddIffs [start_step_union];
5.116 +
5.117 +Goal
5.118 + "(start(union L R), q) : steps (union L R) w = \
5.119 +\ ( (w = [] & q = start(union L R)) | \
5.120 +\ (w ~= [] & (? p. q = True # p & (start L,p) : steps L w | \
5.121 +\ q = False # p & (start R,p) : steps R w)))";
5.122 +by(exhaust_tac "w" 1);
5.123 + by (Asm_simp_tac 1);
5.124 + by(Blast_tac 1);
5.125 +by (Asm_simp_tac 1);
5.126 +by(Blast_tac 1);
5.127 +qed "steps_union";
5.128 +
5.129 +Goalw [union_def]
5.130 + "!L R. fin (union L R) (start(union L R)) = \
5.131 +\ (fin L (start L) | fin R (start R))";
5.132 +by(Simp_tac 1);
5.133 +qed_spec_mp "fin_start_union";
5.134 +AddIffs [fin_start_union];
5.135 +
5.136 +Goal
5.137 + "accepts (union L R) w = (accepts L w | accepts R w)";
5.138 +by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
5.139 +(* get rid of case_tac: *)
5.140 +by(case_tac "w = []" 1);
5.141 +by(Auto_tac);
5.142 +qed "accepts_union";
5.143 +AddIffs [accepts_union];
5.144 +
5.145 +(******************************************************)
5.146 +(* conc *)
5.147 +(******************************************************)
5.148 +
5.149 +(** True/False in fin **)
5.150 +
5.151 +Goalw [conc_def]
5.152 + "!L R. fin (conc L R) (True#p) = (fin L p & fin R (start R))";
5.153 +by (Simp_tac 1);
5.154 +qed_spec_mp "fin_conc_True";
5.155 +
5.156 +Goalw [conc_def]
5.157 + "!L R. fin (conc L R) (False#p) = fin R p";
5.158 +by (Simp_tac 1);
5.159 +qed "fin_conc_False";
5.160 +
5.161 +AddIffs [fin_conc_True,fin_conc_False];
5.162 +
5.163 +(** True/False in step **)
5.164 +
5.165 +Goalw [conc_def,step_def]
5.166 + "!L R. (True#p,q) : step (conc L R) a = \
5.167 +\ ((? r. q=True#r & (p,r): step L a) | \
5.168 +\ (fin L p & (? r. q=False#r & (start R,r) : step R a)))";
5.169 +by (Simp_tac 1);
5.170 +by(Blast_tac 1);
5.171 +qed_spec_mp "True_step_conc";
5.172 +
5.173 +Goalw [conc_def,step_def]
5.174 + "!L R. (False#p,q) : step (conc L R) a = \
5.175 +\ (? r. q = False#r & (p,r) : step R a)";
5.176 +by (Simp_tac 1);
5.177 +by(Blast_tac 1);
5.178 +qed_spec_mp "False_step_conc";
5.179 +
5.180 +AddIffs [True_step_conc, False_step_conc];
5.181 +
5.182 +(** False in steps **)
5.183 +
5.184 +Goal
5.185 + "!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
5.186 +by (induct_tac "w" 1);
5.187 + by (Simp_tac 1);
5.188 + by(Fast_tac 1);
5.189 +by (Simp_tac 1);
5.190 +(* Blast_tac produces PROOF FAILED for depth 8 *)
5.191 +by(Fast_tac 1);
5.192 +qed_spec_mp "False_steps_conc";
5.193 +AddIffs [False_steps_conc];
5.194 +
5.195 +(** True in steps **)
5.196 +
5.197 +Goal
5.198 + "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
5.199 +by(induct_tac "w" 1);
5.200 + by (Simp_tac 1);
5.201 +by (Simp_tac 1);
5.202 +by(Blast_tac 1);
5.203 +qed_spec_mp "True_True_steps_concI";
5.204 +
5.205 +Goal
5.206 + "!L R. (True#p,False#q) : step (conc L R) a = \
5.207 +\ (fin L p & (start R,q) : step R a)";
5.208 +by(Simp_tac 1);
5.209 +qed "True_False_step_conc";
5.210 +AddIffs [True_False_step_conc];
5.211 +
5.212 +Goal
5.213 + "!p. (True#p,q) : steps (conc L R) w --> \
5.214 +\ ((? r. (p,r) : steps L w & q = True#r) | \
5.215 +\ (? u a v. w = u@a#v & \
5.216 +\ (? r. (p,r) : steps L u & fin L r & \
5.217 +\ (? s. (start R,s) : step R a & \
5.218 +\ (? t. (s,t) : steps R v & q = False#t)))))";
5.219 +by(induct_tac "w" 1);
5.220 + by(Simp_tac 1);
5.221 +by(Simp_tac 1);
5.222 +by(clarify_tac (claset() delrules [disjCI]) 1);
5.223 +be disjE 1;
5.224 + by(clarify_tac (claset() delrules [disjCI]) 1);
5.225 + by(etac allE 1 THEN mp_tac 1);
5.226 + be disjE 1;
5.227 + by (Blast_tac 1);
5.228 + br disjI2 1;
5.229 + by (Clarify_tac 1);
5.230 + by(Simp_tac 1);
5.231 + by(res_inst_tac[("x","a#u")] exI 1);
5.232 + by(Simp_tac 1);
5.233 + by (Blast_tac 1);
5.234 +br disjI2 1;
5.235 +by (Clarify_tac 1);
5.236 +by(Simp_tac 1);
5.237 +by(res_inst_tac[("x","[]")] exI 1);
5.238 +by(Simp_tac 1);
5.239 +by (Blast_tac 1);
5.240 +qed_spec_mp "True_steps_concD";
5.241 +
5.242 +Goal
5.243 + "(True#p,q) : steps (conc L R) w = \
5.244 +\ ((? r. (p,r) : steps L w & q = True#r) | \
5.245 +\ (? u a v. w = u@a#v & \
5.246 +\ (? r. (p,r) : steps L u & fin L r & \
5.247 +\ (? s. (start R,s) : step R a & \
5.248 +\ (? t. (s,t) : steps R v & q = False#t)))))";
5.249 +by(fast_tac (claset() addDs [True_steps_concD]
5.250 + addIs [True_True_steps_concI] addss simpset()) 1);
5.251 +qed "True_steps_conc";
5.252 +
5.253 +(** starting from the start **)
5.254 +
5.255 +Goalw [conc_def]
5.256 + "!L R. start(conc L R) = True#start L";
5.257 +by(Simp_tac 1);
5.258 +qed_spec_mp "start_conc";
5.259 +
5.260 +Goalw [conc_def]
5.261 + "!L R. fin(conc L R) p = ((fin R (start R) & (? s. p = True#s & fin L s)) | \
5.262 +\ (? s. p = False#s & fin R s))";
5.263 +by (simp_tac (simpset() addsplits [list.split]) 1);
5.264 +by (Blast_tac 1);
5.265 +qed_spec_mp "final_conc";
5.266 +
5.267 +Goal
5.268 + "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
5.269 +by (simp_tac (simpset() addsimps
5.270 + [accepts_conv_steps,True_steps_conc,final_conc,start_conc]) 1);
5.271 +br iffI 1;
5.272 + by (Clarify_tac 1);
5.273 + be disjE 1;
5.274 + by (Clarify_tac 1);
5.275 + be disjE 1;
5.276 + by(res_inst_tac [("x","w")] exI 1);
5.277 + by(Simp_tac 1);
5.278 + by(Blast_tac 1);
5.279 + by(Blast_tac 1);
5.280 + be disjE 1;
5.281 + by(Blast_tac 1);
5.282 + by (Clarify_tac 1);
5.283 + by(res_inst_tac [("x","u")] exI 1);
5.284 + by(Simp_tac 1);
5.285 + by(Blast_tac 1);
5.286 +by (Clarify_tac 1);
5.287 +by(exhaust_tac "v" 1);
5.288 + by(Asm_full_simp_tac 1);
5.289 + by(Blast_tac 1);
5.290 +by(Asm_full_simp_tac 1);
5.291 +by(Blast_tac 1);
5.292 +qed "accepts_conc";
5.293 +
5.294 +(******************************************************)
5.295 +(* epsilon *)
5.296 +(******************************************************)
5.297 +
5.298 +Goalw [epsilon_def,step_def] "step epsilon a = {}";
5.299 +by(Simp_tac 1);
5.300 +by(Blast_tac 1);
5.301 +qed "step_epsilon";
5.302 +Addsimps [step_epsilon];
5.303 +
5.304 +Goal "((p,q) : steps epsilon w) = (w=[] & p=q)";
5.305 +by(induct_tac "w" 1);
5.306 +by(Auto_tac);
5.307 +qed "steps_epsilon";
5.308 +
5.309 +Goal "accepts epsilon w = (w = [])";
5.310 +by(simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
5.311 +by(simp_tac (simpset() addsimps [epsilon_def]) 1);
5.312 +qed "accepts_epsilon";
5.313 +AddIffs [accepts_epsilon];
5.314 +
5.315 +(******************************************************)
5.316 +(* plus *)
5.317 +(******************************************************)
5.318 +
5.319 +Goalw [plus_def] "!A. start (plus A) = start A";
5.320 +by(Simp_tac 1);
5.321 +qed_spec_mp "start_plus";
5.322 +Addsimps [start_plus];
5.323 +
5.324 +Goalw [plus_def] "!A. fin (plus A) = fin A";
5.325 +by(Simp_tac 1);
5.326 +qed_spec_mp "fin_plus";
5.327 +AddIffs [fin_plus];
5.328 +
5.329 +Goalw [plus_def,step_def]
5.330 + "!A. (p,q) : step A a --> (p,q) : step (plus A) a";
5.331 +by(Simp_tac 1);
5.332 +qed_spec_mp "step_plusI";
5.333 +
5.334 +Goal "!p. (p,q) : steps A w --> (p,q) : steps (plus A) w";
5.335 +by(induct_tac "w" 1);
5.336 + by(Simp_tac 1);
5.337 +by(Simp_tac 1);
5.338 +by(blast_tac (claset() addIs [step_plusI]) 1);
5.339 +qed_spec_mp "steps_plusI";
5.340 +
5.341 +Goalw [plus_def,step_def]
5.342 + "!A. (p,r): step (plus A) a = \
5.343 +\ ( (p,r): step A a | fin A p & (start A,r) : step A a )";
5.344 +by(Simp_tac 1);
5.345 +qed_spec_mp "step_plus_conv";
5.346 +AddIffs [step_plus_conv];
5.347 +
5.348 +Goal
5.349 + "[| (start A,q) : steps A u; u ~= []; fin A p |] \
5.350 +\ ==> (p,q) : steps (plus A) u";
5.351 +by(exhaust_tac "u" 1);
5.352 + by(Blast_tac 1);
5.353 +by(Asm_full_simp_tac 1);
5.354 +by(blast_tac (claset() addIs [steps_plusI]) 1);
5.355 +qed "fin_steps_plusI";
5.356 +
5.357 +(* reverse list induction! Complicates matters for conc? *)
5.358 +Goal
5.359 + "!r. (start A,r) : steps (plus A) w --> \
5.360 +\ (? us v. w = concat us @ v & \
5.361 +\ (!u:set us. u ~= [] & accepts A u) & \
5.362 +\ (start A,r) : steps A v)";
5.363 +by(rev_induct_tac "w" 1);
5.364 + by (Simp_tac 1);
5.365 + by(res_inst_tac [("x","[]")] exI 1);
5.366 + by (Simp_tac 1);
5.367 +by (Simp_tac 1);
5.368 +by (Clarify_tac 1);
5.369 +by(etac allE 1 THEN mp_tac 1);
5.370 +by (Clarify_tac 1);
5.371 +be disjE 1;
5.372 + by(res_inst_tac [("x","us")] exI 1);
5.373 + by(Asm_simp_tac 1);
5.374 + by(Blast_tac 1);
5.375 +by(exhaust_tac "v" 1);
5.376 + by(res_inst_tac [("x","us")] exI 1);
5.377 + by(Asm_full_simp_tac 1);
5.378 +by(res_inst_tac [("x","us@[v]")] exI 1);
5.379 +by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
5.380 +by(Blast_tac 1);
5.381 +qed_spec_mp "start_steps_plusD";
5.382 +
5.383 +Goal
5.384 + "!r. (start A,r) : steps (plus A) w --> \
5.385 +\ (? us v. w = concat us @ v & \
5.386 +\ (!u:set us. accepts A u) & \
5.387 +\ (start A,r) : steps A v)";
5.388 +by(rev_induct_tac "w" 1);
5.389 + by (Simp_tac 1);
5.390 + by(res_inst_tac [("x","[]")] exI 1);
5.391 + by (Simp_tac 1);
5.392 +by (Simp_tac 1);
5.393 +by (Clarify_tac 1);
5.394 +by(etac allE 1 THEN mp_tac 1);
5.395 +by (Clarify_tac 1);
5.396 +be disjE 1;
5.397 + by(res_inst_tac [("x","us")] exI 1);
5.398 + by(Asm_simp_tac 1);
5.399 + by(Blast_tac 1);
5.400 +by(res_inst_tac [("x","us@[v]")] exI 1);
5.401 +by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
5.402 +by(Blast_tac 1);
5.403 +qed_spec_mp "start_steps_plusD";
5.404 +
5.405 +Goal
5.406 + "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
5.407 +by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
5.408 +by(rev_induct_tac "us" 1);
5.409 + by(Simp_tac 1);
5.410 +by(rename_tac "u us" 1);
5.411 +by(Simp_tac 1);
5.412 +by (Clarify_tac 1);
5.413 +by(case_tac "us = []" 1);
5.414 + by(Asm_full_simp_tac 1);
5.415 + by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
5.416 +by (Clarify_tac 1);
5.417 +by(case_tac "u = []" 1);
5.418 + by(Asm_full_simp_tac 1);
5.419 + by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
5.420 +by(Asm_full_simp_tac 1);
5.421 +by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
5.422 +qed_spec_mp "steps_star_cycle";
5.423 +
5.424 +Goal
5.425 + "accepts (plus A) w = \
5.426 +\ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))";
5.427 +br iffI 1;
5.428 + by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
5.429 + by (Clarify_tac 1);
5.430 + bd start_steps_plusD 1;
5.431 + by (Clarify_tac 1);
5.432 + by(res_inst_tac [("x","us@[v]")] exI 1);
5.433 + by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
5.434 + by(Blast_tac 1);
5.435 +by(blast_tac (claset() addIs [steps_star_cycle]) 1);
5.436 +qed "accepts_plus";
5.437 +AddIffs [accepts_plus];
5.438 +
5.439 +(******************************************************)
5.440 +(* star *)
5.441 +(******************************************************)
5.442 +
5.443 +Goalw [star_def]
5.444 +"accepts (star A) w = \
5.445 +\ (? us. (!u : set us. accepts A u) & w = concat us)";
5.446 +br iffI 1;
5.447 + by (Clarify_tac 1);
5.448 + be disjE 1;
5.449 + by(res_inst_tac [("x","[]")] exI 1);
5.450 + by(Simp_tac 1);
5.451 + by(Blast_tac 1);
5.452 + by(Blast_tac 1);
5.453 +by(Auto_tac);
5.454 +qed "accepts_star";
5.455 +
5.456 +(***** Correctness of r2n *****)
5.457 +
5.458 +Goal
5.459 + "!w. accepts (rexp2na r) w = (w : lang r)";
5.460 +by(induct_tac "r" 1);
5.461 + by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
5.462 + by(simp_tac(simpset() addsimps [accepts_atom]) 1);
5.463 + by(Asm_simp_tac 1);
5.464 + by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
5.465 +by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
5.466 +qed_spec_mp "accepts_rexp2na";
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/Lex/RegExp2NA.thy Mon Aug 17 11:00:57 1998 +0200
6.3 @@ -0,0 +1,60 @@
6.4 +(* Title: HOL/Lex/RegExp2NA.thy
6.5 + ID: $Id$
6.6 + Author: Tobias Nipkow
6.7 + Copyright 1998 TUM
6.8 +
6.9 +Conversion of regular expressions *directly*
6.10 +into nondeterministic automata *without* epsilon transitions
6.11 +*)
6.12 +
6.13 +RegExp2NA = NA + RegExp +
6.14 +
6.15 +types 'a bitsNA = ('a,bool list)na
6.16 +
6.17 +syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
6.18 +translations "x ## S" == "op # x `` S"
6.19 +
6.20 +constdefs
6.21 + atom :: 'a => 'a bitsNA
6.22 +"atom a == ([True],
6.23 + %b s. if s=[True] & b=a then {[False]} else {},
6.24 + %s. s=[False])"
6.25 +
6.26 + union :: 'a bitsNA => 'a bitsNA => 'a bitsNA
6.27 +"union == %(ql,dl,fl)(qr,dr,fr).
6.28 + ([],
6.29 + %a s. case s of
6.30 + [] => (True ## dl a ql) Un (False ## dr a qr)
6.31 + | left#s => if left then True ## dl a s
6.32 + else False ## dr a s,
6.33 + %s. case s of [] => (fl ql | fr qr)
6.34 + | left#s => if left then fl s else fr s)"
6.35 +
6.36 + conc :: 'a bitsNA => 'a bitsNA => 'a bitsNA
6.37 +"conc == %(ql,dl,fl)(qr,dr,fr).
6.38 + (True#ql,
6.39 + %a s. case s of
6.40 + [] => {}
6.41 + | left#s => if left then (True ## dl a s) Un
6.42 + (if fl s then False ## dr a qr else {})
6.43 + else False ## dr a s,
6.44 + %s. case s of [] => False | left#s => left & fl s & fr qr | ~left & fr s)"
6.45 +
6.46 + epsilon :: 'a bitsNA
6.47 +"epsilon == ([],%a s. {}, %s. s=[])"
6.48 +
6.49 + plus :: 'a bitsNA => 'a bitsNA
6.50 +"plus == %(q,d,f). (q, %a s. d a s Un (if f s then d a q else {}), f)"
6.51 +
6.52 + star :: 'a bitsNA => 'a bitsNA
6.53 +"star A == union epsilon (plus A)"
6.54 +
6.55 +consts rexp2na :: 'a rexp => 'a bitsNA
6.56 +primrec
6.57 +"rexp2na Empty = ([], %a s. {}, %s. False)"
6.58 +"rexp2na(Atom a) = atom a"
6.59 +"rexp2na(Union r s) = union (rexp2na r) (rexp2na s)"
6.60 +"rexp2na(Conc r s) = conc (rexp2na r) (rexp2na s)"
6.61 +"rexp2na(Star r) = star (rexp2na r)"
6.62 +
6.63 +end
7.1 --- a/src/HOL/Lex/Scanner.ML Mon Aug 17 11:00:27 1998 +0200
7.2 +++ b/src/HOL/Lex/Scanner.ML Mon Aug 17 11:00:57 1998 +0200
7.3 @@ -5,6 +5,11 @@
7.4 *)
7.5
7.6 Goal
7.7 + "DA.accepts (na2da(rexp2na r)) w = (w : lang r)";
7.8 +by (simp_tac (simpset() addsimps [NA_DA_equiv RS sym,accepts_rexp2na]) 1);
7.9 +qed "accepts_na2da_rexp2na";
7.10 +
7.11 +Goal
7.12 "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)";
7.13 by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
7.14 qed "accepts_nae2da_rexp2nae";
8.1 --- a/src/HOL/Lex/Scanner.thy Mon Aug 17 11:00:27 1998 +0200
8.2 +++ b/src/HOL/Lex/Scanner.thy Mon Aug 17 11:00:57 1998 +0200
8.3 @@ -4,4 +4,4 @@
8.4 Copyright 1998 TUM
8.5 *)
8.6
8.7 -Scanner = Automata + RegExp2NAe
8.8 +Scanner = Automata + RegExp2NA + RegExp2NAe