# HG changeset patch
# User urbanc
# Date 1296147491 0
# Node ID cb4403fabda7138006884a758487e25bbb46121f
# Parent  f809cb54de4e54e6873af1947a04984d183e4aa8
added my changes again

diff -r f809cb54de4e -r cb4403fabda7 Myhill.thy
--- 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
 
diff -r f809cb54de4e -r cb4403fabda7 Myhill_1.thy
--- a/Myhill_1.thy	Thu Jan 27 12:35:06 2011 +0000
+++ b/Myhill_1.thy	Thu Jan 27 16:58:11 2011 +0000
@@ -1,5 +1,5 @@
 theory Myhill_1
-  imports Main List_Prefix Prefix_subtract
+  imports Main List_Prefix Prefix_subtract Prelude
 begin
 
 (*
@@ -26,15 +26,20 @@
 
 section {* Preliminary definitions *}
 
-text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *}
+types lang = "string set"
+
+text {* 
+  Sequential composition of two languages @{text "L1"} and @{text "L2"} 
+*}
+
 definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 where 
   "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
 
 text {* Transitive closure of language @{text "L"}. *}
 inductive_set
-  Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102)
-  for L :: "string set"
+  Star :: "lang \<Rightarrow> lang" ("_\<star>" [101] 102)
+  for L 
 where
   start[intro]: "[] \<in> L\<star>"
 | step[intro]:  "\<lbrakk>s1 \<in> L; s2 \<in> L\<star>\<rbrakk> \<Longrightarrow> s1@s2 \<in> L\<star>" 
@@ -193,7 +198,7 @@
   *}
 lemma folds_alt_simp [simp]:
   "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply (rule set_ext, simp add:folds_def)
+apply (rule set_eq_intro, simp add:folds_def)
 apply (rule someI2_ex, erule finite_imp_fold_graph)
 by (erule fold_graph.induct, auto)
 
@@ -206,7 +211,7 @@
   @{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)}"
 
diff -r f809cb54de4e -r cb4403fabda7 tphols-2011/myhill.pdf
Binary file tphols-2011/myhill.pdf has changed