equal
deleted
inserted
replaced
126 definition "children r x = {y. (y, x) \<in> r}" |
126 definition "children r x = {y. (y, x) \<in> r}" |
127 |
127 |
128 locale fbranch = |
128 locale fbranch = |
129 fixes r |
129 fixes r |
130 assumes fb: "\<forall> x \<in> Range r . finite (children r x)" |
130 assumes fb: "\<forall> x \<in> Range r . finite (children r x)" |
|
131 begin |
|
132 |
|
133 lemma finite_children: "finite (children r x)" |
|
134 proof(cases "children r x = {}") |
|
135 case True |
|
136 thus ?thesis by auto |
|
137 next |
|
138 case False |
|
139 then obtain y where "(y, x) \<in> r" by (auto simp:children_def) |
|
140 hence "x \<in> Range r" by auto |
|
141 from fb[rule_format, OF this] |
|
142 show ?thesis . |
|
143 qed |
|
144 |
|
145 end |
131 |
146 |
132 locale fsubtree = fbranch + |
147 locale fsubtree = fbranch + |
133 assumes wf: "wf r" |
148 assumes wf: "wf r" |
134 |
149 |
135 (* ccc *) |
150 (* ccc *) |