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" |
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) |