RTree.thy
changeset 58 ad57323fd4d6
parent 57 f1b39d77db00
child 60 f98a95f3deae
equal deleted inserted replaced
57:f1b39d77db00 58:ad57323fd4d6
     1 theory RTree
     1 theory RTree
     2 imports "~~/src/HOL/Library/Transitive_Closure_Table"
     2 imports "~~/src/HOL/Library/Transitive_Closure_Table" Max
     3 begin
     3 begin
     4 
     4 
     5 section {* A theory of relational trees *}
     5 section {* A theory of relational trees *}
     6 
     6 
     7 inductive_cases path_nilE [elim!]: "rtrancl_path r x [] y"
     7 inductive_cases path_nilE [elim!]: "rtrancl_path r x [] y"
     8 inductive_cases path_consE [elim!]: "rtrancl_path r x (z#zs) y"
     8 inductive_cases path_consE [elim!]: "rtrancl_path r x (z#zs) y"
     9 
     9 
    10 subsection {* Definitions *}
    10 subsection {* Definitions *}
    11 
    11 
    12 text {*
    12 text {*
    13   In this theory, we are giving to give a notion of of `Relational Graph` and
    13   In this theory, we are going to give a notion of of `Relational Graph` and
    14   its derived notion `Relational Tree`. Given a binary relation @{text "r"},
    14   its derived notion `Relational Tree`. Given a binary relation @{text "r"},
    15   the `Relational Graph of @{text "r"}` is the graph, the edges of which
    15   the `Relational Graph of @{text "r"}` is the graph, the edges of which
    16   are those in @{text "r"}. In this way, any binary relation can be viewed
    16   are those in @{text "r"}. In this way, any binary relation can be viewed
    17   as a `Relational Graph`. Note, this notion of graph includes infinite graphs. 
    17   as a `Relational Graph`. Note, this notion of graph includes infinite graphs. 
    18 
    18 
    78   @{text "subtree r x"}, which is defined to be the set of nodes (including itself) 
    78   @{text "subtree r x"}, which is defined to be the set of nodes (including itself) 
    79   which can reach @{text "x"} by following some path in @{text "r"}:
    79   which can reach @{text "x"} by following some path in @{text "r"}:
    80 *}
    80 *}
    81 
    81 
    82 definition "subtree r x = {y . (y, x) \<in> r^*}"
    82 definition "subtree r x = {y . (y, x) \<in> r^*}"
       
    83 
       
    84 definition "ancestors r x = {y. (x, y) \<in> r^+}"
       
    85 
       
    86 definition "root r x = (ancestors r x = {})"
    83 
    87 
    84 text {*
    88 text {*
    85   The following @{text "edge_in r x"} is the set of edges
    89   The following @{text "edge_in r x"} is the set of edges
    86   contained in the sub-tree of @{text "x"}, with @{text "r"} as the underlying graph.
    90   contained in the sub-tree of @{text "x"}, with @{text "r"} as the underlying graph.
    87 *}
    91 *}
   108       by (auto)
   112       by (auto)
   109   } thus ?thesis by (auto simp:edges_in_def)
   113   } thus ?thesis by (auto simp:edges_in_def)
   110 qed
   114 qed
   111 
   115 
   112 text {*
   116 text {*
   113   The following lemma shows the means of @{term "edges_in"} from the other side, 
   117   The following lemma shows the meaning of @{term "edges_in"} from the other side, 
   114   which says to for the edge @{text "(a,b)"} to be outside of the sub-tree of @{text "x"}, 
   118   which says: for the edge @{text "(a,b)"} to be outside of the sub-tree of @{text "x"}, 
   115   it is sufficient if @{text "b"} is.
   119   it is sufficient to show that @{text "b"} is.
   116 *}
   120 *}
   117 lemma edges_in_refutation:
   121 lemma edges_in_refutation:
   118   assumes "b \<notin> subtree r x"
   122   assumes "b \<notin> subtree r x"
   119   shows "(a, b) \<notin> edges_in r x"
   123   shows "(a, b) \<notin> edges_in r x"
   120   using assms by (unfold edges_in_def subtree_def, auto)
   124   using assms by (unfold edges_in_def subtree_def, auto)
       
   125 
       
   126 definition "children r x = {y. (y, x) \<in> r}"
       
   127 
       
   128 locale fbranch =
       
   129   fixes r
       
   130   assumes fb: "\<forall> x \<in> Range r . finite (children r x)"
       
   131 
       
   132 locale fsubtree = fbranch + 
       
   133    assumes wf: "wf r"
       
   134 
       
   135 (* ccc *)
   121 
   136 
   122 subsection {* Auxiliary lemmas *}
   137 subsection {* Auxiliary lemmas *}
   123 
   138 
   124 lemma index_minimize:
   139 lemma index_minimize:
   125   assumes "P (i::nat)"
   140   assumes "P (i::nat)"
   169 
   184 
   170 subsubsection {* Properties of @{text "rpath"} *}
   185 subsubsection {* Properties of @{text "rpath"} *}
   171 
   186 
   172 text {* Induction rule for @{text "rpath"}: *}
   187 text {* Induction rule for @{text "rpath"}: *}
   173 
   188 
   174 print_statement rtrancl_path.induct
       
   175 
       
   176 lemma rpath_induct [consumes 1, case_names rbase rstep, induct pred: rpath]:
   189 lemma rpath_induct [consumes 1, case_names rbase rstep, induct pred: rpath]:
   177   assumes "rpath r x1 x2 x3"
   190   assumes "rpath r x1 x2 x3"
   178     and "\<And>x. P x [] x"
   191     and "\<And>x. P x [] x"
   179     and "\<And>x y ys z. (x, y) \<in> r \<Longrightarrow> rpath r y ys z \<Longrightarrow> P y ys z \<Longrightarrow> P x (y # ys) z"
   192     and "\<And>x y ys z. (x, y) \<in> r \<Longrightarrow> rpath r y ys z \<Longrightarrow> P y ys z \<Longrightarrow> P x (y # ys) z"
   180   shows "P x1 x2 x3"
   193   shows "P x1 x2 x3"
   181   using assms[unfolded rpath_def]
   194   using assms[unfolded rpath_def]
   182   by (induct, auto simp:pred_of_def rpath_def)
   195   by (induct, auto simp:pred_of_def rpath_def)
       
   196 
       
   197 lemma rpathE: 
       
   198   assumes "rpath r x xs y"
       
   199   obtains (base) "y = x" "xs = []"
       
   200      | (step) z zs where "(x, z) \<in> r" "rpath r z zs y" "xs = z#zs"
       
   201   using assms
       
   202   by (induct, auto)
   183 
   203 
   184 text {* Introduction rule for empty path *}
   204 text {* Introduction rule for empty path *}
   185 lemma rbaseI [intro!]: 
   205 lemma rbaseI [intro!]: 
   186   assumes "x = y"
   206   assumes "x = y"
   187   shows "rpath r x [] y"
   207   shows "rpath r x [] y"
   280   using assms
   300   using assms
   281   by (induct, auto)
   301   by (induct, auto)
   282 
   302 
   283 subsubsection {* Properites of @{text "edges_on"} *}
   303 subsubsection {* Properites of @{text "edges_on"} *}
   284 
   304 
       
   305 lemma edges_on_unfold:
       
   306   "edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R")
       
   307 proof -
       
   308   { fix c d
       
   309     assume "(c, d) \<in> ?L"
       
   310     then obtain l1 l2 where h: "(a # b # xs) = l1 @ [c, d] @ l2" 
       
   311         by (auto simp:edges_on_def)
       
   312     have "(c, d) \<in> ?R"
       
   313     proof(cases "l1")
       
   314       case Nil
       
   315       with h have "(c, d) = (a, b)" by auto
       
   316       thus ?thesis by auto
       
   317     next
       
   318       case (Cons e es)
       
   319       from h[unfolded this] have "b#xs = es@[c, d]@l2" by auto
       
   320       thus ?thesis by (auto simp:edges_on_def)
       
   321     qed
       
   322   } moreover
       
   323   { fix c d
       
   324     assume "(c, d) \<in> ?R"
       
   325     moreover have "(a, b) \<in> ?L" 
       
   326     proof -
       
   327       have "(a # b # xs) = []@[a,b]@xs" by simp
       
   328       hence "\<exists> l1 l2. (a # b # xs) = l1@[a,b]@l2" by auto
       
   329       thus ?thesis by (unfold edges_on_def, simp)
       
   330     qed
       
   331     moreover {
       
   332         assume "(c, d) \<in> edges_on (b#xs)"
       
   333         then obtain l1 l2 where "b#xs = l1@[c, d]@l2" by (unfold edges_on_def, auto)
       
   334         hence "a#b#xs = (a#l1)@[c,d]@l2" by simp
       
   335         hence "\<exists> l1 l2. (a # b # xs) = l1@[c,d]@l2" by metis
       
   336         hence "(c,d) \<in> ?L" by (unfold edges_on_def, simp)
       
   337     }
       
   338     ultimately have "(c, d) \<in> ?L" by auto
       
   339   } ultimately show ?thesis by auto
       
   340 qed
       
   341 
   285 lemma edges_on_len:
   342 lemma edges_on_len:
   286   assumes "(a,b) \<in> edges_on l"
   343   assumes "(a,b) \<in> edges_on l"
   287   shows "length l \<ge> 2"
   344   shows "length l \<ge> 2"
   288   using assms
   345   using assms
   289   by (unfold edges_on_def, auto)
   346   by (unfold edges_on_def, auto)
   290 
   347 
   291 text {* Elimination of @{text "edges_on"} for non-empty path *}
   348 text {* Elimination of @{text "edges_on"} for non-empty path *}
       
   349 
   292 lemma edges_on_consE [elim, cases set:edges_on]:
   350 lemma edges_on_consE [elim, cases set:edges_on]:
   293   assumes "(a,b) \<in> edges_on (x#xs)"
   351   assumes "(a,b) \<in> edges_on (x#xs)"
   294   obtains (head)  xs' where "x = a" and "xs = b#xs'"
   352   obtains (head)  xs' where "x = a" and "xs = b#xs'"
   295       |  (tail)  "(a,b) \<in> edges_on xs"
   353       |  (tail)  "(a,b) \<in> edges_on xs"
   296 proof -
   354 proof -
   382     show "rpath r2 y ys z" 
   440     show "rpath r2 y ys z" 
   383      using rstep edges_on_Cons_mono[of "y#ys" "x"] by (auto)
   441      using rstep edges_on_Cons_mono[of "y#ys" "x"] by (auto)
   384   qed
   442   qed
   385 qed (unfold rpath_def, auto intro!:Transitive_Closure_Table.rtrancl_path.base)
   443 qed (unfold rpath_def, auto intro!:Transitive_Closure_Table.rtrancl_path.base)
   386 
   444 
       
   445 lemma edges_on_rpathI:
       
   446   assumes "edges_on (a#xs@[b]) \<subseteq> r"
       
   447   shows "rpath r a (xs@[b]) b"
       
   448   using assms
       
   449 proof(induct xs arbitrary: a b)
       
   450   case Nil
       
   451   moreover have "(a, b) \<in> edges_on (a # [] @ [b])"
       
   452       by (unfold edges_on_def, auto)
       
   453   ultimately have "(a, b) \<in> r" by auto
       
   454   thus ?case by auto
       
   455 next
       
   456   case (Cons x xs a b)
       
   457   from this(2) have "edges_on (x # xs @ [b]) \<subseteq> r" by (simp add:edges_on_unfold)
       
   458   from Cons(1)[OF this] have " rpath r x (xs @ [b]) b" .
       
   459   moreover from Cons(2) have "(a, x) \<in> r" by (auto simp:edges_on_unfold)
       
   460   ultimately show ?case by (auto)
       
   461 qed
   387 
   462 
   388 text {*
   463 text {*
   389   The following lemma extracts the path from @{text "x"} to @{text "y"}
   464   The following lemma extracts the path from @{text "x"} to @{text "y"}
   390   from proposition @{text "(x, y) \<in> r^*"}
   465   from proposition @{text "(x, y) \<in> r^*"}
   391 *}
   466 *}
   414   from iffD2[OF rtranclp_eq_rtrancl_path] and assms[unfolded rpath_def]
   489   from iffD2[OF rtranclp_eq_rtrancl_path] and assms[unfolded rpath_def]
   415   have "(pred_of r)\<^sup>*\<^sup>* x y" by metis
   490   have "(pred_of r)\<^sup>*\<^sup>* x y" by metis
   416   thus ?thesis by (simp add: pred_of_star star_2_pstar)
   491   thus ?thesis by (simp add: pred_of_star star_2_pstar)
   417 qed
   492 qed
   418 
   493 
   419 text {*
   494 lemma subtree_transfer:
   420   The following lemmas establishes a relation from pathes in @{text "r"}
   495   assumes "a \<in> subtree r1 a'"
       
   496   and "r1 \<subseteq> r2"
       
   497   shows "a \<in> subtree r2 a'"
       
   498 proof -
       
   499   from assms(1)[unfolded subtree_def] 
       
   500   have "(a, a') \<in> r1^*" by auto
       
   501   from star_rpath[OF this]
       
   502   obtain xs where rp: "rpath r1 a xs a'" by blast
       
   503   hence "rpath r2 a xs a'"
       
   504   proof(rule rpath_transfer)
       
   505     from rpath_edges_on[OF rp] and assms(2)
       
   506     show "edges_on (a # xs) \<subseteq> r2" by simp
       
   507   qed
       
   508   from rpath_star[OF this]
       
   509   show ?thesis by (auto simp:subtree_def)
       
   510 qed
       
   511 
       
   512 lemma subtree_rev_transfer:
       
   513   assumes "a \<notin> subtree r2 a'"
       
   514   and "r1 \<subseteq> r2"
       
   515   shows "a \<notin> subtree r1 a'"
       
   516   using assms and subtree_transfer by metis
       
   517 
       
   518 text {*
       
   519   The following lemmas establishes a relation from paths in @{text "r"}
   421   to @{text "r^+"} relation.
   520   to @{text "r^+"} relation.
   422 *}
   521 *}
   423 lemma rpath_plus: 
   522 lemma rpath_plus: 
   424   assumes "rpath r x xs y"
   523   assumes "rpath r x xs y"
   425   and "xs \<noteq> []"
   524   and "xs \<noteq> []"
   436       with rstep(1) show "(x, y) \<in> r^+" by auto
   535       with rstep(1) show "(x, y) \<in> r^+" by auto
   437     qed
   536     qed
   438   qed
   537   qed
   439 qed
   538 qed
   440 
   539 
   441 subsubsection {* Properties of @{text "subtree"} *}
   540 lemma plus_rpath: 
       
   541   assumes "(x, y) \<in> r^+"
       
   542   obtains xs where "rpath r x xs y" and "xs \<noteq> []"
       
   543 proof -
       
   544   from assms
       
   545   show ?thesis
       
   546   proof(cases rule:converse_tranclE[consumes 1])
       
   547     case 1
       
   548     hence "rpath r x [y] y" by auto
       
   549     from that[OF this] show ?thesis by auto
       
   550   next
       
   551     case (2 z)
       
   552     from 2(2) have "(z, y) \<in> r^*" by auto
       
   553     from star_rpath[OF this] obtain xs where "rpath r z xs y" by auto
       
   554     from rstepI[OF 2(1) this]
       
   555     have "rpath r x (z # xs) y" .
       
   556     from that[OF this] show ?thesis by auto
       
   557   qed
       
   558 qed
       
   559 
       
   560 subsubsection {* Properties of @{text "subtree"} and @{term "ancestors"}*}
       
   561 
       
   562 lemma ancestors_subtreeI:
       
   563   assumes "b \<in> ancestors r a"
       
   564   shows "a \<in> subtree r b"
       
   565   using assms by (auto simp:subtree_def ancestors_def)
       
   566 
       
   567 lemma subtreeE:
       
   568   assumes "a \<in> subtree r b"
       
   569   obtains "a = b"
       
   570       | "a \<noteq> b" and "b \<in> ancestors r a"
       
   571 proof -
       
   572   from assms have "(a, b) \<in> r^*" by (auto simp:subtree_def)
       
   573   from rtranclD[OF this]
       
   574   have " a = b \<or> a \<noteq> b \<and> (a, b) \<in> r\<^sup>+" .
       
   575   with that[unfolded ancestors_def] show ?thesis by auto
       
   576 qed
       
   577 
       
   578 lemma subtree_ancestorsI:
       
   579   assumes "a \<in> subtree r b"
       
   580   and "a \<noteq> b"
       
   581   shows "b \<in> ancestors r a"
       
   582   using assms
       
   583   by (auto elim!:subtreeE)
   442 
   584 
   443 text {*
   585 text {*
   444   @{text "subtree"} is mono with respect to the underlying graph.
   586   @{text "subtree"} is mono with respect to the underlying graph.
   445 *}
   587 *}
   446 lemma subtree_mono:
   588 lemma subtree_mono:
   511     moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto)
   653     moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto)
   512     ultimately have "c \<in> (subtree r x)" by auto
   654     ultimately have "c \<in> (subtree r x)" by auto
   513   } ultimately show ?thesis by auto
   655   } ultimately show ?thesis by auto
   514 qed
   656 qed
   515 
   657 
       
   658 (* ddd *)
       
   659 lemma subset_del_subtree_outside: (* ddd *)
       
   660     assumes "Range r' \<inter> subtree r x = {}" 
       
   661     shows "subtree (r - r') x = (subtree r x)" 
       
   662 proof -
       
   663   { fix c
       
   664     assume "c \<in> (subtree r x)"
       
   665     hence "(c, x) \<in> r^*" by (auto simp:subtree_def)
       
   666     hence "c \<in> subtree (r - r') x"
       
   667     proof(rule star_rpath)
       
   668       fix xs
       
   669       assume rp: "rpath r c xs x"
       
   670       show ?thesis
       
   671       proof -
       
   672         from rp
       
   673         have "rpath  (r - r') c xs x"
       
   674         proof(rule rpath_transfer)
       
   675           from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r" .
       
   676           moreover {
       
   677               fix a b
       
   678               assume h: "(a, b) \<in> r'"
       
   679               have "(a, b) \<notin> edges_on (c#xs)"
       
   680               proof
       
   681                 assume "(a, b) \<in> edges_on (c # xs)"
       
   682                 then obtain l1 l2 where "c#xs = (l1@[a])@[b]@l2" by (auto simp:edges_on_def)
       
   683                 hence "tl (c#xs) = tl (l1@[a,b]@l2)" by simp
       
   684                 then obtain l1' where eq_xs_b: "xs = l1'@[b]@l2" by (cases l1, auto)
       
   685                 from rp[unfolded this]
       
   686                 show False
       
   687                 proof(rule rpath_appendE)
       
   688                   assume "rpath r b l2 x"
       
   689                   from rpath_star[OF this]
       
   690                   have "b \<in> subtree r x" by (auto simp:subtree_def)
       
   691                   with assms (1) and h show ?thesis by (auto)
       
   692                 qed
       
   693              qed
       
   694          } ultimately show "edges_on (c # xs) \<subseteq> r - r'" by auto
       
   695         qed
       
   696         thus ?thesis by (rule rpath_star[elim_format], auto simp:subtree_def)
       
   697       qed
       
   698     qed
       
   699   } moreover {
       
   700     fix c
       
   701     assume "c \<in> subtree (r - r') x"
       
   702     moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto)
       
   703     ultimately have "c \<in> (subtree r x)" by auto
       
   704   } ultimately show ?thesis by auto
       
   705 qed
       
   706 
   516 lemma subtree_insert_ext:
   707 lemma subtree_insert_ext:
   517     assumes "b \<in> subtree r x"
   708     assumes "b \<in> subtree r x"
   518     shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)" 
   709     shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)" 
   519     using assms by (auto simp:subtree_def rtrancl_insert)
   710     using assms by (auto simp:subtree_def rtrancl_insert)
   520 
   711 
   522     assumes "b \<notin> subtree r x"
   713     assumes "b \<notin> subtree r x"
   523     shows "subtree (r \<union> {(a, b)}) x = (subtree r x)" 
   714     shows "subtree (r \<union> {(a, b)}) x = (subtree r x)" 
   524     using assms
   715     using assms
   525     by (auto simp:subtree_def rtrancl_insert)
   716     by (auto simp:subtree_def rtrancl_insert)
   526 
   717 
       
   718 lemma set_add_rootI:
       
   719   assumes "root r a"
       
   720   and "a \<notin> Domain r1"
       
   721   shows "root (r \<union> r1) a"
       
   722 proof -
       
   723   let ?r = "r \<union> r1"
       
   724   { fix a'
       
   725     assume "a' \<in> ancestors ?r a"
       
   726     hence "(a, a') \<in> ?r^+" by (auto simp:ancestors_def)
       
   727     from tranclD[OF this] obtain z where "(a, z) \<in> ?r" by auto
       
   728     moreover have "(a, z) \<notin> r"
       
   729     proof
       
   730       assume "(a, z) \<in> r"
       
   731       with assms(1) show False 
       
   732         by (auto simp:root_def ancestors_def)
       
   733     qed
       
   734     ultimately have "(a, z) \<in> r1" by auto
       
   735     with assms(2) 
       
   736     have False by (auto)
       
   737   } thus ?thesis by (auto simp:root_def)
       
   738 qed
       
   739 
       
   740 lemma ancestors_mono:
       
   741   assumes "r1 \<subseteq> r2"
       
   742   shows "ancestors r1 x \<subseteq> ancestors r2 x"
       
   743 proof
       
   744  fix a
       
   745  assume "a \<in> ancestors r1 x"
       
   746  hence "(x, a) \<in> r1^+" by (auto simp:ancestors_def)
       
   747  from plus_rpath[OF this] obtain xs where 
       
   748     h: "rpath r1 x xs a" "xs \<noteq> []" .
       
   749  have "rpath r2 x xs a"
       
   750  proof(rule rpath_transfer[OF h(1)])
       
   751   from rpath_edges_on[OF h(1)] and assms
       
   752   show "edges_on (x # xs) \<subseteq> r2" by auto
       
   753  qed
       
   754  from rpath_plus[OF this h(2)]
       
   755  show "a \<in> ancestors r2 x" by (auto simp:ancestors_def)
       
   756 qed
       
   757 
       
   758 lemma subtree_refute:
       
   759   assumes "x \<notin> ancestors r y"
       
   760   and "x \<noteq> y"
       
   761   shows "y \<notin> subtree r x"
       
   762 proof
       
   763    assume "y \<in> subtree r x"
       
   764    thus False
       
   765      by(elim subtreeE, insert assms, auto)
       
   766 qed
       
   767 
   527 subsubsection {* Properties about relational trees *}
   768 subsubsection {* Properties about relational trees *}
   528 
   769 
   529 context rtree 
   770 context rtree 
   530 begin
   771 begin
       
   772 
       
   773 lemma ancestors_headE:
       
   774   assumes "c \<in> ancestors r a"
       
   775   assumes "(a, b) \<in> r"
       
   776   obtains "b = c"
       
   777      |   "c \<in> ancestors r b"
       
   778 proof -
       
   779   from assms(1) 
       
   780   have "(a, c) \<in> r^+" by (auto simp:ancestors_def)
       
   781   hence "b = c \<or> c \<in> ancestors r b"
       
   782   proof(cases rule:converse_tranclE[consumes 1])
       
   783     case 1
       
   784     with assms(2) and sgv have "b = c" by (auto simp:single_valued_def)
       
   785     thus ?thesis by auto
       
   786   next
       
   787     case (2 y)
       
   788     from 2(1) and assms(2) and sgv have "y = b" by (auto simp:single_valued_def)
       
   789     from 2(2)[unfolded this] have "c \<in> ancestors r b" by (auto simp:ancestors_def)
       
   790     thus ?thesis by auto
       
   791   qed
       
   792   with that show ?thesis by metis
       
   793 qed
       
   794 
       
   795 lemma ancestors_accum:
       
   796   assumes "(a, b) \<in> r"
       
   797   shows "ancestors r a = ancestors r b \<union> {b}"
       
   798 proof -
       
   799   { fix c
       
   800     assume "c \<in> ancestors r a"
       
   801     hence "(a, c) \<in> r^+" by (auto simp:ancestors_def)
       
   802     hence "c \<in> ancestors r b \<union> {b}"
       
   803     proof(cases rule:converse_tranclE[consumes 1])
       
   804       case 1
       
   805       with sgv assms have "c = b" by (unfold single_valued_def, auto)
       
   806       thus ?thesis by auto
       
   807     next
       
   808       case (2 c')
       
   809       with sgv assms have "c' = b" by (unfold single_valued_def, auto)
       
   810       from 2(2)[unfolded this]
       
   811       show ?thesis by (auto simp:ancestors_def)
       
   812     qed
       
   813   } moreover {
       
   814     fix c
       
   815     assume "c \<in> ancestors r b \<union> {b}"
       
   816     hence "c = b \<or> c \<in> ancestors r b" by auto
       
   817     hence "c \<in> ancestors r a"
       
   818     proof
       
   819       assume "c = b"
       
   820       from assms[folded this] 
       
   821       show ?thesis by (auto simp:ancestors_def)
       
   822     next
       
   823       assume "c \<in> ancestors r b"
       
   824       with assms show ?thesis by (auto simp:ancestors_def)
       
   825     qed
       
   826   } ultimately show ?thesis by auto
       
   827 qed
       
   828 
       
   829 lemma rootI:
       
   830   assumes h: "\<And> x'. x' \<noteq> x \<Longrightarrow> x \<notin> subtree r' x'"
       
   831   and "r' \<subseteq> r"
       
   832   shows "root r' x"
       
   833 proof -
       
   834   from acyclic_subset[OF acl assms(2)]
       
   835   have acl': "acyclic r'" .
       
   836   { fix x'
       
   837     assume "x' \<in> ancestors r' x"
       
   838     hence h1: "(x, x') \<in> r'^+" by (auto simp:ancestors_def)
       
   839     have "x' \<noteq> x"
       
   840     proof
       
   841       assume eq_x: "x' = x"
       
   842       from h1[unfolded this] and acl'
       
   843       show False by (auto simp:acyclic_def)
       
   844     qed
       
   845     moreover from h1 have "x \<in> subtree r' x'" by (auto simp:subtree_def)
       
   846     ultimately have False using h by auto
       
   847   } thus ?thesis by (auto simp:root_def)
       
   848 qed
   531 
   849 
   532 lemma rpath_overlap_oneside: (* ddd *)
   850 lemma rpath_overlap_oneside: (* ddd *)
   533   assumes "rpath r x xs1 x1"
   851   assumes "rpath r x xs1 x1"
   534   and "rpath r x xs2 x2"
   852   and "rpath r x xs2 x2"
   535   and "length xs1 \<le> length xs2"
   853   and "length xs1 \<le> length xs2"
   951   } 
  1269   } 
   952   -- {* The equality of sets is derived from the two directions just proved. *}
  1270   -- {* The equality of sets is derived from the two directions just proved. *}
   953   ultimately show ?thesis by auto
  1271   ultimately show ?thesis by auto
   954 qed 
  1272 qed 
   955 
  1273 
       
  1274 lemma  set_del_rootI:
       
  1275   assumes "r1 \<subseteq> r"
       
  1276   and "a \<in> Domain r1"
       
  1277   shows "root (r - r1) a"
       
  1278 proof -
       
  1279    let ?r = "r - r1"
       
  1280   { fix a' 
       
  1281     assume neq: "a' \<noteq> a"
       
  1282     have "a \<notin> subtree ?r a'"
       
  1283     proof
       
  1284       assume "a \<in> subtree ?r a'"
       
  1285       hence "(a, a') \<in> ?r^*" by (auto simp:subtree_def)
       
  1286       from star_rpath[OF this] obtain xs
       
  1287       where rp: "rpath ?r a xs a'" by auto
       
  1288       from rpathE[OF this] and neq
       
  1289       obtain z zs where h: "(a, z) \<in> ?r" "rpath ?r z zs a'" "xs = z#zs" by auto
       
  1290       from assms(2) obtain z' where z'_in: "(a, z') \<in> r1" by (auto simp:DomainE)
       
  1291       with assms(1) have "(a, z') \<in> r" by auto
       
  1292       moreover from h(1) have "(a, z) \<in> r" by simp 
       
  1293       ultimately have "z' = z" using sgv by (auto simp:single_valued_def)
       
  1294       from z'_in[unfolded this] and h(1) show False by auto
       
  1295    qed
       
  1296   } thus ?thesis by (intro rootI, auto)
       
  1297 qed
       
  1298 
       
  1299 lemma edge_del_no_rootI:
       
  1300   assumes "(a, b) \<in> r"
       
  1301   shows "root (r - {(a, b)}) a"
       
  1302   by (rule set_del_rootI, insert assms, auto)
       
  1303 
       
  1304 lemma ancestors_children_unique:
       
  1305   assumes "z1 \<in> ancestors r x \<inter> children r y"
       
  1306   and "z2 \<in> ancestors r x \<inter> children r y"
       
  1307   shows "z1 = z2"
       
  1308 proof -
       
  1309   from assms have h:
       
  1310      "(x, z1) \<in> r^+" "(z1, y) \<in> r" 
       
  1311      "(x, z2) \<in> r^+" "(z2, y) \<in> r" 
       
  1312   by (auto simp:ancestors_def children_def)
       
  1313 
       
  1314   -- {* From this, a path containing @{text "z1"} is obtained. *}
       
  1315   from plus_rpath[OF h(1)] obtain xs1 
       
  1316      where h1: "rpath r x xs1 z1" "xs1 \<noteq> []" by auto
       
  1317   from rpath_nnl_lastE[OF this] obtain xs1' where eq_xs1: "xs1 = xs1' @ [z1]"
       
  1318     by auto
       
  1319   from h(2) have h2: "rpath r z1 [y] y" by auto
       
  1320   from rpath_appendI[OF h1(1) h2, unfolded eq_xs1]
       
  1321   have rp1: "rpath r x (xs1' @ [z1, y]) y" by simp
       
  1322 
       
  1323   -- {* Then, another path containing @{text "z2"} is obtained. *}
       
  1324   from plus_rpath[OF h(3)] obtain xs2
       
  1325      where h3: "rpath r x xs2 z2" "xs2 \<noteq> []" by auto
       
  1326   from rpath_nnl_lastE[OF this] obtain xs2' where eq_xs2: "xs2 = xs2' @ [z2]"
       
  1327     by auto
       
  1328   from h(4) have h4: "rpath r z2 [y] y" by auto
       
  1329   from rpath_appendI[OF h3(1) h4, unfolded eq_xs2]
       
  1330      have "rpath r x (xs2' @ [z2, y]) y" by simp
       
  1331 
       
  1332   -- {* Finally @{text "z1 = z2"} is proved by uniqueness of path. *}
       
  1333   from rpath_unique[OF rp1 this]
       
  1334   have "xs1' @ [z1, y] = xs2' @ [z2, y]" .
       
  1335   thus ?thesis by auto
       
  1336 qed
       
  1337 
       
  1338 lemma ancestors_childrenE:
       
  1339   assumes "y \<in> ancestors r x"
       
  1340   obtains "x \<in> children r y"
       
  1341       | z where "z \<in> ancestors r x \<inter> children r y"
       
  1342 proof -
       
  1343   from assms(1) have "(x, y) \<in> r^+" by (auto simp:ancestors_def)
       
  1344   from tranclD2[OF this] obtain z where 
       
  1345      h: "(x, z) \<in> r\<^sup>*" "(z, y) \<in> r" by auto
       
  1346   from h(1)
       
  1347   show ?thesis
       
  1348   proof(cases rule:rtranclE)
       
  1349     case base
       
  1350     from h(2)[folded this] have "x \<in> children r y" 
       
  1351               by (auto simp:children_def)
       
  1352     thus ?thesis by (intro that, auto)
       
  1353   next
       
  1354     case (step u)
       
  1355     hence "z \<in> ancestors r x" by (auto simp:ancestors_def)
       
  1356     moreover from h(2) have "z \<in> children r y" 
       
  1357               by (auto simp:children_def)
       
  1358     ultimately show ?thesis by (intro that, auto)
       
  1359   qed
       
  1360 qed
       
  1361 
       
  1362 
       
  1363 end (* of rtree *)
       
  1364 
       
  1365 lemma subtree_children:
       
  1366   "subtree r x = {x} \<union> (\<Union> (subtree r ` (children r x)))" (is "?L = ?R")
       
  1367 proof -
       
  1368   { fix z
       
  1369     assume "z \<in> ?L"
       
  1370     hence "z \<in> ?R"
       
  1371     proof(cases rule:subtreeE[consumes 1])
       
  1372       case 2
       
  1373       hence "(z, x) \<in> r^+" by (auto simp:ancestors_def)
       
  1374       thus ?thesis
       
  1375       proof(rule tranclE)
       
  1376         assume "(z, x) \<in> r"
       
  1377         hence "z \<in> children r x" by (unfold children_def, auto)
       
  1378         moreover have "z \<in> subtree r z" by (auto simp:subtree_def)
       
  1379         ultimately show ?thesis by auto
       
  1380       next
       
  1381         fix c
       
  1382         assume h: "(z, c) \<in> r\<^sup>+" "(c, x) \<in> r"
       
  1383         hence "c \<in> children r x" by (auto simp:children_def)
       
  1384         moreover from h have "z \<in> subtree r c" by (auto simp:subtree_def)
       
  1385         ultimately show ?thesis by auto
       
  1386       qed
       
  1387     qed auto
       
  1388   } moreover {
       
  1389     fix z
       
  1390     assume h: "z \<in> ?R"
       
  1391     have "x \<in> subtree r x" by (auto simp:subtree_def)
       
  1392     moreover {
       
  1393        assume "z \<in> \<Union>(subtree r ` children r x)"
       
  1394        then obtain y where "(y, x) \<in> r" "(z, y) \<in> r^*" 
       
  1395         by (auto simp:subtree_def children_def)
       
  1396        hence "(z, x) \<in> r^*" by auto
       
  1397        hence "z \<in> ?L" by (auto simp:subtree_def)
       
  1398     } ultimately have "z \<in> ?L" using h by auto
       
  1399   } ultimately show ?thesis by auto
       
  1400 qed
       
  1401 
       
  1402 context fsubtree 
       
  1403 begin
       
  1404   
       
  1405 lemma finite_subtree:
       
  1406   shows "finite (subtree r x)"
       
  1407 proof(induct rule:wf_induct[OF wf])
       
  1408   case (1 x)
       
  1409   have "finite (\<Union>(subtree r ` children r x))"
       
  1410   proof(rule finite_Union)
       
  1411     show "finite (subtree r ` children r x)"
       
  1412     proof(cases "children r x = {}")
       
  1413       case True
       
  1414       thus ?thesis by auto
       
  1415     next
       
  1416       case False
       
  1417       hence "x \<in> Range r" by (auto simp:children_def)
       
  1418       from fb[rule_format, OF this] 
       
  1419       have "finite (children r x)" .
       
  1420       thus ?thesis by (rule finite_imageI)
       
  1421     qed
       
  1422   next
       
  1423     fix M 
       
  1424     assume "M \<in> subtree r ` children r x"
       
  1425     then obtain y where h: "y \<in> children r x" "M = subtree r y" by auto
       
  1426     hence "(y, x) \<in> r" by (auto simp:children_def)
       
  1427     from 1[rule_format, OF this, folded h(2)]
       
  1428     show "finite M" .
       
  1429   qed
       
  1430   thus ?case
       
  1431     by (unfold subtree_children finite_Un, auto)
       
  1432 qed
       
  1433 
   956 end
  1434 end
   957 
  1435 
       
  1436 definition "pairself f = (\<lambda>(a, b). (f a, f b))"
       
  1437 
       
  1438 definition "rel_map f r = (pairself f ` r)"
       
  1439 
       
  1440 lemma rel_mapE: 
       
  1441   assumes "(a, b) \<in> rel_map f r"
       
  1442   obtains c d 
       
  1443   where "(c, d) \<in> r" "(a, b) = (f c, f d)"
       
  1444   using assms
       
  1445   by (unfold rel_map_def pairself_def, auto)
       
  1446 
       
  1447 lemma rel_mapI: 
       
  1448   assumes "(a, b) \<in> r"
       
  1449     and "c = f a"
       
  1450     and "d = f b"
       
  1451   shows "(c, d) \<in> rel_map f r"
       
  1452   using assms
       
  1453   by (unfold rel_map_def pairself_def, auto)
       
  1454 
       
  1455 lemma map_appendE:
       
  1456   assumes "map f zs = xs @ ys"
       
  1457   obtains xs' ys' 
       
  1458   where "zs = xs' @ ys'" "xs = map f xs'" "ys = map f ys'"
       
  1459 proof -
       
  1460   have "\<exists> xs' ys'. zs = xs' @ ys' \<and> xs = map f xs' \<and> ys = map f ys'"
       
  1461   using assms
       
  1462   proof(induct xs arbitrary:zs ys)
       
  1463     case (Nil zs ys)
       
  1464     thus ?case by auto
       
  1465   next
       
  1466     case (Cons x xs zs ys)
       
  1467     note h = this
       
  1468     show ?case
       
  1469     proof(cases zs)
       
  1470       case (Cons e es)
       
  1471       with h have eq_x: "map f es = xs @ ys" "x = f e" by auto
       
  1472       from h(1)[OF this(1)]
       
  1473       obtain xs' ys' where "es = xs' @ ys'" "xs = map f xs'" "ys = map f ys'"
       
  1474         by blast
       
  1475       with Cons eq_x
       
  1476       have "zs = (e#xs') @ ys' \<and> x # xs = map f (e#xs') \<and> ys = map f ys'" by auto
       
  1477       thus ?thesis by metis
       
  1478     qed (insert h, auto)
       
  1479   qed
       
  1480   thus ?thesis by (auto intro!:that)
       
  1481 qed
       
  1482 
       
  1483 lemma rel_map_mono:
       
  1484   assumes "r1 \<subseteq> r2"
       
  1485   shows "rel_map f r1 \<subseteq> rel_map f r2"
       
  1486   using assms
       
  1487   by (auto simp:rel_map_def pairself_def)
       
  1488 
       
  1489 lemma rel_map_compose [simp]:
       
  1490     shows "rel_map f1 (rel_map f2 r) = rel_map (f1 o f2) r"
       
  1491     by (auto simp:rel_map_def pairself_def)
       
  1492 
       
  1493 lemma edges_on_map: "edges_on (map f xs) = rel_map f (edges_on xs)"
       
  1494 proof -
       
  1495   { fix a b
       
  1496     assume "(a, b) \<in> edges_on (map f xs)"
       
  1497     then obtain l1 l2 where eq_map: "map f xs = l1 @ [a, b] @ l2" 
       
  1498       by (unfold edges_on_def, auto)
       
  1499     hence "(a, b) \<in> rel_map f (edges_on xs)"
       
  1500       by (auto elim!:map_appendE intro!:rel_mapI simp:edges_on_def)
       
  1501   } moreover { 
       
  1502     fix a b
       
  1503     assume "(a, b) \<in> rel_map f (edges_on xs)"
       
  1504     then obtain c d where 
       
  1505         h: "(c, d) \<in> edges_on xs" "(a, b) = (f c, f d)" 
       
  1506              by (elim rel_mapE, auto)
       
  1507     then obtain l1 l2 where
       
  1508         eq_xs: "xs = l1 @ [c, d] @ l2" 
       
  1509              by (auto simp:edges_on_def)
       
  1510     hence eq_map: "map f xs = map f l1 @ [f c, f d] @ map f l2" by auto
       
  1511     have "(a, b) \<in> edges_on (map f xs)"
       
  1512     proof -
       
  1513       from h(2) have "[f c, f d] = [a, b]" by simp
       
  1514       from eq_map[unfolded this] show ?thesis by (auto simp:edges_on_def)
       
  1515     qed
       
  1516   } ultimately show ?thesis by auto
       
  1517 qed
       
  1518 
       
  1519 lemma image_id:
       
  1520   assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x"
       
  1521   shows "f ` A = A"
       
  1522   using assms by (auto simp:image_def)
       
  1523 
       
  1524 lemma rel_map_inv_id:
       
  1525   assumes "inj_on f ((Domain r) \<union> (Range r))"
       
  1526   shows "(rel_map (inv_into ((Domain r) \<union> (Range r)) f \<circ> f) r) = r"
       
  1527 proof -
       
  1528  let ?f = "(inv_into (Domain r \<union> Range r) f \<circ> f)"
       
  1529  {
       
  1530   fix a b
       
  1531   assume h0: "(a, b) \<in> r"
       
  1532   have "pairself ?f (a, b) = (a, b)"
       
  1533   proof -
       
  1534     from assms h0 have "?f a = a" by (auto intro:inv_into_f_f)
       
  1535     moreover have "?f b = b"
       
  1536       by (insert h0, simp, intro inv_into_f_f[OF assms], auto intro!:RangeI)
       
  1537     ultimately show ?thesis by (auto simp:pairself_def)
       
  1538   qed
       
  1539  } thus ?thesis by (unfold rel_map_def, intro image_id, case_tac x, auto)
       
  1540 qed 
       
  1541 
       
  1542 lemma rel_map_acyclic:
       
  1543   assumes "acyclic r"
       
  1544   and "inj_on f ((Domain r) \<union> (Range r))"
       
  1545   shows "acyclic (rel_map f r)"
       
  1546 proof -
       
  1547   let ?D = "Domain r \<union> Range r"
       
  1548   { fix a 
       
  1549     assume "(a, a) \<in> (rel_map f r)^+" 
       
  1550     from plus_rpath[OF this]
       
  1551     obtain xs where rp: "rpath (rel_map f r) a xs a" "xs \<noteq> []" by auto
       
  1552     from rpath_nnl_lastE[OF this] obtain xs' where eq_xs: "xs = xs'@[a]" by auto
       
  1553     from rpath_edges_on[OF rp(1)]
       
  1554     have h: "edges_on (a # xs) \<subseteq> rel_map f r" .
       
  1555     from edges_on_map[of "inv_into ?D f" "a#xs"]
       
  1556     have "edges_on (map (inv_into ?D f) (a # xs)) = rel_map (inv_into ?D f) (edges_on (a # xs))" .
       
  1557     with rel_map_mono[OF h, of "inv_into ?D f"]
       
  1558     have "edges_on (map (inv_into ?D f) (a # xs)) \<subseteq> rel_map ((inv_into ?D f) o f) r" by simp
       
  1559     from this[unfolded eq_xs]
       
  1560     have subr: "edges_on (map (inv_into ?D f) (a # xs' @ [a])) \<subseteq> rel_map (inv_into ?D f \<circ> f) r" .
       
  1561     have "(map (inv_into ?D f) (a # xs' @ [a])) = (inv_into ?D f a) # map (inv_into ?D f) xs' @ [inv_into ?D f a]"
       
  1562       by simp
       
  1563     from edges_on_rpathI[OF subr[unfolded this]]
       
  1564     have "rpath (rel_map (inv_into ?D f \<circ> f) r) 
       
  1565                       (inv_into ?D f a) (map (inv_into ?D f) xs' @ [inv_into ?D f a]) (inv_into ?D f a)" .
       
  1566     hence "(inv_into ?D f a, inv_into ?D f a) \<in> (rel_map (inv_into ?D f \<circ> f) r)^+"
       
  1567         by (rule rpath_plus, simp)
       
  1568     moreover have "(rel_map (inv_into ?D f \<circ> f) r) = r" by (rule rel_map_inv_id[OF assms(2)])
       
  1569     moreover note assms(1) 
       
  1570     ultimately have False by (unfold acyclic_def, auto)
       
  1571   } thus ?thesis by (auto simp:acyclic_def)
       
  1572 qed
       
  1573 
       
  1574 lemma relpow_mult: 
       
  1575   "((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)"
       
  1576 proof(induct n arbitrary:m)
       
  1577   case (Suc k m)
       
  1578   thus ?case
       
  1579   proof -
       
  1580     have h: "(m * k + m) = (m + m * k)" by auto
       
  1581     show ?thesis 
       
  1582       apply (simp add:Suc relpow_add[symmetric])
       
  1583       by (unfold h, simp)
       
  1584   qed
       
  1585 qed simp
       
  1586 
       
  1587 lemma compose_relpow_2:
       
  1588   assumes "r1 \<subseteq> r"
       
  1589   and "r2 \<subseteq> r"
       
  1590   shows "r1 O r2 \<subseteq> r ^^ (2::nat)"
       
  1591 proof -
       
  1592   { fix a b
       
  1593     assume "(a, b) \<in> r1 O r2"
       
  1594     then obtain e where "(a, e) \<in> r1" "(e, b) \<in> r2"
       
  1595       by auto
       
  1596     with assms have "(a, e) \<in> r" "(e, b) \<in> r" by auto
       
  1597     hence "(a, b) \<in> r ^^ (Suc (Suc 0))" by auto
       
  1598   } thus ?thesis by (auto simp:numeral_2_eq_2)
       
  1599 qed
       
  1600 
       
  1601 lemma acyclic_compose:
       
  1602   assumes "acyclic r"
       
  1603   and "r1 \<subseteq> r"
       
  1604   and "r2 \<subseteq> r"
       
  1605   shows "acyclic (r1 O r2)"
       
  1606 proof -
       
  1607   { fix a
       
  1608     assume "(a, a) \<in> (r1 O r2)^+"
       
  1609     from trancl_mono[OF this compose_relpow_2[OF assms(2, 3)]]
       
  1610     have "(a, a) \<in> (r ^^ 2) ^+" .
       
  1611     from trancl_power[THEN iffD1, OF this]
       
  1612     obtain n where h: "(a, a) \<in> (r ^^ 2) ^^ n" "n > 0" by blast
       
  1613     from this(1)[unfolded relpow_mult] have h2: "(a, a) \<in> r ^^ (2 * n)" .
       
  1614     have "(a, a) \<in> r^+" 
       
  1615     proof(cases rule:trancl_power[THEN iffD2])
       
  1616       from h(2) h2 show "\<exists>n>0. (a, a) \<in> r ^^ n" 
       
  1617         by (rule_tac x = "2*n" in exI, auto)
       
  1618     qed
       
  1619     with assms have "False" by (auto simp:acyclic_def)
       
  1620   } thus ?thesis by (auto simp:acyclic_def)
       
  1621 qed
       
  1622 
       
  1623 lemma children_compose_unfold: 
       
  1624   "children (r1 O r2) x = \<Union> (children r1 ` (children r2 x))"
       
  1625   by (auto simp:children_def)
       
  1626 
       
  1627 lemma fbranch_compose:
       
  1628   assumes "fbranch r1"
       
  1629   and "fbranch r2"
       
  1630   shows "fbranch (r1 O r2)"
       
  1631 proof -
       
  1632   {  fix x
       
  1633      assume "x\<in>Range (r1 O r2)"
       
  1634      then obtain y z where h: "(y, z) \<in> r1" "(z, x) \<in> r2" by auto
       
  1635      have "finite (children (r1 O r2) x)"
       
  1636      proof(unfold children_compose_unfold, rule finite_Union)
       
  1637       show "finite (children r1 ` children r2 x)"
       
  1638       proof(rule finite_imageI)
       
  1639         from h(2) have "x \<in> Range r2" by auto
       
  1640         from assms(2)[unfolded fbranch_def, rule_format, OF this]
       
  1641         show "finite (children r2 x)" .
       
  1642       qed
       
  1643      next
       
  1644        fix M
       
  1645        assume "M \<in> children r1 ` children r2 x"
       
  1646        then obtain y where h1: "y \<in> children r2 x" "M = children r1 y" by auto
       
  1647        show "finite M"
       
  1648        proof(cases "children r1 y = {}")
       
  1649           case True
       
  1650           with h1(2) show ?thesis by auto
       
  1651        next
       
  1652           case False
       
  1653           hence "y \<in> Range r1" by (unfold children_def, auto)
       
  1654           from assms(1)[unfolded fbranch_def, rule_format, OF this, folded h1(2)]
       
  1655           show ?thesis .
       
  1656        qed
       
  1657      qed
       
  1658   } thus ?thesis by (unfold fbranch_def, auto)
       
  1659 qed
       
  1660 
       
  1661 lemma finite_fbranchI:
       
  1662   assumes "finite r"
       
  1663   shows "fbranch r"
       
  1664 proof -
       
  1665   { fix x 
       
  1666     assume "x \<in>Range r"
       
  1667     have "finite (children r x)"
       
  1668     proof -
       
  1669       have "{y. (y, x) \<in> r} \<subseteq> Domain r" by (auto)
       
  1670       from rev_finite_subset[OF finite_Domain[OF assms] this]
       
  1671       have "finite {y. (y, x) \<in> r}" .
       
  1672       thus ?thesis by (unfold children_def, simp)
       
  1673     qed
       
  1674   } thus ?thesis by (auto simp:fbranch_def)
       
  1675 qed
       
  1676 
       
  1677 lemma subset_fbranchI:
       
  1678   assumes "fbranch r1"
       
  1679   and "r2 \<subseteq> r1"
       
  1680   shows "fbranch r2"
       
  1681 proof -
       
  1682   { fix x
       
  1683     assume "x \<in>Range r2"
       
  1684     with assms(2) have "x \<in> Range r1" by auto
       
  1685     from assms(1)[unfolded fbranch_def, rule_format, OF this]
       
  1686     have "finite (children r1 x)" .
       
  1687     hence "finite (children r2 x)"
       
  1688     proof(rule rev_finite_subset)
       
  1689       from assms(2)
       
  1690       show "children r2 x \<subseteq> children r1 x" by (auto simp:children_def)
       
  1691     qed
       
  1692   } thus ?thesis by (auto simp:fbranch_def)
       
  1693 qed
       
  1694 
       
  1695 lemma children_subtree: 
       
  1696   shows "children r x \<subseteq> subtree r x"
       
  1697   by (auto simp:children_def subtree_def)
       
  1698 
       
  1699 lemma children_union_kept:
       
  1700   assumes "x \<notin> Range r'"
       
  1701   shows "children (r \<union> r') x = children r x"
       
  1702   using assms
       
  1703   by (auto simp:children_def)
       
  1704 
   958 end
  1705 end