equal
deleted
inserted
replaced
82 assumes a: "c # x \<in> A\<star>" |
82 assumes a: "c # x \<in> A\<star>" |
83 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
83 shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>" |
84 using a |
84 using a |
85 by (induct x\<equiv>"c # x" rule: Star.induct) |
85 by (induct x\<equiv>"c # x" rule: Star.induct) |
86 (auto simp add: append_eq_Cons_conv) |
86 (auto simp add: append_eq_Cons_conv) |
|
87 |
|
88 lemma Star_Der_Sequ: |
|
89 shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>" |
|
90 unfolding Der_def |
|
91 by(auto simp add: Der_def Sequ_def Star_decomp) |
|
92 |
|
93 |
87 |
94 |
88 lemma Der_star [simp]: |
95 lemma Der_star [simp]: |
89 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
96 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
90 proof - |
97 proof - |
91 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
98 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
93 also have "... = Der c (A ;; A\<star>)" |
100 also have "... = Der c (A ;; A\<star>)" |
94 by (simp only: Der_union Der_empty) (simp) |
101 by (simp only: Der_union Der_empty) (simp) |
95 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
102 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
96 by simp |
103 by simp |
97 also have "... = (Der c A) ;; A\<star>" |
104 also have "... = (Der c A) ;; A\<star>" |
98 unfolding Sequ_def Der_def |
105 using Star_Der_Sequ by auto |
99 by (auto dest: Star_decomp) |
|
100 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
106 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
101 qed |
107 qed |
102 |
108 |
103 |
109 |
104 section {* Regular Expressions *} |
110 section {* Regular Expressions *} |