theory Myhill_2+
−
  imports Myhill_1 Prefix_subtract+
−
          "~~/src/HOL/Library/List_Prefix"+
−
begin+
−
+
−
section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}+
−
+
−
definition+
−
  str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")+
−
where+
−
  "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"+
−
+
−
lemma str_eq_def2:+
−
  shows "\<approx>A = {(x, y) | x y. x \<approx>A y}"+
−
unfolding str_eq_def+
−
by simp+
−
+
−
definition +
−
   tag_eq_rel :: "(string \<Rightarrow> 'b) \<Rightarrow> (string \<times> string) set" ("=_=")+
−
where+
−
   "=tag= \<equiv> {(x, y). tag x = tag y}"+
−
+
−
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_rel_def+
−
        by (simp) (blast)+
−
      with X_in Y_in +
−
      have "X = Y"+
−
	unfolding quotient_def tag_eq_rel_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_rel_def str_eq_def+
−
    by auto+
−
next+
−
  show "equiv UNIV =tag="+
−
    unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def+
−
    by auto+
−
next+
−
  show "equiv UNIV (\<approx>A)" +
−
    unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def+
−
    by blast+
−
qed+
−
+
−
+
−
subsection {* The proof *}+
−
+
−
subsubsection {* The base case for @{const "NULL"} *}+
−
+
−
lemma quot_null_eq:+
−
  shows "UNIV // \<approx>{} = {UNIV}"+
−
unfolding quotient_def Image_def str_eq_rel_def by auto+
−
+
−
lemma quot_null_finiteI [intro]:+
−
  shows "finite (UNIV // \<approx>{})"+
−
unfolding quot_null_eq by simp+
−
+
−
+
−
subsubsection {* The base case for @{const "EMPTY"} *}+
−
+
−
lemma quot_empty_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_rel_def)+
−
    thus ?thesis by simp+
−
  next+
−
    case False with h+
−
    have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def)+
−
    thus ?thesis by simp+
−
  qed+
−
qed+
−
+
−
lemma quot_empty_finiteI [intro]:+
−
  shows "finite (UNIV // \<approx>{[]})"+
−
by (rule finite_subset[OF quot_empty_subset]) (simp)+
−
+
−
+
−
subsubsection {* The base case for @{const "CHAR"} *}+
−
+
−
lemma quot_char_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_rel_def) } +
−
    moreover +
−
    { assume "y = [c]" hence "x = {[c]}" using h +
−
        by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_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_rel_def)+
−
    } +
−
    ultimately show ?thesis by blast+
−
  qed+
−
qed+
−
+
−
lemma quot_char_finiteI [intro]:+
−
  shows "finite (UNIV // \<approx>{[c]})"+
−
by (rule finite_subset[OF quot_char_subset]) (simp)+
−
+
−
+
−
subsubsection {* The inductive case for @{const ALT} *}+
−
+
−
definition +
−
  tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"+
−
where+
−
  "tag_str_ALT A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"+
−
+
−
lemma quot_union_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_str_ALT 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_str_ALT A B))"+
−
    unfolding tag_str_ALT_def quotient_def+
−
    by (rule rev_finite_subset) (auto)+
−
next+
−
  show "\<And>x y. tag_str_ALT A B x = tag_str_ALT A B y \<Longrightarrow> x \<approx>(A \<union> B) y"+
−
    unfolding tag_str_ALT_def+
−
    unfolding str_eq_def+
−
    unfolding str_eq_rel_def+
−
    by auto+
−
qed+
−
+
−
+
−
subsubsection {* The inductive case for @{text "SEQ"}*}+
−
+
−
definition +
−
  tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"+
−
where+
−
  "tag_str_SEQ L1 L2 \<equiv>+
−
     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"+
−
+
−
lemma Seq_in_cases:+
−
  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 Seq_def prefix_def+
−
by (auto simp add: append_eq_append_conv2)+
−
+
−
lemma tag_str_SEQ_injI:+
−
  assumes eq_tag: "tag_str_SEQ A B x = tag_str_SEQ 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_str_SEQ A B x = tag_str_SEQ 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_str_SEQ_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_rel_def str_eq_def by auto+
−
          with h3 have "(y - y') @ z \<in> B" +
−
	    unfolding str_eq_rel_def 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" by (erule_tac prefixE) (auto simp: Seq_def)+
−
      } +
−
      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_str_SEQ_def by simp+
−
         with h2 have "y @ z' \<in> A"+
−
            unfolding Image_def str_eq_rel_def str_eq_def by auto+
−
        with h1 h3 have "y @ z \<in> A \<cdot> B"+
−
	  unfolding prefix_def Seq_def+
−
	  by (auto) (metis append_assoc)+
−
      }+
−
      ultimately show "y @ z \<in> A \<cdot> B" +
−
	using Seq_in_cases [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 str_eq_rel_def by blast+
−
qed +
−
+
−
lemma quot_seq_finiteI [intro]:+
−
  fixes L1 L2::"lang"+
−
  assumes fin1: "finite (UNIV // \<approx>L1)" +
−
  and     fin2: "finite (UNIV // \<approx>L2)" +
−
  shows "finite (UNIV // \<approx>(L1 \<cdot> L2))"+
−
proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)+
−
  show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y"+
−
    by (rule tag_str_SEQ_injI)+
−
next+
−
  have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" +
−
    using fin1 fin2 by auto+
−
  show "finite (range (tag_str_SEQ L1 L2))" +
−
    unfolding tag_str_SEQ_def+
−
    apply(rule finite_subset[OF _ *])+
−
    unfolding quotient_def+
−
    by auto+
−
qed+
−
+
−
+
−
subsubsection {* The inductive case for @{const "STAR"} *}+
−
+
−
definition +
−
  tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"+
−
where+
−
  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<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: "finite {xa. xa < (x::string)}"+
−
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_str_STAR_injI:+
−
  assumes eq_tag: "tag_str_STAR L\<^isub>1 v = tag_str_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_str_STAR L\<^isub>1 x = tag_str_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_str_STAR_def strict_prefix_def)+
−
      thus ?thesis using xz_in_star True by simp+
−
    next+
−
      case False+
−
      let ?S = "{xa. 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_str_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_rel_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> []" +
−
            by (auto simp:strict_prefix_def elim:prefixE)+
−
          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 (simp add:star_intro3) +
−
                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 by (auto elim:prefixE)+
−
          with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1" +
−
            by (auto simp:str_eq_def str_eq_rel_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 blast+
−
        with eq_zab show ?thesis by simp+
−
      qed+
−
      with h5 h6 show ?thesis +
−
        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim: prefixE)+
−
    qed+
−
  } +
−
  from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]+
−
    show  ?thesis unfolding str_eq_def str_eq_rel_def by blast+
−
qed+
−
+
−
lemma quot_star_finiteI [intro]:+
−
  assumes finite1: "finite (UNIV // \<approx>A)"+
−
  shows "finite (UNIV // \<approx>(A\<star>))"+
−
proof (rule_tac tag = "tag_str_STAR A" in tag_finite_imageD)+
−
  show "\<And>x y. tag_str_STAR A x = tag_str_STAR A y \<Longrightarrow> x \<approx>(A\<star>) y"+
−
    by (rule tag_str_STAR_injI)+
−
next+
−
  have *: "finite (Pow (UNIV // \<approx>A))" +
−
    using finite1 by auto+
−
  show "finite (range (tag_str_STAR A))"+
−
    unfolding tag_str_STAR_def+
−
    apply(rule finite_subset[OF _ *])+
−
    unfolding quotient_def+
−
    by auto+
−
qed+
−
+
−
subsubsection{* The conclusion *}+
−
+
−
lemma Myhill_Nerode2:+
−
  shows "finite (UNIV // \<approx>(L_rexp r))"+
−
by (induct r) (auto)+
−
+
−
+
−
theorem Myhill_Nerode:+
−
  shows "(\<exists>r. A = L_rexp r) \<longleftrightarrow> finite (UNIV // \<approx>A)"+
−
using Myhill_Nerode1 Myhill_Nerode2 by auto+
−
+
−
end+
−