a version of the proof which dispenses with the notion of string-subtraction
theory Myhill_2 imports Myhill_1 "~~/src/HOL/Library/List_Prefix"beginsection {* 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_defby autolemma 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 assmsunfolding str_eq_def tag_eq_defapply(clarify, simp (no_asm_use))by metislemma 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)qedlemma 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)qedlemma 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 blastnext show "equiv UNIV =tag=" unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def by autonext show "equiv UNIV (\<approx>A)" unfolding equiv_def str_eq_def sym_def refl_on_def trans_def by blastqedsubsection {* 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 autolemma quot_zero_finiteI [intro]: shows "finite (UNIV // \<approx>{})"unfolding quot_zero_eq by simpsubsubsection {* 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 qedqedlemma 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 qedqedlemma 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 autoqedsubsubsection {* 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 assmsunfolding conc_def Partitions_defby autolemma conc_partitions_intro: assumes "(u, v) \<in> Partitions x \<and> u \<in> A \<and> v \<in> B" shows "x \<in> A \<cdot> B"using assmsunfolding conc_def Partitions_defby autolemma equiv_class_member: assumes "x \<in> A" and "\<approx>A `` {x} = \<approx>A `` {y}" shows "y \<in> A"using assmsapply(simp add: Image_def str_eq_def set_eq_iff)apply(metis append_Nil2)doneabbreviation tag_Times_1 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang"where "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_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set"where "tag_Times A B \<equiv> \<lambda>x. (tag_Times_1 A B x, tag_Times_2 A B x)"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_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_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 from q1 h2 have "u' \<in> A" using equiv_class_member by auto 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_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}" by simp moreover have "x @ us \<in> A" using h2 eq by simp ultimately 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 then have "y @ z \<in> A \<cdot> B" using eq by simp } ultimately show "y @ z \<in> A \<cdot> B" by blastqedlemma 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 autonext 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 apply(rule finite_subset[OF _ *]) unfolding quotient_def by autoqedsubsubsection {* 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 assmsapply(auto simp add: append_eq_append_conv2 strict_prefix_def)donelemma 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 blastqedlemma 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)}"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 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 aby (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 blastqeddefinition 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" 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 dapply(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 2apply(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)donelemma 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 dapply(simp)using aapply(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) donenext 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) doneqedsubsubsection{* 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 autoend