RTree.thy
changeset 138 20c1d3a14143
parent 137 785c0f6b8184
child 178 da27bece9575
equal deleted inserted replaced
137:785c0f6b8184 138:20c1d3a14143
    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"