--- a/Myhill_2.thy Fri Jun 03 13:59:21 2011 +0000
+++ b/Myhill_2.thy Mon Jul 25 13:33:38 2011 +0000
@@ -6,7 +6,7 @@
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)"
@@ -16,7 +16,7 @@
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}"
@@ -116,20 +116,20 @@
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
@@ -148,14 +148,14 @@
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
@@ -181,43 +181,43 @@
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))"
- unfolding tag_str_ALT_def quotient_def
+ then show "finite (range (tag_str_Plus A B))"
+ 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"
- unfolding tag_str_ALT_def
+ 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_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:
@@ -225,16 +225,16 @@
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:
- assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ A B y"
+lemma tag_str_Times_injI:
+ 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 *)
@@ -247,7 +247,7 @@
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
@@ -271,11 +271,11 @@
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"
@@ -287,30 +287,30 @@
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)
- show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y"
- by (rule tag_str_SEQ_injI)
+proof (rule_tac tag = "tag_str_Times L1 L2" in tag_finite_imageD)
+ 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_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))"
- unfolding tag_str_SEQ_def
+ show "finite (range (tag_str_Times L1 L2))"
+ 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>
@@ -342,31 +342,33 @@
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:
- assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
+lemma tag_str_Star_injI:
+ 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,
- auto simp:finite_strict_prefix_set)
+ 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"
@@ -384,7 +386,7 @@
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
@@ -417,7 +419,7 @@
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)"
@@ -432,11 +434,12 @@
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)
+ with h5 h6 show ?thesis
+ by (auto simp:strict_prefix_def elim: prefixE)
qed
}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
@@ -444,16 +447,17 @@
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)
- 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)
+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"
+ by (rule tag_str_Star_injI)
next
have *: "finite (Pow (UNIV // \<approx>A))"
using finite1 by auto
- show "finite (range (tag_str_STAR A))"
- unfolding tag_str_STAR_def
+ show "finite (range (tag_str_Star A))"
+ unfolding tag_str_Star_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
by auto
@@ -462,12 +466,13 @@
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