1 theory Matcher2

     2   imports "Main" 

     3 begin

     4 

     5 section {* Regular Expressions *}

     6 

     7 datatype rexp =

     8   NULL

     9 | EMPTY

    10 | CHAR char

    11 | SEQ rexp rexp

    12 | ALT rexp rexp

    13 | STAR rexp

    14 | NOT rexp

    15 | PLUS rexp

    16 | OPT rexp

    17 | NTIMES rexp nat

    18 | NMTIMES rexp nat nat

    19 

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

    21 where

    22   "M (NULL) = 0"

    23 | "M (EMPTY) = 0"

    24 | "M (CHAR char) = 0"

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

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

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

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

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

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

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

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

    33 

    34 section {* Sequential Composition of Sets *}

    35 

    36 definition

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

    38 where 

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

    40 

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

    42 

    43 lemma seq_empty [simp]:

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

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

    46 by (simp_all add: Seq_def)

    47 

    48 lemma seq_null [simp]:

    49   shows "A ;; {} = {}"

    50   and   "{} ;; A = {}"

    51 by (simp_all add: Seq_def)

    52 

    53 lemma seq_union:

    54   shows "A ;; (B \<union> C) = A ;; B \<union> A ;; C"

    55 by (auto simp add: Seq_def)

    56 

    57 lemma seq_Union:

    58   shows "A ;; (\<Union>x\<in>B. C x) = (\<Union>x\<in>B. A ;; C x)"

    59 by (auto simp add: Seq_def)

    60 

    61 lemma seq_empty_in [simp]:

    62   "[] \<in> A ;; B \<longleftrightarrow> ([] \<in> A \<and> [] \<in> B)"

    63 by (simp add: Seq_def)

    64 

    65 section {* Kleene Star for Sets *}

    66 

    67 inductive_set

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

    69   for A :: "string set"

    70 where

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

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

    73 

    74 

    75 text {* A Standard Property of Star *}

    76 

    77 lemma star_cases:

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

    79 unfolding Seq_def

    80 by (auto) (metis Star.simps)

    81 

    82 lemma star_decomp: 

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

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

    85 using a

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

    87    (auto simp add: append_eq_Cons_conv)

    88 

    89 section {* Power for Sets *}

    90 

    91 fun 

    92   pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101)

    93 where

    94    "A \<up> 0 = {[]}"

    95 |  "A \<up> (Suc n) = A ;; (A \<up> n)"

    96 

    97 

    98 lemma pow_empty [simp]:

    99   shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)"

   100 by (induct n) (auto)

   101 

   102 

   103 section {* Semantics of Regular Expressions *}

   104  

   105 fun

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

   107 where

   108   "L (NULL) = {}"

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

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

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

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

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

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

   115 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"

   116 | "L (OPT r) = (L r) \<union> {[]}"

   117 | "L (NTIMES r n) = (L r) \<up> n"

   118 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..n+m} . ((L r) \<up> i))" 

   119 

   120 

   121 section {* The Matcher *}

   122 

   123 fun

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

   125 where

   126   "nullable (NULL) = False"

   127 | "nullable (EMPTY) = True"

   128 | "nullable (CHAR c) = False"

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

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

   131 | "nullable (STAR r) = True"

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

   133 | "nullable (PLUS r) = (nullable r)"

   134 | "nullable (OPT r) = True"

   135 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"

   136 | "nullable (NMTIMES r n m) = (if n = 0 then True else nullable r)"

   137 

   138 function

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

   140 where

   141   "der c (NULL) = NULL"

   142 | "der c (EMPTY) = NULL"

   143 | "der c (CHAR d) = (if c = d then EMPTY else NULL)"

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

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

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

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

   148 | "der c (PLUS r) = SEQ (der c r) (STAR r)"

   149 | "der c (OPT r) = der c r"

   150 | "der c (NTIMES r 0) = NULL"

   151 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"

   152 | "der c (NMTIMES r 0 0) = NULL"

   153 | "der c (NMTIMES r 0 (Suc m)) = ALT (der c (NTIMES r (Suc m))) (der c (NMTIMES r 0 m))"

   154 | "der c (NMTIMES r (Suc n) m) = der c  (SEQ r (NMTIMES r n m))"

   155 by pat_completeness auto

   156 

   157 termination der 

   158 apply(relation "measure (\<lambda>(c, r). M r)")

   159 apply(simp_all)

   160 done

   161 

   162 fun 

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

   164 where

   165   "ders [] r = r"

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

   167 

   168 fun

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

   170 where

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

   172 

   173 

   174 section {* Correctness Proof of the Matcher *}

   175 

   176 lemma nullable_correctness:

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

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

   179 

   180 

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

   182 

   183 definition

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

   185 where

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

   187 

   188 lemma Der_null [simp]:

   189   shows "Der c {} = {}"

   190 unfolding Der_def

   191 by auto

   192 

   193 lemma Der_empty [simp]:

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

   195 unfolding Der_def

   196 by auto

   197 

   198 lemma Der_char [simp]:

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

   200 unfolding Der_def

   201 by auto

   202 

   203 lemma Der_union [simp]:

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

   205 unfolding Der_def

   206 by auto

   207 

   208 lemma Der_insert_nil [simp]:

   209   shows "Der c (insert [] A) = Der c A"

   210 unfolding Der_def 

   211 by auto 

   212 

   213 lemma Der_seq [simp]:

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

   215 unfolding Der_def Seq_def

   216 by (auto simp add: Cons_eq_append_conv)

   217 

   218 lemma Der_star [simp]:

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

   220 proof -    

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

   222     by (simp only: star_cases[symmetric])

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

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

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

   226     by simp

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

   228     unfolding Seq_def Der_def

   229     by (auto dest: star_decomp)

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

   231 qed

   232 

   233 lemma Der_UNIV [simp]:

   234   "Der c (UNIV - A) = UNIV - Der c A"

   235 unfolding Der_def

   236 by (auto)

   237 

   238 lemma Der_pow [simp]:

   239   shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"

   240 unfolding Der_def 

   241 by(auto simp add: Cons_eq_append_conv Seq_def)

   242 

   243 

   244 lemma Der_UNION [simp]: 

   245   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"

   246 by (auto simp add: Der_def)

   247 

   248 lemma test:

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

   250 by (metis UN_insert atMost_Suc)

   251 

   252 lemma yy:

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

   254 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)

   255 

   256 lemma uu:

   257   "(Suc n) + m = Suc (n + m)"

   258 by simp

   259 

   260 lemma der_correctness:

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

   262 apply(induct rule: der.induct) 

   263 apply(simp_all add: nullable_correctness)[12]

   264 apply(simp only: L.simps der.simps)

   265 apply(simp only: Der_UNION)

   266 apply(simp del: pow.simps Der_pow)

   267 apply(simp only: atLeast0AtMost)

   268 apply(simp only: test)

   269 apply(simp only: L.simps der.simps)

   270 apply(simp only: Der_UNION)

   271 apply(simp only: yy add_Suc)

   272 apply(simp only: seq_Union)

   273 apply(simp only: Der_UNION)

   274 apply(simp only: pow.simps)

   275 done

   276 

   277 lemma matcher_correctness:

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

   279 by (induct s arbitrary: r)

   280    (simp_all add: nullable_correctness der_correctness Der_def)

   281 

   282 

   283 end