--- a/RTree.thy Fri Apr 15 14:44:09 2016 +0100
+++ b/RTree.thy Thu Jun 02 13:15:03 2016 +0100
@@ -1,5 +1,6 @@
theory RTree
imports "~~/src/HOL/Library/Transitive_Closure_Table" Max
+ (* "Lcrules" *)
begin
section {* A theory of relational trees *}
@@ -99,19 +100,7 @@
*}
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
+ by (auto simp:edges_in_def subtree_def)
text {*
The following lemma shows the meaning of @{term "edges_in"} from the other side,
@@ -131,48 +120,20 @@
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
+ using fb by (cases "children r x = {}", auto simp:children_def)
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
+ by (induct i rule:less_induct, auto)
subsection {* Properties of Relational Graphs and Relational Trees *}
@@ -210,7 +171,7 @@
using assms[unfolded rpath_def]
by (induct, auto simp:pred_of_def rpath_def)
-lemma rpathE:
+lemma rpathE [elim]:
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"
@@ -236,8 +197,15 @@
by (auto simp:pred_of_def rpath_def)
qed
+lemma rpath_stepI'[intro, simp]:
+ assumes "rpath r x xs y"
+ and "(y, z) \<in> r"
+ shows "rpath r x (xs@[z]) z"
+ using assms
+ by (induct, auto)
+
text {* Introduction rule for @{text "@"}-path *}
-lemma rpath_appendI [intro]:
+lemma rpath_appendI [intro,simp]:
assumes "rpath r x xs a" and "rpath r a ys y"
shows "rpath r x (xs @ ys) y"
using assms
@@ -245,7 +213,7 @@
text {* Elimination rule for empty path *}
-lemma rpath_cases [cases pred:rpath]:
+lemma rpath_cases [cases pred:rpath,elim]:
assumes "rpath r a1 a2 a3"
obtains (rbase) "a1 = a3" and "a2 = []"
| (rstep) y :: "'a" and ys :: "'a list"
@@ -258,21 +226,6 @@
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 "#"}.
*}
@@ -287,145 +240,155 @@
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:
+lemma rpath_nnl_lastE [elim]:
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)
+ using assms
+proof(induct)
+ case (rstep x y ys z)
+ thus ?case by (cases ys, auto)
+qed auto
text {* Other elimination rules of @{text "rpath"} *}
-lemma rpath_appendE:
+lemma rpath_appendE [elim]:
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:
+lemma rpath_subE [elim]:
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:
+lemma rpath_dest_eq [simp]:
assumes "rpath r x xs x1"
and "rpath r x xs x2"
shows "x1 = x2"
using assms
by (induct, auto)
+lemma rpath_dest_eq_simp[simp]:
+ assumes "rpath r x xs1 x1"
+ and "rpath r x xs2 x2"
+ and "xs1 = xs2"
+ 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"
+lemma edge_on_headI[simp, intro]:
+ assumes "(a, b) = (a', b')"
+ shows "(a, b) \<in> edges_on (a' # b' # xs)"
using assms
by (unfold edges_on_def, auto)
+lemma edges_on_ConsI[intro]:
+ assumes "(a, b) \<in> edges_on xs"
+ shows "(a, b) \<in> edges_on (x#xs)"
+ using assms
+ apply (unfold edges_on_def, auto)
+ by (meson Cons_eq_appendI)
+
+lemma edges_on_appendI1[intro]:
+ assumes "(a, b) \<in> edges_on xs"
+ shows "(a, b) \<in> edges_on (xs'@xs)"
+ using assms
+ apply (unfold edges_on_def, auto simp:append_assoc)
+ by (metis append_assoc)
+
+lemma edges_on_appendI2[intro]:
+ assumes "(a, b) \<in> edges_on xs"
+ shows "(a, b) \<in> edges_on (xs@xs')"
+ using assms
+ apply (unfold edges_on_def, auto)
+ by metis
+
+lemma edges_onE [elim]:
+ assumes "(a, b) \<in> edges_on xs"
+ obtains a' b' xs' where "(a,b) = (a', b')" "xs = a'#b'#xs'"
+ | a' b' xs' where "(a,b) \<noteq> (a', b')" "xs = a'#b'#xs'" "(a,b) \<in> edges_on (b'#xs')"
+proof(cases xs)
+ case Nil
+ with assms show ?thesis
+ by (unfold edges_on_def, auto)
+next
+ case cs1: (Cons a' xsa)
+ show ?thesis
+ proof(cases xsa)
+ case Nil
+ with cs1 and assms show ?thesis
+ by (unfold edges_on_def, auto)
+ next
+ case (Cons b' xsb)
+ show ?thesis
+ proof(cases "(a,b) = (a', b')")
+ case True
+ with cs1 Cons show ?thesis using that by metis
+ next
+ case False
+ from assms[unfolded cs1 Cons edges_on_def]
+ obtain xs1 ys1 where "a' # b' # xsb = xs1 @ [a, b] @ ys1" by auto
+ moreover with False obtain c xsc where "xs1 = Cons c xsc" by (cases xs1, auto)
+ ultimately have h: "b' # xsb = xsc @ [a, b] @ ys1" by auto
+ show ?thesis
+ apply (rule that(2)[OF False], insert cs1 Cons, simp)
+ using h by auto
+ qed
+ qed
+qed
+
+lemma edges_on_nil [simp]:
+ "edges_on [] = {}" by auto
+
+lemma edges_on_single [simp]:
+ "edges_on [a] = {}" by auto
+
+lemma edges_on_unfold [simp]:
+ "edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R")
+by (auto)
+
+lemma edges_on_len:
+ assumes "x \<in> edges_on l"
+ shows "2 \<le> length l" using assms by (cases x, auto)
+
text {* Elimination of @{text "edges_on"} for non-empty path *}
-lemma edges_on_consE [elim, cases set:edges_on]:
+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
+ using assms
+ by auto
+
text {*
Every edges on the path is a graph edges:
*}
-lemma rpath_edges_on:
+
+lemma rpath_edges_on [intro]:
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
+ shows "edges_on (x#xs) \<subseteq> r"
+ using assms
+ by (induct arbitrary:y, auto)
text {* @{text "edges_on"} is mono with respect to @{text "#"}-operation: *}
-lemma edges_on_Cons_mono:
+lemma edges_on_Cons_mono [intro,simp]:
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
+ by auto
+
+lemma edges_on_append_mono [intro,simp]:
+ shows "edges_on xs \<subseteq> edges_on (xs'@xs)"
+ by auto
+
+lemma edges_on_append_mono' [intro,simp]:
+ shows "edges_on xs \<subseteq> edges_on (xs@xs')"
+ by auto
text {*
The following rule @{text "rpath_transfer"} is used to show
@@ -437,68 +400,52 @@
then @{text "x#xs"} is also a edge in graph @{text "r2"}:
*}
-lemma rpath_transfer:
+lemma rpath_transfer[intro]:
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:
+ by (induct, auto)
+
+lemma edges_on_rpathI[intro, simp]:
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)
+ by (induct xs arbitrary: a b, auto)
+
+lemma list_nnl_appendE [elim]:
+ assumes "xs \<noteq> []"
+ obtains x xs' where "xs = xs'@[x]"
+ by (insert assms, rule rev_exhaust, fastforce)
+
+lemma edges_on_rpathI' [intro]:
+ assumes "edges_on (a#xs) \<subseteq> r"
+ and "xs \<noteq> []"
+ and "last xs = b"
+ shows "rpath r a xs b"
+proof -
+ obtain xs' where "xs = xs'@[b]"
+ using assms by fastforce
+ with assms show ?thesis by fastforce
qed
text {*
The following lemma extracts the path from @{text "x"} to @{text "y"}
from proposition @{text "(x, y) \<in> r^*"}
*}
-lemma star_rpath:
+
+lemma star_rpath [elim]:
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
+ using assms
+ by (induct, auto)
+
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:
+lemma rpath_star [simp]:
assumes "rpath r x xs y"
shows "(x, y) \<in> r^*"
proof -
@@ -507,25 +454,42 @@
thus ?thesis by (simp add: pred_of_star star_2_pstar)
qed
-lemma subtree_transfer:
+declare rpath_star[elim_format]
+
+lemma rpath_transfer' [intro]:
+ assumes "rpath r1 x xs y"
+ and "r1 \<subseteq> r2"
+ shows "rpath r2 x xs y"
+ using assms
+ by (induct, auto)
+
+lemma subtree_transfer[intro]:
assumes "a \<in> subtree r1 a'"
and "r1 \<subseteq> r2"
shows "a \<in> subtree r2 a'"
+ using assms
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
+ from assms(1)
+ obtain xs where h1: "rpath r1 a xs a'" by (auto simp:subtree_def)
+ show ?thesis
+ proof -
+ from rpath_star[OF h1]
+ have "(a, a') \<in> r1\<^sup>*" .
+ with assms(2) have "(a, a') \<in> r2\<^sup>*"
+ using rtrancl_mono subsetCE by blast
+ thus ?thesis by (auto simp:subtree_def)
qed
- from rpath_star[OF this]
- show ?thesis by (auto simp:subtree_def)
-qed
+qed
-lemma subtree_rev_transfer:
+text {*
+ @{text "subtree"} is mono with respect to the underlying graph.
+*}
+lemma subtree_mono[intro]:
+ assumes "r1 \<subseteq> r2"
+ shows "subtree r1 x \<subseteq> subtree r2 x"
+ using assms by auto
+
+lemma subtree_rev_transfer[intro]:
assumes "a \<notin> subtree r2 a'"
and "r1 \<subseteq> r2"
shows "a \<notin> subtree r1 a'"
@@ -535,59 +499,37 @@
The following lemmas establishes a relation from paths in @{text "r"}
to @{text "r^+"} relation.
*}
-lemma rpath_plus:
+lemma rpath_plus[simp]:
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
+ using assms
+ by (induct, simp) fastforce
-lemma plus_rpath:
+lemma plus_rpath [elim]:
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
+ have "\<exists> xs. rpath r x xs y \<and> xs \<noteq> []" by (induct; auto)
+ with that show ?thesis by metis
qed
-
+
subsubsection {* Properties of @{text "subtree"} and @{term "ancestors"}*}
-lemma ancestors_subtreeI:
+lemma ancestors_subtreeI [intro, dest]:
assumes "b \<in> ancestors r a"
shows "a \<in> subtree r b"
using assms by (auto simp:subtree_def ancestors_def)
-lemma ancestors_Field:
+lemma ancestors_Field[elim]:
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:
+lemma subtreeE [elim]:
assumes "a \<in> subtree r b"
obtains "a = b"
| "a \<noteq> b" and "b \<in> ancestors r a"
@@ -599,7 +541,7 @@
qed
-lemma subtree_Field:
+lemma subtree_Field [simp, iff]:
"subtree r x \<subseteq> Field r \<union> {x}"
proof
fix y
@@ -610,8 +552,8 @@
thus ?thesis by auto
next
case 2
- thus ?thesis apply (auto simp:ancestors_def)
- using Field_def tranclD by fastforce
+ thus ?thesis
+ by (unfold Field_def, fast)
qed
qed
@@ -620,28 +562,7 @@
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
+ by auto
text {*
The following lemma characterizes the change of sub-tree of @{text "x"}
@@ -651,14 +572,14 @@
@{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 *)
+lemma subtree_del_outside [simp,intro]: (* ddd *)
assumes "b \<notin> subtree r x"
- shows "subtree (r - {(a, b)}) x = (subtree r x)"
+ shows "subtree (r - {(a, b)}) x = (subtree r x)" (is "?L = ?R")
proof -
{ fix c
- assume "c \<in> (subtree r x)"
+ assume "c \<in> ?R"
hence "(c, x) \<in> r^*" by (auto simp:subtree_def)
- hence "c \<in> subtree (r - {(a, b)}) x"
+ hence "c \<in> ?L"
proof(rule star_rpath)
fix xs
assume rp: "rpath r c xs x"
@@ -667,7 +588,7 @@
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" .
+ from 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)"
@@ -676,27 +597,24 @@
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
+ by (rule rpath_appendE, insert assms(1), auto simp:subtree_def)
qed
- ultimately show "edges_on (c # xs) \<subseteq> r - {(a,b)}" by auto
+ 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)
+ thus ?thesis by (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
+ assume "c \<in> ?L"
+ moreover have "... \<subseteq> (subtree r x)" by auto
+ ultimately have "c \<in> ?R" by auto
} ultimately show ?thesis by auto
qed
(* ddd *)
-lemma subset_del_subtree_outside: (* ddd *)
+lemma subset_del_subtree_outside [simp, intro]: (* ddd *)
assumes "Range r' \<inter> subtree r x = {}"
shows "subtree (r - r') x = (subtree r x)"
proof -
@@ -712,7 +630,7 @@
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" .
+ from rp have "edges_on (c # xs) \<subseteq> r" ..
moreover {
fix a b
assume h: "(a, b) \<in> r'"
@@ -731,7 +649,7 @@
with assms (1) and h show ?thesis by (auto)
qed
qed
- } ultimately show "edges_on (c # xs) \<subseteq> r - r'" by auto
+ } 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
@@ -744,21 +662,22 @@
} ultimately show ?thesis by auto
qed
-lemma subtree_insert_ext:
+lemma subtree_insert_ext [simp, intro]:
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:
+lemma subtree_insert_next [simp, intro]:
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:
+lemma set_add_rootI[simp, intro]:
assumes "root r a"
and "a \<notin> Domain r1"
shows "root (r \<union> r1) a"
+ using assms
proof -
let ?r = "r \<union> r1"
{ fix a'
@@ -777,7 +696,7 @@
} thus ?thesis by (auto simp:root_def)
qed
-lemma ancestors_mono:
+lemma ancestors_mono [simp]:
assumes "r1 \<subseteq> r2"
shows "ancestors r1 x \<subseteq> ancestors r2 x"
proof
@@ -788,8 +707,9 @@
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
+ from h(1) have "edges_on (x # xs) \<subseteq> r1" ..
+ also note assms
+ finally show "edges_on (x # xs) \<subseteq> r2" .
qed
from rpath_plus[OF this h(2)]
show "a \<in> ancestors r2 x" by (auto simp:ancestors_def)
@@ -866,7 +786,7 @@
} ultimately show ?thesis by auto
qed
-lemma rootI:
+lemma rootI [intro]:
assumes h: "\<And> x'. x' \<noteq> x \<Longrightarrow> x \<notin> subtree r' x'"
and "r' \<subseteq> r"
shows "root r' x"
@@ -887,7 +807,7 @@
} thus ?thesis by (auto simp:root_def)
qed
-lemma rpath_overlap_oneside: (* ddd *)
+lemma rpath_overlap_oneside [elim]: (* ddd *)
assumes "rpath r x xs1 x1"
and "rpath r x xs2 x2"
and "length xs1 \<le> length xs2"
@@ -916,7 +836,7 @@
-- {* 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
+ using h2[rule_format, OF lt_j] and h1 by linarith
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"
@@ -950,22 +870,21 @@
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
+ then obtain e es where eq_es: "take ?idx xs1 = es@[e]" by fast
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
+ 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
+ show ?thesis by (auto)
qed
ultimately show ?thesis
using sgv[unfolded single_valued_def] neq_idx by metis
@@ -1068,7 +987,7 @@
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
+ then obtain e es where eq_xs1: "xs1 = es@[e]" by fast
from assms(2)[unfolded less_1 this]
have "rpath r x (es @ [e] @ xs3) y" by simp
thus ?thesis
@@ -1129,7 +1048,7 @@
show ?thesis by metis
next
case False
- then obtain e es where eq_xs1: "xs1 = es@[e]" using rev_exhaust by blast
+ then obtain e es where eq_xs1: "xs1 = es@[e]" by fast
from rp2[unfolded h this]
have "rpath r z (es @ [e] @ xs3) y" by simp
thus ?thesis
@@ -1204,11 +1123,8 @@
-- {* 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
+ hence rp1: "rpath r c xs x" using rpath_edges_on[OF rp0]
+ by auto
-- {* @{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"
@@ -1255,7 +1171,7 @@
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 eq_c: "c = a" by fast
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
@@ -1269,7 +1185,7 @@
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
+ using rpath_edges_on[OF rp0] by (auto)
-- {* Contradiction is thus derived. *}
ultimately show False by auto
qed
@@ -1349,7 +1265,7 @@
qed
}
-- {* The equality of sets is derived from the two directions just proved. *}
- ultimately show ?thesis by auto
+ ultimately show ?thesis by blast
qed
lemma set_del_rootI:
@@ -1461,43 +1377,19 @@
} ultimately show ?thesis by auto
qed
+lemma ancestor_children_subtreeI [intro]:
+ "x \<in> ancestors r z \<Longrightarrow> z \<in> \<Union>(subtree r ` children r x)"
+ by (unfold ancestors_def children_def, auto simp:subtree_def dest:tranclD2)
+
+lemma [iff]: "x \<in> subtree r x"
+ by (auto simp:subtree_def)
+
+lemma [intro]: "xa \<in> children r x \<Longrightarrow> z \<in> subtree r xa \<Longrightarrow> z \<in> subtree r x"
+ by (unfold children_def subtree_def, auto)
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
+ "subtree r x = ({x} \<union> (\<Union> (subtree r ` (children r x))))" (is "?L = ?R")
+ by fast
context fsubtree
begin
@@ -1684,7 +1576,7 @@
qed
qed simp
-lemma compose_relpow_2:
+lemma compose_relpow_2 [intro, simp]:
assumes "r1 \<subseteq> r"
and "r2 \<subseteq> r"
shows "r1 O r2 \<subseteq> r ^^ (2::nat)"
@@ -1698,7 +1590,7 @@
} thus ?thesis by (auto simp:numeral_2_eq_2)
qed
-lemma acyclic_compose:
+lemma acyclic_compose [intro, simp]:
assumes "acyclic r"
and "r1 \<subseteq> r"
and "r2 \<subseteq> r"
@@ -1724,7 +1616,7 @@
"children (r1 O r2) x = \<Union> (children r1 ` (children r2 x))"
by (auto simp:children_def)
-lemma fbranch_compose:
+lemma fbranch_compose [intro, simp]:
assumes "fbranch r1"
and "fbranch r2"
shows "fbranch (r1 O r2)"
@@ -1758,7 +1650,7 @@
} thus ?thesis by (unfold fbranch_def, auto)
qed
-lemma finite_fbranchI:
+lemma finite_fbranchI [intro]:
assumes "finite r"
shows "fbranch r"
proof -
@@ -1774,7 +1666,7 @@
} thus ?thesis by (auto simp:fbranch_def)
qed
-lemma subset_fbranchI:
+lemma subset_fbranchI [intro]:
assumes "fbranch r1"
and "r2 \<subseteq> r1"
shows "fbranch r2"
@@ -1792,17 +1684,17 @@
} thus ?thesis by (auto simp:fbranch_def)
qed
-lemma children_subtree:
+lemma children_subtree [simp, intro]:
shows "children r x \<subseteq> subtree r x"
by (auto simp:children_def subtree_def)
-lemma children_union_kept:
+lemma children_union_kept [simp]:
assumes "x \<notin> Range r'"
shows "children (r \<union> r') x = children r x"
using assms
by (auto simp:children_def)
-lemma wf_rbase:
+lemma wf_rbase [elim]:
assumes "wf r"
obtains b where "(b, a) \<in> r^*" "\<forall> c. (c, b) \<notin> r"
proof -
@@ -1828,7 +1720,7 @@
with that show ?thesis by metis
qed
-lemma wf_base:
+lemma wf_base [elim]:
assumes "wf r"
and "a \<in> Range r"
obtains b where "(b, a) \<in> r^+" "\<forall> c. (c, b) \<notin> r"
@@ -1843,4 +1735,21 @@
with h_b(2) and that show ?thesis by metis
qed
+(*
+lcrules crules
+
+declare crules(26,43,44,45,46,47)[rule del]
+*)
+
+
+declare RTree.subtree_transfer[rule del]
+
+declare RTree.subtreeE[rule del]
+
+declare RTree.ancestors_Field[rule del]
+
+declare RTree.star_rpath[rule del]
+
+declare RTree.plus_rpath[rule del]
+
end
\ No newline at end of file