28 text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *}

    28 types lang = "string set"

    29 definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)

    29 

    30 text {* 

    31   Sequential composition of two languages @{text "L1"} and @{text "L2"} 

    32 *}

    33 

    34 

    35 definition Seq :: "lang \<Rightarrow> lang \<Rightarrow> lang" ("_ ;; _" [100,100] 100)

   208   str_eq_rel ("\<approx>_")

   215   str_eq_rel ("\<approx>_" [100] 100)

  1117 section {* Direction: @{text "regular language \<Rightarrow>finite partition"} *}

  1127 

  1128 

  1129 section {* Direction: @{text "regular language \<Rightarrow> finite partitions"} *}

  1133   The very basic scheme to show the finiteness of the partion generated by a language @{text "Lang"}

  1145   The very basic scheme to show the finiteness of the partion generated by a

  1134   is by attaching tags to every string. The set of tags are carfully choosen to make it finite.

  1146   language @{text "Lang"} is by attaching tags to every string. The set of

  1135   If it can be proved that strings with the same tag are equivlent with respect @{text "Lang"},

  1147   tags are carefully choosen to make it finite.  If it can be proved that

  1136   then the partition given rise by @{text "Lang"} must be finite. The reason for this is a lemma 

  1148   strings with the same tag are equivlent with respect @{text "Lang"}, then

  1137   in standard library (@{text "finite_imageD"}), which says: if the image of an injective 

  1149   the partition given rise by @{text "Lang"} must be finite. The reason for

  1138   function on a set @{text "A"} is finite, then @{text "A"} is finite. It can be shown that

  1150   this is a lemma in standard library (@{text "finite_imageD"}), which says:

  1139   the function obtained by llifting @{text "tag"}

  1151   if the image of an injective function on a set @{text "A"} is finite, then

  1140   to the level of equalent classes (i.e. @{text "((op `) tag)"}) is injective 

  1152   @{text "A"} is finite. It can be shown that the function obtained by

  1141   (by lemma @{text "tag_image_injI"}) and the image of this function is finite 

  1153   lifting @{text "tag"} to the level of equivalence classes (i.e. @{text "((op

  1142   (with the help of lemma @{text "finite_tag_imageI"}). This argument is formalized

  1154   `) tag)"}) is injective (by lemma @{text "tag_image_injI"}) and the image of

  1143   by the following lemma @{text "tag_finite_imageD"}.

  1155   this function is finite (with the help of lemma @{text

  1144   *}

  1156   "finite_tag_imageI"}). This argument is formalized by the following lemma

  1157   @{text "tag_finite_imageD"}.

  1158 

  1159 

  1160   {\bf

  1161   Theorems @{text "tag_image_injI"} and @{text

  1162   "finite_tag_imageI"} do not exist. Can this comment be deleted?

  1163   \marginpar{\bf COMMENT}

  1164   }

  1165 *}

  1147   assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<approx>lang n"

  1168   fixes L1::"lang"

  1169   assumes str_inj: "\<And> m n. tag m = tag n \<Longrightarrow> m \<approx>L1 n"

  1149   shows "finite (UNIV // (\<approx>lang))"

  1171   shows "finite (UNIV // \<approx>L1)"

  1151   show "finite (op ` tag ` UNIV // \<approx>lang)" using range

  1173   show "finite (op ` tag ` UNIV // \<approx>L1)" using range

  1155   show "inj_on (op ` tag) (UNIV // \<approx>lang)" 

  1177   show "inj_on (op ` tag) (UNIV // \<approx>L1)" 

  1158       assume X_in: "X \<in> UNIV // \<approx>lang"

  1180       assume X_in: "X \<in> UNIV // \<approx>L1"

  1159         and  Y_in: "Y \<in> UNIV // \<approx>lang"

  1181         and  Y_in: "Y \<in> UNIV // \<approx>L1"

  1173   The the final result of this direction is in @{text "easier_direction"}, which

  1195   The the final result of this direction is in @{text "rexp_imp_finite"},

  1174   is an induction on the structure of regular expressions. There is one case 

  1196   which is an induction on the structure of regular expressions. There is one

  1175   for each regular expression operator. For basic operators such as @{text "NULL, EMPTY, CHAR c"},

  1197   case for each regular expression operator. For basic operators such as

  1176   the finiteness of their language partition can be established directly with no need

  1198   @{const NULL}, @{const EMPTY}, @{const CHAR}, the finiteness of their 

  1177   of taggiing. This section contains several technical lemma for these base cases.

  1199   language partition can be established directly with no need of tagging. 

  1178 

  1200   This section contains several technical lemma for these base cases.

  1179   The inductive cases involve operators @{text "ALT, SEQ"} and @{text "STAR"}. 

  1201 

  1180   Tagging functions need to be defined individually for each of them. There will be one

  1202   The inductive cases involve operators @{const ALT}, @{const SEQ} and @{const

  1181   dedicated section for each of these cases, and each section goes virtually the same way:

  1203   STAR}. Tagging functions need to be defined individually for each of

  1182   gives definition of the tagging function and prove that strings 

  1204   them. There will be one dedicated section for each of these cases, and each

  1183   with the same tag are equivalent.

  1205   section goes virtually the same way: gives definition of the tagging

  1184   *}

  1206   function and prove that strings with the same tag are equivalent.

  1207 *}

  1208 

  1209 subsection {* The case for @{const "NULL"} *}

  1210 

  1211 lemma quot_null_eq:

  1212   shows "(UNIV // \<approx>{}) = ({UNIV}::lang set)"

  1213   unfolding quotient_def Image_def str_eq_rel_def by auto

  1214 

  1215 lemma quot_null_finiteI [intro]:

  1216   shows "finite ((UNIV // \<approx>{})::lang set)"

  1217 unfolding quot_null_eq by simp

  1218 

  1219 

  1220 subsection {* The case for @{const "EMPTY"} *}

  1221 

  1193   show "x \<in> {{[]}, UNIV - {[]}}" 

  1230   show "x \<in> {{[]}, UNIV - {[]}}"

  1196     have "x = {[]}" by (auto simp:str_eq_rel_def)

  1233     have "x = {[]}" by (auto simp: str_eq_rel_def)

  1200     have "x = UNIV - {[]}" by (auto simp:str_eq_rel_def)

  1237     have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def)

  1230 subsection {* The case for @{text "SEQ"}*}

  1274 lemma quot_char_finiteI [intro]:

  1275   shows "finite (UNIV // (\<approx>{[c]}))"

  1276 by (rule finite_subset[OF quot_char_subset]) (simp)

  1277 

  1278 

  1279 subsection {* The case for @{const "SEQ"}*}

  1310 lemma quot_seq_finiteI:

  1359 lemma quot_seq_finiteI [intro]:

  1316 subsection {* The case for @{text "ALT"} *}

  1365 

  1366 subsection {* The case for @{const "ALT"} *}

  1319   "tag_str_ALT L\<^isub>1 L\<^isub>2 (x::string) \<equiv> ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"

  1369   tag_str_ALT :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang)"

  1320 

  1370 where

  1321 lemma quot_union_finiteI:

  1371   "tag_str_ALT L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, \<approx>L2 `` {x}))"

  1322   assumes finite1: "finite (UNIV // \<approx>(L\<^isub>1::string set))"

  1372 

  1323   and finite2: "finite (UNIV // \<approx>L\<^isub>2)"

  1373 

  1324   shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"

  1374 lemma quot_union_finiteI [intro]:

  1325 proof (rule_tac tag = "tag_str_ALT L\<^isub>1 L\<^isub>2" in tag_finite_imageD)

  1375   fixes L1 L2::"lang"

  1326   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"

  1376   assumes finite1: "finite (UNIV // \<approx>L1)"

  1327     unfolding tag_str_ALT_def str_eq_def Image_def str_eq_rel_def by auto

  1377   and     finite2: "finite (UNIV // \<approx>L2)"

  1378   shows "finite (UNIV // \<approx>(L1 \<union> L2))"

  1379 proof (rule_tac tag = "tag_str_ALT L1 L2" in tag_finite_imageD)

  1380   show "\<And>x y. tag_str_ALT L1 L2 x = tag_str_ALT L1 L2 y \<Longrightarrow> x \<approx>(L1 \<union> L2) y"

  1381     unfolding tag_str_ALT_def 

  1382     unfolding str_eq_def

  1383     unfolding Image_def 

  1384     unfolding str_eq_rel_def

  1385     by auto

  1329   show "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))" using finite1 finite2

  1387   have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))" using finite1 finite2 by auto

  1330     apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)" in finite_subset)

  1388   show "finite (range (tag_str_ALT L1 L2))"

  1331     by (auto simp:tag_str_ALT_def Image_def quotient_def)

  1389     unfolding tag_str_ALT_def

  1332 qed

  1390     apply(rule finite_subset[OF _ *])

  1333 

  1391     unfolding quotient_def

  1334 subsection {*

  1392     by auto

  1335   The case for @{text "STAR"}

  1393 qed

  1336   *}

  1394 

  1395 

  1396 subsection {* The case for @{const "STAR"} *}

  1466 lemma quot_star_finiteI:

  1526 lemma quot_star_finiteI [intro]:

  1471 subsection {*

  1531 

  1472   The main lemma

  1532 subsection {* The main lemma *}

  1473   *}

  1533 

  1474 

  1534 lemma rexp_imp_finite:

  1475 lemma easier_directio\<nu>:

  1535   fixes r::"rexp"

  1476   "Lang = L (r::rexp) \<Longrightarrow> finite (UNIV // (\<approx>Lang))"

  1536   shows "finite (UNIV // \<approx>(L r))"

  1477 proof (induct arbitrary:Lang rule:rexp.induct)

  1537 by (induct r) (auto)

  1478   case NULL

  1538 

  1479   have "UNIV // (\<approx>{}) \<subseteq> {UNIV} "

  1480     by (auto simp:quotient_def str_eq_rel_def str_eq_def)

  1481   with prems show "?case" by (auto intro:finite_subset)

  1482 next

  1483   case EMPTY

  1484   have "UNIV // (\<approx>{[]}) \<subseteq> {{[]}, UNIV - {[]}}" 

  1485     by (rule quot_empty_subset)

  1486   with prems show ?case by (auto intro:finite_subset)

  1487 next

  1488   case (CHAR c)

  1489   have "UNIV // (\<approx>{[c]}) \<subseteq> {{[]},{[c]}, UNIV - {[], [c]}}" 

  1490     by (rule quot_char_subset)

  1491   with prems show ?case by (auto intro:finite_subset)

  1492 next

  1493   case (SEQ r\<^isub>1 r\<^isub>2)

  1494   have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk> 

  1495             \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 ;; L r\<^isub>2))"

  1496     by (erule quot_seq_finiteI, simp)

  1497   with prems show ?case by simp

  1498 next

  1499   case (ALT r\<^isub>1 r\<^isub>2)

  1500   have "\<lbrakk>finite (UNIV // \<approx>(L r\<^isub>1)); finite (UNIV // \<approx>(L r\<^isub>2))\<rbrakk> 

  1501             \<Longrightarrow> finite (UNIV // \<approx>(L r\<^isub>1 \<union> L r\<^isub>2))"

  1502     by (erule quot_union_finiteI, simp)

  1503   with prems show ?case by simp  

  1504 next

  1505   case (STAR r)

  1506   have "finite (UNIV // \<approx>(L r)) 

  1507             \<Longrightarrow> finite (UNIV // \<approx>((L r)\<star>))"

  1508     by (erule quot_star_finiteI)

  1509   with prems show ?case by simp

  1510 qed