src/HOL/Lex/RegExp.thy
author nipkow
Thu Jan 17 19:32:22 2002 +0100 (2002-01-17)
changeset 12792 b344226f924c
parent 11379 0c90ffd3f3e2
permissions -rw-r--r--
Added code generation to Scanner.thy
Renamed Union -> Or, union -> or
nipkow@4832
     1
(*  Title:      HOL/Lex/RegExp.thy
nipkow@4832
     2
    ID:         $Id$
nipkow@4832
     3
    Author:     Tobias Nipkow
nipkow@4832
     4
    Copyright   1998 TUM
nipkow@4832
     5
nipkow@4832
     6
Regular expressions
nipkow@4832
     7
*)
nipkow@4832
     8
nipkow@4832
     9
RegExp = RegSet +
nipkow@4832
    10
nipkow@4832
    11
datatype 'a rexp = Empty
nipkow@4832
    12
                 | Atom 'a
nipkow@12792
    13
                 | Or   ('a rexp) ('a rexp)
nipkow@4832
    14
                 | Conc ('a rexp) ('a rexp)
nipkow@4832
    15
                 | Star ('a rexp)
nipkow@4832
    16
nipkow@4832
    17
consts lang :: 'a rexp => 'a list set
berghofe@5184
    18
primrec
nipkow@11379
    19
"lang Empty = {}"
nipkow@11379
    20
"lang (Atom a) = {[a]}"
nipkow@12792
    21
"lang (Or el er) = (lang el) Un (lang er)"
nipkow@11379
    22
"lang (Conc el er) = RegSet.conc (lang el) (lang er)"
nipkow@11379
    23
"lang (Star e) = RegSet.star(lang e)"
nipkow@4832
    24
nipkow@4832
    25
end