--- a/Myhill.thy Thu Jan 27 12:35:06 2011 +0000
+++ b/Myhill.thy Thu Jan 27 16:58:11 2011 +0000
@@ -13,7 +13,7 @@
*}
definition
- str_eq ("_ \<approx>_ _")
+ str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
where
"x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"
@@ -33,7 +33,6 @@
*}
-(*
(* I am trying to reduce the following proof to even simpler principles. But not yet succeed. *)
definition
@@ -91,22 +90,23 @@
qed
qed
-*)
+(*
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 tag_finite_imageD:
- fixes tag
+ fixes L :: "lang"
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"
+ -- {* 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"
-- {* And strings with same tag are equivalent *}
- shows "finite (UNIV // (\<approx>lang))"
- -- {* Then the partition generated by @{text "(\<approx>lang)"} is finite. *}
+ shows "finite (UNIV // \<approx>L)"
+ -- {* Then the partition generated by @{text "\<approx>L"} 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>lang)"
+ let "?f" = "op ` tag" and ?A = "(UNIV // \<approx>L)"
show ?thesis
proof (rule_tac f = "?f" and A = ?A in finite_imageD)
-- {*
@@ -136,7 +136,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>lang y" .
+ from same_tag_eqvt [OF eq_tg] have "x \<approx>L 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,18 +148,33 @@
subsection {* Lemmas for basic cases *}
text {*
- 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.
+ 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 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.
- *}
+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"} *}
+
lemma quot_empty_subset:
"UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
@@ -168,18 +183,25 @@
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
@@ -205,17 +227,18 @@
qed
qed
-subsection {* The case for @{text "SEQ"}*}
+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}*}
definition
- "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})"
+ 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}))"
-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"
@@ -283,45 +306,71 @@
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:
- "\<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)
+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
-subsection {* The case for @{text "ALT"} *}
+
+subsection {* The case for @{const ALT} *}
definition
- "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
+ 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}))"
+
-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
+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
next
- 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)
+ 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
qed
-subsection {*
- The case for @{text "STAR"}
- *}
+subsection {* The case for @{const "STAR"} *}
text {*
This turned out to be the trickiest case.
*} (* I will make some illustrations for it. *)
definition
- "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<star>}"
+ 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>})"
-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))"
+
+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
@@ -350,13 +399,6 @@
apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
by (auto simp:strict_prefix_def)
-
-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)
-
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"
proof-
@@ -441,51 +483,31 @@
by (auto simp add:str_eq_def str_eq_rel_def)
qed
-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_directio\<nu>:
- "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)
+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)
next
- 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
+ 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)
+
end