--- a/Myhill_2.thy Tue Aug 02 15:27:37 2011 +0000
+++ b/Myhill_2.thy Wed Aug 03 00:52:41 2011 +0000
@@ -15,16 +15,14 @@
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
-by auto
+unfolding str_eq_def by auto
-lemma test_refined_intro:
+lemma 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
-unfolding str_eq_def tag_eq_def
+using assms unfolding str_eq_def tag_eq_def
apply(clarify, simp (no_asm_use))
by metis
@@ -103,14 +101,13 @@
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
- by blast
+ show "=tag= \<subseteq> \<approx>A" .
next
show "equiv UNIV =tag="
unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def
@@ -199,7 +196,7 @@
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)"
@@ -212,14 +209,12 @@
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"
- unfolding tag_Plus_def
- unfolding str_eq_def
- by auto
+ show "=tag_Plus A B= \<subseteq> \<approx>(A \<union> B)"
+ unfolding tag_eq_def tag_Plus_def str_eq_def 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}"
@@ -227,15 +222,13 @@
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
-unfolding conc_def Partitions_def
+using assms 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
-unfolding conc_def Partitions_def
+using assms unfolding conc_def Partitions_def
by auto
lemma equiv_class_member:
@@ -243,7 +236,8 @@
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
@@ -280,7 +274,7 @@
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
@@ -314,21 +308,16 @@
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)"
- apply(rule test_refined_intro)
- apply(rule tag_Times_injI)
- prefer 3
- apply(assumption)
- apply(simp add: tag_Times_def 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
+ 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"
+ by (rule tag_Times_injI)
+ (auto simp add: tag_Times_def tag_eq_def)
+ then show "=tag_Times A B= \<subseteq> \<approx>(A \<cdot> B)"
+ by (rule refined_intro)
+ (auto simp add: tag_eq_def)
next
have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>A \<times> UNIV // \<approx>B)))"
using fin1 fin2 by auto
@@ -342,14 +331,7 @@
subsubsection {* The inductive case for @{const "Star"} *}
-lemma append_eq_append_conv3:
- 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:
+lemma star_partitions_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 -
@@ -359,7 +341,6 @@
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)
@@ -422,9 +403,7 @@
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
- have "a \<noteq> []" using i4 .
- ultimately show "False" by auto
+ with i4 show "False" by auto
qed
with i1 obtain za zb
where k1: "v @ za = a"
@@ -433,107 +412,75 @@
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_injI:
- fixes x::"'a list"
+lemma tag_Star_non_empty_injI:
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
-apply(drule_tac star_spartitions_elim2)
-apply(simp)
-apply(simp add: Partitions_def)
-apply(erule exE | erule conjE)+
-apply(subgoal_tac "((\<approx>A) `` {b}) \<in> tag_Star A x")
-apply(simp add: a)
-apply(simp add: tag_Star_def)
-apply(erule exE | erule conjE)+
-apply(simp add: test)
-apply(simp add: Partitions_def)
-apply(subgoal_tac "v @ aa \<in> A\<star>")
-prefer 2
-apply(simp add: str_eq_def)
-apply(subgoal_tac "(u @ v) @ aa @ ba \<in> A\<star>")
-apply(simp)
-apply(simp (no_asm_use))
-apply(rule append_in_starI)
-apply(simp)
-apply(simp (no_asm) only: append_assoc[symmetric])
-apply(rule append_in_starI)
-apply(simp)
-apply(simp)
-apply(simp add: tag_Star_def)
-apply(rule_tac x="a" in exI)
-apply(rule_tac x="b" in exI)
-apply(simp)
-apply(simp add: Partitions_def)
-done
-
-lemma tag_Star_injI2:
- fixes x::"'a list"
+proof -
+ obtain u v u' v'
+ where a1: "(u, v) \<in> Partitions x" "(u', v')\<in> Partitions z"
+ and a2: "u < x"
+ and a3: "u \<in> A\<star>"
+ and a4: "v @ u' \<in> A"
+ and a5: "v' \<in> A\<star>"
+ using c d by (auto dest: star_spartitions_elim2)
+ have "(\<approx>A) `` {v} \<in> tag_Star A x"
+ apply(simp add: tag_Star_def Partitions_def str_eq_def)
+ using a1 a2 a3 by (auto simp add: Partitions_def)
+ then have "(\<approx>A) `` {v} \<in> tag_Star A y" using a by simp
+ then obtain u1 v1
+ where b1: "v \<approx>A v1"
+ and b3: "u1 \<in> A\<star>"
+ and b4: "(u1, v1) \<in> Partitions y"
+ unfolding tag_Star_def by auto
+ have c: "v1 @ u' \<in> A\<star>" using b1 a4 unfolding str_eq_def by simp
+ have "u1 @ (v1 @ u') @ v' \<in> A\<star>"
+ using b3 c a5 by (simp only: append_in_starI)
+ then show "y @ z \<in> A\<star>" using b4 a1
+ unfolding Partitions_def by auto
+qed
+
+lemma tag_Star_empty_injI:
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>)"
- apply(rule test_refined_intro)
- apply(case_tac "x=[]")
- apply(rule tag_Star_injI2)
- 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
+ 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>"
+ by (case_tac "x = []") (blast intro: tag_Star_empty_injI tag_Star_non_empty_injI)+
+ then show "=(tag_Star A)= \<subseteq> \<approx>(A\<star>)"
+ by (rule refined_intro) (auto simp add: tag_eq_def)
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 _ *])
- unfolding quotient_def
- apply(auto)
- done
+ unfolding tag_Star_def
+ by (rule finite_subset[OF _ *])
+ (auto simp add: quotient_def)
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)
@@ -542,4 +489,4 @@
shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
using Myhill_Nerode1 Myhill_Nerode2 by auto
-end
+end
\ No newline at end of file