equal
deleted
inserted
replaced
1 theory Folds |
1 theory Folds |
2 imports Main |
2 imports "Regular_Exp" |
3 begin |
3 begin |
4 |
4 |
5 section {* Folds for Sets *} |
5 section {* ``Summation'' for regular expressions *} |
6 |
6 |
7 text {* |
7 text {* |
8 To obtain equational system out of finite set of equivalence classes, a fold operation |
8 To obtain equational system out of finite set of equivalence classes, a fold operation |
9 on finite sets @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "folds"} |
9 on finite sets @{text "folds"} is defined. The use of @{text "SOME"} makes @{text "folds"} |
10 more robust than the @{text "fold"} in the Isabelle library. The expression @{text "folds f"} |
10 more robust than the @{text "fold"} in the Isabelle library. The expression @{text "folds f"} |
16 definition |
16 definition |
17 folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" |
17 folds :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b" |
18 where |
18 where |
19 "folds f z S \<equiv> SOME x. fold_graph f z S x" |
19 "folds f z S \<equiv> SOME x. fold_graph f z S x" |
20 |
20 |
|
21 text {* Plus-combination for a set of regular expressions *} |
|
22 |
|
23 abbreviation |
|
24 Setalt :: "'a rexp set \<Rightarrow> 'a rexp" ("\<Uplus>_" [1000] 999) |
|
25 where |
|
26 "\<Uplus>A \<equiv> folds Plus Zero A" |
|
27 |
|
28 text {* |
|
29 For finite sets, @{term Setalt} is preserved under @{term lang}. |
|
30 *} |
|
31 |
|
32 lemma folds_plus_simp [simp]: |
|
33 fixes rs::"('a rexp) set" |
|
34 assumes a: "finite rs" |
|
35 shows "lang (\<Uplus>rs) = \<Union> (lang ` rs)" |
|
36 unfolding folds_def |
|
37 apply(rule set_eqI) |
|
38 apply(rule someI2_ex) |
|
39 apply(rule_tac finite_imp_fold_graph[OF a]) |
|
40 apply(erule fold_graph.induct) |
|
41 apply(auto) |
|
42 done |
21 |
43 |
22 end |
44 end |