# HG changeset patch # User nipkow # Date 1580750579 -3600 # Node ID 63b2789259e7b09789788289746f0b155e5be4dc # Parent c26de1bd7b0037cf6c630ad6d1819c70ff0d31de tuned diff -r c26de1bd7b00 -r 63b2789259e7 src/HOL/Data_Structures/Interval_Tree.thy --- a/src/HOL/Data_Structures/Interval_Tree.thy Mon Feb 03 16:49:44 2020 +0100 +++ b/src/HOL/Data_Structures/Interval_Tree.thy Mon Feb 03 18:22:59 2020 +0100 @@ -40,21 +40,21 @@ instantiation ivl :: (linorder) linorder begin -definition int_less: "(x < y) = (low x < low y | (low x = low y \ high x < high y))" -definition int_less_eq: "(x \ y) = (low x < low y | (low x = low y \ high x \ high y))" +definition ivl_less: "(x < y) = (low x < low y | (low x = low y \ high x < high y))" +definition ivl_less_eq: "(x \ y) = (low x < low y | (low x = low y \ high x \ high y))" instance proof fix x y z :: "'a ivl" show a: "(x < y) = (x \ y \ \ y \ x)" - using int_less int_less_eq by force + using ivl_less ivl_less_eq by force show b: "x \ x" - by (simp add: int_less_eq) + by (simp add: ivl_less_eq) show c: "x \ y \ y \ z \ x \ z" - by (smt int_less_eq dual_order.trans less_trans) + by (smt ivl_less_eq dual_order.trans less_trans) show d: "x \ y \ y \ x \ x = y" - using int_less_eq a ivl_inj int_less by fastforce + using ivl_less_eq a ivl_inj ivl_less by fastforce show e: "x \ y \ y \ x" - by (meson int_less_eq leI not_less_iff_gr_or_eq) + by (meson ivl_less_eq leI not_less_iff_gr_or_eq) qed end @@ -234,7 +234,7 @@ have "p \ set (inorder l)" using p(1) by (simp) moreover have "rp \ set (inorder r)" using asm by (simp) ultimately have "low p \ low rp" - using Node(4) by(fastforce simp: sorted_wrt_append int_less) + using Node(4) by(fastforce simp: sorted_wrt_append ivl_less) then show ?thesis using False by (auto simp: overlap_def) qed