# HG changeset patch
# User urbanc
# Date 1296242260 0
# Node ID bea2466a6084245d7e24041d6a772994d01c605f
# Parent  28d70591042a7b03fbd367090400aedf173fed3c
slightly tuned the main lemma and the finiteness proofs

diff -r 28d70591042a -r bea2466a6084 Myhill.thy
--- 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