[f3dc84]: thys / Functional-Automata / RegExp2NAe.thy  Maximize  Restore  History

Download this file

621 lines (517 with data), 16.9 kB

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

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks