318 more robust than the @{text "fold"} in the Isabelle library. The expression @{text "folds f"} |
318 more robust than the @{text "fold"} in the Isabelle library. The expression @{text "folds f"} |
319 makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"}, |
319 makes sense when @{text "f"} is not @{text "associative"} and @{text "commutitive"}, |
320 while @{text "fold f"} does not. |
320 while @{text "fold f"} does not. |
321 *} |
321 *} |
322 |
322 |
|
323 |
323 definition |
324 definition |
324 folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" |
325 folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" |
325 where |
326 where |
326 "folds f z S \<equiv> SOME x. fold_graph f z S x" |
327 "folds f z S \<equiv> SOME x. fold_graph f z S x" |
|
328 |
|
329 abbreviation |
|
330 Setalt ("\<Uplus>_" [1000] 999) |
|
331 where |
|
332 "\<Uplus>A == folds ALT NULL A" |
327 |
333 |
328 text {* |
334 text {* |
329 The following lemma ensures that the arbitrary choice made by the |
335 The following lemma ensures that the arbitrary choice made by the |
330 @{text "SOME"} in @{text "folds"} does not affect the @{text "L"}-value |
336 @{text "SOME"} in @{text "folds"} does not affect the @{text "L"}-value |
331 of the resultant regular expression. |
337 of the resultant regular expression. |
332 *} |
338 *} |
333 |
339 |
334 lemma folds_alt_simp [simp]: |
340 lemma folds_alt_simp [simp]: |
335 assumes a: "finite rs" |
341 assumes a: "finite rs" |
336 shows "L (folds ALT NULL rs) = \<Union> (L ` rs)" |
342 shows "L (\<Uplus>rs) = \<Union> (L ` rs)" |
337 apply(rule set_eqI) |
343 apply(rule set_eqI) |
338 apply(simp add: folds_def) |
344 apply(simp add: folds_def) |
339 apply(rule someI2_ex) |
345 apply(rule someI2_ex) |
340 apply(rule_tac finite_imp_fold_graph[OF a]) |
346 apply(rule_tac finite_imp_fold_graph[OF a]) |
341 apply(erule fold_graph.induct) |
347 apply(erule fold_graph.induct) |
380 apply(auto) |
386 apply(auto) |
381 apply(drule_tac x = "[]" in spec) |
387 apply(drule_tac x = "[]" in spec) |
382 apply(auto) |
388 apply(auto) |
383 done |
389 done |
384 |
390 |
|
391 lemma finals_included_in_UNIV: |
|
392 shows "finals A \<subseteq> UNIV // \<approx>A" |
|
393 unfolding finals_def |
|
394 unfolding quotient_def |
|
395 by auto |
|
396 |
385 |
397 |
386 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*} |
398 section {* Direction @{text "finite partition \<Rightarrow> regular language"}*} |
387 |
399 |
388 text {* |
400 text {* |
389 The relationship between equivalent classes can be described by an |
401 The relationship between equivalent classes can be described by an |
513 using @{text "ALT"} to form a single regular expression. |
525 using @{text "ALT"} to form a single regular expression. |
514 It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}. |
526 It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}. |
515 *} |
527 *} |
516 |
528 |
517 definition |
529 definition |
518 "rexp_of rhs X \<equiv> folds ALT NULL ((snd o the_Trn) ` items_of rhs X)" |
530 "rexp_of rhs X \<equiv> \<Uplus>((snd o the_Trn) ` items_of rhs X)" |
519 |
531 |
520 text {* |
532 text {* |
521 The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}. |
533 The following @{text "lam_of rhs"} returns all pure regular expression items in @{text "rhs"}. |
522 *} |
534 *} |
523 |
535 |
529 using @{text "ALT"} to form a single regular expression. |
541 using @{text "ALT"} to form a single regular expression. |
530 When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"} |
542 When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"} |
531 is used to compute compute the regular expression corresponds to @{text "rhs"}. |
543 is used to compute compute the regular expression corresponds to @{text "rhs"}. |
532 *} |
544 *} |
533 |
545 |
|
546 |
534 definition |
547 definition |
535 "rexp_of_lam rhs \<equiv> folds ALT NULL (the_r ` lam_of rhs)" |
548 "rexp_of_lam rhs \<equiv> \<Uplus>(the_r ` lam_of rhs)" |
536 |
549 |
537 text {* |
550 text {* |
538 The following @{text "attach_rexp rexp' itm"} attach |
551 The following @{text "attach_rexp rexp' itm"} attach |
539 the regular expression @{text "rexp'"} to |
552 the regular expression @{text "rexp'"} to |
540 the right of right hand side item @{text "itm"}. |
553 the right of right hand side item @{text "itm"}. |
1280 then obtain f |
1293 then obtain f |
1281 where f_prop: "\<forall> X \<in> (UNIV // \<approx>A). X = L ((f X)::rexp)" |
1294 where f_prop: "\<forall> X \<in> (UNIV // \<approx>A). X = L ((f X)::rexp)" |
1282 by (auto dest: bchoice) |
1295 by (auto dest: bchoice) |
1283 def rs \<equiv> "f ` (finals A)" |
1296 def rs \<equiv> "f ` (finals A)" |
1284 have "A = \<Union> (finals A)" using lang_is_union_of_finals by auto |
1297 have "A = \<Union> (finals A)" using lang_is_union_of_finals by auto |
1285 also have "\<dots> = L (folds ALT NULL rs)" |
1298 also have "\<dots> = L (\<Uplus>rs)" |
1286 proof - |
1299 proof - |
1287 have "finite rs" |
1300 have "finite rs" |
1288 proof - |
1301 proof - |
1289 have "finite (finals A)" |
1302 have "finite (finals A)" |
1290 using finite_CS finals_in_partitions[of "A"] |
1303 using finite_CS finals_in_partitions[of "A"] |