theory Reg_demo
  imports Main
begin

(*
  Regular expressions

  https://jflex.de

  if you want to see the original Java function, look for class RegExp, method rev:
  https://github.com/jflex-de/jflex/blob/master/jflex/src/main/java/jflex/core/RegExp.java#L741


  Regexp examples:

  ( a* b* )?

  a
  a*
  ab
  a|b  
  neg a
  
*)

datatype regexp =
    Atom char  
  | Star regexp
  | Conc regexp regexp
  | Alt regexp regexp
  | Neg regexp

term "Conc (Atom (CHR ''a'')) (Atom (CHR ''b''))"

definition all :: regexp where
  "all \<equiv> Alt (Atom CHR ''a'') (Neg (Atom CHR ''a''))"

definition null :: regexp where
  "null = Neg all"

definition epsilon :: regexp where
  "epsilon = Star null"

definition quest :: "regexp \<Rightarrow> regexp" where
  "quest r = Alt r epsilon"

primrec str :: "string \<Rightarrow> regexp" where
  "str [] = epsilon" |
  "str (x # xs) = Conc (Atom x) (str xs)"

value \<open>str ''hello''\<close>

(* rrev (str ''hello'') ~= str ''olleh'' *)

(* 
     Atom char  
  | Star regexp
  | Conc regexp regexp
  | Alt regexp regexp
  | Neg regexp
*)

primrec rrev :: "regexp \<Rightarrow> regexp" where
  "rrev (Atom c) = Atom c" |
  "rrev (Star r) = Star (rrev r)" |
  "rrev (Conc a b) = Conc (rrev b) (rrev a)" |
  "rrev (Alt a b) = Alt (rrev a) (rrev b)" |
  "rrev (Neg r) = Neg (rrev r)"

value "rrev (Star (str ''hello''))"

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

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

print_theorems

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


lemma lang_all[simp]:
  "lang all = UNIV"
  by (simp add: all_def)

lemma lang_null[simp]:
  "lang null = {}"
  by (simp add: null_def)

lemma star_empty:
  "xs \<in> star {} \<Longrightarrow> xs = []"
  by (auto elim: star.cases)

lemma empty_star[simp]:
  "star {} = {[]}"
  by (auto elim: star.cases)

lemma lang_epsilon[simp]:
  "lang epsilon = { [] }"
  by (simp add: epsilon_def)

lemma
  "lang (Alt a b) = lang (Alt b a)"
  by auto

lemma
  "lang (Alt a (Alt b c)) = lang (Alt (Alt a b) c)"
  by auto

lemma
  "lang (Alt a null) = lang a"
  by auto

lemma
  "lang (Alt a all) = lang all"
  by auto

lemma
  "lang (Conc a epsilon) = lang a"
  by (auto simp: conc_def)

lemma conc_rev[simp]:
  "conc (rev ` B) (rev ` A) = rev ` conc A B"
  by (fastforce simp: conc_def image_def)

(*
  eps:  "[] \<in> star L" |
  step: "\<lbrakk> xs \<in> L; ys \<in> star L \<rbrakk> \<Longrightarrow> xs @ ys \<in> star L"
*)
lemmas star_once = step[where ys="[]", simplified]

lemma star_step':
  "\<lbrakk> ys \<in> star L; xs \<in> L \<rbrakk> \<Longrightarrow> ys @ xs \<in> star L"
  apply (induct ys rule: star.induct)
   apply (simp add: star_once)
  apply simp
  apply (rule star.step)
   apply assumption
  apply assumption
  done

lemma star_rev:
  "xs \<in> star (rev ` L) \<Longrightarrow> xs \<in> rev ` star L"
  apply (induct rule: star.induct)
   apply simp
  apply clarsimp
  apply (rename_tac xs ys)
  apply (clarsimp simp: image_iff)
  apply (rule_tac x="ys @ xs" in bexI)
   apply simp
  apply (erule (1) star_step')
  done

lemma rev_star:
  "xs \<in> star L \<Longrightarrow> rev xs \<in> star (rev ` L)"
  apply (induct rule: star.induct)
   apply simp
  apply clarsimp
  apply (rule star_step')
   apply simp
  apply simp
  done

lemma star_rev_eq[simp]:
  "star (rev ` L) = rev ` star L"
  apply (rule equalityI; clarsimp)
   apply (erule star_rev)
  apply (erule rev_star)
  done
  
lemma rev_complement[simp]:
  "rev ` (- L) = - rev ` L"
  apply (rule bij_image_Compl_eq)
  apply (rule involuntory_imp_bij)
  apply simp
  done

theorem
  "lang (rrev r) = rev ` lang r"
  by (induct r) auto

end
