--- a/Theories/Myhill_2.thy Tue May 31 20:32:49 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,470 +0,0 @@
-theory Myhill_2
- imports Myhill_1 Prefix_subtract
- "~~/src/HOL/Library/List_Prefix"
-begin
-
-section {* Direction @{text "regular language \<Rightarrow>finite partition"} *}
-
-definition
- str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
-where
- "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
-
-definition
- tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")
-where
- "=tag= \<equiv> {(x, y) | x y. tag x = tag y}"
-
-lemma finite_eq_tag_rel:
- assumes rng_fnt: "finite (range tag)"
- shows "finite (UNIV // =tag=)"
-proof -
- let "?f" = "\<lambda>X. tag ` X" and ?A = "(UNIV // =tag=)"
- have "finite (?f ` ?A)"
- proof -
- have "range ?f \<subseteq> (Pow (range tag))" unfolding Pow_def by auto
- moreover
- have "finite (Pow (range tag))" using rng_fnt by simp
- ultimately
- have "finite (range ?f)" unfolding image_def by (blast intro: finite_subset)
- moreover
- have "?f ` ?A \<subseteq> range ?f" by auto
- ultimately show "finite (?f ` ?A)" by (rule rev_finite_subset)
- qed
- moreover
- have "inj_on ?f ?A"
- proof -
- { fix X Y
- assume X_in: "X \<in> ?A"
- and Y_in: "Y \<in> ?A"
- and tag_eq: "?f X = ?f Y"
- then obtain x y
- where "x \<in> X" "y \<in> Y" "tag x = tag y"
- unfolding quotient_def Image_def image_def tag_eq_rel_def
- by (simp) (blast)
- with X_in Y_in
- have "X = Y"
- unfolding quotient_def tag_eq_rel_def by auto
- }
- then show "inj_on ?f ?A" unfolding inj_on_def by auto
- qed
- ultimately show "finite (UNIV // =tag=)" by (rule finite_imageD)
-qed
-
-lemma refined_partition_finite:
- assumes fnt: "finite (UNIV // R1)"
- and refined: "R1 \<subseteq> R2"
- and eq1: "equiv UNIV R1" and eq2: "equiv UNIV R2"
- shows "finite (UNIV // R2)"
-proof -
- let ?f = "\<lambda>X. {R1 `` {x} | x. x \<in> X}"
- and ?A = "UNIV // R2" and ?B = "UNIV // R1"
- have "?f ` ?A \<subseteq> Pow ?B"
- unfolding image_def Pow_def quotient_def by auto
- moreover
- have "finite (Pow ?B)" using fnt by simp
- ultimately
- have "finite (?f ` ?A)" by (rule finite_subset)
- moreover
- have "inj_on ?f ?A"
- proof -
- { fix X Y
- assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A" and eq_f: "?f X = ?f Y"
- from quotientE [OF X_in]
- obtain x where "X = R2 `` {x}" by blast
- with equiv_class_self[OF eq2] have x_in: "x \<in> X" by simp
- then have "R1 ``{x} \<in> ?f X" by auto
- with eq_f have "R1 `` {x} \<in> ?f Y" by simp
- then obtain y
- where y_in: "y \<in> Y" and eq_r1_xy: "R1 `` {x} = R1 `` {y}" by auto
- with eq_equiv_class[OF _ eq1]
- have "(x, y) \<in> R1" by blast
- with refined have "(x, y) \<in> R2" by auto
- with quotient_eqI [OF eq2 X_in Y_in x_in y_in]
- have "X = Y" .
- }
- then show "inj_on ?f ?A" unfolding inj_on_def by blast
- qed
- ultimately show "finite (UNIV // R2)" by (rule finite_imageD)
-qed
-
-lemma tag_finite_imageD:
- assumes rng_fnt: "finite (range tag)"
- and same_tag_eqvt: "\<And>m n. tag m = tag n \<Longrightarrow> m \<approx>A n"
- shows "finite (UNIV // \<approx>A)"
-proof (rule_tac refined_partition_finite [of "=tag="])
- show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
-next
- from same_tag_eqvt
- show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_rel_def str_eq_def
- by auto
-next
- show "equiv UNIV =tag="
- unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def
- by auto
-next
- show "equiv UNIV (\<approx>A)"
- unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
- by blast
-qed
-
-
-subsection {* The proof *}
-
-subsubsection {* The base case for @{const "NULL"} *}
-
-lemma quot_null_eq:
- shows "UNIV // \<approx>{} = {UNIV}"
-unfolding quotient_def Image_def str_eq_rel_def by auto
-
-lemma quot_null_finiteI [intro]:
- shows "finite (UNIV // \<approx>{})"
-unfolding quot_null_eq by simp
-
-
-subsubsection {* The base case for @{const "EMPTY"} *}
-
-lemma quot_empty_subset:
- shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}"
-proof
- fix x
- assume "x \<in> UNIV // \<approx>{[]}"
- then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}"
- unfolding quotient_def Image_def by blast
- show "x \<in> {{[]}, UNIV - {[]}}"
- proof (cases "y = []")
- case True with h
- have "x = {[]}" by (auto simp: str_eq_rel_def)
- thus ?thesis by simp
- next
- case False with h
- have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def)
- thus ?thesis by simp
- qed
-qed
-
-lemma quot_empty_finiteI [intro]:
- shows "finite (UNIV // \<approx>{[]})"
-by (rule finite_subset[OF quot_empty_subset]) (simp)
-
-
-subsubsection {* The base case for @{const "CHAR"} *}
-
-lemma quot_char_subset:
- "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
-proof
- fix x
- assume "x \<in> UNIV // \<approx>{[c]}"
- then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[c]}}"
- unfolding quotient_def Image_def by blast
- show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}"
- proof -
- { assume "y = []" hence "x = {[]}" using h
- by (auto simp:str_eq_rel_def) }
- moreover
- { assume "y = [c]" hence "x = {[c]}" using h
- by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) }
- moreover
- { assume "y \<noteq> []" and "y \<noteq> [c]"
- hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto)
- moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])"
- by (case_tac p, auto)
- ultimately have "x = UNIV - {[],[c]}" using h
- by (auto simp add:str_eq_rel_def)
- }
- ultimately show ?thesis by blast
- qed
-qed
-
-lemma quot_char_finiteI [intro]:
- shows "finite (UNIV // \<approx>{[c]})"
-by (rule finite_subset[OF quot_char_subset]) (simp)
-
-
-subsubsection {* The inductive case for @{const ALT} *}
-
-definition
- tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
-where
- "tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
-
-lemma quot_union_finiteI [intro]:
- fixes L1 L2::"lang"
- assumes finite1: "finite (UNIV // \<approx>A)"
- and finite2: "finite (UNIV // \<approx>B)"
- shows "finite (UNIV // \<approx>(A \<union> B))"
-proof (rule_tac tag = "tag_str_ALT A B" in tag_finite_imageD)
- have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"
- using finite1 finite2 by auto
- then show "finite (range (tag_str_ALT A B))"
- unfolding tag_str_ALT_def quotient_def
- by (rule rev_finite_subset) (auto)
-next
- show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
- unfolding tag_str_ALT_def
- unfolding str_eq_def
- unfolding str_eq_rel_def
- by auto
-qed
-
-
-subsubsection {* The inductive case for @{text "SEQ"}*}
-
-definition
- tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
-where
- "tag_str_SEQ L1 L2 \<equiv>
- (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))"
-
-lemma Seq_in_cases:
- assumes "x @ z \<in> A ;; B"
- shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or>
- (\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"
-using assms
-unfolding Seq_def prefix_def
-by (auto simp add: append_eq_append_conv2)
-
-lemma tag_str_SEQ_injI:
- assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y"
- shows "x \<approx>(A ;; B) y"
-proof -
- { fix x y z
- assume xz_in_seq: "x @ z \<in> A ;; B"
- and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y"
- have"y @ z \<in> A ;; B"
- proof -
- { (* first case with x' in A and (x - x') @ z in B *)
- fix x'
- assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B"
- obtain y'
- where "y' \<le> y"
- and "y' \<in> A"
- and "(y - y') @ z \<in> B"
- proof -
- have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} =
- {\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right")
- using tag_xy unfolding tag_str_SEQ_def by simp
- moreover
- have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto
- ultimately
- have "\<approx>B `` {x - x'} \<in> ?Right" by simp
- then obtain y'
- where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"
- and pref_y': "y' \<le> y" and y'_in: "y' \<in> A"
- by simp blast
-
- have "(x - x') \<approx>B (y - y')" using eq_xy'
- unfolding Image_def str_eq_rel_def str_eq_def by auto
- with h3 have "(y - y') @ z \<in> B"
- unfolding str_eq_rel_def str_eq_def by simp
- with pref_y' y'_in
- show ?thesis using that by blast
- qed
- then have "y @ z \<in> A ;; B" by (erule_tac prefixE) (auto simp: Seq_def)
- }
- moreover
- { (* second case with x @ z' in A and z - z' in B *)
- fix z'
- assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B"
- have "\<approx>A `` {x} = \<approx>A `` {y}"
- using tag_xy unfolding tag_str_SEQ_def by simp
- with h2 have "y @ z' \<in> A"
- unfolding Image_def str_eq_rel_def str_eq_def by auto
- with h1 h3 have "y @ z \<in> A ;; B"
- unfolding prefix_def Seq_def
- by (auto) (metis append_assoc)
- }
- ultimately show "y @ z \<in> A ;; B"
- using Seq_in_cases [OF xz_in_seq] by blast
- qed
- }
- from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
- show "x \<approx>(A ;; B) y" unfolding str_eq_def str_eq_rel_def by blast
-qed
-
-lemma quot_seq_finiteI [intro]:
- fixes L1 L2::"lang"
- assumes fin1: "finite (UNIV // \<approx>L1)"
- and fin2: "finite (UNIV // \<approx>L2)"
- shows "finite (UNIV // \<approx>(L1 ;; L2))"
-proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)
- show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y"
- by (rule tag_str_SEQ_injI)
-next
- have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))"
- using fin1 fin2 by auto
- show "finite (range (tag_str_SEQ L1 L2))"
- unfolding tag_str_SEQ_def
- apply(rule finite_subset[OF _ *])
- unfolding quotient_def
- by auto
-qed
-
-
-subsubsection {* The inductive case for @{const "STAR"} *}
-
-definition
- tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
-where
- "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
-
-text {* A technical lemma. *}
-lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow>
- (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))"
-proof (induct rule:finite.induct)
- case emptyI thus ?case by simp
-next
- case (insertI A a)
- show ?case
- proof (cases "A = {}")
- case True thus ?thesis by (rule_tac x = a in bexI, auto)
- next
- case False
- with insertI.hyps and False
- obtain max
- where h1: "max \<in> A"
- and h2: "\<forall>a\<in>A. f a \<le> f max" by blast
- show ?thesis
- proof (cases "f a \<le> f max")
- assume "f a \<le> f max"
- with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto)
- next
- assume "\<not> (f a \<le> f max)"
- thus ?thesis using h2 by (rule_tac x = a in bexI, auto)
- qed
- qed
-qed
-
-
-text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *}
-
-lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"
-apply (induct x rule:rev_induct, simp)
-apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
-by (auto simp:strict_prefix_def)
-
-
-lemma tag_str_STAR_injI:
- assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
- shows "v \<approx>(L\<^isub>1\<star>) w"
-proof-
- { fix x y z
- assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>"
- and tag_xy: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
- have "y @ z \<in> L\<^isub>1\<star>"
- proof(cases "x = []")
- case True
- with tag_xy have "y = []"
- by (auto simp add: tag_str_STAR_def strict_prefix_def)
- thus ?thesis using xz_in_star True by simp
- next
- case False
- let ?S = "{xa. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
- have "finite ?S"
- by (rule_tac B = "{xa. xa < x}" in finite_subset,
- auto simp:finite_strict_prefix_set)
- moreover have "?S \<noteq> {}" using False xz_in_star
- by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
- ultimately have "\<exists> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max"
- using finite_set_has_max by blast
- then obtain xa_max
- where h1: "xa_max < x"
- and h2: "xa_max \<in> L\<^isub>1\<star>"
- and h3: "(x - xa_max) @ z \<in> L\<^isub>1\<star>"
- and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>
- \<longrightarrow> length xa \<le> length xa_max"
- by blast
- obtain ya
- where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>"
- and eq_xya: "(x - xa_max) \<approx>L\<^isub>1 (y - ya)"
- proof-
- from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} =
- {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")
- by (auto simp:tag_str_STAR_def)
- moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto
- ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp
- thus ?thesis using that
- apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast
- qed
- have "(y - ya) @ z \<in> L\<^isub>1\<star>"
- proof-
- obtain za zb where eq_zab: "z = za @ zb"
- and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"
- proof -
- from h1 have "(x - xa_max) @ z \<noteq> []"
- by (auto simp:strict_prefix_def elim:prefixE)
- from star_decom [OF h3 this]
- obtain a b where a_in: "a \<in> L\<^isub>1"
- and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>"
- and ab_max: "(x - xa_max) @ z = a @ b" by blast
- let ?za = "a - (x - xa_max)" and ?zb = "b"
- have pfx: "(x - xa_max) \<le> a" (is "?P1")
- and eq_z: "z = ?za @ ?zb" (is "?P2")
- proof -
- have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or>
- (a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)"
- using append_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
- moreover {
- assume np: "a < (x - xa_max)"
- and b_eqs: "((x - xa_max) - a) @ z = b"
- have "False"
- proof -
- let ?xa_max' = "xa_max @ a"
- have "?xa_max' < x"
- using np h1 by (clarsimp simp:strict_prefix_def diff_prefix)
- moreover have "?xa_max' \<in> L\<^isub>1\<star>"
- using a_in h2 by (simp add:star_intro3)
- moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>"
- using b_eqs b_in np h1 by (simp add:diff_diff_append)
- moreover have "\<not> (length ?xa_max' \<le> length xa_max)"
- using a_neq by simp
- ultimately show ?thesis using h4 by blast
- qed }
- ultimately show ?P1 and ?P2 by auto
- qed
- hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)
- with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1"
- by (auto simp:str_eq_def str_eq_rel_def)
- with eq_z and b_in
- show ?thesis using that by blast
- qed
- have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb by blast
- with eq_zab show ?thesis by simp
- qed
- with h5 h6 show ?thesis
- by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)
- qed
- }
- from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
- show ?thesis unfolding str_eq_def str_eq_rel_def by blast
-qed
-
-lemma quot_star_finiteI [intro]:
- assumes finite1: "finite (UNIV // \<approx>L1)"
- shows "finite (UNIV // \<approx>(L1\<star>))"
-proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD)
- show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y"
- by (rule tag_str_STAR_injI)
-next
- have *: "finite (Pow (UNIV // \<approx>L1))"
- using finite1 by auto
- show "finite (range (tag_str_STAR L1))"
- unfolding tag_str_STAR_def
- apply(rule finite_subset[OF _ *])
- unfolding quotient_def
- by auto
-qed
-
-subsubsection{* The conclusion *}
-
-lemma Myhill_Nerode2:
- fixes r::"rexp"
- shows "finite (UNIV // \<approx>(L r))"
-by (induct r) (auto)
-
-
-theorem Myhill_Nerode:
- shows "(\<exists>r::rexp. A = L r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
-using Myhill_Nerode1 Myhill_Nerode2 by auto
-
-end