1 (*  Author:     Tobias Nipkow

     2     Copyright   1998 TUM

     3 *)

     4 

     5 header "Regular expressions"

     6 

     7 theory Regular_Exp

     8 imports Regular_Set

     9 begin

    10 

    11 datatype 'a rexp =

    12   Zero |

    13   One |

    14   Atom 'a |

    15   Plus "('a rexp)" "('a rexp)" |

    16   Times "('a rexp)" "('a rexp)" |

    17   Star "('a rexp)"

    18 

    19 primrec lang :: "'a rexp => 'a list set" where

    20 "lang Zero = {}" |

    21 "lang One = {[]}" |

    22 "lang (Atom a) = {[a]}" |

    23 "lang (Plus r s) = (lang r) Un (lang s)" |

    24 "lang (Times r s) = conc (lang r) (lang s)" |

    25 "lang (Star r) = star(lang r)"

    26 

    27 primrec atoms :: "'a rexp \<Rightarrow> 'a set"

    28 where

    29 "atoms Zero = {}" |

    30 "atoms One = {}" |

    31 "atoms (Atom a) = {a}" |

    32 "atoms (Plus r s) = atoms r \<union> atoms s" |

    33 "atoms (Times r s) = atoms r \<union> atoms s" |

    34 "atoms (Star r) = atoms r"

    35 

    36 end