886 show False by (auto simp:acyclic_def) |
883 show False by (auto simp:acyclic_def) |
887 qed |
884 qed |
888 moreover from h1 have "x \<in> subtree r' x'" by (auto simp:subtree_def) |
885 moreover from h1 have "x \<in> subtree r' x'" by (auto simp:subtree_def) |
889 ultimately have False using h by auto |
886 ultimately have False using h by auto |
890 } thus ?thesis by (auto simp:root_def) |
887 } thus ?thesis by (auto simp:root_def) |
|
888 qed |
|
889 |
|
890 lemma rpath_overlap_oneside: (* ddd *) |
|
891 assumes "rpath r x xs1 x1" (* ccc *) |
|
892 and "rpath r x xs2 x2" |
|
893 and "length xs1 \<le> length xs2" |
|
894 obtains xs3 where |
|
895 "xs2 = xs1 @ xs3" "rpath r x xs1 x1" "rpath r x1 xs3 x2" |
|
896 proof(cases "xs1 = []") |
|
897 case True |
|
898 with that show ?thesis by auto |
|
899 next |
|
900 case False |
|
901 have "\<forall> i \<le> length xs1. take i xs1 = take i xs2" |
|
902 proof - |
|
903 { assume "\<not> (\<forall> i \<le> length xs1. take i xs1 = take i xs2)" |
|
904 then obtain i where "i \<le> length xs1 \<and> take i xs1 \<noteq> take i xs2" by auto |
|
905 from this(1) have "False" |
|
906 proof(rule index_minimize) |
|
907 fix j |
|
908 assume h1: "j \<le> length xs1 \<and> take j xs1 \<noteq> take j xs2" |
|
909 and h2: " \<forall>k<j. \<not> (k \<le> length xs1 \<and> take k xs1 \<noteq> take k xs2)" |
|
910 -- {* @{text "j - 1"} is the branch point between @{text "xs1"} and @{text "xs2"} *} |
|
911 let ?idx = "j - 1" |
|
912 -- {* A number of inequalities concerning @{text "j - 1"} are derived first *} |
|
913 have lt_i: "?idx < length xs1" using False h1 |
|
914 by (metis Suc_diff_1 le_neq_implies_less length_greater_0_conv lessI less_imp_diff_less) |
|
915 have lt_i': "?idx < length xs2" using lt_i and assms(3) by auto |
|
916 have lt_j: "?idx < j" using h1 by (cases j, auto) |
|
917 -- {* From thesis inequalities, a number of equations concerning @{text "xs1"} |
|
918 and @{text "xs2"} are derived *} |
|
919 have eq_take: "take ?idx xs1 = take ?idx xs2" |
|
920 using h2[rule_format, OF lt_j] and h1 by auto |
|
921 have eq_xs1: " xs1 = take ?idx xs1 @ xs1 ! (?idx) # drop (Suc (?idx)) xs1" |
|
922 using id_take_nth_drop[OF lt_i] . |
|
923 have eq_xs2: "xs2 = take ?idx xs2 @ xs2 ! (?idx) # drop (Suc (?idx)) xs2" |
|
924 using id_take_nth_drop[OF lt_i'] . |
|
925 -- {* The branch point along the path is finally pinpointed *} |
|
926 have neq_idx: "xs1!?idx \<noteq> xs2!?idx" |
|
927 proof - |
|
928 have "take j xs1 = take ?idx xs1 @ [xs1 ! ?idx]" |
|
929 using eq_xs1 Suc_diff_1 lt_i lt_j take_Suc_conv_app_nth by fastforce |
|
930 moreover have eq_tk2: "take j xs2 = take ?idx xs2 @ [xs2 ! ?idx]" |
|
931 using Suc_diff_1 lt_i' lt_j take_Suc_conv_app_nth by fastforce |
|
932 ultimately show ?thesis using eq_take h1 by auto |
|
933 qed |
|
934 show ?thesis |
|
935 proof(cases " take (j - 1) xs1 = []") |
|
936 case True |
|
937 have "(x, xs1!?idx) \<in> r" |
|
938 proof - |
|
939 from eq_xs1[unfolded True, simplified, symmetric] assms(1) |
|
940 have "rpath r x ( xs1 ! ?idx # drop (Suc ?idx) xs1) x1" by simp |
|
941 from this[unfolded rpath_def] |
|
942 show ?thesis by (auto simp:pred_of_def) |
|
943 qed |
|
944 moreover have "(x, xs2!?idx) \<in> r" |
|
945 proof - |
|
946 from eq_xs2[folded eq_take, unfolded True, simplified, symmetric] assms(2) |
|
947 have "rpath r x ( xs2 ! ?idx # drop (Suc ?idx) xs2) x2" by simp |
|
948 from this[unfolded rpath_def] |
|
949 show ?thesis by (auto simp:pred_of_def) |
|
950 qed |
|
951 ultimately show ?thesis using neq_idx sgv[unfolded single_valued_def] by metis |
|
952 next |
|
953 case False |
|
954 then obtain e es where eq_es: "take ?idx xs1 = es@[e]" |
|
955 using rev_exhaust by blast |
|
956 have "(e, xs1!?idx) \<in> r" |
|
957 proof - |
|
958 from eq_xs1[unfolded eq_es] |
|
959 have "xs1 = es@[e, xs1!?idx]@drop (Suc ?idx) xs1" by simp |
|
960 hence "(e, xs1!?idx) \<in> edges_on xs1" by (simp add:edges_on_def, metis) |
|
961 with rpath_edges_on[OF assms(1)] edges_on_Cons_mono[of xs1 x] |
|
962 show ?thesis by auto |
|
963 qed moreover have "(e, xs2!?idx) \<in> r" |
|
964 proof - |
|
965 from eq_xs2[folded eq_take, unfolded eq_es] |
|
966 have "xs2 = es@[e, xs2!?idx]@drop (Suc ?idx) xs2" by simp |
|
967 hence "(e, xs2!?idx) \<in> edges_on xs2" by (simp add:edges_on_def, metis) |
|
968 with rpath_edges_on[OF assms(2)] edges_on_Cons_mono[of xs2 x] |
|
969 show ?thesis by auto |
|
970 qed |
|
971 ultimately show ?thesis |
|
972 using sgv[unfolded single_valued_def] neq_idx by metis |
|
973 qed |
|
974 qed |
|
975 } thus ?thesis by auto |
|
976 qed |
|
977 from this[rule_format, of "length xs1"] |
|
978 have "take (length xs1) xs1 = take (length xs1) xs2" by simp |
|
979 moreover have "xs2 = take (length xs1) xs2 @ drop (length xs1) xs2" by simp |
|
980 ultimately have "xs2 = xs1 @ drop (length xs1) xs2" by auto |
|
981 from that[OF this] show ?thesis . |
891 qed |
982 qed |
892 |
983 |
893 lemma rpath_overlap_oneside: (* ddd *) |
984 lemma rpath_overlap_oneside: (* ddd *) |
894 assumes "rpath r x xs1 x1" |
985 assumes "rpath r x xs1 x1" |
895 and "rpath r x xs2 x2" |
986 and "rpath r x xs2 x2" |
1743 assumes "x \<notin> Range r'" |
1834 assumes "x \<notin> Range r'" |
1744 shows "children (r \<union> r') x = children r x" |
1835 shows "children (r \<union> r') x = children r x" |
1745 using assms |
1836 using assms |
1746 by (auto simp:children_def) |
1837 by (auto simp:children_def) |
1747 |
1838 |
|
1839 lemma wf_rbase: |
|
1840 assumes "wf r" |
|
1841 obtains b where "(b, a) \<in> r^*" "\<forall> c. (c, b) \<notin> r" |
|
1842 proof - |
|
1843 from assms |
|
1844 have "\<exists> b. (b, a) \<in> r^* \<and> (\<forall> c. (c, b) \<notin> r)" |
|
1845 proof(induct) |
|
1846 case (less x) |
|
1847 thus ?case |
|
1848 proof(cases "\<exists> z. (z, x) \<in> r") |
|
1849 case False |
|
1850 moreover have "(x, x) \<in> r^*" by auto |
|
1851 ultimately show ?thesis by metis |
|
1852 next |
|
1853 case True |
|
1854 then obtain z where h_z: "(z, x) \<in> r" by auto |
|
1855 from less[OF this] |
|
1856 obtain b where "(b, z) \<in> r^*" "(\<forall>c. (c, b) \<notin> r)" |
|
1857 by auto |
|
1858 moreover from this(1) h_z have "(b, x) \<in> r^*" by auto |
|
1859 ultimately show ?thesis by metis |
|
1860 qed |
|
1861 qed |
|
1862 with that show ?thesis by metis |
|
1863 qed |
|
1864 |
|
1865 lemma wf_base: |
|
1866 assumes "wf r" |
|
1867 and "a \<in> Range r" |
|
1868 obtains b where "(b, a) \<in> r^+" "\<forall> c. (c, b) \<notin> r" |
|
1869 proof - |
|
1870 from assms(2) obtain a' where h_a: "(a', a) \<in> r" by auto |
|
1871 from wf_rbase[OF assms(1), of a] |
|
1872 obtain b where h_b: "(b, a) \<in> r\<^sup>*" "\<forall>c. (c, b) \<notin> r" by auto |
|
1873 from rtranclD[OF this(1)] |
|
1874 have "b = a \<or> b \<noteq> a \<and> (b, a) \<in> r\<^sup>+" by auto |
|
1875 moreover have "b \<noteq> a" using h_a h_b(2) by auto |
|
1876 ultimately have "(b, a) \<in> r\<^sup>+" by auto |
|
1877 with h_b(2) and that show ?thesis by metis |
|
1878 qed |
|
1879 |
1748 end |
1880 end |