# HG changeset patch
# User nipkow
# Date 1504624062 -7200
# Node ID f23f044148d308da3a597a047c49a679c6651772
# Parent  1af360d1cad257a3302621ee9f9bed14d4476c96
introduced bst_wrt

diff -r 1af360d1cad2 -r f23f044148d3 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Tue Sep 05 14:29:43 2017 +0200
+++ b/src/HOL/Library/Tree.thy	Tue Sep 05 17:07:42 2017 +0200
@@ -77,15 +77,13 @@
 "postorder \<langle>l, x, r\<rangle> = postorder l @ postorder r @ [x]"
 
 text\<open>Binary Search Tree:\<close>
-fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where
-"bst \<langle>\<rangle> \<longleftrightarrow> True" |
-"bst \<langle>l, a, r\<rangle> \<longleftrightarrow> bst l \<and> bst r \<and> (\<forall>x\<in>set_tree l. x < a) \<and> (\<forall>x\<in>set_tree r. a < x)"
+fun bst_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool" where
+"bst_wrt P \<langle>\<rangle> \<longleftrightarrow> True" |
+"bst_wrt P \<langle>l, a, r\<rangle> \<longleftrightarrow>
+ bst_wrt P l \<and> bst_wrt P r \<and> (\<forall>x\<in>set_tree l. P x a) \<and> (\<forall>x\<in>set_tree r. P a x)"
 
-text\<open>Binary Search Tree with duplicates:\<close>
-fun (in linorder) bst_eq :: "'a tree \<Rightarrow> bool" where
-"bst_eq \<langle>\<rangle> \<longleftrightarrow> True" |
-"bst_eq \<langle>l,a,r\<rangle> \<longleftrightarrow>
- bst_eq l \<and> bst_eq r \<and> (\<forall>x\<in>set_tree l. x \<le> a) \<and> (\<forall>x\<in>set_tree r. a \<le> x)"
+abbreviation bst :: "('a::linorder) tree \<Rightarrow> bool" where
+"bst \<equiv> bst_wrt (op <)"
 
 fun (in linorder) heap :: "'a tree \<Rightarrow> bool" where
 "heap Leaf = True" |
@@ -439,24 +437,21 @@
 
 subsection \<open>Binary Search Tree\<close>
 
-lemma (in linorder) bst_eq_if_bst: "bst t \<Longrightarrow> bst_eq t"
+lemma bst_wrt_mono: "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> bst_wrt P t \<Longrightarrow> bst_wrt Q t"
 by (induction t) (auto)
 
-lemma (in linorder) bst_eq_imp_sorted: "bst_eq t \<Longrightarrow> sorted (inorder t)"
+lemma bst_wrt_le_if_bst: "bst t \<Longrightarrow> bst_wrt (op \<le>) t"
+using bst_wrt_mono less_imp_le by blast
+
+lemma bst_wrt_le_iff_sorted: "bst_wrt (op \<le>) t \<longleftrightarrow> sorted (inorder t)"
 apply (induction t)
  apply(simp)
 by (fastforce simp: sorted_append sorted_Cons intro: less_imp_le less_trans)
 
-lemma (in linorder) distinct_preorder_if_bst: "bst t \<Longrightarrow> distinct (preorder t)"
+lemma bst_iff_sorted_wrt_less: "bst t \<longleftrightarrow> sorted_wrt (op <) (inorder t)"
 apply (induction t)
  apply simp
-apply(fastforce elim: order.asym)
-done
-
-lemma (in linorder) distinct_inorder_if_bst: "bst t \<Longrightarrow> distinct (inorder t)"
-apply (induction t)
- apply simp
-apply(fastforce elim: order.asym)
+apply (fastforce simp: sorted_wrt_Cons sorted_wrt_append)
 done