summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 04 Feb 2020 16:36:49 +0100 | |

changeset 71416 | 6a1c1d1ce6ae |

parent 71415 | 63b2789259e7 |

child 71417 | 89d05db6dd1f |

tuned

--- a/src/HOL/Data_Structures/Interval_Tree.thy Mon Feb 03 18:22:59 2020 +0100 +++ b/src/HOL/Data_Structures/Interval_Tree.thy Tue Feb 04 16:36:49 2020 +0100 @@ -231,16 +231,14 @@ case False have "\<not>overlap x rp" if asm: "rp \<in> set_tree r" for rp proof - - have "p \<in> set (inorder l)" using p(1) by (simp) - moreover have "rp \<in> set (inorder r)" using asm by (simp) - ultimately have "low p \<le> low rp" - using Node(4) by(fastforce simp: sorted_wrt_append ivl_less) + have "low p \<le> low rp" + using asm p(1) Node(4) by(fastforce simp: sorted_wrt_append ivl_less) then show ?thesis using False by (auto simp: overlap_def) qed then show ?thesis unfolding search_eval search_l - using a_disjoint by (fastforce simp: has_overlap_def overlap_def) + using a_disjoint by (auto simp: has_overlap_def overlap_def) qed next case False @@ -251,7 +249,7 @@ by (fastforce simp: overlap_def) then show ?thesis unfolding search_eval search_r - using a_disjoint by (fastforce simp: has_overlap_def overlap_def) + using a_disjoint by (auto simp: has_overlap_def overlap_def) qed qed qed