author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45705  a25ff4283352 
child 49962  a8cc904a6820 
permissions  rwrr 
43197  1 
(* Title: HOL/Metis_Examples/Binary_Tree.thy 
2 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 

36487
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset

3 
Author: Jasmin Blanchette, TU Muenchen 
23449  4 

43197  5 
Metis example featuring binary trees. 
23449  6 
*) 
7 

43197  8 
header {* Metis Example Featuring Binary Trees *} 
23449  9 

43197  10 
theory Binary_Tree 
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26312
diff
changeset

11 
imports Main 
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26312
diff
changeset

12 
begin 
23449  13 

42103
6066a35f6678
Metis examples use the new Skolemizer to test it
blanchet
parents:
41144
diff
changeset

14 
declare [[metis_new_skolemizer]] 
6066a35f6678
Metis examples use the new Skolemizer to test it
blanchet
parents:
41144
diff
changeset

15 

23449  16 
datatype 'a bt = 
17 
Lf 

18 
 Br 'a "'a bt" "'a bt" 

19 

39246  20 
primrec n_nodes :: "'a bt => nat" where 
21 
"n_nodes Lf = 0" 

22 
 "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" 

23 

24 
primrec n_leaves :: "'a bt => nat" where 

25 
"n_leaves Lf = Suc 0" 

26 
 "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" 

23449  27 

39246  28 
primrec depth :: "'a bt => nat" where 
29 
"depth Lf = 0" 

30 
 "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" 

23449  31 

39246  32 
primrec reflect :: "'a bt => 'a bt" where 
33 
"reflect Lf = Lf" 

34 
 "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" 

23449  35 

39246  36 
primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where 
23449  37 
"bt_map f Lf = Lf" 
39246  38 
 "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" 
23449  39 

39246  40 
primrec preorder :: "'a bt => 'a list" where 
23449  41 
"preorder Lf = []" 
39246  42 
 "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" 
23449  43 

39246  44 
primrec inorder :: "'a bt => 'a list" where 
23449  45 
"inorder Lf = []" 
39246  46 
 "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" 
23449  47 

39246  48 
primrec postorder :: "'a bt => 'a list" where 
23449  49 
"postorder Lf = []" 
39246  50 
 "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" 
23449  51 

39246  52 
primrec append :: "'a bt => 'a bt => 'a bt" where 
53 
"append Lf t = t" 

54 
 "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" 

23449  55 

56 
text {* \medskip BT simplification *} 

57 

58 
lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" 

36484  59 
proof (induct t) 
36487
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset

60 
case Lf thus ?case 
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset

61 
proof  
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset

62 
let "?p\<^isub>1 x\<^isub>1" = "x\<^isub>1 \<noteq> n_leaves (reflect (Lf::'a bt))" 
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset

63 
have "\<not> ?p\<^isub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1)) 
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset

64 
hence "\<not> ?p\<^isub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1)) 
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset

65 
thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis 
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset

66 
qed 
36484  67 
next 
68 
case (Br a t1 t2) thus ?case 

36487
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset

69 
by (metis n_leaves.simps(2) nat_add_commute reflect.simps(2)) 
36484  70 
qed 
23449  71 

72 
lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" 

36484  73 
proof (induct t) 
74 
case Lf thus ?case by (metis reflect.simps(1)) 

75 
next 

76 
case (Br a t1 t2) thus ?case 

36844  77 
by (metis add_commute n_nodes.simps(2) reflect.simps(2)) 
36484  78 
qed 
23449  79 

80 
lemma depth_reflect: "depth (reflect t) = depth t" 

36484  81 
apply (induct t) 
82 
apply (metis depth.simps(1) reflect.simps(1)) 

83 
by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2)) 

23449  84 

85 
text {* 

36484  86 
The famous relationship between the numbers of leaves and nodes. 
23449  87 
*} 
88 

89 
lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" 

36484  90 
apply (induct t) 
91 
apply (metis n_leaves.simps(1) n_nodes.simps(1)) 

92 
by auto 

23449  93 

94 
lemma reflect_reflect_ident: "reflect (reflect t) = t" 

36484  95 
apply (induct t) 
96 
apply (metis reflect.simps(1)) 

97 
proof  

98 
fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt" 

99 
assume A1: "reflect (reflect t1) = t1" 

100 
assume A2: "reflect (reflect t2) = t2" 

101 
have "\<And>V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)" 

102 
using A1 by (metis reflect.simps(2)) 

103 
hence "\<And>V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))" 

104 
by (metis reflect.simps(2)) 

105 
hence "\<And>U. reflect (reflect (Br U t1 t2)) = Br U t1 t2" 

106 
using A2 by metis 

107 
thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast 

108 
qed 

23449  109 

110 
lemma bt_map_ident: "bt_map (%x. x) = (%y. y)" 

43197  111 
apply (rule ext) 
23449  112 
apply (induct_tac y) 
36484  113 
apply (metis bt_map.simps(1)) 
36571  114 
by (metis bt_map.simps(2)) 
23449  115 

39246  116 
lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)" 
23449  117 
apply (induct t) 
39246  118 
apply (metis append.simps(1) bt_map.simps(1)) 
119 
by (metis append.simps(2) bt_map.simps(2)) 

23449  120 

121 
lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)" 

36484  122 
apply (induct t) 
123 
apply (metis bt_map.simps(1)) 

124 
by (metis bt_map.simps(2) o_eq_dest_lhs) 

23449  125 

126 
lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" 

36484  127 
apply (induct t) 
128 
apply (metis bt_map.simps(1) reflect.simps(1)) 

129 
by (metis bt_map.simps(2) reflect.simps(2)) 

23449  130 

131 
lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" 

36484  132 
apply (induct t) 
133 
apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1)) 

134 
by simp 

23449  135 

136 
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" 

36484  137 
proof (induct t) 
138 
case Lf thus ?case 

139 
proof  

140 
have "map f [] = []" by (metis map.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)) 

143 
thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1)) 

144 
qed 

145 
next 

146 
case (Br a t1 t2) thus ?case by simp 

147 
qed 

23449  148 

149 
lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" 

36484  150 
apply (induct t) 
151 
apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1)) 

152 
by simp 

23449  153 

154 
lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" 

36484  155 
apply (induct t) 
156 
apply (metis bt_map.simps(1) depth.simps(1)) 

157 
by simp 

23449  158 

159 
lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" 

36484  160 
apply (induct t) 
161 
apply (metis bt_map.simps(1) n_leaves.simps(1)) 

162 
proof  

163 
fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt" 

164 
assume A1: "n_leaves (bt_map f t1) = n_leaves t1" 

165 
assume A2: "n_leaves (bt_map f t2) = n_leaves t2" 

166 
have "\<And>V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V" 

167 
using A1 by (metis n_leaves.simps(2)) 

168 
hence "\<And>V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)" 

169 
by (metis bt_map.simps(2)) 

170 
hence F1: "\<And>U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2" 

171 
using A2 by metis 

172 
have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)" 

173 
by (metis n_leaves.simps(2)) 

174 
thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)" 

175 
using F1 by metis 

176 
qed 

23449  177 

178 
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" 

36484  179 
apply (induct t) 
180 
apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) 

181 
reflect.simps(1)) 

39246  182 
apply simp 
183 
done 

23449  184 

185 
lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" 

36484  186 
apply (induct t) 
187 
apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1)) 

188 
by simp 

189 
(* Slow: 

190 
by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2) 

191 
reflect.simps(2) rev.simps(2) rev_append) 

192 
*) 

23449  193 

194 
lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" 

36484  195 
apply (induct t) 
196 
apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) 

197 
reflect.simps(1)) 

198 
by (metis preorder_reflect reflect_reflect_ident rev_swap) 

23449  199 

200 
text {* 

36484  201 
Analogues of the standard properties of the append function for lists. 
23449  202 
*} 
203 

39246  204 
lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)" 
36484  205 
apply (induct t1) 
39246  206 
apply (metis append.simps(1)) 
207 
by (metis append.simps(2)) 

23449  208 

39246  209 
lemma append_Lf2 [simp]: "append t Lf = t" 
36484  210 
apply (induct t) 
39246  211 
apply (metis append.simps(1)) 
212 
by (metis append.simps(2)) 

36484  213 

214 
declare max_add_distrib_left [simp] 

23449  215 

39246  216 
lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2" 
36484  217 
apply (induct t1) 
39246  218 
apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1)) 
36484  219 
by simp 
23449  220 

39246  221 
lemma n_leaves_append [simp]: 
222 
"n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" 

36484  223 
apply (induct t1) 
39246  224 
apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) 
45502
6246bef495ff
avoid theorem references like 'semiring_norm(111)'
huffman
parents:
43197
diff
changeset

225 
Suc_eq_plus1) 
36484  226 
by (simp add: left_distrib) 
23449  227 

39246  228 
lemma (*bt_map_append:*) 
229 
"bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" 

36484  230 
apply (induct t1) 
39246  231 
apply (metis append.simps(1) bt_map.simps(1)) 
232 
by (metis bt_map_append) 

23449  233 

234 
end 