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 362 57ea439feaff
parent 361 9c7eb266594c
child 363 0d6deecdb2eb
equal deleted inserted replaced
361:9c7eb266594c 362:57ea439feaff 
    22 | STAR rexp
 
    22 | STAR rexp
 
    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 | NMTIMES2 rexp nat nat
 
    27 | NMTIMES rexp nat nat
 
    28 (*
 
    28 
    29 fun M :: "rexp \<Rightarrow> nat"
 
    29 fun M :: "rexp \<Rightarrow> nat"
 
    30 where
 
    30 where
 
    31   "M (NULL) = 0"
 
    31   "M (NULL) = 0"
 
    32 | "M (EMPTY) = 0"
 
    32 | "M (EMPTY) = 0"
 
    33 | "M (CHAR char) = 0"
 
    33 | "M (CHAR char) = 0"
 
    36 | "M (STAR r) = Suc (M r)"
 
    36 | "M (STAR r) = Suc (M r)"
 
    37 | "M (NOT r) = Suc (M r)"
 
    37 | "M (NOT r) = Suc (M r)"
 
    38 | "M (PLUS r) = Suc (M r)"
 
    38 | "M (PLUS r) = Suc (M r)"
 
    39 | "M (OPT r) = Suc (M r)"
 
    39 | "M (OPT r) = Suc (M r)"
 
    40 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
    40 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
    41 | "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc m - Suc n)"
 
    41 | "M (NMTIMES r n m) = Suc (M r) * 2 * (Suc m - Suc n)"
 
    42 *)
 
    42 
    43 section {* Sequential Composition of Sets *}
 
    43 section {* Sequential Composition of Sets *}
 
    44 
    44 
    45 definition
 
    45 definition
 
    46   Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 
    46   Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 
    47 where 
    47 where 
   157 | "L (STAR r) = (L r)\<star>"
 
   157 | "L (STAR r) = (L r)\<star>"
 
   158 | "L (NOT r) = UNIV - (L r)"
 
   158 | "L (NOT r) = UNIV - (L r)"
 
   159 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 
   159 | "L (PLUS r) = (L r) ;; ((L r)\<star>)"
 
   160 | "L (OPT r) = (L r) \<union> {[]}"
 
   160 | "L (OPT r) = (L r) \<union> {[]}"
 
   161 | "L (NTIMES r n) = (L r) \<up> n"
 
   161 | "L (NTIMES r n) = (L r) \<up> n"
 
   162 | "L (NMTIMES2 r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
   162 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" 
   163 
   163 
   164 
   164 
   165 lemma "L (NOT NULL) = UNIV"
 
   165 lemma "L (NOT NULL) = UNIV"
 
   166 apply(simp)
 
   166 apply(simp)
 
   167 done
 
   167 done
 
   179 | "nullable (STAR r) = True"
 
   179 | "nullable (STAR r) = True"
 
   180 | "nullable (NOT r) = (\<not>(nullable r))"
 
   180 | "nullable (NOT r) = (\<not>(nullable r))"
 
   181 | "nullable (PLUS r) = (nullable r)"
 
   181 | "nullable (PLUS r) = (nullable r)"
 
   182 | "nullable (OPT r) = True"
 
   182 | "nullable (OPT r) = True"
 
   183 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 
   183 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)"
 
   184 | "nullable (NMTIMES2 r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
   184 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))"
 
   185 
       
   186 fun M :: "rexp \<Rightarrow> nat"
 
       
   187 where
 
       
   188   "M (NULL) = 0"
 
       
   189 | "M (EMPTY) = 0"
 
       
   190 | "M (CHAR char) = 0"
 
       
   191 | "M (SEQ r1 r2) = Suc ((M r1) + (M r2))"
 
       
   192 | "M (ALT r1 r2) = Suc ((M r1) + (M r2))"
 
       
   193 | "M (STAR r) = Suc (M r)"
 
       
   194 | "M (NOT r) = Suc (M r)"
 
       
   195 | "M (PLUS r) = Suc (M r)"
 
       
   196 | "M (OPT r) = Suc (M r)"
 
       
   197 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)"
 
       
   198 | "M (NMTIMES2 r n m) = 3 * (Suc (M r) + n) * 3 * (Suc n) * (Suc (Suc m) - (Suc n))"
 
       
   199 
   185 
   200 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   186 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 
   201 where
 
   187 where
 
   202   "der c (NULL) = NULL"
 
   188   "der c (NULL) = NULL"
 
   203 | "der c (EMPTY) = NULL"
 
   189 | "der c (EMPTY) = NULL"
 
   208 | "der c (NOT r) = NOT(der c r)"
 
   194 | "der c (NOT r) = NOT(der c r)"
 
   209 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 
   195 | "der c (PLUS r) = SEQ (der c r) (STAR r)"
 
   210 | "der c (OPT r) = der c r"
 
   196 | "der c (OPT r) = der c r"
 
   211 | "der c (NTIMES r 0) = NULL"
 
   197 | "der c (NTIMES r 0) = NULL"
 
   212 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
 
   198 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))"
 
   213 | "der c (NMTIMES2 r n m) = (if m < n then NULL else 
   199 | "der c (NMTIMES r n m) = (if m < n then NULL else 
   214                               (if n = m then der c (NTIMES r n) else
 
   200                               (if n = m then der c (NTIMES r n) else
 
   215                                 ALT (der c (NTIMES r n)) (der c (NMTIMES2 r (Suc n) m))))"
 
   201                                 ALT (der c (NTIMES r n)) (der c (NMTIMES r (Suc n) m))))"
 
   216 by pat_completeness auto
 
   202 by pat_completeness auto
 
   217 
   203 
   218 termination der 
   204 termination der 
   219 apply(relation "measure (\<lambda>(c, r). M r)") 
   205 apply(relation "measure (\<lambda>(c, r). M r)") 
   220 apply(simp_all)
 
   206 apply(simp_all)
afl-material