Retrofiting of:
CpsG.thy (the parallel copy of PIPBasics.thy),
ExtGG.thy (The paralell copy of Implemenation.thy),
PrioG.thy (The paralell copy of Correctness.thy)
has completed.
The next step is to overwite original copies with the paralell ones.
theory RTree
imports "~~/src/HOL/Library/Transitive_Closure_Table" Max
begin
section {* A theory of relational trees *}
inductive_cases path_nilE [elim!]: "rtrancl_path r x [] y"
inductive_cases path_consE [elim!]: "rtrancl_path r x (z#zs) y"
subsection {* Definitions *}
text {*
In this theory, we are going to give a notion of of `Relational Graph` and
its derived notion `Relational Tree`. Given a binary relation @{text "r"},
the `Relational Graph of @{text "r"}` is the graph, the edges of which
are those in @{text "r"}. In this way, any binary relation can be viewed
as a `Relational Graph`. Note, this notion of graph includes infinite graphs.
A `Relation Graph` @{text "r"} is said to be a `Relational Tree` if it is both
{\em single valued} and {\em acyclic}.
*}
text {*
The following @{text "sgv"} specifies that relation @{text "r"} is {\em single valued}.
*}
locale sgv =
fixes r
assumes sgv: "single_valued r"
text {*
The following @{text "rtree"} specifies that @{text "r"} is a
{\em Relational Tree}.
*}
locale rtree = sgv +
assumes acl: "acyclic r"
text {*
The following two auxiliary functions @{text "rel_of"} and @{text "pred_of"}
transfer between the predicate and set representation of binary relations.
*}
definition "rel_of r = {(x, y) | x y. r x y}"
definition "pred_of r = (\<lambda> x y. (x, y) \<in> r)"
text {*
To reason about {\em Relational Graph}, a notion of path is
needed, which is given by the following @{text "rpath"} (short
for `relational path`).
The path @{text "xs"} in proposition @{text "rpath r x xs y"} is
a path leading from @{text "x"} to @{text "y"}, which serves as a
witness of the fact @{text "(x, y) \<in> r^*"}.
@{text "rpath"}
is simply a wrapper of the @{text "rtrancl_path"} defined in the imported
theory @{text "Transitive_Closure_Table"}, which defines
a notion of path for the predicate form of binary relations.
*}
definition "rpath r x xs y = rtrancl_path (pred_of r) x xs y"
text {*
Given a path @{text "ps"}, @{text "edges_on ps"} is the
set of edges along the path, which is defined as follows:
*}
definition "edges_on ps = {(a,b) | a b. \<exists> xs ys. ps = xs@[a,b]@ys}"
text {*
The following @{text "indep"} defines a notion of independence.
Two nodes @{text "x"} and @{text "y"} are said to be independent
(expressed as @{text "indep x y"}), if neither one is reachable
from the other in relational graph @{text "r"}.
*}
definition "indep r x y = (((x, y) \<notin> r^*) \<and> ((y, x) \<notin> r^*))"
text {*
In relational tree @{text "r"}, the sub tree of node @{text "x"} is written
@{text "subtree r x"}, which is defined to be the set of nodes (including itself)
which can reach @{text "x"} by following some path in @{text "r"}:
*}
definition "subtree r x = {y . (y, x) \<in> r^*}"
definition "ancestors r x = {y. (x, y) \<in> r^+}"
definition "root r x = (ancestors r x = {})"
text {*
The following @{text "edge_in r x"} is the set of edges
contained in the sub-tree of @{text "x"}, with @{text "r"} as the underlying graph.
*}
definition "edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> b \<in> subtree r x}"
text {*
The following lemma @{text "edges_in_meaning"} shows the intuitive meaning
of `an edge @{text "(a, b)"} is in the sub-tree of @{text "x"}`,
i.e., both @{text "a"} and @{text "b"} are in the sub-tree.
*}
lemma edges_in_meaning:
"edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x}"
proof -
{ fix a b
assume h: "(a, b) \<in> r" "b \<in> subtree r x"
moreover have "a \<in> subtree r x"
proof -
from h(2)[unfolded subtree_def] have "(b, x) \<in> r^*" by simp
with h(1) have "(a, x) \<in> r^*" by auto
thus ?thesis by (auto simp:subtree_def)
qed
ultimately have "((a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x)"
by (auto)
} thus ?thesis by (auto simp:edges_in_def)
qed
text {*
The following lemma shows the meaning of @{term "edges_in"} from the other side,
which says: for the edge @{text "(a,b)"} to be outside of the sub-tree of @{text "x"},
it is sufficient to show that @{text "b"} is.
*}
lemma edges_in_refutation:
assumes "b \<notin> subtree r x"
shows "(a, b) \<notin> edges_in r x"
using assms by (unfold edges_in_def subtree_def, auto)
definition "children r x = {y. (y, x) \<in> r}"
locale fbranch =
fixes r
assumes fb: "\<forall> x \<in> Range r . finite (children r x)"
begin
lemma finite_children: "finite (children r x)"
proof(cases "children r x = {}")
case True
thus ?thesis by auto
next
case False
then obtain y where "(y, x) \<in> r" by (auto simp:children_def)
hence "x \<in> Range r" by auto
from fb[rule_format, OF this]
show ?thesis .
qed
end
locale fsubtree = fbranch +
assumes wf: "wf r"
(* ccc *)
subsection {* Auxiliary lemmas *}
lemma index_minimize:
assumes "P (i::nat)"
obtains j where "P j" and "\<forall> k < j. \<not> P k"
using assms
proof -
have "\<exists> j. P j \<and> (\<forall> k < j. \<not> P k)"
using assms
proof(induct i rule:less_induct)
case (less t)
show ?case
proof(cases "\<forall> j < t. \<not> P j")
case True
with less (2) show ?thesis by blast
next
case False
then obtain j where "j < t" "P j" by auto
from less(1)[OF this]
show ?thesis .
qed
qed
with that show ?thesis by metis
qed
subsection {* Properties of Relational Graphs and Relational Trees *}
subsubsection {* Properties of @{text "rel_of"} and @{text "pred_of"} *}
text {* The following lemmas establish bijectivity of the two functions *}
lemma pred_rel_eq: "pred_of (rel_of r) = r" by (auto simp:rel_of_def pred_of_def)
lemma rel_pred_eq: "rel_of (pred_of r) = r" by (auto simp:rel_of_def pred_of_def)
lemma rel_of_star: "rel_of (r^**) = (rel_of r)^*"
by (unfold rel_of_def rtranclp_rtrancl_eq, auto)
lemma pred_of_star: "pred_of (r^*) = (pred_of r)^**"
proof -
{ fix x y
have "pred_of (r^*) x y = (pred_of r)^** x y"
by (unfold pred_of_def rtranclp_rtrancl_eq, auto)
} thus ?thesis by auto
qed
lemma star_2_pstar: "(x, y) \<in> r^* = (pred_of (r^*)) x y"
by (simp add: pred_of_def)
subsubsection {* Properties of @{text "rpath"} *}
text {* Induction rule for @{text "rpath"}: *}
lemma rpath_induct [consumes 1, case_names rbase rstep, induct pred: rpath]:
assumes "rpath r x1 x2 x3"
and "\<And>x. P x [] x"
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"
shows "P x1 x2 x3"
using assms[unfolded rpath_def]
by (induct, auto simp:pred_of_def rpath_def)
lemma rpathE:
assumes "rpath r x xs y"
obtains (base) "y = x" "xs = []"
| (step) z zs where "(x, z) \<in> r" "rpath r z zs y" "xs = z#zs"
using assms
by (induct, auto)
text {* Introduction rule for empty path *}
lemma rbaseI [intro!]:
assumes "x = y"
shows "rpath r x [] y"
by (unfold rpath_def assms,
rule Transitive_Closure_Table.rtrancl_path.base)
text {* Introduction rule for non-empty path *}
lemma rstepI [intro!]:
assumes "(x, y) \<in> r"
and "rpath r y ys z"
shows "rpath r x (y#ys) z"
proof(unfold rpath_def, rule Transitive_Closure_Table.rtrancl_path.step)
from assms(1) show "pred_of r x y" by (auto simp:pred_of_def)
next
from assms(2) show "rtrancl_path (pred_of r) y ys z"
by (auto simp:pred_of_def rpath_def)
qed
text {* Introduction rule for @{text "@"}-path *}
lemma rpath_appendI [intro]:
assumes "rpath r x xs a" and "rpath r a ys y"
shows "rpath r x (xs @ ys) y"
using assms
by (unfold rpath_def, auto intro:rtrancl_path_trans)
text {* Elimination rule for empty path *}
lemma rpath_cases [cases pred:rpath]:
assumes "rpath r a1 a2 a3"
obtains (rbase) "a1 = a3" and "a2 = []"
| (rstep) y :: "'a" and ys :: "'a list"
where "(a1, y) \<in> r" and "a2 = y # ys" and "rpath r y ys a3"
using assms [unfolded rpath_def]
by (cases, auto simp:rpath_def pred_of_def)
lemma rpath_nilE [elim!, cases pred:rpath]:
assumes "rpath r x [] y"
obtains "y = x"
using assms[unfolded rpath_def] by auto
-- {* This is a auxiliary lemmas used only in the proof of @{text "rpath_nnl_lastE"} *}
lemma rpath_nnl_last:
assumes "rtrancl_path r x xs y"
and "xs \<noteq> []"
obtains xs' where "xs = xs'@[y]"
proof -
from append_butlast_last_id[OF `xs \<noteq> []`, symmetric]
obtain xs' y' where eq_xs: "xs = (xs' @ y' # [])" by simp
with assms(1)
have "rtrancl_path r x ... y" by simp
hence "y = y'" by (rule rtrancl_path_appendE, auto)
with eq_xs have "xs = xs'@[y]" by simp
from that[OF this] show ?thesis .
qed
text {*
Elimination rule for non-empty paths constructed with @{text "#"}.
*}
lemma rpath_ConsE [elim!, cases pred:rpath]:
assumes "rpath r x (y # ys) x2"
obtains (rstep) "(x, y) \<in> r" and "rpath r y ys x2"
using assms[unfolded rpath_def]
by (cases, auto simp:rpath_def pred_of_def)
text {*
Elimination rule for non-empty path, where the destination node
@{text "y"} is shown to be at the end of the path.
*}
lemma rpath_nnl_lastE:
assumes "rpath r x xs y"
and "xs \<noteq> []"
obtains xs' where "xs = xs'@[y]"
using assms[unfolded rpath_def]
by (rule rpath_nnl_last, auto)
text {* Other elimination rules of @{text "rpath"} *}
lemma rpath_appendE:
assumes "rpath r x (xs @ [a] @ ys) y"
obtains "rpath r x (xs @ [a]) a" and "rpath r a ys y"
using rtrancl_path_appendE[OF assms[unfolded rpath_def, simplified], folded rpath_def]
by auto
lemma rpath_subE:
assumes "rpath r x (xs @ [a] @ ys @ [b] @ zs) y"
obtains "rpath r x (xs @ [a]) a" and "rpath r a (ys @ [b]) b" and "rpath r b zs y"
using assms
by (elim rpath_appendE, auto)
text {* Every path has a unique end point. *}
lemma rpath_dest_eq:
assumes "rpath r x xs x1"
and "rpath r x xs x2"
shows "x1 = x2"
using assms
by (induct, auto)
subsubsection {* Properites of @{text "edges_on"} *}
lemma edges_on_unfold:
"edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R")
proof -
{ fix c d
assume "(c, d) \<in> ?L"
then obtain l1 l2 where h: "(a # b # xs) = l1 @ [c, d] @ l2"
by (auto simp:edges_on_def)
have "(c, d) \<in> ?R"
proof(cases "l1")
case Nil
with h have "(c, d) = (a, b)" by auto
thus ?thesis by auto
next
case (Cons e es)
from h[unfolded this] have "b#xs = es@[c, d]@l2" by auto
thus ?thesis by (auto simp:edges_on_def)
qed
} moreover
{ fix c d
assume "(c, d) \<in> ?R"
moreover have "(a, b) \<in> ?L"
proof -
have "(a # b # xs) = []@[a,b]@xs" by simp
hence "\<exists> l1 l2. (a # b # xs) = l1@[a,b]@l2" by auto
thus ?thesis by (unfold edges_on_def, simp)
qed
moreover {
assume "(c, d) \<in> edges_on (b#xs)"
then obtain l1 l2 where "b#xs = l1@[c, d]@l2" by (unfold edges_on_def, auto)
hence "a#b#xs = (a#l1)@[c,d]@l2" by simp
hence "\<exists> l1 l2. (a # b # xs) = l1@[c,d]@l2" by metis
hence "(c,d) \<in> ?L" by (unfold edges_on_def, simp)
}
ultimately have "(c, d) \<in> ?L" by auto
} ultimately show ?thesis by auto
qed
lemma edges_on_len:
assumes "(a,b) \<in> edges_on l"
shows "length l \<ge> 2"
using assms
by (unfold edges_on_def, auto)
text {* Elimination of @{text "edges_on"} for non-empty path *}
lemma edges_on_consE [elim, cases set:edges_on]:
assumes "(a,b) \<in> edges_on (x#xs)"
obtains (head) xs' where "x = a" and "xs = b#xs'"
| (tail) "(a,b) \<in> edges_on xs"
proof -
from assms obtain l1 l2
where h: "(x#xs) = l1 @ [a,b] @ l2" by (unfold edges_on_def, blast)
have "(\<exists> xs'. x = a \<and> xs = b#xs') \<or> ((a,b) \<in> edges_on xs)"
proof(cases "l1")
case Nil with h
show ?thesis by auto
next
case (Cons e el)
from h[unfolded this]
have "xs = el @ [a,b] @ l2" by auto
thus ?thesis
by (unfold edges_on_def, auto)
qed
thus ?thesis
proof
assume "(\<exists>xs'. x = a \<and> xs = b # xs')"
then obtain xs' where "x = a" "xs = b#xs'" by blast
from that(1)[OF this] show ?thesis .
next
assume "(a, b) \<in> edges_on xs"
from that(2)[OF this] show ?thesis .
qed
qed
text {*
Every edges on the path is a graph edges:
*}
lemma rpath_edges_on:
assumes "rpath r x xs y"
shows "(edges_on (x#xs)) \<subseteq> r"
using assms
proof(induct arbitrary:y)
case (rbase x)
thus ?case by (unfold edges_on_def, auto)
next
case (rstep x y ys z)
show ?case
proof -
{ fix a b
assume "(a, b) \<in> edges_on (x # y # ys)"
hence "(a, b) \<in> r" by (cases, insert rstep, auto)
} thus ?thesis by auto
qed
qed
text {* @{text "edges_on"} is mono with respect to @{text "#"}-operation: *}
lemma edges_on_Cons_mono:
shows "edges_on xs \<subseteq> edges_on (x#xs)"
proof -
{ fix a b
assume "(a, b) \<in> edges_on xs"
then obtain l1 l2 where "xs = l1 @ [a,b] @ l2"
by (auto simp:edges_on_def)
hence "x # xs = (x#l1) @ [a, b] @ l2" by auto
hence "(a, b) \<in> edges_on (x#xs)"
by (unfold edges_on_def, blast)
} thus ?thesis by auto
qed
text {*
The following rule @{text "rpath_transfer"} is used to show
that one path is intact as long as all the edges on it are intact
with the change of graph.
If @{text "x#xs"} is path in graph @{text "r1"} and
every edges along the path is also in @{text "r2"},
then @{text "x#xs"} is also a edge in graph @{text "r2"}:
*}
lemma rpath_transfer:
assumes "rpath r1 x xs y"
and "edges_on (x#xs) \<subseteq> r2"
shows "rpath r2 x xs y"
using assms
proof(induct)
case (rstep x y ys z)
show ?case
proof(rule rstepI)
show "(x, y) \<in> r2"
proof -
have "(x, y) \<in> edges_on (x # y # ys)"
by (unfold edges_on_def, auto)
with rstep(4) show ?thesis by auto
qed
next
show "rpath r2 y ys z"
using rstep edges_on_Cons_mono[of "y#ys" "x"] by (auto)
qed
qed (unfold rpath_def, auto intro!:Transitive_Closure_Table.rtrancl_path.base)
lemma edges_on_rpathI:
assumes "edges_on (a#xs@[b]) \<subseteq> r"
shows "rpath r a (xs@[b]) b"
using assms
proof(induct xs arbitrary: a b)
case Nil
moreover have "(a, b) \<in> edges_on (a # [] @ [b])"
by (unfold edges_on_def, auto)
ultimately have "(a, b) \<in> r" by auto
thus ?case by auto
next
case (Cons x xs a b)
from this(2) have "edges_on (x # xs @ [b]) \<subseteq> r" by (simp add:edges_on_unfold)
from Cons(1)[OF this] have " rpath r x (xs @ [b]) b" .
moreover from Cons(2) have "(a, x) \<in> r" by (auto simp:edges_on_unfold)
ultimately show ?case by (auto)
qed
text {*
The following lemma extracts the path from @{text "x"} to @{text "y"}
from proposition @{text "(x, y) \<in> r^*"}
*}
lemma star_rpath:
assumes "(x, y) \<in> r^*"
obtains xs where "rpath r x xs y"
proof -
have "\<exists> xs. rpath r x xs y"
proof(unfold rpath_def, rule iffD1[OF rtranclp_eq_rtrancl_path])
from assms
show "(pred_of r)\<^sup>*\<^sup>* x y"
apply (fold pred_of_star)
by (auto simp:pred_of_def)
qed
from that and this show ?thesis by blast
qed
text {*
The following lemma uses the path @{text "xs"} from @{text "x"} to @{text "y"}
as a witness to show @{text "(x, y) \<in> r^*"}.
*}
lemma rpath_star:
assumes "rpath r x xs y"
shows "(x, y) \<in> r^*"
proof -
from iffD2[OF rtranclp_eq_rtrancl_path] and assms[unfolded rpath_def]
have "(pred_of r)\<^sup>*\<^sup>* x y" by metis
thus ?thesis by (simp add: pred_of_star star_2_pstar)
qed
lemma subtree_transfer:
assumes "a \<in> subtree r1 a'"
and "r1 \<subseteq> r2"
shows "a \<in> subtree r2 a'"
proof -
from assms(1)[unfolded subtree_def]
have "(a, a') \<in> r1^*" by auto
from star_rpath[OF this]
obtain xs where rp: "rpath r1 a xs a'" by blast
hence "rpath r2 a xs a'"
proof(rule rpath_transfer)
from rpath_edges_on[OF rp] and assms(2)
show "edges_on (a # xs) \<subseteq> r2" by simp
qed
from rpath_star[OF this]
show ?thesis by (auto simp:subtree_def)
qed
lemma subtree_rev_transfer:
assumes "a \<notin> subtree r2 a'"
and "r1 \<subseteq> r2"
shows "a \<notin> subtree r1 a'"
using assms and subtree_transfer by metis
text {*
The following lemmas establishes a relation from paths in @{text "r"}
to @{text "r^+"} relation.
*}
lemma rpath_plus:
assumes "rpath r x xs y"
and "xs \<noteq> []"
shows "(x, y) \<in> r^+"
proof -
from assms(2) obtain e es where "xs = e#es" by (cases xs, auto)
from assms(1)[unfolded this]
show ?thesis
proof(cases)
case rstep
show ?thesis
proof -
from rpath_star[OF rstep(2)] have "(e, y) \<in> r\<^sup>*" .
with rstep(1) show "(x, y) \<in> r^+" by auto
qed
qed
qed
lemma plus_rpath:
assumes "(x, y) \<in> r^+"
obtains xs where "rpath r x xs y" and "xs \<noteq> []"
proof -
from assms
show ?thesis
proof(cases rule:converse_tranclE[consumes 1])
case 1
hence "rpath r x [y] y" by auto
from that[OF this] show ?thesis by auto
next
case (2 z)
from 2(2) have "(z, y) \<in> r^*" by auto
from star_rpath[OF this] obtain xs where "rpath r z xs y" by auto
from rstepI[OF 2(1) this]
have "rpath r x (z # xs) y" .
from that[OF this] show ?thesis by auto
qed
qed
subsubsection {* Properties of @{text "subtree"} and @{term "ancestors"}*}
lemma ancestors_subtreeI:
assumes "b \<in> ancestors r a"
shows "a \<in> subtree r b"
using assms by (auto simp:subtree_def ancestors_def)
lemma ancestors_Field:
assumes "b \<in> ancestors r a"
obtains "a \<in> Domain r" "b \<in> Range r"
using assms
apply (unfold ancestors_def, simp)
by (metis Domain.DomainI Range.intros trancl_domain trancl_range)
lemma subtreeE:
assumes "a \<in> subtree r b"
obtains "a = b"
| "a \<noteq> b" and "b \<in> ancestors r a"
proof -
from assms have "(a, b) \<in> r^*" by (auto simp:subtree_def)
from rtranclD[OF this]
have " a = b \<or> a \<noteq> b \<and> (a, b) \<in> r\<^sup>+" .
with that[unfolded ancestors_def] show ?thesis by auto
qed
lemma subtree_Field:
"subtree r x \<subseteq> Field r \<union> {x}"
proof
fix y
assume "y \<in> subtree r x"
thus "y \<in> Field r \<union> {x}"
proof(cases rule:subtreeE)
case 1
thus ?thesis by auto
next
case 2
thus ?thesis apply (auto simp:ancestors_def)
using Field_def tranclD by fastforce
qed
qed
lemma subtree_ancestorsI:
assumes "a \<in> subtree r b"
and "a \<noteq> b"
shows "b \<in> ancestors r a"
using assms
by (auto elim!:subtreeE)
text {*
@{text "subtree"} is mono with respect to the underlying graph.
*}
lemma subtree_mono:
assumes "r1 \<subseteq> r2"
shows "subtree r1 x \<subseteq> subtree r2 x"
proof
fix c
assume "c \<in> subtree r1 x"
hence "(c, x) \<in> r1^*" by (auto simp:subtree_def)
from star_rpath[OF this] obtain xs
where rp:"rpath r1 c xs x" by metis
hence "rpath r2 c xs x"
proof(rule rpath_transfer)
from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r1" .
with assms show "edges_on (c # xs) \<subseteq> r2" by auto
qed
thus "c \<in> subtree r2 x"
by (rule rpath_star[elim_format], auto simp:subtree_def)
qed
text {*
The following lemma characterizes the change of sub-tree of @{text "x"}
with the removal of an outside edge @{text "(a,b)"}.
Note that, according to lemma @{thm edges_in_refutation}, the assumption
@{term "b \<notin> subtree r x"} amounts to saying @{text "(a, b)"}
is outside the sub-tree of @{text "x"}.
*}
lemma subtree_del_outside: (* ddd *)
assumes "b \<notin> subtree r x"
shows "subtree (r - {(a, b)}) x = (subtree r x)"
proof -
{ fix c
assume "c \<in> (subtree r x)"
hence "(c, x) \<in> r^*" by (auto simp:subtree_def)
hence "c \<in> subtree (r - {(a, b)}) x"
proof(rule star_rpath)
fix xs
assume rp: "rpath r c xs x"
show ?thesis
proof -
from rp
have "rpath (r - {(a, b)}) c xs x"
proof(rule rpath_transfer)
from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r" .
moreover have "(a, b) \<notin> edges_on (c#xs)"
proof
assume "(a, b) \<in> edges_on (c # xs)"
then obtain l1 l2 where h: "c#xs = l1@[a,b]@l2" by (auto simp:edges_on_def)
hence "tl (c#xs) = tl (l1@[a,b]@l2)" by simp
then obtain l1' where eq_xs_b: "xs = l1'@[b]@l2" by (cases l1, auto)
from rp[unfolded this]
show False
proof(rule rpath_appendE)
assume "rpath r b l2 x"
thus ?thesis
by(rule rpath_star[elim_format], insert assms(1), auto simp:subtree_def)
qed
qed
ultimately show "edges_on (c # xs) \<subseteq> r - {(a,b)}" by auto
qed
thus ?thesis by (rule rpath_star[elim_format], auto simp:subtree_def)
qed
qed
} moreover {
fix c
assume "c \<in> subtree (r - {(a, b)}) x"
moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto)
ultimately have "c \<in> (subtree r x)" by auto
} ultimately show ?thesis by auto
qed
(* ddd *)
lemma subset_del_subtree_outside: (* ddd *)
assumes "Range r' \<inter> subtree r x = {}"
shows "subtree (r - r') x = (subtree r x)"
proof -
{ fix c
assume "c \<in> (subtree r x)"
hence "(c, x) \<in> r^*" by (auto simp:subtree_def)
hence "c \<in> subtree (r - r') x"
proof(rule star_rpath)
fix xs
assume rp: "rpath r c xs x"
show ?thesis
proof -
from rp
have "rpath (r - r') c xs x"
proof(rule rpath_transfer)
from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r" .
moreover {
fix a b
assume h: "(a, b) \<in> r'"
have "(a, b) \<notin> edges_on (c#xs)"
proof
assume "(a, b) \<in> edges_on (c # xs)"
then obtain l1 l2 where "c#xs = (l1@[a])@[b]@l2" by (auto simp:edges_on_def)
hence "tl (c#xs) = tl (l1@[a,b]@l2)" by simp
then obtain l1' where eq_xs_b: "xs = l1'@[b]@l2" by (cases l1, auto)
from rp[unfolded this]
show False
proof(rule rpath_appendE)
assume "rpath r b l2 x"
from rpath_star[OF this]
have "b \<in> subtree r x" by (auto simp:subtree_def)
with assms (1) and h show ?thesis by (auto)
qed
qed
} ultimately show "edges_on (c # xs) \<subseteq> r - r'" by auto
qed
thus ?thesis by (rule rpath_star[elim_format], auto simp:subtree_def)
qed
qed
} moreover {
fix c
assume "c \<in> subtree (r - r') x"
moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto)
ultimately have "c \<in> (subtree r x)" by auto
} ultimately show ?thesis by auto
qed
lemma subtree_insert_ext:
assumes "b \<in> subtree r x"
shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)"
using assms by (auto simp:subtree_def rtrancl_insert)
lemma subtree_insert_next:
assumes "b \<notin> subtree r x"
shows "subtree (r \<union> {(a, b)}) x = (subtree r x)"
using assms
by (auto simp:subtree_def rtrancl_insert)
lemma set_add_rootI:
assumes "root r a"
and "a \<notin> Domain r1"
shows "root (r \<union> r1) a"
proof -
let ?r = "r \<union> r1"
{ fix a'
assume "a' \<in> ancestors ?r a"
hence "(a, a') \<in> ?r^+" by (auto simp:ancestors_def)
from tranclD[OF this] obtain z where "(a, z) \<in> ?r" by auto
moreover have "(a, z) \<notin> r"
proof
assume "(a, z) \<in> r"
with assms(1) show False
by (auto simp:root_def ancestors_def)
qed
ultimately have "(a, z) \<in> r1" by auto
with assms(2)
have False by (auto)
} thus ?thesis by (auto simp:root_def)
qed
lemma ancestors_mono:
assumes "r1 \<subseteq> r2"
shows "ancestors r1 x \<subseteq> ancestors r2 x"
proof
fix a
assume "a \<in> ancestors r1 x"
hence "(x, a) \<in> r1^+" by (auto simp:ancestors_def)
from plus_rpath[OF this] obtain xs where
h: "rpath r1 x xs a" "xs \<noteq> []" .
have "rpath r2 x xs a"
proof(rule rpath_transfer[OF h(1)])
from rpath_edges_on[OF h(1)] and assms
show "edges_on (x # xs) \<subseteq> r2" by auto
qed
from rpath_plus[OF this h(2)]
show "a \<in> ancestors r2 x" by (auto simp:ancestors_def)
qed
lemma subtree_refute:
assumes "x \<notin> ancestors r y"
and "x \<noteq> y"
shows "y \<notin> subtree r x"
proof
assume "y \<in> subtree r x"
thus False
by(elim subtreeE, insert assms, auto)
qed
subsubsection {* Properties about relational trees *}
context rtree
begin
lemma ancestors_headE:
assumes "c \<in> ancestors r a"
assumes "(a, b) \<in> r"
obtains "b = c"
| "c \<in> ancestors r b"
proof -
from assms(1)
have "(a, c) \<in> r^+" by (auto simp:ancestors_def)
hence "b = c \<or> c \<in> ancestors r b"
proof(cases rule:converse_tranclE[consumes 1])
case 1
with assms(2) and sgv have "b = c" by (auto simp:single_valued_def)
thus ?thesis by auto
next
case (2 y)
from 2(1) and assms(2) and sgv have "y = b" by (auto simp:single_valued_def)
from 2(2)[unfolded this] have "c \<in> ancestors r b" by (auto simp:ancestors_def)
thus ?thesis by auto
qed
with that show ?thesis by metis
qed
lemma ancestors_accum:
assumes "(a, b) \<in> r"
shows "ancestors r a = ancestors r b \<union> {b}"
proof -
{ fix c
assume "c \<in> ancestors r a"
hence "(a, c) \<in> r^+" by (auto simp:ancestors_def)
hence "c \<in> ancestors r b \<union> {b}"
proof(cases rule:converse_tranclE[consumes 1])
case 1
with sgv assms have "c = b" by (unfold single_valued_def, auto)
thus ?thesis by auto
next
case (2 c')
with sgv assms have "c' = b" by (unfold single_valued_def, auto)
from 2(2)[unfolded this]
show ?thesis by (auto simp:ancestors_def)
qed
} moreover {
fix c
assume "c \<in> ancestors r b \<union> {b}"
hence "c = b \<or> c \<in> ancestors r b" by auto
hence "c \<in> ancestors r a"
proof
assume "c = b"
from assms[folded this]
show ?thesis by (auto simp:ancestors_def)
next
assume "c \<in> ancestors r b"
with assms show ?thesis by (auto simp:ancestors_def)
qed
} ultimately show ?thesis by auto
qed
lemma rootI:
assumes h: "\<And> x'. x' \<noteq> x \<Longrightarrow> x \<notin> subtree r' x'"
and "r' \<subseteq> r"
shows "root r' x"
proof -
from acyclic_subset[OF acl assms(2)]
have acl': "acyclic r'" .
{ fix x'
assume "x' \<in> ancestors r' x"
hence h1: "(x, x') \<in> r'^+" by (auto simp:ancestors_def)
have "x' \<noteq> x"
proof
assume eq_x: "x' = x"
from h1[unfolded this] and acl'
show False by (auto simp:acyclic_def)
qed
moreover from h1 have "x \<in> subtree r' x'" by (auto simp:subtree_def)
ultimately have False using h by auto
} thus ?thesis by (auto simp:root_def)
qed
lemma rpath_overlap_oneside: (* ddd *)
assumes "rpath r x xs1 x1"
and "rpath r x xs2 x2"
and "length xs1 \<le> length xs2"
obtains xs3 where "xs2 = xs1 @ xs3"
proof(cases "xs1 = []")
case True
with that show ?thesis by auto
next
case False
have "\<forall> i \<le> length xs1. take i xs1 = take i xs2"
proof -
{ assume "\<not> (\<forall> i \<le> length xs1. take i xs1 = take i xs2)"
then obtain i where "i \<le> length xs1 \<and> take i xs1 \<noteq> take i xs2" by auto
from this(1) have "False"
proof(rule index_minimize)
fix j
assume h1: "j \<le> length xs1 \<and> take j xs1 \<noteq> take j xs2"
and h2: " \<forall>k<j. \<not> (k \<le> length xs1 \<and> take k xs1 \<noteq> take k xs2)"
-- {* @{text "j - 1"} is the branch point between @{text "xs1"} and @{text "xs2"} *}
let ?idx = "j - 1"
-- {* A number of inequalities concerning @{text "j - 1"} are derived first *}
have lt_i: "?idx < length xs1" using False h1
by (metis Suc_diff_1 le_neq_implies_less length_greater_0_conv lessI less_imp_diff_less)
have lt_i': "?idx < length xs2" using lt_i and assms(3) by auto
have lt_j: "?idx < j" using h1 by (cases j, auto)
-- {* From thesis inequalities, a number of equations concerning @{text "xs1"}
and @{text "xs2"} are derived *}
have eq_take: "take ?idx xs1 = take ?idx xs2"
using h2[rule_format, OF lt_j] and h1 by auto
have eq_xs1: " xs1 = take ?idx xs1 @ xs1 ! (?idx) # drop (Suc (?idx)) xs1"
using id_take_nth_drop[OF lt_i] .
have eq_xs2: "xs2 = take ?idx xs2 @ xs2 ! (?idx) # drop (Suc (?idx)) xs2"
using id_take_nth_drop[OF lt_i'] .
-- {* The branch point along the path is finally pinpointed *}
have neq_idx: "xs1!?idx \<noteq> xs2!?idx"
proof -
have "take j xs1 = take ?idx xs1 @ [xs1 ! ?idx]"
using eq_xs1 Suc_diff_1 lt_i lt_j take_Suc_conv_app_nth by fastforce
moreover have eq_tk2: "take j xs2 = take ?idx xs2 @ [xs2 ! ?idx]"
using Suc_diff_1 lt_i' lt_j take_Suc_conv_app_nth by fastforce
ultimately show ?thesis using eq_take h1 by auto
qed
show ?thesis
proof(cases " take (j - 1) xs1 = []")
case True
have "(x, xs1!?idx) \<in> r"
proof -
from eq_xs1[unfolded True, simplified, symmetric] assms(1)
have "rpath r x ( xs1 ! ?idx # drop (Suc ?idx) xs1) x1" by simp
from this[unfolded rpath_def]
show ?thesis by (auto simp:pred_of_def)
qed
moreover have "(x, xs2!?idx) \<in> r"
proof -
from eq_xs2[folded eq_take, unfolded True, simplified, symmetric] assms(2)
have "rpath r x ( xs2 ! ?idx # drop (Suc ?idx) xs2) x2" by simp
from this[unfolded rpath_def]
show ?thesis by (auto simp:pred_of_def)
qed
ultimately show ?thesis using neq_idx sgv[unfolded single_valued_def] by metis
next
case False
then obtain e es where eq_es: "take ?idx xs1 = es@[e]"
using rev_exhaust by blast
have "(e, xs1!?idx) \<in> r"
proof -
from eq_xs1[unfolded eq_es]
have "xs1 = es@[e, xs1!?idx]@drop (Suc ?idx) xs1" by simp
hence "(e, xs1!?idx) \<in> edges_on xs1" by (simp add:edges_on_def, metis)
with rpath_edges_on[OF assms(1)] edges_on_Cons_mono[of xs1 x]
show ?thesis by auto
qed moreover have "(e, xs2!?idx) \<in> r"
proof -
from eq_xs2[folded eq_take, unfolded eq_es]
have "xs2 = es@[e, xs2!?idx]@drop (Suc ?idx) xs2" by simp
hence "(e, xs2!?idx) \<in> edges_on xs2" by (simp add:edges_on_def, metis)
with rpath_edges_on[OF assms(2)] edges_on_Cons_mono[of xs2 x]
show ?thesis by auto
qed
ultimately show ?thesis
using sgv[unfolded single_valued_def] neq_idx by metis
qed
qed
} thus ?thesis by auto
qed
from this[rule_format, of "length xs1"]
have "take (length xs1) xs1 = take (length xs1) xs2" by simp
moreover have "xs2 = take (length xs1) xs2 @ drop (length xs1) xs2" by simp
ultimately have "xs2 = xs1 @ drop (length xs1) xs2" by auto
from that[OF this] show ?thesis .
qed
lemma rpath_overlap_oneside':
assumes "rpath r x xs1 x1"
and "rpath r x xs2 x2"
and "length xs1 \<le> length xs2"
obtains xs3 where
"xs2 = xs1 @ xs3" "rpath r x xs1 x1" "rpath r x1 xs3 x2"
proof -
from rpath_overlap_oneside[OF assms]
obtain xs3 where eq_xs: "xs2 = xs1 @ xs3" by auto
show ?thesis
proof(cases "xs1 = []")
case True
from rpath_nilE[OF assms(1)[unfolded this]]
have eq_x1: "x1 = x" .
have "xs2 = xs3" using True eq_xs by simp
from that[OF eq_xs assms(1) assms(2)[folded eq_x1, unfolded this]]
show ?thesis .
next
case False
from rpath_nnl_lastE[OF assms(1) False]
obtain xs' where eq_xs1: "xs1 = xs'@[x1]" by auto
from assms(2)[unfolded eq_xs this]
have "rpath r x (xs' @ [x1] @ xs3) x2" by simp
from rpath_appendE[OF this]
have "rpath r x (xs' @ [x1]) x1" "rpath r x1 xs3 x2" by auto
from that [OF eq_xs this(1)[folded eq_xs1] this(2)]
show ?thesis .
qed
qed
lemma rpath_overlap [consumes 2, cases pred:rpath]:
assumes "rpath r x xs1 x1"
and "rpath r x xs2 x2"
obtains (less_1) xs3 where "xs2 = xs1 @ xs3"
| (less_2) xs3 where "xs1 = xs2 @ xs3"
proof -
have "length xs1 \<le> length xs2 \<or> length xs2 \<le> length xs1" by auto
with assms rpath_overlap_oneside that show ?thesis by metis
qed
lemma rpath_overlap' [consumes 2, cases pred:rpath]:
assumes "rpath r x xs1 x1"
and "rpath r x xs2 x2"
obtains (less_1) xs3 where "xs2 = xs1 @ xs3" "rpath r x xs1 x1" "rpath r x1 xs3 x2"
| (less_2) xs3 where "xs1 = xs2 @ xs3" "rpath r x xs2 x2" "rpath r x2 xs3 x1"
proof -
have "length xs1 \<le> length xs2 \<or> length xs2 \<le> length xs1" by auto
with assms rpath_overlap_oneside' that show ?thesis by metis
qed
text {*
As a corollary of @{thm "rpath_overlap_oneside"},
the following two lemmas gives one important property of relation tree,
i.e. there is at most one path between any two nodes.
Similar to the proof of @{thm rpath_overlap}, we starts with
the one side version first.
*}
lemma rpath_unique_oneside:
assumes "rpath r x xs1 y"
and "rpath r x xs2 y"
and "length xs1 \<le> length xs2"
shows "xs1 = xs2"
proof -
from rpath_overlap_oneside[OF assms]
obtain xs3 where less_1: "xs2 = xs1 @ xs3" by blast
show ?thesis
proof(cases "xs3 = []")
case True
from less_1[unfolded this] show ?thesis by simp
next
case False
note FalseH = this
show ?thesis
proof(cases "xs1 = []")
case True
have "(x, x) \<in> r^+"
proof(rule rpath_plus)
from assms(1)[unfolded True]
have "y = x" by (cases rule:rpath_nilE, simp)
from assms(2)[unfolded this] show "rpath r x xs2 x" .
next
from less_1 and False show "xs2 \<noteq> []" by simp
qed
with acl show ?thesis by (unfold acyclic_def, auto)
next
case False
then obtain e es where eq_xs1: "xs1 = es@[e]" using rev_exhaust by auto
from assms(2)[unfolded less_1 this]
have "rpath r x (es @ [e] @ xs3) y" by simp
thus ?thesis
proof(cases rule:rpath_appendE)
case 1
from rpath_dest_eq [OF 1(1)[folded eq_xs1] assms(1)]
have "e = y" .
from rpath_plus [OF 1(2)[unfolded this] FalseH]
have "(y, y) \<in> r^+" .
with acl show ?thesis by (unfold acyclic_def, auto)
qed
qed
qed
qed
text {*
The following is the full version of path uniqueness.
*}
lemma rpath_unique:
assumes "rpath r x xs1 y"
and "rpath r x xs2 y"
shows "xs1 = xs2"
proof(cases "length xs1 \<le> length xs2")
case True
from rpath_unique_oneside[OF assms this] show ?thesis .
next
case False
hence "length xs2 \<le> length xs1" by simp
from rpath_unique_oneside[OF assms(2,1) this]
show ?thesis by simp
qed
text {*
The following lemma shows that the `independence` relation is symmetric.
It is an obvious auxiliary lemma which will be used later.
*}
lemma sym_indep: "indep r x y \<Longrightarrow> indep r y x"
by (unfold indep_def, auto)
text {*
This is another `obvious` lemma about trees, which says trees rooted at
independent nodes are disjoint.
*}
lemma subtree_disjoint:
assumes "indep r x y"
shows "subtree r x \<inter> subtree r y = {}"
proof -
{ fix z x y xs1 xs2 xs3
assume ind: "indep r x y"
and rp1: "rpath r z xs1 x"
and rp2: "rpath r z xs2 y"
and h: "xs2 = xs1 @ xs3"
have False
proof(cases "xs1 = []")
case True
from rp1[unfolded this] have "x = z" by auto
from rp2[folded this] rpath_star ind[unfolded indep_def]
show ?thesis by metis
next
case False
then obtain e es where eq_xs1: "xs1 = es@[e]" using rev_exhaust by blast
from rp2[unfolded h this]
have "rpath r z (es @ [e] @ xs3) y" by simp
thus ?thesis
proof(cases rule:rpath_appendE)
case 1
have "e = x" using 1(1)[folded eq_xs1] rp1 rpath_dest_eq by metis
from rpath_star[OF 1(2)[unfolded this]] ind[unfolded indep_def]
show ?thesis by auto
qed
qed
} note my_rule = this
{ fix z
assume h: "z \<in> subtree r x" "z \<in> subtree r y"
from h(1) have "(z, x) \<in> r^*" by (unfold subtree_def, auto)
then obtain xs1 where rp1: "rpath r z xs1 x" using star_rpath by metis
from h(2) have "(z, y) \<in> r^*" by (unfold subtree_def, auto)
then obtain xs2 where rp2: "rpath r z xs2 y" using star_rpath by metis
from rp1 rp2
have False
by (cases, insert my_rule[OF sym_indep[OF assms(1)] rp2 rp1]
my_rule[OF assms(1) rp1 rp2], auto)
} thus ?thesis by auto
qed
text {*
The following lemma @{text "subtree_del"} characterizes the change of sub-tree of
@{text "x"} with the removal of an inside edge @{text "(a, b)"}.
Note that, the case for the removal of an outside edge has already been dealt with
in lemma @{text "subtree_del_outside"}).
This lemma is underpinned by the following two `obvious` facts:
\begin{enumearte}
\item
In graph @{text "r"}, for an inside edge @{text "(a,b) \<in> edges_in r x"},
every node @{text "c"} in the sub-tree of @{text "a"} has a path
which goes first from @{text "c"} to @{text "a"}, then through edge @{text "(a, b)"}, and
finally reaches @{text "x"}. By the uniqueness of path in a tree,
all paths from sub-tree of @{text "a"} to @{text "x"} are such constructed, therefore
must go through @{text "(a, b)"}. The consequence is: with the removal of @{text "(a,b)"},
all such paths will be broken.
\item
On the other hand, all paths not originate from within the sub-tree of @{text "a"}
will not be affected by the removal of edge @{text "(a, b)"}.
The reason is simple: if the path is affected by the removal, it must
contain @{text "(a, b)"}, then it must originate from within the sub-tree of @{text "a"}.
\end{enumearte}
*}
lemma subtree_del_inside: (* ddd *)
assumes "(a,b) \<in> edges_in r x"
shows "subtree (r - {(a, b)}) x = (subtree r x) - subtree r a"
proof -
from assms have asm: "b \<in> subtree r x" "(a, b) \<in> r" by (auto simp:edges_in_def)
-- {* The proof follows a common pattern to prove the equality of sets. *}
{ -- {* The `left to right` direction.
*}
fix c
-- {* Assuming @{text "c"} is inside the sub-tree of @{text "x"} in the reduced graph *}
assume h: "c \<in> subtree (r - {(a, b)}) x"
-- {* We are going to show that @{text "c"} can not be in the sub-tree of @{text "a"} in
the original graph. *}
-- {* In other words, all nodes inside the sub-tree of @{text "a"} in the original
graph will be removed from the sub-tree of @{text "x"} in the reduced graph. *}
-- {* The reason, as analyzed before, is that all paths from within the
sub-tree of @{text "a"} are broken with the removal of edge @{text "(a,b)"}.
*}
have "c \<in> (subtree r x) - subtree r a"
proof -
let ?r' = "r - {(a, b)}" -- {* The reduced graph is abbreviated as @{text "?r'"} *}
from h have "(c, x) \<in> ?r'^*" by (auto simp:subtree_def)
-- {* Extract from the reduced graph the path @{text "xs"} from @{text "c"} to @{text "x"}. *}
then obtain xs where rp0: "rpath ?r' c xs x" by (rule star_rpath, auto)
-- {* It is easy to show @{text "xs"} is also a path in the original graph *}
hence rp1: "rpath r c xs x"
proof(rule rpath_transfer)
from rpath_edges_on[OF rp0]
show "edges_on (c # xs) \<subseteq> r" by auto
qed
-- {* @{text "xs"} is used as the witness to show that @{text "c"}
in the sub-tree of @{text "x"} in the original graph. *}
hence "c \<in> subtree r x"
by (rule rpath_star[elim_format], auto simp:subtree_def)
-- {* The next step is to show that @{text "c"} can not be in the sub-tree of @{text "a"}
in the original graph. *}
-- {* We need to use the fact that all paths originate from within sub-tree of @{text "a"}
are broken. *}
moreover have "c \<notin> subtree r a"
proof
-- {* Proof by contradiction, suppose otherwise *}
assume otherwise: "c \<in> subtree r a"
-- {* Then there is a path in original graph leading from @{text "c"} to @{text "a"} *}
obtain xs1 where rp_c: "rpath r c xs1 a"
proof -
from otherwise have "(c, a) \<in> r^*" by (auto simp:subtree_def)
thus ?thesis by (rule star_rpath, auto intro!:that)
qed
-- {* Starting from this path, we are going to construct a fictional
path from @{text "c"} to @{text "x"}, which, as explained before,
is broken, so that contradiction can be derived. *}
-- {* First, there is a path from @{text "b"} to @{text "x"} *}
obtain ys where rp_b: "rpath r b ys x"
proof -
from asm have "(b, x) \<in> r^*" by (auto simp:subtree_def)
thus ?thesis by (rule star_rpath, auto intro!:that)
qed
-- {* The paths @{text "xs1"} and @{text "ys"} can be
tied together using @{text "(a,b)"} to form a path
from @{text "c"} to @{text "x"}: *}
have "rpath r c (xs1 @ b # ys) x"
proof -
from rstepI[OF asm(2) rp_b] have "rpath r a (b # ys) x" .
from rpath_appendI[OF rp_c this]
show ?thesis .
qed
-- {* By the uniqueness of path between two nodes of a tree, we have: *}
from rpath_unique[OF rp1 this] have eq_xs: "xs = xs1 @ b # ys" .
-- {* Contradiction can be derived from from this fictional path . *}
show False
proof -
-- {* It can be shown that @{term "(a,b)"} is on this fictional path. *}
have "(a, b) \<in> edges_on (c#xs)"
proof(cases "xs1 = []")
case True
from rp_c[unfolded this] have "rpath r c [] a" .
hence eq_c: "c = a" by (rule rpath_nilE, simp)
hence "c#xs = a#xs" by simp
from this and eq_xs have "c#xs = a # xs1 @ b # ys" by simp
from this[unfolded True] have "c#xs = []@[a,b]@ys" by simp
thus ?thesis by (auto simp:edges_on_def)
next
case False
from rpath_nnl_lastE[OF rp_c this]
obtain xs' where "xs1 = xs'@[a]" by auto
from eq_xs[unfolded this] have "c#xs = (c#xs')@[a,b]@ys" by simp
thus ?thesis by (unfold edges_on_def, blast)
qed
-- {* It can also be shown that @{term "(a,b)"} is not on this fictional path. *}
moreover have "(a, b) \<notin> edges_on (c#xs)"
using rpath_edges_on[OF rp0] by auto
-- {* Contradiction is thus derived. *}
ultimately show False by auto
qed
qed
ultimately show ?thesis by auto
qed
} moreover {
-- {* The `right to left` direction.
*}
fix c
-- {* Assuming that @{text "c"} is in the sub-tree of @{text "x"}, but
outside of the sub-tree of @{text "a"} in the original graph, *}
assume h: "c \<in> (subtree r x) - subtree r a"
-- {* we need to show that in the reduced graph, @{text "c"} is still in
the sub-tree of @{text "x"}. *}
have "c \<in> subtree (r - {(a, b)}) x"
proof -
-- {* The proof goes by showing that the path from @{text "c"} to @{text "x"}
in the original graph is not affected by the removal of @{text "(a,b)"}.
*}
from h have "(c, x) \<in> r^*" by (unfold subtree_def, auto)
-- {* Extract the path @{text "xs"} from @{text "c"} to @{text "x"} in the original graph. *}
from star_rpath[OF this] obtain xs where rp: "rpath r c xs x" by auto
-- {* Show that it is also a path in the reduced graph. *}
hence "rpath (r - {(a, b)}) c xs x"
-- {* The proof goes by using rule @{thm rpath_transfer} *}
proof(rule rpath_transfer)
-- {* We need to show all edges on the path are still in the reduced graph. *}
show "edges_on (c # xs) \<subseteq> r - {(a, b)}"
proof -
-- {* It is easy to show that all the edges are in the original graph. *}
from rpath_edges_on [OF rp] have " edges_on (c # xs) \<subseteq> r" .
-- {* The essential part is to show that @{text "(a, b)"} is not on the path. *}
moreover have "(a,b) \<notin> edges_on (c#xs)"
proof
-- {* Proof by contradiction, suppose otherwise: *}
assume otherwise: "(a, b) \<in> edges_on (c#xs)"
-- {* Then @{text "(a, b)"} is in the middle of the path.
with @{text "l1"} and @{text "l2"} be the nodes in
the front and rear respectively. *}
then obtain l1 l2 where eq_xs:
"c#xs = l1 @ [a, b] @ l2" by (unfold edges_on_def, blast)
-- {* From this, it can be shown that @{text "c"} is
in the sub-tree of @{text "a"} *}
have "c \<in> subtree r a"
proof(cases "l1 = []")
case True
-- {* If @{text "l1"} is null, it can be derived that @{text "c = a"}. *}
with eq_xs have "c = a" by auto
-- {* So, @{text "c"} is obviously in the sub-tree of @{text "a"}. *}
thus ?thesis by (unfold subtree_def, auto)
next
case False
-- {* When @{text "l1"} is not null, it must have a tail @{text "es"}: *}
then obtain e es where "l1 = e#es" by (cases l1, auto)
-- {* The relation of this tail with @{text "xs"} is derived: *}
with eq_xs have "xs = es@[a,b]@l2" by auto
-- {* From this, a path from @{text "c"} to @{text "a"} is made visible: *}
from rp[unfolded this] have "rpath r c (es @ [a] @ (b#l2)) x" by simp
thus ?thesis
proof(cases rule:rpath_appendE)
-- {* The path from @{text "c"} to @{text "a"} is extraced
using @{thm "rpath_appendE"}: *}
case 1
from rpath_star[OF this(1)]
-- {* The extracted path servers as a witness that @{text "c"} is
in the sub-tree of @{text "a"}: *}
show ?thesis by (simp add:subtree_def)
qed
qed with h show False by auto
qed ultimately show ?thesis by auto
qed
qed
-- {* From , it is shown that @{text "c"} is in the sub-tree of @{text "x"}
inthe reduced graph. *}
from rpath_star[OF this] show ?thesis by (auto simp:subtree_def)
qed
}
-- {* The equality of sets is derived from the two directions just proved. *}
ultimately show ?thesis by auto
qed
lemma set_del_rootI:
assumes "r1 \<subseteq> r"
and "a \<in> Domain r1"
shows "root (r - r1) a"
proof -
let ?r = "r - r1"
{ fix a'
assume neq: "a' \<noteq> a"
have "a \<notin> subtree ?r a'"
proof
assume "a \<in> subtree ?r a'"
hence "(a, a') \<in> ?r^*" by (auto simp:subtree_def)
from star_rpath[OF this] obtain xs
where rp: "rpath ?r a xs a'" by auto
from rpathE[OF this] and neq
obtain z zs where h: "(a, z) \<in> ?r" "rpath ?r z zs a'" "xs = z#zs" by auto
from assms(2) obtain z' where z'_in: "(a, z') \<in> r1" by (auto simp:DomainE)
with assms(1) have "(a, z') \<in> r" by auto
moreover from h(1) have "(a, z) \<in> r" by simp
ultimately have "z' = z" using sgv by (auto simp:single_valued_def)
from z'_in[unfolded this] and h(1) show False by auto
qed
} thus ?thesis by (intro rootI, auto)
qed
lemma edge_del_no_rootI:
assumes "(a, b) \<in> r"
shows "root (r - {(a, b)}) a"
by (rule set_del_rootI, insert assms, auto)
lemma ancestors_children_unique:
assumes "z1 \<in> ancestors r x \<inter> children r y"
and "z2 \<in> ancestors r x \<inter> children r y"
shows "z1 = z2"
proof -
from assms have h:
"(x, z1) \<in> r^+" "(z1, y) \<in> r"
"(x, z2) \<in> r^+" "(z2, y) \<in> r"
by (auto simp:ancestors_def children_def)
-- {* From this, a path containing @{text "z1"} is obtained. *}
from plus_rpath[OF h(1)] obtain xs1
where h1: "rpath r x xs1 z1" "xs1 \<noteq> []" by auto
from rpath_nnl_lastE[OF this] obtain xs1' where eq_xs1: "xs1 = xs1' @ [z1]"
by auto
from h(2) have h2: "rpath r z1 [y] y" by auto
from rpath_appendI[OF h1(1) h2, unfolded eq_xs1]
have rp1: "rpath r x (xs1' @ [z1, y]) y" by simp
-- {* Then, another path containing @{text "z2"} is obtained. *}
from plus_rpath[OF h(3)] obtain xs2
where h3: "rpath r x xs2 z2" "xs2 \<noteq> []" by auto
from rpath_nnl_lastE[OF this] obtain xs2' where eq_xs2: "xs2 = xs2' @ [z2]"
by auto
from h(4) have h4: "rpath r z2 [y] y" by auto
from rpath_appendI[OF h3(1) h4, unfolded eq_xs2]
have "rpath r x (xs2' @ [z2, y]) y" by simp
-- {* Finally @{text "z1 = z2"} is proved by uniqueness of path. *}
from rpath_unique[OF rp1 this]
have "xs1' @ [z1, y] = xs2' @ [z2, y]" .
thus ?thesis by auto
qed
lemma ancestors_childrenE:
assumes "y \<in> ancestors r x"
obtains "x \<in> children r y"
| z where "z \<in> ancestors r x \<inter> children r y"
proof -
from assms(1) have "(x, y) \<in> r^+" by (auto simp:ancestors_def)
from tranclD2[OF this] obtain z where
h: "(x, z) \<in> r\<^sup>*" "(z, y) \<in> r" by auto
from h(1)
show ?thesis
proof(cases rule:rtranclE)
case base
from h(2)[folded this] have "x \<in> children r y"
by (auto simp:children_def)
thus ?thesis by (intro that, auto)
next
case (step u)
hence "z \<in> ancestors r x" by (auto simp:ancestors_def)
moreover from h(2) have "z \<in> children r y"
by (auto simp:children_def)
ultimately show ?thesis by (intro that, auto)
qed
qed
end (* of rtree *)
lemma subtree_trancl:
"subtree r x = {x} \<union> {y. (y, x) \<in> r^+}" (is "?L = ?R")
proof -
{ fix z
assume "z \<in> ?L"
hence "z \<in> ?R"
proof(cases rule:subtreeE)
case 2
thus ?thesis
by (unfold ancestors_def, auto)
qed auto
} moreover
{ fix z
assume "z \<in> ?R"
hence "z \<in> ?L"
by (unfold subtree_def, auto)
} ultimately show ?thesis by auto
qed
lemma subtree_children:
"subtree r x = {x} \<union> (\<Union> (subtree r ` (children r x)))" (is "?L = ?R")
proof -
{ fix z
assume "z \<in> ?L"
hence "z \<in> ?R"
proof(cases rule:subtreeE[consumes 1])
case 2
hence "(z, x) \<in> r^+" by (auto simp:ancestors_def)
thus ?thesis
proof(rule tranclE)
assume "(z, x) \<in> r"
hence "z \<in> children r x" by (unfold children_def, auto)
moreover have "z \<in> subtree r z" by (auto simp:subtree_def)
ultimately show ?thesis by auto
next
fix c
assume h: "(z, c) \<in> r\<^sup>+" "(c, x) \<in> r"
hence "c \<in> children r x" by (auto simp:children_def)
moreover from h have "z \<in> subtree r c" by (auto simp:subtree_def)
ultimately show ?thesis by auto
qed
qed auto
} moreover {
fix z
assume h: "z \<in> ?R"
have "x \<in> subtree r x" by (auto simp:subtree_def)
moreover {
assume "z \<in> \<Union>(subtree r ` children r x)"
then obtain y where "(y, x) \<in> r" "(z, y) \<in> r^*"
by (auto simp:subtree_def children_def)
hence "(z, x) \<in> r^*" by auto
hence "z \<in> ?L" by (auto simp:subtree_def)
} ultimately have "z \<in> ?L" using h by auto
} ultimately show ?thesis by auto
qed
context fsubtree
begin
lemma finite_subtree:
shows "finite (subtree r x)"
proof(induct rule:wf_induct[OF wf])
case (1 x)
have "finite (\<Union>(subtree r ` children r x))"
proof(rule finite_Union)
show "finite (subtree r ` children r x)"
proof(cases "children r x = {}")
case True
thus ?thesis by auto
next
case False
hence "x \<in> Range r" by (auto simp:children_def)
from fb[rule_format, OF this]
have "finite (children r x)" .
thus ?thesis by (rule finite_imageI)
qed
next
fix M
assume "M \<in> subtree r ` children r x"
then obtain y where h: "y \<in> children r x" "M = subtree r y" by auto
hence "(y, x) \<in> r" by (auto simp:children_def)
from 1[rule_format, OF this, folded h(2)]
show "finite M" .
qed
thus ?case
by (unfold subtree_children finite_Un, auto)
qed
end
definition "pairself f = (\<lambda>(a, b). (f a, f b))"
definition "rel_map f r = (pairself f ` r)"
lemma rel_mapE:
assumes "(a, b) \<in> rel_map f r"
obtains c d
where "(c, d) \<in> r" "(a, b) = (f c, f d)"
using assms
by (unfold rel_map_def pairself_def, auto)
lemma rel_mapI:
assumes "(a, b) \<in> r"
and "c = f a"
and "d = f b"
shows "(c, d) \<in> rel_map f r"
using assms
by (unfold rel_map_def pairself_def, auto)
lemma map_appendE:
assumes "map f zs = xs @ ys"
obtains xs' ys'
where "zs = xs' @ ys'" "xs = map f xs'" "ys = map f ys'"
proof -
have "\<exists> xs' ys'. zs = xs' @ ys' \<and> xs = map f xs' \<and> ys = map f ys'"
using assms
proof(induct xs arbitrary:zs ys)
case (Nil zs ys)
thus ?case by auto
next
case (Cons x xs zs ys)
note h = this
show ?case
proof(cases zs)
case (Cons e es)
with h have eq_x: "map f es = xs @ ys" "x = f e" by auto
from h(1)[OF this(1)]
obtain xs' ys' where "es = xs' @ ys'" "xs = map f xs'" "ys = map f ys'"
by blast
with Cons eq_x
have "zs = (e#xs') @ ys' \<and> x # xs = map f (e#xs') \<and> ys = map f ys'" by auto
thus ?thesis by metis
qed (insert h, auto)
qed
thus ?thesis by (auto intro!:that)
qed
lemma rel_map_mono:
assumes "r1 \<subseteq> r2"
shows "rel_map f r1 \<subseteq> rel_map f r2"
using assms
by (auto simp:rel_map_def pairself_def)
lemma rel_map_compose [simp]:
shows "rel_map f1 (rel_map f2 r) = rel_map (f1 o f2) r"
by (auto simp:rel_map_def pairself_def)
lemma edges_on_map: "edges_on (map f xs) = rel_map f (edges_on xs)"
proof -
{ fix a b
assume "(a, b) \<in> edges_on (map f xs)"
then obtain l1 l2 where eq_map: "map f xs = l1 @ [a, b] @ l2"
by (unfold edges_on_def, auto)
hence "(a, b) \<in> rel_map f (edges_on xs)"
by (auto elim!:map_appendE intro!:rel_mapI simp:edges_on_def)
} moreover {
fix a b
assume "(a, b) \<in> rel_map f (edges_on xs)"
then obtain c d where
h: "(c, d) \<in> edges_on xs" "(a, b) = (f c, f d)"
by (elim rel_mapE, auto)
then obtain l1 l2 where
eq_xs: "xs = l1 @ [c, d] @ l2"
by (auto simp:edges_on_def)
hence eq_map: "map f xs = map f l1 @ [f c, f d] @ map f l2" by auto
have "(a, b) \<in> edges_on (map f xs)"
proof -
from h(2) have "[f c, f d] = [a, b]" by simp
from eq_map[unfolded this] show ?thesis by (auto simp:edges_on_def)
qed
} ultimately show ?thesis by auto
qed
lemma image_id:
assumes "\<And> x. x \<in> A \<Longrightarrow> f x = x"
shows "f ` A = A"
using assms by (auto simp:image_def)
lemma rel_map_inv_id:
assumes "inj_on f ((Domain r) \<union> (Range r))"
shows "(rel_map (inv_into ((Domain r) \<union> (Range r)) f \<circ> f) r) = r"
proof -
let ?f = "(inv_into (Domain r \<union> Range r) f \<circ> f)"
{
fix a b
assume h0: "(a, b) \<in> r"
have "pairself ?f (a, b) = (a, b)"
proof -
from assms h0 have "?f a = a" by (auto intro:inv_into_f_f)
moreover have "?f b = b"
by (insert h0, simp, intro inv_into_f_f[OF assms], auto intro!:RangeI)
ultimately show ?thesis by (auto simp:pairself_def)
qed
} thus ?thesis by (unfold rel_map_def, intro image_id, case_tac x, auto)
qed
lemma rel_map_acyclic:
assumes "acyclic r"
and "inj_on f ((Domain r) \<union> (Range r))"
shows "acyclic (rel_map f r)"
proof -
let ?D = "Domain r \<union> Range r"
{ fix a
assume "(a, a) \<in> (rel_map f r)^+"
from plus_rpath[OF this]
obtain xs where rp: "rpath (rel_map f r) a xs a" "xs \<noteq> []" by auto
from rpath_nnl_lastE[OF this] obtain xs' where eq_xs: "xs = xs'@[a]" by auto
from rpath_edges_on[OF rp(1)]
have h: "edges_on (a # xs) \<subseteq> rel_map f r" .
from edges_on_map[of "inv_into ?D f" "a#xs"]
have "edges_on (map (inv_into ?D f) (a # xs)) = rel_map (inv_into ?D f) (edges_on (a # xs))" .
with rel_map_mono[OF h, of "inv_into ?D f"]
have "edges_on (map (inv_into ?D f) (a # xs)) \<subseteq> rel_map ((inv_into ?D f) o f) r" by simp
from this[unfolded eq_xs]
have subr: "edges_on (map (inv_into ?D f) (a # xs' @ [a])) \<subseteq> rel_map (inv_into ?D f \<circ> f) r" .
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]"
by simp
from edges_on_rpathI[OF subr[unfolded this]]
have "rpath (rel_map (inv_into ?D f \<circ> f) r)
(inv_into ?D f a) (map (inv_into ?D f) xs' @ [inv_into ?D f a]) (inv_into ?D f a)" .
hence "(inv_into ?D f a, inv_into ?D f a) \<in> (rel_map (inv_into ?D f \<circ> f) r)^+"
by (rule rpath_plus, simp)
moreover have "(rel_map (inv_into ?D f \<circ> f) r) = r" by (rule rel_map_inv_id[OF assms(2)])
moreover note assms(1)
ultimately have False by (unfold acyclic_def, auto)
} thus ?thesis by (auto simp:acyclic_def)
qed
lemma relpow_mult:
"((r::'a rel) ^^ m) ^^ n = r ^^ (m*n)"
proof(induct n arbitrary:m)
case (Suc k m)
thus ?case
proof -
have h: "(m * k + m) = (m + m * k)" by auto
show ?thesis
apply (simp add:Suc relpow_add[symmetric])
by (unfold h, simp)
qed
qed simp
lemma compose_relpow_2:
assumes "r1 \<subseteq> r"
and "r2 \<subseteq> r"
shows "r1 O r2 \<subseteq> r ^^ (2::nat)"
proof -
{ fix a b
assume "(a, b) \<in> r1 O r2"
then obtain e where "(a, e) \<in> r1" "(e, b) \<in> r2"
by auto
with assms have "(a, e) \<in> r" "(e, b) \<in> r" by auto
hence "(a, b) \<in> r ^^ (Suc (Suc 0))" by auto
} thus ?thesis by (auto simp:numeral_2_eq_2)
qed
lemma acyclic_compose:
assumes "acyclic r"
and "r1 \<subseteq> r"
and "r2 \<subseteq> r"
shows "acyclic (r1 O r2)"
proof -
{ fix a
assume "(a, a) \<in> (r1 O r2)^+"
from trancl_mono[OF this compose_relpow_2[OF assms(2, 3)]]
have "(a, a) \<in> (r ^^ 2) ^+" .
from trancl_power[THEN iffD1, OF this]
obtain n where h: "(a, a) \<in> (r ^^ 2) ^^ n" "n > 0" by blast
from this(1)[unfolded relpow_mult] have h2: "(a, a) \<in> r ^^ (2 * n)" .
have "(a, a) \<in> r^+"
proof(cases rule:trancl_power[THEN iffD2])
from h(2) h2 show "\<exists>n>0. (a, a) \<in> r ^^ n"
by (rule_tac x = "2*n" in exI, auto)
qed
with assms have "False" by (auto simp:acyclic_def)
} thus ?thesis by (auto simp:acyclic_def)
qed
lemma children_compose_unfold:
"children (r1 O r2) x = \<Union> (children r1 ` (children r2 x))"
by (auto simp:children_def)
lemma fbranch_compose:
assumes "fbranch r1"
and "fbranch r2"
shows "fbranch (r1 O r2)"
proof -
{ fix x
assume "x\<in>Range (r1 O r2)"
then obtain y z where h: "(y, z) \<in> r1" "(z, x) \<in> r2" by auto
have "finite (children (r1 O r2) x)"
proof(unfold children_compose_unfold, rule finite_Union)
show "finite (children r1 ` children r2 x)"
proof(rule finite_imageI)
from h(2) have "x \<in> Range r2" by auto
from assms(2)[unfolded fbranch_def, rule_format, OF this]
show "finite (children r2 x)" .
qed
next
fix M
assume "M \<in> children r1 ` children r2 x"
then obtain y where h1: "y \<in> children r2 x" "M = children r1 y" by auto
show "finite M"
proof(cases "children r1 y = {}")
case True
with h1(2) show ?thesis by auto
next
case False
hence "y \<in> Range r1" by (unfold children_def, auto)
from assms(1)[unfolded fbranch_def, rule_format, OF this, folded h1(2)]
show ?thesis .
qed
qed
} thus ?thesis by (unfold fbranch_def, auto)
qed
lemma finite_fbranchI:
assumes "finite r"
shows "fbranch r"
proof -
{ fix x
assume "x \<in>Range r"
have "finite (children r x)"
proof -
have "{y. (y, x) \<in> r} \<subseteq> Domain r" by (auto)
from rev_finite_subset[OF finite_Domain[OF assms] this]
have "finite {y. (y, x) \<in> r}" .
thus ?thesis by (unfold children_def, simp)
qed
} thus ?thesis by (auto simp:fbranch_def)
qed
lemma subset_fbranchI:
assumes "fbranch r1"
and "r2 \<subseteq> r1"
shows "fbranch r2"
proof -
{ fix x
assume "x \<in>Range r2"
with assms(2) have "x \<in> Range r1" by auto
from assms(1)[unfolded fbranch_def, rule_format, OF this]
have "finite (children r1 x)" .
hence "finite (children r2 x)"
proof(rule rev_finite_subset)
from assms(2)
show "children r2 x \<subseteq> children r1 x" by (auto simp:children_def)
qed
} thus ?thesis by (auto simp:fbranch_def)
qed
lemma children_subtree:
shows "children r x \<subseteq> subtree r x"
by (auto simp:children_def subtree_def)
lemma children_union_kept:
assumes "x \<notin> Range r'"
shows "children (r \<union> r') x = children r x"
using assms
by (auto simp:children_def)
lemma wf_rbase:
assumes "wf r"
obtains b where "(b, a) \<in> r^*" "\<forall> c. (c, b) \<notin> r"
proof -
from assms
have "\<exists> b. (b, a) \<in> r^* \<and> (\<forall> c. (c, b) \<notin> r)"
proof(induct)
case (less x)
thus ?case
proof(cases "\<exists> z. (z, x) \<in> r")
case False
moreover have "(x, x) \<in> r^*" by auto
ultimately show ?thesis by metis
next
case True
then obtain z where h_z: "(z, x) \<in> r" by auto
from less[OF this]
obtain b where "(b, z) \<in> r^*" "(\<forall>c. (c, b) \<notin> r)"
by auto
moreover from this(1) h_z have "(b, x) \<in> r^*" by auto
ultimately show ?thesis by metis
qed
qed
with that show ?thesis by metis
qed
lemma wf_base:
assumes "wf r"
and "a \<in> Range r"
obtains b where "(b, a) \<in> r^+" "\<forall> c. (c, b) \<notin> r"
proof -
from assms(2) obtain a' where h_a: "(a', a) \<in> r" by auto
from wf_rbase[OF assms(1), of a]
obtain b where h_b: "(b, a) \<in> r\<^sup>*" "\<forall>c. (c, b) \<notin> r" by auto
from rtranclD[OF this(1)]
have "b = a \<or> b \<noteq> a \<and> (b, a) \<in> r\<^sup>+" by auto
moreover have "b \<noteq> a" using h_a h_b(2) by auto
ultimately have "(b, a) \<in> r\<^sup>+" by auto
with h_b(2) and that show ?thesis by metis
qed
end