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 \<not> ( (a.b|c)* )

Then define a few regular expressions, like the one a

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 "[\<longrightarrow>]" 60)
      means that (Trans a b) can be noted (a [\<longrightarrow>] 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 \<Rightarrow> 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:  "{} \<in> Fin" |
         insertI: "A \<in> Fin \<Longrightarrow> insert a A \<in> 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