regexp: comparison Myhill

equal deleted inserted replaced

-:560712a29a36
+:c4893e84c88e
 abbreviation
 tag_eq_applied :: "'a list \<Rightarrow> ('a list \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> bool" ("_ =_= _")
 where
 "x =tag= y \<equiv> (x, y) \<in> =tag="
-lemma test:
+lemma [simp]:
 shows "(\<approx>A) `` {x} = (\<approx>A) `` {y} \<longleftrightarrow> x \<approx>A y"
-unfolding str_eq_def
+unfolding str_eq_def by auto
-by auto
+lemma refined_intro:
-lemma test_refined_intro:
 assumes "\<And>x y z. \<lbrakk>x =tag= y; x @ z \<in> A\<rbrakk> \<Longrightarrow> y @ z \<in> A"
 shows "=tag= \<subseteq> \<approx>A"
-using assms
+using assms unfolding str_eq_def tag_eq_def
-unfolding str_eq_def tag_eq_def
 apply(clarify, simp (no_asm_use))
 by metis
 lemma finite_eq_tag_rel:
 assumes rng_fnt: "finite (range tag)"
 ultimately show "finite (UNIV // R2)" by (rule finite_imageD)
 qed
 lemma tag_finite_imageD:
 assumes rng_fnt: "finite (range tag)"
-and same_tag_eqvt: "\<And>m n. tag m = tag n \<Longrightarrow> m \<approx>A n"
+and same_tag_eqvt: "=tag=  \<subseteq> \<approx>A"
 shows "finite (UNIV // \<approx>A)"
 proof (rule_tac refined_partition_finite [of "=tag="])
 show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
 next
 from same_tag_eqvt
-show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_def str_eq_def
+show "=tag= \<subseteq> \<approx>A" .
-by blast
 next
 show "equiv UNIV =tag="
 unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def
 by auto
 next
 subsubsection {* The inductive case for @{const Plus} *}
 definition
 tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
 where
-"tag_Plus A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
+"tag_Plus A B \<equiv> \<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x})"
 lemma quot_plus_finiteI [intro]:
 assumes finite1: "finite (UNIV // \<approx>A)"
 and     finite2: "finite (UNIV // \<approx>B)"
 shows "finite (UNIV // \<approx>(A \<union> B))"
 using finite1 finite2 by auto
 then show "finite (range (tag_Plus A B))"
 unfolding tag_Plus_def quotient_def
 by (rule rev_finite_subset) (auto)
 next
-show "\<And>x y. tag_Plus A B x = tag_Plus A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
+show "=tag_Plus A B= \<subseteq> \<approx>(A \<union> B)"
-unfolding tag_Plus_def
+unfolding tag_eq_def tag_Plus_def str_eq_def by auto
-unfolding str_eq_def
+qed
-by auto
-qed
+subsubsection {* The inductive case for @{text "Times"} *}
-subsubsection {* The inductive case for @{text "Times"}*}
 definition
 "Partitions s \<equiv> {(u, v). u @ v = s}"
 lemma conc_partitions_elim:
 assumes "x \<in> A \<cdot> B"
 shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B"
-using assms
+using assms unfolding conc_def Partitions_def
-unfolding conc_def Partitions_def
 by auto
 lemma conc_partitions_intro:
 assumes "(u, v) \<in> Partitions x \<and> u \<in> A \<and>  v \<in> B"
 shows "x \<in> A \<cdot> B"
-using assms
+using assms unfolding conc_def Partitions_def
-unfolding conc_def Partitions_def
 by auto
 lemma equiv_class_member:
 assumes "x \<in> A"
 and "\<approx>A `` {x} = \<approx>A `` {y}"
 shows "y \<in> A"
 using assms
-apply(simp add: Image_def str_eq_def set_eq_iff)
+apply(simp)
+apply(simp add: str_eq_def)
 apply(metis append_Nil2)
 done
 abbreviation
 where "(x = u @ us \<and> us @ z = v) \<or> (x @ us = u \<and> z = us @ v)"
 by (auto simp add: append_eq_append_conv2)
 moreover
 { assume eq: "x = u @ us" "us @ z = v"
 have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B x"
-unfolding Partitions_def using eq by auto
+unfolding Partitions_def using eq by (auto simp add: str_eq_def)
 then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B y"
 using b by simp
 then obtain u' us' where
 q1: "\<approx>A `` {u} = \<approx>A `` {u'}" and
 q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and
 }
 ultimately show "y @ z \<in> A \<cdot> B" by blast
 qed
 lemma quot_conc_finiteI [intro]:
-fixes A B::"'a lang"
 assumes fin1: "finite (UNIV // \<approx>A)"
 and     fin2: "finite (UNIV // \<approx>B)"
 shows "finite (UNIV // \<approx>(A \<cdot> B))"
 proof (rule_tac tag = "tag_Times A B" in tag_finite_imageD)
-have "=(tag_Times A B)= \<subseteq> \<approx>(A \<cdot> B)"
+have "\<And>x y z. \<lbrakk>tag_Times A B x = tag_Times A B y; x @ z \<in> A \<cdot> B\<rbrakk> \<Longrightarrow> y @ z \<in> A \<cdot> B"
-apply(rule test_refined_intro)
+by (rule tag_Times_injI)
-apply(rule tag_Times_injI)
+(auto simp add: tag_Times_def tag_eq_def)
-prefer 3
+then show "=tag_Times A B= \<subseteq> \<approx>(A \<cdot> B)"
-apply(assumption)
+by (rule refined_intro)
-apply(simp add: tag_Times_def tag_eq_def)
+(auto simp add: tag_eq_def)
-apply(simp add: tag_eq_def tag_Times_def)
-done
-then show "\<And>x y. tag_Times A B x = tag_Times A B y \<Longrightarrow> x \<approx>(A \<cdot> B) y"
-unfolding tag_eq_def by auto
 next
 have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>A \<times> UNIV // \<approx>B)))"
 using fin1 fin2 by auto
 show "finite (range (tag_Times A B))"
 unfolding tag_Times_def
 qed
 subsubsection {* The inductive case for @{const "Star"} *}
-lemma append_eq_append_conv3:
+lemma star_partitions_elim:
-assumes "xs @ ys = zs @ ts" "zs < xs"
-shows "\<exists>us. xs = zs @ us \<and> us @ ys = ts"
-using assms
-apply(auto simp add: append_eq_append_conv2 strict_prefix_def)
-done
-lemma star_spartitions_elim:
 assumes "x @ z \<in> A\<star>" "x \<noteq> []"
 shows "\<exists>(u, v) \<in> Partitions (x @ z). u < x \<and> u \<in> A\<star> \<and> v \<in> A\<star>"
 proof -
 have "([], x @ z) \<in> Partitions (x @ z)" "[] < x" "[] \<in> A\<star>" "x @ z \<in> A\<star>"
 using assms by (auto simp add: Partitions_def strict_prefix_def)
 then show "\<exists>(u, v) \<in> Partitions (x @ z). u < x \<and> u \<in> A\<star> \<and> v \<in> A\<star>"
 by blast
 qed
 lemma finite_set_has_max2:
 "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max"
 apply(induct rule:finite.induct)
 apply(simp)
 moreover
 have "u_max @ a \<in> A\<star>" using i2 h2 by simp
 moreover
 have "as @ z \<in> A\<star>" using i1' i2 i3 eq by auto
 ultimately have "length (u_max @ a) \<le> length u_max" using h4 by blast
-moreover
+with i4 show "False" by auto
-have "a \<noteq> []" using i4 .
-ultimately show "False" by auto
 qed
 with i1 obtain za zb
 where k1: "v @ za = a"
 and   k2: "(za, zb) \<in> Partitions z"
 and   k4: "zb = b"
 unfolding Partitions_def prefix_def
 by (auto simp add: append_eq_append_conv2)
 show "\<exists> (u, v) \<in> Partitions x. \<exists> (u', v') \<in> Partitions z. u < x \<and> u \<in> A\<star> \<and> v @ u' \<in> A \<and> v' \<in> A\<star>"
-using h0 k2 h1 h2 i2 k1 i3 k4 unfolding Partitions_def by blast
+using h0 h1 h2 i2 i3 k1 k2 k4 unfolding Partitions_def by blast
 qed
 definition
 tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
 where
 "tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {v} | u v. u < x \<and> u \<in> A\<star> \<and> (u, v) \<in> Partitions x})"
+lemma tag_Star_non_empty_injI:
-lemma tag_Star_injI:
-fixes x::"'a list"
 assumes a: "tag_Star A x = tag_Star A y"
 and     c: "x @ z \<in> A\<star>"
 and     d: "x \<noteq> []"
 shows "y @ z \<in> A\<star>"
-using c d
+proof -
-apply(drule_tac star_spartitions_elim2)
+obtain u v u' v'
-apply(simp)
+where a1: "(u,  v) \<in> Partitions x" "(u', v')\<in> Partitions z"
-apply(simp add: Partitions_def)
+and   a2: "u < x"
-apply(erule exE | erule conjE)+
+and   a3: "u \<in> A\<star>"
-apply(subgoal_tac "((\<approx>A) `` {b}) \<in> tag_Star A x")
+and   a4: "v @ u' \<in> A"
-apply(simp add: a)
+and   a5: "v' \<in> A\<star>"
-apply(simp add: tag_Star_def)
+using c d by (auto dest: star_spartitions_elim2)
-apply(erule exE | erule conjE)+
+have "(\<approx>A) `` {v} \<in> tag_Star A x"
-apply(simp add: test)
+apply(simp add: tag_Star_def Partitions_def str_eq_def)
-apply(simp add: Partitions_def)
+using a1 a2 a3 by (auto simp add: Partitions_def)
-apply(subgoal_tac "v @ aa \<in> A\<star>")
+then have "(\<approx>A) `` {v} \<in> tag_Star A y" using a by simp
-prefer 2
+then obtain u1 v1
-apply(simp add: str_eq_def)
+where b1: "v \<approx>A v1"
-apply(subgoal_tac "(u @ v) @ aa @ ba \<in> A\<star>")
+and   b3: "u1 \<in> A\<star>"
-apply(simp)
+and   b4: "(u1, v1) \<in> Partitions y"
-apply(simp (no_asm_use))
+unfolding tag_Star_def by auto
-apply(rule append_in_starI)
+have c: "v1 @ u' \<in> A\<star>" using b1 a4 unfolding str_eq_def by simp
-apply(simp)
+have "u1 @ (v1 @ u') @ v' \<in> A\<star>"
-apply(simp (no_asm) only: append_assoc[symmetric])
+using b3 c a5 by (simp only: append_in_starI)
-apply(rule append_in_starI)
+then show "y @ z \<in> A\<star>" using b4 a1
-apply(simp)
+unfolding Partitions_def by auto
-apply(simp)
+qed
-apply(simp add: tag_Star_def)
-apply(rule_tac x="a" in exI)
+lemma tag_Star_empty_injI:
-apply(rule_tac x="b" in exI)
-apply(simp)
-apply(simp add: Partitions_def)
-done
-lemma tag_Star_injI2:
-fixes x::"'a list"
 assumes a: "tag_Star A x = tag_Star A y"
 and     c: "x @ z \<in> A\<star>"
 and     d: "x = []"
 shows "y @ z \<in> A\<star>"
-using c d
+using assms
 apply(simp)
-using a
 apply(simp add: tag_Star_def strict_prefix_def)
 apply(auto simp add: prefix_def Partitions_def)
 by (metis Nil_in_star append_self_conv2)
 lemma quot_star_finiteI [intro]:
-fixes A::"('a::finite) lang"
 assumes finite1: "finite (UNIV // \<approx>A)"
 shows "finite (UNIV // \<approx>(A\<star>))"
 proof (rule_tac tag = "tag_Star A" in tag_finite_imageD)
-have "=(tag_Star A)= \<subseteq> \<approx>(A\<star>)"
+have "\<And>x y z. \<lbrakk>tag_Star A x = tag_Star A y; x @ z \<in> A\<star>\<rbrakk> \<Longrightarrow> y @ z \<in> A\<star>"
-apply(rule test_refined_intro)
+by (case_tac "x = []") (blast intro: tag_Star_empty_injI tag_Star_non_empty_injI)+
-apply(case_tac "x=[]")
+then show "=(tag_Star A)= \<subseteq> \<approx>(A\<star>)"
-apply(rule tag_Star_injI2)
+by (rule refined_intro) (auto simp add: tag_eq_def)
-prefer 3
-apply(assumption)
-prefer 2
-apply(assumption)
-apply(simp add: tag_eq_def)
-apply(rule tag_Star_injI)
-prefer 3
-apply(assumption)
-prefer 2
-apply(assumption)
-unfolding tag_eq_def
-apply(simp)
-done
-then show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
-apply(simp add: tag_eq_def)
-apply(auto)
-done
 next
 have *: "finite (Pow (UNIV // \<approx>A))"
 using finite1 by auto
 show "finite (range (tag_Star A))"
 unfolding tag_Star_def
-apply(rule finite_subset[OF _ *])
+by (rule finite_subset[OF _ *])
-unfolding quotient_def
+(auto simp add: quotient_def)
-apply(auto)
-done
 qed
 subsubsection{* The conclusion *}
 lemma Myhill_Nerode2:
-fixes r::"('a::finite) rexp"
+fixes r::"'a rexp"
 shows "finite (UNIV // \<approx>(lang r))"
 by (induct r) (auto)
 theorem Myhill_Nerode:
 fixes A::"('a::finite) lang"

changeset 183	c4893e84c88e
parent 182	560712a29a36
child 184	2455db3b06ac