equal
deleted
inserted
replaced
64 apply(auto) |
64 apply(auto) |
65 apply(drule star_decom) |
65 apply(drule star_decom) |
66 apply(auto simp add: Cons_eq_append_conv) |
66 apply(auto simp add: Cons_eq_append_conv) |
67 done |
67 done |
68 |
68 |
69 have "Der c (A\<star>) = Der c ({[]} \<union> A \<cdot> A\<star>)" |
69 have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})" |
70 by (simp only: star_cases[symmetric]) |
70 by (simp only: star_unfold_left[symmetric]) |
71 also have "... = Der c (A \<cdot> A\<star>)" |
71 also have "... = Der c (A \<cdot> A\<star>)" |
72 by (simp only: Der_union Der_one) (simp) |
72 by (simp only: Der_union Der_one) (simp) |
73 also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))" |
73 also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))" |
74 by simp |
74 by simp |
75 also have "... = (Der c A) \<cdot> A\<star>" |
75 also have "... = (Der c A) \<cdot> A\<star>" |
155 |
155 |
156 fun |
156 fun |
157 pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
157 pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
158 where |
158 where |
159 "pders [] r = {r}" |
159 "pders [] r = {r}" |
160 | "pders (c # s) r = (\<Union>r'\<in> (pder c r). (pders s r'))" |
160 | "pders (c # s) r = \<Union> (pders s) ` (pder c r)" |
161 |
161 |
162 abbreviation |
162 abbreviation |
163 "pders_set A r \<equiv> \<Union>s \<in> A. pders s r" |
163 "pders_set A r \<equiv> \<Union>s \<in> A. pders s r" |
164 |
164 |
165 lemma pders_append: |
165 lemma pders_append: |