163 subsection {* Finite and co-finite set are regular *}

   164 

   165 lemma singleton_regular:

   166   shows "regular {s}"

   167 proof (induct s)

   168   case Nil

   169   have "{[]} = lang (One)" by simp

   170   then show "regular {[]}" by blast

   171 next

   172   case (Cons c s)

   173   have "regular {s}" by fact

   174   then obtain r where "{s} = lang r" by blast

   175   then have "{c # s} = lang (Times (Atom c) r)" 

   176     by (auto simp add: conc_def)

   177   then show "regular {c # s}" by blast

   178 qed

   179 

   180 lemma finite_regular:

   181   assumes "finite A"

   182   shows "regular A"

   183 using assms

   184 proof (induct)

   185   case empty

   186   have "{} = lang (Zero)" by simp

   187   then show "regular {}" by blast

   188 next

   189   case (insert s A)

   190   have "regular {s}" by (simp add: singleton_regular)

   191   moreover

   192   have "regular A" by fact

   193   ultimately have "regular ({s} \<union> A)" by (rule closure_union)

   194   then show "regular (insert s A)" by simp

   195 qed

   196 

   197 lemma cofinite_regular:

   198   fixes A::"('a::finite list) set"

   199   assumes "finite (- A)"

   200   shows "regular A"

   201 proof -

   202   from assms have "regular (- A)" by (simp add: finite_regular)

   203   then have "regular (-(- A))" by (rule closure_complement)

   204   then show "regular A" by simp

   205 qed

   206 

   207 

   208 subsection {* non-regularity of particular languages *}

   209 

   210 lemma continuation_lemma:

   211   fixes A B::"('a::finite list) set"

   212   assumes reg: "regular A"

   213   and     inf: "infinite B"

   214   shows "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y"

   215 proof -

   216   def eqfun \<equiv> "\<lambda>A x::('a::finite list). (\<approx>A) `` {x}"

   217   have "finite (UNIV // \<approx>A)" using reg by (simp add: Myhill_Nerode)

   218   moreover

   219   have "(eqfun A) ` B \<subseteq> UNIV // (\<approx>A)"

   220     unfolding eqfun_def quotient_def by auto

   221   ultimately have "finite ((eqfun A) ` B)" by (rule rev_finite_subset)

   222   with inf have "\<exists>a \<in> B. infinite {b \<in> B. eqfun A b = eqfun A a}"

   223     by (rule pigeonhole_infinite)

   224   then obtain a where in_a: "a \<in> B" and "infinite {b \<in> B. eqfun A b = eqfun A a}"

   225     by blast

   226   moreover 

   227   have "{b \<in> B. eqfun A b = eqfun A a} = {b \<in> B. b \<approx>A a}"

   228     unfolding eqfun_def Image_def str_eq_def by auto

   229   ultimately have "infinite {b \<in> B. b \<approx>A a}" by simp

   230   then have "infinite ({b \<in> B. b \<approx>A a} - {a})" by simp

   231   moreover

   232   have "{b \<in> B. b \<approx>A a} - {a} = {b \<in> B. b \<approx>A a \<and> b \<noteq> a}" by auto

   233   ultimately have "infinite {b \<in> B. b \<approx>A a \<and> b \<noteq> a}" by simp

   234   then have "{b \<in> B. b \<approx>A a \<and> b \<noteq> a} \<noteq> {}"

   235     by (metis finite.emptyI)

   236   then obtain b where "b \<in> B" "b \<noteq> a" "b \<approx>A a" by blast

   237   with in_a show "\<exists>x \<in> B. \<exists>y \<in> B. x \<noteq> y \<and> x \<approx>A y"

   238     by blast

   239 qed

   240 

   241 definition

   242   "ex1 a b \<equiv> {replicate n a @ replicate n b | n. True}"

   243 

   244 (*

   245 lemma

   246   fixes a b::"'a::finite"

   247   assumes "a \<noteq> b"

   248   shows "\<not> regular (ex1 a b)"

   249 proof -

   250   { assume a: "regular (ex1 a b)"

   251     def fool \<equiv> "{replicate i a | i. True}"

   252     have b: "infinite fool"

   253       unfolding fool_def

   254       unfolding infinite_iff_countable_subset

   255       apply(rule_tac x="\<lambda>i. replicate i a" in exI)

   256       apply(auto simp add: inj_on_def)

   257       done

   258     from a b have "\<exists>x \<in> fool. \<exists>y \<in> fool. x \<noteq> y \<and> x \<approx>(ex1 a b) y"

   259       using continuation_lemma by blast

   260     moreover

   261     have c: "\<forall>x \<in> fool. \<forall>y \<in> fool. x \<noteq> y \<longrightarrow> \<not>(x \<approx>(ex1 a b) y)"

   262       apply(rule ballI)

   263       apply(rule ballI)

   264       apply(rule impI)

   265       unfolding fool_def

   266       apply(simp)

   267       apply(erule exE)+

   268       unfolding str_eq_def

   269       apply(simp)

   270       apply(rule_tac x="replicate i b" in exI)

   271       apply(simp add: ex1_def)

   272       apply(rule iffI)

   273       prefer 2

   274       apply(rule_tac x="i" in exI)

   275       apply(simp)

   276       apply(rule allI)

   277       apply(rotate_tac 3)

   278       apply(thin_tac "?X")

   279       apply(auto)

   280       sorry

   281     ultimately have "False" by auto

   282   }

   283   then show "\<not> regular (ex1 a b)" by auto

   284 qed

   285 *)    

   286