--- a/Myhill.thy Wed Jan 26 23:39:42 2011 +0000
+++ b/Myhill.thy Thu Jan 27 00:51:46 2011 +0000
@@ -25,8 +25,14 @@
section {* Preliminary definitions *}
-text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *}
-definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
+types lang = "string set"
+
+text {*
+ Sequential composition of two languages @{text "L1"} and @{text "L2"}
+*}
+
+
+definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" ("_ ;; _" [100,100] 100)
where
"L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
@@ -204,8 +210,9 @@
text {*
@{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.
*}
+
definition
- str_eq_rel ("\<approx>_")
+ str_eq_rel ("\<approx>_" [100] 100)
where
"\<approx>Lang \<equiv> {(x, y). (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)}"
@@ -237,6 +244,9 @@
by (drule_tac x = "[]" in spec, auto)
qed
+
+
+
section {* Direction @{text "finite partition \<Rightarrow> regular language"}*}
text {*
@@ -1114,7 +1124,9 @@
finally show ?thesis by blast
qed
-section {* Direction: @{text "regular language \<Rightarrow>finite partition"} *}
+
+
+section {* Direction: @{text "regular language \<Rightarrow> finite partitions"} *}
subsection {* The scheme for this direction *}
@@ -1130,33 +1142,43 @@
"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 tags to every string. The set of tags are carfully choosen to make it 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 reason for this is a lemma
- in standard library (@{text "finite_imageD"}), which says: if the image of an injective
- function on a set @{text "A"} is finite, then @{text "A"} is finite. It can be shown that
- the function obtained by llifting @{text "tag"}
- to the level of equalent classes (i.e. @{text "((op `) tag)"}) is injective
- (by lemma @{text "tag_image_injI"}) and the image of this function is finite
- (with the help of lemma @{text "finite_tag_imageI"}). This argument is formalized
- by the following lemma @{text "tag_finite_imageD"}.
- *}
+ The very basic scheme to show the finiteness of the partion generated by a
+ language @{text "Lang"} is by attaching tags to every string. The set of
+ tags are carefully choosen to make it 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 reason for
+ this is a lemma in standard library (@{text "finite_imageD"}), which says:
+ if the image of an injective function on a set @{text "A"} is finite, then
+ @{text "A"} is finite. It can be shown that the function obtained by
+ lifting @{text "tag"} to the level of equivalence classes (i.e. @{text "((op
+ `) tag)"}) is injective (by lemma @{text "tag_image_injI"}) and the image of
+ this function is finite (with the help of lemma @{text
+ "finite_tag_imageI"}). This argument is formalized by the following lemma
+ @{text "tag_finite_imageD"}.
+
+
+ {\bf
+ Theorems @{text "tag_image_injI"} and @{text
+ "finite_tag_imageI"} do not exist. Can this comment be deleted?
+ \marginpar{\bf COMMENT}
+ }
+*}
lemma tag_finite_imageD:
- assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>lang n"
+ fixes L1::"lang"
+ assumes str_inj: "\<And> m n. tag m = tag n \<Longrightarrow> m \<approx>L1 n"
and range: "finite (range tag)"
- shows "finite (UNIV // (\<approx>lang))"
+ shows "finite (UNIV // \<approx>L1)"
proof (rule_tac f = "(op `) tag" in finite_imageD)
- show "finite (op ` tag ` UNIV // \<approx>lang)" using range
+ show "finite (op ` tag ` UNIV // \<approx>L1)" using range
apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset)
by (auto simp add:image_def Pow_def)
next
- show "inj_on (op ` tag) (UNIV // \<approx>lang)"
+ show "inj_on (op ` tag) (UNIV // \<approx>L1)"
proof-
{ fix X Y
- assume X_in: "X \<in> UNIV // \<approx>lang"
- and Y_in: "Y \<in> UNIV // \<approx>lang"
+ assume X_in: "X \<in> UNIV // \<approx>L1"
+ and Y_in: "Y \<in> UNIV // \<approx>L1"
and tag_eq: "tag ` X = tag ` Y"
then obtain x y where "x \<in> X" and "y \<in> Y" and "tag x = tag y"
unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def
@@ -1170,18 +1192,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 - {[]}}"
@@ -1190,18 +1227,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
@@ -1227,7 +1271,12 @@
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>
@@ -1307,33 +1356,44 @@
by (auto simp add: str_eq_def str_eq_rel_def)
qed
-lemma quot_seq_finiteI:
+lemma quot_seq_finiteI [intro]:
"\<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 @{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.
@@ -1463,51 +1523,19 @@
by (auto simp add:str_eq_def str_eq_rel_def)
qed
-lemma quot_star_finiteI:
+lemma quot_star_finiteI [intro]:
"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
- *}
+
+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)
-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
+lemma rexp_imp_finite:
+ fixes r::"rexp"
+ shows "finite (UNIV // \<approx>(L r))"
+by (induct r) (auto)
+
end
--- a/Paper/Paper.thy Wed Jan 26 23:39:42 2011 +0000
+++ b/Paper/Paper.thy Thu Jan 27 00:51:46 2011 +0000
@@ -1,7 +1,13 @@
(*<*)
theory Paper
-imports "../Myhill"
+imports "../Myhill" "LaTeXsugar"
begin
+
+declare [[show_question_marks = false]]
+
+notation (latex output)
+ str_eq_rel ("\<approx>\<^bsub>_\<^esub>")
+
(*>*)
section {* Introduction *}
@@ -10,6 +16,34 @@
*}
+
+section {* Regular expressions have finitely many partitions *}
+
+text {*
+
+ \begin{lemma}
+ Given @{text "r"} is a regular expressions, then @{thm rexp_imp_finite}.
+ \end{lemma}
+
+ \begin{proof}
+ By induction on the structure of @{text r}. The cases for @{const NULL}, @{const EMPTY}
+ and @{const CHAR} are starightforward, because we can easily establish
+
+ \begin{center}
+ \begin{tabular}{l}
+ @{thm quot_null_eq}\\
+ @{thm quot_empty_subset}\\
+ @{thm quot_char_subset}
+ \end{tabular}
+ \end{center}
+
+
+
+ \end{proof}
+
+*}
+
+
(*<*)
end
(*>*)
\ No newline at end of file
--- a/tphols-2011/ROOT.ML Wed Jan 26 23:39:42 2011 +0000
+++ b/tphols-2011/ROOT.ML Thu Jan 27 00:51:46 2011 +0000
@@ -3,6 +3,6 @@
use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
*)
-no_document use_thys ["../Prefix_subtract"];
+no_document use_thys ["../Prefix_subtract", "../Prelude"];
use_thys ["../Myhill"];
Binary file tphols-2011/myhill.pdf has changed