28 by (cases t) auto |
28 by (cases t) auto |
29 |
29 |
30 lemma finite_set_tree[simp]: "finite(set_tree t)" |
30 lemma finite_set_tree[simp]: "finite(set_tree t)" |
31 by(induction t) auto |
31 by(induction t) auto |
32 |
32 |
|
33 lemma size_map_tree[simp]: "size (map_tree f t) = size t" |
|
34 by (induction t) auto |
|
35 |
|
36 lemma size1_map_tree[simp]: "size1 (map_tree f t) = size1 t" |
|
37 by (simp add: size1_def) |
|
38 |
|
39 |
|
40 subsection "The depth" |
|
41 |
|
42 fun depth :: "'a tree => nat" where |
|
43 "depth Leaf = 0" | |
|
44 "depth (Node t1 a t2) = Suc (max (depth t1) (depth t2))" |
|
45 |
|
46 lemma depth_map_tree[simp]: "depth (map_tree f t) = depth t" |
|
47 by (induction t) auto |
|
48 |
33 |
49 |
34 subsection "The set of subtrees" |
50 subsection "The set of subtrees" |
35 |
51 |
36 fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where |
52 fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where |
37 "subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" | |
53 "subtrees \<langle>\<rangle> = {\<langle>\<rangle>}" | |
45 |
61 |
46 lemma in_set_tree_if: "\<langle>l, a, r\<rangle> \<in> subtrees t \<Longrightarrow> a \<in> set_tree t" |
62 lemma in_set_tree_if: "\<langle>l, a, r\<rangle> \<in> subtrees t \<Longrightarrow> a \<in> set_tree t" |
47 by (metis Node_notin_subtrees_if) |
63 by (metis Node_notin_subtrees_if) |
48 |
64 |
49 |
65 |
50 subsection "Inorder list of entries" |
66 subsection "List of entries" |
|
67 |
|
68 fun preorder :: "'a tree \<Rightarrow> 'a list" where |
|
69 "preorder \<langle>\<rangle> = []" | |
|
70 "preorder \<langle>l, x, r\<rangle> = x # preorder l @ preorder r" |
51 |
71 |
52 fun inorder :: "'a tree \<Rightarrow> 'a list" where |
72 fun inorder :: "'a tree \<Rightarrow> 'a list" where |
53 "inorder \<langle>\<rangle> = []" | |
73 "inorder \<langle>\<rangle> = []" | |
54 "inorder \<langle>l, x, r\<rangle> = inorder l @ [x] @ inorder r" |
74 "inorder \<langle>l, x, r\<rangle> = inorder l @ [x] @ inorder r" |
55 |
75 |
56 lemma set_inorder[simp]: "set (inorder t) = set_tree t" |
76 lemma set_inorder[simp]: "set (inorder t) = set_tree t" |
|
77 by (induction t) auto |
|
78 |
|
79 lemma set_preorder[simp]: "set (preorder t) = set_tree t" |
|
80 by (induction t) auto |
|
81 |
|
82 lemma length_preorder[simp]: "length (preorder t) = size t" |
|
83 by (induction t) auto |
|
84 |
|
85 lemma length_inorder[simp]: "length (inorder t) = size t" |
|
86 by (induction t) auto |
|
87 |
|
88 lemma preorder_map: "preorder (map_tree f t) = map f (preorder t)" |
|
89 by (induction t) auto |
|
90 |
|
91 lemma inorder_map: "inorder (map_tree f t) = map f (inorder t)" |
57 by (induction t) auto |
92 by (induction t) auto |
58 |
93 |
59 |
94 |
60 subsection {* Binary Search Tree predicate *} |
95 subsection {* Binary Search Tree predicate *} |
61 |
96 |
76 lemma (in linorder) bst_eq_imp_sorted: "bst_eq t \<Longrightarrow> sorted (inorder t)" |
111 lemma (in linorder) bst_eq_imp_sorted: "bst_eq t \<Longrightarrow> sorted (inorder t)" |
77 apply (induction t) |
112 apply (induction t) |
78 apply(simp) |
113 apply(simp) |
79 by (fastforce simp: sorted_append sorted_Cons intro: less_imp_le less_trans) |
114 by (fastforce simp: sorted_append sorted_Cons intro: less_imp_le less_trans) |
80 |
115 |
|
116 |
81 subsection "Function @{text mirror}" |
117 subsection "Function @{text mirror}" |
82 |
118 |
83 fun mirror :: "'a tree \<Rightarrow> 'a tree" where |
119 fun mirror :: "'a tree \<Rightarrow> 'a tree" where |
84 "mirror \<langle>\<rangle> = Leaf" | |
120 "mirror \<langle>\<rangle> = Leaf" | |
85 "mirror \<langle>l,x,r\<rangle> = \<langle>mirror r, x, mirror l\<rangle>" |
121 "mirror \<langle>l,x,r\<rangle> = \<langle>mirror r, x, mirror l\<rangle>" |
90 lemma size_mirror[simp]: "size(mirror t) = size t" |
126 lemma size_mirror[simp]: "size(mirror t) = size t" |
91 by (induction t) simp_all |
127 by (induction t) simp_all |
92 |
128 |
93 lemma size1_mirror[simp]: "size1(mirror t) = size1 t" |
129 lemma size1_mirror[simp]: "size1(mirror t) = size1 t" |
94 by (simp add: size1_def) |
130 by (simp add: size1_def) |
|
131 |
|
132 lemma depth_mirror[simp]: "depth(mirror t) = depth t" |
|
133 by (induction t) simp_all |
|
134 |
|
135 lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)" |
|
136 by (induction t) simp_all |
|
137 |
|
138 lemma map_mirror: "map_tree f (mirror t) = mirror (map_tree f t)" |
|
139 by (induction t) simp_all |
95 |
140 |
96 lemma mirror_mirror[simp]: "mirror(mirror t) = t" |
141 lemma mirror_mirror[simp]: "mirror(mirror t) = t" |
97 by (induction t) simp_all |
142 by (induction t) simp_all |
98 |
143 |
99 |
144 |