--- a/RTree.thy~ Sun Jan 17 22:18:35 2016 +0800
+++ b/RTree.thy~ Wed Jan 27 19:26:56 2016 +0800
@@ -154,6 +154,7 @@
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
@@ -597,10 +598,6 @@
with that[unfolded ancestors_def] show ?thesis by auto
qed
-lemma subtree_Field:
- assumes "a \<in> Field r"
- shows "subtree r a \<subseteq> Field r"
-by (metis Field_def UnI1 ancestors_Field assms subsetI subtreeE)
lemma subtree_Field:
"subtree r x \<subseteq> Field r \<union> {x}"
@@ -891,6 +888,100 @@
qed
lemma rpath_overlap_oneside: (* ddd *)
+ assumes "rpath r x xs1 x1" (* ccc *)
+ 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(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: (* ddd *)
assumes "rpath r x xs1 x1"
and "rpath r x xs2 x2"
and "length xs1 \<le> length xs2"
@@ -1745,4 +1836,45 @@
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
\ No newline at end of file