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 455 1dbf84ade62c
parent 397 cf3ca219c727
child 456 2fddf8ab744f
equal deleted inserted replaced
454:edb4ad356c56 455:1dbf84ade62c 
    23 | NOT rexp
 
    23 | NOT rexp
 
    24 | PLUS rexp
 
    24 | PLUS rexp
 
    25 | OPT rexp
 
    25 | OPT rexp
 
    26 | NTIMES rexp nat
 
    26 | NTIMES rexp nat
 
    27 | NMTIMES rexp nat nat
 
    27 | NMTIMES rexp nat nat
 
       
    28 | UPNTIMES rexp nat
 
    28 
    29 
    29 
    30 
    30 section {* Sequential Composition of Sets *}
 
    31 section {* Sequential Composition of Sets *}
 
    31 
    32 
    32 definition
 
    33 definition
 
   145 | "L (NOT r) = UNIV - (L r)"
 
   146 | "L (NOT r) = UNIV - (L r)"
 
   146 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 
   147 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 
   147 | "L (OPT r) = (L r) \<union> {[]}"
 
   148 | "L (OPT r) = (L r) \<union> {[]}"
 
   148 | "L (NTIMES r n) = (L r) \<up> n"
 
   149 | "L (NTIMES r n) = (L r) \<up> n"
 
   149 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
   150 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
   150 
   151 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . ((L r) \<up> i))"
 
   151 
   152 
   152 lemma "L (NOT NULL) = UNIV"
 
   153 lemma "L (NOT NULL) = UNIV"
 
   153 apply(simp)
 
   154 apply(simp)
 
   154 done
 
   155 done
 
   155 
   156 
   167 | "nullable (NOT r) = (\<not>(nullable r))"
 
   168 | "nullable (NOT r) = (\<not>(nullable r))"
 
   168 | "nullable (PLUS r) = (nullable r)"
 
   169 | "nullable (PLUS r) = (nullable r)"
 
   169 | "nullable (OPT r) = True"
 
   170 | "nullable (OPT r) = True"
 
   170 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 
   171 | "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))"
 
   172 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
       
   173 | "nullable (UPNTIMES r n) = True"
 
   172 
   174 
   173 fun M :: "rexp \<Rightarrow> nat"
 
   175 fun M :: "rexp \<Rightarrow> nat"
 
   174 where
 
   176 where
 
   175   "M (NULL) = 0"
 
   177   "M (NULL) = 0"
 
   176 | "M (EMPTY) = 0"
 
   178 | "M (EMPTY) = 0"
 
   181 | "M (NOT r) = Suc (M r)"
 
   183 | "M (NOT r) = Suc (M r)"
 
   182 | "M (PLUS r) = Suc (M r)"
 
   184 | "M (PLUS r) = Suc (M r)"
 
   183 | "M (OPT r) = Suc (M r)"
 
   185 | "M (OPT r) = Suc (M r)"
 
   184 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
   186 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
   185 | "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
 
   187 | "M (NMTIMES r n m) = Suc (Suc (M r)) * 2 * (Suc m) * (Suc (Suc m) - Suc n)"
 
   186 
   188 | "M (UPNTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
   187 
   189 
   188 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   190 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   189 where
 
   191 where
 
   190   "der c (NULL) = NULL"
 
   192   "der c (NULL) = NULL"
 
   191 | "der c (EMPTY) = NULL"
 
   193 | "der c (EMPTY) = NULL"
 
   200 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
 
   202 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
 
   201 | "der c (NMTIMES r n m) = 
   203 | "der c (NMTIMES r n m) = 
   202         (if m < n then NULL else 
   204         (if m < n then NULL else 
   203         (if n = m then der c (NTIMES r n) else
 
   205         (if n = m then der c (NTIMES r n) else
 
   204                        ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
 
   206                        ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
 
       
   207 | "der c (UPNTIMES r 0) = NULL"
 
       
   208 | "der c (UPNTIMES r (Suc n)) = der c (ALT (NTIMES r (Suc n)) (UPNTIMES r n))"
 
   205 by pat_completeness auto
 
   209 by pat_completeness auto
 
   206 
   210 
   207 lemma bigger1:
 
   211 lemma bigger1:
 
   208   "\<lbrakk>c < (d::nat); a < b; 0 < a; 0 < c\<rbrakk> \<Longrightarrow> c * a < d * b"
 
   212   "\<lbrakk>c < (d::nat); a < b; 0 < a; 0 < c\<rbrakk> \<Longrightarrow> c * a < d * b"
 
   209 by (metis le0 mult_strict_mono')
 
   213 by (metis le0 mult_strict_mono')
 
   221 apply(simp)
 
   225 apply(simp)
 
   222 apply(simp)
 
   226 apply(simp)
 
   223 apply(simp)
 
   227 apply(simp)
 
   224 apply(simp_all del: M.simps)
 
   228 apply(simp_all del: M.simps)
 
   225 apply(simp_all only: M.simps)
 
   229 apply(simp_all only: M.simps)
 
       
   230 defer
 
       
   231 defer
 
   226 defer
 
   232 defer
 
   227 apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
 
   233 apply(subgoal_tac "Suc (Suc m) - Suc (Suc n) < Suc (Suc m) - Suc n")
 
   228 prefer 2
 
   234 prefer 2
 
   229 apply(auto)[1]
 
   235 apply(auto)[1]
 
       
   236 (*
 
   230 apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
 
   237 apply (metis Suc_mult_less_cancel1 mult.assoc numeral_eq_Suc)
 
   231 apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
 
   238 apply(subgoal_tac "0 < (Suc (Suc m) - Suc n)")
 
   232 prefer 2
 
   239 prefer 2
 
   233 apply(auto)[1]
 
   240 apply(auto)[1]
 
   234 apply(subgoal_tac "Suc n < Suc m")
 
   241 apply(subgoal_tac "Suc n < Suc m")
 
   250 apply(simp)
 
   257 apply(simp)
 
   251 apply(simp)
 
   258 apply(simp)
 
   252 apply (metis zero_less_one)
 
   259 apply (metis zero_less_one)
 
   253 apply(simp)
 
   260 apply(simp)
 
   254 done
 
   261 done
 
       
   262 *)
 
       
   263 sorry
 
   255 
   264 
   256 fun 
   265 fun 
   257  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   266  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"
 
   258 where
 
   267 where
 
   259   "ders [] r = r"
 
   268   "ders [] r = r"
 
   344 apply(induct rule: der.induct) 
   353 apply(induct rule: der.induct) 
   345 apply(simp_all add: nullable_correctness 
   354 apply(simp_all add: nullable_correctness 
   346     Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
 
   355     Suc_Union Suc_reduce_Union seq_Union atLeast0AtMost)
 
   347 apply(rule impI)+
 
   356 apply(rule impI)+
 
   348 apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
 
   357 apply(subgoal_tac "{n..m} = {n} \<union> {Suc n..m}")
 
       
   358 apply(auto simp add: Seq_def)
 
       
   359 done
 
       
   360 
       
   361 lemma L_der_NTIMES:
 
       
   362   shows "L(der c (NTIMES r n)) = (if n = 0 then {} else if nullable r then 
       
   363        L(SEQ (der c r) (UPNTIMES r (n - 1)))
 
       
   364        else L(SEQ (der c r) (NTIMES r (n - 1))))"
 
       
   365 apply(induct n)
 
       
   366 apply(simp)
 
       
   367 apply(simp)
 
   349 apply(auto)
 
   368 apply(auto)
 
   350 done
 
   369 apply(auto simp add: Seq_def)
 
       
   370 apply(rule_tac x="s1" in exI)
 
       
   371 apply(simp)
 
       
   372 apply(rule_tac x="xa" in bexI)
 
       
   373 apply(simp)
 
       
   374 apply(simp)
 
       
   375 apply(rule_tac x="s1" in exI)
 
       
   376 apply(simp)
 
       
   377 by (metis Suc_pred atMost_iff le_Suc_eq)
 
       
   378 
       
   379 lemma "L(der c (UPNTIMES r (Suc n))) = L(SEQ (der c r) (UPNTIMES r n))"
 
       
   380 using assms
 
       
   381 proof(induct n)
 
       
   382   case 0 show ?case by simp
 
       
   383 next
 
       
   384   case (Suc n)
 
       
   385   have IH: "L (der c (UPNTIMES r (Suc n))) = L (SEQ (der c r) (UPNTIMES r n))" by fact
 
       
   386   { assume a: "nullable r"
 
       
   387     have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
 
       
   388     by (simp only: der_correctness)
 
       
   389     also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
 
       
   390     by(simp only: L.simps Suc_Union)
 
       
   391     also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
 
       
   392     by (simp only: der_correctness)
 
       
   393     also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
 
       
   394     by(auto simp add: Seq_def)
 
       
   395     also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
 
       
   396     using IH by simp
 
       
   397     also have "... = L (SEQ (der c r) (UPNTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
 
       
   398     using a unfolding L_der_NTIMES by simp
 
       
   399     also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
 
       
   400     by (auto, metis Suc_Union Un_iff seq_Union)
 
       
   401     finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
 
       
   402     } 
       
   403   moreover
 
       
   404   { assume a: "\<not>nullable r"
 
       
   405     have "L (der c (UPNTIMES r (Suc (Suc n)))) = Der c (L (UPNTIMES r (Suc (Suc n))))"
 
       
   406     by (simp only: der_correctness)
 
       
   407     also have "... = Der c (L (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
 
       
   408     by(simp only: L.simps Suc_Union)
 
       
   409     also have "... = L (der c (ALT (NTIMES r (Suc (Suc n))) (UPNTIMES r (Suc n))))"
 
       
   410     by (simp only: der_correctness)
 
       
   411     also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (der c (UPNTIMES r (Suc n)))"
 
       
   412     by(auto simp add: Seq_def)
 
       
   413     also have "... = L (der c (NTIMES r (Suc (Suc n)))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
 
       
   414     using IH by simp
 
       
   415     also have "... = L (SEQ (der c r) (NTIMES r (Suc n))) \<union> L (SEQ (der c r) (UPNTIMES r n))"
 
       
   416     using a unfolding L_der_NTIMES by simp
 
       
   417     also have "... =  L (SEQ (der c r) (UPNTIMES r (Suc n)))"
 
       
   418     by (simp add: Suc_Union seq_union(1))
 
       
   419     finally have "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))" .
 
       
   420   }
 
       
   421   ultimately  
       
   422   show "L (der c (UPNTIMES r (Suc (Suc n)))) = L (SEQ (der c r) (UPNTIMES r (Suc n)))"
 
       
   423   by blast
 
       
   424 qed
 
   351 
   425 
   352 lemma matcher_correctness:
 
   426 lemma matcher_correctness:
 
   353   shows "matcher r s \<longleftrightarrow> s \<in> L r"
 
   427   shows "matcher r s \<longleftrightarrow> s \<in> L r"
 
   354 by (induct s arbitrary: r)
 
   428 by (induct s arbitrary: r)
 
   355    (simp_all add: nullable_correctness der_correctness Der_def)
 
   429    (simp_all add: nullable_correctness der_correctness Der_def)
afl-material