theory Reg 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 \<Rightarrow> 'a lang \<Rightarrow> '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"

primrec lang :: "'a reg \<Rightarrow> '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)"

text {* Sanity checks (ask students what they think these should be) *}

lemma
  "lang (Conc (Letter CHR ''x'') (Letter CHR ''y'')) = X"
  apply (simp add: conc_def)
  oops

lemma
  "lang (Alt (Letter CHR ''x'') (Letter CHR ''y'')) = X"
  apply (simp add: conc_def)
  oops

lemma
  "lang (Alt (Letter CHR ''x'')  (Neg (Letter CHR ''x''))) = X"
  apply (auto)
  oops

text {* Regular expression reversal *}

primrec rv :: "'a reg \<Rightarrow> '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)"
  sorry

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) \<Longrightarrow> x \<in> 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_rev_image [simp]:
  "rev ` star l = star (rev ` l)"
  sorry

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

end
