71 In relational tree @{text "r"}, the sub tree of node @{text "x"} is |
71 In relational tree @{text "r"}, the sub tree of node @{text "x"} is |
72 written @{text "subtree r x"}, which is defined to be the set of |
72 written @{text "subtree r x"}, which is defined to be the set of |
73 nodes (including itself) which can reach @{text "x"} by following |
73 nodes (including itself) which can reach @{text "x"} by following |
74 some path in @{text "r"}: *} |
74 some path in @{text "r"}: *} |
75 |
75 |
76 definition "subtree r x = {node' . (node', x) \<in> r^*}" |
76 definition "subtree r x = {y . (y, x) \<in> r^*}" |
77 |
77 |
78 definition "ancestors r x = {node'. (x, node') \<in> r^+}" |
78 definition "ancestors r x = {y. (x, y) \<in> r^+}" |
79 |
79 |
80 definition "root r x = (ancestors r x = {})" |
80 definition "root r x = (ancestors r x = {})" |
|
81 |
|
82 lemma root_indep: |
|
83 assumes "root r x" |
|
84 and "root r y" |
|
85 and "y \<noteq> x" |
|
86 shows "indep r x y" |
|
87 proof - |
|
88 { assume "(x, y) \<in> r^*" |
|
89 hence False using assms |
|
90 by (unfold root_def ancestors_def, auto dest:tranclD rtranclD) |
|
91 } moreover { |
|
92 assume "(y, x) \<in> r^*" |
|
93 hence False using assms |
|
94 by (unfold root_def ancestors_def, auto dest:tranclD rtranclD) |
|
95 } ultimately show ?thesis by (auto simp:indep_def) |
|
96 qed |
81 |
97 |
82 text {* |
98 text {* |
83 |
99 |
84 The following @{text "edge_in r x"} is the set of edges contained in |
100 The following @{text "edge_in r x"} is the set of edges contained in |
85 the sub-tree of @{text "x"}, with @{text "r"} as the underlying |
101 the sub-tree of @{text "x"}, with @{text "r"} as the underlying |
106 lemma edges_in_refutation: |
122 lemma edges_in_refutation: |
107 assumes "b \<notin> subtree r x" |
123 assumes "b \<notin> subtree r x" |
108 shows "(a, b) \<notin> edges_in r x" |
124 shows "(a, b) \<notin> edges_in r x" |
109 using assms by (unfold edges_in_def subtree_def, auto) |
125 using assms by (unfold edges_in_def subtree_def, auto) |
110 |
126 |
111 definition "children r x = {node'. (node', x) \<in> r}" |
127 definition "children r x = {y. (y, x) \<in> r}" |
112 |
128 |
113 locale fforest = forest + |
129 locale fforest = forest + |
114 assumes fb: "finite (children r x)" |
130 assumes fb: "finite (children r x)" |
115 assumes wf: "wf r" |
131 assumes wf: "wf r" |
116 begin |
132 begin |
1062 then obtain xs2 where rp2: "rpath r z xs2 y" using star_rpath by metis |
1078 then obtain xs2 where rp2: "rpath r z xs2 y" using star_rpath by metis |
1063 from rp1 rp2 |
1079 from rp1 rp2 |
1064 have False |
1080 have False |
1065 by (cases, insert my_rule[OF sym_indep[OF assms(1)] rp2 rp1] |
1081 by (cases, insert my_rule[OF sym_indep[OF assms(1)] rp2 rp1] |
1066 my_rule[OF assms(1) rp1 rp2], auto) |
1082 my_rule[OF assms(1) rp1 rp2], auto) |
|
1083 } thus ?thesis by auto |
|
1084 qed |
|
1085 |
|
1086 lemma root_unique: |
|
1087 assumes "x \<in> subtree r y" |
|
1088 and "x \<in> subtree r z" |
|
1089 and "root r y" |
|
1090 and "root r z" |
|
1091 shows "y = z" |
|
1092 proof - |
|
1093 { assume "y \<noteq> z" |
|
1094 from root_indep[OF assms(4,3) this] |
|
1095 have "indep r z y" . |
|
1096 from subtree_disjoint[OF this] and assms |
|
1097 have False by auto |
1067 } thus ?thesis by auto |
1098 } thus ?thesis by auto |
1068 qed |
1099 qed |
1069 |
1100 |
1070 text {* |
1101 text {* |
1071 The following lemma @{text "subtree_del"} characterizes the change of sub-tree of |
1102 The following lemma @{text "subtree_del"} characterizes the change of sub-tree of |