theory Regexp imports Main begin

datatype
  regexp = Atom char ("<_>")
         | Conc regexp regexp (infixl "\<cdot>" 70)
         | Alt regexp regexp 
         | Star regexp ("_\<star>" [79] 80) 
         | Neg regexp

instantiation regexp :: plus 
begin
  definition [simp,intro!]: "A + B \<equiv> Alt A B"
  instance ..
end

definition
  "conc A B = {xs @ ys|xs ys. xs \<in> A \<and> ys \<in> B}"

inductive_set 
  star :: "'a list set \<Rightarrow> 'a list set"  
for L :: "'a list set"
where
  empty_star [simp,intro!]: "[] \<in> star L"
| app_star: "\<lbrakk> xs \<in> L; ys \<in> star L \<rbrakk> \<Longrightarrow> xs @ ys \<in> star L"

primrec
  lang :: "regexp \<Rightarrow> char list set"
where
  "lang <c> = { [c] }"
| "lang (r1 \<cdot> 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
  "lang (<CHR ''x''> \<cdot> <CHR ''y''>) = {''xy''}"
  apply (simp add: conc_def)
  done

lemma
  "lang (Alt (Atom CHR ''x'') (Atom CHR ''y'')) = {''x'', ''y''}"
  apply (auto simp add: conc_def)
  done

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

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

instantiation regexp :: "{zero,one}"
begin
  definition null_def: "0 \<equiv> Neg U"
  definition eps_def: "1 = Star 0" 
  instance ..
end

lemma lang_Null [simp]:
  "lang 0 = {}"
  by (simp add: null_def)

lemma lang_eps [simp]:
  "lang 1 = {[]}"
  apply (simp add: eps_def)
  apply (rule set_ext)
  apply clarsimp
  apply (rule iffI)
   prefer 2
   apply clarsimp
  apply (erule star.cases)
   apply simp
  apply simp
  done

lemma
  "lang (X + 0) = lang X"
  by simp

lemma
  "lang (Alt (Alt x y) z) = lang (Alt x (Alt y z))"
  apply auto
  done

lemma 
  "lang (0 \<cdot> A) = lang 0"
  apply (simp add: conc_def)
  done

lemma "lang (A \<cdot> 0) = lang 0"
  apply (simp add: conc_def)
  done

lemma "lang (A \<cdot> 1) = lang A"
  apply (simp add: conc_def)
  done

lemma "lang (1 \<cdot> Neg 1) = lang (Neg 1)"
  apply (simp add: conc_def)
  apply auto
  done

lemma "lang ((A + B) \<cdot> C) = lang (A \<cdot> C + B \<cdot> C)"
  apply (simp add: conc_def)
  apply auto
  done

primrec 
  String :: "char list \<Rightarrow> regexp"
  where 
  "String [] = 1" |
  "String (x # xs) = Atom x \<cdot> String xs"

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

primrec
  Repeat :: "regexp \<Rightarrow> nat \<Rightarrow> regexp" where
  "Repeat R 0 = 1" |
  "Repeat R (Suc n) = R \<cdot> Repeat R n"

lemma
  "lang (Repeat (String ''xy'') 2) = {''xyxy''}"
  apply (simp add: conc_def nat_number)
  done

definition 
  Maybe :: "regexp \<Rightarrow> regexp" ("_?" [79] 80)
where
  "Maybe R \<equiv> 1 + R"

lemma lang_Maybe [simp]:
  "lang (R?) = {[]} \<union> lang R"
  by (auto simp: Maybe_def)

lemma
  "lang (String ''x'' \<cdot> (String ''y'')?) = {''x'', ''xy''}"
  by (auto simp add: conc_def)

definition 
  "RepeatUpTo R n m \<equiv> Repeat R n \<cdot> Repeat (R?) (m - n)"

primrec Rev where
  "Rev (Atom x) = Atom x"
| "Rev (Conc x y) = Conc (Rev y) (Rev x)"
| "Rev (Star x) = Star (Rev x)"
| "Rev (Alt x y) = Alt (Rev x) (Rev y)"
| "Rev (Neg x) = Neg (Rev x)"

lemma surj_rev [simp, intro!]:
  "surj rev"
  apply (clarsimp simp: surj_def)
  apply (rule_tac x = "rev y" in exI)
  apply simp
  done
  
lemma conc_rev [simp]:
  "conc (rev ` lang r2) (rev ` lang r1) = rev ` conc (lang r1) (lang r2)"
  apply (simp add: 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 simp
  done

lemma star_app:
  "\<lbrakk> xs \<in> star L; ys \<in> L \<rbrakk> \<Longrightarrow> xs @ ys \<in> star L"
  apply (erule star.induct)
   apply clarsimp
   apply (drule app_star)
    apply (rule empty_star)
   apply simp
  apply clarsimp
  apply (erule (1) app_star)
  done
   
lemma star_rev [simp]:
  "star (rev ` lang r) = rev ` star (lang r)"
  apply (rule set_ext)
  apply (rule iffI)
   apply (erule star.induct)
    apply simp
   apply clarsimp
   apply (rule_tac x="xa @ x" in image_eqI)
    apply simp
   apply (erule (1) star_app)
  apply clarsimp
  apply (erule star.induct)
   apply simp
  apply clarsimp
  apply (erule star_app)
  apply simp
  done

lemma Rev_is_rev:
  "lang (Rev r) = rev ` lang r"
  apply (induct r)
      apply simp
     apply simp
    apply simp
    apply blast
   apply clarsimp
  apply clarsimp
  apply (simp add: bij_image_Compl_eq bijI)
  done

end