37 | "M (STAR r) = Suc (M r)" |
36 | "M (STAR r) = Suc (M r)" |
38 | "M (NOT r) = Suc (M r)" |
37 | "M (NOT r) = Suc (M r)" |
39 | "M (PLUS r) = Suc (M r)" |
38 | "M (PLUS r) = Suc (M r)" |
40 | "M (OPT r) = Suc (M r)" |
39 | "M (OPT r) = Suc (M r)" |
41 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)" |
40 | "M (NTIMES r n) = Suc (M r) * 2 * (Suc n)" |
42 | "M (NMTIMES r n m) = Suc (M r) * 2 * (Suc n + Suc m)" |
41 | "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc m - Suc n)" |
43 | "M (NMTIMES2 r n m) = Suc (M r) * 2 * (Suc n + Suc m)" |
42 *) |
44 |
|
45 section {* Sequential Composition of Sets *} |
43 section {* Sequential Composition of Sets *} |
46 |
44 |
47 definition |
45 definition |
48 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) |
49 where |
47 where |
159 | "L (STAR r) = (L r)\<star>" |
157 | "L (STAR r) = (L r)\<star>" |
160 | "L (NOT r) = UNIV - (L r)" |
158 | "L (NOT r) = UNIV - (L r)" |
161 | "L (PLUS r) = (L r) ;; ((L r)\<star>)" |
159 | "L (PLUS r) = (L r) ;; ((L r)\<star>)" |
162 | "L (OPT r) = (L r) \<union> {[]}" |
160 | "L (OPT r) = (L r) \<union> {[]}" |
163 | "L (NTIMES r n) = (L r) \<up> n" |
161 | "L (NTIMES r n) = (L r) \<up> n" |
164 | "L (NMTIMES r n m) = (\<Union>i\<in> {n..n+m} . ((L r) \<up> i))" |
|
165 | "L (NMTIMES2 r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" |
162 | "L (NMTIMES2 r n m) = (\<Union>i\<in> {n..m} . ((L r) \<up> i))" |
166 |
163 |
167 |
164 |
168 lemma "L (NOT NULL) = UNIV" |
165 lemma "L (NOT NULL) = UNIV" |
169 apply(simp) |
166 apply(simp) |
170 done |
167 done |
171 |
|
172 lemma "L (NMTIMES r (Suc n) m) = L (SEQ r (NMTIMES r n m))" |
|
173 apply(simp add: Suc_reduce_Union Seq_def) |
|
174 apply(auto) |
|
175 done |
|
176 |
|
177 lemma "L (NMTIMES2 r (Suc n) (Suc m)) = L (SEQ r (NMTIMES2 r n m))" |
|
178 apply(simp add: Suc_reduce_Union Seq_def) |
|
179 apply(auto) |
|
180 done |
|
181 |
|
182 lemma "L (NMTIMES2 r 0 0) = {[]}" |
|
183 apply(simp add: Suc_reduce_Union Seq_def) |
|
184 done |
|
185 |
|
186 lemma t: "\<lbrakk>n \<le> i; i \<le> m\<rbrakk> \<Longrightarrow> L (NMTIMES2 r n m) = L (NMTIMES2 r n i) \<union> L (NMTIMES2 r i m)" |
|
187 apply(auto) |
|
188 apply (metis atLeastAtMost_iff nat_le_linear) |
|
189 apply (metis atLeastAtMost_iff le_trans) |
|
190 by (metis atLeastAtMost_iff le_trans) |
|
191 |
|
192 |
|
193 lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \<union> L (NMTIMES2 r 1 (Suc m))" |
|
194 apply(rule t) |
|
195 apply(auto) |
|
196 done |
|
197 |
|
198 lemma "L (NMTIMES2 r 0 (Suc m)) = L (NMTIMES2 r 0 1) \<union> L (NMTIMES2 r 1 (Suc m))" |
|
199 apply(rule t) |
|
200 apply(auto) |
|
201 done |
|
202 |
|
203 lemma "L (NMTIMES2 r 0 1) = {[]} \<union> L r" |
|
204 apply(simp) |
|
205 apply(auto) |
|
206 apply(case_tac xa) |
|
207 apply(auto) |
|
208 done |
|
209 |
|
210 |
|
211 lemma "L (NMTIMES2 r n n) = L (NTIMES r n)" |
|
212 apply(simp) |
|
213 done |
|
214 |
|
215 lemma "n < m \<Longrightarrow> L (NMTIMES2 r n m) = L (NTIMES r n) \<union> L (NMTIMES2 r (Suc n) m)" |
|
216 apply(simp) |
|
217 apply(auto) |
|
218 apply (metis Suc_leI atLeastAtMost_iff le_eq_less_or_eq) |
|
219 apply (metis atLeastAtMost_iff le_eq_less_or_eq) |
|
220 by (metis Suc_leD atLeastAtMost_iff) |
|
221 |
168 |
222 section {* The Matcher *} |
169 section {* The Matcher *} |
223 |
170 |
224 fun |
171 fun |
225 nullable :: "rexp \<Rightarrow> bool" |
172 nullable :: "rexp \<Rightarrow> bool" |
232 | "nullable (STAR r) = True" |
179 | "nullable (STAR r) = True" |
233 | "nullable (NOT r) = (\<not>(nullable r))" |
180 | "nullable (NOT r) = (\<not>(nullable r))" |
234 | "nullable (PLUS r) = (nullable r)" |
181 | "nullable (PLUS r) = (nullable r)" |
235 | "nullable (OPT r) = True" |
182 | "nullable (OPT r) = True" |
236 | "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)" |
237 | "nullable (NMTIMES r n m) = (if n = 0 then True else nullable r)" |
|
238 | "nullable (NMTIMES2 r n m) = (if m < n then False else (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))" |
239 |
185 |
240 function |
186 fun M :: "rexp \<Rightarrow> nat" |
241 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
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 |
|
200 function der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
242 where |
201 where |
243 "der c (NULL) = NULL" |
202 "der c (NULL) = NULL" |
244 | "der c (EMPTY) = NULL" |
203 | "der c (EMPTY) = NULL" |
245 | "der c (CHAR d) = (if c = d then EMPTY else NULL)" |
204 | "der c (CHAR d) = (if c = d then EMPTY else NULL)" |
246 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
205 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
249 | "der c (NOT r) = NOT(der c r)" |
208 | "der c (NOT r) = NOT(der c r)" |
250 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
209 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
251 | "der c (OPT r) = der c r" |
210 | "der c (OPT r) = der c r" |
252 | "der c (NTIMES r 0) = NULL" |
211 | "der c (NTIMES r 0) = NULL" |
253 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))" |
212 | "der c (NTIMES r (Suc n)) = der c (SEQ r (NTIMES r n))" |
254 | "der c (NMTIMES r 0 0) = NULL" |
|
255 | "der c (NMTIMES r 0 (Suc m)) = ALT (der c (NTIMES r (Suc m))) (der c (NMTIMES r 0 m))" |
|
256 | "der c (NMTIMES r (Suc n) m) = der c (SEQ r (NMTIMES r n m))" |
|
257 | "der c (NMTIMES2 r n m) = (if m < n then NULL else |
213 | "der c (NMTIMES2 r n m) = (if m < n then NULL else |
258 (if n = m then der c (NTIMES r n) else |
214 (if n = m then der c (NTIMES r n) else |
259 ALT (der c (NTIMES r n)) (der c (NMTIMES2 r (Suc n) m))))" |
215 ALT (der c (NTIMES r n)) (der c (NMTIMES2 r (Suc n) m))))" |
260 by pat_completeness auto |
216 by pat_completeness auto |
261 |
217 |
262 termination der |
218 termination der |
|
219 apply(relation "measure (\<lambda>(c, r). M r)") |
|
220 apply(simp_all) |
263 sorry |
221 sorry |
264 (*by (relation "measure (\<lambda>(c, r). M r)") (simp_all)*) |
222 |
265 |
223 |
266 |
224 |
267 fun |
225 fun |
268 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
226 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
269 where |
227 where |