1 theory MatcherNot

     2   imports "Main" 

     3 begin

     4 

     5 

     6 section {* Regular Expressions *}

     7 

     8 datatype rexp =

     9   NULL

    10 | EMPTY

    11 | CHAR char

    12 | SEQ rexp rexp

    13 | ALT rexp rexp

    14 | STAR rexp

    15 | NOT rexp

    16 

    17 section {* Sequential Composition of Sets *}

    18 

    19 definition

    20   Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)

    21 where 

    22   "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}"

    23 

    24 text {* Two Simple Properties about Sequential Composition *}

    25 

    26 lemma seq_empty [simp]:

    27   shows "A ;; {[]} = A"

    28   and   "{[]} ;; A = A"

    29 by (simp_all add: Seq_def)

    30 

    31 lemma seq_null [simp]:

    32   shows "A ;; {} = {}"

    33   and   "{} ;; A = {}"

    34 by (simp_all add: Seq_def)

    35 

    36 section {* Kleene Star for Sets *}

    37 

    38 inductive_set

    39   Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)

    40   for A :: "string set"

    41 where

    42   start[intro]: "[] \<in> A\<star>"

    43 | step[intro]:  "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>"

    44 

    45 

    46 text {* A Standard Property of Star *}

    47 

    48 lemma star_cases:

    49   shows "A\<star> = {[]} \<union> A ;; A\<star>"

    50 unfolding Seq_def

    51 by (auto) (metis Star.simps)

    52 

    53 lemma star_decomp: 

    54   assumes a: "c # x \<in> A\<star>" 

    55   shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"

    56 using a

    57 by (induct x\<equiv>"c # x" rule: Star.induct) 

    58    (auto simp add: append_eq_Cons_conv)

    59 

    60 

    61 section {* Semantics of Regular Expressions *}

    62  

    63 fun

    64   L :: "rexp \<Rightarrow> string set"

    65 where

    66   "L (NULL) = {}"

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

    68 | "L (CHAR c) = {[c]}"

    69 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"

    70 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"

    71 | "L (STAR r) = (L r)\<star>"

    72 | "L (NOT r) = UNIV - (L r)"

    73 

    74 section {* The Matcher *}

    75 

    76 fun

    77  nullable :: "rexp \<Rightarrow> bool"

    78 where

    79   "nullable (NULL) = False"

    80 | "nullable (EMPTY) = True"

    81 | "nullable (CHAR c) = False"

    82 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"

    83 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"

    84 | "nullable (STAR r) = True"

    85 | "nullable (NOT r) = (\<not> nullable r)"

    86 

    87 fun

    88  noccurs :: "rexp \<Rightarrow> bool"

    89 where

    90   "noccurs (NULL) = True"

    91 | "noccurs (EMPTY) = False"

    92 | "noccurs (CHAR c) = False"

    93 | "noccurs (ALT r1 r2) = (noccurs r1 \<or> noccurs r2)"

    94 | "noccurs (SEQ r1 r2) = (noccurs r1 \<or> noccurs r2)"

    95 | "noccurs (STAR r) = (noccurs r)"

    96 | "noccurs (NOT r) = (\<not>noccurs r)"

    97 

    98 lemma

    99   "L r = {} \<Longrightarrow> noccurs r"

   100 apply(induct r)

   101 apply(auto simp add: Seq_def)

   102 oops

   103 

   104 lemma

   105   "\<not> noccurs r \<Longrightarrow> L r \<noteq> {}"

   106 apply(induct r)

   107 apply(auto simp add: Seq_def)

   108 oops

   109 

   110 

   111 fun

   112  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"

   113 where

   114   "der c (NULL) = NULL"

   115 | "der c (EMPTY) = NULL"

   116 | "der c (CHAR c') = (if c = c' then EMPTY else NULL)"

   117 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"

   118 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"

   119 | "der c (STAR r) = SEQ (der c r) (STAR r)"

   120 | "der c (NOT r) = NOT (der c r)"

   121 

   122 fun 

   123  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"

   124 where

   125   "ders [] r = r"

   126 | "ders (c # s) r = ders s (der c r)"

   127 

   128 fun

   129   matcher :: "rexp \<Rightarrow> string \<Rightarrow> bool"

   130 where

   131   "matcher r s = nullable (ders s r)"

   132 

   133 

   134 section {* Correctness Proof of the Matcher *}

   135 

   136 lemma nullable_correctness:

   137   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"

   138 by (induct r) (auto simp add: Seq_def) 

   139 section {* Left-Quotient of a Set *}

   140 

   141 fun

   142  zeroable :: "rexp \<Rightarrow> bool"

   143 where

   144   "zeroable (NULL) = True"

   145 | "zeroable (EMPTY) = False"

   146 | "zeroable (CHAR c) = False"

   147 | "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"

   148 | "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"

   149 | "zeroable (STAR r) = False"

   150 | "zeroable (NOT r) = ((nullable r))"

   151 

   152 lemma zeroable_correctness:

   153   shows "zeroable r  \<longleftrightarrow>  (L r = {})"

   154 apply(induct r)

   155 apply(auto simp add: Seq_def)[6]

   156 apply(simp add: nullable_correctness)

   157 apply(auto)

   158 

   159 

   160 by (induct r) (auto simp add: Seq_def) 

   161 section {* Left-Quotient of a Set *}

   162 

   163 

   164 definition

   165   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"

   166 where

   167   "Der c A \<equiv> {s. [c] @ s \<in> A}"

   168 

   169 lemma Der_null [simp]:

   170   shows "Der c {} = {}"

   171 unfolding Der_def

   172 by auto

   173 

   174 lemma Der_empty [simp]:

   175   shows "Der c {[]} = {}"

   176 unfolding Der_def

   177 by auto

   178 

   179 lemma Der_char [simp]:

   180   shows "Der c {[d]} = (if c = d then {[]} else {})"

   181 unfolding Der_def

   182 by auto

   183 

   184 lemma Der_union [simp]:

   185   shows "Der c (A \<union> B) = Der c A \<union> Der c B"

   186 unfolding Der_def

   187 by auto

   188 

   189 lemma Der_seq [simp]:

   190   shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})"

   191 unfolding Der_def Seq_def

   192 by (auto simp add: Cons_eq_append_conv)

   193 

   194 lemma Der_star [simp]:

   195   shows "Der c (A\<star>) = (Der c A) ;; A\<star>"

   196 proof -    

   197   have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)"

   198     by (simp only: star_cases[symmetric])

   199   also have "... = Der c (A ;; A\<star>)"

   200     by (simp only: Der_union Der_empty) (simp)

   201   also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})"

   202     by simp

   203   also have "... =  (Der c A) ;; A\<star>"

   204     unfolding Seq_def Der_def

   205     by (auto dest: star_decomp)

   206   finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .

   207 qed

   208 

   209 

   210 lemma der_correctness:

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

   212 by (induct r) 

   213    (simp_all add: nullable_correctness)

   214 

   215 lemma matcher_correctness:

   216   shows "matcher r s \<longleftrightarrow> s \<in> L r"

   217 by (induct s arbitrary: r)

   218    (simp_all add: nullable_correctness der_correctness Der_def)

   219 

   220 section {* Examples *}

   221 

   222 definition 

   223   "CHRA \<equiv> CHAR (CHR ''a'')"

   224 

   225 definition 

   226   "ALT1 \<equiv> ALT CHRA EMPTY"

   227 

   228 definition 

   229   "SEQ3 \<equiv> SEQ (SEQ ALT1 ALT1) ALT1"

   230 

   231 value "matcher SEQ3 ''aaa''"

   232 

   233 value "matcher NULL []"

   234 value "matcher (CHAR (CHR ''a'')) [CHR ''a'']"

   235 value "matcher (CHAR a) [a,a]"

   236 value "matcher (STAR (CHAR a)) []"

   237 value "matcher (STAR (CHAR a))  [a,a]"

   238 value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbbbc''"

   239 value "matcher (SEQ (CHAR (CHR ''a'')) (SEQ (STAR (CHAR (CHR ''b''))) (CHAR (CHR ''c'')))) ''abbcbbc''"

   240 

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

   242 

   243 fun

   244   match :: "rexp list \<Rightarrow> string \<Rightarrow> bool"

   245 where

   246   "match [] [] = True"

   247 | "match [] (c # s) = False"

   248 | "match (NULL # rs) s = False"  

   249 | "match (EMPTY # rs) s = match rs s"

   250 | "match (CHAR c # rs) [] = False"

   251 | "match (CHAR c # rs) (d # s) = (if c = d then match rs s else False)"         

   252 | "match (ALT r1 r2 # rs) s = (match (r1 # rs) s \<or> match (r2 # rs) s)" 

   253 | "match (SEQ r1 r2 # rs) s = match (r1 # r2 # rs) s"

   254 | "match (STAR r # rs) s = (match rs s \<or> match (r # (STAR r) # rs) s)"

   255 

   256 

   257 end