equal
deleted
inserted
replaced
128 apply (metis bt_map.simps(1) reflect.simps(1)) |
128 apply (metis bt_map.simps(1) reflect.simps(1)) |
129 by (metis bt_map.simps(2) reflect.simps(2)) |
129 by (metis bt_map.simps(2) reflect.simps(2)) |
130 |
130 |
131 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" |
131 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" |
132 apply (induct t) |
132 apply (induct t) |
133 apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1)) |
133 apply (metis bt_map.simps(1) list.map(1) preorder.simps(1)) |
134 by simp |
134 by simp |
135 |
135 |
136 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" |
136 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" |
137 proof (induct t) |
137 proof (induct t) |
138 case Lf thus ?case |
138 case Lf thus ?case |
139 proof - |
139 proof - |
140 have "map f [] = []" by (metis map.simps(1)) |
140 have "map f [] = []" by (metis list.map(1)) |
141 hence "map f [] = inorder Lf" by (metis inorder.simps(1)) |
141 hence "map f [] = inorder Lf" by (metis inorder.simps(1)) |
142 hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1)) |
142 hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1)) |
143 thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1)) |
143 thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1)) |
144 qed |
144 qed |
145 next |
145 next |