equal
deleted
inserted
replaced
1277 |
1277 |
1278 |
1278 |
1279 subsection {* The case for @{const "SEQ"}*} |
1279 subsection {* The case for @{const "SEQ"}*} |
1280 |
1280 |
1281 definition |
1281 definition |
1282 "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> |
1282 tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)" |
1283 ((\<approx>L\<^isub>1) `` {x}, {(\<approx>L\<^isub>2) `` {x - xa}| xa. xa \<le> x \<and> xa \<in> L\<^isub>1})" |
1283 where |
1284 |
1284 "tag_str_SEQ L1 L2 = (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))" |
1285 lemma tag_str_seq_range_finite: |
|
1286 "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> |
|
1287 \<Longrightarrow> finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))" |
|
1288 apply (rule_tac B = "(UNIV // \<approx>L\<^isub>1) \<times> (Pow (UNIV // \<approx>L\<^isub>2))" in finite_subset) |
|
1289 by (auto simp:tag_str_SEQ_def Image_def quotient_def split:if_splits) |
|
1290 |
1285 |
1291 lemma append_seq_elim: |
1286 lemma append_seq_elim: |
1292 assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2" |
1287 assumes "x @ y \<in> L\<^isub>1 ;; L\<^isub>2" |
1293 shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> |
1288 shows "(\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ y \<in> L\<^isub>2) \<or> |
1294 (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)" |
1289 (\<exists> ya \<le> y. (x @ ya) \<in> L\<^isub>1 \<and> (y - ya) \<in> L\<^isub>2)" |
1355 } 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" |
1350 } 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" |
1356 by (auto simp add: str_eq_def str_eq_rel_def) |
1351 by (auto simp add: str_eq_def str_eq_rel_def) |
1357 qed |
1352 qed |
1358 |
1353 |
1359 lemma quot_seq_finiteI [intro]: |
1354 lemma quot_seq_finiteI [intro]: |
1360 "\<lbrakk>finite (UNIV // \<approx>L\<^isub>1); finite (UNIV // \<approx>L\<^isub>2)\<rbrakk> |
1355 fixes L1 L2::"lang" |
1361 \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1 ;; L\<^isub>2))" |
1356 assumes fin1: "finite (UNIV // \<approx>L1)" |
1362 apply (rule_tac tag = "tag_str_SEQ L\<^isub>1 L\<^isub>2" in tag_finite_imageD) |
1357 and fin2: "finite (UNIV // \<approx>L2)" |
1363 by (auto intro:tag_str_SEQ_injI elim:tag_str_seq_range_finite) |
1358 shows "finite (UNIV // \<approx>(L1 ;; L2))" |
|
1359 proof (rule_tac tag = "tag_str_SEQ L1 L2" in tag_finite_imageD) |
|
1360 show "\<And>x y. tag_str_SEQ L1 L2 x = tag_str_SEQ L1 L2 y \<Longrightarrow> x \<approx>(L1 ;; L2) y" |
|
1361 by (rule tag_str_SEQ_injI) |
|
1362 next |
|
1363 have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))" |
|
1364 using fin1 fin2 by auto |
|
1365 show "finite (range (tag_str_SEQ L1 L2))" |
|
1366 unfolding tag_str_SEQ_def |
|
1367 apply(rule finite_subset[OF _ *]) |
|
1368 unfolding quotient_def |
|
1369 by auto |
|
1370 qed |
1364 |
1371 |
1365 |
1372 |
1366 subsection {* The case for @{const "ALT"} *} |
1373 subsection {* The case for @{const "ALT"} *} |
1367 |
1374 |
1368 definition |
1375 definition |
1382 unfolding str_eq_def |
1389 unfolding str_eq_def |
1383 unfolding Image_def |
1390 unfolding Image_def |
1384 unfolding str_eq_rel_def |
1391 unfolding str_eq_rel_def |
1385 by auto |
1392 by auto |
1386 next |
1393 next |
1387 have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))" using finite1 finite2 by auto |
1394 have *: "finite ((UNIV // \<approx>L1) \<times> (UNIV // \<approx>L2))" |
|
1395 using finite1 finite2 by auto |
1388 show "finite (range (tag_str_ALT L1 L2))" |
1396 show "finite (range (tag_str_ALT L1 L2))" |
1389 unfolding tag_str_ALT_def |
1397 unfolding tag_str_ALT_def |
1390 apply(rule finite_subset[OF _ *]) |
1398 apply(rule finite_subset[OF _ *]) |
1391 unfolding quotient_def |
1399 unfolding quotient_def |
1392 by auto |
1400 by auto |
1398 text {* |
1406 text {* |
1399 This turned out to be the trickiest case. |
1407 This turned out to be the trickiest case. |
1400 *} (* I will make some illustrations for it. *) |
1408 *} (* I will make some illustrations for it. *) |
1401 |
1409 |
1402 definition |
1410 definition |
1403 "tag_str_STAR L\<^isub>1 x \<equiv> {(\<approx>L\<^isub>1) `` {x - xa} | xa. xa < x \<and> xa \<in> L\<^isub>1\<star>}" |
1411 tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set" |
|
1412 where |
|
1413 "tag_str_STAR L1 = (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})" |
1404 |
1414 |
1405 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
1415 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> |
1406 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
1416 (\<exists> max \<in> A. \<forall> a \<in> A. f a <= (f max :: nat))" |
1407 proof (induct rule:finite.induct) |
1417 proof (induct rule:finite.induct) |
1408 case emptyI thus ?case by simp |
1418 case emptyI thus ?case by simp |
1429 |
1439 |
1430 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}" |
1440 lemma finite_strict_prefix_set: "finite {xa. xa < (x::string)}" |
1431 apply (induct x rule:rev_induct, simp) |
1441 apply (induct x rule:rev_induct, simp) |
1432 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
1442 apply (subgoal_tac "{xa. xa < xs @ [x]} = {xa. xa < xs} \<union> {xs}") |
1433 by (auto simp:strict_prefix_def) |
1443 by (auto simp:strict_prefix_def) |
1434 |
|
1435 |
|
1436 lemma tag_str_star_range_finite: |
|
1437 "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (range (tag_str_STAR L\<^isub>1))" |
|
1438 apply (rule_tac B = "Pow (UNIV // \<approx>L\<^isub>1)" in finite_subset) |
|
1439 by (auto simp:tag_str_STAR_def Image_def |
|
1440 quotient_def split:if_splits) |
|
1441 |
1444 |
1442 lemma tag_str_STAR_injI: |
1445 lemma tag_str_STAR_injI: |
1443 "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n" |
1446 "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n" |
1444 proof- |
1447 proof- |
1445 { fix x y z |
1448 { fix x y z |
1521 qed |
1524 qed |
1522 } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n" |
1525 } thus "tag_str_STAR L\<^isub>1 m = tag_str_STAR L\<^isub>1 n \<Longrightarrow> m \<approx>(L\<^isub>1\<star>) n" |
1523 by (auto simp add:str_eq_def str_eq_rel_def) |
1526 by (auto simp add:str_eq_def str_eq_rel_def) |
1524 qed |
1527 qed |
1525 |
1528 |
|
1529 |
1526 lemma quot_star_finiteI [intro]: |
1530 lemma quot_star_finiteI [intro]: |
1527 "finite (UNIV // \<approx>L\<^isub>1) \<Longrightarrow> finite (UNIV // \<approx>(L\<^isub>1\<star>))" |
1531 fixes L1::"lang" |
1528 apply (rule_tac tag = "tag_str_STAR L\<^isub>1" in tag_finite_imageD) |
1532 assumes finite1: "finite (UNIV // \<approx>L1)" |
1529 by (auto intro:tag_str_STAR_injI elim:tag_str_star_range_finite) |
1533 shows "finite (UNIV // \<approx>(L1\<star>))" |
|
1534 proof (rule_tac tag = "tag_str_STAR L1" in tag_finite_imageD) |
|
1535 show "\<And>x y. tag_str_STAR L1 x = tag_str_STAR L1 y \<Longrightarrow> x \<approx>(L1\<star>) y" |
|
1536 by (rule tag_str_STAR_injI) |
|
1537 next |
|
1538 have *: "finite (Pow (UNIV // \<approx>L1))" |
|
1539 using finite1 by auto |
|
1540 show "finite (range (tag_str_STAR L1))" |
|
1541 unfolding tag_str_STAR_def |
|
1542 apply(rule finite_subset[OF _ *]) |
|
1543 unfolding quotient_def |
|
1544 by auto |
|
1545 qed |
1530 |
1546 |
1531 |
1547 |
1532 subsection {* The main lemma *} |
1548 subsection {* The main lemma *} |
1533 |
1549 |
1534 lemma rexp_imp_finite: |
1550 lemma rexp_imp_finite: |