theory Matcher2

  imports "Main" 

begin

lemma Suc_Union:

  "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))"

by (metis UN_insert atMost_Suc)

lemma Suc_reduce_Union:

  "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"

by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)

section \<open>Regular Expressions\<close>

datatype rexp =

  NULL

| EMPTY

| CH char

| SEQ rexp rexp

| ALT rexp rexp

| STAR rexp

| NOT rexp

| PLUS rexp

| OPT rexp

| NTIMES rexp nat

| NMTIMES rexp nat nat

| UPNTIMES 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 (NULL) = {}"

| "L (EMPTY) = {[]}"

| "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 (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 

| "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"

lemma "L (NOT NULL) = UNIV"

apply(simp)

done

section \<open>The Matcher\<close>

fun

 nullable :: "rexp \<Rightarrow> bool"

where

  "nullable (NULL) = False"

| "nullable (EMPTY) = 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 (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"

| "nullable (UPNTIMES r n) = True"

fun M :: "rexp \<Rightarrow> nat"

where

  "M (NULL) = 0"

| "M (EMPTY) = 0"

| "M (CH char) = 0"

| "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"

| "M (ALT r1 r2) = Suc ((M r1) + (M r2))"

| "M (STAR r) = Suc (M r)"

| "M (NOT r) = Suc (M r)"

| "M (PLUS r) = Suc (M r)"

| "M (OPT r) = Suc (M r)"

| "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"

| "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"

| "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)"

where

  "der c (NULL) = NULL"

| "der c (EMPTY) = NULL"

| "der c (CH d) = (if c = d 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)"

| "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 (NMTIMES r n m) = 

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 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 NULL

  then show ?case by simp

next

  case EMPTY

  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

next

  case (NMTIMES r n m)

  then show ?case 

    apply(case_tac n)

    sorry

next

  case (UPNTIMES r x2)

qed

lemma der_correctness:

  shows "L (der c r) = Der c (L r)"

apply(induct rule: der.induct) 

apply(simp_all add: nullable_correctness 

    Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)

apply(rule impI)+

apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")

apply(auto simp add: Seq_def)

done

lemma L_der_NTIMES:

  shows "L(der c (NTIMES r n)) = L (if n = 0 then NULL else if nullable r then 

         SEQ (der c r) (UPNTIMES r (n - 1)) else SEQ (der c r) (NTIMES r (n - 1)))"

apply(induct n)

apply(simp)

apply(simp)

apply(auto)

apply(auto simp add: Seq_def)

apply(rule_tac x="s1" in exI)

apply(simp)

apply(rule_tac x="xa" in bexI)

apply(simp)

apply(simp)

apply(rule_tac x="s1" in exI)

apply(simp)

by (metis Suc_pred atMost_iff le_Suc_eq)

lemma "L(der c (UPNTIMES r 0)) = {}"

by simp

lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"

proof(induct n)

  case 0 show ?case by simp

next

  case (Suc n)

  have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact

  { assume a: "nullable r"

    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"

    by (simp only: der_correctness)

    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"

    by(simp only: L.simps Suc_Union)

    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"

    by (simp only: der_correctness)

    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"

    by(auto simp add: Seq_def)

    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"

    using IH by simp

    also have "... = L (SEQ (der c r) (UPNTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"

    using a unfolding L_der_NTIMES by simp

    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"

    by (auto, metis Suc_Union Un_iff seq_Union)

    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .

    } 

  moreover

  { assume a: "\<not>nullable r"

    have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"

    by (simp only: der_correctness)

    also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"

    by(simp only: L.simps Suc_Union)

    also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"

    by (simp only: der_correctness)

    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"

    by(auto simp add: Seq_def)

    also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"

    using IH by simp

    also have "... = L (SEQ (der c r) (NTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"

    using a unfolding L_der_NTIMES by simp

    also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"

    by (simp add: Suc_Union seq_union(1))

    finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .

  }

  ultimately  

  show "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))"

  by blast

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