equal
deleted
inserted
replaced
1 (* Author: Tobias Nipkow *) |
1 (* Author: Tobias Nipkow *) |
2 |
2 |
3 section {* Binary Tree *} |
3 section \<open>Binary Tree\<close> |
4 |
4 |
5 theory Tree |
5 theory Tree |
6 imports Main |
6 imports Main |
7 begin |
7 begin |
8 |
8 |
12 where |
12 where |
13 "left Leaf = Leaf" |
13 "left Leaf = Leaf" |
14 | "right Leaf = Leaf" |
14 | "right Leaf = Leaf" |
15 datatype_compat tree |
15 datatype_compat tree |
16 |
16 |
17 text{* Can be seen as counting the number of leaves rather than nodes: *} |
17 text\<open>Can be seen as counting the number of leaves rather than nodes:\<close> |
18 |
18 |
19 definition size1 :: "'a tree \<Rightarrow> nat" where |
19 definition size1 :: "'a tree \<Rightarrow> nat" where |
20 "size1 t = size t + 1" |
20 "size1 t = size t + 1" |
21 |
21 |
22 lemma size1_simps[simp]: |
22 lemma size1_simps[simp]: |
90 |
90 |
91 lemma inorder_map: "inorder (map_tree f t) = map f (inorder t)" |
91 lemma inorder_map: "inorder (map_tree f t) = map f (inorder t)" |
92 by (induction t) auto |
92 by (induction t) auto |
93 |
93 |
94 |
94 |
95 subsection {* Binary Search Tree predicate *} |
95 subsection \<open>Binary Search Tree predicate\<close> |
96 |
96 |
97 fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where |
97 fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where |
98 "bst \<langle>\<rangle> \<longleftrightarrow> True" | |
98 "bst \<langle>\<rangle> \<longleftrightarrow> True" | |
99 "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)" |
99 "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)" |
100 |
100 |
101 text{* In case there are duplicates: *} |
101 text\<open>In case there are duplicates:\<close> |
102 |
102 |
103 fun (in linorder) bst_eq :: "'a tree \<Rightarrow> bool" where |
103 fun (in linorder) bst_eq :: "'a tree \<Rightarrow> bool" where |
104 "bst_eq \<langle>\<rangle> \<longleftrightarrow> True" | |
104 "bst_eq \<langle>\<rangle> \<longleftrightarrow> True" | |
105 "bst_eq \<langle>l,a,r\<rangle> \<longleftrightarrow> |
105 "bst_eq \<langle>l,a,r\<rangle> \<longleftrightarrow> |
106 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)" |
106 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)" |