(* Author: Xingyuan Zhang, Chunhan Wu, Christian Urban *) theory Myhill_2 imports Myhill_1 "HOL-Library.Sublist" begin section ‹Second direction of MN: ‹regular language ⇒ finite partition›› subsection ‹Tagging functions› definition tag_eq :: "('a list ⇒ 'b) ⇒ ('a list × 'a list) set" ("=_=") where "=tag= ≡ {(x, y). tag x = tag y}" abbreviation tag_eq_applied :: "'a list ⇒ ('a list ⇒ 'b) ⇒ 'a list ⇒ bool" ("_ =_= _") where "x =tag= y ≡ (x, y) ∈ =tag=" lemma [simp]: shows "(≈A) `` {x} = (≈A) `` {y} ⟷ x ≈A y" unfolding str_eq_def by auto lemma refined_intro: assumes "⋀x y z. ⟦x =tag= y; x @ z ∈ A⟧ ⟹ y @ z ∈ A" shows "=tag= ⊆ ≈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" = "λX. tag ` X" and ?A = "(UNIV // =tag=)" have "finite (?f ` ?A)" proof - have "range ?f ⊆ (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 ⊆ 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 ∈ ?A" and Y_in: "Y ∈ ?A" and tag_eq: "?f X = ?f Y" then obtain x y where "x ∈ X" "y ∈ 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 ⊆ R2" and eq1: "equiv UNIV R1" and eq2: "equiv UNIV R2" shows "finite (UNIV // R2)" proof - let ?f = "λX. {R1 `` {x} | x. x ∈ X}" and ?A = "UNIV // R2" and ?B = "UNIV // R1" have "?f ` ?A ⊆ 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 ∈ ?A" and Y_in: "Y ∈ ?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 ∈ X" by simp then have "R1 ``{x} ∈ ?f X" by auto with eq_f have "R1 `` {x} ∈ ?f Y" by simp then obtain y where y_in: "y ∈ Y" and eq_r1_xy: "R1 `` {x} = R1 `` {y}" by auto with eq_equiv_class[OF _ eq1] have "(x, y) ∈ R1" by blast with refined have "(x, y) ∈ 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 refined: "=tag= ⊆ ≈A" shows "finite (UNIV // ≈A)" proof (rule_tac refined_partition_finite [of "=tag="]) show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt]) next show "=tag= ⊆ ≈A" using refined . next show "equiv UNIV =tag=" and "equiv UNIV (≈A)" unfolding equiv_def str_eq_def tag_eq_def refl_on_def sym_def trans_def by auto qed subsection ‹Base cases: @{const Zero}, @{const One} and @{const Atom}› lemma quot_zero_eq: shows "UNIV // ≈{} = {UNIV}" unfolding quotient_def Image_def str_eq_def by auto lemma quot_zero_finiteI [intro]: shows "finite (UNIV // ≈{})" unfolding quot_zero_eq by simp lemma quot_one_subset: shows "UNIV // ≈{[]} ⊆ {{[]}, UNIV - {[]}}" proof fix x assume "x ∈ UNIV // ≈{[]}" then obtain y where h: "x = {z. y ≈{[]} z}" unfolding quotient_def Image_def by blast { assume "y = []" with h have "x = {[]}" by (auto simp: str_eq_def) then have "x ∈ {{[]}, UNIV - {[]}}" by simp } moreover { assume "y ≠ []" with h have "x = UNIV - {[]}" by (auto simp: str_eq_def) then have "x ∈ {{[]}, UNIV - {[]}}" by simp } ultimately show "x ∈ {{[]}, UNIV - {[]}}" by blast qed lemma quot_one_finiteI [intro]: shows "finite (UNIV // ≈{[]})" by (rule finite_subset[OF quot_one_subset]) (simp) lemma quot_atom_subset: "UNIV // (≈{[c]}) ⊆ {{[]},{[c]}, UNIV - {[], [c]}}" proof fix x assume "x ∈ UNIV // ≈{[c]}" then obtain y where h: "x = {z. (y, z) ∈ ≈{[c]}}" unfolding quotient_def Image_def by blast show "x ∈ {{[]},{[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 ≠ []" and "y ≠ [c]" hence "∀ z. (y @ z) ≠ [c]" by (case_tac y, auto) moreover have "⋀ p. (p ≠ [] ∧ p ≠ [c]) = (∀ q. p @ q ≠ [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 // ≈{[c]})" by (rule finite_subset[OF quot_atom_subset]) (simp) subsection ‹Case for @{const Plus}› definition tag_Plus :: "'a lang ⇒ 'a lang ⇒ 'a list ⇒ ('a lang × 'a lang)" where "tag_Plus A B ≡ λx. (≈A `` {x}, ≈B `` {x})" lemma quot_plus_finiteI [intro]: assumes finite1: "finite (UNIV // ≈A)" and finite2: "finite (UNIV // ≈B)" shows "finite (UNIV // ≈(A ∪ B))" proof (rule_tac tag = "tag_Plus A B" in tag_finite_imageD) have "finite ((UNIV // ≈A) × (UNIV // ≈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 "=tag_Plus A B= ⊆ ≈(A ∪ B)" unfolding tag_eq_def tag_Plus_def str_eq_def by auto qed subsection ‹Case for ‹Times›› definition "Partitions x ≡ {(x⇩_{p}, x⇩_{s}). x⇩_{p}@ x⇩_{s}= x}" lemma conc_partitions_elim: assumes "x ∈ A ⋅ B" shows "∃(u, v) ∈ Partitions x. u ∈ A ∧ v ∈ B" using assms unfolding conc_def Partitions_def by auto lemma conc_partitions_intro: assumes "(u, v) ∈ Partitions x ∧ u ∈ A ∧ v ∈ B" shows "x ∈ A ⋅ B" using assms unfolding conc_def Partitions_def by auto lemma equiv_class_member: assumes "x ∈ A" and "≈A `` {x} = ≈A `` {y}" shows "y ∈ A" using assms apply(simp) apply(simp add: str_eq_def) apply(metis append_Nil2) done definition tag_Times :: "'a lang ⇒ 'a lang ⇒ 'a list ⇒ 'a lang × 'a lang set" where "tag_Times A B ≡ λx. (≈A `` {x}, {(≈B `` {x⇩_{s}}) | x⇩_{p}x⇩_{s}. x⇩_{p}∈ A ∧ (x⇩_{p}, x⇩_{s}) ∈ Partitions x})" lemma tag_Times_injI: assumes a: "tag_Times A B x = tag_Times A B y" and c: "x @ z ∈ A ⋅ B" shows "y @ z ∈ A ⋅ B" proof - from c obtain u v where h1: "(u, v) ∈ Partitions (x @ z)" and h2: "u ∈ A" and h3: "v ∈ 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 ∧ us @ z = v) ∨ (x @ us = u ∧ z = us @ v)" by (auto simp add: append_eq_append_conv2) moreover { assume eq: "x = u @ us" "us @ z = v" have "(≈B `` {us}) ∈ snd (tag_Times A B x)" unfolding Partitions_def tag_Times_def using h2 eq by (auto simp add: str_eq_def) then have "(≈B `` {us}) ∈ snd (tag_Times A B y)" using a by simp then obtain u' us' where q1: "u' ∈ A" and q2: "≈B `` {us} = ≈B `` {us'}" and q3: "(u', us') ∈ Partitions y" unfolding tag_Times_def by auto from q2 h3 eq have "us' @ z ∈ B" unfolding Image_def str_eq_def by auto then have "y @ z ∈ A ⋅ B" using q1 q3 unfolding Partitions_def by auto } moreover { assume eq: "x @ us = u" "z = us @ v" have "(≈A `` {x}) = fst (tag_Times A B x)" by (simp add: tag_Times_def) then have "(≈A `` {x}) = fst (tag_Times A B y)" using a by simp then have "≈A `` {x} = ≈A `` {y}" by (simp add: tag_Times_def) moreover have "x @ us ∈ A" using h2 eq by simp ultimately have "y @ us ∈ A" using equiv_class_member unfolding Image_def str_eq_def by blast then have "(y @ us) @ v ∈ A ⋅ B" using h3 unfolding conc_def by blast then have "y @ z ∈ A ⋅ B" using eq by simp } ultimately show "y @ z ∈ A ⋅ B" by blast qed lemma quot_conc_finiteI [intro]: assumes fin1: "finite (UNIV // ≈A)" and fin2: "finite (UNIV // ≈B)" shows "finite (UNIV // ≈(A ⋅ B))" proof (rule_tac tag = "tag_Times A B" in tag_finite_imageD) have "⋀x y z. ⟦tag_Times A B x = tag_Times A B y; x @ z ∈ A ⋅ B⟧ ⟹ y @ z ∈ A ⋅ B" by (rule tag_Times_injI) (auto simp add: tag_Times_def tag_eq_def) then show "=tag_Times A B= ⊆ ≈(A ⋅ B)" by (rule refined_intro) (auto simp add: tag_eq_def) next have *: "finite ((UNIV // ≈A) × (Pow (UNIV // ≈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 subsection ‹Case for @{const "Star"}› lemma star_partitions_elim: assumes "x @ z ∈ A⋆" "x ≠ []" shows "∃(u, v) ∈ Partitions (x @ z). strict_prefix u x ∧ u ∈ A⋆ ∧ v ∈ A⋆" proof - have "([], x @ z) ∈ Partitions (x @ z)" "strict_prefix [] x" "[] ∈ A⋆" "x @ z ∈ A⋆" using assms by (auto simp add: Partitions_def strict_prefix_def) then show "∃(u, v) ∈ Partitions (x @ z). strict_prefix u x ∧ u ∈ A⋆ ∧ v ∈ A⋆" by blast qed lemma finite_set_has_max2: "⟦finite A; A ≠ {}⟧ ⟹ ∃ max ∈ A. ∀ a ∈ A. length a ≤ length max" apply(induct rule:finite.induct) apply(simp) by (metis (no_types) all_not_in_conv insert_iff linorder_le_cases order_trans) lemma finite_strict_prefix_set: shows "finite {xa. strict_prefix xa (x::'a list)}" apply (induct x rule:rev_induct, simp) apply (subgoal_tac "{xa. strict_prefix xa (xs @ [x])} = {xa. strict_prefix xa xs} ∪ {xs}") by (auto simp:strict_prefix_def) lemma append_eq_cases: assumes a: "x @ y = m @ n" "m ≠ []" shows "prefix x m ∨ strict_prefix 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 ∈ A⋆" and b: "x ≠ []" shows "∃(u, v) ∈ Partitions x. ∃ (u', v') ∈ Partitions z. strict_prefix u x ∧ u ∈ A⋆ ∧ v @ u' ∈ A ∧ v' ∈ A⋆" proof - define S where "S = {u | u v. (u, v) ∈ Partitions x ∧ strict_prefix u x ∧ u ∈ A⋆ ∧ v @ z ∈ A⋆}" have "finite {u. strict_prefix u x}" by (rule finite_strict_prefix_set) then have "finite S" unfolding S_def by (rule rev_finite_subset) (auto) moreover have "S ≠ {}" using a b unfolding S_def Partitions_def by (auto simp: strict_prefix_def) ultimately have "∃ u_max ∈ S. ∀ u ∈ S. length u ≤ length u_max" using finite_set_has_max2 by blast then obtain u_max v where h0: "(u_max, v) ∈ Partitions x" and h1: "strict_prefix u_max x" and h2: "u_max ∈ A⋆" and h3: "v @ z ∈ A⋆" and h4: "∀ u v. (u, v) ∈ Partitions x ∧ strict_prefix u x ∧ u ∈ A⋆ ∧ v @ z ∈ A⋆ ⟶ length u ≤ length u_max" unfolding S_def Partitions_def by blast have q: "v ≠ []" using h0 h1 b unfolding Partitions_def by auto from h3 obtain a b where i1: "(a, b) ∈ Partitions (v @ z)" and i2: "a ∈ A" and i3: "b ∈ A⋆" and i4: "a ≠ []" unfolding Partitions_def using q by (auto dest: star_decom) have "prefix v a" proof (rule ccontr) assume a: "¬(prefix v a)" from i1 have i1': "a @ b = v @ z" unfolding Partitions_def by simp then have "prefix a v ∨ strict_prefix v a" using append_eq_cases q by blast then have q: "strict_prefix 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) ∈ Partitions x" using eq h0 unfolding Partitions_def by auto moreover have "strict_prefix (u_max @ a) x" using h0 eq q unfolding Partitions_def prefix_def strict_prefix_def by auto moreover have "u_max @ a ∈ A⋆" using i2 h2 by simp moreover have "as @ z ∈ A⋆" using i1' i2 i3 eq by auto ultimately have "length (u_max @ a) ≤ length u_max" using h4 by blast with i4 show "False" by auto qed with i1 obtain za zb where k1: "v @ za = a" and k2: "(za, zb) ∈ Partitions z" and k4: "zb = b" unfolding Partitions_def prefix_def by (auto simp add: append_eq_append_conv2) show "∃ (u, v) ∈ Partitions x. ∃ (u', v') ∈ Partitions z. strict_prefix u x ∧ u ∈ A⋆ ∧ v @ u' ∈ A ∧ v' ∈ A⋆" using h0 h1 h2 i2 i3 k1 k2 k4 unfolding Partitions_def by blast qed definition tag_Star :: "'a lang ⇒ 'a list ⇒ ('a lang) set" where "tag_Star A ≡ λx. {≈A `` {v} | u v. strict_prefix u x ∧ u ∈ A⋆ ∧ (u, v) ∈ Partitions x}" lemma tag_Star_non_empty_injI: assumes a: "tag_Star A x = tag_Star A y" and c: "x @ z ∈ A⋆" and d: "x ≠ []" shows "y @ z ∈ A⋆" proof - obtain u v u' v' where a1: "(u, v) ∈ Partitions x" "(u', v')∈ Partitions z" and a2: "strict_prefix u x" and a3: "u ∈ A⋆" and a4: "v @ u' ∈ A" and a5: "v' ∈ A⋆" using c d by (auto dest: star_spartitions_elim2) have "(≈A) `` {v} ∈ 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 "(≈A) `` {v} ∈ tag_Star A y" using a by simp then obtain u1 v1 where b1: "v ≈A v1" and b3: "u1 ∈ A⋆" and b4: "(u1, v1) ∈ Partitions y" unfolding tag_Star_def by auto have c: "v1 @ u' ∈ A⋆" using b1 a4 unfolding str_eq_def by simp have "u1 @ (v1 @ u') @ v' ∈ A⋆" using b3 c a5 by (simp only: append_in_starI) then show "y @ z ∈ A⋆" 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 ∈ A⋆" and d: "x = []" shows "y @ z ∈ A⋆" proof - from a have "{} = tag_Star A y" unfolding tag_Star_def using d by auto then have "y = []" unfolding tag_Star_def Partitions_def strict_prefix_def prefix_def by (auto) (metis Nil_in_star append_self_conv2) then show "y @ z ∈ A⋆" using c d by simp qed lemma quot_star_finiteI [intro]: assumes finite1: "finite (UNIV // ≈A)" shows "finite (UNIV // ≈(A⋆))" proof (rule_tac tag = "tag_Star A" in tag_finite_imageD) have "⋀x y z. ⟦tag_Star A x = tag_Star A y; x @ z ∈ A⋆⟧ ⟹ y @ z ∈ A⋆" by (case_tac "x = []") (blast intro: tag_Star_empty_injI tag_Star_non_empty_injI)+ then show "=(tag_Star A)= ⊆ ≈(A⋆)" by (rule refined_intro) (auto simp add: tag_eq_def) next have *: "finite (Pow (UNIV // ≈A))" using finite1 by auto show "finite (range (tag_Star A))" unfolding tag_Star_def by (rule finite_subset[OF _ *]) (auto simp add: quotient_def) qed subsection ‹The conclusion of the second direction› lemma Myhill_Nerode2: fixes r::"'a rexp" shows "finite (UNIV // ≈(lang r))" by (induct r) (auto) end