theory Reg2 imports Main
begin

datatype 'a reg =
    Letter 'a
  | Conc "'a reg" "'a reg"
  | Alt "'a reg" "'a reg"
  | Star "'a reg" 
  | Neg "'a reg"

term "Neg (Star (Alt (Letter a) 
                 (Conc (Letter b) (Letter c))))"

type_synonym 'a lang = "'a list set"

definition 
  conc :: "'a lang => 'a lang => 'a lang"
where
  "conc l1 l2 \<equiv> {x1 @ x2|x1 x2. x1 \<in> l1 \<and> x2 \<in> l2}"

inductive_set star :: "'a lang => 'a lang" 
  for l where
  empty: "[] \<in> star l" |
  step: "\<lbrakk> ys \<in> l; xs \<in> star l; zs = xs @ ys \<rbrakk> \<Longrightarrow> 
          zs \<in> star l"

declare empty[intro!]

primrec lang :: "'a reg => 'a lang" where
  "lang (Letter x) = {[x]}" |
  "lang (Conc r1 r2) = conc (lang r1) (lang r2)" |
  "lang (Alt r1 r2) = lang r1 \<union> lang r2" |
  "lang (Star r) = star (lang r)" |
  "lang (Neg r) = - lang r"

lemma star_empty [simp]: "star {} = {[]}"
  apply (rule equalityI)
   apply clarsimp 
   apply (erule star.induct)
    apply (rule refl)
   apply simp
  apply clarsimp
  done  

primrec rv :: "'a reg => 'a reg" where
  "rv (Letter x) = Letter x" |
  "rv (Conc r1 r2) = Conc (rv r2) (rv r1)" | 
  "rv (Alt r1 r2) = Alt (rv r1) (rv r2)" |
  "rv (Star r) = Star (rv r)" |
  "rv (Neg r) = Neg (rv r)"

lemma conc_rev_image [simp]:
  "rev ` conc l1 l2 = conc (rev ` l2)  (rev ` l1)"
  apply (rule equalityI)
   apply (fastsimp simp: conc_def)
  apply (auto intro!: image_eqI simp: conc_def)
  done

lemma star_append:
 "\<lbrakk> xs \<in> star l; ys \<in> l\<rbrakk> \<Longrightarrow> ys @ xs \<in> star l"
 apply (induct rule: star.induct)
  apply (rule step, assumption)
   apply (rule empty)
  apply simp
 apply clarsimp 
 apply (rule_tac xs="ys @ xs" in step, assumption)
  apply assumption
 apply simp
 done
 
lemma star_rev1:
  "x \<in> star (rev ` l) ==> x : rev ` star l"
  apply (induct rule: star.induct)
   apply (rule image_eqI [where x="[]"])
    apply simp
   apply (rule empty)
  apply clarsimp
  apply (rule_tac x="x@xa" in image_eqI)
   apply simp
  apply (rule star_append)
    apply assumption
   apply assumption
  done

lemma star_rev2:
  "x \<in> star l ==> rev x \<in> star (rev ` l)"
  apply (induct rule: star.induct)
   apply clarsimp
  apply (clarsimp intro!: star_append) 
  done

lemma star_rev_image [simp]:
  "rev ` star l = star (rev ` l)" 
  by (blast intro: star_rev1 star_rev2)  

lemma rev_bij [simp]:
  "bij rev"
  apply (rule bijI)
   apply clarsimp
  apply (rule_tac f="rev" in surjI)
  apply simp
  done

lemma "lang (rv r) = rev ` lang r" 
  apply (induct r)
      apply simp
     apply clarsimp
    apply (clarsimp simp: image_Un)
   apply clarsimp
  apply (clarsimp simp: bij_image_Compl_eq)
  done


consts something :: "'a reg"

definition
  "everything = Alt something (Neg something)"

definition
  "nothing = Neg everything"

lemma lang_everything [simp]: 
  "lang everything = UNIV"
  apply (simp add: everything_def)
  apply blast
  done
  
lemma lang_nothing [simp]:
  "lang nothing = {}"
  apply (simp add: nothing_def)
  done

lemma "lang (Alt x nothing) = lang x"
  apply simp
  done

definition
  "\<epsilon> = Star nothing"

lemma "lang \<epsilon> = {[]}"
  by (simp add: \<epsilon>_def)

end