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