src/HOL/Lex/RegExp2NA.ML
author nipkow
Mon Aug 17 11:00:57 1998 +0200 (1998-08-17)
changeset 5323 028e00595280
child 5457 367878234bb2
permissions -rw-r--r--
Direct translation RegExp -> NA!
     1 (*  Title:      HOL/Lex/RegExp2NA.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 Goalw [atom_def,step_def]
    20  "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)";
    21 by(Simp_tac 1);
    22 qed "in_step_atom_Some";
    23 Addsimps [in_step_atom_Some];
    24 
    25 Goal
    26  "([False],[False]) : steps (atom a) w = (w = [])";
    27 by (induct_tac "w" 1);
    28  by(Simp_tac 1);
    29 by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
    30 qed "False_False_in_steps_atom";
    31 
    32 Goal
    33  "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
    34 by (induct_tac "w" 1);
    35  by(asm_simp_tac (simpset() addsimps [start_atom]) 1);
    36 by(asm_full_simp_tac (simpset()
    37      addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
    38 qed "start_fin_in_steps_atom";
    39 
    40 Goal
    41  "accepts (atom a) w = (w = [a])";
    42 by(simp_tac(simpset() addsimps
    43        [accepts_conv_steps,start_fin_in_steps_atom,fin_atom]) 1);
    44 qed "accepts_atom";
    45 
    46 
    47 (******************************************************)
    48 (*                      union                         *)
    49 (******************************************************)
    50 
    51 (***** True/False ueber fin anheben *****)
    52 
    53 Goalw [union_def] 
    54  "!L R. fin (union L R) (True#p) = fin L p";
    55 by (Simp_tac 1);
    56 qed_spec_mp "fin_union_True";
    57 
    58 Goalw [union_def] 
    59  "!L R. fin (union L R) (False#p) = fin R p";
    60 by (Simp_tac 1);
    61 qed_spec_mp "fin_union_False";
    62 
    63 AddIffs [fin_union_True,fin_union_False];
    64 
    65 (***** True/False ueber step anheben *****)
    66 
    67 Goalw [union_def,step_def]
    68 "!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
    69 by (Simp_tac 1);
    70 by(Blast_tac 1);
    71 qed_spec_mp "True_in_step_union";
    72 
    73 Goalw [union_def,step_def]
    74 "!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
    75 by (Simp_tac 1);
    76 by(Blast_tac 1);
    77 qed_spec_mp "False_in_step_union";
    78 
    79 AddIffs [True_in_step_union,False_in_step_union];
    80 
    81 
    82 (***** True/False ueber steps anheben *****)
    83 
    84 Goal
    85  "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
    86 by (induct_tac "w" 1);
    87 by (ALLGOALS Asm_simp_tac);
    88 (* Blast_tac produces PROOF FAILED for depth 8 *)
    89 by(ALLGOALS Fast_tac);
    90 qed_spec_mp "lift_True_over_steps_union";
    91 
    92 Goal 
    93  "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
    94 by (induct_tac "w" 1);
    95 by (ALLGOALS Asm_simp_tac);
    96 (* Blast_tac produces PROOF FAILED for depth 8 *)
    97 by(ALLGOALS Fast_tac);
    98 qed_spec_mp "lift_False_over_steps_union";
    99 
   100 AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
   101 
   102 
   103 (** From the start  **)
   104 
   105 Goalw [union_def,step_def]
   106  "!L R. (start(union L R),q) : step(union L R) a = \
   107 \       (? p. (q = True#p & (start L,p) : step L a) | \
   108 \             (q = False#p & (start R,p) : step R a))";
   109 by(Simp_tac 1);
   110 by(Blast_tac 1);
   111 qed_spec_mp "start_step_union";
   112 AddIffs [start_step_union];
   113 
   114 Goal
   115  "(start(union L R), q) : steps (union L R) w = \
   116 \ ( (w = [] & q = start(union L R)) | \
   117 \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
   118 \                     q = False # p & (start R,p) : steps R w)))";
   119 by(exhaust_tac "w" 1);
   120  by (Asm_simp_tac 1);
   121  by(Blast_tac 1);
   122 by (Asm_simp_tac 1);
   123 by(Blast_tac 1);
   124 qed "steps_union";
   125 
   126 Goalw [union_def]
   127  "!L R. fin (union L R) (start(union L R)) = \
   128 \       (fin L (start L) | fin R (start R))";
   129 by(Simp_tac 1);
   130 qed_spec_mp "fin_start_union";
   131 AddIffs [fin_start_union];
   132 
   133 Goal
   134  "accepts (union L R) w = (accepts L w | accepts R w)";
   135 by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
   136 (* get rid of case_tac: *)
   137 by(case_tac "w = []" 1);
   138 by(Auto_tac);
   139 qed "accepts_union";
   140 AddIffs [accepts_union];
   141 
   142 (******************************************************)
   143 (*                      conc                        *)
   144 (******************************************************)
   145 
   146 (** True/False in fin **)
   147 
   148 Goalw [conc_def]
   149  "!L R. fin (conc L R) (True#p) = (fin L p & fin R (start R))";
   150 by (Simp_tac 1);
   151 qed_spec_mp "fin_conc_True";
   152 
   153 Goalw [conc_def] 
   154  "!L R. fin (conc L R) (False#p) = fin R p";
   155 by (Simp_tac 1);
   156 qed "fin_conc_False";
   157 
   158 AddIffs [fin_conc_True,fin_conc_False];
   159 
   160 (** True/False in step **)
   161 
   162 Goalw [conc_def,step_def]
   163  "!L R. (True#p,q) : step (conc L R) a = \
   164 \       ((? r. q=True#r & (p,r): step L a) | \
   165 \        (fin L p & (? r. q=False#r & (start R,r) : step R a)))";
   166 by (Simp_tac 1);
   167 by(Blast_tac 1);
   168 qed_spec_mp "True_step_conc";
   169 
   170 Goalw [conc_def,step_def]
   171  "!L R. (False#p,q) : step (conc L R) a = \
   172 \       (? r. q = False#r & (p,r) : step R a)";
   173 by (Simp_tac 1);
   174 by(Blast_tac 1);
   175 qed_spec_mp "False_step_conc";
   176 
   177 AddIffs [True_step_conc, False_step_conc];
   178 
   179 (** False in steps **)
   180 
   181 Goal
   182  "!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
   183 by (induct_tac "w" 1);
   184  by (Simp_tac 1);
   185  by(Fast_tac 1);
   186 by (Simp_tac 1);
   187 (* Blast_tac produces PROOF FAILED for depth 8 *)
   188 by(Fast_tac 1);
   189 qed_spec_mp "False_steps_conc";
   190 AddIffs [False_steps_conc];
   191 
   192 (** True in steps **)
   193 
   194 Goal
   195  "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
   196 by(induct_tac "w" 1);
   197  by (Simp_tac 1);
   198 by (Simp_tac 1);
   199 by(Blast_tac 1);
   200 qed_spec_mp "True_True_steps_concI";
   201 
   202 Goal
   203  "!L R. (True#p,False#q) : step (conc L R) a = \
   204 \       (fin L p & (start R,q) : step R a)";
   205 by(Simp_tac 1);
   206 qed "True_False_step_conc";
   207 AddIffs [True_False_step_conc];
   208 
   209 Goal
   210  "!p. (True#p,q) : steps (conc L R) w --> \
   211 \     ((? r. (p,r) : steps L w & q = True#r)  | \
   212 \  (? u a v. w = u@a#v & \
   213 \            (? r. (p,r) : steps L u & fin L r & \
   214 \            (? s. (start R,s) : step R a & \
   215 \            (? t. (s,t) : steps R v & q = False#t)))))";
   216 by(induct_tac "w" 1);
   217  by(Simp_tac 1);
   218 by(Simp_tac 1);
   219 by(clarify_tac (claset() delrules [disjCI]) 1);
   220 be disjE 1;
   221  by(clarify_tac (claset() delrules [disjCI]) 1);
   222  by(etac allE 1 THEN mp_tac 1);
   223  be disjE 1;
   224   by (Blast_tac 1);
   225  br disjI2 1;
   226  by (Clarify_tac 1);
   227  by(Simp_tac 1);
   228  by(res_inst_tac[("x","a#u")] exI 1);
   229  by(Simp_tac 1);
   230  by (Blast_tac 1);
   231 br disjI2 1;
   232 by (Clarify_tac 1);
   233 by(Simp_tac 1);
   234 by(res_inst_tac[("x","[]")] exI 1);
   235 by(Simp_tac 1);
   236 by (Blast_tac 1);
   237 qed_spec_mp "True_steps_concD";
   238 
   239 Goal
   240  "(True#p,q) : steps (conc L R) w = \
   241 \ ((? r. (p,r) : steps L w & q = True#r)  | \
   242 \  (? u a v. w = u@a#v & \
   243 \            (? r. (p,r) : steps L u & fin L r & \
   244 \            (? s. (start R,s) : step R a & \
   245 \            (? t. (s,t) : steps R v & q = False#t)))))";
   246 by(fast_tac (claset() addDs [True_steps_concD]
   247      addIs [True_True_steps_concI] addss simpset()) 1);
   248 qed "True_steps_conc";
   249 
   250 (** starting from the start **)
   251 
   252 Goalw [conc_def]
   253   "!L R. start(conc L R) = True#start L";
   254 by(Simp_tac 1);
   255 qed_spec_mp "start_conc";
   256 
   257 Goalw [conc_def]
   258  "!L R. fin(conc L R) p = ((fin R (start R) & (? s. p = True#s & fin L s)) | \
   259 \                          (? s. p = False#s & fin R s))";
   260 by (simp_tac (simpset() addsplits [list.split]) 1);
   261 by (Blast_tac 1);
   262 qed_spec_mp "final_conc";
   263 
   264 Goal
   265  "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
   266 by (simp_tac (simpset() addsimps
   267      [accepts_conv_steps,True_steps_conc,final_conc,start_conc]) 1);
   268 br iffI 1;
   269  by (Clarify_tac 1);
   270  be disjE 1;
   271   by (Clarify_tac 1);
   272   be disjE 1;
   273    by(res_inst_tac [("x","w")] exI 1);
   274    by(Simp_tac 1);
   275    by(Blast_tac 1);
   276   by(Blast_tac 1);
   277  be disjE 1;
   278   by(Blast_tac 1);
   279  by (Clarify_tac 1);
   280  by(res_inst_tac [("x","u")] exI 1);
   281  by(Simp_tac 1);
   282  by(Blast_tac 1);
   283 by (Clarify_tac 1);
   284 by(exhaust_tac "v" 1);
   285  by(Asm_full_simp_tac 1);
   286  by(Blast_tac 1);
   287 by(Asm_full_simp_tac 1);
   288 by(Blast_tac 1);
   289 qed "accepts_conc";
   290 
   291 (******************************************************)
   292 (*                     epsilon                        *)
   293 (******************************************************)
   294 
   295 Goalw [epsilon_def,step_def] "step epsilon a = {}";
   296 by(Simp_tac 1);
   297 by(Blast_tac 1);
   298 qed "step_epsilon";
   299 Addsimps [step_epsilon];
   300 
   301 Goal "((p,q) : steps epsilon w) = (w=[] & p=q)";
   302 by(induct_tac "w" 1);
   303 by(Auto_tac);
   304 qed "steps_epsilon";
   305 
   306 Goal "accepts epsilon w = (w = [])";
   307 by(simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
   308 by(simp_tac (simpset() addsimps [epsilon_def]) 1);
   309 qed "accepts_epsilon";
   310 AddIffs [accepts_epsilon];
   311 
   312 (******************************************************)
   313 (*                       plus                         *)
   314 (******************************************************)
   315 
   316 Goalw [plus_def] "!A. start (plus A) = start A";
   317 by(Simp_tac 1);
   318 qed_spec_mp "start_plus";
   319 Addsimps [start_plus];
   320 
   321 Goalw [plus_def] "!A. fin (plus A) = fin A";
   322 by(Simp_tac 1);
   323 qed_spec_mp "fin_plus";
   324 AddIffs [fin_plus];
   325 
   326 Goalw [plus_def,step_def]
   327   "!A. (p,q) : step A a --> (p,q) : step (plus A) a";
   328 by(Simp_tac 1);
   329 qed_spec_mp "step_plusI";
   330 
   331 Goal "!p. (p,q) : steps A w --> (p,q) : steps (plus A) w";
   332 by(induct_tac "w" 1);
   333  by(Simp_tac 1);
   334 by(Simp_tac 1);
   335 by(blast_tac (claset() addIs [step_plusI]) 1);
   336 qed_spec_mp "steps_plusI";
   337 
   338 Goalw [plus_def,step_def]
   339  "!A. (p,r): step (plus A) a = \
   340 \     ( (p,r): step A a | fin A p & (start A,r) : step A a )";
   341 by(Simp_tac 1);
   342 qed_spec_mp "step_plus_conv";
   343 AddIffs [step_plus_conv];
   344 
   345 Goal
   346  "[| (start A,q) : steps A u; u ~= []; fin A p |] \
   347 \ ==> (p,q) : steps (plus A) u";
   348 by(exhaust_tac "u" 1);
   349  by(Blast_tac 1);
   350 by(Asm_full_simp_tac 1);
   351 by(blast_tac (claset() addIs [steps_plusI]) 1);
   352 qed "fin_steps_plusI";
   353 
   354 (* reverse list induction! Complicates matters for conc? *)
   355 Goal
   356  "!r. (start A,r) : steps (plus A) w --> \
   357 \     (? us v. w = concat us @ v & \
   358 \              (!u:set us. u ~= [] & accepts A u) & \
   359 \              (start A,r) : steps A v)";
   360 by(rev_induct_tac "w" 1);
   361  by (Simp_tac 1);
   362  by(res_inst_tac [("x","[]")] exI 1);
   363  by (Simp_tac 1);
   364 by (Simp_tac 1);
   365 by (Clarify_tac 1);
   366 by(etac allE 1 THEN mp_tac 1);
   367 by (Clarify_tac 1);
   368 be disjE 1;
   369  by(res_inst_tac [("x","us")] exI 1);
   370  by(Asm_simp_tac 1);
   371  by(Blast_tac 1);
   372 by(exhaust_tac "v" 1);
   373  by(res_inst_tac [("x","us")] exI 1);
   374  by(Asm_full_simp_tac 1);
   375 by(res_inst_tac [("x","us@[v]")] exI 1);
   376 by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   377 by(Blast_tac 1);
   378 qed_spec_mp "start_steps_plusD";
   379 
   380 Goal
   381  "!r. (start A,r) : steps (plus A) w --> \
   382 \     (? us v. w = concat us @ v & \
   383 \              (!u:set us. accepts A u) & \
   384 \              (start A,r) : steps A v)";
   385 by(rev_induct_tac "w" 1);
   386  by (Simp_tac 1);
   387  by(res_inst_tac [("x","[]")] exI 1);
   388  by (Simp_tac 1);
   389 by (Simp_tac 1);
   390 by (Clarify_tac 1);
   391 by(etac allE 1 THEN mp_tac 1);
   392 by (Clarify_tac 1);
   393 be disjE 1;
   394  by(res_inst_tac [("x","us")] exI 1);
   395  by(Asm_simp_tac 1);
   396  by(Blast_tac 1);
   397 by(res_inst_tac [("x","us@[v]")] exI 1);
   398 by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   399 by(Blast_tac 1);
   400 qed_spec_mp "start_steps_plusD";
   401 
   402 Goal
   403  "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
   404 by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   405 by(rev_induct_tac "us" 1);
   406  by(Simp_tac 1);
   407 by(rename_tac "u us" 1);
   408 by(Simp_tac 1);
   409 by (Clarify_tac 1);
   410 by(case_tac "us = []" 1);
   411  by(Asm_full_simp_tac 1);
   412  by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   413 by (Clarify_tac 1);
   414 by(case_tac "u = []" 1);
   415  by(Asm_full_simp_tac 1);
   416  by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   417 by(Asm_full_simp_tac 1);
   418 by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   419 qed_spec_mp "steps_star_cycle";
   420 
   421 Goal
   422  "accepts (plus A) w = \
   423 \ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))";
   424 br iffI 1;
   425  by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   426  by (Clarify_tac 1);
   427  bd start_steps_plusD 1;
   428  by (Clarify_tac 1);
   429  by(res_inst_tac [("x","us@[v]")] exI 1);
   430  by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   431  by(Blast_tac 1);
   432 by(blast_tac (claset() addIs [steps_star_cycle]) 1);
   433 qed "accepts_plus";
   434 AddIffs [accepts_plus];
   435 
   436 (******************************************************)
   437 (*                       star                         *)
   438 (******************************************************)
   439 
   440 Goalw [star_def]
   441 "accepts (star A) w = \
   442 \ (? us. (!u : set us. accepts A u) & w = concat us)";
   443 br iffI 1;
   444  by (Clarify_tac 1);
   445  be disjE 1;
   446   by(res_inst_tac [("x","[]")] exI 1);
   447   by(Simp_tac 1);
   448   by(Blast_tac 1);
   449  by(Blast_tac 1);
   450 by(Auto_tac);
   451 qed "accepts_star";
   452 
   453 (***** Correctness of r2n *****)
   454 
   455 Goal
   456  "!w. accepts (rexp2na r) w = (w : lang r)";
   457 by(induct_tac "r" 1);
   458     by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   459    by(simp_tac(simpset() addsimps [accepts_atom]) 1);
   460   by(Asm_simp_tac 1);
   461  by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
   462 by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
   463 qed_spec_mp "accepts_rexp2na";