Commit 9c89bc6a authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

theory of regular expressions

parent 0ff0abb1
(** {1 Theory of regular expressions} *)
theory Regexp
type char
(** Syntax *)
type regexp =
| Empty
| Epsilon
| Char char
| Alt regexp regexp
| Concat regexp regexp
| Star regexp
(** Semantics *)
(** Words are list of characters. *)
use export list.List
use export list.Append
type word = list char
(** Inductive predicate [mem w r] means
``word [w] belongs to the language of [r]''. *)
inductive mem (w: word) (r: regexp) =
| mem_eps:
mem Nil Epsilon
| mem_char:
forall c: char. mem (Cons c Nil) (Char c)
| mem_altl:
forall w: word, r1 r2: regexp. mem w r1 -> mem w (Alt r1 r2)
| mem_altr:
forall w: word, r1 r2: regexp. mem w r2 -> mem w (Alt r1 r2)
| mem_concat:
forall w1 w2: word, r1 r2: regexp.
mem w1 r1 -> mem w2 r2 -> mem (w1 ++ w2) (Concat r1 r2)
| mems1:
forall r: regexp. mem Nil (Star r)
| mems2:
forall w1 w2: word, r: regexp.
mem w1 r -> mem w2 (Star r) -> mem (w1 ++ w2) (Star r)
theory Test
clone import Regexp with type char = int
lemma empty_is_empty: forall w: word. not (mem w Empty)
constant a: int = 0
constant b: int = 1
constant c: int = 2
goal G: mem (Cons a (Cons b Nil)) (Concat (Char a) (Star (Char b)))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment