# HG changeset patch
# User wu
# Date 1296106759 0
# Node ID 50d00d7dc4137521087f7b009c3e7032f3fbf78a
# Parent  a59473f0229da2b8616e5bca70eb0c54aa7601eb
tuned a bit more the last STAR-proof

diff -r a59473f0229d -r 50d00d7dc413 Myhill.thy
--- a/Myhill.thy	Thu Jan 27 00:51:46 2011 +0000
+++ b/Myhill.thy	Thu Jan 27 05:39:19 2011 +0000
@@ -1279,14 +1279,9 @@
 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})"
-
-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)
+  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 append_seq_elim:
   assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"
@@ -1357,10 +1352,22 @@
 qed 
 
 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)
+  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 @{const "ALT"} *}
@@ -1384,7 +1391,8 @@
     unfolding str_eq_rel_def
     by auto
 next
-  have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))" using finite1 finite2 by auto
+  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 _ *])
@@ -1400,7 +1408,9 @@
   *} (* 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))"
@@ -1432,13 +1442,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-
@@ -1523,10 +1526,23 @@
     by (auto simp add:str_eq_def str_eq_rel_def)
 qed
 
+
 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)
+  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
+  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 *}
diff -r a59473f0229d -r 50d00d7dc413 tphols-2011/myhill.pdf
Binary file tphols-2011/myhill.pdf has changed