--- a/Myhill.thy Thu Jan 27 17:37:20 2011 +0000
+++ b/Myhill.thy Fri Jan 28 11:52:11 2011 +0000
@@ -13,46 +13,51 @@
*}
definition
- str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
+ str_eq ("_ \<approx>_ _")
where
"x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"
text {*
- The very basic scheme to show the finiteness of the partion generated by a language @{text "Lang"}
- is by attaching a tag to every string. The set of tags are carfully choosen to be finite so that
- the range of tagging function is finite. If it can be proved that strings with the same tag
- are equivlent with respect @{text "Lang"}, then the partition given rise by @{text "Lang"} must be finite.
- The detailed argjument for this is formalized by the following lemma @{text "tag_finite_imageD"}.
- The basic idea is using lemma @{thm [source] "finite_imageD"}
- from standard library:
- \[
- @{thm "finite_imageD" [no_vars]}
- \]
- which says: if the image of injective function @{text "f"} over set @{text "A"} is
- finite, then @{text "A"} must be finte.
- *}
+ The basic idea to show the finiteness of the partition induced by relation @{text "\<approx>Lang"}
+ is to attach a tag @{text "tag(x)"} to every string @{text "x"}, the set of tags are carfully
+ choosen, so that the range of tagging function @{text "tag"} (denoted @{text "range(tag)"}) is finite.
+ If strings with the same tag are equivlent with respect @{text "\<approx>Lang"},
+ i.e. @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} (this property is named `injectivity' in the following),
+ then it can be proved that: the partition given rise by @{text "(\<approx>Lang)"} is finite.
+
+ There are two arguments for this. The first goes as the following:
+ \begin{enumerate}
+ \item First, the tagging function @{text "tag"} induces an equivalent relation @{text "(=tag=)"}
+ (defiintion of @{text "f_eq_rel"} and lemma @{text "equiv_f_eq_rel"}).
+ \item It is shown that: if the range of @{text "tag"} is finite,
+ the partition given rise by @{text "(=tag=)"} is finite (lemma @{text "finite_eq_f_rel"}).
+ \item It is proved that if equivalent relation @{text "R1"} is more refined than @{text "R2"}
+ (expressed as @{text "R1 \<subseteq> R2"}),
+ and the partition induced by @{text "R1"} is finite, then the partition induced by @{text "R2"}
+ is finite as well (lemma @{text "refined_partition_finite"}).
+ \item The injectivity assumption @{text "tag(x) = tag(y) \<Longrightarrow> x \<approx>Lang y"} implies that
+ @{text "(=tag=)"} is more refined than @{text "(\<approx>Lang)"}.
+ \item Combining the points above, we have: the partition induced by language @{text "Lang"}
+ is finite (lemma @{text "tag_finite_imageD"}).
+ \end{enumerate}
+*}
-
+definition
+ f_eq_rel ("=_=")
+where
+ "(=f=) = {(x, y) | x y. f x = f y}"
-(* I am trying to reduce the following proof to even simpler principles. But not yet succeed. *)
-definition
- f_eq_rel ("\<cong>_")
-where
- "\<cong>(f::'a \<Rightarrow> 'b) = {(x, y) | x y. f x = f y}"
-
-thm finite.induct
+lemma equiv_f_eq_rel:"equiv UNIV (=f=)"
+ by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)
lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)"
by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def)
-lemma "equiv UNIV (\<cong>f)"
- by (auto simp:equiv_def f_eq_rel_def refl_on_def sym_def trans_def)
-
-lemma
+lemma finite_eq_f_rel:
assumes rng_fnt: "finite (range tag)"
- shows "finite (UNIV // (\<cong>tag))"
+ shows "finite (UNIV // (=tag=))"
proof -
- let "?f" = "op ` tag" and ?A = "(UNIV // (\<cong>tag))"
+ let "?f" = "op ` tag" and ?A = "(UNIV // (=tag=))"
show ?thesis
proof (rule_tac f = "?f" and A = ?A in finite_imageD)
-- {*
@@ -68,7 +73,7 @@
qed
next
-- {*
- The injectivity of @{text "f"}-image is a consequence of the definition of @{text "\<cong>tag"}
+ The injectivity of @{text "f"}-image is a consequence of the definition of @{text "(=tag=)"}:
*}
show "inj_on ?f ?A"
proof-
@@ -79,8 +84,10 @@
have "X = Y"
proof -
from X_in Y_in tag_eq
- obtain x y where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"
- unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def f_eq_rel_def
+ obtain x y
+ where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"
+ unfolding quotient_def Image_def str_eq_rel_def
+ str_eq_def image_def f_eq_rel_def
apply simp by blast
with X_in Y_in show ?thesis
by (auto simp:quotient_def str_eq_rel_def str_eq_def f_eq_rel_def)
@@ -90,23 +97,114 @@
qed
qed
+lemma finite_image_finite: "\<lbrakk>\<forall> x \<in> A. f x \<in> B; finite B\<rbrakk> \<Longrightarrow> finite (f ` A)"
+ by (rule finite_subset [of _ B], auto)
-(*
-lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)"
- by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def)
-*)
+lemma refined_partition_finite:
+ fixes R1 R2 A
+ assumes fnt: "finite (A // R1)"
+ and refined: "R1 \<subseteq> R2"
+ and eq1: "equiv A R1" and eq2: "equiv A R2"
+ shows "finite (A // R2)"
+proof -
+ let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}"
+ and ?A = "(A // R2)" and ?B = "(A // R1)"
+ show ?thesis
+ proof(rule_tac f = ?f and A = ?A in finite_imageD)
+ show "finite (?f ` ?A)"
+ proof(rule finite_subset [of _ "Pow ?B"])
+ from fnt show "finite (Pow (A // R1))" by simp
+ next
+ from eq2
+ show " ?f ` A // R2 \<subseteq> Pow ?B"
+ apply (unfold image_def Pow_def quotient_def, auto)
+ by (rule_tac x = xb in bexI, simp,
+ unfold equiv_def sym_def refl_on_def, blast)
+ qed
+ next
+ show "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" (is "?L = ?R")
+ have "X = Y" using X_in
+ proof(rule quotientE)
+ fix x
+ assume "X = R2 `` {x}" and "x \<in> A" with eq2
+ have x_in: "x \<in> X"
+ by (unfold equiv_def quotient_def refl_on_def, auto)
+ with eq_f have "R1 `` {x} \<in> ?R" by auto
+ then obtain y where
+ y_in: "y \<in> Y" and eq_r: "R1 `` {x} = R1 ``{y}" by auto
+ have "(x, y) \<in> R1"
+ proof -
+ from x_in X_in y_in Y_in eq2
+ have "x \<in> A" and "y \<in> A"
+ by (unfold equiv_def quotient_def refl_on_def, auto)
+ from eq_equiv_class_iff [OF eq1 this] and eq_r
+ show ?thesis by simp
+ qed
+ with refined have xy_r2: "(x, y) \<in> R2" by auto
+ from quotient_eqI [OF eq2 X_in Y_in x_in y_in this]
+ show ?thesis .
+ qed
+ } thus ?thesis by (auto simp:inj_on_def)
+ qed
+ qed
+qed
+
+lemma equiv_lang_eq: "equiv UNIV (\<approx>Lang)"
+ apply (unfold equiv_def str_eq_rel_def sym_def refl_on_def trans_def)
+ by blast
lemma tag_finite_imageD:
- fixes L :: "lang"
+ fixes tag
assumes rng_fnt: "finite (range tag)"
- -- {* Suppose the range of tagging fucntion @{text "tag"} is finite. *}
- and same_tag_eqvt: "\<And> m n. tag m = tag n \<Longrightarrow> m \<approx>L n"
+ -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *}
+ and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n"
-- {* And strings with same tag are equivalent *}
- shows "finite (UNIV // \<approx>L)"
- -- {* Then the partition generated by @{text "\<approx>L"} is finite. *}
+ shows "finite (UNIV // (\<approx>Lang))"
+proof -
+ let ?R1 = "(=tag=)"
+ show ?thesis
+ proof(rule_tac refined_partition_finite [of _ ?R1])
+ from finite_eq_f_rel [OF rng_fnt]
+ show "finite (UNIV // =tag=)" .
+ next
+ from same_tag_eqvt
+ show "(=tag=) \<subseteq> (\<approx>Lang)"
+ by (auto simp:f_eq_rel_def str_eq_def)
+ next
+ from equiv_f_eq_rel
+ show "equiv UNIV (=tag=)" by blast
+ next
+ from equiv_lang_eq
+ show "equiv UNIV (\<approx>Lang)" by blast
+ qed
+qed
+
+text {*
+ A more concise, but less intelligible argument for @{text "tag_finite_imageD"}
+ is given as the following. The basic idea is still using standard library
+ lemma @{thm [source] "finite_imageD"}:
+ \[
+ @{thm "finite_imageD" [no_vars]}
+ \]
+ which says: if the image of injective function @{text "f"} over set @{text "A"} is
+ finite, then @{text "A"} must be finte, as we did in the lemmas above.
+ *}
+
+lemma
+ fixes tag
+ assumes rng_fnt: "finite (range tag)"
+ -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *}
+ and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>Lang n"
+ -- {* And strings with same tag are equivalent *}
+ shows "finite (UNIV // (\<approx>Lang))"
+ -- {* Then the partition generated by @{text "(\<approx>Lang)"} is finite. *}
proof -
-- {* The particular @{text "f"} and @{text "A"} used in @{thm [source] "finite_imageD"} are:*}
- let "?f" = "op ` tag" and ?A = "(UNIV // \<approx>L)"
+ let "?f" = "op ` tag" and ?A = "(UNIV // \<approx>Lang)"
show ?thesis
proof (rule_tac f = "?f" and A = ?A in finite_imageD)
-- {*
@@ -136,7 +234,7 @@
obtain x y where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"
unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def
apply simp by blast
- from same_tag_eqvt [OF eq_tg] have "x \<approx>L y" .
+ from same_tag_eqvt [OF eq_tg] have "x \<approx>Lang y" .
with X_in Y_in x_in y_in
show ?thesis by (auto simp:quotient_def str_eq_rel_def str_eq_def)
qed
@@ -148,33 +246,18 @@
subsection {* Lemmas for basic cases *}
text {*
- The the final result of this direction is in @{text "rexp_imp_finite"},
- which is an induction on the structure of regular expressions. There is one
- case for each regular expression operator. For basic operators such as
- @{const NULL}, @{const EMPTY}, @{const CHAR}, the finiteness of their
- language partition can be established directly with no need of tagging.
- This section contains several technical lemma for these base cases.
-
- The inductive cases involve operators @{const ALT}, @{const SEQ} and @{const
- STAR}. Tagging functions need to be defined individually for each of
- them. There will be one dedicated section for each of these cases, and each
- section goes virtually the same way: gives definition of the tagging
- function and prove that strings with the same tag are equivalent.
-*}
+ The the final result of this direction is in @{text "easier_direction"}, which
+ is an induction on the structure of regular expressions. There is one case
+ for each regular expression operator. For basic operators such as @{text "NULL, EMPTY, CHAR c"},
+ the finiteness of their language partition can be established directly with no need
+ of taggiing. This section contains several technical lemma for these base cases.
-subsection {* The case for @{const "NULL"} *}
-
-lemma quot_null_eq:
- shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"
- unfolding quotient_def Image_def str_eq_rel_def by auto
-
-lemma quot_null_finiteI [intro]:
- shows "finite ((UNIV // \<approx>{})::lang set)"
-unfolding quot_null_eq by simp
-
-
-subsection {* The case for @{const "EMPTY"} *}
-
+ The inductive cases involve operators @{text "ALT, SEQ"} and @{text "STAR"}.
+ Tagging functions need to be defined individually for each of them. There will be one
+ dedicated section for each of these cases, and each section goes virtually the same way:
+ gives definition of the tagging function and prove that strings
+ with the same tag are equivalent.
+ *}
lemma quot_empty_subset:
"UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
@@ -183,25 +266,18 @@
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 - {[]}}"
+ show "x \<in> {{[]}, UNIV - {[]}}"
proof (cases "y = []")
case True with h
- have "x = {[]}" by (auto simp: str_eq_rel_def)
+ 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)
+ 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)
-
-
-subsection {* The case for @{const "CHAR"} *}
-
lemma quot_char_subset:
"UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
proof
@@ -227,18 +303,17 @@
qed
qed
-lemma quot_char_finiteI [intro]:
- shows "finite (UNIV // (\<approx>{[c]}))"
-by (rule finite_subset[OF quot_char_subset]) (simp)
-
-
-subsection {* The case for @{const SEQ}*}
+subsection {* The case for @{text "SEQ"}*}
definition
- tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
-where
- "tag_str_SEQ L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))"
+ "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv>
+ ((\<approx>L\<^isub>1) `` {x}, {(\<approx>L\<^isub>2) `` {x - xa}| xa. xa \<le> x \<and> xa \<in> L\<^isub>1})"
+lemma tag_str_seq_range_finite:
+ "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk>
+ \<Longrightarrow> finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))"
+apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (Pow (UNIV // \<approx>L\<^isub>2))" in finite_subset)
+by (auto simp:tag_str_SEQ_def Image_def quotient_def split:if_splits)
lemma append_seq_elim:
assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"
@@ -306,71 +381,52 @@
qed
} thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n"
by (auto simp add: str_eq_def str_eq_rel_def)
-qed
+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
+lemma quot_seq_finiteI:
+ "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk>
+ \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1 ;; L\<^isub>2))"
+ apply (rule_tac tag = "tag_str_SEQ L\<^isub>1 L\<^isub>2" in tag_finite_imageD)
+ by (auto intro:tag_str_SEQ_injI elim:tag_str_seq_range_finite)
-
-subsection {* The case for @{const ALT} *}
+subsection {* The case for @{text "ALT"} *}
definition
- tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
-where
- "tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"
-
+ "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
-lemma quot_union_finiteI [intro]:
- fixes L1 L2::"lang"
- assumes finite1: "finite (UNIV // \<approx>L1)"
- and finite2: "finite (UNIV // \<approx>L2)"
- shows "finite (UNIV // \<approx>(L1 \<union> L2))"
-proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD)
- show "\<And>x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \<Longrightarrow> x \<approx>(L1 \<union> L2) y"
- unfolding tag_str_ALT_def
- unfolding str_eq_def
- unfolding Image_def
- unfolding str_eq_rel_def
- by auto
+lemma quot_union_finiteI:
+ assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))"
+ and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
+ shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
+proof (rule_tac tag = "tag_str_ALT L\<^isub>1 L\<^isub>2" in tag_finite_imageD)
+ show "\<And>m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 \<union> L\<^isub>2) n"
+ unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto
next
- have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))"
- using finite1 finite2 by auto
- show "finite (range (tag_str_ALT L1 L2))"
- unfolding tag_str_ALT_def
- apply(rule finite_subset[OF _ *])
- unfolding quotient_def
- by auto
+ show "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" using finite1 finite2
+ apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" in finite_subset)
+ by (auto simp:tag_str_ALT_def Image_def quotient_def)
qed
-subsection {* The case for @{const "STAR"} *}
+subsection {*
+ The case for @{text "STAR"}
+ *}
text {*
This turned out to be the trickiest case.
- *} (* I will make some illustrations for it. *)
+ Any string @{text "x"} in language @{text "L\<^isub>1\<star>"},
+ can be splited into a prefix @{text "xa \<in> L\<^isub>1\<star>"} and a suffix @{text "x - xa \<in> L\<^isub>1"}.
+ For one such @{text "x"}, there can be many such splits. The tagging of @{text "x"} is then
+ defined by collecting the @{text "L\<^isub>1"}-state of the suffixes from every possible split.
+ *}
+
+(* I will make some illustrations for it. *)
definition
- tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
-where
- "tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
+ "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<star>}"
-
-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))"
+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
@@ -394,24 +450,62 @@
qed
qed
+
+text {* Technical lemma. *}
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)
+text {*
+ The following lemma @{text "tag_str_star_range_finite"} establishes the range finiteness
+ of the tagging function.
+ *}
+lemma tag_str_star_range_finite:
+ "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (range (tag_str_STAR L\<^isub>1))"
+apply (rule_tac B = "Pow (UNIV // \<approx>L\<^isub>1)" in finite_subset)
+by (auto simp:tag_str_STAR_def Image_def
+ quotient_def split:if_splits)
+
+text {*
+ The following lemma @{text "tag_str_STAR_injI"} establishes the injectivity of
+ the tagging function for case @{text "STAR"}.
+ *}
+
lemma tag_str_STAR_injI:
- "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
+ fixes v w
+ assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
+ shows "(v::string) \<approx>(L\<^isub>1\<star>) w"
proof-
+ -- {*
+ \begin{minipage}{0.9\textwidth}
+ According to the definition of @{text "\<approx>Lang"},
+ proving @{text "v \<approx>(L\<^isub>1\<star>) w"} amounts to
+ showing: for any string @{text "u"},
+ if @{text "v @ u \<in> (L\<^isub>1\<star>)"} then @{text "w @ u \<in> (L\<^isub>1\<star>)"} and vice versa.
+ The reasoning pattern for both directions are the same, as derived
+ in the following:
+ \end{minipage}
+ *}
{ 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"
+ 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 = []")
+ -- {*
+ The degenerated case when @{text "x"} is a null string is easy to prove:
+ *}
case True
with tag_xy have "y = []"
by (auto simp:tag_str_STAR_def strict_prefix_def)
thus ?thesis using xz_in_star True by simp
next
+ -- {*
+ \begin{minipage}{0.9\textwidth}
+ The case when @{text "x"} is not null, and
+ @{text "x @ z"} is in @{text "L\<^isub>1\<star>"},
+ \end{minipage}
+ *}
case False
obtain x_max
where h1: "x_max < x"
@@ -478,36 +572,163 @@
qed
with h5 h6 show ?thesis
by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)
- qed
- } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
- by (auto simp add:str_eq_def str_eq_rel_def)
+ qed
+ }
+ -- {* By instantiating the reasoning pattern just derived for both directions:*}
+ from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
+ -- {* The thesis is proved as a trival consequence: *}
+ show ?thesis by (unfold str_eq_def str_eq_rel_def, blast)
qed
-lemma quot_star_finiteI [intro]:
- fixes L1::"lang"
- 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)
+lemma quot_star_finiteI:
+ "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1\<star>))"
+ apply (rule_tac tag = "tag_str_STAR L\<^isub>1" in tag_finite_imageD)
+ by (auto intro:tag_str_STAR_injI elim:tag_str_star_range_finite)
+
+subsection {*
+ The main lemma
+ *}
+
+lemma easier_direction:
+ "Lang = L (r::rexp) \<Longrightarrow> finite (UNIV // (\<approx>Lang))"
+proof (induct arbitrary:Lang rule:rexp.induct)
+ case NULL
+ have "UNIV // (\<approx>{}) \<subseteq> {UNIV} "
+ by (auto simp:quotient_def str_eq_rel_def str_eq_def)
+ with prems show "?case" by (auto intro:finite_subset)
+next
+ case EMPTY
+ have "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
+ by (rule quot_empty_subset)
+ with prems show ?case by (auto intro:finite_subset)
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
-
-
-subsection {* The main lemma *}
-
-lemma rexp_imp_finite:
- fixes r::"rexp"
- shows "finite (UNIV // \<approx>(L r))"
-by (induct r) (auto)
-
+ case (CHAR c)
+ have "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
+ by (rule quot_char_subset)
+ with prems show ?case by (auto intro:finite_subset)
+next
+ case (SEQ r\<^isub>1 r\<^isub>2)
+ have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk>
+ \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 ;; L r\<^isub>2))"
+ by (erule quot_seq_finiteI, simp)
+ with prems show ?case by simp
+next
+ case (ALT r\<^isub>1 r\<^isub>2)
+ have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk>
+ \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 \<union> L r\<^isub>2))"
+ by (erule quot_union_finiteI, simp)
+ with prems show ?case by simp
+next
+ case (STAR r)
+ have "finite (UNIV // \<approx>(L r))
+ \<Longrightarrow> finite (UNIV // \<approx>((L r)\<star>))"
+ by (erule quot_star_finiteI)
+ with prems show ?case by simp
+qed
end
+(*
+lemma refined_quotient_union_eq:
+ assumes refined: "R1 \<subseteq> R2"
+ and eq1: "equiv A R1" and eq2: "equiv A R2"
+ and y_in: "y \<in> A"
+ shows "\<Union>{R1 `` {x} | x. x \<in> (R2 `` {y})} = R2 `` {y}"
+proof
+ show "\<Union>{R1 `` {x} |x. x \<in> R2 `` {y}} \<subseteq> R2 `` {y}" (is "?L \<subseteq> ?R")
+ proof -
+ { fix z
+ assume zl: "z \<in> ?L" and nzr: "z \<notin> ?R"
+ have "False"
+ proof -
+ from zl and eq1 eq2 and y_in
+ obtain x where xy2: "(x, y) \<in> R2" and zx1: "(z, x) \<in> R1"
+ by (simp only:equiv_def sym_def, blast)
+ have "(z, y) \<in> R2"
+ proof -
+ from zx1 and refined have "(z, x) \<in> R2" by blast
+ moreover from xy2 have "(x, y) \<in> R2" .
+ ultimately show ?thesis using eq2
+ by (simp only:equiv_def, unfold trans_def, blast)
+ qed
+ with nzr eq2 show ?thesis by (auto simp:equiv_def sym_def)
+ qed
+ } thus ?thesis by blast
+ qed
+next
+ show "R2 `` {y} \<subseteq> \<Union>{R1 `` {x} |x. x \<in> R2 `` {y}}" (is "?L \<subseteq> ?R")
+ proof
+ fix x
+ assume x_in: "x \<in> ?L"
+ with eq1 eq2 have "x \<in> R1 `` {x}"
+ by (unfold equiv_def refl_on_def, auto)
+ with x_in show "x \<in> ?R" by auto
+ qed
+qed
+*)
+
+(*
+lemma refined_partition_finite:
+ fixes R1 R2 A
+ assumes fnt: "finite (A // R1)"
+ and refined: "R1 \<subseteq> R2"
+ and eq1: "equiv A R1" and eq2: "equiv A R2"
+ shows "finite (A // R2)"
+proof -
+ let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}"
+ and ?A = "(A // R2)" and ?B = "(A // R1)"
+ show ?thesis
+ proof(rule_tac f = ?f and A = ?A in finite_imageD)
+ show "finite (?f ` ?A)"
+ proof(rule finite_subset [of _ "Pow ?B"])
+ from fnt show "finite (Pow (A // R1))" by simp
+ next
+ from eq2
+ show " ?f ` A // R2 \<subseteq> Pow ?B"
+ apply (unfold image_def Pow_def quotient_def, auto)
+ by (rule_tac x = xb in bexI, simp,
+ unfold equiv_def sym_def refl_on_def, blast)
+ qed
+ next
+ show "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" (is "?L = ?R")
+ hence "X = Y"
+ proof -
+ from X_in eq2
+ obtain x
+ where x_in: "x \<in> A"
+ and eq_x: "X = R2 `` {x}" (is "X = ?X")
+ by (unfold quotient_def equiv_def refl_on_def, auto)
+ from Y_in eq2 obtain y
+ where y_in: "y \<in> A"
+ and eq_y: "Y = R2 `` {y}" (is "Y = ?Y")
+ by (unfold quotient_def equiv_def refl_on_def, auto)
+ have "?X = ?Y"
+ proof -
+ from eq_f have "\<Union> ?L = \<Union> ?R" by auto
+ moreover have "\<Union> ?L = ?X"
+ proof -
+ from eq_x have "\<Union> ?L = \<Union>{R1 `` {x} |x. x \<in> ?X}" by simp
+ also from refined_quotient_union_eq [OF refined eq1 eq2 x_in]
+ have "\<dots> = ?X" .
+ finally show ?thesis .
+ qed
+ moreover have "\<Union> ?R = ?Y"
+ proof -
+ from eq_y have "\<Union> ?R = \<Union>{R1 `` {y} |y. y \<in> ?Y}" by simp
+ also from refined_quotient_union_eq [OF refined eq1 eq2 y_in]
+ have "\<dots> = ?Y" .
+ finally show ?thesis .
+ qed
+ ultimately show ?thesis by simp
+ qed
+ with eq_x eq_y show ?thesis by auto
+ qed
+ } thus ?thesis by (auto simp:inj_on_def)
+ qed
+ qed
+qed
+*)