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