19 definition |
19 definition |
20 Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
20 Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
21 where |
21 where |
22 "Ders s A \<equiv> {s'. s @ s' \<in> A}" |
22 "Ders s A \<equiv> {s'. s @ s' \<in> A}" |
23 |
23 |
24 definition |
24 abbreviation |
25 Ders_set :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" |
25 "Derss s A \<equiv> \<Union> (Ders s) ` A" |
26 where |
26 |
27 "Ders_set A B \<equiv> {s' | s s'. s @ s' \<in> B \<and> s \<in> A}" |
27 lemma Der_simps [simp]: |
28 |
|
29 lemma Ders_set_Ders: |
|
30 shows "Ders_set A B = (\<Union>s \<in> A. Ders s B)" |
|
31 unfolding Ders_set_def Ders_def |
|
32 by auto |
|
33 |
|
34 lemma Der_zero [simp]: |
|
35 shows "Der c {} = {}" |
28 shows "Der c {} = {}" |
36 unfolding Der_def |
29 and "Der c {[]} = {}" |
37 by auto |
30 and "Der c {[d]} = (if c = d then {[]} else {})" |
38 |
31 and "Der c (A \<union> B) = Der c A \<union> Der c B" |
39 lemma Der_one [simp]: |
32 unfolding Der_def by auto |
40 shows "Der c {[]} = {}" |
|
41 unfolding Der_def |
|
42 by auto |
|
43 |
|
44 lemma Der_atom [simp]: |
|
45 shows "Der c {[d]} = (if c = d then {[]} else {})" |
|
46 unfolding Der_def |
|
47 by auto |
|
48 |
|
49 lemma Der_union [simp]: |
|
50 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
|
51 unfolding Der_def |
|
52 by auto |
|
53 |
33 |
54 lemma Der_conc [simp]: |
34 lemma Der_conc [simp]: |
55 shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)" |
35 shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)" |
56 unfolding Der_def Delta_def conc_def |
36 unfolding Der_def Delta_def conc_def |
57 by (auto simp add: Cons_eq_append_conv) |
37 by (auto simp add: Cons_eq_append_conv) |
58 |
38 |
59 lemma Der_star [simp]: |
39 lemma Der_star [simp]: |
60 shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" |
40 shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" |
61 proof - |
41 proof - |
62 have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>" |
42 have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>" |
63 unfolding Der_def Delta_def |
43 unfolding Der_def Delta_def conc_def |
64 apply(auto) |
44 apply(auto) |
65 apply(drule star_decom) |
45 apply(drule star_decom) |
66 apply(auto simp add: Cons_eq_append_conv) |
46 apply(auto simp add: Cons_eq_append_conv) |
67 done |
47 done |
68 |
48 |
69 have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})" |
49 have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})" |
70 by (simp only: star_unfold_left[symmetric]) |
50 by (simp only: star_unfold_left[symmetric]) |
71 also have "... = Der c (A \<cdot> A\<star>)" |
51 also have "... = Der c (A \<cdot> A\<star>)" |
72 by (simp only: Der_union Der_one) (simp) |
52 by (simp only: Der_simps) (simp) |
73 also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))" |
53 also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))" |
74 by simp |
54 by simp |
75 also have "... = (Der c A) \<cdot> A\<star>" |
55 also have "... = (Der c A) \<cdot> A\<star>" |
76 using incl by auto |
56 using incl by auto |
77 finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . |
57 finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . |
78 qed |
58 qed |
79 |
59 |
80 lemma Ders_nil [simp]: |
60 lemma Ders_simps [simp]: |
81 shows "Ders [] A = A" |
61 shows "Ders [] A = A" |
82 unfolding Ders_def by simp |
62 and "Ders (c # s) A = Ders s (Der c A)" |
83 |
63 and "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)" |
84 lemma Ders_cons [simp]: |
|
85 shows "Ders (c # s) A = Ders s (Der c A)" |
|
86 unfolding Ders_def Der_def by auto |
64 unfolding Ders_def Der_def by auto |
87 |
|
88 lemma Ders_append [simp]: |
|
89 shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)" |
|
90 unfolding Ders_def by simp |
|
91 |
|
92 |
65 |
93 subsection {* Brozowsky's derivatives of regular expressions *} |
66 subsection {* Brozowsky's derivatives of regular expressions *} |
94 |
67 |
95 fun |
68 fun |
96 nullable :: "'a rexp \<Rightarrow> bool" |
69 nullable :: "'a rexp \<Rightarrow> bool" |
135 |
108 |
136 |
109 |
137 subsection {* Antimirov's Partial Derivatives *} |
110 subsection {* Antimirov's Partial Derivatives *} |
138 |
111 |
139 abbreviation |
112 abbreviation |
140 "Times_set rs r \<equiv> {Times r' r | r'. r' \<in> rs}" |
113 "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}" |
141 |
114 |
142 fun |
115 fun |
143 pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
116 pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
144 where |
117 where |
145 "pder c Zero = {Zero}" |
118 "pder c Zero = {Zero}" |
146 | "pder c One = {Zero}" |
119 | "pder c One = {Zero}" |
147 | "pder c (Atom c') = (if c = c' then {One} else {Zero})" |
120 | "pder c (Atom c') = (if c = c' then {One} else {Zero})" |
148 | "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)" |
121 | "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)" |
149 | "pder c (Times r1 r2) = |
122 | "pder c (Times r1 r2) = |
150 (if nullable r1 then Times_set (pder c r1) r2 \<union> pder c r2 else Times_set (pder c r1) r2)" |
123 (if nullable r1 then Timess (pder c r1) r2 \<union> pder c r2 else Timess (pder c r1) r2)" |
151 | "pder c (Star r) = Times_set (pder c r) (Star r)" |
124 | "pder c (Star r) = Timess (pder c r) (Star r)" |
152 |
125 |
153 abbreviation |
126 abbreviation |
154 "pder_set c rs \<equiv> \<Union>r \<in> rs. pder c r" |
127 "pder_set c rs \<equiv> \<Union> pder c ` rs" |
155 |
128 |
156 fun |
129 fun |
157 pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
130 pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set" |
158 where |
131 where |
159 "pders [] r = {r}" |
132 "pders [] r = {r}" |
160 | "pders (c # s) r = \<Union> (pders s) ` (pder c r)" |
133 | "pders (c # s) r = \<Union> (pders s) ` (pder c r)" |
161 |
134 |
162 abbreviation |
135 abbreviation |
163 "pders_set A r \<equiv> \<Union>s \<in> A. pders s r" |
136 "pderss s A \<equiv> \<Union> (pders s) ` A" |
164 |
137 |
165 lemma pders_append: |
138 lemma pders_append: |
166 "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)" |
139 "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)" |
167 by (induct s1 arbitrary: r) (simp_all) |
140 by (induct s1 arbitrary: r) (simp_all) |
168 |
141 |
169 lemma pders_snoc: |
142 lemma pders_snoc: |
170 shows "pders (s @ [c]) r = pder_set c (pders s r)" |
143 shows "pders (s @ [c]) r = pder_set c (pders s r)" |
171 by (simp add: pders_append) |
144 by (simp add: pders_append) |
172 |
145 |
173 lemma pders_set_lang: |
146 lemma pders_simps [simp]: |
174 shows "(\<Union> (lang ` pder_set c rs)) = (\<Union>r \<in> rs. (\<Union>lang ` (pder c r)))" |
|
175 unfolding image_def |
|
176 by auto |
|
177 |
|
178 lemma pders_Zero [simp]: |
|
179 shows "pders s Zero = {Zero}" |
147 shows "pders s Zero = {Zero}" |
180 by (induct s) (simp_all) |
148 and "pders s One = (if s = [] then {One} else {Zero})" |
181 |
149 and "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))" |
182 lemma pders_One [simp]: |
150 and "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))" |
183 shows "pders s One = (if s = [] then {One} else {Zero})" |
|
184 by (induct s) (auto) |
151 by (induct s) (auto) |
185 |
152 |
186 lemma pders_Atom [simp]: |
153 subsection {* Relating left-quotients and partial derivatives *} |
187 shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))" |
154 |
188 by (induct s) (auto) |
155 lemma Der_pder: |
189 |
156 shows "Der c (lang r) = \<Union> lang ` (pder c r)" |
190 lemma pders_Plus [simp]: |
157 by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib) |
191 shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))" |
158 |
192 by (induct s) (auto) |
159 lemma Ders_pders: |
|
160 shows "Ders s (lang r) = \<Union> lang ` (pders s r)" |
|
161 proof (induct s arbitrary: r) |
|
162 case (Cons c s) |
|
163 have ih: "\<And>r. Ders s (lang r) = \<Union> lang ` (pders s r)" by fact |
|
164 have "Ders (c # s) (lang r) = Ders s (Der c (lang r))" by simp |
|
165 also have "\<dots> = Ders s (\<Union> lang ` (pder c r))" by (simp add: Der_pder) |
|
166 also have "\<dots> = Derss s (lang ` (pder c r))" |
|
167 by (auto simp add: Ders_def) |
|
168 also have "\<dots> = \<Union> lang ` (pderss s (pder c r))" |
|
169 using ih by auto |
|
170 also have "\<dots> = \<Union> lang ` (pders (c # s) r)" by simp |
|
171 finally show "Ders (c # s) (lang r) = \<Union> lang ` pders (c # s) r" . |
|
172 qed (simp add: Ders_def) |
|
173 |
|
174 subsection {* Relating derivatives and partial derivatives *} |
|
175 |
|
176 lemma |
|
177 shows "(\<Union> lang ` (pder c r)) = lang (der c r)" |
|
178 unfolding Der_der[symmetric] Der_pder by simp |
|
179 |
|
180 lemma |
|
181 shows "(\<Union> lang ` (pders s r)) = lang (ders s r)" |
|
182 unfolding Ders_ders[symmetric] Ders_pders by simp |
|
183 |
|
184 |
|
185 subsection {* There are only finitely many partial derivatives for a language *} |
|
186 |
|
187 abbreviation |
|
188 "pders_set A r \<equiv> \<Union>s \<in> A. pders s r" |
193 |
189 |
194 text {* Non-empty suffixes of a string *} |
190 text {* Non-empty suffixes of a string *} |
195 |
191 |
196 definition |
192 definition |
197 "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" |
193 "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}" |
198 |
194 |
199 lemma Suf: |
195 lemma Suf_snoc: |
200 shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}" |
196 shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}" |
201 unfolding Suf_def conc_def |
197 unfolding Suf_def conc_def |
202 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv) |
198 by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv) |
203 |
199 |
204 lemma Suf_Union: |
200 lemma Suf_Union: |
205 shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))" |
201 shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))" |
206 by (auto simp add: conc_def) |
202 by (auto simp add: conc_def) |
207 |
203 |
|
204 lemma pders_set_snoc: |
|
205 shows "pders_set (Suf s \<cdot> {[c]}) r = (pder_set c (pders_set (Suf s) r))" |
|
206 by (simp add: Suf_Union pders_snoc) |
|
207 |
208 lemma pders_Times: |
208 lemma pders_Times: |
209 shows "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" |
209 shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2)" |
210 proof (induct s rule: rev_induct) |
210 proof (induct s rule: rev_induct) |
211 case (snoc c s) |
211 case (snoc c s) |
212 have ih: "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" |
212 have ih: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2)" |
213 by fact |
213 by fact |
214 have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" |
214 have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" |
215 by (simp add: pders_snoc) |
215 by (simp add: pders_snoc) |
216 also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))" |
216 also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2 \<union> (pders_set (Suf s) r2))" |
217 using ih by (auto) (blast) |
217 using ih by (auto) (blast) |
218 also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)" |
218 also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_set (Suf s) r2)" |
219 by (simp) |
219 by (simp) |
220 also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))" |
220 also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_set (Suf s \<cdot> {[c]}) r2" |
221 by (simp) |
221 by (simp add: pders_set_snoc) |
222 also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)" |
222 also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2" |
223 by (auto simp add: pders_snoc) |
223 by auto |
224 also have "\<dots> \<subseteq> Times_set (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)" |
224 also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2" |
225 by (auto simp add: if_splits) (blast) |
225 by (auto simp add: if_splits pders_snoc) (blast) |
226 also have "\<dots> = Times_set (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)" |
226 also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_set (Suf (s @ [c])) r2" |
227 by (auto simp add: pders_snoc Suf Suf_Union) |
227 by (auto simp add: Suf_snoc) |
228 finally show ?case . |
228 finally show ?case . |
229 qed (simp) |
229 qed (simp) |
|
230 |
230 |
231 |
231 lemma pders_Star: |
232 lemma pders_Star: |
232 assumes a: "s \<noteq> []" |
233 assumes a: "s \<noteq> []" |
233 shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Times_set (pders v r) (Star r))" |
234 shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Timess (pders v r) (Star r))" |
234 using a |
235 using a |
235 proof (induct s rule: rev_induct) |
236 proof (induct s rule: rev_induct) |
236 case (snoc c s) |
237 case (snoc c s) |
237 have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r))" by fact |
238 have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Timess (pders v r) (Star r))" by fact |
238 { assume asm: "s \<noteq> []" |
239 { assume asm: "s \<noteq> []" |
239 have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc) |
240 have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc) |
240 also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r)))" |
241 also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Timess (pders v r) (Star r)))" |
241 using ih[OF asm] by blast |
242 using ih[OF asm] by (auto) (blast) |
242 also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Times_set (pders v r) (Star r)))" |
243 also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Timess (pders v r) (Star r)))" |
243 by simp |
244 by simp |
244 also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))" |
245 also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))" |
245 by (auto split: if_splits) |
246 by (auto split: if_splits) |
246 also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)" |
247 also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)" |
247 using asm by (auto simp add: Suf_def) |
248 using asm by (auto simp add: Suf_def) |
248 also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pders (v @ [c]) r) (Star r))) \<union> (Times_set (pder c r) (Star r))" |
249 also have "\<dots> = (\<Union>v\<in>Suf s. (Timess (pders (v @ [c]) r) (Star r))) \<union> (Timess (pder c r) (Star r))" |
249 by (simp add: pders_snoc) |
250 by (simp add: pders_snoc) |
250 also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (pders v r) (Star r)))" |
251 also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Timess (pders v r) (Star r)))" |
251 by (auto simp add: Suf Suf_Union pders_snoc) |
252 by (auto simp add: Suf_snoc Suf_Union pders_snoc) |
252 finally have ?case . |
253 finally have ?case . |
253 } |
254 } |
254 moreover |
255 moreover |
255 { assume asm: "s = []" |
256 { assume asm: "s = []" |
256 then have ?case |
257 then have ?case |
367 using finite_pders_set by simp |
368 using finite_pders_set by simp |
368 ultimately |
369 ultimately |
369 show "finite {pders s r | s. s \<in> A}" |
370 show "finite {pders s r | s. s \<in> A}" |
370 by(rule finite_subset) |
371 by(rule finite_subset) |
371 qed |
372 qed |
372 |
|
373 |
|
374 subsection {* Relating left-quotients and partial derivatives *} |
|
375 |
|
376 lemma Der_pder: |
|
377 shows "Der c (lang r) = \<Union> lang ` (pder c r)" |
|
378 by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib) |
|
379 |
|
380 lemma Ders_pders: |
|
381 shows "Ders s (lang r) = \<Union> lang ` (pders s r)" |
|
382 proof (induct s rule: rev_induct) |
|
383 case (snoc c s) |
|
384 have ih: "Ders s (lang r) = \<Union> lang ` (pders s r)" by fact |
|
385 have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))" |
|
386 by (simp add: Ders_append) |
|
387 also have "\<dots> = Der c (\<Union> lang ` (pders s r))" using ih |
|
388 by (simp) |
|
389 also have "\<dots> = (\<Union>r\<in>pders s r. Der c (lang r))" |
|
390 unfolding Der_def image_def by auto |
|
391 also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> lang ` (pder c r)))" |
|
392 by (simp add: Der_pder) |
|
393 also have "\<dots> = (\<Union>lang ` (pder_set c (pders s r)))" |
|
394 by (simp add: pders_set_lang) |
|
395 also have "\<dots> = (\<Union>lang ` (pders (s @ [c]) r))" |
|
396 by (simp add: pders_snoc) |
|
397 finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" . |
|
398 qed (simp add: Ders_def) |
|
399 |
|
400 lemma Ders_set_pders_set: |
|
401 shows "Ders_set A (lang r) = (\<Union> lang ` (pders_set A r))" |
|
402 by (simp add: Ders_set_Ders Ders_pders) |
|
403 |
|
404 |
|
405 subsection {* Relating derivatives and partial derivatives *} |
|
406 |
|
407 lemma |
|
408 shows "(\<Union> lang ` (pder c r)) = lang (der c r)" |
|
409 unfolding Der_der[symmetric] Der_pder by simp |
|
410 |
|
411 lemma |
|
412 shows "(\<Union> lang ` (pders s r)) = lang (ders s r)" |
|
413 unfolding Ders_ders[symmetric] Ders_pders by simp |
|
414 |
373 |
415 |
374 |
416 text {* Relating the Myhill-Nerode relation with left-quotients. *} |
375 text {* Relating the Myhill-Nerode relation with left-quotients. *} |
417 |
376 |
418 lemma MN_Rel_Ders: |
377 lemma MN_Rel_Ders: |