equal
deleted
inserted
replaced
19 A `Relation Graph` @{text "r"} is said to be a `Relational Tree` if it is both |
19 A `Relation Graph` @{text "r"} is said to be a `Relational Tree` if it is both |
20 {\em single valued} and {\em acyclic}. |
20 {\em single valued} and {\em acyclic}. |
21 *} |
21 *} |
22 |
22 |
23 |
23 |
24 locale rtree = |
24 locale forest = |
25 fixes r |
25 fixes r |
26 assumes sgv: "single_valued r" |
26 assumes sgv: "single_valued r" |
27 assumes acl: "acyclic r" |
27 assumes acl: "acyclic r" |
28 |
28 |
29 text {* |
29 text {* |
108 shows "(a, b) \<notin> edges_in r x" |
108 shows "(a, b) \<notin> edges_in r x" |
109 using assms by (unfold edges_in_def subtree_def, auto) |
109 using assms by (unfold edges_in_def subtree_def, auto) |
110 |
110 |
111 definition "children r x = {y. (y, x) \<in> r}" |
111 definition "children r x = {y. (y, x) \<in> r}" |
112 |
112 |
113 locale fgraph = rtree + |
113 locale fforest = forest + |
114 assumes fb: "finite (children r x)" |
114 assumes fb: "finite (children r x)" |
115 assumes wf: "wf r" |
115 assumes wf: "wf r" |
116 begin |
116 begin |
117 |
117 |
118 lemma finite_children: "finite (children r x)" |
118 lemma finite_children: "finite (children r x)" |
719 by(elim subtreeE, insert assms, auto) |
719 by(elim subtreeE, insert assms, auto) |
720 qed |
720 qed |
721 |
721 |
722 subsubsection {* Properties about relational trees *} |
722 subsubsection {* Properties about relational trees *} |
723 |
723 |
724 context rtree |
724 context forest |
725 begin |
725 begin |
726 |
726 |
727 lemma ancestors_headE: |
727 lemma ancestors_headE: |
728 assumes "c \<in> ancestors r a" |
728 assumes "c \<in> ancestors r a" |
729 assumes "(a, b) \<in> r" |
729 assumes "(a, b) \<in> r" |
1348 by (auto simp:children_def) |
1348 by (auto simp:children_def) |
1349 ultimately show ?thesis by (intro that, auto) |
1349 ultimately show ?thesis by (intro that, auto) |
1350 qed |
1350 qed |
1351 qed |
1351 qed |
1352 |
1352 |
1353 end (* of rtree *) |
1353 end (* of forest *) |
1354 |
1354 |
1355 lemma subtree_trancl: |
1355 lemma subtree_trancl: |
1356 "subtree r x = {x} \<union> {y. (y, x) \<in> r^+}" (is "?L = ?R") |
1356 "subtree r x = {x} \<union> {y. (y, x) \<in> r^+}" (is "?L = ?R") |
1357 proof - |
1357 proof - |
1358 { fix z |
1358 { fix z |
1383 |
1383 |
1384 lemma subtree_children: |
1384 lemma subtree_children: |
1385 "subtree r x = ({x} \<union> (\<Union> (subtree r ` (children r x))))" (is "?L = ?R") |
1385 "subtree r x = ({x} \<union> (\<Union> (subtree r ` (children r x))))" (is "?L = ?R") |
1386 by fast |
1386 by fast |
1387 |
1387 |
1388 context fgraph |
1388 context fforest |
1389 begin |
1389 begin |
1390 |
1390 |
1391 lemma finite_subtree: |
1391 lemma finite_subtree: |
1392 shows "finite (subtree r x)" |
1392 shows "finite (subtree r x)" |
1393 proof(induct rule:wf_induct[OF wf]) |
1393 proof(induct rule:wf_induct[OF wf]) |
1555 moreover note assms(1) |
1555 moreover note assms(1) |
1556 ultimately have False by (unfold acyclic_def, auto) |
1556 ultimately have False by (unfold acyclic_def, auto) |
1557 } thus ?thesis by (auto simp:acyclic_def) |
1557 } thus ?thesis by (auto simp:acyclic_def) |
1558 qed |
1558 qed |
1559 |
1559 |
|
1560 lemma compose_relpow_2 [intro, simp]: |
|
1561 assumes "r1 \<subseteq> r" |
|
1562 and "r2 \<subseteq> r" |
|
1563 shows "r1 O r2 \<subseteq> r ^^ (2::nat)" |
|
1564 proof - |
|
1565 { fix a b |
|
1566 assume "(a, b) \<in> r1 O r2" |
|
1567 then obtain e where "(a, e) \<in> r1" "(e, b) \<in> r2" |
|
1568 by auto |
|
1569 with assms have "(a, e) \<in> r" "(e, b) \<in> r" by auto |
|
1570 hence "(a, b) \<in> r ^^ (Suc (Suc 0))" by auto |
|
1571 } thus ?thesis by (auto simp:numeral_2_eq_2) |
|
1572 qed |
|
1573 |
1560 lemma relpow_mult: |
1574 lemma relpow_mult: |
1561 "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)" |
1575 "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)" |
1562 proof(induct n arbitrary:m) |
1576 proof(induct n arbitrary:m) |
1563 case (Suc k m) |
1577 case (Suc k m) |
1564 thus ?case |
1578 thus ?case |
1567 show ?thesis |
1581 show ?thesis |
1568 apply (simp add:Suc relpow_add[symmetric]) |
1582 apply (simp add:Suc relpow_add[symmetric]) |
1569 by (unfold h, simp) |
1583 by (unfold h, simp) |
1570 qed |
1584 qed |
1571 qed simp |
1585 qed simp |
1572 |
|
1573 lemma compose_relpow_2 [intro, simp]: |
|
1574 assumes "r1 \<subseteq> r" |
|
1575 and "r2 \<subseteq> r" |
|
1576 shows "r1 O r2 \<subseteq> r ^^ (2::nat)" |
|
1577 proof - |
|
1578 { fix a b |
|
1579 assume "(a, b) \<in> r1 O r2" |
|
1580 then obtain e where "(a, e) \<in> r1" "(e, b) \<in> r2" |
|
1581 by auto |
|
1582 with assms have "(a, e) \<in> r" "(e, b) \<in> r" by auto |
|
1583 hence "(a, b) \<in> r ^^ (Suc (Suc 0))" by auto |
|
1584 } thus ?thesis by (auto simp:numeral_2_eq_2) |
|
1585 qed |
|
1586 |
1586 |
1587 lemma acyclic_compose [intro, simp]: |
1587 lemma acyclic_compose [intro, simp]: |
1588 assumes "acyclic r" |
1588 assumes "acyclic r" |
1589 and "r1 \<subseteq> r" |
1589 and "r1 \<subseteq> r" |
1590 and "r2 \<subseteq> r" |
1590 and "r2 \<subseteq> r" |
1621 have "finite (children (r1 O r2) x)" |
1621 have "finite (children (r1 O r2) x)" |
1622 proof(unfold children_compose_unfold, rule finite_Union) |
1622 proof(unfold children_compose_unfold, rule finite_Union) |
1623 show "finite (children r1 ` children r2 x)" |
1623 show "finite (children r1 ` children r2 x)" |
1624 proof(rule finite_imageI) |
1624 proof(rule finite_imageI) |
1625 from h(2) have "x \<in> Range r2" by auto |
1625 from h(2) have "x \<in> Range r2" by auto |
1626 from assms(2)[unfolded fgraph_def] this |
1626 from assms(2)[unfolded fforest_def] this |
1627 show "finite (children r2 x)" by auto |
1627 show "finite (children r2 x)" by auto |
1628 qed |
1628 qed |
1629 next |
1629 next |
1630 fix M |
1630 fix M |
1631 assume "M \<in> children r1 ` children r2 x" |
1631 assume "M \<in> children r1 ` children r2 x" |
1635 case True |
1635 case True |
1636 with h1(2) show ?thesis by auto |
1636 with h1(2) show ?thesis by auto |
1637 next |
1637 next |
1638 case False |
1638 case False |
1639 hence "y \<in> Range r1" by (unfold children_def, auto) |
1639 hence "y \<in> Range r1" by (unfold children_def, auto) |
1640 from assms(1)[unfolded fgraph_def] this h1(2) |
1640 from assms(1)[unfolded fforest_def] this h1(2) |
1641 show ?thesis by auto |
1641 show ?thesis by auto |
1642 qed |
1642 qed |
1643 qed |
1643 qed |
1644 } thus ?thesis using assms by auto |
1644 } thus ?thesis using assms by auto |
1645 qed |
1645 qed |