|
4907
|
1 |
(* Title: HOL/Lex/Scanner.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1998 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
12792
|
7 |
theory Scanner = Automata + RegExp2NA + RegExp2NAe:
|
|
|
8 |
|
|
|
9 |
theorem "DA.accepts (na2da(rexp2na r)) w = (w : lang r)"
|
|
|
10 |
by (simp add: NA_DA_equiv[THEN sym] accepts_rexp2na)
|
|
|
11 |
|
|
|
12 |
theorem "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)"
|
|
|
13 |
by (simp add: NAe_DA_equiv accepts_rexp2nae)
|
|
|
14 |
|
|
|
15 |
(* Testing code generation: *)
|
|
|
16 |
|
|
|
17 |
types_code
|
|
|
18 |
set ("_ list")
|
|
|
19 |
|
|
|
20 |
consts_code
|
|
|
21 |
"{}" ("[]")
|
|
|
22 |
"insert" ("(_ ins _)")
|
|
|
23 |
"op :" ("(_ mem _)")
|
|
|
24 |
"op Un" ("(_ union _)")
|
|
|
25 |
"image" ("map")
|
|
|
26 |
"UNION" ("(fn A => fn f => flat(map f A))")
|
|
|
27 |
"Bex" ("(fn A => fn f => exists f A)")
|
|
|
28 |
|
|
|
29 |
generate_code
|
|
|
30 |
test = "let r0 = Atom(0::nat);
|
|
|
31 |
r1 = Atom(1::nat);
|
|
|
32 |
re = Conc (Star(Or(Conc r1 r1)r0))
|
|
|
33 |
(Star(Or(Conc r0 r0)r1));
|
|
|
34 |
N = rexp2na re;
|
|
|
35 |
D = na2da N
|
|
|
36 |
in (NA.accepts N [0,1,1,0,0,1], DA.accepts D [0,1,1,0,0,1])"
|
|
|
37 |
ML test
|
|
|
38 |
|
|
|
39 |
end
|