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