author | blanchet |
Thu, 24 Mar 2011 17:49:27 +0100 | |
changeset 42103 | 6066a35f6678 |
parent 41144 | 509e51b7509a |
permissions | -rw-r--r-- |
41141
ad923cdd4a5d
added example to exercise higher-order reasoning with Sledgehammer and Metis
blanchet
parents:
39246
diff
changeset
|
1 |
(* Title: HOL/Metis_Examples/BT.thy |
23449 | 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 |
|
41144 | 5 |
Testing Metis. |
23449 | 6 |
*) |
7 |
||
8 |
header {* Binary trees *} |
|
9 |
||
27104
791607529f6d
rep_datatype command now takes list of constructors as input arguments
haftmann
parents:
26312
diff
changeset
|
10 |
theory BT |
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 |
||
38991 | 58 |
declare [[ sledgehammer_problem_prefix = "BT__n_leaves_reflect" ]] |
36484 | 59 |
|
23449 | 60 |
lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" |
36484 | 61 |
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
|
62 |
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
|
63 |
proof - |
50fd056cc3ce
insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs
blanchet
parents:
36484
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
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
|
67 |
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
|
68 |
qed |
36484 | 69 |
next |
70 |
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
|
71 |
by (metis n_leaves.simps(2) nat_add_commute reflect.simps(2)) |
36484 | 72 |
qed |
23449 | 73 |
|
38991 | 74 |
declare [[ sledgehammer_problem_prefix = "BT__n_nodes_reflect" ]] |
36484 | 75 |
|
23449 | 76 |
lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" |
36484 | 77 |
proof (induct t) |
78 |
case Lf thus ?case by (metis reflect.simps(1)) |
|
79 |
next |
|
80 |
case (Br a t1 t2) thus ?case |
|
36844 | 81 |
by (metis add_commute n_nodes.simps(2) reflect.simps(2)) |
36484 | 82 |
qed |
23449 | 83 |
|
38991 | 84 |
declare [[ sledgehammer_problem_prefix = "BT__depth_reflect" ]] |
36484 | 85 |
|
23449 | 86 |
lemma depth_reflect: "depth (reflect t) = depth t" |
36484 | 87 |
apply (induct t) |
88 |
apply (metis depth.simps(1) reflect.simps(1)) |
|
89 |
by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2)) |
|
23449 | 90 |
|
91 |
text {* |
|
36484 | 92 |
The famous relationship between the numbers of leaves and nodes. |
23449 | 93 |
*} |
94 |
||
38991 | 95 |
declare [[ sledgehammer_problem_prefix = "BT__n_leaves_nodes" ]] |
36484 | 96 |
|
23449 | 97 |
lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" |
36484 | 98 |
apply (induct t) |
99 |
apply (metis n_leaves.simps(1) n_nodes.simps(1)) |
|
100 |
by auto |
|
23449 | 101 |
|
38991 | 102 |
declare [[ sledgehammer_problem_prefix = "BT__reflect_reflect_ident" ]] |
36484 | 103 |
|
23449 | 104 |
lemma reflect_reflect_ident: "reflect (reflect t) = t" |
36484 | 105 |
apply (induct t) |
106 |
apply (metis reflect.simps(1)) |
|
107 |
proof - |
|
108 |
fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt" |
|
109 |
assume A1: "reflect (reflect t1) = t1" |
|
110 |
assume A2: "reflect (reflect t2) = t2" |
|
111 |
have "\<And>V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)" |
|
112 |
using A1 by (metis reflect.simps(2)) |
|
113 |
hence "\<And>V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))" |
|
114 |
by (metis reflect.simps(2)) |
|
115 |
hence "\<And>U. reflect (reflect (Br U t1 t2)) = Br U t1 t2" |
|
116 |
using A2 by metis |
|
117 |
thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast |
|
118 |
qed |
|
23449 | 119 |
|
38991 | 120 |
declare [[ sledgehammer_problem_prefix = "BT__bt_map_ident" ]] |
36484 | 121 |
|
23449 | 122 |
lemma bt_map_ident: "bt_map (%x. x) = (%y. y)" |
123 |
apply (rule ext) |
|
124 |
apply (induct_tac y) |
|
36484 | 125 |
apply (metis bt_map.simps(1)) |
36571 | 126 |
by (metis bt_map.simps(2)) |
23449 | 127 |
|
39246 | 128 |
declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]] |
36484 | 129 |
|
39246 | 130 |
lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)" |
23449 | 131 |
apply (induct t) |
39246 | 132 |
apply (metis append.simps(1) bt_map.simps(1)) |
133 |
by (metis append.simps(2) bt_map.simps(2)) |
|
23449 | 134 |
|
38991 | 135 |
declare [[ sledgehammer_problem_prefix = "BT__bt_map_compose" ]] |
36484 | 136 |
|
23449 | 137 |
lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)" |
36484 | 138 |
apply (induct t) |
139 |
apply (metis bt_map.simps(1)) |
|
140 |
by (metis bt_map.simps(2) o_eq_dest_lhs) |
|
23449 | 141 |
|
38991 | 142 |
declare [[ sledgehammer_problem_prefix = "BT__bt_map_reflect" ]] |
36484 | 143 |
|
23449 | 144 |
lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" |
36484 | 145 |
apply (induct t) |
146 |
apply (metis bt_map.simps(1) reflect.simps(1)) |
|
147 |
by (metis bt_map.simps(2) reflect.simps(2)) |
|
23449 | 148 |
|
38991 | 149 |
declare [[ sledgehammer_problem_prefix = "BT__preorder_bt_map" ]] |
36484 | 150 |
|
23449 | 151 |
lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" |
36484 | 152 |
apply (induct t) |
153 |
apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1)) |
|
154 |
by simp |
|
23449 | 155 |
|
38991 | 156 |
declare [[ sledgehammer_problem_prefix = "BT__inorder_bt_map" ]] |
36484 | 157 |
|
23449 | 158 |
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" |
36484 | 159 |
proof (induct t) |
160 |
case Lf thus ?case |
|
161 |
proof - |
|
162 |
have "map f [] = []" by (metis map.simps(1)) |
|
163 |
hence "map f [] = inorder Lf" by (metis inorder.simps(1)) |
|
164 |
hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1)) |
|
165 |
thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1)) |
|
166 |
qed |
|
167 |
next |
|
168 |
case (Br a t1 t2) thus ?case by simp |
|
169 |
qed |
|
23449 | 170 |
|
38991 | 171 |
declare [[ sledgehammer_problem_prefix = "BT__postorder_bt_map" ]] |
36484 | 172 |
|
23449 | 173 |
lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" |
36484 | 174 |
apply (induct t) |
175 |
apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1)) |
|
176 |
by simp |
|
23449 | 177 |
|
38991 | 178 |
declare [[ sledgehammer_problem_prefix = "BT__depth_bt_map" ]] |
36484 | 179 |
|
23449 | 180 |
lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" |
36484 | 181 |
apply (induct t) |
182 |
apply (metis bt_map.simps(1) depth.simps(1)) |
|
183 |
by simp |
|
23449 | 184 |
|
38991 | 185 |
declare [[ sledgehammer_problem_prefix = "BT__n_leaves_bt_map" ]] |
36484 | 186 |
|
23449 | 187 |
lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" |
36484 | 188 |
apply (induct t) |
189 |
apply (metis bt_map.simps(1) n_leaves.simps(1)) |
|
190 |
proof - |
|
191 |
fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt" |
|
192 |
assume A1: "n_leaves (bt_map f t1) = n_leaves t1" |
|
193 |
assume A2: "n_leaves (bt_map f t2) = n_leaves t2" |
|
194 |
have "\<And>V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V" |
|
195 |
using A1 by (metis n_leaves.simps(2)) |
|
196 |
hence "\<And>V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)" |
|
197 |
by (metis bt_map.simps(2)) |
|
198 |
hence F1: "\<And>U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2" |
|
199 |
using A2 by metis |
|
200 |
have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)" |
|
201 |
by (metis n_leaves.simps(2)) |
|
202 |
thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)" |
|
203 |
using F1 by metis |
|
204 |
qed |
|
23449 | 205 |
|
38991 | 206 |
declare [[ sledgehammer_problem_prefix = "BT__preorder_reflect" ]] |
36484 | 207 |
|
23449 | 208 |
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" |
36484 | 209 |
apply (induct t) |
210 |
apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) |
|
211 |
reflect.simps(1)) |
|
39246 | 212 |
apply simp |
213 |
done |
|
23449 | 214 |
|
38991 | 215 |
declare [[ sledgehammer_problem_prefix = "BT__inorder_reflect" ]] |
36484 | 216 |
|
23449 | 217 |
lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" |
36484 | 218 |
apply (induct t) |
219 |
apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1)) |
|
220 |
by simp |
|
221 |
(* Slow: |
|
222 |
by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2) |
|
223 |
reflect.simps(2) rev.simps(2) rev_append) |
|
224 |
*) |
|
23449 | 225 |
|
38991 | 226 |
declare [[ sledgehammer_problem_prefix = "BT__postorder_reflect" ]] |
36484 | 227 |
|
23449 | 228 |
lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" |
36484 | 229 |
apply (induct t) |
230 |
apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) |
|
231 |
reflect.simps(1)) |
|
232 |
by (metis preorder_reflect reflect_reflect_ident rev_swap) |
|
23449 | 233 |
|
234 |
text {* |
|
36484 | 235 |
Analogues of the standard properties of the append function for lists. |
23449 | 236 |
*} |
237 |
||
39246 | 238 |
declare [[ sledgehammer_problem_prefix = "BT__append_assoc" ]] |
36484 | 239 |
|
39246 | 240 |
lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)" |
36484 | 241 |
apply (induct t1) |
39246 | 242 |
apply (metis append.simps(1)) |
243 |
by (metis append.simps(2)) |
|
23449 | 244 |
|
39246 | 245 |
declare [[ sledgehammer_problem_prefix = "BT__append_Lf2" ]] |
36484 | 246 |
|
39246 | 247 |
lemma append_Lf2 [simp]: "append t Lf = t" |
36484 | 248 |
apply (induct t) |
39246 | 249 |
apply (metis append.simps(1)) |
250 |
by (metis append.simps(2)) |
|
36484 | 251 |
|
252 |
declare max_add_distrib_left [simp] |
|
23449 | 253 |
|
39246 | 254 |
declare [[ sledgehammer_problem_prefix = "BT__depth_append" ]] |
36484 | 255 |
|
39246 | 256 |
lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2" |
36484 | 257 |
apply (induct t1) |
39246 | 258 |
apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1)) |
36484 | 259 |
by simp |
23449 | 260 |
|
39246 | 261 |
declare [[ sledgehammer_problem_prefix = "BT__n_leaves_append" ]] |
36484 | 262 |
|
39246 | 263 |
lemma n_leaves_append [simp]: |
264 |
"n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" |
|
36484 | 265 |
apply (induct t1) |
39246 | 266 |
apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) |
36484 | 267 |
semiring_norm(111)) |
268 |
by (simp add: left_distrib) |
|
23449 | 269 |
|
39246 | 270 |
declare [[ sledgehammer_problem_prefix = "BT__bt_map_append" ]] |
36484 | 271 |
|
39246 | 272 |
lemma (*bt_map_append:*) |
273 |
"bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" |
|
36484 | 274 |
apply (induct t1) |
39246 | 275 |
apply (metis append.simps(1) bt_map.simps(1)) |
276 |
by (metis bt_map_append) |
|
23449 | 277 |
|
278 |
end |