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 fbranch = |
113 locale fgraph = |
114 fixes r |
114 fixes r |
115 assumes fb: "\<forall> x \<in> Range r . finite (children r x)" |
115 assumes fb: "\<forall> x \<in> Range r . finite (children r x)" |
|
116 assumes wf: "wf r" |
116 begin |
117 begin |
117 |
118 |
118 lemma finite_children: "finite (children r x)" |
119 lemma finite_children: "finite (children r x)" |
119 using fb by (cases "children r x = {}", auto simp:children_def) |
120 using fb by (cases "children r x = {}", auto simp:children_def) |
120 |
121 |
121 end |
122 end |
122 |
123 |
123 locale fsubtree = fbranch + |
|
124 assumes wf: "wf r" |
|
125 |
124 |
126 subsection {* Auxiliary lemmas *} |
125 subsection {* Auxiliary lemmas *} |
127 |
126 |
128 lemma index_minimize: |
127 lemma index_minimize: |
129 assumes "P (i::nat)" |
128 assumes "P (i::nat)" |
1611 lemma children_compose_unfold: |
1610 lemma children_compose_unfold: |
1612 "children (r1 O r2) x = \<Union> (children r1 ` (children r2 x))" |
1611 "children (r1 O r2) x = \<Union> (children r1 ` (children r2 x))" |
1613 by (auto simp:children_def) |
1612 by (auto simp:children_def) |
1614 |
1613 |
1615 lemma fbranch_compose [intro, simp]: |
1614 lemma fbranch_compose [intro, simp]: |
1616 assumes "fbranch r1" |
1615 assumes "\<forall> x \<in> Range r1 . finite (children r1 x)" |
1617 and "fbranch r2" |
1616 and "\<forall> x \<in> Range r2 . finite (children r2 x)" |
1618 shows "fbranch (r1 O r2)" |
1617 shows "\<forall> x \<in> Range (r1 O r2) . finite (children (r1 O r2) x)" |
1619 proof - |
1618 proof - |
1620 { fix x |
1619 { fix x |
1621 assume "x\<in>Range (r1 O r2)" |
1620 assume "x\<in>Range (r1 O r2)" |
1622 then obtain y z where h: "(y, z) \<in> r1" "(z, x) \<in> r2" by auto |
1621 then obtain y z where h: "(y, z) \<in> r1" "(z, x) \<in> r2" by auto |
1623 have "finite (children (r1 O r2) x)" |
1622 have "finite (children (r1 O r2) x)" |
1624 proof(unfold children_compose_unfold, rule finite_Union) |
1623 proof(unfold children_compose_unfold, rule finite_Union) |
1625 show "finite (children r1 ` children r2 x)" |
1624 show "finite (children r1 ` children r2 x)" |
1626 proof(rule finite_imageI) |
1625 proof(rule finite_imageI) |
1627 from h(2) have "x \<in> Range r2" by auto |
1626 from h(2) have "x \<in> Range r2" by auto |
1628 from assms(2)[unfolded fbranch_def, rule_format, OF this] |
1627 from assms(2)[unfolded fgraph_def] this |
1629 show "finite (children r2 x)" . |
1628 show "finite (children r2 x)" by auto |
1630 qed |
1629 qed |
1631 next |
1630 next |
1632 fix M |
1631 fix M |
1633 assume "M \<in> children r1 ` children r2 x" |
1632 assume "M \<in> children r1 ` children r2 x" |
1634 then obtain y where h1: "y \<in> children r2 x" "M = children r1 y" by auto |
1633 then obtain y where h1: "y \<in> children r2 x" "M = children r1 y" by auto |
1637 case True |
1636 case True |
1638 with h1(2) show ?thesis by auto |
1637 with h1(2) show ?thesis by auto |
1639 next |
1638 next |
1640 case False |
1639 case False |
1641 hence "y \<in> Range r1" by (unfold children_def, auto) |
1640 hence "y \<in> Range r1" by (unfold children_def, auto) |
1642 from assms(1)[unfolded fbranch_def, rule_format, OF this, folded h1(2)] |
1641 from assms(1)[unfolded fgraph_def] this h1(2) |
1643 show ?thesis . |
1642 show ?thesis by auto |
1644 qed |
1643 qed |
1645 qed |
1644 qed |
1646 } thus ?thesis by (unfold fbranch_def, auto) |
1645 } thus ?thesis using assms by auto |
1647 qed |
1646 qed |
1648 |
1647 |
1649 lemma finite_fbranchI [intro]: |
1648 lemma finite_fbranchI [intro]: |
1650 assumes "finite r" |
1649 assumes "finite r" |
1651 shows "fbranch r" |
1650 shows "\<forall> x \<in> Range r . finite (children r x)" |
1652 proof - |
1651 proof - |
1653 { fix x |
1652 { fix x |
1654 assume "x \<in>Range r" |
1653 assume "x \<in>Range r" |
1655 have "finite (children r x)" |
1654 have "finite (children r x)" |
1656 proof - |
1655 proof - |
1657 have "{y. (y, x) \<in> r} \<subseteq> Domain r" by (auto) |
1656 have "{y. (y, x) \<in> r} \<subseteq> Domain r" by (auto) |
1658 from rev_finite_subset[OF finite_Domain[OF assms] this] |
1657 from rev_finite_subset[OF finite_Domain[OF assms] this] |
1659 have "finite {y. (y, x) \<in> r}" . |
1658 have "finite {y. (y, x) \<in> r}" . |
1660 thus ?thesis by (unfold children_def, simp) |
1659 thus ?thesis by (unfold children_def, simp) |
1661 qed |
1660 qed |
1662 } thus ?thesis by (auto simp:fbranch_def) |
1661 } thus ?thesis by auto |
1663 qed |
1662 qed |
1664 |
1663 |
1665 lemma subset_fbranchI [intro]: |
1664 lemma subset_fbranchI [intro]: |
1666 assumes "fbranch r1" |
1665 assumes "\<forall> x \<in> Range r1 . finite (children r1 x)" |
1667 and "r2 \<subseteq> r1" |
1666 and "r2 \<subseteq> r1" |
1668 shows "fbranch r2" |
1667 shows "\<forall> x \<in> Range r2 . finite (children r2 x)" |
1669 proof - |
1668 proof - |
1670 { fix x |
1669 { fix x |
1671 assume "x \<in>Range r2" |
1670 assume "x \<in>Range r2" |
1672 with assms(2) have "x \<in> Range r1" by auto |
1671 with assms(2) have "x \<in> Range r1" by auto |
1673 from assms(1)[unfolded fbranch_def, rule_format, OF this] |
1672 from assms(1)[rule_format, OF this] |
1674 have "finite (children r1 x)" . |
1673 have "finite (children r1 x)" . |
1675 hence "finite (children r2 x)" |
1674 hence "finite (children r2 x)" |
1676 proof(rule rev_finite_subset) |
1675 proof(rule rev_finite_subset) |
1677 from assms(2) |
1676 from assms(2) |
1678 show "children r2 x \<subseteq> children r1 x" by (auto simp:children_def) |
1677 show "children r2 x \<subseteq> children r1 x" by (auto simp:children_def) |
1679 qed |
1678 qed |
1680 } thus ?thesis by (auto simp:fbranch_def) |
1679 } thus ?thesis by auto |
1681 qed |
1680 qed |
1682 |
1681 |
1683 lemma children_subtree [simp, intro]: |
1682 lemma children_subtree [simp, intro]: |
1684 shows "children r x \<subseteq> subtree r x" |
1683 shows "children r x \<subseteq> subtree r x" |
1685 by (auto simp:children_def subtree_def) |
1684 by (auto simp:children_def subtree_def) |