regexp: comparison Myhill

equal deleted inserted replaced

-:b794db0b79db
+:b1258b7d2789
 begin
 section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
 definition
-str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
+str_eq :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>_ _")
 where
 "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
 lemma str_eq_def2:
 shows "\<approx>A = {(x, y) | x y. x \<approx>A y}"
 unfolding str_eq_def
 by simp
 definition
-tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")
+tag_eq_rel :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=")
 where
 "=tag= \<equiv> {(x, y). tag x = tag y}"
 lemma finite_eq_tag_rel:
 assumes rng_fnt: "finite (range tag)"
 qed
 subsection {* The proof *}
-subsubsection {* The base case for @{const "NULL"} *}
+subsubsection {* The base case for @{const "Zero"} *}
-lemma quot_null_eq:
+lemma quot_zero_eq:
 shows "UNIV // \<approx>{} = {UNIV}"
 unfolding quotient_def Image_def str_eq_rel_def by auto
-lemma quot_null_finiteI [intro]:
+lemma quot_zero_finiteI [intro]:
 shows "finite (UNIV // \<approx>{})"
-unfolding quot_null_eq by simp
+unfolding quot_zero_eq by simp
-subsubsection {* The base case for @{const "EMPTY"} *}
+subsubsection {* The base case for @{const "One"} *}
-lemma quot_empty_subset:
+lemma quot_one_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>{[]}}"
 have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def)
 thus ?thesis by simp
 qed
 qed
-lemma quot_empty_finiteI [intro]:
+lemma quot_one_finiteI [intro]:
 shows "finite (UNIV // \<approx>{[]})"
-by (rule finite_subset[OF quot_empty_subset]) (simp)
+by (rule finite_subset[OF quot_one_subset]) (simp)
-subsubsection {* The base case for @{const "CHAR"} *}
+subsubsection {* The base case for @{const "Atom"} *}
-lemma quot_char_subset:
+lemma quot_atom_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]}}"
 }
 ultimately show ?thesis by blast
 qed
 qed
-lemma quot_char_finiteI [intro]:
+lemma quot_atom_finiteI [intro]:
 shows "finite (UNIV // \<approx>{[c]})"
-by (rule finite_subset[OF quot_char_subset]) (simp)
+by (rule finite_subset[OF quot_atom_subset]) (simp)
-subsubsection {* The inductive case for @{const ALT} *}
+subsubsection {* The inductive case for @{const Plus} *}
 definition
-tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
+tag_str_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
 where
-"tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
+"tag_str_Plus A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
 lemma quot_union_finiteI [intro]:
 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)
+proof (rule_tac tag = "tag_str_Plus 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))"
+then show "finite (range (tag_str_Plus A B))"
-unfolding tag_str_ALT_def quotient_def
+unfolding tag_str_Plus_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"
+show "\<And>x y. tag_str_Plus A B x = tag_str_Plus A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
-unfolding tag_str_ALT_def
+unfolding tag_str_Plus_def
 unfolding str_eq_def
 unfolding str_eq_rel_def
 by auto
 qed
-subsubsection {* The inductive case for @{text "SEQ"}*}
+subsubsection {* The inductive case for @{text "Times"}*}
 definition
-tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
+tag_str_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)"
 where
-"tag_str_SEQ L1 L2 \<equiv>
+"tag_str_Times 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 \<cdot> 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
+unfolding conc_def prefix_def
 by (auto simp add: append_eq_append_conv2)
-lemma tag_str_SEQ_injI:
+lemma tag_str_Times_injI:
-assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y"
+assumes eq_tag: "tag_str_Times A B x = tag_str_Times A B y"
 shows "x \<approx>(A \<cdot> B) y"
 proof -
 { fix x y z
 assume xz_in_seq: "x @ z \<in> A \<cdot> B"
-and tag_xy: "tag_str_SEQ A B x = tag_str_SEQ A B y"
+and tag_xy: "tag_str_Times A B x = tag_str_Times A B y"
 have"y @ z \<in> A \<cdot> 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"
 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
+using tag_xy unfolding tag_str_Times_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'
 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
+using tag_xy unfolding tag_str_Times_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 \<cdot> B"
-	  unfolding prefix_def Seq_def
+	  unfolding prefix_def conc_def
 	  by (auto) (metis append_assoc)
 }
 ultimately show "y @ z \<in> A \<cdot> 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 \<cdot> B) y" unfolding str_eq_def str_eq_rel_def by blast
 qed
 lemma quot_seq_finiteI [intro]:
-fixes L1 L2::"lang"
+fixes L1 L2::"'a lang"
 assumes fin1: "finite (UNIV // \<approx>L1)"
 and     fin2: "finite (UNIV // \<approx>L2)"
 shows "finite (UNIV // \<approx>(L1 \<cdot> L2))"
-proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)
+proof (rule_tac tag = "tag_str_Times 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 \<cdot> L2) y"
+show "\<And>x y. tag_str_Times L1 L2 x = tag_str_Times L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y"
-by (rule tag_str_SEQ_injI)
+by (rule tag_str_Times_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))"
+show "finite (range (tag_str_Times L1 L2))"
-unfolding tag_str_SEQ_def
+unfolding tag_str_Times_def
 apply(rule finite_subset[OF _ *])
 unfolding quotient_def
 by auto
 qed
-subsubsection {* The inductive case for @{const "STAR"} *}
+subsubsection {* The inductive case for @{const "Star"} *}
 definition
-tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
+tag_str_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
 where
-"tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
+"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)
 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)}"
+lemma finite_strict_prefix_set:
+shows "finite {xa. xa < (x::'a list)}"
 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:
+lemma tag_str_Star_injI:
-assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
+fixes L\<^isub>1::"('a::finite) lang"
+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"
+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)
+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>}"
+let ?S = "{xa::('a::finite) list. 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,
+	by (rule_tac B = "{xa. xa < x}" in finite_subset)
-auto simp:finite_strict_prefix_set)
+	   (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 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)
+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
 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)
+using a_in h2 by (auto)
 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
 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
+have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using  l_za ls_zb
+	  by (rule_tac append_in_starI) (auto)
 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)
+by (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]:
+fixes A::"('a::finite) lang"
 assumes finite1: "finite (UNIV // \<approx>A)"
 shows "finite (UNIV // \<approx>(A\<star>))"
-proof (rule_tac tag = "tag_str_STAR A" in tag_finite_imageD)
+proof (rule_tac tag = "tag_str_Star A" in tag_finite_imageD)
-show "\<And>x y. tag_str_STAR A x = tag_str_STAR A y \<Longrightarrow> x \<approx>(A\<star>) y"
+show "\<And>x y. tag_str_Star A x = tag_str_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
-by (rule tag_str_STAR_injI)
+by (rule tag_str_Star_injI)
 next
 have *: "finite (Pow (UNIV // \<approx>A))"
 using finite1 by auto
-show "finite (range (tag_str_STAR A))"
+show "finite (range (tag_str_Star A))"
-unfolding tag_str_STAR_def
+unfolding tag_str_Star_def
 apply(rule finite_subset[OF _ *])
 unfolding quotient_def
 by auto
 qed
 subsubsection{* The conclusion *}
 lemma Myhill_Nerode2:
-shows "finite (UNIV // \<approx>(L_rexp r))"
+fixes r::"('a::finite) rexp"
+shows "finite (UNIV // \<approx>(lang r))"
 by (induct r) (auto)
 theorem Myhill_Nerode:
-shows "(\<exists>r. A = L_rexp r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
+fixes A::"('a::finite) lang"
+shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
 using Myhill_Nerode1 Myhill_Nerode2 by auto
 end

changeset 170	b1258b7d2789
parent 166	7743d2ad71d1
child 180	b755090d0f3d