equal
deleted
inserted
replaced
1 theory Myhill |
1 theory Myhill |
2 imports Main List_Prefix Prefix_subtract |
2 imports Main List_Prefix Prefix_subtract Prelude |
3 begin |
3 begin |
4 |
4 |
5 (* |
5 (* |
6 text {* |
6 text {* |
7 \begin{figure} |
7 \begin{figure} |
190 The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"} |
190 The following lemma assures that the arbitrary choice made by the @{text "SOME"} in @{text "folds"} |
191 does not affect the @{text "L"}-value of the resultant regular expression. |
191 does not affect the @{text "L"}-value of the resultant regular expression. |
192 *} |
192 *} |
193 lemma folds_alt_simp [simp]: |
193 lemma folds_alt_simp [simp]: |
194 "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)" |
194 "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)" |
195 apply (rule set_ext, simp add:folds_def) |
195 apply (rule set_eq_intro, simp add:folds_def) |
196 apply (rule someI2_ex, erule finite_imp_fold_graph) |
196 apply (rule someI2_ex, erule finite_imp_fold_graph) |
197 by (erule fold_graph.induct, auto) |
197 by (erule fold_graph.induct, auto) |
198 |
198 |
199 (* Just a technical lemma. *) |
199 (* Just a technical lemma. *) |
200 lemma [simp]: |
200 lemma [simp]: |