# HG changeset patch # User urbanc # Date 1289178789 0 # Node ID 48744a7f2661c5338ff844d484479d22d874b9a1 # Parent fbd62804f15342aba19681458ed58229dd127279 slight tuning of proof by Chunhan diff -r fbd62804f153 -r 48744a7f2661 MyhillNerode.thy --- a/MyhillNerode.thy Sat Nov 06 23:31:53 2010 +0000 +++ b/MyhillNerode.thy Mon Nov 08 01:13:09 2010 +0000 @@ -1512,25 +1512,13 @@ done -lemma QUOT_union: - "(QUOT (L1 \ L2)) \ ((QUOT L1) \ (QUOT L2))" -sorry - - -lemma quot_alt: - assumes finite1: "finite (QUOT L\<^isub>1)" - and finite2: "finite (QUOT L\<^isub>2)" - shows "finite (QUOT (L\<^isub>1 \ L\<^isub>2))" -apply(rule finite_subset) -apply(rule QUOT_union) -apply(simp add: finite1 finite2) -done - +(* lemma quot_star: assumes finite1: "finite (QUOT L\<^isub>1)" shows "finite (QUOT (L\<^isub>1\))" sorry + lemma other_direction: "Lang = L (r::rexp) \ finite (QUOT Lang)" apply (induct arbitrary:Lang rule:rexp.induct) @@ -1540,8 +1528,7 @@ lemma test: "UNIV Quo Lang = QUOT Lang" by (auto simp add: quot_def QUOT_def) - - +*) (* by chunhan *) @@ -1552,9 +1539,12 @@ apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset) by (auto simp add:image_def Pow_def) +term image +term "(op `) tag" + lemma str_inj_imps: assumes str_inj: "\ m n. tag m = tag (n::string) \ m \lang\ n" - shows "inj_on ((op `) tag) (QUOT lang)" + shows "inj_on (image tag) (QUOT lang)" proof (clarsimp simp add:inj_on_def QUOT_def) fix x y assume eq_tag: "tag ` \x\lang = tag ` \y\lang" @@ -1573,17 +1563,24 @@ qed qed -definition tag_str_ALT :: "string set \ string set \ string \ (string set \ string set)" +definition + tag_str_ALT :: "string set \ string set \ string \ (string set \ string set)" where "tag_str_ALT L\<^isub>1 L\<^isub>2 x \ (\x\L\<^isub>1, \x\L\<^isub>2)" +lemma + "{(\x\L\<^isub>1, \x\L\<^isub>2) | x. True} \ (QUOT L\<^isub>1) \ (QUOT L\<^isub>2)" +unfolding QUOT_def +by (auto) + lemma tag_str_alt_range_finite: assumes finite1: "finite (QUOT L\<^isub>1)" and finite2: "finite (QUOT L\<^isub>2)" shows "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" proof - have "{y. \x. y = (\x\L\<^isub>1, \x\L\<^isub>2)} \ (QUOT L\<^isub>1) \ (QUOT L\<^isub>2)" - by (auto simp:QUOT_def) + unfolding QUOT_def + by auto thus ?thesis using finite1 finite2 by (auto simp: image_def tag_str_ALT_def UNION_def intro: finite_subset[where B = "(QUOT L\<^isub>1) \ (QUOT L\<^isub>2)"]) @@ -1598,16 +1595,111 @@ assumes finite1: "finite (QUOT L\<^isub>1)" and finite2: "finite (QUOT L\<^isub>2)" shows "finite (QUOT (L\<^isub>1 \ L\<^isub>2))" -proof (rule_tac f = "(op `) (tag_str_ALT L\<^isub>1 L\<^isub>2)" in finite_imageD) - show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \ L\<^isub>2))" +proof - + have "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \ L\<^isub>2))" using finite_tag_image tag_str_alt_range_finite finite1 finite2 by auto -next - show "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \ L\<^isub>2))" + moreover + have "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \ L\<^isub>2))" apply (rule_tac str_inj_imps) by (erule_tac tag_str_alt_inj) + ultimately + show "finite (QUOT (L\<^isub>1 \ L\<^isub>2))" by (rule finite_imageD) qed + +(*by cu *) + + +definition + str_eq ("_ \_ _") +where + "x \Lang y \ (\z. x @ z \ Lang \ y @ z \ Lang)" + +definition + str_eq_rel ("\_") +where + "\Lang \ {(x, y). x \Lang y}" + +lemma [simp]: + "(x, y) \ {(x, y). P x y} \ P x y" +by simp + +lemma inj_image_lang: + fixes f::"string \ 'a" + assumes str_inj: "\x y. f x = f y \ x \Lang y" + shows "inj_on (image f) (UNIV // (\Lang))" +proof - + { fix x y::string + assume eq_tag: "f ` {z. x \Lang z} = f ` {z. y \Lang z}" + moreover + have "{z. x \Lang z} \ {}" unfolding str_eq_def by auto + ultimately obtain a b where "x \Lang a" "y \Lang b" "f a = f b" by blast + then have "x \Lang a" "y \Lang b" "a \Lang b" using str_inj by auto + then have "x \Lang y" unfolding str_eq_def by simp + then have "{z. x \Lang z} = {z. y \Lang z}" unfolding str_eq_def by simp + } + then have "\x\UNIV // \Lang. \y\UNIV // \Lang. f ` x = f ` y \ x = y" + unfolding quotient_def Image_def str_eq_rel_def by simp + then show "inj_on (image f) (UNIV // (\Lang))" + unfolding inj_on_def by simp +qed + + +lemma finite_range_image: + assumes fin: "finite (range f)" + shows "finite ((image f) ` X)" +proof - + from fin have "finite (Pow (f ` UNIV))" by auto + moreover + have "(image f) ` X \ Pow (f ` UNIV)" by auto + ultimately show "finite ((image f) ` X)" using finite_subset by auto +qed + +definition + tag1 :: "string set \ string set \ string \ (string set \ string set)" +where + "tag1 L\<^isub>1 L\<^isub>2 \ \x. ((\L\<^isub>1) `` {x}, (\L\<^isub>2) `` {x})" + +lemma tag1_range_finite: + assumes finite1: "finite (UNIV // \L\<^isub>1)" + and finite2: "finite (UNIV // \L\<^isub>2)" + shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))" +proof - + have "finite (UNIV // \L\<^isub>1 \ UNIV // \L\<^isub>2)" using finite1 finite2 by auto + moreover + have "range (tag1 L\<^isub>1 L\<^isub>2) \ (UNIV // \L\<^isub>1) \ (UNIV // \L\<^isub>2)" + unfolding tag1_def quotient_def by auto + ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))" + using finite_subset by blast +qed + +lemma tag1_inj: + "tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \ x \(L\<^isub>1 \ L\<^isub>2) y" +unfolding tag1_def Image_def str_eq_rel_def str_eq_def +by auto + +lemma quot_alt_cu: + fixes L\<^isub>1 L\<^isub>2::"string set" + assumes fin1: "finite (UNIV // \L\<^isub>1)" + and fin2: "finite (UNIV // \L\<^isub>2)" + shows "finite (UNIV // \(L\<^isub>1 \ L\<^isub>2))" +proof - + have "finite (range (tag1 L\<^isub>1 L\<^isub>2))" + using fin1 fin2 tag1_range_finite by simp + then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \(L\<^isub>1 \ L\<^isub>2)))" + using finite_range_image by blast + moreover + have "\x y. tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \ x \(L\<^isub>1 \ L\<^isub>2) y" + using tag1_inj by simp + then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \(L\<^isub>1 \ L\<^isub>2))" + using inj_image_lang by blast + ultimately + show "finite (UNIV // \(L\<^isub>1 \ L\<^isub>2))" by (rule finite_imageD) +qed + +(* by chunhan *) + (* list_diff:: list substract, once different return tailer *) fun list_diff :: "'a list \ 'a list \ 'a list" (infix "-" 51) where