64 "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)" |
64 "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)" |
65 |
65 |
66 lemma (in linorder) bst_imp_sorted: "bst t \<Longrightarrow> sorted (inorder t)" |
66 lemma (in linorder) bst_imp_sorted: "bst t \<Longrightarrow> sorted (inorder t)" |
67 by (induction t) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans) |
67 by (induction t) (auto simp: sorted_append sorted_Cons intro: less_imp_le less_trans) |
68 |
68 |
|
69 text{* In case there are duplicates: *} |
|
70 |
|
71 fun (in linorder) bst_eq :: "'a tree \<Rightarrow> bool" where |
|
72 "bst_eq \<langle>\<rangle> \<longleftrightarrow> True" | |
|
73 "bst_eq \<langle>l,a,r\<rangle> \<longleftrightarrow> |
|
74 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)" |
|
75 |
|
76 lemma (in linorder) bst_eq_imp_sorted: "bst_eq t \<Longrightarrow> sorted (inorder t)" |
|
77 apply (induction t) |
|
78 apply(simp) |
|
79 by (fastforce simp: sorted_append sorted_Cons intro: less_imp_le less_trans) |
|
80 |
|
81 subsection "Function @{text mirror}" |
|
82 |
|
83 fun mirror :: "'a tree \<Rightarrow> 'a tree" where |
|
84 "mirror \<langle>\<rangle> = Leaf" | |
|
85 "mirror \<langle>l,x,r\<rangle> = \<langle>mirror r, x, mirror l\<rangle>" |
|
86 |
|
87 lemma mirror_Leaf[simp]: "mirror t = \<langle>\<rangle> \<longleftrightarrow> t = \<langle>\<rangle>" |
|
88 by (induction t) simp_all |
|
89 |
|
90 lemma size_mirror[simp]: "size(mirror t) = size t" |
|
91 by (induction t) simp_all |
|
92 |
|
93 lemma size1_mirror[simp]: "size1(mirror t) = size1 t" |
|
94 by (simp add: size1_def) |
|
95 |
|
96 lemma mirror_mirror[simp]: "mirror(mirror t) = t" |
|
97 by (induction t) simp_all |
|
98 |
69 |
99 |
70 subsection "Deletion of the rightmost entry" |
100 subsection "Deletion of the rightmost entry" |
71 |
101 |
72 fun del_rightmost :: "'a tree \<Rightarrow> 'a tree * 'a" where |
102 fun del_rightmost :: "'a tree \<Rightarrow> 'a tree * 'a" where |
73 "del_rightmost \<langle>l, a, \<langle>\<rangle>\<rangle> = (l,a)" | |
103 "del_rightmost \<langle>l, a, \<langle>\<rangle>\<rangle> = (l,a)" | |