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 31 b6815473ee2e
parent 30 f5db9e08effc
child 33 a3d1868ada7d
equal deleted inserted replaced
30:f5db9e08effc 31:b6815473ee2e 
     1 theory Myhill
 
     1 theory Myhill
 
     2   imports Main List_Prefix
 
     2   imports Main List_Prefix Prefix_subtract
 
     3 begin
 
     3 begin
 
     4 
     4 
     5 section {* Preliminary definitions *}
 
     5 section {* Preliminary definitions *}
 
     6 
     6 
     7 text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *}
 
     7 text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *}
 
   178 (* Just a technical lemma. *)
 
   178 (* Just a technical lemma. *)
 
   179 lemma [simp]:
 
   179 lemma [simp]:
 
   180   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 
   180   shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
 
   181 by simp
 
   181 by simp
 
   182 
   182 
   183 
       
   184 text {*
 
   183 text {*
 
   185   @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.
 
   184   @{text "\<approx>L"} is an equivalent class defined by language @{text "Lang"}.
 
   186 *}
 
   185 *}
 
   187 definition
 
   186 definition
 
   188   str_eq_rel ("\<approx>_")
 
   187   str_eq_rel ("\<approx>_")
 
   450   *}
 
   449   *}
 
   451 definition 
   450 definition 
   452   "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"
 
   451   "valid_eqns ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> (X = L rhs)"
 
   453 
   452 
   454 text {*
 
   453 text {*
 
   455   @{text "rhs_nonempty rhs"} requires regular expressions occuring in transitional 
   454   The following @{text "rhs_nonempty rhs"} requires regular expressions occuring in transitional 
   456   items of @{text "rhs"} does not contain empty string. This is necessary for
 
   455   items of @{text "rhs"} does not contain empty string. This is necessary for
 
   457   the application of Arden's transformation to @{text "rhs"}.
 
   456   the application of Arden's transformation to @{text "rhs"}.
 
   458   *}
 
   457   *}
 
   459 definition 
   458 definition 
   460   "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
 
   459   "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)"
 
   461 
   460 
   462 text {*
 
   461 text {*
 
   463   @{text "ardenable ES"} requires that Arden's transformation is applicable
 
   462   The following @{text "ardenable ES"} requires that Arden's transformation is applicable
 
   464   to every equation of equational system @{text "ES"}.
 
   463   to every equation of equational system @{text "ES"}.
 
   465   *}
 
   464   *}
 
   466 definition 
   465 definition 
   467   "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"
 
   466   "ardenable ES \<equiv> \<forall> X rhs. (X, rhs) \<in> ES \<longrightarrow> rhs_nonempty rhs"
 
   468 
   467 
   498 definition 
   497 definition 
   499   "self_contained ES \<equiv> \<forall> (X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"
 
   498   "self_contained ES \<equiv> \<forall> (X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES"
 
   500 
   499 
   501 
   500 
   502 text {*
 
   501 text {*
 
   503   The invariant @{text "Inv(ES)"} is obtained by conjunctioning all the previous
 
   502   The invariant @{text "Inv(ES)"} is a conjunction of all the previously defined constaints.
 
   504   defined constaints on @{text "ES"}.
 
       
   505   *}
 
   503   *}
 
   506 definition 
   504 definition 
   507   "Inv ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 
   505   "Inv ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> 
   508                 non_empty ES \<and> finite_rhs ES \<and> self_contained ES"
 
   506                 non_empty ES \<and> finite_rhs ES \<and> self_contained ES"
 
   509 
   507 
   510 subsection {* Proof for this direction *}
 
   508 subsection {* The proof of this direction *}
 
   511 
   509 
   512 
   510 subsubsection {* Basic properties *}
 
   513 
   511 
   514 text {*
 
   512 text {*
 
   515   The following are some basic properties of the above definitions.
 
   513   The following are some basic properties of the above definitions.
 
   516 *}
 
   514 *}
 
   517 
   515 
   582 lemma lefts_of_union_distrib:
 
   580 lemma lefts_of_union_distrib:
 
   583   "lefts_of A \<union> lefts_of B = lefts_of (A \<union> B)"
 
   581   "lefts_of A \<union> lefts_of B = lefts_of (A \<union> B)"
 
   584 by (auto simp:lefts_of_def)
 
   582 by (auto simp:lefts_of_def)
 
   585 
   583 
   586 
   584 
   587 text {*
 
   585 subsubsection {* Intialization *}
 
   588   The following several lemmas until @{text "init_ES_satisfy_Inv"} are
 
   586 
   589   to prove that initial equational system satisfies invariant @{text "Inv"}.
 
   587 text {*
 
       
   588   The following several lemmas until @{text "init_ES_satisfy_Inv"} shows that
 
       
   589   the initial equational system satisfies invariant @{text "Inv"}.
 
   590   *}
 
   590   *}
 
   591 
   591 
   592 lemma defined_by_str:
 
   592 lemma defined_by_str:
 
   593   "\<lbrakk>s \<in> X; X \<in> UNIV // (\<approx>Lang)\<rbrakk> \<Longrightarrow> X = (\<approx>Lang) `` {s}"
 
   593   "\<lbrakk>s \<in> X; X \<in> UNIV // (\<approx>Lang)\<rbrakk> \<Longrightarrow> X = (\<approx>Lang) `` {s}"
 
   594 by (auto simp:quotient_def Image_def str_eq_rel_def)
 
   594 by (auto simp:quotient_def Image_def str_eq_rel_def)
 
   688   moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))"
 
   688   moreover have "self_contained (eqs (UNIV // (\<approx>Lang)))"
 
   689     by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def)
 
   689     by (auto simp:self_contained_def eqs_def init_rhs_def classes_of_def lefts_of_def)
 
   690   ultimately show ?thesis by (simp add:Inv_def)
 
   690   ultimately show ?thesis by (simp add:Inv_def)
 
   691 qed
 
   691 qed
 
   692 
   692 
   693 text {*
 
   693 subsubsection {* 
   694   From this point until @{text "iteration_step"}, we are trying to prove 
   694   Interation step
 
       
   695   *}
 
       
   696 
       
   697 text {*
 
       
   698   From this point until @{text "iteration_step"}, it is proved
 
   695   that there exists iteration steps which keep @{text "Inv(ES)"} while
 
   699   that there exists iteration steps which keep @{text "Inv(ES)"} while
 
   696   decreasing the size of @{text "ES"} with every iteration.
 
   700   decreasing the size of @{text "ES"}.
 
   697   *}
 
   701   *}
 
   698 lemma arden_variate_keeps_eq:
 
   702 lemma arden_variate_keeps_eq:
 
   699   assumes l_eq_r: "X = L rhs"
 
   703   assumes l_eq_r: "X = L rhs"
 
   700   and not_empty: "[] \<notin> L (rexp_of rhs X)"
 
   704   and not_empty: "[] \<notin> L (rexp_of rhs X)"
 
   701   and finite: "finite rhs"
 
   705   and finite: "finite rhs"
 
   971     qed
 
   975     qed
 
   972     ultimately show ?thesis by simp
 
   976     ultimately show ?thesis by simp
 
   973   qed
 
   977   qed
 
   974   thus ?thesis by blast
 
   978   thus ?thesis by blast
 
   975 qed
 
   979 qed
 
       
   980 
       
   981 subsubsection {*
 
       
   982   Conclusion of the proof
 
       
   983   *}
 
   976 
   984 
   977 text {*
 
   985 text {*
 
   978   From this point until @{text "hard_direction"}, the hard direction is proved
 
   986   From this point until @{text "hard_direction"}, the hard direction is proved
 
   979   through a simple application of the iteration principle.
 
   987   through a simple application of the iteration principle.
 
   980 *}
 
   988 *}
 
  1108   in standard library (@{text "finite_imageD"}), which says: if the image of an injective 
  1116   in standard library (@{text "finite_imageD"}), which says: if the image of an injective 
  1109   function on a set @{text "A"} is finite, then @{text "A"} is finite. It can be shown that
 
  1117   function on a set @{text "A"} is finite, then @{text "A"} is finite. It can be shown that
 
  1110   the function obtained by llifting @{text "tag"}
 
  1118   the function obtained by llifting @{text "tag"}
 
  1111   to the level of equalent classes (i.e. @{text "((op `) tag)"}) is injective 
  1119   to the level of equalent classes (i.e. @{text "((op `) tag)"}) is injective 
  1112   (by lemma @{text "tag_image_injI"}) and the image of this function is finite 
  1120   (by lemma @{text "tag_image_injI"}) and the image of this function is finite 
  1113   (with the help of lemma @{text "finite_tag_imageI"}).
 
  1121   (with the help of lemma @{text "finite_tag_imageI"}). This argument is formalized
 
  1114 
  1122   by the following lemma @{text "tag_finite_imageD"}.
 
  1115   BUT, I think this argument can be encapsulated by one lemma instead of the current presentation.
 
  1123   *}
 
  1116   *}
 
  1124 
  1117 
  1125 lemma tag_finite_imageD:
 
  1118 lemma eq_class_equalI:
 
  1126   assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>lang n"
 
  1119   "\<lbrakk>X \<in> UNIV // \<approx>lang; Y \<in> UNIV // \<approx>lang; x \<in> X; y \<in> Y; x \<approx>lang y\<rbrakk> 
  1127   and range: "finite (range tag)"
 
  1120                          \<Longrightarrow> X = Y"
 
  1128   shows "finite (UNIV // (\<approx>lang))"
 
  1121 by (auto simp:quotient_def str_eq_rel_def str_eq_def)
 
  1129 proof (rule_tac f = "(op `) tag" in finite_imageD)
 
  1122 
  1130   show "finite (op ` tag ` UNIV // \<approx>lang)" using range
 
  1123 lemma tag_image_injI:
 
  1131     apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset)
 
  1124   assumes str_inj: "\<And> x y. tag x = tag (y::string) \<Longrightarrow> x \<approx>lang y"
 
  1132     by (auto simp add:image_def Pow_def)
 
  1125   shows "inj_on ((op `) tag) (UNIV // \<approx>lang)"
 
  1133 next
 
  1126 proof-
 
  1134   show "inj_on (op ` tag) (UNIV // \<approx>lang)" 
  1127   { fix X Y
 
  1135   proof-
 
  1128     assume X_in: "X \<in> UNIV // \<approx>lang"
 
  1136     { fix X Y
 
  1129       and  Y_in: "Y \<in> UNIV // \<approx>lang"
 
  1137       assume X_in: "X \<in> UNIV // \<approx>lang"
 
  1130       and  tag_eq: "tag ` X = tag ` Y"
 
  1138         and  Y_in: "Y \<in> UNIV // \<approx>lang"
 
  1131     then obtain x y where "x \<in> X" and "y \<in> Y" and "tag x = tag y"
 
  1139         and  tag_eq: "tag ` X = tag ` Y"
 
  1132       unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def
 
  1140       then obtain x y where "x \<in> X" and "y \<in> Y" and "tag x = tag y"
 
  1133       apply simp by blast
 
  1141         unfolding quotient_def Image_def str_eq_rel_def str_eq_def image_def
 
  1134     with X_in Y_in str_inj
 
  1142         apply simp by blast
 
  1135     have "X = Y" by (rule_tac eq_class_equalI, simp+)
 
  1143       with X_in Y_in str_inj[of x y]
 
  1136   }
 
  1144       have "X = Y" by (auto simp:quotient_def str_eq_rel_def str_eq_def) 
  1137   thus ?thesis unfolding inj_on_def by auto
 
  1145     } thus ?thesis unfolding inj_on_def by auto
 
  1138 qed
 
  1146   qed
 
  1139 
  1147 qed
 
  1140 lemma finite_tag_imageI: 
       
  1141   "finite (range tag) \<Longrightarrow> finite (((op `) tag) ` S)"
 
       
  1142 apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset)
 
       
  1143 by (auto simp add:image_def Pow_def)
 
       
  1144 
       
  1145 
       
  1146 subsection {* A small theory for list difference *}
 
       
  1147 
       
  1148 text {*
 
       
  1149   The notion of list diffrence is need to make proofs more readable.
 
       
  1150   *}
 
       
  1151 
       
  1152 (* list_diff:: list substract, once different return tailer *)
 
       
  1153 fun list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)
 
       
  1154 where
 
       
  1155   "list_diff []  xs = []" |
 
       
  1156   "list_diff (x#xs) [] = x#xs" |
 
       
  1157   "list_diff (x#xs) (y#ys) = (if x = y then list_diff xs ys else (x#xs))"
 
       
  1158 
       
  1159 lemma [simp]: "(x @ y) - x = y"
 
       
  1160 apply (induct x)
 
       
  1161 by (case_tac y, simp+)
 
       
  1162 
       
  1163 lemma [simp]: "x - x = []"
 
       
  1164 by (induct x, auto)
 
       
  1165 
       
  1166 lemma [simp]: "x = xa @ y \<Longrightarrow> x - xa = y "
 
       
  1167 by (induct x, auto)
 
       
  1168 
       
  1169 lemma [simp]: "x - [] = x"
 
       
  1170 by (induct x, auto)
 
       
  1171 
       
  1172 lemma [simp]: "(x - y = []) \<Longrightarrow> (x \<le> y)"
 
       
  1173 proof-   
       
  1174   have "\<exists>xa. x = xa @ (x - y) \<and> xa \<le> y"
 
       
  1175     apply (rule list_diff.induct[of _ x y], simp+)
 
       
  1176     by (clarsimp, rule_tac x = "y # xa" in exI, simp+)
 
       
  1177   thus "(x - y = []) \<Longrightarrow> (x \<le> y)" by simp
 
       
  1178 qed
 
       
  1179 
       
  1180 lemma diff_prefix:
 
       
  1181   "\<lbrakk>c \<le> a - b; b \<le> a\<rbrakk> \<Longrightarrow> b @ c \<le> a"
 
       
  1182 by (auto elim:prefixE)
 
       
  1183 
       
  1184 lemma diff_diff_appd: 
       
  1185   "\<lbrakk>c < a - b; b < a\<rbrakk> \<Longrightarrow> (a - b) - c = a - (b @ c)"
 
       
  1186 apply (clarsimp simp:strict_prefix_def)
 
       
  1187 by (drule diff_prefix, auto elim:prefixE)
 
       
  1188 
       
  1189 lemma app_eq_cases[rule_format]:
 
       
  1190   "\<forall> x . x @ y = m @ n \<longrightarrow> (x \<le> m \<or> m \<le> x)"
 
       
  1191 apply (induct y, simp)
 
       
  1192 apply (clarify, drule_tac x = "x @ [a]" in spec)
 
       
  1193 by (clarsimp, auto simp:prefix_def)
 
       
  1194 
       
  1195 lemma app_eq_dest:
 
       
  1196   "x @ y = m @ n \<Longrightarrow> 
       
  1197                (x \<le> m \<and> (m - x) @ n = y) \<or> (m \<le> x \<and> (x - m) @ y = n)"
 
       
  1198 by (frule_tac app_eq_cases, auto elim:prefixE)
 
       
  1199 
  1148 
  1200 subsection {* Lemmas for basic cases *}
 
  1149 subsection {* Lemmas for basic cases *}
 
  1201 
  1150 
  1202 text {*
 
  1151 text {*
 
  1203   The the final result of this direction is in @{text "easier_direction"}, which
 
  1152   The the final result of this direction is in @{text "easier_direction"}, which
 
  1336   } 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" 
  1285   } 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" 
  1337     by (auto simp add: str_eq_def str_eq_rel_def)
 
  1286     by (auto simp add: str_eq_def str_eq_rel_def)
 
  1338 qed 
  1287 qed 
  1339 
  1288 
  1340 lemma quot_seq_finiteI:
 
  1289 lemma quot_seq_finiteI:
 
  1341   assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))"
 
  1290   "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> 
  1342   and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
 
  1291   \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1 ;; L\<^isub>2))"
 
  1343   shows "finite (UNIV // \<approx>(L\<^isub>1 ;; L\<^isub>2))"
 
  1292   apply (rule_tac tag = "tag_str_SEQ L\<^isub>1 L\<^isub>2" in tag_finite_imageD)  
  1344 proof(rule_tac f = "(op `) (tag_str_SEQ L\<^isub>1 L\<^isub>2)" in finite_imageD)
 
  1293   by (auto intro:tag_str_SEQ_injI elim:tag_str_seq_range_finite)
 
  1345   show "finite (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2) ` UNIV // \<approx>L\<^isub>1 ;; L\<^isub>2)" 
       
  1346     using finite1 finite2
 
       
  1347     by (auto intro:finite_tag_imageI tag_str_seq_range_finite)
 
       
  1348 next
 
       
  1349   show  "inj_on (op ` (tag_str_SEQ L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>L\<^isub>1 ;; L\<^isub>2)"
 
       
  1350     apply (rule tag_image_injI)
 
       
  1351     apply (rule tag_str_SEQ_injI)
 
       
  1352     by (auto intro:tag_image_injI tag_str_SEQ_injI simp:)
 
       
  1353 qed
 
       
  1354 
  1294 
  1355 subsection {* The case for @{text "ALT"} *}
 
  1295 subsection {* The case for @{text "ALT"} *}
 
  1356 
  1296 
  1357 definition 
  1297 definition 
  1358   "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
 
  1298   "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
 
  1359 
       
  1360 lemma tag_str_alt_range_finite:
 
       
  1361   "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> 
       
  1362                               \<Longrightarrow> finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))"
 
       
  1363 apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" in finite_subset)
 
       
  1364 by (auto simp:tag_str_ALT_def Image_def quotient_def)
 
       
  1365 
  1299 
  1366 lemma quot_union_finiteI:
 
  1300 lemma quot_union_finiteI:
 
  1367   assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))"
 
  1301   assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))"
 
  1368   and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
 
  1302   and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
 
  1369   shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
 
  1303   shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
 
  1370 proof(rule_tac f = "(op `) (tag_str_ALT L\<^isub>1 L\<^isub>2)" in finite_imageD)
 
  1304 proof (rule_tac tag = "tag_str_ALT L\<^isub>1 L\<^isub>2" in tag_finite_imageD)
 
  1371   show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` UNIV // \<approx>L\<^isub>1 \<union> L\<^isub>2)" 
  1305   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"
 
  1372     using finite1 finite2
 
  1306     unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto
 
  1373     by (auto intro:finite_tag_imageI tag_str_alt_range_finite)
 
       
  1374 next
 
  1307 next
 
  1375   show "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>L\<^isub>1 \<union> L\<^isub>2)"
 
  1308   show "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" using finite1 finite2
 
  1376   proof-
 
  1309     apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" in finite_subset)
 
  1377     have "\<And>m n. tag_str_ALT L\<^isub>1 L\<^isub>2 m = tag_str_ALT L\<^isub>1 L\<^isub>2 n 
  1310     by (auto simp:tag_str_ALT_def Image_def quotient_def)
 
  1378                          \<Longrightarrow> m \<approx>(L\<^isub>1 \<union> L\<^isub>2) n"
 
  1311 qed
 
  1379       unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto
 
       
  1380     thus ?thesis by (auto intro:tag_image_injI)
 
       
  1381   qed
 
       
  1382 qed
 
       
  1383 
       
  1384 
  1312 
  1385 subsection {*
 
  1313 subsection {*
 
  1386   The case for @{text "STAR"}
 
  1314   The case for @{text "STAR"}
 
  1387   *}
 
  1315   *}
 
  1388 
  1316 
  1389 text {* 
  1317 text {* 
  1390   This turned out to be the most tricky case. 
  1318   This turned out to be the trickiest case. 
  1391   *} (* I will make some illustrations for it. *)
 
  1319   *} (* I will make some illustrations for it. *)
 
  1392 
  1320 
  1393 definition 
  1321 definition 
  1394   "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<star>}"
 
  1322   "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<star>}"
 
  1395 
  1323 
  1513   } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
 
  1441   } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n"
 
  1514     by (auto simp add:str_eq_def str_eq_rel_def)
 
  1442     by (auto simp add:str_eq_def str_eq_rel_def)
 
  1515 qed
 
  1443 qed
 
  1516 
  1444 
  1517 lemma quot_star_finiteI:
 
  1445 lemma quot_star_finiteI:
 
  1518   assumes finite: "finite (UNIV // \<approx>(L\<^isub>1::string set))"
 
  1446   "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1\<star>))"
 
  1519   shows "finite (UNIV // \<approx>(L\<^isub>1\<star>))"
 
  1447   apply (rule_tac tag = "tag_str_STAR L\<^isub>1" in tag_finite_imageD)
 
  1520 proof(rule_tac f = "(op `) (tag_str_STAR L\<^isub>1)" in finite_imageD)
 
  1448   by (auto intro:tag_str_STAR_injI elim:tag_str_star_range_finite)
 
  1521   show "finite (op ` (tag_str_STAR L\<^isub>1) ` UNIV // \<approx>L\<^isub>1\<star>)" using finite
 
       
  1522     by (auto intro:finite_tag_imageI tag_str_star_range_finite)
 
       
  1523 next
 
       
  1524   show "inj_on (op ` (tag_str_STAR L\<^isub>1)) (UNIV // \<approx>L\<^isub>1\<star>)"
 
       
  1525     by (auto intro:tag_image_injI tag_str_STAR_injI)
 
       
  1526 qed
 
       
  1527 
  1449 
  1528 subsection {*
 
  1450 subsection {*
 
  1529   The main lemma
 
  1451   The main lemma
 
  1530   *}
 
  1452   *}
 
  1531 
  1453
regexp