equal
deleted
inserted
replaced
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 = {y . (y, x) \<in> r^*}" |
76 definition "subtree r x = {node' . (node', x) \<in> r^*}" |
77 |
77 |
78 definition "ancestors r x = {y. (x, y) \<in> r^+}" |
78 definition "ancestors r x = {node'. (x, node') \<in> r^+}" |
79 |
79 |
80 definition "root r x = (ancestors r x = {})" |
80 definition "root r x = (ancestors r x = {})" |
81 |
81 |
82 text {* |
82 text {* |
83 |
83 |
106 lemma edges_in_refutation: |
106 lemma edges_in_refutation: |
107 assumes "b \<notin> subtree r x" |
107 assumes "b \<notin> subtree r x" |
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 = {node'. (node', x) \<in> r}" |
112 |
112 |
113 locale fforest = forest + |
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 |