equal
deleted
inserted
replaced
79 (auto simp add: append_eq_Cons_conv) |
79 (auto simp add: append_eq_Cons_conv) |
80 |
80 |
81 lemma Der_star [simp]: |
81 lemma Der_star [simp]: |
82 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
82 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
83 proof - |
83 proof - |
84 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
84 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
85 |
|
86 by (simp only: star_cases[symmetric]) |
85 by (simp only: star_cases[symmetric]) |
87 also have "... = Der c (A ;; A\<star>)" |
86 also have "... = Der c (A ;; A\<star>)" |
88 by (simp only: Der_union Der_empty) (simp) |
87 by (simp only: Der_union Der_empty) (simp) |
89 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
88 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
90 by simp |
89 by simp |