theory Reg_demo_sol
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.
*)

datatype regexp =
  Atom char ("<_>")
 |Alt regexp regexp (infixl "\<bar>" 50)
 |Conc regexp regexp (infixl "\<cdot>"  60)
 |Star regexp ("_ \<star>" [79] 80)
 |Neg regexp ("!_" [70] 70)

term "!(<CHR ''a''>\<cdot><CHR ''b''>)"
term "(!(<CHR ''a''>))\<cdot><CHR ''b''>"
term "!((<CHR ''a''>\<cdot><CHR ''b''>\<bar><CHR ''c''>)\<star>)"

definition mye0::regexp
where
  "mye0=Alt (Atom CHR ''a'') (Conc (Atom CHR ''b'')(Atom CHR ''c''))"
  
thm mye0_def

definition mye1::regexp
where
  "mye1=Conc (Atom CHR ''a'') (Alt (Atom CHR ''b'')(Atom CHR ''c''))"

thm mye1_def
  

  
(*-----------------------------------------------------*)
(* 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"
*)

inductive_set star for L
where 
  star_empty[simp,intro!]: "[] \<in> star L"
 |star_app: "\<lbrakk>u\<in>L; v\<in>star L\<rbrakk> \<Longrightarrow> u@v \<in> star L"
 
print_theorems
 

definition conc :: "word set \<Rightarrow> word set \<Rightarrow> word set"
  where
  "conc  l1 l2 \<equiv>{ w1@w2  |w1 w2. w1 \<in>  l1 \<and> w2 \<in>  l2}"
  
primrec 
  lang :: "regexp \<Rightarrow> word set"
where
  "lang (Atom c) = {[c]}"
 |"lang (Alt e1 e2) = lang e1 \<union> lang e2"
 |"lang (Conc e1 e2) = conc (lang e1) (lang e2)"
 |"lang (Star e) = star (lang e)"
 |"lang (Neg e) = - (lang e)"
 

value "lang mye0" 
 
value "lang mye1" 
 
 
(*-----------------------------------------------------*)
(* Defining the reverse of a regular expression *)

primrec rev_regexp :: "regexp \<Rightarrow> regexp"
where 
  "rev_regexp (Atom c) = Atom c"
 |"rev_regexp (Alt e1 e2) = Alt (rev_regexp e1) (rev_regexp e2)"
 |"rev_regexp (Conc e1 e2) = Conc (rev_regexp e2) (rev_regexp e1)"
 |"rev_regexp (Star e) = Star (rev_regexp e)"
 |"rev_regexp (Neg e) = Neg (rev_regexp e)"



(*-----------------------------------------------------*)
(* 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)"
    *)

lemma star_app_aux:
  "xa \<in> star l \<Longrightarrow> x \<in> l \<Longrightarrow>  xa @ x \<in> star l"
  apply (erule star.induct)
   apply clarsimp
   apply (drule_tac v="[]" in star_app, simp_all)[1]
  apply clarsimp
  apply (rule star_app, simp_all)
  done
  
lemma star_rev_aux1:
  " x \<in> star (rev ` l) \<Longrightarrow> x \<in> rev ` star l"
  thm star.induct
  apply (induct rule: star.induct) 
   apply simp
  apply clarsimp
  apply (rename_tac x y)
  apply (rule_tac x="y@x" in image_eqI, simp)
  apply (clarsimp simp: star_app_aux)
  done

lemma star_rev_aux2:
  " xa \<in> star l \<Longrightarrow> rev xa \<in> star (rev ` l)"
  apply (induct rule: star.induct)
   apply simp
  apply clarsimp
  apply (erule star_app_aux)
  apply simp
  done
  
  
lemma star_rev:
  "star (rev ` l) = rev ` star l"
  apply (rule equalityI)
   apply (clarsimp simp: star_rev_aux1)
  apply (clarsimp simp: star_rev_aux2)
  done
  

lemma conc_rev:
  "conc (rev ` l2) (rev ` l1) = rev ` conc l1 l2"
  apply (simp add: conc_def)
  apply (rule equalityI)
   apply clarsimp
   apply (rename_tac u v)
   apply (rule_tac x="v@u" in image_eqI, auto)[1]
  apply clarsimp
  apply auto
  done
  
lemma neg_rev:
  "- rev ` l = rev ` (- l)"
  apply (rule bij_image_Compl_eq[symmetric])
  apply (rule bijI)
   apply (rule injI)
   apply simp
  apply (rule_tac f=rev in surjI)
  apply auto[1]
  done
  
lemma "lang (rev_regexp e) = rev ` (lang e)"
  apply (induct e) 
      -- "Atom"
      apply clarsimp
     -- "Alt"
     apply auto[1]  (* or image_Un *)
    -- "Conc"
    apply (clarsimp simp: conc_rev)
   -- "Star" 
   apply (clarsimp simp add: star_rev)
  -- "Neg"
  apply (clarsimp simp: neg_rev)
  done


end
