theory Matcher2
  imports "Main" 
begin



section \<open>Regular Expressions\<close>

datatype rexp =
  ZERO
| ONE
| CH char
| SEQ rexp rexp
| ALT rexp rexp
| STAR rexp

| NOT rexp
| PLUS rexp
| OPT rexp
| NTIMES rexp nat
| BETWEEN rexp nat nat
| UPTO rexp nat


section \<open>Sequential Composition of Sets\<close>

definition
  Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
where 
  "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"

text \<open>Two Simple Properties about Sequential Composition\<close>

lemma seq_empty [simp]:
  shows "A ;; {[]} = A"
  and   "{[]} ;; A = A"
by (simp_all add: Seq_def)

lemma seq_null [simp]:
  shows "A ;; {} = {}"
  and   "{} ;; A = {}"
by (simp_all add: Seq_def)

lemma seq_union:
  shows "A ;; (B \<union> C) = A ;; B \<union> A ;; C"
  and   "(B \<union> C) ;; A = B ;; A \<union> C ;; A"
by (auto simp add: Seq_def)

lemma seq_Union:
  shows "A ;; (\<Union>x\<in>B. C x) = (\<Union>x\<in>B. A ;; C x)"
by (auto simp add: Seq_def)

lemma seq_empty_in [simp]:
  "[] \<in> A ;; B \<longleftrightarrow> ([] \<in> A \<and> [] \<in> B)"
by (simp add: Seq_def)

lemma seq_assoc: 
  shows "A ;; (B ;; C) = (A ;; B) ;; C" 
apply(auto simp add: Seq_def)
apply(metis append_assoc)
apply(metis)
done


section \<open>Power for Sets\<close>

fun 
  pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101)
where
   "A \<up> 0 = {[]}"
|  "A \<up> (Suc n) = A ;; (A \<up> n)"

lemma pow_empty [simp]:
  shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"
by (induct n) (auto)

lemma pow_plus:
  "A \<up> (n + m) = A \<up> n ;; A \<up> m"
by (induct n) (simp_all add: seq_assoc)

section \<open>Kleene Star for Sets\<close>

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

text \<open>A Standard Property of Star\<close>

lemma star_decomp: 
  assumes a: "c # x \<in> A\<star>" 
  shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
using a 
using a
by (induct x\<equiv>"c # x" rule: Star.induct) 
   (auto simp add: append_eq_Cons_conv)

lemma star_cases:
  shows "A\<star> = {[]} \<union> A ;; A\<star>"
unfolding Seq_def 
by (auto) (metis Star.simps)

lemma Star_in_Pow:
  assumes a: "s \<in> A\<star>"
  shows "\<exists>n. s \<in> A \<up> n"
using a
apply(induct)
apply(auto)
apply(rule_tac x="Suc n" in exI)
apply(auto simp add: Seq_def)
done

lemma Pow_in_Star:
  assumes a: "s \<in> A \<up> n"
  shows "s \<in> A\<star>"
using a
by (induct n arbitrary: s) (auto simp add: Seq_def)


lemma Star_def2: 
  shows "A\<star> = (\<Union>n. A \<up> n)"
using Star_in_Pow Pow_in_Star
by (auto)


section \<open>Semantics of Regular Expressions\<close>
 
fun
  L :: "rexp \<Rightarrow> string set"
where
  "L (ZERO) = {}"
| "L (ONE) = {[]}"
| "L (CH 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>"
| "L (NOT r) = UNIV - (L r)"
| "L (PLUS r) = (L r) ;; ((L r)\<star>)"
| "L (OPT r) = (L r) \<union> {[]}"
| "L (NTIMES r n) = (L r) \<up> n"
| "L (BETWEEN r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
| "L (UPTO r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"

lemma "L (NOT ZERO) = UNIV"
apply(simp)
done

section \<open>The Matcher\<close>

fun
 nullable :: "rexp \<Rightarrow> bool"
where
  "nullable (ZERO) = False"
| "nullable (ONE) = True"
| "nullable (CH c) = False"
| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
| "nullable (STAR r) = True"
| "nullable (NOT r) = (\<not>(nullable r))"
| "nullable (PLUS r) = (nullable r)"
| "nullable (OPT r) = True"
| "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
| "nullable (BETWEEN r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
| "nullable (UPTO r n) = True"


fun der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
where
  "der c (ZERO) = ZERO"
| "der c (ONE) = ZERO"
| "der c (CH d) = (if c = d then ONE else ZERO)"
| "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 ZERO)"
| "der c (STAR r) = SEQ (der c r) (STAR r)"
| "der c (NOT r) = NOT(der c r)"
| "der c (PLUS r) = SEQ (der c r) (STAR r)"
| "der c (OPT r) = der c r"
| "der c (NTIMES r n) = (if n = 0 then ZERO else (SEQ (der c r) (NTIMES r (n - 1))))"
| "der c (BETWEEN r n m) = 
        (if m = 0 then ZERO else 
        (if n = 0 then SEQ (der c r) (UPTO r (m - 1))
         else SEQ (der c r) (BETWEEN r (n - 1) (m - 1))))"
| "der c (UPTO r n) = (if n = 0 then ZERO else SEQ (der c r) (UPTO r (n - 1)))"

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

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


section \<open>Correctness Proof of the Matcher\<close>

lemma nullable_correctness:
  shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
apply(induct r) 
apply(auto simp add: Seq_def) 
done

section \<open>Left-Quotient of a Set\<close>

definition
  Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
where
  "Der c A \<equiv> {s. [c] @ s \<in> A}"

lemma Der_null [simp]:
  shows "Der c {} = {}"
unfolding Der_def
by auto

lemma Der_empty [simp]:
  shows "Der c {[]} = {}"
unfolding Der_def
by auto

lemma Der_char [simp]:
  shows "Der c {[d]} = (if c = d then {[]} else {})"
unfolding Der_def
by auto

lemma Der_union [simp]:
  shows "Der c (A \<union> B) = Der c A \<union> Der c B"
unfolding Der_def
by auto

lemma Der_insert_nil [simp]:
  shows "Der c (insert [] A) = Der c A"
unfolding Der_def 
by auto 

lemma Der_seq [simp]:
  shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"
unfolding Der_def Seq_def
by (auto simp add: Cons_eq_append_conv)

lemma Der_star [simp]:
  shows "Der c (A\<star>) = (Der c A) ;; A\<star>"
proof -    
  have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"
    by (simp only: star_cases[symmetric])
  also have "... = Der c (A ;; A\<star>)"
    by (simp only: Der_union Der_empty) (simp)
  also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"
    by simp
  also have "... =  (Der c A) ;; A\<star>"
    unfolding Seq_def Der_def
    by (auto dest: star_decomp)
  finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
qed

lemma test:
  assumes "[] \<in> A"
  shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)"
  using assms
  apply(induct n)
   apply(simp)
  apply(simp)
  apply(auto simp add: Der_def Seq_def)
  apply blast
  by force


lemma Der_ntimes [simp]:
  shows "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
proof -    
  have "Der c (A  \<up> (Suc n)) = Der c (A ;; A \<up> n)"
    by(simp)
  also have "... = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
    by simp
  also have "... =  (Der c A) ;; (A \<up> n)"
    using test by force
  finally show "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" .
qed



lemma Der_UNIV [simp]:
  "Der c (UNIV - A) = UNIV - Der c A"
unfolding Der_def
by (auto)

lemma Der_pow [simp]:
  shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
unfolding Der_def 
by(auto simp add: Cons_eq_append_conv Seq_def)

lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs \<in> A \<Longrightarrow> xs \<in> A ;; B"
  using Matcher2.Seq_def by auto

lemma Der_pow2:
  shows "Der c (A \<up> n) = (if n = 0 then {} else (Der c A) ;; (A \<up> (n - 1)))"
  apply(induct n arbitrary: A)
  using Der_ntimes by auto


lemma Der_UNION [simp]: 
  shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
  by (auto simp add: Der_def)

lemma if_f:
  shows "f(if B then C else D) = (if B then f(C) else f(D))"
  by simp


lemma der_correctness:
  shows "L (der c r) = Der c (L r)"
proof(induct r)
  case ZERO
  then show ?case by simp
next
  case ONE
  then show ?case by simp
next
  case (CH x)
  then show ?case by simp
next
  case (SEQ r1 r2)
  then show ?case
    by (simp add: nullable_correctness) 
next
  case (ALT r1 r2)
  then show ?case by simp
next
  case (STAR r)
  then show ?case
    by simp 
next
  case (NOT r)
  then show ?case by simp
next
  case (PLUS r)
  then show ?case by simp
next
  case (OPT r)
  then show ?case by simp
next
  case (NTIMES r n)
  then show ?case
    apply(auto simp add: Seq_def)
    using Der_ntimes Matcher2.Seq_def less_iff_Suc_add apply fastforce
    using Der_ntimes Matcher2.Seq_def less_iff_Suc_add by auto
next
  case (BETWEEN r n m)
  then show ?case 
    apply(auto simp add: Seq_def)
    apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_pred atLeast0AtMost atMost_iff diff_Suc_Suc
        diff_is_0_eq mem_Collect_eq)
      apply(subst (asm) Der_pow2)
      apply(case_tac xa)
       apply(simp)
      apply(auto simp add: Seq_def)[1]
    apply (metis atMost_iff diff_Suc_1' diff_le_mono)
    apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atLeastAtMost_iff
        mem_Collect_eq)
    apply(subst (asm) Der_pow2)
      apply(case_tac xa)
       apply(simp)
    apply(auto simp add: Seq_def)[1]
    by force
next
  case (UPTO r x2)
  then show ?case 
    apply(auto simp add: Seq_def)
    apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atMost_iff
        mem_Collect_eq)
    apply(subst (asm) Der_pow2)
    apply(case_tac xa)
     apply(simp)
    apply(auto simp add: Seq_def)
    by (metis atMost_iff diff_Suc_1' diff_le_mono)
qed

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

end