theory Myhill_2
imports Myhill_1 Prefix_subtract
"~~/src/HOL/Library/List_Prefix"
begin
section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
definition
tag_eq :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=")
where
"=tag= \<equiv> {(x, y). tag x = tag y}"
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:
shows "(\<approx>A) `` {x} = (\<approx>A) `` {y} \<longleftrightarrow> x \<approx>A y"
unfolding str_eq_def
by auto
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
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)"
shows "finite (UNIV // =tag=)"
proof -
let "?f" = "\<lambda>X. tag ` X" and ?A = "(UNIV // =tag=)"
have "finite (?f ` ?A)"
proof -
have "range ?f \<subseteq> (Pow (range tag))" unfolding Pow_def by auto
moreover
have "finite (Pow (range tag))" using rng_fnt by simp
ultimately
have "finite (range ?f)" unfolding image_def by (blast intro: finite_subset)
moreover
have "?f ` ?A \<subseteq> range ?f" by auto
ultimately show "finite (?f ` ?A)" by (rule rev_finite_subset)
qed
moreover
have "inj_on ?f ?A"
proof -
{ fix X Y
assume X_in: "X \<in> ?A"
and Y_in: "Y \<in> ?A"
and tag_eq: "?f X = ?f Y"
then obtain x y
where "x \<in> X" "y \<in> Y" "tag x = tag y"
unfolding quotient_def Image_def image_def tag_eq_def
by (simp) (blast)
with X_in Y_in
have "X = Y"
unfolding quotient_def tag_eq_def by auto
}
then show "inj_on ?f ?A" unfolding inj_on_def by auto
qed
ultimately show "finite (UNIV // =tag=)" by (rule finite_imageD)
qed
lemma refined_partition_finite:
assumes fnt: "finite (UNIV // R1)"
and refined: "R1 \<subseteq> R2"
and eq1: "equiv UNIV R1" and eq2: "equiv UNIV R2"
shows "finite (UNIV // R2)"
proof -
let ?f = "\<lambda>X. {R1 `` {x} | x. x \<in> X}"
and ?A = "UNIV // R2" and ?B = "UNIV // R1"
have "?f ` ?A \<subseteq> Pow ?B"
unfolding image_def Pow_def quotient_def by auto
moreover
have "finite (Pow ?B)" using fnt by simp
ultimately
have "finite (?f ` ?A)" by (rule finite_subset)
moreover
have "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"
from quotientE [OF X_in]
obtain x where "X = R2 `` {x}" by blast
with equiv_class_self[OF eq2] have x_in: "x \<in> X" by simp
then have "R1 ``{x} \<in> ?f X" by auto
with eq_f have "R1 `` {x} \<in> ?f Y" by simp
then obtain y
where y_in: "y \<in> Y" and eq_r1_xy: "R1 `` {x} = R1 `` {y}" by auto
with eq_equiv_class[OF _ eq1]
have "(x, y) \<in> R1" by blast
with refined have "(x, y) \<in> R2" by auto
with quotient_eqI [OF eq2 X_in Y_in x_in y_in]
have "X = Y" .
}
then show "inj_on ?f ?A" unfolding inj_on_def by blast
qed
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"
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
next
show "equiv UNIV =tag="
unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def
by auto
next
show "equiv UNIV (\<approx>A)"
unfolding equiv_def str_eq_def sym_def refl_on_def trans_def
by blast
qed
subsection {* The proof *}
subsubsection {* The base case for @{const "Zero"} *}
lemma quot_zero_eq:
shows "UNIV // \<approx>{} = {UNIV}"
unfolding quotient_def Image_def str_eq_def by auto
lemma quot_zero_finiteI [intro]:
shows "finite (UNIV // \<approx>{})"
unfolding quot_zero_eq by simp
subsubsection {* The base case for @{const "One"} *}
lemma quot_one_subset:
shows "UNIV // \<approx>{[]} \<subseteq> {{[]}, UNIV - {[]}}"
proof
fix x
assume "x \<in> UNIV // \<approx>{[]}"
then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}"
unfolding quotient_def Image_def by blast
show "x \<in> {{[]}, UNIV - {[]}}"
proof (cases "y = []")
case True with h
have "x = {[]}" by (auto simp: str_eq_def)
thus ?thesis by simp
next
case False with h
have "x = UNIV - {[]}" by (auto simp: str_eq_def)
thus ?thesis by simp
qed
qed
lemma quot_one_finiteI [intro]:
shows "finite (UNIV // \<approx>{[]})"
by (rule finite_subset[OF quot_one_subset]) (simp)
subsubsection {* The base case for @{const "Atom"} *}
lemma quot_atom_subset:
"UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
proof
fix x
assume "x \<in> UNIV // \<approx>{[c]}"
then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[c]}}"
unfolding quotient_def Image_def by blast
show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}"
proof -
{ assume "y = []" hence "x = {[]}" using h
by (auto simp: str_eq_def) }
moreover
{ assume "y = [c]" hence "x = {[c]}" using h
by (auto dest!: spec[where x = "[]"] simp: str_eq_def) }
moreover
{ assume "y \<noteq> []" and "y \<noteq> [c]"
hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto)
moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])"
by (case_tac p, auto)
ultimately have "x = UNIV - {[],[c]}" using h
by (auto simp add: str_eq_def)
}
ultimately show ?thesis by blast
qed
qed
lemma quot_atom_finiteI [intro]:
shows "finite (UNIV // \<approx>{[c]})"
by (rule finite_subset[OF quot_atom_subset]) (simp)
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}))"
lemma quot_plus_finiteI [intro]:
assumes finite1: "finite (UNIV // \<approx>A)"
and finite2: "finite (UNIV // \<approx>B)"
shows "finite (UNIV // \<approx>(A \<union> B))"
proof (rule_tac tag = "tag_Plus A B" in tag_finite_imageD)
have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>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"
unfolding tag_Plus_def
unfolding str_eq_def
by auto
qed
subsubsection {* The inductive case for @{text "Times"}*}
definition
"Partitions s \<equiv> {(u, v). u @ v = s}"
lemma conc_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
by auto
lemma conc_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
by auto
lemma y:
"\<lbrakk>x \<in> A; x \<approx>A y\<rbrakk> \<Longrightarrow> y \<in> A"
apply(simp add: str_eq_def)
apply(drule_tac x="[]" in spec)
apply(simp)
done
definition
tag_Times3a :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang"
where
"tag_Times3a A B \<equiv> (\<lambda>x. \<approx>A `` {x})"
definition
tag_Times3b :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set"
where
"tag_Times3b A B \<equiv>
(\<lambda>x. ({(\<approx>A `` {u}, \<approx>B `` {v}) | u v. (u, v) \<in> Partitions x}))"
definition
tag_Times3 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set"
where
"tag_Times3 A B \<equiv>
(\<lambda>x. (tag_Times3a A B x, tag_Times3b A B x))"
lemma
assumes a: "tag_Times3a A B x = tag_Times3a A B y"
and b: "tag_Times3b A B x = tag_Times3b A B y"
and c: "x @ z \<in> A \<cdot> B"
shows "y @ z \<in> A \<cdot> B"
proof -
from c obtain u v where
h1: "(u, v) \<in> Partitions (x @ z)" and
h2: "u \<in> A" and
h3: "v \<in> B" by (auto dest: conc_elim)
from h1 have "x @ z = u @ v" unfolding Partitions_def by simp
then obtain us
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_Times3b A B x"
unfolding tag_Times3b_def Partitions_def using eq by auto
then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times3b 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
q3: "(u', us') \<in> Partitions y"
by (auto simp add: tag_Times3b_def)
from q1 h2 have "u' \<in> A"
using y unfolding Image_def str_eq_def by blast
moreover from q2 h3 eq
have "us' @ z \<in> B"
unfolding Image_def str_eq_def by auto
ultimately have "y @ z \<in> A \<cdot> B" using q3
unfolding Partitions_def by auto
}
moreover
{ assume eq: "x @ us = u" "z = us @ v"
have "(\<approx>A `` {x}) = tag_Times3a A B x"
unfolding tag_Times3a_def by simp
then have "(\<approx>A `` {x}) = tag_Times3a A B y"
using a by simp
then have "\<approx>A `` {x} = \<approx>A `` {y}"
unfolding tag_Times3a_def by simp
moreover
have "x @ us \<in> A" using h2 eq by simp
ultimately
have "y @ us \<in> A" using y
unfolding Image_def str_eq_def by blast
then have "(y @ us) @ v \<in> A \<cdot> B"
using h3 unfolding conc_def by blast
then have "y @ z \<in> A \<cdot> B" using eq by simp
}
ultimately show "y @ z \<in> A \<cdot> B" by blast
qed
lemma conc_in_cases2:
assumes "x @ z \<in> A \<cdot> B"
shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or>
(\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"
using assms
unfolding conc_def prefix_def
by (auto simp add: append_eq_append_conv2)
definition
tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)"
where
"tag_Times A B \<equiv>
(\<lambda>x. (\<approx>A `` {x}, {(\<approx>B `` {x - x'}) | x'. x' \<le> x \<and> x' \<in> A}))"
lemma tag_Times_injI:
assumes eq_tag: "tag_Times A B x = tag_Times A B y"
shows "x \<approx>(A \<cdot> B) y"
proof -
{ fix x y z
assume xz_in_seq: "x @ z \<in> A \<cdot> B"
and tag_xy: "tag_Times A B x = tag_Times A B y"
have"y @ z \<in> A \<cdot> B"
proof -
{ (* first case with x' in A and (x - x') @ z in B *)
fix x'
assume h1: "x' \<le> x" and h2: "x' \<in> A" and h3: "(x - x') @ z \<in> B"
obtain y'
where "y' \<le> y"
and "y' \<in> A"
and "(y - y') @ z \<in> B"
proof -
have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} =
{\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right")
using tag_xy unfolding tag_Times_def by simp
moreover
have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto
ultimately
have "\<approx>B `` {x - x'} \<in> ?Right" by simp
then obtain y'
where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"
and pref_y': "y' \<le> y" and y'_in: "y' \<in> A"
by simp blast
have "(x - x') \<approx>B (y - y')" using eq_xy'
unfolding Image_def str_eq_def by auto
with h3 have "(y - y') @ z \<in> B"
unfolding str_eq_def by simp
with pref_y' y'_in
show ?thesis using that by blast
qed
then have "y @ z \<in> A \<cdot> B"
unfolding prefix_def by auto
}
moreover
{ (* second case with x @ z' in A and z - z' in B *)
fix z'
assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B"
have "\<approx>A `` {x} = \<approx>A `` {y}"
using tag_xy unfolding tag_Times_def by simp
with h2 have "y @ z' \<in> A"
unfolding Image_def str_eq_def by auto
with h1 h3 have "y @ z \<in> A \<cdot> B"
unfolding prefix_def conc_def
by (auto) (metis append_assoc)
}
ultimately show "y @ z \<in> A \<cdot> B"
using conc_in_cases2 [OF xz_in_seq] by blast
qed
}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def 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)
show "\<And>x y. tag_Times A B x = tag_Times A B y \<Longrightarrow> x \<approx>(A \<cdot> B) y"
by (rule tag_Times_injI)
next
have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"
using fin1 fin2 by auto
show "finite (range (tag_Times A B))"
unfolding tag_Times_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
by auto
qed
subsubsection {* The inductive case for @{const "Star"} *}
definition
"SPartitions s \<equiv> {(u, v). u @ v = s \<and> u < s}"
lemma
assumes "x \<in> A\<star>" "x \<noteq> []"
shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v \<in> A\<star>"
using assms
apply(subst (asm) star_unfold_left)
apply(simp)
apply(simp add: conc_def)
apply(erule exE)+
apply(erule conjE)+
apply(rule_tac x="([], xs @ ys)" in bexI)
apply(simp)
apply(simp add: SPartitions_def)
apply(auto)
apply (metis append_Cons list.exhaust strict_prefix_simps(2))
by (metis Nil_is_append_conv Nil_prefix xt1(11))
lemma
assumes "x @ z \<in> A\<star>" "x \<noteq> []"
shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v @ z \<in> A\<star>"
using assms
apply(subst (asm) star_unfold_left)
apply(simp)
apply(simp add: conc_def)
apply(erule exE)+
apply(erule conjE)+
apply(rule_tac x="([], x)" in bexI)
apply(simp)
apply(simp add: SPartitions_def)
by (metis Nil_prefix xt1(11))
lemma finite_set_has_max:
"\<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)
by (metis (full_types) all_not_in_conv insertI1 insert_iff linorder_linear order_eq_iff order_trans prefix_length_le)
definition
tag_Star3 :: "'a lang \<Rightarrow> 'a list \<Rightarrow> (bool \<times> 'a lang) set"
where
"tag_Star3 A \<equiv>
(\<lambda>x. ({(u \<in> A\<star>, \<approx>A `` {v}) | u v. (u, v) \<in> Partitions x}))"
definition
tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
where
"tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {x - xa} | xa. xa < x \<and> xa \<in> A\<star>})"
text {* A technical lemma. *}
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))"
proof (induct rule:finite.induct)
case emptyI thus ?case by simp
next
case (insertI A a)
show ?case
proof (cases "A = {}")
case True thus ?thesis by (rule_tac x = a in bexI, auto)
next
case False
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"
with h1 h2 show ?thesis by (rule_tac x = max in bexI, auto)
next
assume "\<not> (f a \<le> f max)"
thus ?thesis using h2 by (rule_tac x = a in bexI, auto)
qed
qed
qed
text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *}
lemma finite_strict_prefix_set:
shows "finite {xa. xa < (x::'a list)}"
apply (induct x rule:rev_induct, simp)
apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
by (auto simp:strict_prefix_def)
lemma tag_Star_injI:
fixes L\<^isub>1::"('a::finite) lang"
assumes eq_tag: "tag_Star L\<^isub>1 v = tag_Star L\<^isub>1 w"
shows "v \<approx>(L\<^isub>1\<star>) w"
proof-
{ fix x y z
assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>"
and tag_xy: "tag_Star L\<^isub>1 x = tag_Star L\<^isub>1 y"
have "y @ z \<in> L\<^isub>1\<star>"
proof(cases "x = []")
case True
with tag_xy have "y = []"
by (auto simp add: tag_Star_def strict_prefix_def)
thus ?thesis using xz_in_star True by simp
next
case False
let ?S = "{xa::('a::finite) list. xa < x \<and> xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>}"
have "finite ?S"
by (rule_tac B = "{xa. xa < x}" in finite_subset)
(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> xa_max \<in> ?S. \<forall> xa \<in> ?S. length xa \<le> length xa_max"
using finite_set_has_max by blast
then obtain xa_max
where h1: "xa_max < x"
and h2: "xa_max \<in> L\<^isub>1\<star>"
and h3: "(x - xa_max) @ z \<in> L\<^isub>1\<star>"
and h4:"\<forall> xa < x. xa \<in> L\<^isub>1\<star> \<and> (x - xa) @ z \<in> L\<^isub>1\<star>
\<longrightarrow> length xa \<le> length xa_max"
by blast
obtain ya
where h5: "ya < y" and h6: "ya \<in> L\<^isub>1\<star>"
and eq_xya: "(x - xa_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_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
thus ?thesis using that
apply (simp add: Image_def str_eq_def) by blast
qed
have "(y - ya) @ z \<in> L\<^isub>1\<star>"
proof-
obtain za zb where eq_zab: "z = za @ zb"
and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"
proof -
from h1 have "(x - xa_max) @ z \<noteq> []"
unfolding strict_prefix_def prefix_def by auto
from star_decom [OF h3 this]
obtain a b where a_in: "a \<in> L\<^isub>1"
and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>"
and ab_max: "(x - xa_max) @ z = a @ b" by blast
let ?za = "a - (x - xa_max)" and ?zb = "b"
have pfx: "(x - xa_max) \<le> a" (is "?P1")
and eq_z: "z = ?za @ ?zb" (is "?P2")
proof -
have "((x - xa_max) \<le> a \<and> (a - (x - xa_max)) @ b = z) \<or>
(a < (x - xa_max) \<and> ((x - xa_max) - a) @ z = b)"
using append_eq_dest[OF ab_max] by (auto simp:strict_prefix_def)
moreover {
assume np: "a < (x - xa_max)"
and b_eqs: "((x - xa_max) - a) @ z = b"
have "False"
proof -
let ?xa_max' = "xa_max @ a"
have "?xa_max' < x"
using np h1 by (clarsimp simp:strict_prefix_def diff_prefix)
moreover have "?xa_max' \<in> L\<^isub>1\<star>"
using a_in h2 by (auto)
moreover have "(x - ?xa_max') @ z \<in> L\<^isub>1\<star>"
using b_eqs b_in np h1 by (simp add:diff_diff_append)
moreover have "\<not> (length ?xa_max' \<le> length xa_max)"
using a_neq by simp
ultimately show ?thesis using h4 by blast
qed }
ultimately show ?P1 and ?P2 by auto
qed
hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in unfolding prefix_def by auto
with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1"
by (auto simp: str_eq_def)
with eq_z and b_in
show ?thesis using that by blast
qed
have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb
by (rule_tac append_in_starI) (auto)
with eq_zab show ?thesis by simp
qed
with h5 h6 show ?thesis
unfolding strict_prefix_def prefix_def by auto
qed
}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
show ?thesis unfolding str_eq_def by blast
qed
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)
show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
by (rule tag_Star_injI)
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
by auto
qed
subsubsection{* The conclusion *}
lemma Myhill_Nerode2:
fixes r::"('a::finite) rexp"
shows "finite (UNIV // \<approx>(lang r))"
by (induct r) (auto)
theorem Myhill_Nerode:
fixes A::"('a::finite) lang"
shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
using Myhill_Nerode1 Myhill_Nerode2 by auto
end