equal
deleted
inserted
replaced
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 = |
113 locale fgraph = rtree + |
114 fixes r |
114 assumes fb: "finite (children r x)" |
115 assumes fb: "\<forall> x \<in> Range r . finite (children r x)" |
|
116 assumes wf: "wf r" |
115 assumes wf: "wf r" |
117 begin |
116 begin |
118 |
117 |
119 lemma finite_children: "finite (children r x)" |
118 lemma finite_children: "finite (children r x)" |
120 using fb by (cases "children r x = {}", auto simp:children_def) |
119 using fb by (cases "children r x = {}", auto simp:children_def) |
1400 case True |
1399 case True |
1401 thus ?thesis by auto |
1400 thus ?thesis by auto |
1402 next |
1401 next |
1403 case False |
1402 case False |
1404 hence "x \<in> Range r" by (auto simp:children_def) |
1403 hence "x \<in> Range r" by (auto simp:children_def) |
1405 from fb[rule_format, OF this] |
1404 from fb |
1406 have "finite (children r x)" . |
1405 have "finite (children r x)" . |
1407 thus ?thesis by (rule finite_imageI) |
1406 thus ?thesis by (rule finite_imageI) |
1408 qed |
1407 qed |
1409 next |
1408 next |
1410 fix M |
1409 fix M |
1643 qed |
1642 qed |
1644 qed |
1643 qed |
1645 } thus ?thesis using assms by auto |
1644 } thus ?thesis using assms by auto |
1646 qed |
1645 qed |
1647 |
1646 |
|
1647 lemma fbranch_compose1 [intro, simp]: |
|
1648 assumes "\<forall>x. finite (children r1 x)" |
|
1649 and "\<forall>x. finite (children r2 x)" |
|
1650 shows "\<forall>x. finite (children (r1 O r2) x)" |
|
1651 by (metis (no_types, lifting) Collect_empty_eq Range.intros assms(1) |
|
1652 assms(2) children_def fbranch_compose finite.emptyI) |
|
1653 |
|
1654 |
1648 lemma finite_fbranchI [intro]: |
1655 lemma finite_fbranchI [intro]: |
1649 assumes "finite r" |
1656 assumes "finite r" |
1650 shows "\<forall> x \<in> Range r . finite (children r x)" |
1657 shows "\<forall> x \<in> Range r . finite (children r x)" |
1651 proof - |
1658 proof - |
1652 { fix x |
1659 { fix x |
1658 have "finite {y. (y, x) \<in> r}" . |
1665 have "finite {y. (y, x) \<in> r}" . |
1659 thus ?thesis by (unfold children_def, simp) |
1666 thus ?thesis by (unfold children_def, simp) |
1660 qed |
1667 qed |
1661 } thus ?thesis by auto |
1668 } thus ?thesis by auto |
1662 qed |
1669 qed |
|
1670 |
|
1671 lemma finite_fbranchI1 [intro]: |
|
1672 assumes "finite r" |
|
1673 shows "\<forall> x . finite (children r x)" |
|
1674 by (metis (no_types, lifting) Collect_empty_eq Range.intros assms |
|
1675 children_def finite.emptyI finite_fbranchI) |
1663 |
1676 |
1664 lemma subset_fbranchI [intro]: |
1677 lemma subset_fbranchI [intro]: |
1665 assumes "\<forall> x \<in> Range r1 . finite (children r1 x)" |
1678 assumes "\<forall> x \<in> Range r1 . finite (children r1 x)" |
1666 and "r2 \<subseteq> r1" |
1679 and "r2 \<subseteq> r1" |
1667 shows "\<forall> x \<in> Range r2 . finite (children r2 x)" |
1680 shows "\<forall> x \<in> Range r2 . finite (children r2 x)" |