theory Reg_demo
imports Main
begin
(*
The aim of this demo is to:
(1) define a datatype representing regular expressions
(2) define the language expressed by a regular expression
(3) define the reverse of a regular expression
(4) prove that the language of the reverse of an
expression e is equal to the reverse of the language of e.
*)
(*-----------------------------------------------------*)
(* Defining the datatype of regular expressions *)
(*
Define a datatype representing regular expressions,
for instance the regular expression \ ( (a.b|c)* )
Then define a few regular expressions, like the one above
Remember the syntax:
datatype ’a list = Nil | Cons 'a "'a list"
Note: you can define notation for your constructors;
for example Trans 'a 'b (infixr "[\]" 60)
means that (Trans a b) can be noted (a [\] b)
where the operator is infix, associates to the
right, and is of priority 60.
*)
(* TODO *)
(*-----------------------------------------------------*)
(* Defining the language of a regular expression *)
type_synonym word = "char list"
(*
Define a recursive function computing the language of a
given regular expression:
lang:: "regexp \ word set"
Try it on small examples.
Hint: You might need to define an inductive set.
Recall the notation:
inductive_set Fin :: "'a set set"
where
emptyI: "{} \ Fin" |
insertI: "A \ Fin \ insert a A \ Fin"
*)
(* TODO *)
(*-----------------------------------------------------*)
(* Defining the reverse of a regular expression *)
(* TODO *)
(*-----------------------------------------------------*)
(* Proof that the language of the reverse of an
expression e is equal to the reverse of the language of e
"lang (rev_regexp e) = rev ` (lang e)"
*)
(* TODO *)
end