Mercurial Mercurial > hg > afl-material / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
progs/Matcher2.thy
changeset 1011 31e011ce66e3
parent 1010 ae9ffbf979ff
equal deleted inserted replaced
1010:ae9ffbf979ff 1011:31e011ce66e3 
     1 theory Matcher2
 
     1 theory Matcher2
 
     2   imports "Main" 
     2   imports "Main" 
     3 begin
 
     3 begin
 
     4 
     4 
     5 lemma Suc_Union:
 
       
     6   "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))"
 
       
     7 by (metis UN_insert atMost_Suc)
 
       
     8 
       
     9 lemma Suc_reduce_Union:
 
       
    10   "(\<Union>x\<in>{Suc n..Suc m}. B x) = (\<Union>x\<in>{n..m}. B (Suc x))"
 
       
    11 by (metis UN_extend_simps(10) image_Suc_atLeastAtMost)
 
       
    12 
     5 
    13 
     6 
    14 section \<open>Regular Expressions\<close>
 
     7 section \<open>Regular Expressions\<close>
 
    15 
     8 
    16 datatype rexp =
 
     9 datatype rexp =
 
    17   NULL
 
    10   ZERO
 
    18 | EMPTY
 
    11 | ONE
 
    19 | CH char
 
    12 | CH char
 
    20 | SEQ rexp rexp
 
    13 | SEQ rexp rexp
 
    21 | ALT rexp rexp
 
    14 | ALT rexp rexp
 
    22 | STAR rexp
 
    15 | STAR rexp
 
       
    16 
    23 | NOT rexp
 
    17 | NOT rexp
 
    24 | PLUS rexp
 
    18 | PLUS rexp
 
    25 | OPT rexp
 
    19 | OPT rexp
 
    26 | NTIMES rexp nat
 
    20 | NTIMES rexp nat
 
    27 | NMTIMES rexp nat nat
 
    21 | BETWEEN rexp nat nat
 
    28 | UPNTIMES rexp nat
 
    22 | UPTO rexp nat
 
    29 
    23 
    30 
    24 
    31 section \<open>Sequential Composition of Sets\<close>
 
    25 section \<open>Sequential Composition of Sets\<close>
 
    32 
    26 
    33 definition
 
    27 definition
 
   134 section \<open>Semantics of Regular Expressions\<close>
 
   128 section \<open>Semantics of Regular Expressions\<close>
 
   135  
   129  
   136 fun
 
   130 fun
 
   137   L :: "rexp \<Rightarrow> string set"
 
   131   L :: "rexp \<Rightarrow> string set"
 
   138 where
 
   132 where
 
   139   "L (NULL) = {}"
 
   133   "L (ZERO) = {}"
 
   140 | "L (EMPTY) = {[]}"
 
   134 | "L (ONE) = {[]}"
 
   141 | "L (CH c) = {[c]}"
 
   135 | "L (CH c) = {[c]}"
 
   142 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
   136 | "L (SEQ r1 r2) = (L r1) ;; (L r2)"
 
   143 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
   137 | "L (ALT r1 r2) = (L r1) \<union> (L r2)"
 
   144 | "L (STAR r) = (L r)\<star>"
 
   138 | "L (STAR r) = (L r)\<star>"
 
   145 | "L (NOT r) = UNIV - (L r)"
 
   139 | "L (NOT r) = UNIV - (L r)"
 
   146 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 
   140 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 
   147 | "L (OPT r) = (L r) \<union> {[]}"
 
   141 | "L (OPT r) = (L r) \<union> {[]}"
 
   148 | "L (NTIMES r n) = (L r) \<up> n"
 
   142 | "L (NTIMES r n) = (L r) \<up> n"
 
   149 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
   143 | "L (BETWEEN r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
   150 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"
 
   144 | "L (UPTO r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"
 
   151 
   145 
   152 lemma "L (NOT NULL) = UNIV"
 
   146 lemma "L (NOT ZERO) = UNIV"
 
   153 apply(simp)
 
   147 apply(simp)
 
   154 done
 
   148 done
 
   155 
   149 
   156 section \<open>The Matcher\<close>
 
   150 section \<open>The Matcher\<close>
 
   157 
   151 
   158 fun
 
   152 fun
 
   159  nullable :: "rexp \<Rightarrow> bool"
 
   153  nullable :: "rexp \<Rightarrow> bool"
 
   160 where
 
   154 where
 
   161   "nullable (NULL) = False"
 
   155   "nullable (ZERO) = False"
 
   162 | "nullable (EMPTY) = True"
 
   156 | "nullable (ONE) = True"
 
   163 | "nullable (CH c) = False"
 
   157 | "nullable (CH c) = False"
 
   164 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
   158 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"
 
   165 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
   159 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"
 
   166 | "nullable (STAR r) = True"
 
   160 | "nullable (STAR r) = True"
 
   167 | "nullable (NOT r) = (\<not>(nullable r))"
 
   161 | "nullable (NOT r) = (\<not>(nullable r))"
 
   168 | "nullable (PLUS r) = (nullable r)"
 
   162 | "nullable (PLUS r) = (nullable r)"
 
   169 | "nullable (OPT r) = True"
 
   163 | "nullable (OPT r) = True"
 
   170 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 
   164 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 
   171 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
   165 | "nullable (BETWEEN r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
   172 | "nullable (UPNTIMES r n) = True"
 
   166 | "nullable (UPTO r n) = True"
 
   173 
   167 
   174 fun M :: "rexp \<Rightarrow> nat"
 
       
   175 where
 
       
   176   "M (NULL) = 0"
 
       
   177 | "M (EMPTY) = 0"
 
       
   178 | "M (CH char) = 0"
 
       
   179 | "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"
 
       
   180 | "M (ALT r1 r2) = Suc ((M r1) + (M r2))"
 
       
   181 | "M (STAR r) = Suc (M r)"
 
       
   182 | "M (NOT r) = Suc (M r)"
 
       
   183 | "M (PLUS r) = Suc (M r)"
 
       
   184 | "M (OPT r) = Suc (M r)"
 
       
   185 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
       
   186 | "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
 
       
   187 | "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
       
   188 
   168 
   189 fun der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   169 fun der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   190 where
 
   170 where
 
   191   "der c (NULL) = NULL"
 
   171   "der c (ZERO) = ZERO"
 
   192 | "der c (EMPTY) = NULL"
 
   172 | "der c (ONE) = ZERO"
 
   193 | "der c (CH d) = (if c = d then EMPTY else NULL)"
 
   173 | "der c (CH d) = (if c = d then ONE else ZERO)"
 
   194 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 
   174 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 
   195 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"
 
   175 | "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else ZERO)"
 
   196 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 
   176 | "der c (STAR r) = SEQ (der c r) (STAR r)"
 
   197 | "der c (NOT r) = NOT(der c r)"
 
   177 | "der c (NOT r) = NOT(der c r)"
 
   198 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 
   178 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 
   199 | "der c (OPT r) = der c r"
 
   179 | "der c (OPT r) = der c r"
 
   200 | "der c (NTIMES r n) = (if n = 0 then NULL else (SEQ (der c r) (NTIMES r (n - 1))))"
 
   180 | "der c (NTIMES r n) = (if n = 0 then ZERO else (SEQ (der c r) (NTIMES r (n - 1))))"
 
   201 | "der c (NMTIMES r n m) = 
   181 | "der c (BETWEEN r n m) = 
   202         (if m = 0 then NULL else 
   182         (if m = 0 then ZERO else 
   203         (if n = 0 then SEQ (der c r) (UPNTIMES r (m - 1))
 
   183         (if n = 0 then SEQ (der c r) (UPTO r (m - 1))
 
   204          else SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))"
 
   184          else SEQ (der c r) (BETWEEN r (n - 1) (m - 1))))"
 
   205 | "der c (UPNTIMES r n) = (if n = 0 then NULL else SEQ (der c r) (UPNTIMES r (n - 1)))"
 
   185 | "der c (UPTO r n) = (if n = 0 then ZERO else SEQ (der c r) (UPTO r (n - 1)))"
 
   206 
   186 
   207 fun 
   187 fun 
   208  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   188  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   209 where
 
   189 where
 
   210   "ders [] r = r"
 
   190   "ders [] r = r"
 
   285   apply(simp)
 
   265   apply(simp)
 
   286   apply(auto simp add: Der_def Seq_def)
 
   266   apply(auto simp add: Der_def Seq_def)
 
   287   apply blast
 
   267   apply blast
 
   288   by force
 
   268   by force
 
   289 
   269 
       
   270 
   290 lemma Der_ntimes [simp]:
 
   271 lemma Der_ntimes [simp]:
 
   291   shows "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
 
   272   shows "Der c (A  \<up> (Suc n)) = (Der c A) ;; (A \<up> n)"
 
   292 proof -    
   273 proof -    
   293   have "Der c (A  \<up> (Suc n)) = Der c (A ;; A \<up> n)"
 
   274   have "Der c (A  \<up> (Suc n)) = Der c (A ;; A \<up> n)"
 
   294     by(simp)
 
   275     by(simp)
 
   309 lemma Der_pow [simp]:
 
   290 lemma Der_pow [simp]:
 
   310   shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
 
   291   shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})"
 
   311 unfolding Der_def 
   292 unfolding Der_def 
   312 by(auto simp add: Cons_eq_append_conv Seq_def)
 
   293 by(auto simp add: Cons_eq_append_conv Seq_def)
 
   313 
   294 
       
   295 lemma concI_if_Nil2: "[] \<in> B \<Longrightarrow> xs \<in> A \<Longrightarrow> xs \<in> A ;; B"
 
       
   296   using Matcher2.Seq_def by auto
 
       
   297 
       
   298 lemma Der_pow2:
 
       
   299   shows "Der c (A \<up> n) = (if n = 0 then {} else (Der c A) ;; (A \<up> (n - 1)))"
 
       
   300   apply(induct n arbitrary: A)
 
       
   301   using Der_ntimes by auto
 
       
   302 
   314 
   303 
   315 lemma Der_UNION [simp]: 
   304 lemma Der_UNION [simp]: 
   316   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
 
   305   shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))"
 
   317   by (auto simp add: Der_def)
 
   306   by (auto simp add: Der_def)
 
   318 
   307 
   322 
   311 
   323 
   312 
   324 lemma der_correctness:
 
   313 lemma der_correctness:
 
   325   shows "L (der c r) = Der c (L r)"
 
   314   shows "L (der c r) = Der c (L r)"
 
   326 proof(induct r)
 
   315 proof(induct r)
 
   327   case NULL
 
   316   case ZERO
 
   328   then show ?case by simp
 
   317   then show ?case by simp
 
   329 next
 
   318 next
 
   330   case EMPTY
 
   319   case ONE
 
   331   then show ?case by simp
 
   320   then show ?case by simp
 
   332 next
 
   321 next
 
   333   case (CH x)
 
   322   case (CH x)
 
   334   then show ?case by simp
 
   323   then show ?case by simp
 
   335 next
 
   324 next
 
   357   then show ?case
 
   346   then show ?case
 
   358     apply(auto simp add: Seq_def)
 
   347     apply(auto simp add: Seq_def)
 
   359     using Der_ntimes Matcher2.Seq_def less_iff_Suc_add apply fastforce
 
   348     using Der_ntimes Matcher2.Seq_def less_iff_Suc_add apply fastforce
 
   360     using Der_ntimes Matcher2.Seq_def less_iff_Suc_add by auto
 
   349     using Der_ntimes Matcher2.Seq_def less_iff_Suc_add by auto
 
   361 next
 
   350 next
 
   362   case (NMTIMES r n m)
 
   351   case (BETWEEN r n m)
 
   363   then show ?case 
   352   then show ?case 
   364     apply(auto simp add: Seq_def)
 
   353     apply(auto simp add: Seq_def)
 
   365     sledgeham mer[timeout=1000]
 
   354     apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_pred atLeast0AtMost atMost_iff diff_Suc_Suc
 
   366     apply(case_tac n)
 
   355         diff_is_0_eq mem_Collect_eq)
 
   367     sorry
 
   356       apply(subst (asm) Der_pow2)
 
   368 next
 
   357       apply(case_tac xa)
 
   369   case (UPNTIMES r x2)
 
   358        apply(simp)
 
       
   359       apply(auto simp add: Seq_def)[1]
 
       
   360     apply (metis atMost_iff diff_Suc_1' diff_le_mono)
 
       
   361     apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atLeastAtMost_iff
 
       
   362         mem_Collect_eq)
 
       
   363     apply(subst (asm) Der_pow2)
 
       
   364       apply(case_tac xa)
 
       
   365        apply(simp)
 
       
   366     apply(auto simp add: Seq_def)[1]
 
       
   367     by force
 
       
   368 next
 
       
   369   case (UPTO r x2)
 
   370   then show ?case 
   370   then show ?case 
   371     apply(auto simp add: Seq_def)
 
   371     apply(auto simp add: Seq_def)
 
   372     apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atMost_iff
 
   372     apply (metis (mono_tags, lifting) Der_ntimes Matcher2.Seq_def Suc_le_mono Suc_pred atMost_iff
 
   373         mem_Collect_eq)
 
   373         mem_Collect_eq)
 
   374 sledgehammer[timeout=1000]
 
   374     apply(subst (asm) Der_pow2)
 
   375     sorry
 
   375     apply(case_tac xa)
 
   376 qed
 
   376      apply(simp)
 
   377 
   377     apply(auto simp add: Seq_def)
 
   378 
   378     by (metis atMost_iff diff_Suc_1' diff_le_mono)
 
   379 
       
   380 
       
   381 lemma der_correctness:
 
       
   382   shows "L (der c r) = Der c (L r)"
 
       
   383 apply(induct rule: der.induct) 
       
   384 apply(simp_all add: nullable_correctness 
       
   385     Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
 
       
   386 apply(rule impI)+
 
       
   387 apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
 
       
   388 apply(auto simp add: Seq_def)
 
       
   389 done
 
       
   390 
       
   391 lemma L_der_NTIMES:
 
       
   392   shows "L(der c (NTIMES r n)) = L (if n = 0 then NULL else if nullable r then 
       
   393          SEQ (der c r) (UPNTIMES r (n - 1)) else SEQ (der c r) (NTIMES r (n - 1)))"
 
       
   394 apply(induct n)
 
       
   395 apply(simp)
 
       
   396 apply(simp)
 
       
   397 apply(auto)
 
       
   398 apply(auto simp add: Seq_def)
 
       
   399 apply(rule_tac x="s1" in exI)
 
       
   400 apply(simp)
 
       
   401 apply(rule_tac x="xa" in bexI)
 
       
   402 apply(simp)
 
       
   403 apply(simp)
 
       
   404 apply(rule_tac x="s1" in exI)
 
       
   405 apply(simp)
 
       
   406 by (metis Suc_pred atMost_iff le_Suc_eq)
 
       
   407 
       
   408 lemma "L(der c (UPNTIMES r 0)) = {}"
 
       
   409 by simp
 
       
   410 
       
   411 lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
 
       
   412 proof(induct n)
 
       
   413   case 0 show ?case by simp
 
       
   414 next
 
       
   415   case (Suc n)
 
       
   416   have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact
 
       
   417   { assume a: "nullable r"
 
       
   418     have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
 
       
   419     by (simp only: der_correctness)
 
       
   420     also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
 
       
   421     by(simp only: L.simps Suc_Union)
 
       
   422     also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
 
       
   423     by (simp only: der_correctness)
 
       
   424     also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
 
       
   425     by(auto simp add: Seq_def)
 
       
   426     also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
 
       
   427     using IH by simp
 
       
   428     also have "... = L (SEQ (der c r) (UPNTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
 
       
   429     using a unfolding L_der_NTIMES by simp
 
       
   430     also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
 
       
   431     by (auto, metis Suc_Union Un_iff seq_Union)
 
       
   432     finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
 
       
   433     } 
       
   434   moreover
 
       
   435   { assume a: "\<not>nullable r"
 
       
   436     have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
 
       
   437     by (simp only: der_correctness)
 
       
   438     also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
 
       
   439     by(simp only: L.simps Suc_Union)
 
       
   440     also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
 
       
   441     by (simp only: der_correctness)
 
       
   442     also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
 
       
   443     by(auto simp add: Seq_def)
 
       
   444     also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
 
       
   445     using IH by simp
 
       
   446     also have "... = L (SEQ (der c r) (NTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
 
       
   447     using a unfolding L_der_NTIMES by simp
 
       
   448     also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
 
       
   449     by (simp add: Suc_Union seq_union(1))
 
       
   450     finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
 
       
   451   }
 
       
   452   ultimately  
       
   453   show "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))"
 
       
   454   by blast
 
       
   455 qed
 
   379 qed
 
   456 
   380 
   457 lemma matcher_correctness:
 
   381 lemma matcher_correctness:
 
   458   shows "matcher r s \<longleftrightarrow> s \<in> L r"
 
   382   shows "matcher r s \<longleftrightarrow> s \<in> L r"
 
   459 by (induct s arbitrary: r)
 
   383 by (induct s arbitrary: r)
afl-material