theory Regexp
imports Main
begin

datatype regexp =
 Alt regexp regexp
 |Conc regexp regexp (infix "\<cdot>" 60)
 |Star regexp
 |Neg regexp
 |Atom char
 
type_synonym word = "char list"
 
inductive_set
  star:: "word set \<Rightarrow> word set" for L
 where 
   star_e: "[] \<in> star L"
 | star_step: "y \<in>L \<Longrightarrow> x \<in> star L \<Longrightarrow> x@y \<in> star L"

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"  
  
primrec Rev::"regexp \<Rightarrow> regexp"
 where
 "Rev (Atom c) = Atom c"
 |"Rev (Alt e1 e2) = Alt (Rev e1) (Rev e2)"
 |"Rev (Conc e1 e2) = Conc (Rev e2) (Rev e1)"
 |"Rev (Star e) = Star (Rev e)"
 |"Rev (Neg e) = Neg (Rev e)"
 
lemma conc_rev:
  "conc (rev ` l2) (rev ` l1) = rev ` conc l1 l2"
  apply (rule equalityI)
   apply clarsimp 
   apply (simp add: conc_def) thm image_eqI
   apply clarsimp find_theorems intro "_ \<in> _ ` _"
   apply (rule_tac x="xb@xa" in image_eqI) 
    apply simp
   apply auto[1]
  apply (clarsimp simp: conc_def)
  apply auto
  done

lemma star_app:
  "xa \<in> l \<Longrightarrow> xb \<in> star l \<Longrightarrow> xa @ xb \<in> star l"
  sorry
  
  
lemma star_rev1:
  "x \<in> star (rev ` l) \<Longrightarrow> x \<in> rev ` star l "
  thm star.induct
  (*apply (erule star.induct)*)
  apply (induct rule: star.induct)
   apply (simp add: star_e)
  apply clarsimp
  apply (rule_tac x="xa@xb" in image_eqI)
   apply simp
  apply (simp add: star_app)
  done
  
lemma star_rev:
  "star (rev ` l) = rev ` star l"
  apply (rule equalityI)
   apply (clarsimp simp: star_rev1)
  apply clarsimp
  sorry
  
 lemma rev_bij: "bij rev"
 sorry
 
theorem "lang (Rev e) = rev ` (lang e)"
  apply (induct e)
      apply auto[1]
     apply (simp add: conc_rev)
    apply (simp add: star_rev)
   apply clarsimp
  apply (rule bij_image_Compl_eq[symmetric])
  apply (rule rev_bij)
  find_theorems " _` (-_)"
  apply simp
  done
  
end