1 theory RTree

     1 theory RTree

     2 imports "~~/src/HOL/Library/Transitive_Closure_Table" Max

     2 imports "~~/src/HOL/Library/Transitive_Closure_Table" Max

     3 begin

     4 begin

     4 

     5 

     5 section {* A theory of relational trees *}

     6 section {* A theory of relational trees *}

     6 

     7 

     7 inductive_cases path_nilE [elim!]: "rtrancl_path r x [] y"

     8 inductive_cases path_nilE [elim!]: "rtrancl_path r x [] y"

    97   of `an edge @{text "(a, b)"} is in the sub-tree of @{text "x"}`, 

    98   of `an edge @{text "(a, b)"} is in the sub-tree of @{text "x"}`, 

    98   i.e., both @{text "a"} and @{text "b"} are in the sub-tree.

    99   i.e., both @{text "a"} and @{text "b"} are in the sub-tree.

    99 *}

   100 *}

   100 lemma edges_in_meaning: 

   101 lemma edges_in_meaning: 

   101   "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x}"

   102   "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x}"

   115 

   104 

   116 text {*

   105 text {*

   117   The following lemma shows the meaning of @{term "edges_in"} from the other side, 

   106   The following lemma shows the meaning of @{term "edges_in"} from the other side, 

   118   which says: for the edge @{text "(a,b)"} to be outside of the sub-tree of @{text "x"}, 

   107   which says: for the edge @{text "(a,b)"} to be outside of the sub-tree of @{text "x"}, 

   119   it is sufficient to show that @{text "b"} is.

   108   it is sufficient to show that @{text "b"} is.

   129   fixes r

   118   fixes r

   130   assumes fb: "\<forall> x \<in> Range r . finite (children r x)"

   119   assumes fb: "\<forall> x \<in> Range r . finite (children r x)"

   131 begin

   120 begin

   132 

   121 

   133 lemma finite_children: "finite (children r x)"

   122 lemma finite_children: "finite (children r x)"

   144 

   124 

   145 end

   125 end

   146 

   126 

   147 locale fsubtree = fbranch + 

   127 locale fsubtree = fbranch + 

   148    assumes wf: "wf r"

   128    assumes wf: "wf r"

   151 

   129 

   152 subsection {* Auxiliary lemmas *}

   130 subsection {* Auxiliary lemmas *}

   153 

   131 

   154 lemma index_minimize:

   132 lemma index_minimize:

   155   assumes "P (i::nat)"

   133   assumes "P (i::nat)"

   156   obtains j where "P j" and "\<forall> k < j. \<not> P k" 

   134   obtains j where "P j" and "\<forall> k < j. \<not> P k" 

   176 

   137 

   177 subsection {* Properties of Relational Graphs and Relational Trees *}

   138 subsection {* Properties of Relational Graphs and Relational Trees *}

   178 

   139 

   179 subsubsection {* Properties of @{text "rel_of"} and @{text "pred_of"} *}

   140 subsubsection {* Properties of @{text "rel_of"} and @{text "pred_of"} *}

   180 

   141 

   208     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"

   169     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"

   209   shows "P x1 x2 x3"

   170   shows "P x1 x2 x3"

   210   using assms[unfolded rpath_def]

   171   using assms[unfolded rpath_def]

   211   by (induct, auto simp:pred_of_def rpath_def)

   172   by (induct, auto simp:pred_of_def rpath_def)

   212 

   173 

   214   assumes "rpath r x xs y"

   175   assumes "rpath r x xs y"

   215   obtains (base) "y = x" "xs = []"

   176   obtains (base) "y = x" "xs = []"

   216      | (step) z zs where "(x, z) \<in> r" "rpath r z zs y" "xs = z#zs"

   177      | (step) z zs where "(x, z) \<in> r" "rpath r z zs y" "xs = z#zs"

   217   using assms

   178   using assms

   218   by (induct, auto)

   179   by (induct, auto)

   234 next

   195 next

   235   from assms(2) show "rtrancl_path (pred_of r) y ys z"  

   196   from assms(2) show "rtrancl_path (pred_of r) y ys z"  

   236   by (auto simp:pred_of_def rpath_def)

   197   by (auto simp:pred_of_def rpath_def)

   237 qed

   198 qed

   238 

   199 

   239 text {* Introduction rule for @{text "@"}-path *}

   207 text {* Introduction rule for @{text "@"}-path *}

   241   assumes "rpath r x xs a" and "rpath r a ys y"

   209   assumes "rpath r x xs a" and "rpath r a ys y"

   242   shows "rpath r x (xs @ ys) y"

   210   shows "rpath r x (xs @ ys) y"

   243   using assms 

   211   using assms 

   244   by (unfold rpath_def, auto intro:rtrancl_path_trans)

   212   by (unfold rpath_def, auto intro:rtrancl_path_trans)

   245 

   213 

   246 text {* Elimination rule for empty path *}

   214 text {* Elimination rule for empty path *}

   247 

   215 

   249   assumes "rpath r a1 a2 a3"

   217   assumes "rpath r a1 a2 a3"

   250   obtains (rbase)  "a1 = a3" and "a2 = []"

   218   obtains (rbase)  "a1 = a3" and "a2 = []"

   251     | (rstep)  y :: "'a" and ys :: "'a list"  

   219     | (rstep)  y :: "'a" and ys :: "'a list"  

   252          where "(a1, y) \<in> r" and "a2 = y # ys" and "rpath r y ys a3"

   220          where "(a1, y) \<in> r" and "a2 = y # ys" and "rpath r y ys a3"

   253   using assms [unfolded rpath_def]

   221   using assms [unfolded rpath_def]

   256 lemma rpath_nilE [elim!, cases pred:rpath]: 

   224 lemma rpath_nilE [elim!, cases pred:rpath]: 

   257   assumes "rpath r x [] y"

   225   assumes "rpath r x [] y"

   258   obtains "y = x"

   226   obtains "y = x"

   259   using assms[unfolded rpath_def] by auto

   227   using assms[unfolded rpath_def] by auto

   260 

   228 

   276 text {*

   229 text {*

   277   Elimination rule for non-empty paths constructed with @{text "#"}.

   230   Elimination rule for non-empty paths constructed with @{text "#"}.

   278 *}

   231 *}

   279 

   232 

   280 lemma rpath_ConsE [elim!, cases pred:rpath]:

   233 lemma rpath_ConsE [elim!, cases pred:rpath]:

   285 

   238 

   286 text {*

   239 text {*

   287   Elimination rule for non-empty path, where the destination node 

   240   Elimination rule for non-empty path, where the destination node 

   288   @{text "y"} is shown to be at the end of the path.

   241   @{text "y"} is shown to be at the end of the path.

   289 *}

   242 *}

   291   assumes "rpath r x xs y"

   244   assumes "rpath r x xs y"

   292   and "xs \<noteq> []"

   245   and "xs \<noteq> []"

   293   obtains xs' where "xs = xs'@[y]"

   246   obtains xs' where "xs = xs'@[y]"

   296 

   252 

   297 text {* Other elimination rules of @{text "rpath"} *}

   253 text {* Other elimination rules of @{text "rpath"} *}

   298 

   254 

   300   assumes "rpath r x (xs @ [a] @ ys) y"

   256   assumes "rpath r x (xs @ [a] @ ys) y"

   301   obtains "rpath r x (xs @ [a]) a" and "rpath r a ys y"

   257   obtains "rpath r x (xs @ [a]) a" and "rpath r a ys y"

   302   using rtrancl_path_appendE[OF assms[unfolded rpath_def, simplified], folded rpath_def]

   258   using rtrancl_path_appendE[OF assms[unfolded rpath_def, simplified], folded rpath_def]

   303   by auto

   259   by auto

   304 

   260 

   306   assumes "rpath r x (xs @ [a] @ ys @ [b] @ zs) y"

   262   assumes "rpath r x (xs @ [a] @ ys @ [b] @ zs) y"

   307   obtains "rpath r x (xs @ [a]) a" and "rpath r a (ys @ [b]) b" and "rpath r b zs y" 

   263   obtains "rpath r x (xs @ [a]) a" and "rpath r a (ys @ [b]) b" and "rpath r b zs y" 

   308   using assms

   264   using assms

   309  by (elim rpath_appendE, auto)

   265  by (elim rpath_appendE, auto)

   310 

   266 

   311 text {* Every path has a unique end point. *}

   267 text {* Every path has a unique end point. *}

   313   assumes "rpath r x xs x1"

   269   assumes "rpath r x xs x1"

   314   and "rpath r x xs x2"

   270   and "rpath r x xs x2"

   315   shows "x1 = x2"

   271   shows "x1 = x2"

   316   using assms

   272   using assms

   317   by (induct, auto)

   273   by (induct, auto)

   318 

   274 

   319 subsubsection {* Properites of @{text "edges_on"} *}

   283 subsubsection {* Properites of @{text "edges_on"} *}

   320 

   284 

   322   "edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R")

   353   "edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R")

   357 

   355 

   358 lemma edges_on_len:

   356 lemma edges_on_len:

   363 

   359 

   364 text {* Elimination of @{text "edges_on"} for non-empty path *}

   360 text {* Elimination of @{text "edges_on"} for non-empty path *}

   365 

   361 

   367   assumes "(a,b) \<in> edges_on (x#xs)"

   363   assumes "(a,b) \<in> edges_on (x#xs)"

   368   obtains (head)  xs' where "x = a" and "xs = b#xs'"

   364   obtains (head)  xs' where "x = a" and "xs = b#xs'"

   369       |  (tail)  "(a,b) \<in> edges_on xs"

   365       |  (tail)  "(a,b) \<in> edges_on xs"

   394 

   369 

   395 text {*

   370 text {*

   396   Every edges on the path is a graph edges:

   371   Every edges on the path is a graph edges:

   397 *}

   372 *}

   399   assumes "rpath r x xs y"

   375   assumes "rpath r x xs y"

   415 

   379 

   416 text {* @{text "edges_on"} is mono with respect to @{text "#"}-operation: *}

   380 text {* @{text "edges_on"} is mono with respect to @{text "#"}-operation: *}

   418    shows "edges_on xs \<subseteq> edges_on (x#xs)"

   382    shows "edges_on xs \<subseteq> edges_on (x#xs)"

   429 

   392 

   430 text {*

   393 text {*

   431   The following rule @{text "rpath_transfer"} is used to show 

   394   The following rule @{text "rpath_transfer"} is used to show 

   432   that one path is intact as long as all the edges on it are intact

   395   that one path is intact as long as all the edges on it are intact

   433   with the change of graph.

   396   with the change of graph.

   435   If @{text "x#xs"} is path in graph @{text "r1"} and 

   398   If @{text "x#xs"} is path in graph @{text "r1"} and 

   436   every edges along the path is also in @{text "r2"}, 

   399   every edges along the path is also in @{text "r2"}, 

   437   then @{text "x#xs"} is also a edge in graph @{text "r2"}:

   400   then @{text "x#xs"} is also a edge in graph @{text "r2"}:

   438 *}

   401 *}

   439 

   402 

   441   assumes "rpath r1 x xs y"

   404   assumes "rpath r1 x xs y"

   442   and "edges_on (x#xs) \<subseteq> r2"

   405   and "edges_on (x#xs) \<subseteq> r2"

   443   shows "rpath r2 x xs y"

   406   shows "rpath r2 x xs y"

   444   using assms

   407   using assms

   462   assumes "edges_on (a#xs@[b]) \<subseteq> r"

   411   assumes "edges_on (a#xs@[b]) \<subseteq> r"

   463   shows "rpath r a (xs@[b]) b"

   412   shows "rpath r a (xs@[b]) b"

   464   using assms

   413   using assms

   477 qed

   430 qed

   478 

   431 

   479 text {*

   432 text {*

   480   The following lemma extracts the path from @{text "x"} to @{text "y"}

   433   The following lemma extracts the path from @{text "x"} to @{text "y"}

   481   from proposition @{text "(x, y) \<in> r^*"}

   434   from proposition @{text "(x, y) \<in> r^*"}

   482 *}

   435 *}

   484   assumes "(x, y) \<in> r^*"

   438   assumes "(x, y) \<in> r^*"

   485   obtains xs where "rpath r x xs y"

   439   obtains xs where "rpath r x xs y"

   496 

   443 

   497 text {*

   444 text {*

   498   The following lemma uses the path @{text "xs"} from @{text "x"} to @{text "y"}

   445   The following lemma uses the path @{text "xs"} from @{text "x"} to @{text "y"}

   499   as a witness to show @{text "(x, y) \<in> r^*"}.

   446   as a witness to show @{text "(x, y) \<in> r^*"}.

   500 *}

   447 *}

   502   assumes "rpath r x xs y"

   449   assumes "rpath r x xs y"

   503   shows "(x, y) \<in> r^*"

   450   shows "(x, y) \<in> r^*"

   504 proof -

   451 proof -

   505   from iffD2[OF rtranclp_eq_rtrancl_path] and assms[unfolded rpath_def]

   452   from iffD2[OF rtranclp_eq_rtrancl_path] and assms[unfolded rpath_def]

   506   have "(pred_of r)\<^sup>*\<^sup>* x y" by metis

   453   have "(pred_of r)\<^sup>*\<^sup>* x y" by metis

   507   thus ?thesis by (simp add: pred_of_star star_2_pstar)

   454   thus ?thesis by (simp add: pred_of_star star_2_pstar)

   508 qed  

   455 qed  

   509 

   456 

   511   assumes "a \<in> subtree r1 a'"

   467   assumes "a \<in> subtree r1 a'"

   512   and "r1 \<subseteq> r2"

   468   and "r1 \<subseteq> r2"

   513   shows "a \<in> subtree r2 a'"

   469   shows "a \<in> subtree r2 a'"

   523   qed

   481   qed

   529   assumes "a \<notin> subtree r2 a'"

   493   assumes "a \<notin> subtree r2 a'"

   530   and "r1 \<subseteq> r2"

   494   and "r1 \<subseteq> r2"

   531   shows "a \<notin> subtree r1 a'"

   495   shows "a \<notin> subtree r1 a'"

   532   using assms and subtree_transfer by metis

   496   using assms and subtree_transfer by metis

   533 

   497 

   534 text {*

   498 text {*

   535   The following lemmas establishes a relation from paths in @{text "r"}

   499   The following lemmas establishes a relation from paths in @{text "r"}

   536   to @{text "r^+"} relation.

   500   to @{text "r^+"} relation.

   537 *}

   501 *}

   539   assumes "rpath r x xs y"

   503   assumes "rpath r x xs y"

   540   and "xs \<noteq> []"

   504   and "xs \<noteq> []"

   541   shows "(x, y) \<in> r^+"

   505   shows "(x, y) \<in> r^+"

   557   assumes "(x, y) \<in> r^+"

   510   assumes "(x, y) \<in> r^+"

   558   obtains xs where "rpath r x xs y" and "xs \<noteq> []"

   511   obtains xs where "rpath r x xs y" and "xs \<noteq> []"

   559 proof -

   512 proof -

   560   from assms

   513   from assms

   576 subsubsection {* Properties of @{text "subtree"} and @{term "ancestors"}*}

   518 subsubsection {* Properties of @{text "subtree"} and @{term "ancestors"}*}

   577 

   519 

   579   assumes "b \<in> ancestors r a"

   521   assumes "b \<in> ancestors r a"

   580   shows "a \<in> subtree r b"

   522   shows "a \<in> subtree r b"

   581   using assms by (auto simp:subtree_def ancestors_def)

   523   using assms by (auto simp:subtree_def ancestors_def)

   582 

   524 

   584   assumes "b \<in> ancestors r a"

   526   assumes "b \<in> ancestors r a"

   585   obtains "a \<in> Domain r" "b \<in> Range r"

   527   obtains "a \<in> Domain r" "b \<in> Range r"

   586   using assms 

   528   using assms 

   587   apply (unfold ancestors_def, simp)

   529   apply (unfold ancestors_def, simp)

   588   by (metis Domain.DomainI Range.intros trancl_domain trancl_range)

   530   by (metis Domain.DomainI Range.intros trancl_domain trancl_range)

   589 

   531 

   591   assumes "a \<in> subtree r b"

   533   assumes "a \<in> subtree r b"

   592   obtains "a = b"

   534   obtains "a = b"

   593       | "a \<noteq> b" and "b \<in> ancestors r a"

   535       | "a \<noteq> b" and "b \<in> ancestors r a"

   594 proof -

   536 proof -

   595   from assms have "(a, b) \<in> r^*" by (auto simp:subtree_def)

   537   from assms have "(a, b) \<in> r^*" by (auto simp:subtree_def)

   597   have " a = b \<or> a \<noteq> b \<and> (a, b) \<in> r\<^sup>+" .

   539   have " a = b \<or> a \<noteq> b \<and> (a, b) \<in> r\<^sup>+" .

   598   with that[unfolded ancestors_def] show ?thesis by auto

   540   with that[unfolded ancestors_def] show ?thesis by auto

   599 qed

   541 qed

   600 

   542 

   601 

   543 

   603   "subtree r x \<subseteq> Field r \<union> {x}"

   545   "subtree r x \<subseteq> Field r \<union> {x}"

   604 proof

   546 proof

   605   fix y

   547   fix y

   606   assume "y \<in> subtree r x"

   548   assume "y \<in> subtree r x"

   607   thus "y \<in> Field r \<union> {x}"

   549   thus "y \<in> Field r \<union> {x}"

   608   proof(cases rule:subtreeE)

   550   proof(cases rule:subtreeE)

   609     case 1

   551     case 1

   610     thus ?thesis by auto

   552     thus ?thesis by auto

   611   next

   553   next

   612     case 2

   554     case 2

   615   qed

   557   qed

   616 qed

   558 qed

   617 

   559 

   618 lemma subtree_ancestorsI:

   560 lemma subtree_ancestorsI:

   619   assumes "a \<in> subtree r b"

   561   assumes "a \<in> subtree r b"

   620   and "a \<noteq> b"

   562   and "a \<noteq> b"

   621   shows "b \<in> ancestors r a"

   563   shows "b \<in> ancestors r a"

   622   using assms

   564   using assms

   645 

   566 

   646 text {*

   567 text {*

   647   The following lemma characterizes the change of sub-tree of @{text "x"}

   568   The following lemma characterizes the change of sub-tree of @{text "x"}

   648   with the removal of an outside edge @{text "(a,b)"}. 

   569   with the removal of an outside edge @{text "(a,b)"}. 

   649 

   570 

   650   Note that, according to lemma @{thm edges_in_refutation}, the assumption

   571   Note that, according to lemma @{thm edges_in_refutation}, the assumption

   651   @{term "b \<notin> subtree r x"} amounts to saying @{text "(a, b)"} 

   572   @{term "b \<notin> subtree r x"} amounts to saying @{text "(a, b)"} 

   652   is outside the sub-tree of @{text "x"}.

   573   is outside the sub-tree of @{text "x"}.

   653 *}

   574 *}

   655     assumes "b \<notin> subtree r x" 

   576     assumes "b \<notin> subtree r x" 

   657 proof -

   578 proof -

   658   { fix c

   579   { fix c

   660     hence "(c, x) \<in> r^*" by (auto simp:subtree_def)

   581     hence "(c, x) \<in> r^*" by (auto simp:subtree_def)

   662     proof(rule star_rpath)

   583     proof(rule star_rpath)

   663       fix xs

   584       fix xs

   664       assume rp: "rpath r c xs x"

   585       assume rp: "rpath r c xs x"

   665       show ?thesis

   586       show ?thesis

   666       proof -

   587       proof -

   667         from rp

   588         from rp

   668         have "rpath  (r - {(a, b)}) c xs x"

   589         have "rpath  (r - {(a, b)}) c xs x"

   669         proof(rule rpath_transfer)

   590         proof(rule rpath_transfer)

   671           moreover have "(a, b) \<notin> edges_on (c#xs)"

   592           moreover have "(a, b) \<notin> edges_on (c#xs)"

   672           proof

   593           proof

   673             assume "(a, b) \<in> edges_on (c # xs)"

   594             assume "(a, b) \<in> edges_on (c # xs)"

   674             then obtain l1 l2 where h: "c#xs = l1@[a,b]@l2" by (auto simp:edges_on_def)

   595             then obtain l1 l2 where h: "c#xs = l1@[a,b]@l2" by (auto simp:edges_on_def)

   675             hence "tl (c#xs) = tl (l1@[a,b]@l2)" by simp

   596             hence "tl (c#xs) = tl (l1@[a,b]@l2)" by simp

   676             then obtain l1' where eq_xs_b: "xs = l1'@[b]@l2" by (cases l1, auto)

   597             then obtain l1' where eq_xs_b: "xs = l1'@[b]@l2" by (cases l1, auto)

   677             from rp[unfolded this]

   598             from rp[unfolded this]

   678             show False

   599             show False

   684           qed

   601           qed

   686         qed

   604         qed

   688       qed

   606       qed

   689     qed

   607     qed

   690   } moreover {

   608   } moreover {

   691     fix c

   609     fix c

   695   } ultimately show ?thesis by auto

   613   } ultimately show ?thesis by auto

   696 qed

   614 qed

   697 

   615 

   698 (* ddd *)

   616 (* ddd *)

   700     assumes "Range r' \<inter> subtree r x = {}" 

   618     assumes "Range r' \<inter> subtree r x = {}" 

   701     shows "subtree (r - r') x = (subtree r x)" 

   619     shows "subtree (r - r') x = (subtree r x)" 

   702 proof -

   620 proof -

   703   { fix c

   621   { fix c

   704     assume "c \<in> (subtree r x)"

   622     assume "c \<in> (subtree r x)"

   710       show ?thesis

   628       show ?thesis

   711       proof -

   629       proof -

   712         from rp

   630         from rp

   713         have "rpath  (r - r') c xs x"

   631         have "rpath  (r - r') c xs x"

   714         proof(rule rpath_transfer)

   632         proof(rule rpath_transfer)

   716           moreover {

   634           moreover {

   717               fix a b

   635               fix a b

   718               assume h: "(a, b) \<in> r'"

   636               assume h: "(a, b) \<in> r'"

   719               have "(a, b) \<notin> edges_on (c#xs)"

   637               have "(a, b) \<notin> edges_on (c#xs)"

   720               proof

   638               proof

   729                   from rpath_star[OF this]

   647                   from rpath_star[OF this]

   730                   have "b \<in> subtree r x" by (auto simp:subtree_def)

   648                   have "b \<in> subtree r x" by (auto simp:subtree_def)

   731                   with assms (1) and h show ?thesis by (auto)

   649                   with assms (1) and h show ?thesis by (auto)

   732                 qed

   650                 qed

   733              qed

   651              qed

   735         qed

   653         qed

   736         thus ?thesis by (rule rpath_star[elim_format], auto simp:subtree_def)

   654         thus ?thesis by (rule rpath_star[elim_format], auto simp:subtree_def)

   737       qed

   655       qed

   738     qed

   656     qed

   739   } moreover {

   657   } moreover {

   742     moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto)

   660     moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto)

   743     ultimately have "c \<in> (subtree r x)" by auto

   661     ultimately have "c \<in> (subtree r x)" by auto

   744   } ultimately show ?thesis by auto

   662   } ultimately show ?thesis by auto

   745 qed

   663 qed

   746 

   664 

   748     assumes "b \<in> subtree r x"

   666     assumes "b \<in> subtree r x"

   749     shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)" 

   667     shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)" 

   750     using assms by (auto simp:subtree_def rtrancl_insert)

   668     using assms by (auto simp:subtree_def rtrancl_insert)

   751 

   669 

   753     assumes "b \<notin> subtree r x"

   671     assumes "b \<notin> subtree r x"

   754     shows "subtree (r \<union> {(a, b)}) x = (subtree r x)" 

   672     shows "subtree (r \<union> {(a, b)}) x = (subtree r x)" 

   755     using assms

   673     using assms

   756     by (auto simp:subtree_def rtrancl_insert)

   674     by (auto simp:subtree_def rtrancl_insert)

   757 

   675 

   759   assumes "root r a"

   677   assumes "root r a"

   760   and "a \<notin> Domain r1"

   678   and "a \<notin> Domain r1"

   761   shows "root (r \<union> r1) a"

   679   shows "root (r \<union> r1) a"

   762 proof -

   681 proof -

   763   let ?r = "r \<union> r1"

   682   let ?r = "r \<union> r1"

   764   { fix a'

   683   { fix a'

   765     assume "a' \<in> ancestors ?r a"

   684     assume "a' \<in> ancestors ?r a"

   766     hence "(a, a') \<in> ?r^+" by (auto simp:ancestors_def)

   685     hence "(a, a') \<in> ?r^+" by (auto simp:ancestors_def)

   775     with assms(2) 

   694     with assms(2) 

   776     have False by (auto)

   695     have False by (auto)

   777   } thus ?thesis by (auto simp:root_def)

   696   } thus ?thesis by (auto simp:root_def)

   778 qed

   697 qed

   779 

   698 

   781   assumes "r1 \<subseteq> r2"

   700   assumes "r1 \<subseteq> r2"

   782   shows "ancestors r1 x \<subseteq> ancestors r2 x"

   701   shows "ancestors r1 x \<subseteq> ancestors r2 x"

   783 proof

   702 proof

   784  fix a

   703  fix a

   785  assume "a \<in> ancestors r1 x"

   704  assume "a \<in> ancestors r1 x"

   786  hence "(x, a) \<in> r1^+" by (auto simp:ancestors_def)

   705  hence "(x, a) \<in> r1^+" by (auto simp:ancestors_def)

   787  from plus_rpath[OF this] obtain xs where 

   706  from plus_rpath[OF this] obtain xs where 

   788     h: "rpath r1 x xs a" "xs \<noteq> []" .

   707     h: "rpath r1 x xs a" "xs \<noteq> []" .

   789  have "rpath r2 x xs a"

   708  have "rpath r2 x xs a"

   790  proof(rule rpath_transfer[OF h(1)])

   709  proof(rule rpath_transfer[OF h(1)])

   793  qed

   713  qed

   794  from rpath_plus[OF this h(2)]

   714  from rpath_plus[OF this h(2)]

   795  show "a \<in> ancestors r2 x" by (auto simp:ancestors_def)

   715  show "a \<in> ancestors r2 x" by (auto simp:ancestors_def)

   796 qed

   716 qed

   797 

   717 

   864       with assms show ?thesis by (auto simp:ancestors_def)

   784       with assms show ?thesis by (auto simp:ancestors_def)

   865     qed

   785     qed

   866   } ultimately show ?thesis by auto

   786   } ultimately show ?thesis by auto

   867 qed

   787 qed

   868 

   788 

   870   assumes h: "\<And> x'. x' \<noteq> x \<Longrightarrow> x \<notin> subtree r' x'"

   790   assumes h: "\<And> x'. x' \<noteq> x \<Longrightarrow> x \<notin> subtree r' x'"

   871   and "r' \<subseteq> r"

   791   and "r' \<subseteq> r"

   872   shows "root r' x"

   792   shows "root r' x"

   873 proof -

   793 proof -

   874   from acyclic_subset[OF acl assms(2)]

   794   from acyclic_subset[OF acl assms(2)]

   885     moreover from h1 have "x \<in> subtree r' x'" by (auto simp:subtree_def)

   805     moreover from h1 have "x \<in> subtree r' x'" by (auto simp:subtree_def)

   886     ultimately have False using h by auto

   806     ultimately have False using h by auto

   887   } thus ?thesis by (auto simp:root_def)

   807   } thus ?thesis by (auto simp:root_def)

   888 qed

   808 qed

   889 

   809 

   891   assumes "rpath r x xs1 x1"

   811   assumes "rpath r x xs1 x1"

   892   and "rpath r x xs2 x2"

   812   and "rpath r x xs2 x2"

   893   and "length xs1 \<le> length xs2"

   813   and "length xs1 \<le> length xs2"

   894   obtains xs3 where "xs2 = xs1 @ xs3"

   814   obtains xs3 where "xs2 = xs1 @ xs3"

   895 proof(cases "xs1 = []")

   815 proof(cases "xs1 = []")

   914           have lt_i': "?idx < length xs2" using lt_i and assms(3) by auto

   834           have lt_i': "?idx < length xs2" using lt_i and assms(3) by auto

   915           have lt_j: "?idx < j" using h1 by (cases j, auto)

   835           have lt_j: "?idx < j" using h1 by (cases j, auto)

   916           -- {* From thesis inequalities, a number of equations concerning @{text "xs1"}

   836           -- {* From thesis inequalities, a number of equations concerning @{text "xs1"}

   917                  and @{text "xs2"} are derived *}

   837                  and @{text "xs2"} are derived *}

   918           have eq_take: "take ?idx xs1 = take ?idx xs2"

   838           have eq_take: "take ?idx xs1 = take ?idx xs2"

   920           have eq_xs1: " xs1 = take ?idx xs1 @ xs1 ! (?idx) # drop (Suc (?idx)) xs1" 

   840           have eq_xs1: " xs1 = take ?idx xs1 @ xs1 ! (?idx) # drop (Suc (?idx)) xs1" 

   921             using id_take_nth_drop[OF lt_i] .

   841             using id_take_nth_drop[OF lt_i] .

   922           have eq_xs2: "xs2 = take ?idx xs2 @ xs2 ! (?idx) # drop (Suc (?idx)) xs2" 

   842           have eq_xs2: "xs2 = take ?idx xs2 @ xs2 ! (?idx) # drop (Suc (?idx)) xs2" 

   923               using id_take_nth_drop[OF lt_i'] .

   843               using id_take_nth_drop[OF lt_i'] .

   924           -- {* The branch point along the path is finally pinpointed *}

   844           -- {* The branch point along the path is finally pinpointed *}

   948               show ?thesis by (auto simp:pred_of_def)

   868               show ?thesis by (auto simp:pred_of_def)

   949             qed

   869             qed

   950             ultimately show ?thesis using neq_idx sgv[unfolded single_valued_def] by metis

   870             ultimately show ?thesis using neq_idx sgv[unfolded single_valued_def] by metis

   951         next

   871         next

   952            case False

   872            case False

   955            have "(e, xs1!?idx) \<in> r"

   874            have "(e, xs1!?idx) \<in> r"

   956            proof -

   875            proof -

   957             from eq_xs1[unfolded eq_es] 

   876             from eq_xs1[unfolded eq_es] 

   958             have "xs1 = es@[e, xs1!?idx]@drop (Suc ?idx) xs1" by simp

   877             have "xs1 = es@[e, xs1!?idx]@drop (Suc ?idx) xs1" by simp

   959             hence "(e, xs1!?idx) \<in> edges_on xs1" by (simp add:edges_on_def, metis)

   878             hence "(e, xs1!?idx) \<in> edges_on xs1" by (simp add:edges_on_def, metis)

   960             with rpath_edges_on[OF assms(1)] edges_on_Cons_mono[of xs1 x]

   879             with rpath_edges_on[OF assms(1)] edges_on_Cons_mono[of xs1 x]

   962            qed moreover have "(e, xs2!?idx) \<in> r"

   881            qed moreover have "(e, xs2!?idx) \<in> r"

   963            proof -

   882            proof -

   964             from eq_xs2[folded eq_take, unfolded eq_es]

   883             from eq_xs2[folded eq_take, unfolded eq_es]

   965             have "xs2 = es@[e, xs2!?idx]@drop (Suc ?idx) xs2" by simp

   884             have "xs2 = es@[e, xs2!?idx]@drop (Suc ?idx) xs2" by simp

   966             hence "(e, xs2!?idx) \<in> edges_on xs2" by (simp add:edges_on_def, metis)

   885             hence "(e, xs2!?idx) \<in> edges_on xs2" by (simp add:edges_on_def, metis)

   967             with rpath_edges_on[OF assms(2)] edges_on_Cons_mono[of xs2 x]

   886             with rpath_edges_on[OF assms(2)] edges_on_Cons_mono[of xs2 x]

   969            qed

   888            qed

   970            ultimately show ?thesis 

   889            ultimately show ?thesis 

   971               using sgv[unfolded single_valued_def] neq_idx by metis

   890               using sgv[unfolded single_valued_def] neq_idx by metis

   972         qed

   891         qed

   973        qed

   892        qed

  1066         from less_1 and False show "xs2 \<noteq> []" by simp

   985         from less_1 and False show "xs2 \<noteq> []" by simp

  1067       qed

   986       qed

  1068       with acl show ?thesis by (unfold acyclic_def, auto)

   987       with acl show ?thesis by (unfold acyclic_def, auto)

  1069     next 

   988     next 

  1070       case False

   989       case False

  1072       from assms(2)[unfolded less_1 this]

   991       from assms(2)[unfolded less_1 this]

  1073       have "rpath r x (es @ [e] @ xs3) y" by simp

   992       have "rpath r x (es @ [e] @ xs3) y" by simp

  1074       thus ?thesis

   993       thus ?thesis

  1075       proof(cases rule:rpath_appendE)

   994       proof(cases rule:rpath_appendE)

  1076         case 1

   995         case 1

  1127         from rp1[unfolded this] have "x = z" by auto

  1046         from rp1[unfolded this] have "x = z" by auto

  1128         from rp2[folded this] rpath_star ind[unfolded indep_def]

  1047         from rp2[folded this] rpath_star ind[unfolded indep_def]

  1129         show ?thesis by metis

  1048         show ?thesis by metis

  1130       next

  1049       next

  1131         case False

  1050         case False

  1133         from rp2[unfolded h this]

  1052         from rp2[unfolded h this]

  1134         have "rpath r z (es @ [e] @ xs3) y" by simp

  1053         have "rpath r z (es @ [e] @ xs3) y" by simp

  1135         thus ?thesis

  1054         thus ?thesis

  1136         proof(cases rule:rpath_appendE)

  1055         proof(cases rule:rpath_appendE)

  1137           case 1

  1056           case 1

  1202       let ?r' = "r - {(a, b)}" -- {* The reduced graph is abbreviated as @{text "?r'"} *}

  1121       let ?r' = "r - {(a, b)}" -- {* The reduced graph is abbreviated as @{text "?r'"} *}

  1203       from h have "(c, x) \<in> ?r'^*" by (auto simp:subtree_def)

  1122       from h have "(c, x) \<in> ?r'^*" by (auto simp:subtree_def)

  1204       -- {* Extract from the reduced graph the path @{text "xs"} from @{text "c"} to @{text "x"}. *}

  1123       -- {* Extract from the reduced graph the path @{text "xs"} from @{text "c"} to @{text "x"}. *}

  1205       then obtain xs where rp0: "rpath ?r' c xs x" by (rule star_rpath, auto)

  1124       then obtain xs where rp0: "rpath ?r' c xs x" by (rule star_rpath, auto)

  1206       -- {* It is easy to show @{text "xs"} is also a path in the original graph *}

  1125       -- {* It is easy to show @{text "xs"} is also a path in the original graph *}

  1212       -- {* @{text "xs"} is used as the witness to show that @{text "c"} 

  1128       -- {* @{text "xs"} is used as the witness to show that @{text "c"} 

  1213                    in the sub-tree of @{text "x"} in the original graph. *}

  1129                    in the sub-tree of @{text "x"} in the original graph. *}

  1214       hence "c \<in> subtree r x"

  1130       hence "c \<in> subtree r x"

  1215          by (rule rpath_star[elim_format], auto simp:subtree_def)

  1131          by (rule rpath_star[elim_format], auto simp:subtree_def)

  1216       -- {* The next step is to show that @{text "c"} can not be in the sub-tree of @{text "a"}

  1132       -- {* The next step is to show that @{text "c"} can not be in the sub-tree of @{text "a"}

  1253           -- {* It can be shown that @{term "(a,b)"} is on this fictional path. *}

  1169           -- {* It can be shown that @{term "(a,b)"} is on this fictional path. *}

  1254           have "(a, b) \<in> edges_on (c#xs)"

  1170           have "(a, b) \<in> edges_on (c#xs)"

  1255           proof(cases "xs1 = []")

  1171           proof(cases "xs1 = []")

  1256             case True

  1172             case True

  1257             from rp_c[unfolded this] have "rpath r c [] a" .

  1173             from rp_c[unfolded this] have "rpath r c [] a" .

  1259             hence "c#xs = a#xs" by simp

  1175             hence "c#xs = a#xs" by simp

  1260             from this and eq_xs have "c#xs = a # xs1 @ b # ys" by simp

  1176             from this and eq_xs have "c#xs = a # xs1 @ b # ys" by simp

  1261             from this[unfolded True] have "c#xs = []@[a,b]@ys" by simp

  1177             from this[unfolded True] have "c#xs = []@[a,b]@ys" by simp

  1262             thus ?thesis by (auto simp:edges_on_def)

  1178             thus ?thesis by (auto simp:edges_on_def)

  1263           next

  1179           next

  1267             from eq_xs[unfolded this] have "c#xs = (c#xs')@[a,b]@ys" by simp

  1183             from eq_xs[unfolded this] have "c#xs = (c#xs')@[a,b]@ys" by simp

  1268             thus ?thesis by (unfold edges_on_def, blast)

  1184             thus ?thesis by (unfold edges_on_def, blast)

  1269           qed

  1185           qed

  1270           -- {* It can also be shown that @{term "(a,b)"} is not on this fictional path. *}

  1186           -- {* It can also be shown that @{term "(a,b)"} is not on this fictional path. *}

  1271           moreover have "(a, b) \<notin> edges_on (c#xs)"

  1187           moreover have "(a, b) \<notin> edges_on (c#xs)"

  1273           -- {* Contradiction is thus derived. *}

  1189           -- {* Contradiction is thus derived. *}

  1274           ultimately show False by auto

  1190           ultimately show False by auto

  1275         qed

  1191         qed

  1276       qed

  1192       qed

  1277       ultimately show ?thesis by auto

  1193       ultimately show ?thesis by auto

  1347            inthe reduced graph. *}

  1263            inthe reduced graph. *}

  1348      from rpath_star[OF this] show ?thesis by (auto simp:subtree_def)

  1264      from rpath_star[OF this] show ?thesis by (auto simp:subtree_def)

  1349     qed

  1265     qed

  1350   } 

  1266   } 

  1351   -- {* The equality of sets is derived from the two directions just proved. *}

  1267   -- {* The equality of sets is derived from the two directions just proved. *}

  1353 qed 

  1269 qed 

  1354 

  1270 

  1355 lemma  set_del_rootI:

  1271 lemma  set_del_rootI:

  1356   assumes "r1 \<subseteq> r"

  1272   assumes "r1 \<subseteq> r"

  1357   and "a \<in> Domain r1"

  1273   and "a \<in> Domain r1"

  1459     hence "z \<in> ?L" 

  1375     hence "z \<in> ?L" 

  1460       by (unfold subtree_def, auto)

  1376       by (unfold subtree_def, auto)

  1461   } ultimately show ?thesis by auto

  1377   } ultimately show ?thesis by auto

  1462 qed

  1378 qed

  1463 

  1379 

  1464 

  1389 

  1465 lemma subtree_children:

  1390 lemma subtree_children:

  1501 

  1393 

  1502 context fsubtree 

  1394 context fsubtree 

  1503 begin

  1395 begin

  1504   

  1396   

  1505 lemma finite_subtree:

  1397 lemma finite_subtree:

  1682       apply (simp add:Suc relpow_add[symmetric])

  1574       apply (simp add:Suc relpow_add[symmetric])

  1683       by (unfold h, simp)

  1575       by (unfold h, simp)

  1684   qed

  1576   qed

  1685 qed simp

  1577 qed simp

  1686 

  1578 

  1688   assumes "r1 \<subseteq> r"

  1580   assumes "r1 \<subseteq> r"

  1689   and "r2 \<subseteq> r"

  1581   and "r2 \<subseteq> r"

  1690   shows "r1 O r2 \<subseteq> r ^^ (2::nat)"

  1582   shows "r1 O r2 \<subseteq> r ^^ (2::nat)"

  1691 proof -

  1583 proof -

  1692   { fix a b

  1584   { fix a b

  1696     with assms have "(a, e) \<in> r" "(e, b) \<in> r" by auto

  1588     with assms have "(a, e) \<in> r" "(e, b) \<in> r" by auto

  1697     hence "(a, b) \<in> r ^^ (Suc (Suc 0))" by auto

  1589     hence "(a, b) \<in> r ^^ (Suc (Suc 0))" by auto

  1698   } thus ?thesis by (auto simp:numeral_2_eq_2)

  1590   } thus ?thesis by (auto simp:numeral_2_eq_2)

  1699 qed

  1591 qed

  1700 

  1592 

  1702   assumes "acyclic r"

  1594   assumes "acyclic r"

  1703   and "r1 \<subseteq> r"

  1595   and "r1 \<subseteq> r"

  1704   and "r2 \<subseteq> r"

  1596   and "r2 \<subseteq> r"

  1705   shows "acyclic (r1 O r2)"

  1597   shows "acyclic (r1 O r2)"

  1706 proof -

  1598 proof -

  1722 

  1614 

  1723 lemma children_compose_unfold: 

  1615 lemma children_compose_unfold: 

  1724   "children (r1 O r2) x = \<Union> (children r1 ` (children r2 x))"

  1616   "children (r1 O r2) x = \<Union> (children r1 ` (children r2 x))"

  1725   by (auto simp:children_def)

  1617   by (auto simp:children_def)

  1726 

  1618 

  1728   assumes "fbranch r1"

  1620   assumes "fbranch r1"

  1729   and "fbranch r2"

  1621   and "fbranch r2"

  1730   shows "fbranch (r1 O r2)"

  1622   shows "fbranch (r1 O r2)"

  1731 proof -

  1623 proof -

  1732   {  fix x

  1624   {  fix x

  1756        qed

  1648        qed

  1757      qed

  1649      qed

  1758   } thus ?thesis by (unfold fbranch_def, auto)

  1650   } thus ?thesis by (unfold fbranch_def, auto)

  1759 qed

  1651 qed

  1760 

  1652 

  1762   assumes "finite r"

  1654   assumes "finite r"

  1763   shows "fbranch r"

  1655   shows "fbranch r"

  1764 proof -

  1656 proof -

  1765   { fix x 

  1657   { fix x 

  1766     assume "x \<in>Range r"

  1658     assume "x \<in>Range r"

  1772       thus ?thesis by (unfold children_def, simp)

  1664       thus ?thesis by (unfold children_def, simp)

  1773     qed

  1665     qed

  1774   } thus ?thesis by (auto simp:fbranch_def)

  1666   } thus ?thesis by (auto simp:fbranch_def)

  1775 qed

  1667 qed

  1776 

  1668 

  1778   assumes "fbranch r1"

  1670   assumes "fbranch r1"

  1779   and "r2 \<subseteq> r1"

  1671   and "r2 \<subseteq> r1"

  1780   shows "fbranch r2"

  1672   shows "fbranch r2"

  1781 proof -

  1673 proof -

  1782   { fix x

  1674   { fix x

  1790       show "children r2 x \<subseteq> children r1 x" by (auto simp:children_def)

  1682       show "children r2 x \<subseteq> children r1 x" by (auto simp:children_def)

  1791     qed

  1683     qed

  1792   } thus ?thesis by (auto simp:fbranch_def)

  1684   } thus ?thesis by (auto simp:fbranch_def)

  1793 qed

  1685 qed

  1794 

  1686 

  1796   shows "children r x \<subseteq> subtree r x"

  1688   shows "children r x \<subseteq> subtree r x"

  1797   by (auto simp:children_def subtree_def)

  1689   by (auto simp:children_def subtree_def)

  1798 

  1690 

  1800   assumes "x \<notin> Range r'"

  1692   assumes "x \<notin> Range r'"

  1801   shows "children (r \<union> r') x = children r x"

  1693   shows "children (r \<union> r') x = children r x"

  1802   using assms

  1694   using assms

  1803   by (auto simp:children_def)

  1695   by (auto simp:children_def)

  1804 

  1696 

  1806   assumes "wf r"

  1698   assumes "wf r"

  1807   obtains b where "(b, a) \<in> r^*" "\<forall> c. (c, b) \<notin> r"

  1699   obtains b where "(b, a) \<in> r^*" "\<forall> c. (c, b) \<notin> r"

  1808 proof -

  1700 proof -

  1809   from assms

  1701   from assms

  1810   have "\<exists> b. (b, a) \<in> r^* \<and> (\<forall> c. (c, b) \<notin> r)"

  1702   have "\<exists> b. (b, a) \<in> r^* \<and> (\<forall> c. (c, b) \<notin> r)"

  1826     qed

  1718     qed

  1827   qed

  1719   qed

  1828   with that show ?thesis by metis

  1720   with that show ?thesis by metis

  1829 qed

  1721 qed

  1830 

  1722 

  1832   assumes "wf r"

  1724   assumes "wf r"

  1833   and "a \<in> Range r"

  1725   and "a \<in> Range r"

  1834   obtains b where "(b, a) \<in> r^+" "\<forall> c. (c, b) \<notin> r"

  1726   obtains b where "(b, a) \<in> r^+" "\<forall> c. (c, b) \<notin> r"

  1835 proof -

  1727 proof -

  1836   from assms(2) obtain a' where h_a: "(a', a) \<in> r" by auto

  1728   from assms(2) obtain a' where h_a: "(a', a) \<in> r" by auto

  1841   moreover have "b \<noteq> a" using h_a h_b(2) by auto

  1733   moreover have "b \<noteq> a" using h_a h_b(2) by auto

  1842   ultimately have "(b, a) \<in> r\<^sup>+" by auto

  1734   ultimately have "(b, a) \<in> r\<^sup>+" by auto

  1843   with h_b(2) and that show ?thesis by metis

  1735   with h_b(2) and that show ?thesis by metis

  1844 qed

  1736 qed

  1845 

  1737 

  1846 end

  1755 end