--- a/Myhill.thy Wed Feb 02 06:05:12 2011 +0000
+++ b/Myhill.thy Wed Feb 02 13:25:09 2011 +0000
@@ -258,7 +258,6 @@
Each case is given in a separate section, as well as the final main lemma. Detailed explainations accompanied by
illustrations are given for non-trivial cases.
-
For ever inductive case, there are two tasks, the easier one is to show the range finiteness of
of the tagging function based on the finiteness of component partitions, the
difficult one is to show that strings with the same tag are equivalent with respect to the
@@ -483,7 +482,7 @@
qed
-- {* Now, @{text "ya"} has all properties to be a qualified candidate:*}
with pref_ya ya_in
- show ?thesis using prems by blast
+ show ?thesis using that by blast
qed
-- {* From the properties of @{text "ya"}, @{text "y @ z \<in> L\<^isub>1 ;; L\<^isub>2"} is derived easily.*}
hence "y @ z \<in> L\<^isub>1 ;; L\<^isub>2" by (erule_tac prefixE, auto simp:Seq_def)
@@ -592,7 +591,8 @@
case True thus ?thesis by (rule_tac x = a in bexI, auto)
next
case False
- with prems obtain max
+ with insertI.hyps and False
+ obtain max
where h1: "max \<in> A"
and h2: "\<forall>a\<in>A. f a \<le> f max" by blast
show ?thesis
@@ -679,8 +679,8 @@
by (auto simp:tag_str_STAR_def)
moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto
ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp
- with prems show ?thesis apply
- (simp add:Image_def str_eq_rel_def str_eq_def) by blast
+ thus ?thesis using that
+ apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast
qed
-- {*
\begin{minipage}{0.8\textwidth}
@@ -745,8 +745,8 @@
-- {* Now candidates @{text "?za"} and @{text "?zb"} have all the requred properteis. *}
with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1"
by (auto simp:str_eq_def str_eq_rel_def)
- with eq_z and b_in prems
- show ?thesis by blast
+ with eq_z and b_in
+ show ?thesis using that by blast
qed
-- {*
@{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}:
@@ -764,7 +764,6 @@
show ?thesis unfolding str_eq_def str_eq_rel_def by blast
qed
-
lemma -- {* The oringal version with less explicit details. *}
fixes v w
assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_STAR L\<^isub>1 w"
@@ -815,7 +814,7 @@
by (simp, rule_tac x = "[]" in exI, auto simp:strict_prefix_def)
ultimately have "\<exists> max \<in> ?S. \<forall> a \<in> ?S. length a \<le> length max"
using finite_set_has_max by blast
- with prems show ?thesis by blast
+ thus ?thesis using that by blast
qed
obtain ya
where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>" and h7: "(x - x_max) \<approx>L\<^isub>1 (y - ya)"
@@ -825,7 +824,7 @@
by (auto simp:tag_str_STAR_def)
moreover have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?left" using h1 h2 by auto
ultimately have "\<approx>L\<^isub>1 `` {x - x_max} \<in> ?right" by simp
- with prems show ?thesis apply
+ with that show ?thesis apply
(simp add:Image_def str_eq_rel_def str_eq_def) by blast
qed
have "(y - ya) @ z \<in> L\<^isub>1\<star>"
@@ -898,110 +897,4 @@
shows "finite (UNIV // \<approx>(L r))"
by (induct r) (auto)
-
end
-
-(*
-lemma refined_quotient_union_eq:
- assumes refined: "R1 \<subseteq> R2"
- and eq1: "equiv A R1" and eq2: "equiv A R2"
- and y_in: "y \<in> A"
- shows "\<Union>{R1 `` {x} | x. x \<in> (R2 `` {y})} = R2 `` {y}"
-proof
- show "\<Union>{R1 `` {x} |x. x \<in> R2 `` {y}} \<subseteq> R2 `` {y}" (is "?L \<subseteq> ?R")
- proof -
- { fix z
- assume zl: "z \<in> ?L" and nzr: "z \<notin> ?R"
- have "False"
- proof -
- from zl and eq1 eq2 and y_in
- obtain x where xy2: "(x, y) \<in> R2" and zx1: "(z, x) \<in> R1"
- by (simp only:equiv_def sym_def, blast)
- have "(z, y) \<in> R2"
- proof -
- from zx1 and refined have "(z, x) \<in> R2" by blast
- moreover from xy2 have "(x, y) \<in> R2" .
- ultimately show ?thesis using eq2
- by (simp only:equiv_def, unfold trans_def, blast)
- qed
- with nzr eq2 show ?thesis by (auto simp:equiv_def sym_def)
- qed
- } thus ?thesis by blast
- qed
-next
- show "R2 `` {y} \<subseteq> \<Union>{R1 `` {x} |x. x \<in> R2 `` {y}}" (is "?L \<subseteq> ?R")
- proof
- fix x
- assume x_in: "x \<in> ?L"
- with eq1 eq2 have "x \<in> R1 `` {x}"
- by (unfold equiv_def refl_on_def, auto)
- with x_in show "x \<in> ?R" by auto
- qed
-qed
-*)
-
-(*
-lemma refined_partition_finite:
- fixes R1 R2 A
- assumes fnt: "finite (A // R1)"
- and refined: "R1 \<subseteq> R2"
- and eq1: "equiv A R1" and eq2: "equiv A R2"
- shows "finite (A // R2)"
-proof -
- let ?f = "\<lambda> X. {R1 `` {x} | x. x \<in> X}"
- and ?A = "(A // R2)" and ?B = "(A // R1)"
- show ?thesis
- proof(rule_tac f = ?f and A = ?A in finite_imageD)
- show "finite (?f ` ?A)"
- proof(rule finite_subset [of _ "Pow ?B"])
- from fnt show "finite (Pow (A // R1))" by simp
- next
- from eq2
- show " ?f ` A // R2 \<subseteq> Pow ?B"
- apply (unfold image_def Pow_def quotient_def, auto)
- by (rule_tac x = xb in bexI, simp,
- unfold equiv_def sym_def refl_on_def, blast)
- qed
- next
- show "inj_on ?f ?A"
- proof -
- { fix X Y
- assume X_in: "X \<in> ?A" and Y_in: "Y \<in> ?A"
- and eq_f: "?f X = ?f Y" (is "?L = ?R")
- hence "X = Y"
- proof -
- from X_in eq2
- obtain x
- where x_in: "x \<in> A"
- and eq_x: "X = R2 `` {x}" (is "X = ?X")
- by (unfold quotient_def equiv_def refl_on_def, auto)
- from Y_in eq2 obtain y
- where y_in: "y \<in> A"
- and eq_y: "Y = R2 `` {y}" (is "Y = ?Y")
- by (unfold quotient_def equiv_def refl_on_def, auto)
- have "?X = ?Y"
- proof -
- from eq_f have "\<Union> ?L = \<Union> ?R" by auto
- moreover have "\<Union> ?L = ?X"
- proof -
- from eq_x have "\<Union> ?L = \<Union>{R1 `` {x} |x. x \<in> ?X}" by simp
- also from refined_quotient_union_eq [OF refined eq1 eq2 x_in]
- have "\<dots> = ?X" .
- finally show ?thesis .
- qed
- moreover have "\<Union> ?R = ?Y"
- proof -
- from eq_y have "\<Union> ?R = \<Union>{R1 `` {y} |y. y \<in> ?Y}" by simp
- also from refined_quotient_union_eq [OF refined eq1 eq2 y_in]
- have "\<dots> = ?Y" .
- finally show ?thesis .
- qed
- ultimately show ?thesis by simp
- qed
- with eq_x eq_y show ?thesis by auto
- qed
- } thus ?thesis by (auto simp:inj_on_def)
- qed
- qed
-qed
-*)