# HG changeset patch
# User urbanc
# Date 1296089506 0
# Node ID a59473f0229da2b8616e5bca70eb0c54aa7601eb
# Parent  a1268fb0deea146c2aef855de88c4982bf955641
tuned a little bit the section about finite partitions

diff -r a1268fb0deea -r a59473f0229d Myhill.thy
--- 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
 
diff -r a1268fb0deea -r a59473f0229d Paper/Paper.thy
--- 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
diff -r a1268fb0deea -r a59473f0229d tphols-2011/ROOT.ML
--- 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"];
diff -r a1268fb0deea -r a59473f0229d tphols-2011/myhill.pdf
Binary file tphols-2011/myhill.pdf has changed