522 assumes "b \<notin> subtree r x" |
713 assumes "b \<notin> subtree r x" |
523 shows "subtree (r \<union> {(a, b)}) x = (subtree r x)" |
714 shows "subtree (r \<union> {(a, b)}) x = (subtree r x)" |
524 using assms |
715 using assms |
525 by (auto simp:subtree_def rtrancl_insert) |
716 by (auto simp:subtree_def rtrancl_insert) |
526 |
717 |
|
718 lemma set_add_rootI: |
|
719 assumes "root r a" |
|
720 and "a \<notin> Domain r1" |
|
721 shows "root (r \<union> r1) a" |
|
722 proof - |
|
723 let ?r = "r \<union> r1" |
|
724 { fix a' |
|
725 assume "a' \<in> ancestors ?r a" |
|
726 hence "(a, a') \<in> ?r^+" by (auto simp:ancestors_def) |
|
727 from tranclD[OF this] obtain z where "(a, z) \<in> ?r" by auto |
|
728 moreover have "(a, z) \<notin> r" |
|
729 proof |
|
730 assume "(a, z) \<in> r" |
|
731 with assms(1) show False |
|
732 by (auto simp:root_def ancestors_def) |
|
733 qed |
|
734 ultimately have "(a, z) \<in> r1" by auto |
|
735 with assms(2) |
|
736 have False by (auto) |
|
737 } thus ?thesis by (auto simp:root_def) |
|
738 qed |
|
739 |
|
740 lemma ancestors_mono: |
|
741 assumes "r1 \<subseteq> r2" |
|
742 shows "ancestors r1 x \<subseteq> ancestors r2 x" |
|
743 proof |
|
744 fix a |
|
745 assume "a \<in> ancestors r1 x" |
|
746 hence "(x, a) \<in> r1^+" by (auto simp:ancestors_def) |
|
747 from plus_rpath[OF this] obtain xs where |
|
748 h: "rpath r1 x xs a" "xs \<noteq> []" . |
|
749 have "rpath r2 x xs a" |
|
750 proof(rule rpath_transfer[OF h(1)]) |
|
751 from rpath_edges_on[OF h(1)] and assms |
|
752 show "edges_on (x # xs) \<subseteq> r2" by auto |
|
753 qed |
|
754 from rpath_plus[OF this h(2)] |
|
755 show "a \<in> ancestors r2 x" by (auto simp:ancestors_def) |
|
756 qed |
|
757 |
|
758 lemma subtree_refute: |
|
759 assumes "x \<notin> ancestors r y" |
|
760 and "x \<noteq> y" |
|
761 shows "y \<notin> subtree r x" |
|
762 proof |
|
763 assume "y \<in> subtree r x" |
|
764 thus False |
|
765 by(elim subtreeE, insert assms, auto) |
|
766 qed |
|
767 |
527 subsubsection {* Properties about relational trees *} |
768 subsubsection {* Properties about relational trees *} |
528 |
769 |
529 context rtree |
770 context rtree |
530 begin |
771 begin |
|
772 |
|
773 lemma ancestors_headE: |
|
774 assumes "c \<in> ancestors r a" |
|
775 assumes "(a, b) \<in> r" |
|
776 obtains "b = c" |
|
777 | "c \<in> ancestors r b" |
|
778 proof - |
|
779 from assms(1) |
|
780 have "(a, c) \<in> r^+" by (auto simp:ancestors_def) |
|
781 hence "b = c \<or> c \<in> ancestors r b" |
|
782 proof(cases rule:converse_tranclE[consumes 1]) |
|
783 case 1 |
|
784 with assms(2) and sgv have "b = c" by (auto simp:single_valued_def) |
|
785 thus ?thesis by auto |
|
786 next |
|
787 case (2 y) |
|
788 from 2(1) and assms(2) and sgv have "y = b" by (auto simp:single_valued_def) |
|
789 from 2(2)[unfolded this] have "c \<in> ancestors r b" by (auto simp:ancestors_def) |
|
790 thus ?thesis by auto |
|
791 qed |
|
792 with that show ?thesis by metis |
|
793 qed |
|
794 |
|
795 lemma ancestors_accum: |
|
796 assumes "(a, b) \<in> r" |
|
797 shows "ancestors r a = ancestors r b \<union> {b}" |
|
798 proof - |
|
799 { fix c |
|
800 assume "c \<in> ancestors r a" |
|
801 hence "(a, c) \<in> r^+" by (auto simp:ancestors_def) |
|
802 hence "c \<in> ancestors r b \<union> {b}" |
|
803 proof(cases rule:converse_tranclE[consumes 1]) |
|
804 case 1 |
|
805 with sgv assms have "c = b" by (unfold single_valued_def, auto) |
|
806 thus ?thesis by auto |
|
807 next |
|
808 case (2 c') |
|
809 with sgv assms have "c' = b" by (unfold single_valued_def, auto) |
|
810 from 2(2)[unfolded this] |
|
811 show ?thesis by (auto simp:ancestors_def) |
|
812 qed |
|
813 } moreover { |
|
814 fix c |
|
815 assume "c \<in> ancestors r b \<union> {b}" |
|
816 hence "c = b \<or> c \<in> ancestors r b" by auto |
|
817 hence "c \<in> ancestors r a" |
|
818 proof |
|
819 assume "c = b" |
|
820 from assms[folded this] |
|
821 show ?thesis by (auto simp:ancestors_def) |
|
822 next |
|
823 assume "c \<in> ancestors r b" |
|
824 with assms show ?thesis by (auto simp:ancestors_def) |
|
825 qed |
|
826 } ultimately show ?thesis by auto |
|
827 qed |
|
828 |
|
829 lemma rootI: |
|
830 assumes h: "\<And> x'. x' \<noteq> x \<Longrightarrow> x \<notin> subtree r' x'" |
|
831 and "r' \<subseteq> r" |
|
832 shows "root r' x" |
|
833 proof - |
|
834 from acyclic_subset[OF acl assms(2)] |
|
835 have acl': "acyclic r'" . |
|
836 { fix x' |
|
837 assume "x' \<in> ancestors r' x" |
|
838 hence h1: "(x, x') \<in> r'^+" by (auto simp:ancestors_def) |
|
839 have "x' \<noteq> x" |
|
840 proof |
|
841 assume eq_x: "x' = x" |
|
842 from h1[unfolded this] and acl' |
|
843 show False by (auto simp:acyclic_def) |
|
844 qed |
|
845 moreover from h1 have "x \<in> subtree r' x'" by (auto simp:subtree_def) |
|
846 ultimately have False using h by auto |
|
847 } thus ?thesis by (auto simp:root_def) |
|
848 qed |
531 |
849 |
532 lemma rpath_overlap_oneside: (* ddd *) |
850 lemma rpath_overlap_oneside: (* ddd *) |
533 assumes "rpath r x xs1 x1" |
851 assumes "rpath r x xs1 x1" |
534 and "rpath r x xs2 x2" |
852 and "rpath r x xs2 x2" |
535 and "length xs1 \<le> length xs2" |
853 and "length xs1 \<le> length xs2" |
951 } |
1269 } |
952 -- {* The equality of sets is derived from the two directions just proved. *} |
1270 -- {* The equality of sets is derived from the two directions just proved. *} |
953 ultimately show ?thesis by auto |
1271 ultimately show ?thesis by auto |
954 qed |
1272 qed |
955 |
1273 |
|
1274 lemma set_del_rootI: |
|
1275 assumes "r1 \<subseteq> r" |
|
1276 and "a \<in> Domain r1" |
|
1277 shows "root (r - r1) a" |
|
1278 proof - |
|
1279 let ?r = "r - r1" |
|
1280 { fix a' |
|
1281 assume neq: "a' \<noteq> a" |
|
1282 have "a \<notin> subtree ?r a'" |
|
1283 proof |
|
1284 assume "a \<in> subtree ?r a'" |
|
1285 hence "(a, a') \<in> ?r^*" by (auto simp:subtree_def) |
|
1286 from star_rpath[OF this] obtain xs |
|
1287 where rp: "rpath ?r a xs a'" by auto |
|
1288 from rpathE[OF this] and neq |
|
1289 obtain z zs where h: "(a, z) \<in> ?r" "rpath ?r z zs a'" "xs = z#zs" by auto |
|
1290 from assms(2) obtain z' where z'_in: "(a, z') \<in> r1" by (auto simp:DomainE) |
|
1291 with assms(1) have "(a, z') \<in> r" by auto |
|
1292 moreover from h(1) have "(a, z) \<in> r" by simp |
|
1293 ultimately have "z' = z" using sgv by (auto simp:single_valued_def) |
|
1294 from z'_in[unfolded this] and h(1) show False by auto |
|
1295 qed |
|
1296 } thus ?thesis by (intro rootI, auto) |
|
1297 qed |
|
1298 |
|
1299 lemma edge_del_no_rootI: |
|
1300 assumes "(a, b) \<in> r" |
|
1301 shows "root (r - {(a, b)}) a" |
|
1302 by (rule set_del_rootI, insert assms, auto) |
|
1303 |
|
1304 lemma ancestors_children_unique: |
|
1305 assumes "z1 \<in> ancestors r x \<inter> children r y" |
|
1306 and "z2 \<in> ancestors r x \<inter> children r y" |
|
1307 shows "z1 = z2" |
|
1308 proof - |
|
1309 from assms have h: |
|
1310 "(x, z1) \<in> r^+" "(z1, y) \<in> r" |
|
1311 "(x, z2) \<in> r^+" "(z2, y) \<in> r" |
|
1312 by (auto simp:ancestors_def children_def) |
|
1313 |
|
1314 -- {* From this, a path containing @{text "z1"} is obtained. *} |
|
1315 from plus_rpath[OF h(1)] obtain xs1 |
|
1316 where h1: "rpath r x xs1 z1" "xs1 \<noteq> []" by auto |
|
1317 from rpath_nnl_lastE[OF this] obtain xs1' where eq_xs1: "xs1 = xs1' @ [z1]" |
|
1318 by auto |
|
1319 from h(2) have h2: "rpath r z1 [y] y" by auto |
|
1320 from rpath_appendI[OF h1(1) h2, unfolded eq_xs1] |
|
1321 have rp1: "rpath r x (xs1' @ [z1, y]) y" by simp |
|
1322 |
|
1323 -- {* Then, another path containing @{text "z2"} is obtained. *} |
|
1324 from plus_rpath[OF h(3)] obtain xs2 |
|
1325 where h3: "rpath r x xs2 z2" "xs2 \<noteq> []" by auto |
|
1326 from rpath_nnl_lastE[OF this] obtain xs2' where eq_xs2: "xs2 = xs2' @ [z2]" |
|
1327 by auto |
|
1328 from h(4) have h4: "rpath r z2 [y] y" by auto |
|
1329 from rpath_appendI[OF h3(1) h4, unfolded eq_xs2] |
|
1330 have "rpath r x (xs2' @ [z2, y]) y" by simp |
|
1331 |
|
1332 -- {* Finally @{text "z1 = z2"} is proved by uniqueness of path. *} |
|
1333 from rpath_unique[OF rp1 this] |
|
1334 have "xs1' @ [z1, y] = xs2' @ [z2, y]" . |
|
1335 thus ?thesis by auto |
|
1336 qed |
|
1337 |
|
1338 lemma ancestors_childrenE: |
|
1339 assumes "y \<in> ancestors r x" |
|
1340 obtains "x \<in> children r y" |
|
1341 | z where "z \<in> ancestors r x \<inter> children r y" |
|
1342 proof - |
|
1343 from assms(1) have "(x, y) \<in> r^+" by (auto simp:ancestors_def) |
|
1344 from tranclD2[OF this] obtain z where |
|
1345 h: "(x, z) \<in> r\<^sup>*" "(z, y) \<in> r" by auto |
|
1346 from h(1) |
|
1347 show ?thesis |
|
1348 proof(cases rule:rtranclE) |
|
1349 case base |
|
1350 from h(2)[folded this] have "x \<in> children r y" |
|
1351 by (auto simp:children_def) |
|
1352 thus ?thesis by (intro that, auto) |
|
1353 next |
|
1354 case (step u) |
|
1355 hence "z \<in> ancestors r x" by (auto simp:ancestors_def) |
|
1356 moreover from h(2) have "z \<in> children r y" |
|
1357 by (auto simp:children_def) |
|
1358 ultimately show ?thesis by (intro that, auto) |
|
1359 qed |
|
1360 qed |
|
1361 |
|
1362 |
|
1363 end (* of rtree *) |
|
1364 |
|
1365 lemma subtree_children: |
|
1366 "subtree r x = {x} \<union> (\<Union> (subtree r ` (children r x)))" (is "?L = ?R") |
|
1367 proof - |
|
1368 { fix z |
|
1369 assume "z \<in> ?L" |
|
1370 hence "z \<in> ?R" |
|
1371 proof(cases rule:subtreeE[consumes 1]) |
|
1372 case 2 |
|
1373 hence "(z, x) \<in> r^+" by (auto simp:ancestors_def) |
|
1374 thus ?thesis |
|
1375 proof(rule tranclE) |
|
1376 assume "(z, x) \<in> r" |
|
1377 hence "z \<in> children r x" by (unfold children_def, auto) |
|
1378 moreover have "z \<in> subtree r z" by (auto simp:subtree_def) |
|
1379 ultimately show ?thesis by auto |
|
1380 next |
|
1381 fix c |
|
1382 assume h: "(z, c) \<in> r\<^sup>+" "(c, x) \<in> r" |
|
1383 hence "c \<in> children r x" by (auto simp:children_def) |
|
1384 moreover from h have "z \<in> subtree r c" by (auto simp:subtree_def) |
|
1385 ultimately show ?thesis by auto |
|
1386 qed |
|
1387 qed auto |
|
1388 } moreover { |
|
1389 fix z |
|
1390 assume h: "z \<in> ?R" |
|
1391 have "x \<in> subtree r x" by (auto simp:subtree_def) |
|
1392 moreover { |
|
1393 assume "z \<in> \<Union>(subtree r ` children r x)" |
|
1394 then obtain y where "(y, x) \<in> r" "(z, y) \<in> r^*" |
|
1395 by (auto simp:subtree_def children_def) |
|
1396 hence "(z, x) \<in> r^*" by auto |
|
1397 hence "z \<in> ?L" by (auto simp:subtree_def) |
|
1398 } ultimately have "z \<in> ?L" using h by auto |
|
1399 } ultimately show ?thesis by auto |
|
1400 qed |
|
1401 |
|
1402 context fsubtree |
|
1403 begin |
|
1404 |
|
1405 lemma finite_subtree: |
|
1406 shows "finite (subtree r x)" |
|
1407 proof(induct rule:wf_induct[OF wf]) |
|
1408 case (1 x) |
|
1409 have "finite (\<Union>(subtree r ` children r x))" |
|
1410 proof(rule finite_Union) |
|
1411 show "finite (subtree r ` children r x)" |
|
1412 proof(cases "children r x = {}") |
|
1413 case True |
|
1414 thus ?thesis by auto |
|
1415 next |
|
1416 case False |
|
1417 hence "x \<in> Range r" by (auto simp:children_def) |
|
1418 from fb[rule_format, OF this] |
|
1419 have "finite (children r x)" . |
|
1420 thus ?thesis by (rule finite_imageI) |
|
1421 qed |
|
1422 next |
|
1423 fix M |
|
1424 assume "M \<in> subtree r ` children r x" |
|
1425 then obtain y where h: "y \<in> children r x" "M = subtree r y" by auto |
|
1426 hence "(y, x) \<in> r" by (auto simp:children_def) |
|
1427 from 1[rule_format, OF this, folded h(2)] |
|
1428 show "finite M" . |
|
1429 qed |
|
1430 thus ?case |
|
1431 by (unfold subtree_children finite_Un, auto) |
|
1432 qed |
|
1433 |
956 end |
1434 end |
957 |
1435 |
|
1436 definition "pairself f = (\<lambda>(a, b). (f a, f b))" |
|
1437 |
|
1438 definition "rel_map f r = (pairself f ` r)" |
|
1439 |
|
1440 lemma rel_mapE: |
|
1441 assumes "(a, b) \<in> rel_map f r" |
|
1442 obtains c d |
|
1443 where "(c, d) \<in> r" "(a, b) = (f c, f d)" |
|
1444 using assms |
|
1445 by (unfold rel_map_def pairself_def, auto) |
|
1446 |
|
1447 lemma rel_mapI: |
|
1448 assumes "(a, b) \<in> r" |
|
1449 and "c = f a" |
|
1450 and "d = f b" |
|
1451 shows "(c, d) \<in> rel_map f r" |
|
1452 using assms |
|
1453 by (unfold rel_map_def pairself_def, auto) |
|
1454 |
|
1455 lemma map_appendE: |
|
1456 assumes "map f zs = xs @ ys" |
|
1457 obtains xs' ys' |
|
1458 where "zs = xs' @ ys'" "xs = map f xs'" "ys = map f ys'" |
|
1459 proof - |
|
1460 have "\<exists> xs' ys'. zs = xs' @ ys' \<and> xs = map f xs' \<and> ys = map f ys'" |
|
1461 using assms |
|
1462 proof(induct xs arbitrary:zs ys) |
|
1463 case (Nil zs ys) |
|
1464 thus ?case by auto |
|
1465 next |
|
1466 case (Cons x xs zs ys) |
|
1467 note h = this |
|
1468 show ?case |
|
1469 proof(cases zs) |
|
1470 case (Cons e es) |
|
1471 with h have eq_x: "map f es = xs @ ys" "x = f e" by auto |
|
1472 from h(1)[OF this(1)] |
|
1473 obtain xs' ys' where "es = xs' @ ys'" "xs = map f xs'" "ys = map f ys'" |
|
1474 by blast |
|
1475 with Cons eq_x |
|
1476 have "zs = (e#xs') @ ys' \<and> x # xs = map f (e#xs') \<and> ys = map f ys'" by auto |
|
1477 thus ?thesis by metis |
|
1478 qed (insert h, auto) |
|
1479 qed |
|
1480 thus ?thesis by (auto intro!:that) |
|
1481 qed |
|
1482 |
|
1483 lemma rel_map_mono: |
|
1484 assumes "r1 \<subseteq> r2" |
|
1485 shows "rel_map f r1 \<subseteq> rel_map f r2" |
|
1486 using assms |
|
1487 by (auto simp:rel_map_def pairself_def) |
|
1488 |
|
1489 lemma rel_map_compose [simp]: |
|
1490 shows "rel_map f1 (rel_map f2 r) = rel_map (f1 o f2) r" |
|
1491 by (auto simp:rel_map_def pairself_def) |
|
1492 |
|
1493 lemma edges_on_map: "edges_on (map f xs) = rel_map f (edges_on xs)" |
|
1494 proof - |
|
1495 { fix a b |
|
1496 assume "(a, b) \<in> edges_on (map f xs)" |
|
1497 then obtain l1 l2 where eq_map: "map f xs = l1 @ [a, b] @ l2" |
|
1498 by (unfold edges_on_def, auto) |
|
1499 hence "(a, b) \<in> rel_map f (edges_on xs)" |
|
1500 by (auto elim!:map_appendE intro!:rel_mapI simp:edges_on_def) |
|
1501 } moreover { |
|
1502 fix a b |
|
1503 assume "(a, b) \<in> rel_map f (edges_on xs)" |
|
1504 then obtain c d where |
|
1505 h: "(c, d) \<in> edges_on xs" "(a, b) = (f c, f d)" |
|
1506 by (elim rel_mapE, auto) |
|
1507 then obtain l1 l2 where |
|
1508 eq_xs: "xs = l1 @ [c, d] @ l2" |
|
1509 by (auto simp:edges_on_def) |
|
1510 hence eq_map: "map f xs = map f l1 @ [f c, f d] @ map f l2" by auto |
|
1511 have "(a, b) \<in> edges_on (map f xs)" |
|
1512 proof - |
|
1513 from h(2) have "[f c, f d] = [a, b]" by simp |
|
1514 from eq_map[unfolded this] show ?thesis by (auto simp:edges_on_def) |
|
1515 qed |
|
1516 } ultimately show ?thesis by auto |
|
1517 qed |
|
1518 |
|
1519 lemma image_id: |
|
1520 assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x" |
|
1521 shows "f ` A = A" |
|
1522 using assms by (auto simp:image_def) |
|
1523 |
|
1524 lemma rel_map_inv_id: |
|
1525 assumes "inj_on f ((Domain r) \<union> (Range r))" |
|
1526 shows "(rel_map (inv_into ((Domain r) \<union> (Range r)) f \<circ> f) r) = r" |
|
1527 proof - |
|
1528 let ?f = "(inv_into (Domain r \<union> Range r) f \<circ> f)" |
|
1529 { |
|
1530 fix a b |
|
1531 assume h0: "(a, b) \<in> r" |
|
1532 have "pairself ?f (a, b) = (a, b)" |
|
1533 proof - |
|
1534 from assms h0 have "?f a = a" by (auto intro:inv_into_f_f) |
|
1535 moreover have "?f b = b" |
|
1536 by (insert h0, simp, intro inv_into_f_f[OF assms], auto intro!:RangeI) |
|
1537 ultimately show ?thesis by (auto simp:pairself_def) |
|
1538 qed |
|
1539 } thus ?thesis by (unfold rel_map_def, intro image_id, case_tac x, auto) |
|
1540 qed |
|
1541 |
|
1542 lemma rel_map_acyclic: |
|
1543 assumes "acyclic r" |
|
1544 and "inj_on f ((Domain r) \<union> (Range r))" |
|
1545 shows "acyclic (rel_map f r)" |
|
1546 proof - |
|
1547 let ?D = "Domain r \<union> Range r" |
|
1548 { fix a |
|
1549 assume "(a, a) \<in> (rel_map f r)^+" |
|
1550 from plus_rpath[OF this] |
|
1551 obtain xs where rp: "rpath (rel_map f r) a xs a" "xs \<noteq> []" by auto |
|
1552 from rpath_nnl_lastE[OF this] obtain xs' where eq_xs: "xs = xs'@[a]" by auto |
|
1553 from rpath_edges_on[OF rp(1)] |
|
1554 have h: "edges_on (a # xs) \<subseteq> rel_map f r" . |
|
1555 from edges_on_map[of "inv_into ?D f" "a#xs"] |
|
1556 have "edges_on (map (inv_into ?D f) (a # xs)) = rel_map (inv_into ?D f) (edges_on (a # xs))" . |
|
1557 with rel_map_mono[OF h, of "inv_into ?D f"] |
|
1558 have "edges_on (map (inv_into ?D f) (a # xs)) \<subseteq> rel_map ((inv_into ?D f) o f) r" by simp |
|
1559 from this[unfolded eq_xs] |
|
1560 have subr: "edges_on (map (inv_into ?D f) (a # xs' @ [a])) \<subseteq> rel_map (inv_into ?D f \<circ> f) r" . |
|
1561 have "(map (inv_into ?D f) (a # xs' @ [a])) = (inv_into ?D f a) # map (inv_into ?D f) xs' @ [inv_into ?D f a]" |
|
1562 by simp |
|
1563 from edges_on_rpathI[OF subr[unfolded this]] |
|
1564 have "rpath (rel_map (inv_into ?D f \<circ> f) r) |
|
1565 (inv_into ?D f a) (map (inv_into ?D f) xs' @ [inv_into ?D f a]) (inv_into ?D f a)" . |
|
1566 hence "(inv_into ?D f a, inv_into ?D f a) \<in> (rel_map (inv_into ?D f \<circ> f) r)^+" |
|
1567 by (rule rpath_plus, simp) |
|
1568 moreover have "(rel_map (inv_into ?D f \<circ> f) r) = r" by (rule rel_map_inv_id[OF assms(2)]) |
|
1569 moreover note assms(1) |
|
1570 ultimately have False by (unfold acyclic_def, auto) |
|
1571 } thus ?thesis by (auto simp:acyclic_def) |
|
1572 qed |
|
1573 |
|
1574 lemma relpow_mult: |
|
1575 "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)" |
|
1576 proof(induct n arbitrary:m) |
|
1577 case (Suc k m) |
|
1578 thus ?case |
|
1579 proof - |
|
1580 have h: "(m * k + m) = (m + m * k)" by auto |
|
1581 show ?thesis |
|
1582 apply (simp add:Suc relpow_add[symmetric]) |
|
1583 by (unfold h, simp) |
|
1584 qed |
|
1585 qed simp |
|
1586 |
|
1587 lemma compose_relpow_2: |
|
1588 assumes "r1 \<subseteq> r" |
|
1589 and "r2 \<subseteq> r" |
|
1590 shows "r1 O r2 \<subseteq> r ^^ (2::nat)" |
|
1591 proof - |
|
1592 { fix a b |
|
1593 assume "(a, b) \<in> r1 O r2" |
|
1594 then obtain e where "(a, e) \<in> r1" "(e, b) \<in> r2" |
|
1595 by auto |
|
1596 with assms have "(a, e) \<in> r" "(e, b) \<in> r" by auto |
|
1597 hence "(a, b) \<in> r ^^ (Suc (Suc 0))" by auto |
|
1598 } thus ?thesis by (auto simp:numeral_2_eq_2) |
|
1599 qed |
|
1600 |
|
1601 lemma acyclic_compose: |
|
1602 assumes "acyclic r" |
|
1603 and "r1 \<subseteq> r" |
|
1604 and "r2 \<subseteq> r" |
|
1605 shows "acyclic (r1 O r2)" |
|
1606 proof - |
|
1607 { fix a |
|
1608 assume "(a, a) \<in> (r1 O r2)^+" |
|
1609 from trancl_mono[OF this compose_relpow_2[OF assms(2, 3)]] |
|
1610 have "(a, a) \<in> (r ^^ 2) ^+" . |
|
1611 from trancl_power[THEN iffD1, OF this] |
|
1612 obtain n where h: "(a, a) \<in> (r ^^ 2) ^^ n" "n > 0" by blast |
|
1613 from this(1)[unfolded relpow_mult] have h2: "(a, a) \<in> r ^^ (2 * n)" . |
|
1614 have "(a, a) \<in> r^+" |
|
1615 proof(cases rule:trancl_power[THEN iffD2]) |
|
1616 from h(2) h2 show "\<exists>n>0. (a, a) \<in> r ^^ n" |
|
1617 by (rule_tac x = "2*n" in exI, auto) |
|
1618 qed |
|
1619 with assms have "False" by (auto simp:acyclic_def) |
|
1620 } thus ?thesis by (auto simp:acyclic_def) |
|
1621 qed |
|
1622 |
|
1623 lemma children_compose_unfold: |
|
1624 "children (r1 O r2) x = \<Union> (children r1 ` (children r2 x))" |
|
1625 by (auto simp:children_def) |
|
1626 |
|
1627 lemma fbranch_compose: |
|
1628 assumes "fbranch r1" |
|
1629 and "fbranch r2" |
|
1630 shows "fbranch (r1 O r2)" |
|
1631 proof - |
|
1632 { fix x |
|
1633 assume "x\<in>Range (r1 O r2)" |
|
1634 then obtain y z where h: "(y, z) \<in> r1" "(z, x) \<in> r2" by auto |
|
1635 have "finite (children (r1 O r2) x)" |
|
1636 proof(unfold children_compose_unfold, rule finite_Union) |
|
1637 show "finite (children r1 ` children r2 x)" |
|
1638 proof(rule finite_imageI) |
|
1639 from h(2) have "x \<in> Range r2" by auto |
|
1640 from assms(2)[unfolded fbranch_def, rule_format, OF this] |
|
1641 show "finite (children r2 x)" . |
|
1642 qed |
|
1643 next |
|
1644 fix M |
|
1645 assume "M \<in> children r1 ` children r2 x" |
|
1646 then obtain y where h1: "y \<in> children r2 x" "M = children r1 y" by auto |
|
1647 show "finite M" |
|
1648 proof(cases "children r1 y = {}") |
|
1649 case True |
|
1650 with h1(2) show ?thesis by auto |
|
1651 next |
|
1652 case False |
|
1653 hence "y \<in> Range r1" by (unfold children_def, auto) |
|
1654 from assms(1)[unfolded fbranch_def, rule_format, OF this, folded h1(2)] |
|
1655 show ?thesis . |
|
1656 qed |
|
1657 qed |
|
1658 } thus ?thesis by (unfold fbranch_def, auto) |
|
1659 qed |
|
1660 |
|
1661 lemma finite_fbranchI: |
|
1662 assumes "finite r" |
|
1663 shows "fbranch r" |
|
1664 proof - |
|
1665 { fix x |
|
1666 assume "x \<in>Range r" |
|
1667 have "finite (children r x)" |
|
1668 proof - |
|
1669 have "{y. (y, x) \<in> r} \<subseteq> Domain r" by (auto) |
|
1670 from rev_finite_subset[OF finite_Domain[OF assms] this] |
|
1671 have "finite {y. (y, x) \<in> r}" . |
|
1672 thus ?thesis by (unfold children_def, simp) |
|
1673 qed |
|
1674 } thus ?thesis by (auto simp:fbranch_def) |
|
1675 qed |
|
1676 |
|
1677 lemma subset_fbranchI: |
|
1678 assumes "fbranch r1" |
|
1679 and "r2 \<subseteq> r1" |
|
1680 shows "fbranch r2" |
|
1681 proof - |
|
1682 { fix x |
|
1683 assume "x \<in>Range r2" |
|
1684 with assms(2) have "x \<in> Range r1" by auto |
|
1685 from assms(1)[unfolded fbranch_def, rule_format, OF this] |
|
1686 have "finite (children r1 x)" . |
|
1687 hence "finite (children r2 x)" |
|
1688 proof(rule rev_finite_subset) |
|
1689 from assms(2) |
|
1690 show "children r2 x \<subseteq> children r1 x" by (auto simp:children_def) |
|
1691 qed |
|
1692 } thus ?thesis by (auto simp:fbranch_def) |
|
1693 qed |
|
1694 |
|
1695 lemma children_subtree: |
|
1696 shows "children r x \<subseteq> subtree r x" |
|
1697 by (auto simp:children_def subtree_def) |
|
1698 |
|
1699 lemma children_union_kept: |
|
1700 assumes "x \<notin> Range r'" |
|
1701 shows "children (r \<union> r') x = children r x" |
|
1702 using assms |
|
1703 by (auto simp:children_def) |
|
1704 |
958 end |
1705 end |