theory Reg imports Main begin

datatype 'a regexp =
  Atom 'a
| Seq "'a regexp" "'a regexp"
| Star "'a regexp"
| Alt "'a regexp" "'a regexp"
| Neg "'a regexp"

types 'a lang = "'a list set"

definition
  conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
where
  "conc X Y \<equiv> {xs @ ys|xs ys. xs \<in> X \<and> ys \<in> Y}"

primrec
  repeat_n :: "'a lang \<Rightarrow> nat \<Rightarrow> 'a lang"
where
  "repeat_n X 0 = {[]}" |
  "repeat_n X (Suc n) = conc (repeat_n X n) X"

definition
  star_r :: "'a lang \<Rightarrow> 'a lang"
where
  "star_r X \<equiv> \<Union>n. repeat_n X n"

inductive_set
  star :: "'a lang \<Rightarrow> 'a lang"
for X :: "'a lang"
where
  star_empty [simp,intro!]: "[] \<in> star X"
| star_app [intro]: "\<lbrakk> xs \<in> X; ys \<in> star X \<rbrakk> \<Longrightarrow> ys @ xs \<in> star X"

lemma repeat_n_star [rule_format]:
  "\<forall>xs. xs \<in> repeat_n X n \<longrightarrow> xs \<in> star X"
  apply (induct_tac n)
   apply clarsimp
  apply clarsimp
  apply (clarsimp simp: conc_def)
  apply blast
  done

lemma "star_r X = star X"
  apply (rule set_ext)
  apply (rule iffI)
   prefer 2
   apply (erule star.induct)
    apply (simp add: star_r_def)
    apply (rule exI [where x=0])
    apply simp
   apply (simp add: star_r_def)
   apply clarsimp
   apply (rule_tac x="Suc x" in exI)
   apply simp
   apply (clarsimp simp: conc_def)
   apply blast
  apply (clarsimp simp: star_r_def)
  apply (rename_tac xs n)
  apply (erule repeat_n_star)
  done

primrec
  lang :: "'a regexp \<Rightarrow> 'a lang"
where
  "lang (Atom x) = {[x]}"
| "lang (Seq x y) = conc (lang x) (lang y)"
| "lang (Alt x y) = lang x \<union> lang y"
| "lang (Neg x) = - lang x"
| "lang (Star x) = star (lang x)"

primrec
  Rev :: "'a regexp \<Rightarrow> 'a regexp"
where
  "Rev (Atom x) = Atom x"
| "Rev (Seq x y) = Seq (Rev y) (Rev x)"
| "Rev (Alt x y) = Alt (Rev x) (Rev y)"
| "Rev (Star x) = Star (Rev x)"
| "Rev (Neg x) = Neg (Rev x)"

lemma conc_rev [simp]:
  "conc (rev ` A) (rev ` B) = rev ` conc B A"
  apply (clarsimp simp: conc_def)
  apply (rule set_ext)
  apply clarsimp
  apply (rule iffI)
   apply clarsimp
   apply (rule_tac x="xb@xa" in image_eqI)
    apply simp
   apply clarsimp
   apply blast
  apply clarsimp
  apply (rule_tac x="rev ys" in exI)
  apply (rule_tac x="rev xs" in exI)
  apply blast
  done

lemma app_star [rule_format]:
  "ys \<in> star X \<Longrightarrow> xs \<in> X \<longrightarrow> xs @ ys \<in> star X"
  apply (erule star.induct)
   apply clarsimp 
   apply (drule star_app)
    apply (rule star_empty)
   apply simp
  apply clarsimp 
  apply (drule_tac ys="xs @ ys" in star_app)
   apply assumption
  apply simp
  done

lemma star_rev [simp]:
  "star (rev ` A) = rev ` star A"
  apply (rule set_ext)
  apply (rule iffI)
   apply (erule star.induct)
    apply simp
   apply clarsimp
   apply (rule image_eqI)
    prefer 2
    apply (erule (1) app_star)
   apply simp
  apply clarsimp
  apply (erule star.induct)
   apply simp
  apply clarsimp
  apply (rule app_star)
   apply clarsimp
  apply simp
  done

lemma 
  "lang (Rev x) = rev ` lang x"
  apply (induct x)
      apply simp
     apply clarsimp
    apply clarsimp
   apply simp
   apply blast
  apply simp
  apply (rule bij_image_Compl_eq [symmetric])
  apply (rule bijI)
   apply simp
  apply (simp add: surj_def)
  apply clarsimp
  apply (rule_tac x = "rev y" in exI)
  apply simp
  done
 
end