--- a/src/HOL/Data_Structures/Tree23_Set.thy Thu Jul 07 09:24:03 2016 +0200
+++ b/src/HOL/Data_Structures/Tree23_Set.thy Thu Jul 07 18:08:02 2016 +0200
@@ -9,7 +9,7 @@
Set_by_Ordered
begin
-fun isin :: "'a::cmp tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
+fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
"isin Leaf x = False" |
"isin (Node2 l a r) x =
(case cmp x a of
@@ -32,7 +32,7 @@
"tree\<^sub>i (T\<^sub>i t) = t" |
"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
-fun ins :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
+fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
"ins x (Node2 l a r) =
(case cmp x a of
@@ -66,7 +66,7 @@
hide_const insert
-definition insert :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
"insert x t = tree\<^sub>i(ins x t)"
datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
@@ -108,7 +108,7 @@
"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
-fun del :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
+fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
"del x Leaf = T\<^sub>d Leaf" |
"del x (Node2 Leaf a Leaf) =
(if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
@@ -131,7 +131,7 @@
EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
GT \<Rightarrow> node33 l a m b (del x r)))"
-definition delete :: "'a::cmp \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
+definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
"delete x t = tree\<^sub>d(del x t)"