equal
deleted
inserted
replaced
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 = {y . (y, x) \<in> r^*}" |
77 |
77 |
78 definition "ancestors r x = {y. (x, y) \<in> r^+}" |
78 definition "ancestors r x = {y. (x, y) \<in> r^+}" |
|
79 |
|
80 (* tmp *) |
|
81 definition |
|
82 "nancestors r x \<equiv> ancestors r x \<union> {x}" |
|
83 |
|
84 lemma nancestors_def2: |
|
85 "nancestors r x \<equiv> {y. (x, y) \<in> r\<^sup>*}" |
|
86 unfolding nancestors_def |
|
87 apply(auto) |
|
88 by (smt Collect_cong ancestors_def insert_compr mem_Collect_eq rtrancl_eq_or_trancl) |
|
89 |
|
90 lemma nancestors2: |
|
91 "y \<in> ancestors r x \<Longrightarrow> y \<in> nancestors r x" |
|
92 apply(auto simp add: nancestors_def) |
|
93 done |
|
94 |
|
95 lemma nancestors3: |
|
96 "\<lbrakk>y \<in> nancestors r x; x \<noteq> y\<rbrakk> \<Longrightarrow> y \<in> ancestors r x" |
|
97 apply(auto simp add: nancestors_def) |
|
98 done |
|
99 (* end tmp *) |
79 |
100 |
80 definition "root r x = (ancestors r x = {})" |
101 definition "root r x = (ancestors r x = {})" |
81 |
102 |
82 lemma root_indep: |
103 lemma root_indep: |
83 assumes "root r x" |
104 assumes "root r x" |