theory Matcher
  imports "Main" 
begin


section {* Sequential Composition of Sets *}

fun
  lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
where 
  "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"


section {* Kleene Star for Sets *}

inductive_set
  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
  for L :: "string set"
where
  start[intro]: "[] \<in> L\<star>"
| step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> L\<star>"


text {* A standard property of Star *}

lemma lang_star_cases:
  shows "L\<star> =  {[]} \<union> L ;; L\<star>"
by (auto) (metis Star.simps)

section {* Regular Expressions *}

datatype rexp =
  NULL
| EMPTY
| CHAR char
| SEQ rexp rexp
| ALT rexp rexp
| STAR rexp

types lang = "string set" 

definition
  DERIV :: "string \<Rightarrow> lang \<Rightarrow> lang"
where
  "DERIV s A \<equiv> {s'. s @ s' \<in> A}"

definition
  delta :: "lang \<Rightarrow> lang"
where
  "delta A = (if [] \<in> A then {[]} else {})"

lemma
  "DERIV s (P ; Q) = \<Union>{(delta (DERIV s1 P)) ; (DERIV s2 Q) | s1 s2. s = s1 @ s2}"
apply(auto)

fun
  D1 :: "string \<Rightarrow> lang \<Rightarrow> lang"
where
  "D1 [] A = A"
| "D1 (c # s) A = DERIV [c] (D1 s A)"

fun
  D2 :: "string \<Rightarrow> lang \<Rightarrow> lang"
where
  "D2 [] A = A"
| "D2 (c # s) A = DERIV [c] (D1 s A)"

function
  D
where
  "D s P Q = P ;; Q"
| "D (c#s) = 

section {* Semantics of Regular Expressions *}
 
fun
  L :: "rexp \<Rightarrow> string set"
where
  "L (NULL) = {}"
| "L (EMPTY) = {[]}"
| "L (CHAR c) = {[c]}"
| "L (SEQ r1 r2) = (L r1) ; (L r2)"
| "L (ALT r1 r2) = (L r1) \<union> (L r2)"
| "L (STAR r) = (L r)\<star>"


section {* The Matcher *}

fun
 nullable :: "rexp \<Rightarrow> bool"
where
  "nullable (NULL) = False"
| "nullable (EMPTY) = True"
| "nullable (CHAR c) = False"
| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
| "nullable (STAR r) = True"

fun
 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
where
  "der c (NULL) = NULL"
| "der c (EMPTY) = NULL"
| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"
| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
| "der c (STAR r) = SEQ (der c r) (STAR r)"

fun 
 derivative :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
where
  "derivative [] r = r"
| "derivative (c # s) r = derivative s (der c r)"

fun
  matches :: "rexp \<Rightarrow> string \<Rightarrow> bool"
where
  "matches r s = nullable (derivative s r)"


section {* Correctness Proof of the Matcher *}

lemma nullable_correctness:
  shows "nullable r \<longleftrightarrow> [] \<in> L r"
by (induct r) (auto) 

lemma der_correctness:
  shows "s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r"
proof (induct r arbitrary: s)
  case (SEQ r1 r2 s)
  have ih1: "\<And>s. s \<in> L (der c r1) \<longleftrightarrow> c # s \<in> L r1" by fact
  have ih2: "\<And>s. s \<in> L (der c r2) \<longleftrightarrow> c # s \<in> L r2" by fact
  show "s \<in> L (der c (SEQ r1 r2)) \<longleftrightarrow> c # s \<in> L (SEQ r1 r2)" 
    using ih1 ih2 by (auto simp add: nullable_correctness Cons_eq_append_conv)
next
  case (STAR r s)
  have ih: "\<And>s. s \<in> L (der c r) \<longleftrightarrow> c # s \<in> L r" by fact
  show "s \<in> L (der c (STAR r)) \<longleftrightarrow> c # s \<in> L (STAR r)"
  proof
    assume "s \<in> L (der c (STAR r))"
    then have "s \<in> L (der c r) ; L r\<star>" by simp
    then have "c # s \<in> L r ; (L r)\<star>" 
      by (auto simp add: ih Cons_eq_append_conv)
    then have "c # s \<in> (L r)\<star>" using lang_star_cases by auto
    then show "c # s \<in> L (STAR r)" by simp
  next
    assume "c # s \<in> L (STAR r)"
    then have "c # s \<in> (L r)\<star>" by simp
    then have "s \<in> L (der c r); (L r)\<star>"
      by (induct x\<equiv>"c # s" rule: Star.induct)
         (auto simp add: ih append_eq_Cons_conv)
    then show "s \<in> L (der c (STAR r))" by simp  
  qed
qed (simp_all)

lemma matches_correctness:
  shows "matches r s \<longleftrightarrow> s \<in> L r"
by (induct s arbitrary: r)
   (simp_all add: nullable_correctness der_correctness)

section {* Examples *}

value "matches NULL []"
value "matches (CHAR (CHR ''a'')) [CHR ''a'']"
value "matches (CHAR a) [a,a]"
value "matches (STAR (CHAR a)) []"
value "matches (STAR (CHAR a))  [a,a]"
value "matches (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"
value "matches (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"

section {* Incorrect Matcher - fun-definition rejected *}

function 
  match :: "rexp list \<Rightarrow> string \<Rightarrow> bool"
where
  "match [] [] = True"
| "match [] (c # s) = False"
| "match (NULL # rs) s = False"  
| "match (EMPTY # rs) s = match rs s"
| "match (CHAR c # rs) [] = False"
| "match (CHAR c # rs) (d # s) = (if c = d then match rs s else False)"         
| "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)" 
| "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s"
| "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)"
apply(pat_completeness)
apply(auto)
done

end