src/HOL/Lex/RegExp2NAe.ML
author nipkow
Thu Jan 17 19:32:22 2002 +0100 (2002-01-17)
changeset 12792 b344226f924c
parent 12566 fe20540bcf93
child 13145 59bc43b51aa2
permissions -rw-r--r--
Added code generation to Scanner.thy
Renamed Union -> Or, union -> or
nipkow@4907
     1
(*  Title:      HOL/Lex/RegExp2NAe.ML
nipkow@4907
     2
    ID:         $Id$
nipkow@4907
     3
    Author:     Tobias Nipkow
nipkow@4907
     4
    Copyright   1998 TUM
nipkow@4907
     5
*)
nipkow@4907
     6
nipkow@4907
     7
(******************************************************)
nipkow@4907
     8
(*                       atom                         *)
nipkow@4907
     9
(******************************************************)
nipkow@4907
    10
wenzelm@5069
    11
Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
wenzelm@5132
    12
by (Simp_tac 1);
nipkow@4907
    13
qed "fin_atom";
nipkow@4907
    14
wenzelm@5069
    15
Goalw [atom_def] "start (atom a) = [True]";
wenzelm@5132
    16
by (Simp_tac 1);
nipkow@4907
    17
qed "start_atom";
nipkow@4907
    18
nipkow@4907
    19
(* Use {x. False} = {}? *)
nipkow@4907
    20
wenzelm@5069
    21
Goalw [atom_def,step_def]
nipkow@4907
    22
 "eps(atom a) = {}";
wenzelm@5132
    23
by (Simp_tac 1);
nipkow@4907
    24
qed "eps_atom";
nipkow@4907
    25
Addsimps [eps_atom];
nipkow@4907
    26
wenzelm@5069
    27
Goalw [atom_def,step_def]
nipkow@4907
    28
 "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)";
wenzelm@5132
    29
by (Simp_tac 1);
nipkow@4907
    30
qed "in_step_atom_Some";
nipkow@4907
    31
Addsimps [in_step_atom_Some];
nipkow@4907
    32
nipkow@5118
    33
Goal "([False],[False]) : steps (atom a) w = (w = [])";
nipkow@4907
    34
by (induct_tac "w" 1);
wenzelm@5132
    35
 by (Simp_tac 1);
nipkow@12487
    36
by (asm_simp_tac (simpset() addsimps [rel_comp_def]) 1);
nipkow@4907
    37
qed "False_False_in_steps_atom";
nipkow@4907
    38
nipkow@5118
    39
Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
nipkow@4907
    40
by (induct_tac "w" 1);
nipkow@10996
    41
 by (asm_simp_tac (simpset() addsimps [start_atom,thm"rtrancl_empty"]) 1);
wenzelm@5132
    42
by (asm_full_simp_tac (simpset()
nipkow@12487
    43
     addsimps [False_False_in_steps_atom,rel_comp_def,start_atom]) 1);
nipkow@4907
    44
qed "start_fin_in_steps_atom";
nipkow@4907
    45
nipkow@5118
    46
Goal "accepts (atom a) w = (w = [a])";
wenzelm@5132
    47
by (simp_tac(simpset() addsimps
nipkow@4907
    48
       [accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
nipkow@4907
    49
qed "accepts_atom";
nipkow@4907
    50
nipkow@4907
    51
nipkow@4907
    52
(******************************************************)
nipkow@12792
    53
(*                      or                            *)
nipkow@4907
    54
(******************************************************)
nipkow@4907
    55
nipkow@4907
    56
(***** True/False ueber fin anheben *****)
nipkow@4907
    57
nipkow@12792
    58
Goalw [or_def] 
nipkow@12792
    59
 "!L R. fin (or L R) (True#p) = fin L p";
nipkow@4907
    60
by (Simp_tac 1);
nipkow@12792
    61
qed_spec_mp "fin_or_True";
nipkow@4907
    62
nipkow@12792
    63
Goalw [or_def] 
nipkow@12792
    64
 "!L R. fin (or L R) (False#p) = fin R p";
nipkow@4907
    65
by (Simp_tac 1);
nipkow@12792
    66
qed_spec_mp "fin_or_False";
nipkow@4907
    67
nipkow@12792
    68
AddIffs [fin_or_True,fin_or_False];
nipkow@4907
    69
nipkow@4907
    70
(***** True/False ueber step anheben *****)
nipkow@4907
    71
nipkow@12792
    72
Goalw [or_def,step_def]
nipkow@12792
    73
"!L R. (True#p,q) : step (or L R) a = (? r. q = True#r & (p,r) : step L a)";
nipkow@4907
    74
by (Simp_tac 1);
wenzelm@5132
    75
by (Blast_tac 1);
nipkow@12792
    76
qed_spec_mp "True_in_step_or";
nipkow@4907
    77
nipkow@12792
    78
Goalw [or_def,step_def]
nipkow@12792
    79
"!L R. (False#p,q) : step (or L R) a = (? r. q = False#r & (p,r) : step R a)";
nipkow@4907
    80
by (Simp_tac 1);
wenzelm@5132
    81
by (Blast_tac 1);
nipkow@12792
    82
qed_spec_mp "False_in_step_or";
nipkow@4907
    83
nipkow@12792
    84
AddIffs [True_in_step_or,False_in_step_or];
nipkow@4907
    85
nipkow@4907
    86
(***** True/False ueber epsclosure anheben *****)
nipkow@4907
    87
wenzelm@5069
    88
Goal
nipkow@12792
    89
 "(tp,tq) : (eps(or L R))^* ==> \
nipkow@4907
    90
\ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
wenzelm@5132
    91
by (etac rtrancl_induct 1);
wenzelm@5132
    92
 by (Blast_tac 1);
wenzelm@5132
    93
by (Clarify_tac 1);
wenzelm@5132
    94
by (Asm_full_simp_tac 1);
wenzelm@5132
    95
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
    96
val lemma1a = result();
nipkow@4907
    97
wenzelm@5069
    98
Goal
nipkow@12792
    99
 "(tp,tq) : (eps(or L R))^* ==> \
nipkow@4907
   100
\ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
wenzelm@5132
   101
by (etac rtrancl_induct 1);
wenzelm@5132
   102
 by (Blast_tac 1);
wenzelm@5132
   103
by (Clarify_tac 1);
wenzelm@5132
   104
by (Asm_full_simp_tac 1);
wenzelm@5132
   105
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   106
val lemma1b = result();
nipkow@4907
   107
wenzelm@5069
   108
Goal
nipkow@12792
   109
 "(p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(or L R))^*";
wenzelm@5132
   110
by (etac rtrancl_induct 1);
wenzelm@5132
   111
 by (Blast_tac 1);
wenzelm@5132
   112
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   113
val lemma2a = result();
nipkow@4907
   114
wenzelm@5069
   115
Goal
nipkow@12792
   116
 "(p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(or L R))^*";
wenzelm@5132
   117
by (etac rtrancl_induct 1);
wenzelm@5132
   118
 by (Blast_tac 1);
wenzelm@5132
   119
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   120
val lemma2b = result();
nipkow@4907
   121
wenzelm@5069
   122
Goal
nipkow@12792
   123
 "(True#p,q) : (eps(or L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
wenzelm@5132
   124
by (blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
nipkow@12792
   125
qed "True_epsclosure_or";
nipkow@4907
   126
wenzelm@5069
   127
Goal
nipkow@12792
   128
 "(False#p,q) : (eps(or L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
wenzelm@5132
   129
by (blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
nipkow@12792
   130
qed "False_epsclosure_or";
nipkow@4907
   131
nipkow@12792
   132
AddIffs [True_epsclosure_or,False_epsclosure_or];
nipkow@4907
   133
nipkow@4907
   134
(***** True/False ueber steps anheben *****)
nipkow@4907
   135
wenzelm@5069
   136
Goal
nipkow@12792
   137
 "!p. (True#p,q):steps (or L R) w = (? r. q = True # r & (p,r):steps L w)";
nipkow@4907
   138
by (induct_tac "w" 1);
oheimb@5758
   139
 by Auto_tac;
oheimb@5758
   140
by (Force_tac 1);
nipkow@12792
   141
qed_spec_mp "lift_True_over_steps_or";
nipkow@4907
   142
wenzelm@5069
   143
Goal 
nipkow@12792
   144
 "!p. (False#p,q):steps (or L R) w = (? r. q = False#r & (p,r):steps R w)";
nipkow@4907
   145
by (induct_tac "w" 1);
oheimb@5758
   146
 by Auto_tac;
oheimb@5758
   147
by (Force_tac 1);
nipkow@12792
   148
qed_spec_mp "lift_False_over_steps_or";
nipkow@4907
   149
nipkow@12792
   150
AddIffs [lift_True_over_steps_or,lift_False_over_steps_or];
nipkow@4907
   151
nipkow@4907
   152
nipkow@4907
   153
(***** Epsilonhuelle des Startzustands  *****)
nipkow@4907
   154
wenzelm@5069
   155
Goal
nipkow@5608
   156
 "R^* = Id Un (R^* O R)";
wenzelm@5132
   157
by (rtac set_ext 1);
wenzelm@5132
   158
by (split_all_tac 1);
wenzelm@5132
   159
by (rtac iffI 1);
wenzelm@5132
   160
 by (etac rtrancl_induct 1);
wenzelm@5132
   161
  by (Blast_tac 1);
wenzelm@5132
   162
 by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@12566
   163
by (blast_tac (claset() addIs [converse_rtrancl_into_rtrancl]) 1);
nipkow@4907
   164
qed "unfold_rtrancl2";
nipkow@4907
   165
wenzelm@5069
   166
Goal
nipkow@4907
   167
 "(p,q) : R^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))";
wenzelm@5132
   168
by (rtac (unfold_rtrancl2 RS equalityE) 1);
wenzelm@5132
   169
by (Blast_tac 1);
nipkow@4907
   170
qed "in_unfold_rtrancl2";
nipkow@4907
   171
nipkow@12792
   172
val epsclosure_start_step_or =
nipkow@12792
   173
  read_instantiate [("p","start(or L R)")] in_unfold_rtrancl2;
nipkow@12792
   174
AddIffs [epsclosure_start_step_or];
nipkow@4907
   175
nipkow@12792
   176
Goalw [or_def,step_def]
nipkow@12792
   177
 "!L R. (start(or L R),q) : eps(or L R) = \
nipkow@4907
   178
\       (q = True#start L | q = False#start R)";
wenzelm@5132
   179
by (Simp_tac 1);
nipkow@12792
   180
qed_spec_mp "start_eps_or";
nipkow@12792
   181
AddIffs [start_eps_or];
nipkow@4907
   182
nipkow@12792
   183
Goalw [or_def,step_def]
nipkow@12792
   184
 "!L R. (start(or L R),q) ~: step (or L R) (Some a)";
wenzelm@5132
   185
by (Simp_tac 1);
nipkow@12792
   186
qed_spec_mp "not_start_step_or_Some";
nipkow@12792
   187
AddIffs [not_start_step_or_Some];
nipkow@4907
   188
wenzelm@5069
   189
Goal
nipkow@12792
   190
 "(start(or L R), q) : steps (or L R) w = \
nipkow@12792
   191
\ ( (w = [] & q = start(or L R)) | \
nipkow@4907
   192
\   (? p.  q = True  # p & (start L,p) : steps L w | \
nipkow@4907
   193
\          q = False # p & (start R,p) : steps R w) )";
wenzelm@8442
   194
by (case_tac "w" 1);
nipkow@4907
   195
 by (Asm_simp_tac 1);
paulson@5457
   196
 by (Blast_tac 1);
nipkow@4907
   197
by (Asm_simp_tac 1);
paulson@5457
   198
by (Blast_tac 1);
nipkow@12792
   199
qed "steps_or";
nipkow@4907
   200
nipkow@12792
   201
Goalw [or_def]
nipkow@12792
   202
 "!L R. ~ fin (or L R) (start(or L R))";
wenzelm@5132
   203
by (Simp_tac 1);
nipkow@12792
   204
qed_spec_mp "start_or_not_final";
nipkow@12792
   205
AddIffs [start_or_not_final];
nipkow@4907
   206
wenzelm@5069
   207
Goalw [accepts_def]
nipkow@12792
   208
 "accepts (or L R) w = (accepts L w | accepts R w)";
nipkow@12792
   209
by (simp_tac (simpset() addsimps [steps_or]) 1);
wenzelm@5132
   210
by Auto_tac;
nipkow@12792
   211
qed "accepts_or";
nipkow@4907
   212
nipkow@4907
   213
nipkow@4907
   214
(******************************************************)
nipkow@12792
   215
(*                      conc                          *)
nipkow@4907
   216
(******************************************************)
nipkow@4907
   217
nipkow@4907
   218
(** True/False in fin **)
nipkow@4907
   219
wenzelm@5069
   220
Goalw [conc_def]
nipkow@4907
   221
 "!L R. fin (conc L R) (True#p) = False";
nipkow@4907
   222
by (Simp_tac 1);
nipkow@4907
   223
qed_spec_mp "fin_conc_True";
nipkow@4907
   224
wenzelm@5069
   225
Goalw [conc_def] 
nipkow@4907
   226
 "!L R. fin (conc L R) (False#p) = fin R p";
nipkow@4907
   227
by (Simp_tac 1);
nipkow@4907
   228
qed "fin_conc_False";
nipkow@4907
   229
nipkow@4907
   230
AddIffs [fin_conc_True,fin_conc_False];
nipkow@4907
   231
nipkow@4907
   232
(** True/False in step **)
nipkow@4907
   233
wenzelm@5069
   234
Goalw [conc_def,step_def]
nipkow@4907
   235
 "!L R. (True#p,q) : step (conc L R) a = \
nipkow@4907
   236
\       ((? r. q=True#r & (p,r): step L a) | \
nipkow@4907
   237
\        (fin L p & a=None & q=False#start R))";
nipkow@4907
   238
by (Simp_tac 1);
wenzelm@5132
   239
by (Blast_tac 1);
nipkow@4907
   240
qed_spec_mp "True_step_conc";
nipkow@4907
   241
wenzelm@5069
   242
Goalw [conc_def,step_def]
nipkow@4907
   243
 "!L R. (False#p,q) : step (conc L R) a = \
nipkow@4907
   244
\       (? r. q = False#r & (p,r) : step R a)";
nipkow@4907
   245
by (Simp_tac 1);
wenzelm@5132
   246
by (Blast_tac 1);
nipkow@4907
   247
qed_spec_mp "False_step_conc";
nipkow@4907
   248
nipkow@4907
   249
AddIffs [True_step_conc, False_step_conc];
nipkow@4907
   250
nipkow@4907
   251
(** False in epsclosure **)
nipkow@4907
   252
wenzelm@5069
   253
Goal
nipkow@5118
   254
 "(tp,tq) : (eps(conc L R))^* ==> \
nipkow@4907
   255
\ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
wenzelm@5132
   256
by (etac rtrancl_induct 1);
wenzelm@5132
   257
 by (Blast_tac 1);
wenzelm@5132
   258
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   259
qed "lemma1b";
nipkow@4907
   260
wenzelm@5069
   261
Goal
nipkow@5118
   262
 "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
wenzelm@5132
   263
by (etac rtrancl_induct 1);
wenzelm@5132
   264
 by (Blast_tac 1);
wenzelm@5132
   265
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   266
val lemma2b = result();
nipkow@4907
   267
wenzelm@5069
   268
Goal
nipkow@4907
   269
 "((False # p, q) : (eps (conc L R))^*) = \
nipkow@4907
   270
\ (? r. q = False # r & (p, r) : (eps R)^*)";
nipkow@4907
   271
by (rtac iffI 1);
wenzelm@5132
   272
 by (blast_tac (claset() addDs [lemma1b]) 1);
wenzelm@5132
   273
by (blast_tac (claset() addDs [lemma2b]) 1);
nipkow@4907
   274
qed "False_epsclosure_conc";
nipkow@4907
   275
AddIffs [False_epsclosure_conc];
nipkow@4907
   276
nipkow@4907
   277
(** False in steps **)
nipkow@4907
   278
wenzelm@5069
   279
Goal
nipkow@4907
   280
 "!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
nipkow@4907
   281
by (induct_tac "w" 1);
nipkow@4907
   282
 by (Simp_tac 1);
nipkow@4907
   283
by (Simp_tac 1);
paulson@5457
   284
by (Fast_tac 1);  (*MUCH faster than Blast_tac*)
nipkow@4907
   285
qed_spec_mp "False_steps_conc";
nipkow@4907
   286
AddIffs [False_steps_conc];
nipkow@4907
   287
nipkow@4907
   288
(** True in epsclosure **)
nipkow@4907
   289
wenzelm@5069
   290
Goal
nipkow@5118
   291
 "(p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*";
wenzelm@5132
   292
by (etac rtrancl_induct 1);
wenzelm@5132
   293
 by (Blast_tac 1);
wenzelm@5132
   294
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   295
qed "True_True_eps_concI";
nipkow@4907
   296
wenzelm@5069
   297
Goal
nipkow@5118
   298
 "!p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
wenzelm@5132
   299
by (induct_tac "w" 1);
nipkow@4907
   300
 by (simp_tac (simpset() addsimps [True_True_eps_concI]) 1);
nipkow@4907
   301
by (Simp_tac 1);
wenzelm@5132
   302
by (blast_tac (claset() addIs [True_True_eps_concI]) 1);
nipkow@4907
   303
qed_spec_mp "True_True_steps_concI";
nipkow@4907
   304
wenzelm@5069
   305
Goal
nipkow@5118
   306
 "(tp,tq) : (eps(conc L R))^* ==> \
nipkow@4907
   307
\ !p. tp = True#p --> \
nipkow@4907
   308
\ (? q. tq = True#q & (p,q) : (eps L)^*) | \
nipkow@4907
   309
\ (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*)";
wenzelm@5132
   310
by (etac rtrancl_induct 1);
wenzelm@5132
   311
 by (Blast_tac 1);
wenzelm@5132
   312
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   313
val lemma1a = result();
nipkow@4907
   314
wenzelm@5069
   315
Goal
nipkow@5118
   316
 "(p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*";
wenzelm@5132
   317
by (etac rtrancl_induct 1);
wenzelm@5132
   318
 by (Blast_tac 1);
wenzelm@5132
   319
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   320
val lemma2a = result();
nipkow@4907
   321
wenzelm@5069
   322
Goalw [conc_def,step_def]
nipkow@4907
   323
 "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None";
wenzelm@5132
   324
by (split_all_tac 1);
nipkow@4907
   325
by (Asm_full_simp_tac 1);
nipkow@4907
   326
val lemma = result();
nipkow@4907
   327
wenzelm@5069
   328
Goal
nipkow@5118
   329
 "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
wenzelm@5132
   330
by (etac rtrancl_induct 1);
wenzelm@5132
   331
 by (Blast_tac 1);
nipkow@4907
   332
by (dtac lemma 1);
wenzelm@5132
   333
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   334
val lemma2b = result();
nipkow@4907
   335
wenzelm@5069
   336
Goalw [conc_def,step_def]
nipkow@4907
   337
 "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)";
wenzelm@5132
   338
by (split_all_tac 1);
wenzelm@5132
   339
by (Asm_full_simp_tac 1);
nipkow@4907
   340
qed "True_False_eps_concI";
nipkow@4907
   341
wenzelm@5069
   342
Goal
nipkow@4907
   343
 "((True#p,q) : (eps(conc L R))^*) = \
nipkow@4907
   344
\ ((? r. (p,r) : (eps L)^* & q = True#r) | \
nipkow@4907
   345
\  (? r. (p,r) : (eps L)^* & fin L r & \
nipkow@4907
   346
\        (? s. (start R, s) : (eps R)^* & q = False#s)))";
wenzelm@5132
   347
by (rtac iffI 1);
wenzelm@5132
   348
 by (blast_tac (claset() addDs [lemma1a]) 1);
wenzelm@5132
   349
by (etac disjE 1);
wenzelm@5132
   350
 by (blast_tac (claset() addIs [lemma2a]) 1);
wenzelm@5132
   351
by (Clarify_tac 1);
wenzelm@5132
   352
by (rtac (rtrancl_trans) 1);
wenzelm@5132
   353
by (etac lemma2a 1);
nipkow@12566
   354
by (rtac converse_rtrancl_into_rtrancl 1);
wenzelm@5132
   355
by (etac True_False_eps_concI 1);
wenzelm@5132
   356
by (etac lemma2b 1);
nipkow@4907
   357
qed "True_epsclosure_conc";
nipkow@4907
   358
AddIffs [True_epsclosure_conc];
nipkow@4907
   359
nipkow@4907
   360
(** True in steps **)
nipkow@4907
   361
wenzelm@5069
   362
Goal
nipkow@4907
   363
 "!p. (True#p,q) : steps (conc L R) w --> \
nipkow@4907
   364
\     ((? r. (p,r) : steps L w & q = True#r)  | \
nipkow@4907
   365
\      (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
nipkow@4907
   366
\              (? s. (start R,s) : steps R v & q = False#s))))";
wenzelm@5132
   367
by (induct_tac "w" 1);
wenzelm@5132
   368
 by (Simp_tac 1);
wenzelm@5132
   369
by (Simp_tac 1);
wenzelm@5132
   370
by (clarify_tac (claset() delrules [disjCI]) 1);
wenzelm@5132
   371
 by (etac disjE 1);
wenzelm@5132
   372
 by (clarify_tac (claset() delrules [disjCI]) 1);
wenzelm@5132
   373
 by (etac disjE 1);
wenzelm@5132
   374
  by (clarify_tac (claset() delrules [disjCI]) 1);
wenzelm@5132
   375
  by (etac allE 1 THEN mp_tac 1);
wenzelm@5132
   376
  by (etac disjE 1);
nipkow@4907
   377
   by (Blast_tac 1);
wenzelm@5132
   378
  by (rtac disjI2 1);
nipkow@4907
   379
  by (Clarify_tac 1);
wenzelm@5132
   380
  by (Simp_tac 1);
wenzelm@5132
   381
  by (res_inst_tac[("x","a#u")] exI 1);
wenzelm@5132
   382
  by (Simp_tac 1);
nipkow@4907
   383
  by (Blast_tac 1);
nipkow@4907
   384
 by (Blast_tac 1);
wenzelm@5132
   385
by (rtac disjI2 1);
nipkow@4907
   386
by (Clarify_tac 1);
wenzelm@5132
   387
by (Simp_tac 1);
wenzelm@5132
   388
by (res_inst_tac[("x","[]")] exI 1);
wenzelm@5132
   389
by (Simp_tac 1);
nipkow@4907
   390
by (Blast_tac 1);
nipkow@4907
   391
qed_spec_mp "True_steps_concD";
nipkow@4907
   392
wenzelm@5069
   393
Goal
nipkow@4907
   394
 "(True#p,q) : steps (conc L R) w = \
nipkow@4907
   395
\ ((? r. (p,r) : steps L w & q = True#r)  | \
nipkow@4907
   396
\  (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
nipkow@4907
   397
\          (? s. (start R,s) : steps R v & q = False#s))))";
wenzelm@5132
   398
by (blast_tac (claset() addDs [True_steps_concD]
nipkow@11232
   399
     addIs [True_True_steps_concI,in_steps_epsclosure]) 1);
nipkow@4907
   400
qed "True_steps_conc";
nipkow@4907
   401
nipkow@4907
   402
(** starting from the start **)
nipkow@4907
   403
wenzelm@5069
   404
Goalw [conc_def]
nipkow@4907
   405
  "!L R. start(conc L R) = True#start L";
wenzelm@5132
   406
by (Simp_tac 1);
nipkow@4907
   407
qed_spec_mp "start_conc";
nipkow@4907
   408
wenzelm@5069
   409
Goalw [conc_def]
nipkow@4907
   410
 "!L R. fin(conc L R) p = (? s. p = False#s & fin R s)";
berghofe@5184
   411
by (simp_tac (simpset() addsplits [list.split]) 1);
nipkow@4907
   412
qed_spec_mp "final_conc";
nipkow@4907
   413
wenzelm@5069
   414
Goal
nipkow@4907
   415
 "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
nipkow@4907
   416
by (simp_tac (simpset() addsimps
nipkow@4907
   417
     [accepts_def,True_steps_conc,final_conc,start_conc]) 1);
wenzelm@5132
   418
by (Blast_tac 1);
nipkow@4907
   419
qed "accepts_conc";
nipkow@4907
   420
nipkow@4907
   421
(******************************************************)
nipkow@4907
   422
(*                       star                         *)
nipkow@4907
   423
(******************************************************)
nipkow@4907
   424
wenzelm@5069
   425
Goalw [star_def,step_def]
nipkow@4907
   426
 "!A. (True#p,q) : eps(star A) = \
nipkow@4907
   427
\     ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )";
wenzelm@5132
   428
by (Simp_tac 1);
wenzelm@5132
   429
by (Blast_tac 1);
nipkow@4907
   430
qed_spec_mp "True_in_eps_star";
nipkow@4907
   431
AddIffs [True_in_eps_star];
nipkow@4907
   432
wenzelm@5069
   433
Goalw [star_def,step_def]
nipkow@4907
   434
  "!A. (p,q) : step A a --> (True#p, True#q) : step (star A) a";
wenzelm@5132
   435
by (Simp_tac 1);
nipkow@4907
   436
qed_spec_mp "True_True_step_starI";
nipkow@4907
   437
wenzelm@5069
   438
Goal
nipkow@5118
   439
  "(p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
wenzelm@5132
   440
by (etac rtrancl_induct 1);
wenzelm@5132
   441
 by (Blast_tac 1);
wenzelm@5132
   442
by (blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
nipkow@4907
   443
qed_spec_mp "True_True_eps_starI";
nipkow@4907
   444
wenzelm@5069
   445
Goalw [star_def,step_def]
nipkow@4907
   446
 "!A. fin A p --> (True#p,True#start A) : eps(star A)";
wenzelm@5132
   447
by (Simp_tac 1);
nipkow@4907
   448
qed_spec_mp "True_start_eps_starI";
nipkow@4907
   449
wenzelm@5069
   450
Goal
nipkow@5118
   451
 "(tp,s) : (eps(star A))^* ==> (! p. tp = True#p --> \
nipkow@4907
   452
\ (? r. ((p,r) : (eps A)^* | \
nipkow@4907
   453
\        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
nipkow@4907
   454
\       s = True#r))";
wenzelm@5132
   455
by (etac rtrancl_induct 1);
wenzelm@5132
   456
 by (Simp_tac 1);
nipkow@4907
   457
by (Clarify_tac 1);
nipkow@4907
   458
by (Asm_full_simp_tac 1);
wenzelm@5132
   459
by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
nipkow@4907
   460
val lemma = result();
nipkow@4907
   461
wenzelm@5069
   462
Goal
nipkow@4907
   463
 "((True#p,s) : (eps(star A))^*) = \
nipkow@4907
   464
\ (? r. ((p,r) : (eps A)^* | \
nipkow@4907
   465
\        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
nipkow@4907
   466
\       s = True#r)";
wenzelm@5132
   467
by (rtac iffI 1);
wenzelm@5132
   468
 by (dtac lemma 1);
wenzelm@5132
   469
 by (Blast_tac 1);
nipkow@4907
   470
(* Why can't blast_tac do the rest? *)
nipkow@4907
   471
by (Clarify_tac 1);
wenzelm@5132
   472
by (etac disjE 1);
wenzelm@5132
   473
by (etac True_True_eps_starI 1);
nipkow@4907
   474
by (Clarify_tac 1);
wenzelm@5132
   475
by (rtac rtrancl_trans 1);
wenzelm@5132
   476
by (etac True_True_eps_starI 1);
wenzelm@5132
   477
by (rtac rtrancl_trans 1);
wenzelm@5132
   478
by (rtac r_into_rtrancl 1);
wenzelm@5132
   479
by (etac True_start_eps_starI 1);
wenzelm@5132
   480
by (etac True_True_eps_starI 1);
nipkow@4907
   481
qed "True_eps_star";
nipkow@4907
   482
AddIffs [True_eps_star];
nipkow@4907
   483
nipkow@4907
   484
(** True in step Some **)
nipkow@4907
   485
wenzelm@5069
   486
Goalw [star_def,step_def]
nipkow@4907
   487
 "!A. (True#p,r): step (star A) (Some a) = \
nipkow@4907
   488
\     (? q. (p,q): step A (Some a) & r=True#q)";
wenzelm@5132
   489
by (Simp_tac 1);
wenzelm@5132
   490
by (Blast_tac 1);
nipkow@4907
   491
qed_spec_mp "True_step_star";
nipkow@4907
   492
AddIffs [True_step_star];
nipkow@4907
   493
nipkow@4907
   494
nipkow@4907
   495
(** True in steps **)
nipkow@4907
   496
nipkow@4907
   497
(* reverse list induction! Complicates matters for conc? *)
wenzelm@5069
   498
Goal
nipkow@4907
   499
 "!rr. (True#start A,rr) : steps (star A) w --> \
nipkow@4907
   500
\ (? us v. w = concat us @ v & \
nipkow@4907
   501
\             (!u:set us. accepts A u) & \
nipkow@4907
   502
\             (? r. (start A,r) : steps A v & rr = True#r))";
nipkow@9747
   503
by (rev_induct_tac "w" 1);
nipkow@4907
   504
 by (Asm_full_simp_tac 1);
nipkow@4907
   505
 by (Clarify_tac 1);
wenzelm@5132
   506
 by (res_inst_tac [("x","[]")] exI 1);
wenzelm@5132
   507
 by (etac disjE 1);
nipkow@4907
   508
  by (Asm_simp_tac 1);
nipkow@4907
   509
 by (Clarify_tac 1);
nipkow@4907
   510
 by (Asm_simp_tac 1);
wenzelm@5132
   511
by (simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
nipkow@4907
   512
by (Clarify_tac 1);
wenzelm@5132
   513
by (etac allE 1 THEN mp_tac 1);
nipkow@4907
   514
by (Clarify_tac 1);
wenzelm@5132
   515
by (etac disjE 1);
wenzelm@5132
   516
 by (res_inst_tac [("x","us")] exI 1);
wenzelm@5132
   517
 by (res_inst_tac [("x","v@[x]")] exI 1);
wenzelm@5132
   518
 by (asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
wenzelm@5132
   519
 by (Blast_tac 1);
nipkow@4907
   520
by (Clarify_tac 1);
wenzelm@5132
   521
by (res_inst_tac [("x","us@[v@[x]]")] exI 1);
wenzelm@5132
   522
by (res_inst_tac [("x","[]")] exI 1);
wenzelm@5132
   523
by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
wenzelm@5132
   524
by (Blast_tac 1);
nipkow@4907
   525
qed_spec_mp "True_start_steps_starD";
nipkow@4907
   526
wenzelm@5069
   527
Goal "!p. (p,q) : steps A w --> (True#p,True#q) : steps (star A) w";
wenzelm@5132
   528
by (induct_tac "w" 1);
wenzelm@5132
   529
 by (Simp_tac 1);
wenzelm@5132
   530
by (Simp_tac 1);
wenzelm@5132
   531
by (blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
nipkow@4907
   532
qed_spec_mp "True_True_steps_starI";
nipkow@4907
   533
wenzelm@5069
   534
Goalw [accepts_def]
nipkow@4907
   535
 "(!u : set us. accepts A u) --> \
nipkow@4907
   536
\ (True#start A,True#start A) : steps (star A) (concat us)";
wenzelm@5132
   537
by (induct_tac "us" 1);
wenzelm@5132
   538
 by (Simp_tac 1);
wenzelm@5132
   539
by (Simp_tac 1);
nipkow@11232
   540
by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,in_epsclosure_steps]) 1);
nipkow@4907
   541
qed_spec_mp "steps_star_cycle";
nipkow@4907
   542
nipkow@4907
   543
(* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
wenzelm@5069
   544
Goal
nipkow@4907
   545
 "(True#start A,rr) : steps (star A) w = \
nipkow@4907
   546
\ (? us v. w = concat us @ v & \
nipkow@4907
   547
\             (!u:set us. accepts A u) & \
nipkow@4907
   548
\             (? r. (start A,r) : steps A v & rr = True#r))";
wenzelm@5132
   549
by (rtac iffI 1);
wenzelm@5132
   550
 by (etac True_start_steps_starD 1);
nipkow@4907
   551
by (Clarify_tac 1);
wenzelm@5132
   552
by (Asm_simp_tac 1);
wenzelm@5132
   553
by (blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
nipkow@4907
   554
qed "True_start_steps_star";
nipkow@4907
   555
nipkow@4907
   556
(** the start state **)
nipkow@4907
   557
wenzelm@5069
   558
Goalw [star_def,step_def]
nipkow@4907
   559
  "!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)";
wenzelm@5132
   560
by (Simp_tac 1);
nipkow@4907
   561
qed_spec_mp "start_step_star";
nipkow@4907
   562
AddIffs [start_step_star];
nipkow@4907
   563
nipkow@4907
   564
val epsclosure_start_step_star =
nipkow@4907
   565
  read_instantiate [("p","start(star A)")] in_unfold_rtrancl2;
nipkow@4907
   566
wenzelm@5069
   567
Goal
nipkow@4907
   568
 "(start(star A),r) : steps (star A) w = \
nipkow@4907
   569
\ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
wenzelm@5132
   570
by (rtac iffI 1);
wenzelm@8442
   571
 by (case_tac "w" 1);
wenzelm@5132
   572
  by (asm_full_simp_tac (simpset() addsimps
nipkow@4907
   573
    [epsclosure_start_step_star]) 1);
wenzelm@5132
   574
 by (Asm_full_simp_tac 1);
nipkow@4907
   575
 by (Clarify_tac 1);
wenzelm@5132
   576
 by (asm_full_simp_tac (simpset() addsimps
nipkow@4907
   577
    [epsclosure_start_step_star]) 1);
wenzelm@5132
   578
 by (Blast_tac 1);
wenzelm@5132
   579
by (etac disjE 1);
wenzelm@5132
   580
 by (Asm_simp_tac 1);
nipkow@11232
   581
by (blast_tac (claset() addIs [in_steps_epsclosure]) 1);
nipkow@4907
   582
qed "start_steps_star";
nipkow@4907
   583
wenzelm@5069
   584
Goalw [star_def] "!A. fin (star A) (True#p) = fin A p";
wenzelm@5132
   585
by (Simp_tac 1);
nipkow@4907
   586
qed_spec_mp "fin_star_True";
nipkow@4907
   587
AddIffs [fin_star_True];
nipkow@4907
   588
wenzelm@5069
   589
Goalw [star_def] "!A. fin (star A) (start(star A))";
wenzelm@5132
   590
by (Simp_tac 1);
nipkow@4907
   591
qed_spec_mp "fin_star_start";
nipkow@4907
   592
AddIffs [fin_star_start];
nipkow@4907
   593
nipkow@4907
   594
(* too complex! Simpler if loop back to start(star A)? *)
wenzelm@5069
   595
Goalw [accepts_def]
nipkow@4907
   596
 "accepts (star A) w = \
nipkow@4907
   597
\ (? us. (!u : set(us). accepts A u) & (w = concat us) )";
wenzelm@5132
   598
by (simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
wenzelm@5132
   599
by (rtac iffI 1);
nipkow@4907
   600
 by (Clarify_tac 1);
wenzelm@5132
   601
 by (etac disjE 1);
nipkow@4907
   602
  by (Clarify_tac 1);
wenzelm@5132
   603
  by (Simp_tac 1);
wenzelm@5132
   604
  by (res_inst_tac [("x","[]")] exI 1);
wenzelm@5132
   605
  by (Simp_tac 1);
nipkow@4907
   606
 by (Clarify_tac 1);
wenzelm@5132
   607
 by (res_inst_tac [("x","us@[v]")] exI 1);
wenzelm@5132
   608
 by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
wenzelm@5132
   609
 by (Blast_tac 1);
nipkow@4907
   610
by (Clarify_tac 1);
wenzelm@5132
   611
by (res_inst_tac [("xs","us")] rev_exhaust 1);
wenzelm@5132
   612
 by (Asm_simp_tac 1);
wenzelm@5132
   613
 by (Blast_tac 1);
nipkow@4907
   614
by (Clarify_tac 1);
wenzelm@5132
   615
by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
wenzelm@5132
   616
by (Blast_tac 1);
nipkow@4907
   617
qed "accepts_star";
nipkow@4907
   618
nipkow@4907
   619
nipkow@4907
   620
(***** Correctness of r2n *****)
nipkow@4907
   621
wenzelm@5069
   622
Goal
nipkow@4907
   623
 "!w. accepts (rexp2nae r) w = (w : lang r)";
wenzelm@5132
   624
by (induct_tac "r" 1);
wenzelm@5132
   625
    by (simp_tac (simpset() addsimps [accepts_def]) 1);
wenzelm@5132
   626
   by (simp_tac(simpset() addsimps [accepts_atom]) 1);
nipkow@12792
   627
  by (asm_simp_tac (simpset() addsimps [accepts_or]) 1);
wenzelm@5132
   628
 by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
wenzelm@5132
   629
by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
nipkow@4907
   630
qed "accepts_rexp2nae";