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