199 |
200 |
200 |
201 |
201 lemma finite_Trn: |
202 lemma finite_Trn: |
202 assumes fin: "finite rhs" |
203 assumes fin: "finite rhs" |
203 shows "finite {r. Trn Y r \<in> rhs}" |
204 shows "finite {r. Trn Y r \<in> rhs}" |
204 proof - |
205 using assms by (auto intro!: finite_vimageI simp add: inj_on_def) |
205 have "finite {Trn Y r | Y r. Trn Y r \<in> rhs}" |
|
206 by (rule rev_finite_subset[OF fin]) (auto) |
|
207 then have "finite ((\<lambda>(Y, r). Trn Y r) ` {(Y, r) | Y r. Trn Y r \<in> rhs})" |
|
208 by (simp add: image_Collect) |
|
209 then have "finite {(Y, r) | Y r. Trn Y r \<in> rhs}" |
|
210 by (erule_tac finite_imageD) (simp add: inj_on_def) |
|
211 then show "finite {r. Trn Y r \<in> rhs}" |
|
212 by (erule_tac f="snd" in finite_surj) (auto simp add: image_def) |
|
213 qed |
|
214 |
206 |
215 lemma finite_Lam: |
207 lemma finite_Lam: |
216 assumes fin: "finite rhs" |
208 assumes fin: "finite rhs" |
217 shows "finite {r. Lam r \<in> rhs}" |
209 shows "finite {r. Lam r \<in> rhs}" |
218 proof - |
210 using assms by (auto intro!: finite_vimageI simp add: inj_on_def) |
219 have "finite {Lam r | r. Lam r \<in> rhs}" |
|
220 by (rule rev_finite_subset[OF fin]) (auto) |
|
221 then show "finite {r. Lam r \<in> rhs}" |
|
222 apply(simp add: image_Collect[symmetric]) |
|
223 apply(erule finite_imageD) |
|
224 apply(auto simp add: inj_on_def) |
|
225 done |
|
226 qed |
|
227 |
211 |
228 lemma trm_soundness: |
212 lemma trm_soundness: |
229 assumes finite:"finite rhs" |
213 assumes finite:"finite rhs" |
230 shows "lang_rhs ({Trn X r| r. Trn X r \<in> rhs}) = X \<cdot> (lang (\<Uplus>{r. Trn X r \<in> rhs}))" |
214 shows "lang_rhs ({Trn X r| r. Trn X r \<in> rhs}) = X \<cdot> (lang (\<Uplus>{r. Trn X r \<in> rhs}))" |
231 proof - |
215 proof - |
284 proof |
268 proof |
285 fix x |
269 fix x |
286 assume in_X: "x \<in> X" |
270 assume in_X: "x \<in> X" |
287 { assume empty: "x = []" |
271 { assume empty: "x = []" |
288 then have "x \<in> lang_rhs rhs" using X_in_eqs in_X |
272 then have "x \<in> lang_rhs rhs" using X_in_eqs in_X |
289 unfolding Init_def Init_rhs_def |
273 unfolding Init_def Init_rhs_def |
290 by auto |
274 by auto |
291 } |
275 } |
292 moreover |
276 moreover |
293 { assume not_empty: "x \<noteq> []" |
277 { assume not_empty: "x \<noteq> []" |
294 then obtain s c where decom: "x = s @ [c]" |
278 then obtain s c where decom: "x = s @ [c]" |
295 using rev_cases by blast |
279 using rev_cases by blast |
296 have "X \<in> UNIV // \<approx>A" using X_in_eqs unfolding Init_def by auto |
280 have "X \<in> UNIV // \<approx>A" using X_in_eqs unfolding Init_def by auto |
297 then obtain Y where "Y \<in> UNIV // \<approx>A" "Y \<cdot> {[c]} \<subseteq> X" "s \<in> Y" |
281 then obtain Y where "Y \<in> UNIV // \<approx>A" "Y \<cdot> {[c]} \<subseteq> X" "s \<in> Y" |
298 using decom in_X every_eqclass_has_transition by metis |
282 using decom in_X every_eqclass_has_transition by metis |
299 then have "x \<in> lang_rhs {Trn Y (Atom c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}" |
283 then have "x \<in> lang_rhs {Trn Y (Atom c)| Y c. Y \<in> UNIV // \<approx>A \<and> Y \<Turnstile>c\<Rightarrow> X}" |
300 unfolding transition_def |
284 unfolding transition_def |
301 using decom by (force simp add: conc_def) |
285 using decom by (force simp add: conc_def) |
302 then have "x \<in> lang_rhs rhs" using X_in_eqs in_X |
286 then have "x \<in> lang_rhs rhs" using X_in_eqs in_X |
303 unfolding Init_def Init_rhs_def by simp |
287 unfolding Init_def Init_rhs_def by simp |
304 } |
288 } |
305 ultimately show "x \<in> lang_rhs rhs" by blast |
289 ultimately show "x \<in> lang_rhs rhs" by blast |
306 qed |
290 qed |
307 next |
291 next |
308 show "lang_rhs rhs \<subseteq> X" using X_in_eqs |
292 show "lang_rhs rhs \<subseteq> X" using X_in_eqs |
313 |
297 |
314 lemma finite_Init_rhs: |
298 lemma finite_Init_rhs: |
315 fixes CS::"(('a::finite) lang) set" |
299 fixes CS::"(('a::finite) lang) set" |
316 assumes finite: "finite CS" |
300 assumes finite: "finite CS" |
317 shows "finite (Init_rhs CS X)" |
301 shows "finite (Init_rhs CS X)" |
318 proof- |
302 using assms unfolding Init_rhs_def transition_def by simp |
319 def S \<equiv> "{(Y, c)| Y c::'a. Y \<in> CS \<and> Y \<cdot> {[c]} \<subseteq> X}" |
|
320 def h \<equiv> "\<lambda> (Y, c::'a). Trn Y (Atom c)" |
|
321 have "finite (CS \<times> (UNIV::('a::finite) set))" using finite by auto |
|
322 then have "finite S" using S_def |
|
323 by (rule_tac B = "CS \<times> UNIV" in finite_subset) (auto) |
|
324 moreover have "{Trn Y (Atom c) |Y c::'a. Y \<in> CS \<and> Y \<cdot> {[c]} \<subseteq> X} = h ` S" |
|
325 unfolding S_def h_def image_def by auto |
|
326 ultimately |
|
327 have "finite {Trn Y (Atom c) |Y c. Y \<in> CS \<and> Y \<cdot> {[c]} \<subseteq> X}" by auto |
|
328 then show "finite (Init_rhs CS X)" unfolding Init_rhs_def transition_def by simp |
|
329 qed |
|
330 |
303 |
331 |
304 |
332 lemma Init_ES_satisfies_invariant: |
305 lemma Init_ES_satisfies_invariant: |
333 fixes A::"(('a::finite) lang)" |
306 fixes A::"(('a::finite) lang)" |
334 assumes finite_CS: "finite (UNIV // \<approx>A)" |
307 assumes finite_CS: "finite (UNIV // \<approx>A)" |
442 by (auto simp: Subst_def Append_preserves_finite) |
415 by (auto simp: Subst_def Append_preserves_finite) |
443 |
416 |
444 lemma Subst_all_preserves_finite: |
417 lemma Subst_all_preserves_finite: |
445 assumes finite: "finite ES" |
418 assumes finite: "finite ES" |
446 shows "finite (Subst_all ES Y yrhs)" |
419 shows "finite (Subst_all ES Y yrhs)" |
447 proof - |
420 using assms unfolding Subst_all_def by simp |
448 def eqns \<equiv> "{(X::'a lang, rhs) |X rhs. (X, rhs) \<in> ES}" |
|
449 def h \<equiv> "\<lambda>(X::'a lang, rhs). (X, Subst rhs Y yrhs)" |
|
450 have "finite (h ` eqns)" using finite h_def eqns_def by auto |
|
451 moreover |
|
452 have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto |
|
453 ultimately |
|
454 show "finite (Subst_all ES Y yrhs)" by simp |
|
455 qed |
|
456 |
421 |
457 lemma Subst_all_preserves_finite_rhs: |
422 lemma Subst_all_preserves_finite_rhs: |
458 "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)" |
423 "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)" |
459 by (auto intro:Subst_preserves_finite_rhs simp add:Subst_all_def finite_rhs_def) |
424 by (auto intro:Subst_preserves_finite_rhs simp add:Subst_all_def finite_rhs_def) |
460 |
425 |