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