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