Mercurial Mercurial > hg > regexp / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Myhill.thy
changeset 43 cb4403fabda7
parent 42 f809cb54de4e
child 45 7aa6c20e6d31
equal deleted inserted replaced
42:f809cb54de4e 43:cb4403fabda7 
    11   string @{text "x"} and @{text "y"} are equivalent with respect to 
    11   string @{text "x"} and @{text "y"} are equivalent with respect to 
    12   language @{text "Lang"}.
 
    12   language @{text "Lang"}.
 
    13   *}
 
    13   *}
 
    14 
    14 
    15 definition
 
    15 definition
 
    16   str_eq ("_ \<approx>_ _")
 
    16   str_eq :: "string \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> bool" ("_ \<approx>_ _")
 
    17 where
 
    17 where
 
    18   "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"
 
    18   "x \<approx>Lang y \<equiv> (x, y) \<in> (\<approx>Lang)"
 
    19 
    19 
    20 text {*
 
    20 text {*
 
    21   The very basic scheme to show the finiteness of the partion generated by a language @{text "Lang"}
 
    21   The very basic scheme to show the finiteness of the partion generated by a language @{text "Lang"}
 
    31   which says: if the image of injective function @{text "f"} over set @{text "A"} is 
    31   which says: if the image of injective function @{text "f"} over set @{text "A"} is 
    32   finite, then @{text "A"} must be finte.
 
    32   finite, then @{text "A"} must be finte.
 
    33   *}
 
    33   *}
 
    34 
    34 
    35 
    35 
    36 (* 
       
    37 
    36 
    38 (* I am trying to reduce the following proof to even simpler principles. But not yet succeed. *)
 
    37 (* I am trying to reduce the following proof to even simpler principles. But not yet succeed. *)
 
    39 definition 
    38 definition 
    40    f_eq_rel ("\<cong>_")
 
    39    f_eq_rel ("\<cong>_")
 
    41 where
 
    40 where
 
    89       } thus ?thesis unfolding inj_on_def by auto
 
    88       } thus ?thesis unfolding inj_on_def by auto
 
    90     qed
 
    89     qed
 
    91   qed
 
    90   qed
 
    92 qed
 
    91 qed
 
    93 
    92 
    94 *)
 
    93 
    95 
    94 (*
 
    96 lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)"
 
    95 lemma finite_range_image: "finite (range f) \<Longrightarrow> finite (f ` A)"
 
    97   by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def)
 
    96   by (rule_tac B = "{y. \<exists>x. y = f x}" in finite_subset, auto simp:image_def)
 
       
    97 *)
 
    98 
    98 
    99 lemma tag_finite_imageD:
 
    99 lemma tag_finite_imageD:
 
   100   fixes tag
 
   100   fixes L :: "lang"
 
   101   assumes rng_fnt: "finite (range tag)" 
   101   assumes rng_fnt: "finite (range tag)" 
   102   -- {* Suppose the rang of tagging fucntion @{text "tag"} is finite. *}
 
   102   -- {* Suppose the range of tagging fucntion @{text "tag"} is finite. *}
 
   103   and same_tag_eqvt: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>lang n"
 
   103   and same_tag_eqvt: "\<And> m n. tag m = tag n \<Longrightarrow> m \<approx>L n"
 
   104   -- {* And strings with same tag are equivalent *}
 
   104   -- {* And strings with same tag are equivalent *}
 
   105   shows "finite (UNIV // (\<approx>lang))"
 
   105   shows "finite (UNIV // \<approx>L)"
 
   106   -- {* Then the partition generated by @{text "(\<approx>lang)"} is finite. *}
 
   106   -- {* Then the partition generated by @{text "\<approx>L"} is finite. *}
 
   107 proof -
 
   107 proof -
 
   108   -- {* The particular @{text "f"} and @{text "A"} used in @{thm [source] "finite_imageD"} are:*}
 
   108   -- {* The particular @{text "f"} and @{text "A"} used in @{thm [source] "finite_imageD"} are:*}
 
   109   let "?f" =  "op ` tag" and ?A = "(UNIV // \<approx>lang)"
 
   109   let "?f" =  "op ` tag" and ?A = "(UNIV // \<approx>L)"
 
   110   show ?thesis
 
   110   show ?thesis
 
   111   proof (rule_tac f = "?f" and A = ?A in finite_imageD) 
   111   proof (rule_tac f = "?f" and A = ?A in finite_imageD) 
   112     -- {* 
   112     -- {* 
   113       The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}:
 
   113       The finiteness of @{text "f"}-image is a simple consequence of assumption @{text "rng_fnt"}:
 
   114       *}
 
   114       *}
 
   134         proof -
 
   134         proof -
 
   135           from X_in Y_in tag_eq 
   135           from X_in Y_in tag_eq 
   136           obtain x y where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"
 
   136           obtain x y where x_in: "x \<in> X" and y_in: "y \<in> Y" and eq_tg: "tag x = tag y"
 
   137             unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def
 
   137             unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def
 
   138             apply simp by blast 
   138             apply simp by blast 
   139           from same_tag_eqvt [OF eq_tg] have "x \<approx>lang y" .
 
   139           from same_tag_eqvt [OF eq_tg] have "x \<approx>L y" .
 
   140           with X_in Y_in x_in y_in
 
   140           with X_in Y_in x_in y_in
 
   141           show ?thesis by (auto simp:quotient_def str_eq_rel_def str_eq_def) 
   141           show ?thesis by (auto simp:quotient_def str_eq_rel_def str_eq_def) 
   142         qed
 
   142         qed
 
   143       } thus ?thesis unfolding inj_on_def by auto
 
   143       } thus ?thesis unfolding inj_on_def by auto
 
   144     qed
 
   144     qed
 
   146 qed
 
   146 qed
 
   147 
   147 
   148 subsection {* Lemmas for basic cases *}
 
   148 subsection {* Lemmas for basic cases *}
 
   149 
   149 
   150 text {*
 
   150 text {*
 
   151   The the final result of this direction is in @{text "easier_direction"}, which
 
   151   The the final result of this direction is in @{text "rexp_imp_finite"},
 
   152   is an induction on the structure of regular expressions. There is one case 
   152   which is an induction on the structure of regular expressions. There is one
 
   153   for each regular expression operator. For basic operators such as @{text "NULL, EMPTY, CHAR c"},
 
   153   case for each regular expression operator. For basic operators such as
 
   154   the finiteness of their language partition can be established directly with no need
 
   154   @{const NULL}, @{const EMPTY}, @{const CHAR}, the finiteness of their 
   155   of taggiing. This section contains several technical lemma for these base cases.
 
   155   language partition can be established directly with no need of tagging. 
   156 
   156   This section contains several technical lemma for these base cases.
 
   157   The inductive cases involve operators @{text "ALT, SEQ"} and @{text "STAR"}. 
   157 
   158   Tagging functions need to be defined individually for each of them. There will be one
 
   158   The inductive cases involve operators @{const ALT}, @{const SEQ} and @{const
 
   159   dedicated section for each of these cases, and each section goes virtually the same way:
 
   159   STAR}. Tagging functions need to be defined individually for each of
 
   160   gives definition of the tagging function and prove that strings 
   160   them. There will be one dedicated section for each of these cases, and each
 
   161   with the same tag are equivalent.
 
   161   section goes virtually the same way: gives definition of the tagging
 
   162   *}
 
   162   function and prove that strings with the same tag are equivalent.
 
       
   163 *}
 
       
   164 
       
   165 subsection {* The case for @{const "NULL"} *}
 
       
   166 
       
   167 lemma quot_null_eq:
 
       
   168   shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"
 
       
   169   unfolding quotient_def Image_def str_eq_rel_def by auto
 
       
   170 
       
   171 lemma quot_null_finiteI [intro]:
 
       
   172   shows "finite ((UNIV // \<approx>{})::lang set)"
 
       
   173 unfolding quot_null_eq by simp
 
       
   174 
       
   175 
       
   176 subsection {* The case for @{const "EMPTY"} *}
 
       
   177 
   163 
   178 
   164 lemma quot_empty_subset:
 
   179 lemma quot_empty_subset:
 
   165   "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
 
   180   "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}"
 
   166 proof
 
   181 proof
 
   167   fix x
 
   182   fix x
 
   168   assume "x \<in> UNIV // \<approx>{[]}"
 
   183   assume "x \<in> UNIV // \<approx>{[]}"
 
   169   then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" 
   184   then obtain y where h: "x = {z. (y, z) \<in> \<approx>{[]}}" 
   170     unfolding quotient_def Image_def by blast
 
   185     unfolding quotient_def Image_def by blast
 
   171   show "x \<in> {{[]}, UNIV - {[]}}" 
   186   show "x \<in> {{[]}, UNIV - {[]}}"
 
   172   proof (cases "y = []")
 
   187   proof (cases "y = []")
 
   173     case True with h
 
   188     case True with h
 
   174     have "x = {[]}" by (auto simp:str_eq_rel_def)
 
   189     have "x = {[]}" by (auto simp: str_eq_rel_def)
 
   175     thus ?thesis by simp
 
   190     thus ?thesis by simp
 
   176   next
 
   191   next
 
   177     case False with h
 
   192     case False with h
 
   178     have "x = UNIV - {[]}" by (auto simp:str_eq_rel_def)
 
   193     have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def)
 
   179     thus ?thesis by simp
 
   194     thus ?thesis by simp
 
   180   qed
 
   195   qed
 
   181 qed
 
   196 qed
 
       
   197 
       
   198 lemma quot_empty_finiteI [intro]:
 
       
   199   shows "finite (UNIV // (\<approx>{[]}))"
 
       
   200 by (rule finite_subset[OF quot_empty_subset]) (simp)
 
       
   201 
       
   202 
       
   203 subsection {* The case for @{const "CHAR"} *}
 
   182 
   204 
   183 lemma quot_char_subset:
 
   205 lemma quot_char_subset:
 
   184   "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
 
   206   "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}"
 
   185 proof 
   207 proof 
   186   fix x 
   208   fix x 
   203         by (auto simp add:str_eq_rel_def)
 
   225         by (auto simp add:str_eq_rel_def)
 
   204     } ultimately show ?thesis by blast
 
   226     } ultimately show ?thesis by blast
 
   205   qed
 
   227   qed
 
   206 qed
 
   228 qed
 
   207 
   229 
   208 subsection {* The case for @{text "SEQ"}*}
 
   230 lemma quot_char_finiteI [intro]:
 
       
   231   shows "finite (UNIV // (\<approx>{[c]}))"
 
       
   232 by (rule finite_subset[OF quot_char_subset]) (simp)
 
       
   233 
       
   234 
       
   235 subsection {* The case for @{const SEQ}*}
 
   209 
   236 
   210 definition 
   237 definition 
   211   "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> 
   238   tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
 
   212        ((\<approx>L\<^isub>1) `` {x}, {(\<approx>L\<^isub>2) `` {x - xa}| xa.  xa \<le> x \<and> xa \<in> L\<^isub>1})"
 
   239 where
 
   213 
   240   "tag_str_SEQ L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
 
   214 lemma tag_str_seq_range_finite:
 
   241 
   215   "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> 
       
   216                               \<Longrightarrow> finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))"
 
       
   217 apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (Pow (UNIV // \<approx>L\<^isub>2))" in finite_subset)
 
       
   218 by (auto simp:tag_str_SEQ_def Image_def quotient_def split:if_splits)
 
       
   219 
   242 
   220 lemma append_seq_elim:
 
   243 lemma append_seq_elim:
 
   221   assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"
 
   244   assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2"
 
   222   shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> 
   245   shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> 
   223           (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"
 
   246           (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)"
 
   281       }
 
   304       }
 
   282       ultimately show ?thesis by blast
 
   305       ultimately show ?thesis by blast
 
   283     qed
 
   306     qed
 
   284   } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n" 
   307   } thus "tag_str_SEQ L\<^isub>1 L\<^isub>2 m = tag_str_SEQ L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 ;; L\<^isub>2) n" 
   285     by (auto simp add: str_eq_def str_eq_rel_def)
 
   308     by (auto simp add: str_eq_def str_eq_rel_def)
 
   286 qed 
   309 qed
 
   287 
   310 
   288 lemma quot_seq_finiteI:
 
   311 lemma quot_seq_finiteI [intro]:
 
   289   "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> 
   312   fixes L1 L2::"lang"
 
   290   \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1 ;; L\<^isub>2))"
 
   313   assumes fin1: "finite (UNIV // \<approx>L1)" 
   291   apply (rule_tac tag = "tag_str_SEQ L\<^isub>1 L\<^isub>2" in tag_finite_imageD)  
   314   and     fin2: "finite (UNIV // \<approx>L2)" 
   292   by (auto intro:tag_str_SEQ_injI elim:tag_str_seq_range_finite)
 
   315   shows "finite (UNIV // \<approx>(L1 ;; L2))"
 
   293 
   316 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD)
 
   294 subsection {* The case for @{text "ALT"} *}
 
   317   show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y"
 
       
   318     by (rule tag_str_SEQ_injI)
 
       
   319 next
 
       
   320   have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" 
       
   321     using fin1 fin2 by auto
 
       
   322   show "finite (range (tag_str_SEQ L1 L2))" 
       
   323     unfolding tag_str_SEQ_def
 
       
   324     apply(rule finite_subset[OF _ *])
 
       
   325     unfolding quotient_def
 
       
   326     by auto
 
       
   327 qed
 
       
   328 
       
   329 
       
   330 subsection {* The case for @{const ALT} *}
 
   295 
   331 
   296 definition 
   332 definition 
   297   "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
 
   333   tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"
 
   298 
   334 where
 
   299 lemma quot_union_finiteI:
 
   335   "tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"
 
   300   assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))"
 
   336 
   301   and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
 
   337 
   302   shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
 
   338 lemma quot_union_finiteI [intro]:
 
   303 proof (rule_tac tag = "tag_str_ALT L\<^isub>1 L\<^isub>2" in tag_finite_imageD)
 
   339   fixes L1 L2::"lang"
 
   304   show "\<And>m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n \<Longrightarrow> m \<approx>(L\<^isub>1 \<union> L\<^isub>2) n"
 
   340   assumes finite1: "finite (UNIV // \<approx>L1)"
 
   305     unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto
 
   341   and     finite2: "finite (UNIV // \<approx>L2)"
 
       
   342   shows "finite (UNIV // \<approx>(L1 \<union> L2))"
 
       
   343 proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD)
 
       
   344   show "\<And>x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \<Longrightarrow> x \<approx>(L1 \<union> L2) y"
 
       
   345     unfolding tag_str_ALT_def 
       
   346     unfolding str_eq_def
 
       
   347     unfolding Image_def 
       
   348     unfolding str_eq_rel_def
 
       
   349     by auto
 
   306 next
 
   350 next
 
   307   show "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" using finite1 finite2
 
   351   have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))" 
   308     apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" in finite_subset)
 
   352     using finite1 finite2 by auto
 
   309     by (auto simp:tag_str_ALT_def Image_def quotient_def)
 
   353   show "finite (range (tag_str_ALT L1 L2))"
 
   310 qed
 
   354     unfolding tag_str_ALT_def
 
   311 
   355     apply(rule finite_subset[OF _ *])
 
   312 subsection {*
 
   356     unfolding quotient_def
 
   313   The case for @{text "STAR"}
 
   357     by auto
 
   314   *}
 
   358 qed
 
       
   359 
       
   360 subsection {* The case for @{const "STAR"} *}
 
   315 
   361 
   316 text {* 
   362 text {* 
   317   This turned out to be the trickiest case. 
   363   This turned out to be the trickiest case. 
   318   *} (* I will make some illustrations for it. *)
 
   364   *} (* I will make some illustrations for it. *)
 
   319 
   365 
   320 definition 
   366 definition 
   321   "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<star>}"
 
   367   tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
 
   322 
   368 where
 
   323 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> 
   369   "tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
 
   324            (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))"
 
   370 
       
   371 
       
   372 lemma finite_set_has_max: 
       
   373   "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))"
 
   325 proof (induct rule:finite.induct)
 
   374 proof (induct rule:finite.induct)
 
   326   case emptyI thus ?case by simp
 
   375   case emptyI thus ?case by simp
 
   327 next
 
   376 next
 
   328   case (insertI A a)
 
   377   case (insertI A a)
 
   329   show ?case
 
   378   show ?case
 
   347 
   396 
   348 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"
 
   397 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}"
 
   349 apply (induct x rule:rev_induct, simp)
 
   398 apply (induct x rule:rev_induct, simp)
 
   350 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
 
   399 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}")
 
   351 by (auto simp:strict_prefix_def)
 
   400 by (auto simp:strict_prefix_def)
 
   352 
       
   353 
       
   354 lemma tag_str_star_range_finite:
 
       
   355   "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (range (tag_str_STAR L\<^isub>1))"
 
       
   356 apply (rule_tac B = "Pow (UNIV // \<approx>L\<^isub>1)" in finite_subset)
 
       
   357 by (auto simp:tag_str_STAR_def Image_def 
       
   358                        quotient_def split:if_splits)
 
       
   359 
   401 
   360 lemma tag_str_STAR_injI:
 
   402 lemma tag_str_STAR_injI:
 
   361   "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
 
   403   "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
 
   362 proof-
 
   404 proof-
 
   363   { fix x y z
 
   405   { fix x y z
 
   439     qed      
   481     qed      
   440   } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
 
   482   } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
 
   441     by (auto simp add:str_eq_def str_eq_rel_def)
 
   483     by (auto simp add:str_eq_def str_eq_rel_def)
 
   442 qed
 
   484 qed
 
   443 
   485 
   444 lemma quot_star_finiteI:
 
   486 lemma quot_star_finiteI [intro]:
 
   445   "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1\<star>))"
 
   487   fixes L1::"lang"
 
   446   apply (rule_tac tag = "tag_str_STAR L\<^isub>1" in tag_finite_imageD)
 
   488   assumes finite1: "finite (UNIV // \<approx>L1)"
 
   447   by (auto intro:tag_str_STAR_injI elim:tag_str_star_range_finite)
 
   489   shows "finite (UNIV // \<approx>(L1\<star>))"
 
   448 
   490 proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD)
 
   449 subsection {*
 
   491   show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y"
 
   450   The main lemma
 
   492     by (rule tag_str_STAR_injI)
 
   451   *}
 
       
   452 
       
   453 lemma easier_directio\<nu>:
 
       
   454   "Lang = L (r::rexp) \<Longrightarrow> finite (UNIV // (\<approx>Lang))"
 
       
   455 proof (induct arbitrary:Lang rule:rexp.induct)
 
       
   456   case NULL
 
       
   457   have "UNIV // (\<approx>{}) \<subseteq> {UNIV} "
 
       
   458     by (auto simp:quotient_def str_eq_rel_def str_eq_def)
 
       
   459   with prems show "?case" by (auto intro:finite_subset)
 
       
   460 next
 
   493 next
 
   461   case EMPTY
 
   494   have *: "finite (Pow (UNIV // \<approx>L1))" 
   462   have "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}" 
   495     using finite1 by auto
 
   463     by (rule quot_empty_subset)
 
   496   show "finite (range (tag_str_STAR L1))"
 
   464   with prems show ?case by (auto intro:finite_subset)
 
   497     unfolding tag_str_STAR_def
 
   465 next
 
   498     apply(rule finite_subset[OF _ *])
 
   466   case (CHAR c)
 
   499     unfolding quotient_def
 
   467   have "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" 
   500     by auto
 
   468     by (rule quot_char_subset)
 
   501 qed
 
   469   with prems show ?case by (auto intro:finite_subset)
 
   502 
   470 next
 
   503 
   471   case (SEQ r\<^isub>1 r\<^isub>2)
 
   504 subsection {* The main lemma *}
 
   472   have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk> 
   505 
   473             \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 ;; L r\<^isub>2))"
 
   506 lemma rexp_imp_finite:
 
   474     by (erule quot_seq_finiteI, simp)
 
   507   fixes r::"rexp"
 
   475   with prems show ?case by simp
 
   508   shows "finite (UNIV // \<approx>(L r))"
 
   476 next
 
   509 by (induct r) (auto)
 
   477   case (ALT r\<^isub>1 r\<^isub>2)
 
   510 
   478   have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk> 
       
   479             \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 \<union> L r\<^isub>2))"
 
       
   480     by (erule quot_union_finiteI, simp)
 
       
   481   with prems show ?case by simp  
       
   482 next
 
       
   483   case (STAR r)
 
       
   484   have "finite (UNIV // \<approx>(L r)) 
       
   485             \<Longrightarrow> finite (UNIV // \<approx>((L r)\<star>))"
 
       
   486     by (erule quot_star_finiteI)
 
       
   487   with prems show ?case by simp
 
       
   488 qed 
       
   489 
   511 
   490 end
 
   512 end
 
   491 
   513
regexp