176 show "?P \<Longrightarrow> ?Q ?vs" by (induct us) auto |
173 show "?P \<Longrightarrow> ?Q ?vs" by (induct us) auto |
177 qed |
174 qed |
178 } thus ?thesis by (auto simp: star_conv_concat) |
175 } thus ?thesis by (auto simp: star_conv_concat) |
179 qed |
176 qed |
180 |
177 |
|
178 lemma star_decom: |
|
179 assumes a: "x \<in> star A" "x \<noteq> []" |
|
180 shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A" |
|
181 using a by (induct rule: star_induct) (blast)+ |
|
182 |
|
183 subsection {* Arden's Lemma *} |
|
184 |
|
185 lemma arden_helper: |
|
186 assumes eq: "X = A @@ X \<union> B" |
|
187 shows "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" |
|
188 proof (induct n) |
|
189 case 0 |
|
190 show "X = (A ^^ Suc 0) @@ X \<union> (\<Union>m\<le>0. (A ^^ m) @@ B)" |
|
191 using eq by simp |
|
192 next |
|
193 case (Suc n) |
|
194 have ih: "X = (A ^^ Suc n) @@ X \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" by fact |
|
195 also have "\<dots> = (A ^^ Suc n) @@ (A @@ X \<union> B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" using eq by simp |
|
196 also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> ((A ^^ Suc n) @@ B) \<union> (\<Union>m\<le>n. (A ^^ m) @@ B)" |
|
197 by (simp add: conc_Un_distrib conc_assoc[symmetric] conc_pow_comm) |
|
198 also have "\<dots> = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)" |
|
199 by (auto simp add: le_Suc_eq) |
|
200 finally show "X = (A ^^ Suc (Suc n)) @@ X \<union> (\<Union>m\<le>Suc n. (A ^^ m) @@ B)" . |
|
201 qed |
|
202 |
181 lemma Arden: |
203 lemma Arden: |
182 assumes "[] \<notin> A" and "X = A @@ X \<union> B" |
204 assumes "[] \<notin> A" |
183 shows "X = star A @@ B" |
205 shows "X = A @@ X \<union> B \<longleftrightarrow> X = star A @@ B" |
184 proof - |
206 proof |
185 { fix n have "X = A^^(n+1)@@X \<union> (\<Union>i\<le>n. A^^i@@B)" |
207 assume eq: "X = A @@ X \<union> B" |
186 proof(induct n) |
|
187 case 0 show ?case using `X = A @@ X \<union> B` by simp |
|
188 next |
|
189 case (Suc n) |
|
190 have "X = A@@X Un B" by(rule assms(2)) |
|
191 also have "\<dots> = A@@(A^^(n+1)@@X \<union> (\<Union>i\<le>n. A^^i@@B)) Un B" |
|
192 by(subst Suc)(rule refl) |
|
193 also have "\<dots> = A^^(n+2)@@X \<union> (\<Union>i\<le>n. A^^(i+1)@@B) Un B" |
|
194 by(simp add:conc_UNION_distrib conc_assoc conc_Un_distrib) |
|
195 also have "\<dots> = A^^(n+2)@@X \<union> (UN i : {1..n+1}. A^^i@@B) \<union> B" |
|
196 by(subst UN_le_add_shift)(rule refl) |
|
197 also have "\<dots> = A^^(n+2)@@X \<union> (UN i : {1..n+1}. A^^i@@B) \<union> A^^0@@B" |
|
198 by(simp) |
|
199 also have "\<dots> = A^^(n+2)@@X \<union> (\<Union>i\<le>n+1. A^^i@@B)" |
|
200 by(auto simp: UN_le_eq_Un0) |
|
201 finally show ?case by simp |
|
202 qed |
|
203 } note 1 = this |
|
204 { fix w assume "w : X" |
208 { fix w assume "w : X" |
205 let ?n = "size w" |
209 let ?n = "size w" |
206 from `[] \<notin> A` have "ALL u : A. length u \<ge> 1" |
210 from `[] \<notin> A` have "ALL u : A. length u \<ge> 1" |
207 by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq) |
211 by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq) |
208 hence "ALL u : A^^(?n+1). length u \<ge> ?n+1" |
212 hence "ALL u : A^^(?n+1). length u \<ge> ?n+1" |
209 by (metis length_lang_pow_lb nat_mult_1) |
213 by (metis length_lang_pow_lb nat_mult_1) |
210 hence "ALL u : A^^(?n+1)@@X. length u \<ge> ?n+1" |
214 hence "ALL u : A^^(?n+1)@@X. length u \<ge> ?n+1" |
211 by(auto simp only: conc_def length_append) |
215 by(auto simp only: conc_def length_append) |
212 hence "w \<notin> A^^(?n+1)@@X" by auto |
216 hence "w \<notin> A^^(?n+1)@@X" by auto |
213 hence "w : star A @@ B" using `w : X` 1[of ?n] |
217 hence "w : star A @@ B" using `w : X` using arden_helper[OF eq, where n="?n"] |
214 by(auto simp add: star_def conc_UNION_distrib) |
218 by (auto simp add: star_def conc_UNION_distrib) |
215 } moreover |
219 } moreover |
216 { fix w assume "w : star A @@ B" |
220 { fix w assume "w : star A @@ B" |
217 hence "EX n. w : A^^n @@ B" by(auto simp: conc_def star_def) |
221 hence "EX n. w : A^^n @@ B" by(auto simp: conc_def star_def) |
218 hence "w : X" using 1 by blast |
222 hence "w : X" using arden_helper[OF eq] by blast |
219 } ultimately show ?thesis by blast |
223 } ultimately show "X = star A @@ B" by blast |
220 qed |
224 next |
221 |
225 assume eq: "X = star A @@ B" |
222 subsection{* @{const deriv} *} |
226 have "star A = A @@ star A \<union> {[]}" |
223 |
227 by (rule star_unfold_left) |
224 lemma deriv_empty[simp]: "deriv a {} = {}" |
228 then have "star A @@ B = (A @@ star A \<union> {[]}) @@ B" |
225 and deriv_epsilon[simp]: "deriv a {[]} = {}" |
229 by metis |
226 and deriv_char[simp]: "deriv a {[b]} = (if a = b then {[]} else {})" |
230 also have "\<dots> = (A @@ star A) @@ B \<union> B" |
227 and deriv_union[simp]: "deriv a (A \<union> B) = deriv a A \<union> deriv a B" |
231 unfolding conc_Un_distrib by simp |
228 by (auto simp: deriv_def) |
232 also have "\<dots> = A @@ (star A @@ B) \<union> B" |
229 |
233 by (simp only: conc_assoc) |
230 lemma deriv_conc_subset: |
234 finally show "X = A @@ X \<union> B" |
231 "deriv a A @@ B \<subseteq> deriv a (A @@ B)" (is "?L \<subseteq> ?R") |
235 using eq by blast |
232 proof |
236 qed |
233 fix w assume "w \<in> ?L" |
237 |
234 then obtain u v where "w = u @ v" "a # u \<in> A" "v \<in> B" |
238 |
235 by (auto simp: deriv_def) |
239 lemma reversed_arden_helper: |
236 then have "a # w \<in> A @@ B" |
240 assumes eq: "X = X @@ A \<union> B" |
237 by (auto intro: concI[of "a # u", simplified]) |
241 shows "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" |
238 thus "w \<in> ?R" by (auto simp: deriv_def) |
242 proof (induct n) |
239 qed |
243 case 0 |
240 |
244 show "X = X @@ (A ^^ Suc 0) \<union> (\<Union>m\<le>0. B @@ (A ^^ m))" |
241 lemma deriv_conc1: |
245 using eq by simp |
242 assumes "[] \<notin> A" |
246 next |
243 shows "deriv a (A @@ B) = deriv a A @@ B" (is "?L = ?R") |
247 case (Suc n) |
244 proof |
248 have ih: "X = X @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" by fact |
245 show "?L \<subseteq> ?R" |
249 also have "\<dots> = (X @@ A \<union> B) @@ (A ^^ Suc n) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" using eq by simp |
246 proof |
250 also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (B @@ (A ^^ Suc n)) \<union> (\<Union>m\<le>n. B @@ (A ^^ m))" |
247 fix w assume "w \<in> ?L" |
251 by (simp add: conc_Un_distrib conc_assoc) |
248 then have "a # w \<in> A @@ B" by (simp add: deriv_def) |
252 also have "\<dots> = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))" |
249 then obtain x y |
253 by (auto simp add: le_Suc_eq) |
250 where aw: "a # w = x @ y" "x \<in> A" "y \<in> B" by auto |
254 finally show "X = X @@ (A ^^ Suc (Suc n)) \<union> (\<Union>m\<le>Suc n. B @@ (A ^^ m))" . |
251 with `[] \<notin> A` obtain x' where "x = a # x'" |
255 qed |
252 by (cases x) auto |
256 |
253 with aw have "w = x' @ y" "x' \<in> deriv a A" |
257 theorem reversed_Arden: |
254 by (auto simp: deriv_def) |
258 assumes nemp: "[] \<notin> A" |
255 with `y \<in> B` show "w \<in> ?R" by simp |
259 shows "X = X @@ A \<union> B \<longleftrightarrow> X = B @@ star A" |
256 qed |
260 proof |
257 show "?R \<subseteq> ?L" by (fact deriv_conc_subset) |
261 assume eq: "X = X @@ A \<union> B" |
258 qed |
262 { fix w assume "w : X" |
259 |
263 let ?n = "size w" |
260 lemma deriv_conc2: |
264 from `[] \<notin> A` have "ALL u : A. length u \<ge> 1" |
261 assumes "[] \<in> A" |
265 by (metis Suc_eq_plus1 add_leD2 le_0_eq length_0_conv not_less_eq_eq) |
262 shows "deriv a (A @@ B) = deriv a A @@ B \<union> deriv a B" |
266 hence "ALL u : A^^(?n+1). length u \<ge> ?n+1" |
263 (is "?L = ?R") |
267 by (metis length_lang_pow_lb nat_mult_1) |
264 proof |
268 hence "ALL u : X @@ A^^(?n+1). length u \<ge> ?n+1" |
265 show "?L \<subseteq> ?R" |
269 by(auto simp only: conc_def length_append) |
266 proof |
270 hence "w \<notin> X @@ A^^(?n+1)" by auto |
267 fix w assume "w \<in> ?L" |
271 hence "w : B @@ star A" using `w : X` using reversed_arden_helper[OF eq, where n="?n"] |
268 then have "a # w \<in> A @@ B" by (simp add: deriv_def) |
272 by (auto simp add: star_def conc_UNION_distrib) |
269 then obtain x y |
273 } moreover |
270 where aw: "a # w = x @ y" "x \<in> A" "y \<in> B" by auto |
274 { fix w assume "w : B @@ star A" |
271 show "w \<in> ?R" |
275 hence "EX n. w : B @@ A^^n" by (auto simp: conc_def star_def) |
272 proof (cases x) |
276 hence "w : X" using reversed_arden_helper[OF eq] by blast |
273 case Nil |
277 } ultimately show "X = B @@ star A" by blast |
274 with aw have "w \<in> deriv a B" by (auto simp: deriv_def) |
278 next |
275 thus ?thesis .. |
279 assume eq: "X = B @@ star A" |
276 next |
280 have "star A = {[]} \<union> star A @@ A" |
277 case (Cons b x') |
281 unfolding conc_star_comm[symmetric] |
278 with aw have "w = x' @ y" "x' \<in> deriv a A" |
282 by(metis Un_commute star_unfold_left) |
279 by (auto simp: deriv_def) |
283 then have "B @@ star A = B @@ ({[]} \<union> star A @@ A)" |
280 with `y \<in> B` show "w \<in> ?R" by simp |
284 by metis |
281 qed |
285 also have "\<dots> = B \<union> B @@ (star A @@ A)" |
282 qed |
286 unfolding conc_Un_distrib by simp |
283 |
287 also have "\<dots> = B \<union> (B @@ star A) @@ A" |
284 from concI[OF `[] \<in> A`, simplified] |
288 by (simp only: conc_assoc) |
285 have "B \<subseteq> A @@ B" .. |
289 finally show "X = X @@ A \<union> B" |
286 then have "deriv a B \<subseteq> deriv a (A @@ B)" by (auto simp: deriv_def) |
290 using eq by blast |
287 with deriv_conc_subset[of a A B] |
291 qed |
288 show "?R \<subseteq> ?L" by auto |
292 |
289 qed |
|
290 |
|
291 lemma wlog_no_eps: |
|
292 assumes PB: "\<And>B. [] \<notin> B \<Longrightarrow> P B" |
|
293 assumes preserved: "\<And>A. P A \<Longrightarrow> P (insert [] A)" |
|
294 shows "P A" |
|
295 proof - |
|
296 let ?B = "A - {[]}" |
|
297 have "P ?B" by (rule PB) auto |
|
298 thus "P A" |
|
299 proof cases |
|
300 assume "[] \<in> A" |
|
301 then have "(insert [] ?B) = A" by auto |
|
302 with preserved[OF `P ?B`] |
|
303 show ?thesis by simp |
|
304 qed auto |
|
305 qed |
|
306 |
|
307 lemma deriv_insert_eps[simp]: |
|
308 "deriv a (insert [] A) = deriv a A" |
|
309 by (auto simp: deriv_def) |
|
310 |
|
311 lemma deriv_star[simp]: "deriv a (star A) = deriv a A @@ star A" |
|
312 proof (induct A rule: wlog_no_eps) |
|
313 fix B :: "'a list set" assume "[] \<notin> B" |
|
314 thus "deriv a (star B) = deriv a B @@ star B" |
|
315 by (subst star_unfold_left) (simp add: deriv_conc1) |
|
316 qed auto |
|
317 |
|
318 |
|
319 subsection{* @{const bisimilar} *} |
|
320 |
|
321 lemma equal_if_bisimilar: |
|
322 assumes "bisimilar K L" shows "K = L" |
|
323 proof (rule set_eqI) |
|
324 fix w |
|
325 from `bisimilar K L` show "w \<in> K \<longleftrightarrow> w \<in> L" |
|
326 proof (induct w arbitrary: K L) |
|
327 case Nil thus ?case by (auto elim: bisimilar.cases) |
|
328 next |
|
329 case (Cons a w K L) |
|
330 from `bisimilar K L` have "bisimilar (deriv a K) (deriv a L)" |
|
331 by (auto elim: bisimilar.cases) |
|
332 then have "w \<in> deriv a K \<longleftrightarrow> w \<in> deriv a L" by (rule Cons(1)) |
|
333 thus ?case by (auto simp: deriv_def) |
|
334 qed |
|
335 qed |
|
336 |
|
337 lemma language_coinduct: |
|
338 fixes R (infixl "\<sim>" 50) |
|
339 assumes "K \<sim> L" |
|
340 assumes "\<And>K L. K \<sim> L \<Longrightarrow> ([] \<in> K \<longleftrightarrow> [] \<in> L)" |
|
341 assumes "\<And>K L x. K \<sim> L \<Longrightarrow> deriv x K \<sim> deriv x L" |
|
342 shows "K = L" |
|
343 apply (rule equal_if_bisimilar) |
|
344 apply (rule bisimilar.coinduct[of R, OF `K \<sim> L`]) |
|
345 apply (auto simp: assms) |
|
346 done |
|
347 |
293 |
348 end |
294 end |