regexp: comparison Myhill.thy

equal deleted inserted replaced

-:b3898315e687
+:76ab7c09d575
 text {*
 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
 composite language. Suppose the composite language be @{text "Lang"}, tagging function be
 @{text "tag"}, it amounts to show:
 unfolding Image_def str_eq_rel_def str_eq_def by auto
 with h3 show ?thesis unfolding str_eq_rel_def str_eq_def by simp
 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)
 } moreover {
 -- {* The other case is even more simpler: *}
 show ?case
 proof (cases "A = {}")
 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
 proof (cases "f a \<le> f max")
 assume "f a \<le> f max"
 from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} =
 {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")
 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
+thus ?thesis using that
-(simp add:Image_def str_eq_rel_def str_eq_def) by blast
+apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast
 qed
 -- {*
 \begin{minipage}{0.8\textwidth}
 The @{text "?thesis"}, @{prop "y @ z \<in> L\<^isub>1\<star>"}, is a simple consequence
 of the following proposition:
 qed
 hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)
 -- {* 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
+with eq_z and b_in
-show ?thesis by blast
+show ?thesis using that by blast
 qed
 -- {*
 @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}:
 *}
 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using  l_za ls_zb by blast
 -- {* By instantiating the reasoning pattern just derived for both directions:*}
 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
 -- {* The thesis is proved as a trival consequence: *}
 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"
 shows "(v::string) \<approx>(L\<^isub>1\<star>) w"
 auto simp:finite_strict_prefix_set)
 moreover have "?S \<noteq> {}" using False xz_in_star
 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)"
 proof-
 from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} =
 {\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")
 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>"
 proof-
 from h3 h1 obtain a b where a_in: "a \<in> L\<^isub>1"
 lemma rexp_imp_finite:
 fixes r::"rexp"
 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
-*)

changeset 57	76ab7c09d575
parent 56	b3898315e687
child 62	d94209ad2880