1 theory RTree

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

     3 begin

     4 

     5 section {* A theory of relational trees *}

     6 

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

     8 inductive_cases path_consE [elim!]: "rtrancl_path r x (z#zs) y"

     9 

    10 subsection {* Definitions *}

    11 

    12 text {*

    13   In this theory, we are giving to give a notion of of `Relational Graph` and

    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

    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. 

    18 

    19   A `Relation Graph` @{text "r"} is said to be a `Relational Tree` if it is both

    20   {\em single valued} and {\em acyclic}. 

    21 *}

    22 

    23 text {*

    24   The following @{text "sgv"} specifies that relation @{text "r"} is {\em single valued}.

    25 *}

    26 locale sgv = 

    27   fixes r

    28   assumes sgv: "single_valued r"

    29 

    30 text {*

    31   The following @{text "rtree"} specifies that @{text "r"} is a 

    32   {\em Relational Tree}.

    33 *}

    34 locale rtree = sgv + 

    35   assumes acl: "acyclic r"

    36 

    37 text {* 

    38   The following two auxiliary functions @{text "rel_of"} and @{text "pred_of"} 

    39   transfer between the predicate and set representation of binary relations.

    40 *}

    41 

    42 definition "rel_of r = {(x, y) | x y. r x y}"

    43 

    44 definition "pred_of r = (\<lambda> x y. (x, y) \<in> r)"

    45 

    46 text {*

    47   To reason about {\em Relational Graph}, a notion of path is 

    48   needed, which is given by the following @{text "rpath"} (short 

    49   for `relational path`). 

    50   The path @{text "xs"} in proposition @{text "rpath r x xs y"} is 

    51   a path leading from @{text "x"} to @{text "y"}, which serves as a 

    52   witness of the fact @{text "(x, y) \<in> r^*"}. 

    53 

    54   @{text "rpath"}

    55   is simply a wrapper of the @{text "rtrancl_path"} defined in the imported 

    56   theory @{text "Transitive_Closure_Table"}, which defines 

    57   a notion of path for the predicate form of binary relations. 

    58 *}

    59 definition "rpath r x xs y = rtrancl_path (pred_of r) x xs y"

    60 

    61 text {*

    62   Given a path @{text "ps"}, @{text "edges_on ps"} is the 

    63   set of edges along the path, which is defined as follows:

    64 *}

    65 

    66 definition "edges_on ps = {(a,b) | a b. \<exists> xs ys. ps = xs@[a,b]@ys}"

    67 

    68 text {*

    69    The following @{text "indep"} defines a notion of independence. 

    70    Two nodes @{text "x"} and @{text "y"} are said to be independent

    71    (expressed as @{text "indep x y"}),  if neither one is reachable 

    72    from the other in relational graph @{text "r"}.

    73 *}

    74 definition "indep r x y = (((x, y) \<notin> r^*) \<and> ((y, x) \<notin> r^*))"

    75 

    76 text {*

    77   In relational tree @{text "r"}, the sub tree of node @{text "x"} is written

    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"}:

    80 *}

    81 

    82 definition "subtree r x = {y . (y, x) \<in> r^*}"

    83 

    84 text {*

    85   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.

    87 *}

    88 

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

    90 

    91 text {*

    92   The following lemma @{text "edges_in_meaning"} shows the intuitive meaning 

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

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

    95 *}

    96 lemma edges_in_meaning: 

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

    98 proof -

    99   { fix a b

   100     assume h: "(a, b) \<in> r" "b \<in> subtree r x"

   101     moreover have "a \<in> subtree r x"

   102     proof -

   103       from h(2)[unfolded subtree_def] have "(b, x) \<in> r^*" by simp

   104       with h(1) have "(a, x) \<in> r^*" by auto

   105       thus ?thesis by (auto simp:subtree_def)

   106     qed

   107     ultimately have "((a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x)" 

   108       by (auto)

   109   } thus ?thesis by (auto simp:edges_in_def)

   110 qed

   111 

   112 text {*

   113   The following lemma shows the means 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"}, 

   115   it is sufficient if @{text "b"} is.

   116 *}

   117 lemma edges_in_refutation:

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

   119   shows "(a, b) \<notin> edges_in r x"

   120   using assms by (unfold edges_in_def subtree_def, auto)

   121 

   122 subsection {* Auxiliary lemmas *}

   123 

   124 lemma index_minimize:

   125   assumes "P (i::nat)"

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

   127 proof -

   128   have "\<exists> j. P j \<and> (\<forall> k < j. \<not> P k)"

   129   using assms

   130   proof(induct i rule:less_induct)

   131     case (less t)

   132     show ?case

   133     proof(cases "\<forall> j < t. \<not> P j")

   134       case True

   135       with less (2) show ?thesis by blast

   136     next

   137       case False

   138       then obtain j where "j < t" "P j" by auto

   139       from less(1)[OF this]

   140       show ?thesis .

   141     qed

   142   qed 

   143   with that show ?thesis by metis

   144 qed

   145 

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

   147 

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

   149 

   150 text {* The following lemmas establish bijectivity of the two functions *}

   151 

   152 lemma pred_rel_eq: "pred_of (rel_of r) = r" by (auto simp:rel_of_def pred_of_def)

   153 

   154 lemma rel_pred_eq: "rel_of (pred_of r) = r" by (auto simp:rel_of_def pred_of_def)

   155 

   156 lemma rel_of_star: "rel_of (r^**) = (rel_of r)^*"

   157   by (unfold rel_of_def rtranclp_rtrancl_eq, auto)

   158 

   159 lemma pred_of_star: "pred_of (r^*) = (pred_of r)^**"

   160 proof -

   161   { fix x y

   162     have "pred_of (r^*) x y = (pred_of r)^** x y"

   163     by (unfold pred_of_def rtranclp_rtrancl_eq, auto)

   164   } thus ?thesis by auto

   165 qed

   166 

   167 lemma star_2_pstar: "(x, y) \<in> r^* = (pred_of (r^*)) x y"

   168   by (simp add: pred_of_def)

   169 

   170 subsubsection {* Properties of @{text "rpath"} *}

   171 

   172 text {* Induction rule for @{text "rpath"}: *}

   173 

   174 print_statement rtrancl_path.induct

   175 

   176 lemma rpath_induct [consumes 1, case_names rbase rstep, induct pred: rpath]:

   177   assumes "rpath r x1 x2 x3"

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

   180   shows "P x1 x2 x3"

   181   using assms[unfolded rpath_def]

   182   by (induct, auto simp:pred_of_def rpath_def)

   183 

   184 text {* Introduction rule for empty path *}

   185 lemma rbaseI [intro!]: 

   186   assumes "x = y"

   187   shows "rpath r x [] y"

   188   by  (unfold rpath_def assms, 

   189          rule Transitive_Closure_Table.rtrancl_path.base)

   190 

   191 text {* Introduction rule for non-empty path *}

   192 lemma rstepI [intro!]: 

   193   assumes "(x, y) \<in> r"

   194     and "rpath r y ys z"

   195   shows "rpath r x (y#ys) z" 

   196 proof(unfold rpath_def, rule Transitive_Closure_Table.rtrancl_path.step)

   197   from assms(1) show "pred_of r x y" by (auto simp:pred_of_def)

   198 next

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

   200   by (auto simp:pred_of_def rpath_def)

   201 qed

   202 

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

   204 lemma rpath_appendI [intro]: 

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

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

   207   using assms 

   208   by (unfold rpath_def, auto intro:rtrancl_path_trans)

   209 

   210 text {* Elimination rule for empty path *}

   211 

   212 lemma rpath_cases [cases pred:rpath]:

   213   assumes "rpath r a1 a2 a3"

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

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

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

   217   using assms [unfolded rpath_def]

   218   by (cases, auto simp:rpath_def pred_of_def)

   219 

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

   221   assumes "rpath r x [] y"

   222   obtains "y = x"

   223   using assms[unfolded rpath_def] by auto

   224 

   225 -- {* This is a auxiliary lemmas used only in the proof of @{text "rpath_nnl_lastE"} *}

   226 lemma rpath_nnl_last:

   227   assumes "rtrancl_path r x xs y"

   228   and "xs \<noteq> []"

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

   230 proof -

   231   from append_butlast_last_id[OF `xs \<noteq> []`, symmetric] 

   232   obtain xs' y' where eq_xs: "xs = (xs' @ y' # [])" by simp

   233   with assms(1)

   234   have "rtrancl_path r x ... y" by simp

   235   hence "y = y'" by (rule rtrancl_path_appendE, auto)

   236   with eq_xs have "xs = xs'@[y]" by simp

   237   from that[OF this] show ?thesis .

   238 qed

   239 

   240 text {*

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

   242 *}

   243 

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

   245   assumes "rpath r x (y # ys) x2"

   246   obtains (rstep) "(x, y) \<in> r" and "rpath r y ys x2"

   247   using assms[unfolded rpath_def]

   248   by (cases, auto simp:rpath_def pred_of_def)

   249 

   250 text {*

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

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

   253 *}

   254 lemma rpath_nnl_lastE: 

   255   assumes "rpath r x xs y"

   256   and "xs \<noteq> []"

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

   258   using assms[unfolded rpath_def]

   259   by (rule rpath_nnl_last, auto)

   260 

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

   262 

   263 lemma rpath_appendE:

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

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

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

   267   by auto

   268 

   269 lemma rpath_subE: 

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

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

   272   using assms

   273  by (elim rpath_appendE, auto)

   274 

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

   276 lemma rpath_dest_eq:

   277   assumes "rpath r x xs x1"

   278   and "rpath r x xs x2"

   279   shows "x1 = x2"

   280   using assms

   281   by (induct, auto)

   282 

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

   284 

   285 lemma edges_on_len:

   286   assumes "(a,b) \<in> edges_on l"

   287   shows "length l \<ge> 2"

   288   using assms

   289   by (unfold edges_on_def, auto)

   290 

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

   292 lemma edges_on_consE [elim, cases set:edges_on]:

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

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

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

   296 proof -

   297   from assms obtain l1 l2 

   298   where h: "(x#xs) = l1 @ [a,b] @ l2" by (unfold edges_on_def, blast)

   299   have "(\<exists> xs'. x = a \<and> xs = b#xs') \<or> ((a,b) \<in> edges_on xs)"

   300   proof(cases "l1")

   301     case Nil with h 

   302     show ?thesis by auto

   303   next

   304     case (Cons e el)

   305     from h[unfolded this] 

   306     have "xs = el @ [a,b] @ l2" by auto

   307     thus ?thesis 

   308       by (unfold edges_on_def, auto)

   309   qed

   310   thus ?thesis 

   311   proof

   312     assume "(\<exists>xs'. x = a \<and> xs = b # xs')"

   313     then obtain xs' where "x = a" "xs = b#xs'" by blast

   314     from that(1)[OF this] show ?thesis .

   315   next

   316     assume "(a, b) \<in> edges_on xs"

   317     from that(2)[OF this] show ?thesis .

   318   qed

   319 qed

   320 

   321 text {*

   322   Every edges on the path is a graph edges:

   323 *}

   324 lemma rpath_edges_on:

   325   assumes "rpath r x xs y"

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

   327   using assms

   328 proof(induct arbitrary:y)

   329   case (rbase x)

   330   thus ?case by (unfold edges_on_def, auto)

   331 next

   332   case (rstep x y ys z)

   333   show ?case

   334   proof -

   335     { fix a b

   336       assume "(a, b) \<in> edges_on (x # y # ys)"

   337       hence "(a, b) \<in> r" by (cases, insert rstep, auto)

   338     } thus ?thesis by auto

   339   qed

   340 qed

   341 

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

   343 lemma edges_on_Cons_mono:

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

   345 proof -

   346   { fix a b

   347     assume "(a, b) \<in> edges_on xs"

   348     then obtain l1 l2 where "xs = l1 @ [a,b] @ l2" 

   349       by (auto simp:edges_on_def)

   350     hence "x # xs = (x#l1) @ [a, b] @ l2" by auto

   351     hence "(a, b) \<in> edges_on (x#xs)" 

   352       by (unfold edges_on_def, blast)

   353   } thus ?thesis by auto

   354 qed

   355 

   356 text {*

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

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

   359   with the change of graph.

   360 

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

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

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

   364 *}

   365 

   366 lemma rpath_transfer:

   367   assumes "rpath r1 x xs y"

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

   369   shows "rpath r2 x xs y"

   370   using assms

   371 proof(induct)

   372   case (rstep x y ys z)

   373   show ?case 

   374   proof(rule rstepI)

   375     show "(x, y) \<in> r2"

   376     proof -

   377       have "(x, y) \<in> edges_on  (x # y # ys)"

   378           by (unfold edges_on_def, auto)

   379      with rstep(4) show ?thesis by auto

   380     qed

   381   next

   382     show "rpath r2 y ys z" 

   383      using rstep edges_on_Cons_mono[of "y#ys" "x"] by (auto)

   384   qed

   385 qed (unfold rpath_def, auto intro!:Transitive_Closure_Table.rtrancl_path.base)

   386 

   387 

   388 text {*

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

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

   391 *}

   392 lemma star_rpath:

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

   394   obtains xs where "rpath r x xs y"

   395 proof -

   396   have "\<exists> xs. rpath r x xs y"

   397   proof(unfold rpath_def, rule iffD1[OF rtranclp_eq_rtrancl_path])

   398     from assms

   399     show "(pred_of r)\<^sup>*\<^sup>* x y"

   400       apply (fold pred_of_star)

   401       by (auto simp:pred_of_def)

   402   qed

   403   from that and this show ?thesis by blast

   404 qed

   405 

   406 text {*

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

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

   409 *}

   410 lemma rpath_star: 

   411   assumes "rpath r x xs y"

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

   413 proof -

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

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

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

   417 qed

   418 

   419 text {*

   420   The following lemmas establishes a relation from pathes in @{text "r"}

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

   422 *}

   423 lemma rpath_plus: 

   424   assumes "rpath r x xs y"

   425   and "xs \<noteq> []"

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

   427 proof -

   428   from assms(2) obtain e es where "xs = e#es" by (cases xs, auto)

   429   from assms(1)[unfolded this]

   430   show ?thesis

   431   proof(cases)

   432     case rstep

   433     show ?thesis

   434     proof -

   435       from rpath_star[OF rstep(2)] have "(e, y) \<in> r\<^sup>*" .

   436       with rstep(1) show "(x, y) \<in> r^+" by auto

   437     qed

   438   qed

   439 qed

   440 

   441 subsubsection {* Properties of @{text "subtree"} *}

   442 

   443 text {*

   444   @{text "subtree"} is mono with respect to the underlying graph.

   445 *}

   446 lemma subtree_mono:

   447   assumes "r1 \<subseteq> r2"

   448   shows "subtree r1 x \<subseteq> subtree r2 x"

   449 proof

   450   fix c

   451   assume "c \<in> subtree r1 x"

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

   453   from star_rpath[OF this] obtain xs 

   454   where rp:"rpath r1 c xs x" by metis

   455   hence "rpath r2 c xs x"

   456   proof(rule rpath_transfer)

   457     from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r1" .

   458     with assms show "edges_on (c # xs) \<subseteq> r2" by auto

   459   qed

   460   thus "c \<in> subtree r2 x"

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

   462 qed

   463 

   464 text {*

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

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

   467 

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

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

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

   471 *}

   472 lemma subtree_del_outside: (* ddd *)

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

   474     shows "subtree (r - {(a, b)}) x = (subtree r x)" 

   475 proof -

   476   { fix c

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

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

   479     hence "c \<in> subtree (r - {(a, b)}) x"

   480     proof(rule star_rpath)

   481       fix xs

   482       assume rp: "rpath r c xs x"

   483       show ?thesis

   484       proof -

   485         from rp

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

   487         proof(rule rpath_transfer)

   488           from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r" .

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

   490           proof

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

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

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

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

   495             from rp[unfolded this]

   496             show False

   497             proof(rule rpath_appendE)

   498               assume "rpath r b l2 x"

   499               thus ?thesis

   500               by(rule rpath_star[elim_format], insert assms(1), auto simp:subtree_def)

   501             qed

   502           qed

   503           ultimately show "edges_on (c # xs) \<subseteq> r - {(a,b)}" by auto

   504         qed

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

   506       qed

   507     qed

   508   } moreover {

   509     fix c

   510     assume "c \<in> subtree (r - {(a, b)}) x"

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

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

   513   } ultimately show ?thesis by auto

   514 qed

   515 

   516 lemma subtree_insert_ext:

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

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

   519     using assms by (auto simp:subtree_def rtrancl_insert)

   520 

   521 lemma subtree_insert_next:

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

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

   524     using assms

   525     by (auto simp:subtree_def rtrancl_insert)

   526 

   527 subsubsection {* Properties about relational trees *}

   528 

   529 context rtree 

   530 begin

   531 

   532 lemma rpath_overlap_oneside: (* ddd *)

   533   assumes "rpath r x xs1 x1"

   534   and "rpath r x xs2 x2"

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

   536   obtains xs3 where "xs2 = xs1 @ xs3"

   537 proof(cases "xs1 = []")

   538   case True

   539   with that show ?thesis by auto

   540 next

   541   case False

   542   have "\<forall> i \<le> length xs1. take i xs1 = take i xs2"

   543   proof -

   544      { assume "\<not> (\<forall> i \<le> length xs1. take i xs1 = take i xs2)"

   545        then obtain i where "i \<le> length xs1 \<and> take i xs1 \<noteq> take i xs2" by auto

   546        from this(1) have "False"

   547        proof(rule index_minimize)

   548           fix j

   549           assume h1: "j \<le> length xs1 \<and> take j xs1 \<noteq> take j xs2"

   550           and h2: " \<forall>k<j. \<not> (k \<le> length xs1 \<and> take k xs1 \<noteq> take k xs2)"

   551           -- {* @{text "j - 1"} is the branch point between @{text "xs1"} and @{text "xs2"} *}

   552           let ?idx = "j - 1"

   553           -- {* A number of inequalities concerning @{text "j - 1"} are derived first *}

   554           have lt_i: "?idx < length xs1" using False h1 

   555             by (metis Suc_diff_1 le_neq_implies_less length_greater_0_conv lessI less_imp_diff_less)

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

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

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

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

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

   561             using h2[rule_format, OF lt_j] and h1 by auto

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

   563             using id_take_nth_drop[OF lt_i] .

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

   565               using id_take_nth_drop[OF lt_i'] .

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

   567           have neq_idx: "xs1!?idx \<noteq> xs2!?idx" 

   568           proof -

   569             have "take j xs1 = take ?idx xs1 @ [xs1 ! ?idx]"

   570                 using eq_xs1 Suc_diff_1 lt_i lt_j take_Suc_conv_app_nth by fastforce 

   571             moreover have eq_tk2: "take j xs2 = take ?idx xs2 @ [xs2 ! ?idx]"

   572                 using Suc_diff_1 lt_i' lt_j take_Suc_conv_app_nth by fastforce 

   573             ultimately show ?thesis using eq_take h1 by auto

   574           qed

   575           show ?thesis

   576           proof(cases " take (j - 1) xs1 = []")

   577             case True

   578             have "(x, xs1!?idx) \<in> r"

   579             proof -

   580                 from eq_xs1[unfolded True, simplified, symmetric] assms(1) 

   581                 have "rpath r x ( xs1 ! ?idx # drop (Suc ?idx) xs1) x1" by simp

   582                 from this[unfolded rpath_def]

   583                 show ?thesis by (auto simp:pred_of_def)

   584             qed

   585             moreover have "(x, xs2!?idx) \<in> r"

   586             proof -

   587               from eq_xs2[folded eq_take, unfolded True, simplified, symmetric] assms(2)

   588               have "rpath r x ( xs2 ! ?idx # drop (Suc ?idx) xs2) x2" by simp

   589               from this[unfolded rpath_def]

   590               show ?thesis by (auto simp:pred_of_def)

   591             qed

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

   593         next

   594            case False

   595            then obtain e es where eq_es: "take ?idx xs1 = es@[e]" 

   596             using rev_exhaust by blast 

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

   598            proof -

   599             from eq_xs1[unfolded eq_es] 

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

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

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

   603             show ?thesis by auto

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

   605            proof -

   606             from eq_xs2[folded eq_take, unfolded eq_es]

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

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

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

   610             show ?thesis by auto

   611            qed

   612            ultimately show ?thesis 

   613               using sgv[unfolded single_valued_def] neq_idx by metis

   614         qed

   615        qed

   616      } thus ?thesis by auto

   617   qed

   618   from this[rule_format, of "length xs1"]

   619   have "take (length xs1) xs1 = take (length xs1) xs2" by simp

   620   moreover have "xs2 = take (length xs1) xs2 @ drop (length xs1) xs2" by simp

   621   ultimately have "xs2 = xs1 @ drop (length xs1) xs2" by auto

   622   from that[OF this] show ?thesis .

   623 qed

   624 

   625 lemma rpath_overlap [consumes 2, cases pred:rpath]:

   626   assumes "rpath r x xs1 x1"

   627   and "rpath r x xs2 x2"

   628   obtains (less_1) xs3 where "xs2 = xs1 @ xs3"

   629      |    (less_2) xs3 where "xs1 = xs2 @ xs3"

   630 proof -

   631   have "length xs1 \<le> length xs2 \<or> length xs2 \<le> length xs1" by auto

   632   with assms rpath_overlap_oneside that show ?thesis by metis

   633 qed

   634 

   635 text {*

   636   As a corollary of @{thm "rpath_overlap_oneside"}, 

   637   the following two lemmas gives one important property of relation tree, 

   638   i.e. there is at most one path between any two nodes.

   639   Similar to the proof of @{thm rpath_overlap}, we starts with

   640   the one side version first.

   641 *}

   642 

   643 lemma rpath_unique_oneside:

   644   assumes "rpath r x xs1 y"

   645     and "rpath r x xs2 y"

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

   647   shows "xs1 = xs2"

   648 proof -

   649   from rpath_overlap_oneside[OF assms] 

   650   obtain xs3 where less_1: "xs2 = xs1 @ xs3" by blast

   651   show ?thesis

   652   proof(cases "xs3 = []") 

   653     case True

   654     from less_1[unfolded this] show ?thesis by simp

   655   next

   656     case False

   657     note FalseH = this

   658     show ?thesis

   659     proof(cases "xs1 = []")

   660       case True

   661       have "(x, x) \<in> r^+"

   662       proof(rule rpath_plus)

   663         from assms(1)[unfolded True] 

   664         have "y = x" by (cases rule:rpath_nilE, simp)

   665         from assms(2)[unfolded this] show "rpath r x xs2 x" .

   666       next

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

   668       qed

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

   670     next 

   671       case False

   672       then obtain e es where eq_xs1: "xs1 = es@[e]" using rev_exhaust by auto

   673       from assms(2)[unfolded less_1 this]

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

   675       thus ?thesis

   676       proof(cases rule:rpath_appendE)

   677         case 1

   678         from rpath_dest_eq [OF 1(1)[folded eq_xs1] assms(1)]

   679         have "e = y" .

   680         from rpath_plus [OF 1(2)[unfolded this] FalseH]

   681         have "(y, y) \<in> r^+" .

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

   683       qed

   684     qed

   685   qed

   686 qed

   687 

   688 text {*

   689   The following is the full version of path uniqueness.

   690 *}

   691 lemma rpath_unique:

   692   assumes "rpath r x xs1 y"

   693     and "rpath r x xs2 y"

   694   shows "xs1 = xs2"

   695 proof(cases "length xs1 \<le> length xs2")

   696    case True

   697    from rpath_unique_oneside[OF assms this] show ?thesis .

   698 next

   699   case False

   700   hence "length xs2 \<le> length xs1" by simp

   701   from rpath_unique_oneside[OF assms(2,1) this]

   702   show ?thesis by simp

   703 qed

   704 

   705 text {*

   706   The following lemma shows that the `independence` relation is symmetric.

   707   It is an obvious auxiliary lemma which will be used later. 

   708 *}

   709 lemma sym_indep: "indep r x y \<Longrightarrow> indep r y x"

   710   by (unfold indep_def, auto)

   711 

   712 text {*

   713   This is another `obvious` lemma about trees, which says trees rooted at 

   714   independent nodes are disjoint.

   715 *}

   716 lemma subtree_disjoint:

   717   assumes "indep r x y"

   718   shows "subtree r x \<inter> subtree r y = {}"

   719 proof -

   720   { fix z x y xs1 xs2 xs3

   721       assume ind: "indep r x y"

   722       and rp1: "rpath r z xs1 x"

   723       and rp2: "rpath r z xs2 y"

   724       and h: "xs2 = xs1 @ xs3"

   725       have False

   726       proof(cases "xs1 = []")

   727         case True

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

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

   730         show ?thesis by metis

   731       next

   732         case False

   733         then obtain e es where eq_xs1: "xs1 = es@[e]" using rev_exhaust by blast

   734         from rp2[unfolded h this]

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

   736         thus ?thesis

   737         proof(cases rule:rpath_appendE)

   738           case 1

   739           have "e = x" using 1(1)[folded eq_xs1] rp1 rpath_dest_eq by metis

   740           from rpath_star[OF 1(2)[unfolded this]] ind[unfolded indep_def]

   741           show ?thesis by auto

   742         qed

   743       qed

   744   } note my_rule = this

   745   { fix z

   746     assume h: "z \<in> subtree r x" "z \<in> subtree r y"

   747     from h(1) have "(z, x) \<in> r^*" by (unfold subtree_def, auto)

   748     then obtain xs1 where rp1: "rpath r z xs1 x" using star_rpath by metis

   749     from h(2) have "(z, y) \<in> r^*" by (unfold subtree_def, auto)

   750     then obtain xs2 where rp2: "rpath r z xs2 y" using star_rpath by metis

   751     from rp1 rp2

   752     have False

   753     by (cases, insert my_rule[OF sym_indep[OF assms(1)] rp2 rp1] 

   754                   my_rule[OF assms(1) rp1 rp2], auto)

   755   } thus ?thesis by auto

   756 qed

   757 

   758 text {*

   759   The following lemma @{text "subtree_del"} characterizes the change of sub-tree of 

   760   @{text "x"} with the removal of an inside edge @{text "(a, b)"}. 

   761   Note that, the case for the removal of an outside edge has already been dealt with

   762   in lemma @{text "subtree_del_outside"}). 

   763 

   764   This lemma is underpinned by the following two `obvious` facts:

   765   \begin{enumearte}

   766   \item

   767   In graph @{text "r"}, for an inside edge @{text "(a,b) \<in> edges_in r x"},  

   768   every node @{text "c"} in the sub-tree of @{text "a"} has a path

   769   which goes first from @{text "c"} to @{text "a"}, then through edge @{text "(a, b)"}, and 

   770   finally reaches @{text "x"}. By the uniqueness of path in a tree,

   771   all paths from sub-tree of @{text "a"} to @{text "x"} are such constructed, therefore 

   772   must go through @{text "(a, b)"}. The consequence is: with the removal of @{text "(a,b)"},

   773   all such paths will be broken. 

   774 

   775   \item

   776   On the other hand, all paths not originate from within the sub-tree of @{text "a"}

   777   will not be affected by the removal of edge @{text "(a, b)"}. 

   778   The reason is simple: if the path is affected by the removal, it must 

   779   contain @{text "(a, b)"}, then it must originate from within the sub-tree of @{text "a"}.

   780   \end{enumearte}

   781 *}

   782 

   783 lemma subtree_del_inside: (* ddd *)

   784     assumes "(a,b) \<in> edges_in r x"

   785     shows "subtree (r - {(a, b)}) x = (subtree r x) - subtree r a"

   786 proof -

   787   from assms have asm: "b \<in> subtree r x" "(a, b) \<in> r" by (auto simp:edges_in_def)

   788   -- {* The proof follows a common pattern to prove the equality of sets. *}

   789   { -- {* The `left to right` direction.

   790        *}

   791     fix c

   792     -- {* Assuming @{text "c"} is inside the sub-tree of @{text "x"} in the reduced graph *}

   793     assume h: "c \<in> subtree (r - {(a, b)}) x" 

   794     -- {* We are going to show that @{text "c"} can not be in the sub-tree of @{text "a"} in 

   795           the original graph. *}

   796     -- {* In other words, all nodes inside the sub-tree of @{text "a"} in the original 

   797           graph will be removed from the sub-tree of @{text "x"} in the reduced graph. *}

   798     -- {* The reason, as analyzed before, is that all paths from within the 

   799           sub-tree of @{text "a"} are broken with the removal of edge @{text "(a,b)"}.

   800        *}

   801     have "c \<in> (subtree r x) - subtree r a" 

   802     proof -

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

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

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

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

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

   808       hence rp1: "rpath r c xs x"

   809       proof(rule rpath_transfer)

   810           from rpath_edges_on[OF rp0] 

   811           show "edges_on (c # xs) \<subseteq> r" by auto

   812       qed

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

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

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

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

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

   818             in the original graph. *}

   819       -- {* We need to use the fact that all paths originate from within sub-tree of @{text "a"}

   820              are broken. *}

   821       moreover have "c \<notin> subtree r a"

   822       proof

   823         -- {* Proof by contradiction, suppose otherwise *}

   824         assume otherwise: "c \<in> subtree r a"

   825         -- {* Then there is a path in original graph leading from @{text "c"} to @{text "a"} *}

   826         obtain xs1 where rp_c: "rpath r c xs1 a" 

   827         proof -

   828           from otherwise have "(c, a) \<in> r^*" by (auto simp:subtree_def)

   829           thus ?thesis by (rule star_rpath, auto intro!:that)

   830         qed

   831         -- {* Starting from this path, we are going to construct a fictional 

   832                   path from @{text "c"} to @{text "x"}, which, as explained before,

   833               is broken, so that contradiction can be derived. *}

   834         -- {* First, there is a path from @{text "b"} to @{text "x"} *}

   835         obtain ys where rp_b: "rpath r b ys x" 

   836         proof -

   837           from asm have "(b, x) \<in> r^*" by (auto simp:subtree_def)

   838           thus ?thesis by (rule star_rpath, auto intro!:that)

   839         qed

   840         -- {* The paths @{text "xs1"} and @{text "ys"} can be 

   841                  tied together using @{text "(a,b)"} to form a path 

   842                from @{text "c"} to @{text "x"}: *}

   843         have "rpath r c (xs1 @ b # ys) x"

   844         proof -

   845           from rstepI[OF asm(2) rp_b] have "rpath r a (b # ys) x" .

   846           from rpath_appendI[OF rp_c this]

   847           show ?thesis .

   848         qed

   849         -- {* By the uniqueness of path between two nodes of a tree, we have: *}

   850         from rpath_unique[OF rp1 this] have eq_xs: "xs = xs1 @ b # ys" .

   851         -- {* Contradiction can be derived from from this fictional path . *}

   852         show False

   853         proof -

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

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

   856           proof(cases "xs1 = []")

   857             case True

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

   859             hence eq_c: "c = a" by (rule rpath_nilE, simp)

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

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

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

   863             thus ?thesis by (auto simp:edges_on_def)

   864           next

   865             case False

   866             from rpath_nnl_lastE[OF rp_c this]

   867             obtain xs' where "xs1 = xs'@[a]" by auto

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

   869             thus ?thesis by (unfold edges_on_def, blast)

   870           qed

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

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

   873               using rpath_edges_on[OF rp0] by auto

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

   875           ultimately show False by auto

   876         qed

   877       qed

   878       ultimately show ?thesis by auto

   879     qed

   880   } moreover {

   881     -- {* The `right to left` direction.

   882        *} 

   883      fix c

   884    -- {* Assuming that @{text "c"} is in the sub-tree of @{text "x"}, but

   885          outside of the sub-tree of @{text "a"} in the original graph, *}

   886    assume h: "c \<in> (subtree r x) - subtree r a"

   887    -- {* we need to show that in the reduced graph, @{text "c"} is still in 

   888          the sub-tree of @{text "x"}. *}

   889    have "c \<in> subtree (r - {(a, b)}) x"

   890    proof -

   891       -- {* The proof goes by showing that the path from @{text "c"} to @{text "x"}

   892             in the original graph is not affected by the removal of @{text "(a,b)"}.

   893          *}

   894       from h have "(c, x) \<in> r^*" by (unfold subtree_def, auto)

   895       -- {* Extract the path @{text "xs"} from @{text "c"} to @{text "x"} in the original graph. *}

   896       from star_rpath[OF this] obtain xs where rp: "rpath r c xs x" by auto

   897       -- {* Show that it is also a path in the reduced graph. *}

   898       hence "rpath (r - {(a, b)}) c xs x"

   899       -- {* The proof goes by using rule @{thm rpath_transfer} *} 

   900       proof(rule rpath_transfer)

   901         -- {* We need to show all edges on the path are still in the reduced graph. *}

   902         show "edges_on (c # xs) \<subseteq> r - {(a, b)}"

   903         proof -

   904           -- {* It is easy to show that all the edges are in the original graph. *}

   905           from rpath_edges_on [OF rp] have " edges_on (c # xs) \<subseteq> r" .

   906           -- {* The essential part is to show that @{text "(a, b)"} is not on the path. *}

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

   908           proof

   909             -- {* Proof by contradiction, suppose otherwise: *}

   910             assume otherwise: "(a, b) \<in> edges_on (c#xs)"

   911             -- {* Then @{text "(a, b)"} is in the middle of the path. 

   912                   with @{text "l1"} and @{text "l2"} be the nodes in 

   913                   the front and rear respectively. *}

   914               then obtain l1 l2 where eq_xs: 

   915                 "c#xs = l1 @ [a, b] @ l2" by (unfold edges_on_def, blast)

   916             -- {* From this, it can be shown that @{text "c"} is 

   917                       in the sub-tree of @{text "a"} *}

   918             have "c \<in> subtree r a" 

   919             proof(cases "l1 = []")

   920               case True

   921               -- {* If @{text "l1"} is null, it can be derived that @{text "c = a"}. *}

   922               with eq_xs have "c = a" by auto

   923               -- {* So, @{text "c"} is obviously in the sub-tree of @{text "a"}. *}

   924               thus ?thesis by (unfold subtree_def, auto)

   925             next

   926               case False

   927               -- {* When @{text "l1"} is not null, it must have a tail @{text "es"}: *}

   928               then obtain e es where "l1 = e#es" by (cases l1, auto)

   929               -- {* The relation of this tail with @{text "xs"} is derived: *}

   930               with eq_xs have "xs = es@[a,b]@l2" by auto

   931               -- {* From this, a path from @{text "c"} to @{text "a"} is made visible: *}

   932               from rp[unfolded this] have "rpath r c (es @ [a] @ (b#l2)) x" by simp

   933               thus ?thesis

   934               proof(cases rule:rpath_appendE)

   935                 -- {* The path from @{text "c"} to @{text "a"} is extraced 

   936                              using @{thm "rpath_appendE"}: *}

   937                 case 1

   938                 from rpath_star[OF this(1)] 

   939                 -- {* The extracted path servers as a witness that @{text "c"} is 

   940                           in the sub-tree of @{text "a"}: *}

   941                 show ?thesis by (simp add:subtree_def)

   942             qed

   943           qed with h show False by auto         

   944          qed ultimately show ?thesis by auto

   945        qed

   946      qed

   947      -- {* From , it is shown that @{text "c"} is in the sub-tree of @{text "x"}

   948            inthe reduced graph. *}

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

   950     qed

   951   } 

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

   953   ultimately show ?thesis by auto

   954 qed 

   955 

   956 end

   957 

   958 end