theory Reg
imports Main
begin

datatype regexp =
  Atom char
| Alt regexp regexp
| Conc regexp regexp (infix "\<cdot>" 60)
| Star regexp ("_*" [100] 100)
| Neg regexp

definition
  "Plus r \<equiv> r \<cdot> r*"

definition
  "U \<equiv> Alt (Atom CHR ''x'') (Neg (Atom CHR ''x''))"

definition
  "Null = Neg U"

definition
  "\<epsilon> \<equiv> Null*"

definition
  "Maybe r \<equiv> Alt \<epsilon> r"

primrec
  String :: "char list \<Rightarrow> regexp"
where
  "String [] = \<epsilon>" |
  "String (c#cs) = Atom c \<cdot> String cs"

primrec      
  Rev :: "regexp \<Rightarrow> regexp"
where
  "Rev (Atom c) = Atom c" |
  "Rev (Alt a b) = Alt (Rev a) (Rev b)" |
  "Rev (a \<cdot> b) = Rev b \<cdot> Rev a" |
  "Rev (a*) = (Rev a)*" |
  "Rev (Neg a) = Neg (Rev a)"

type_synonym word = "char list"

definition 
  conc :: "word set \<Rightarrow> word set \<Rightarrow> word set"
where
  "conc A B = {xs @ ys | xs ys. xs \<in> A \<and> ys \<in> B}"

inductive_set
  star :: "word set \<Rightarrow> word set" for L
where
  star_e [simp,intro!]: "[] \<in> star L" |
  star_step: "ys \<in> L \<Longrightarrow> xs \<in> star L \<Longrightarrow> xs @ ys \<in> star L"

primrec
  lang :: "regexp \<Rightarrow> word set"
where
  "lang (Atom c) = { [c] }" |
  "lang (Alt a b) = lang a \<union> lang b" |
  "lang (a \<cdot> b) = conc (lang a) (lang b)" |
  "lang (a*) = star (lang a)" |
  "lang (Neg a) = -lang a"

lemma U[simp]: "lang U = UNIV"
  apply (simp add: U_def)
  apply auto
  done

lemma Null[simp]: "lang Null = {}"
  apply (simp add: Null_def)
  done

lemma star_empty:
  "x \<in> star {} \<Longrightarrow> x = []"
  apply (induct rule: star.induct)
   apply simp
  apply clarsimp
  done

lemma \<epsilon>[simp]: "lang \<epsilon> = {[]}"
  apply (simp add: \<epsilon>_def)
  apply (rule set_eqI)
  apply (rule iffI)
   prefer 2
   apply clarsimp
  apply clarsimp
  apply (erule star_empty)
  done

lemma "lang (String ''xyz'') = {''xyz''}"
  apply (simp add: conc_def)
  done

instantiation regexp :: "{zero,one,plus}"
begin
  definition [simp]: "0 \<equiv> Null"
  definition [simp]: "1 \<equiv> \<epsilon>"
  definition [simp]: "a + b \<equiv> Alt a b"
  instance ..
end

lemma "lang (a + 0) = lang a"
  apply simp
  done

lemma "lang (x \<cdot> 1) = lang x"
  apply simp
  apply (unfold conc_def)
  apply simp
  done

lemma "lang (x + y) = lang (y + x)"
  apply simp
  apply auto
  done

lemma "lang (a \<cdot> (b \<cdot> c)) = lang ((a \<cdot> b) \<cdot> c)"
  apply (clarsimp simp: conc_def)
  apply safe
   apply (rule_tac x="xs @ xsa" in exI)
   apply clarsimp
   apply auto[1]
  apply (rule_tac x="xsa" in exI)
  apply auto
  done

lemma conc_rev[simp]:
  "rev ` conc A B = conc (rev ` B) (rev ` A)"
  apply (rule equalityI)
   apply (fastforce simp: conc_def)
  apply (clarsimp simp: conc_def)
  apply (rule_tac x="xb@xa" in image_eqI)
   apply simp
  apply auto
  done

lemma star_one: "xs \<in> L \<Longrightarrow> xs \<in> star L"
  by (rule star_step [where xs="[]", simplified])

lemma star_append:
  "xs \<in> star L \<Longrightarrow> ys \<in> L \<Longrightarrow> ys @ xs \<in> star L"
  apply (induct rule: star.induct)
   apply (simp add: star_one)
  apply clarsimp
  apply (drule_tac xs="ys @ xs" in star_step, assumption)
  apply simp
  done

lemma star1 [intro!]: 
  "x \<in> star L \<Longrightarrow> rev x \<in> star (rev ` L)"
  apply (induct rule: star.induct)
   apply simp
  apply clarsimp
  apply (rule star_append)
   apply assumption
  apply clarsimp
  done

lemma star2:
  "x \<in> star (rev ` L) \<Longrightarrow> x \<in> rev ` star L"
  apply (induct rule: star.induct)
   apply clarsimp
  apply clarsimp
  apply (rule_tac x="x@xa" in image_eqI)
   apply simp
  apply (erule (1) star_append)
  done

lemma star_rev [simp]:
  "rev ` star L = star (rev ` L)"
  apply (rule equalityI)
   apply clarsimp
  apply (clarsimp simp: star2)
  done

lemma bij_rev: "bij rev"
  apply (rule bijI)
   apply (rule injI)
   apply simp
  apply (rule_tac f=rev in surjI)
  apply simp
  done

lemma "lang (Rev r) = rev ` lang r"
  apply (induct r)
      apply simp
     apply simp
     apply auto[1]
    apply simp
   apply simp
  apply (simp add: bij_image_Compl_eq bij_rev)
  done

end