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 \ 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 \ regexp" where "quest r = Alt r epsilon" primrec str :: "string \ regexp" where "str [] = epsilon" | "str (x # xs) = Conc (Atom x) (str xs)" value \str ''hello''\ (* rrev (str ''hello'') ~= str ''olleh'' *) (* Atom char | Star regexp | Conc regexp regexp | Alt regexp regexp | Neg regexp *) primrec rrev :: "regexp \ 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 \ 'a list set \ 'a list set" where "conc X Y = { xs@ys | xs ys. xs \ X \ ys \ Y }" inductive_set star :: "'a list set \ 'a list set" for L where eps[simp, intro!]: "[] \ star L" | step: "\ xs \ L; ys \ star L \ \ xs @ ys \ star L" print_theorems primrec lang :: "regexp \ 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 \ 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 \ star {} \ 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: "[] \ star L" | step: "\ xs \ L; ys \ star L \ \ xs @ ys \ star L" *) lemmas star_once = step[where ys="[]", simplified] lemma star_step': "\ ys \ star L; xs \ L \ \ ys @ xs \ 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 \ star (rev ` L) \ xs \ 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 \ star L \ rev xs \ 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