# HG changeset patch
# User urbanc
# Date 1312298857 0
# Node ID 560712a29a36cd78a33fb4745964361d67fbe958
# Parent 97090fc7aa9fe850a65adfb0cef95dd81ced3371
a version of the proof which dispenses with the notion of string-subtraction
diff -r 97090fc7aa9f -r 560712a29a36 Attic/Prefix_subtract.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Prefix_subtract.thy Tue Aug 02 15:27:37 2011 +0000
@@ -0,0 +1,60 @@
+theory Prefix_subtract
+ imports Main "~~/src/HOL/Library/List_Prefix"
+begin
+
+
+section {* A small theory of prefix subtraction *}
+
+text {*
+ The notion of @{text "prefix_subtract"} makes
+ the second direction of the Myhill-Nerode theorem
+ more readable.
+*}
+
+instantiation list :: (type) minus
+begin
+
+fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+ "minus_list [] xs = []"
+| "minus_list (x#xs) [] = x#xs"
+| "minus_list (x#xs) (y#ys) = (if x = y then minus_list xs ys else (x#xs))"
+
+instance by default
+
+end
+
+lemma [simp]: "x - [] = x"
+by (induct x) (auto)
+
+lemma [simp]: "(x @ y) - x = y"
+by (induct x) (auto)
+
+lemma [simp]: "x - x = []"
+by (induct x) (auto)
+
+lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y "
+by (induct x) (auto)
+
+lemma diff_prefix:
+ "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"
+by (auto elim: prefixE)
+
+lemma diff_diff_append:
+ "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"
+apply (clarsimp simp:strict_prefix_def)
+by (drule diff_prefix, auto elim:prefixE)
+
+lemma append_eq_cases:
+ assumes a: "x @ y = m @ n"
+ shows "x \<le> m \<or> m \<le> x"
+unfolding prefix_def using a
+by (auto simp add: append_eq_append_conv2)
+
+lemma append_eq_dest:
+ assumes a: "x @ y = m @ n"
+ shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
+using append_eq_cases[OF a] a
+by (auto elim: prefixE)
+
+end
diff -r 97090fc7aa9f -r 560712a29a36 Journal/Paper.thy
--- a/Journal/Paper.thy Sun Jul 31 10:27:41 2011 +0000
+++ b/Journal/Paper.thy Tue Aug 02 15:27:37 2011 +0000
@@ -1,6 +1,6 @@
(*<*)
theory Paper
-imports "../Closures"
+imports "../Closures" "../Attic/Prefix_subtract"
begin
declare [[show_question_marks = false]]
@@ -1290,15 +1290,7 @@
%
\noindent
and \emph{string subtraction}:
- %
- \begin{center}
- \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
- @{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\
- @{text "x - []"} & @{text "\<equiv>"} & @{text "x"}\\
- @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}
- \end{tabular}
- \end{center}
- %
+
\noindent
where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
diff -r 97090fc7aa9f -r 560712a29a36 Myhill_2.thy
--- a/Myhill_2.thy Sun Jul 31 10:27:41 2011 +0000
+++ b/Myhill_2.thy Tue Aug 02 15:27:37 2011 +0000
@@ -1,6 +1,6 @@
theory Myhill_2
- imports Myhill_1 Prefix_subtract
- "~~/src/HOL/Library/List_Prefix"
+ imports Myhill_1
+ "~~/src/HOL/Library/List_Prefix"
begin
section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
@@ -28,7 +28,6 @@
apply(clarify, simp (no_asm_use))
by metis
-
lemma finite_eq_tag_rel:
assumes rng_fnt: "finite (range tag)"
shows "finite (UNIV // =tag=)"
@@ -225,72 +224,71 @@
definition
"Partitions s \<equiv> {(u, v). u @ v = s}"
-lemma conc_elim:
+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
by auto
-lemma conc_intro:
+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
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)
+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(metis append_Nil2)
done
-definition
- tag_Times3a :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang"
+
+abbreviation
+ tag_Times_1 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang"
where
- "tag_Times3a A B \<equiv> (\<lambda>x. \<approx>A `` {x})"
+ "tag_Times_1 A B \<equiv> \<lambda>x. \<approx>A `` {x}"
+
+abbreviation
+ tag_Times_2 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set"
+where
+ "tag_Times_2 A B \<equiv> \<lambda>x. {(\<approx>A `` {u}, \<approx>B `` {v}) | u v. (u, v) \<in> Partitions x}"
definition
- tag_Times3b :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set"
+ tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('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}))"
+ "tag_Times A B \<equiv> \<lambda>x. (tag_Times_1 A B x, tag_Times_2 A B 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"
+lemma tag_Times_injI:
+ assumes a: "tag_Times_1 A B x = tag_Times_1 A B y"
+ and b: "tag_Times_2 A B x = tag_Times_2 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)
+ h3: "v \<in> B" by (auto dest: conc_partitions_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"
+ have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B x"
+ unfolding Partitions_def using eq by auto
+ 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
- q3: "(u', us') \<in> Partitions y"
- by (auto simp add: tag_Times3b_def)
+ q3: "(u', us') \<in> Partitions y" by auto
from q1 h2 have "u' \<in> A"
- using y unfolding Image_def str_eq_def by blast
+ using equiv_class_member by auto
moreover from q2 h3 eq
have "us' @ z \<in> B"
unfolding Image_def str_eq_def by auto
@@ -299,16 +297,14 @@
}
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"
+ have "(\<approx>A `` {x}) = tag_Times_1 A B x" by simp
+ then have "(\<approx>A `` {x}) = tag_Times_1 A B y"
using a by simp
- then have "\<approx>A `` {x} = \<approx>A `` {y}"
- unfolding tag_Times3a_def by simp
+ then have "\<approx>A `` {x} = \<approx>A `` {y}" by simp
moreover
have "x @ us \<in> A" using h2 eq by simp
ultimately
- have "y @ us \<in> A" using y
+ have "y @ us \<in> A" using equiv_class_member
unfolding Image_def str_eq_def by blast
then have "(y @ us) @ v \<in> A \<cdot> B"
using h3 unfolding conc_def by blast
@@ -317,88 +313,24 @@
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)
+ 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
next
- have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"
+ 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
@@ -410,90 +342,29 @@
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>"
+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(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)
-
+apply(auto simp add: append_eq_append_conv2 strict_prefix_def)
+done
-
-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
+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
-text {* The following is a technical lemma, which helps to show the range finiteness of tag function. *}
+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)
+by (metis (full_types) all_not_in_conv insert_iff linorder_linear order_trans)
lemma finite_strict_prefix_set:
shows "finite {xa. xa < (x::'a list)}"
@@ -501,119 +372,162 @@
apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
by (auto simp:strict_prefix_def)
+lemma append_eq_cases:
+ assumes a: "x @ y = m @ n" "m \<noteq> []"
+ shows "x \<le> m \<or> m < x"
+unfolding prefix_def strict_prefix_def using a
+by (auto simp add: append_eq_append_conv2)
+
+lemma star_spartitions_elim2:
+ assumes a: "x @ z \<in> A\<star>"
+ and b: "x \<noteq> []"
+ shows "\<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>"
+proof -
+ def S \<equiv> "{u | u v. (u, v) \<in> Partitions x \<and> u < x \<and> u \<in> A\<star> \<and> v @ z \<in> A\<star>}"
+ have "finite {u. u < x}" by (rule finite_strict_prefix_set)
+ then have "finite S" unfolding S_def
+ by (rule rev_finite_subset) (auto)
+ moreover
+ have "S \<noteq> {}" using a b unfolding S_def Partitions_def
+ by (auto simp: strict_prefix_def)
+ ultimately have "\<exists> u_max \<in> S. \<forall> u \<in> S. length u \<le> length u_max"
+ using finite_set_has_max2 by blast
+ then obtain u_max v
+ where h0: "(u_max, v) \<in> Partitions x"
+ and h1: "u_max < x"
+ and h2: "u_max \<in> A\<star>"
+ and h3: "v @ z \<in> A\<star>"
+ and h4: "\<forall> u v. (u, v) \<in> Partitions x \<and> u < x \<and> u \<in> A\<star> \<and> v @ z \<in> A\<star> \<longrightarrow> length u \<le> length u_max"
+ unfolding S_def Partitions_def by blast
+ have q: "v \<noteq> []" using h0 h1 b unfolding Partitions_def by auto
+ from h3 obtain a b
+ where i1: "(a, b) \<in> Partitions (v @ z)"
+ and i2: "a \<in> A"
+ and i3: "b \<in> A\<star>"
+ and i4: "a \<noteq> []"
+ unfolding Partitions_def
+ using q by (auto dest: star_decom)
+ have "v \<le> a"
+ proof (rule ccontr)
+ assume a: "\<not>(v \<le> a)"
+ from i1 have i1': "a @ b = v @ z" unfolding Partitions_def by simp
+ then have "a \<le> v \<or> v < a" using append_eq_cases q by blast
+ then have q: "a < v" using a unfolding strict_prefix_def prefix_def by auto
+ then obtain as where eq: "a @ as = v" unfolding strict_prefix_def prefix_def by auto
+ have "(u_max @ a, as) \<in> Partitions x" using eq h0 unfolding Partitions_def by auto
+ moreover
+ have "u_max @ a < x" using h0 eq q unfolding Partitions_def strict_prefix_def prefix_def by auto
+ 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
+ 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
+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 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
+ 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
+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"
+ 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
+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)
- show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
- by (rule tag_Star_injI)
+ 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
next
have *: "finite (Pow (UNIV // \<approx>A))"
- using finite1 by auto
+ using finite1 by auto
show "finite (range (tag_Star A))"
unfolding tag_Star_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
- by auto
+ apply(auto)
+ done
qed
subsubsection{* The conclusion *}
diff -r 97090fc7aa9f -r 560712a29a36 Prefix_subtract.thy
--- a/Prefix_subtract.thy Sun Jul 31 10:27:41 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-theory Prefix_subtract
- imports Main "~~/src/HOL/Library/List_Prefix"
-begin
-
-
-section {* A small theory of prefix subtraction *}
-
-text {*
- The notion of @{text "prefix_subtract"} makes
- the second direction of the Myhill-Nerode theorem
- more readable.
-*}
-
-instantiation list :: (type) minus
-begin
-
-fun minus_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
- "minus_list [] xs = []"
-| "minus_list (x#xs) [] = x#xs"
-| "minus_list (x#xs) (y#ys) = (if x = y then minus_list xs ys else (x#xs))"
-
-instance by default
-
-end
-
-lemma [simp]: "x - [] = x"
-by (induct x) (auto)
-
-lemma [simp]: "(x @ y) - x = y"
-by (induct x) (auto)
-
-lemma [simp]: "x - x = []"
-by (induct x) (auto)
-
-lemma [simp]: "x = z @ y \<Longrightarrow> x - z = y "
-by (induct x) (auto)
-
-lemma diff_prefix:
- "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"
-by (auto elim: prefixE)
-
-lemma diff_diff_append:
- "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"
-apply (clarsimp simp:strict_prefix_def)
-by (drule diff_prefix, auto elim:prefixE)
-
-lemma append_eq_cases:
- assumes a: "x @ y = m @ n"
- shows "x \<le> m \<or> m \<le> x"
-unfolding prefix_def using a
-by (auto simp add: append_eq_append_conv2)
-
-lemma append_eq_dest:
- assumes a: "x @ y = m @ n"
- shows "(x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
-using append_eq_cases[OF a] a
-by (auto elim: prefixE)
-
-end