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