--- a/Myhill.thy Fri Jan 28 12:53:01 2011 +0000
+++ b/Myhill.thy Fri Jan 28 19:17:40 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)"
@@ -245,19 +245,19 @@
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.
+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
- 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_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 - {[]}}"
@@ -266,18 +266,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
@@ -303,17 +310,19 @@
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 @{text "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"
@@ -383,33 +392,55 @@
by (auto simp add: str_eq_def str_eq_rel_def)
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.
@@ -417,12 +448,14 @@
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 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>})"
+
+
text {* A technical lemma. *}
lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow>
@@ -457,15 +490,6 @@
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
@@ -580,51 +604,28 @@
show ?thesis by (unfold str_eq_def str_eq_rel_def, blast)
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_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)
+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
+
+
+lemma rexp_imp_finite:
+ fixes r::"rexp"
+ shows "finite (UNIV // \<approx>(L r))"
+by (induct r) (auto)
end