src/HOL/Metis_Examples/Binary_Tree.thy
 author haftmann Fri Oct 10 19:55:32 2014 +0200 (2014-10-10) changeset 58646 cd63a4b12a33 parent 58310 91ea607a34d8 child 58889 5b7a9633cfa8 permissions -rw-r--r--
specialized specification: avoid trivial instances
 blanchet@43197 ` 1` ```(* Title: HOL/Metis_Examples/Binary_Tree.thy ``` blanchet@43197 ` 2` ``` Author: Lawrence C. Paulson, Cambridge University Computer Laboratory ``` blanchet@36487 ` 3` ``` Author: Jasmin Blanchette, TU Muenchen ``` paulson@23449 ` 4` blanchet@43197 ` 5` ```Metis example featuring binary trees. ``` paulson@23449 ` 6` ```*) ``` paulson@23449 ` 7` blanchet@43197 ` 8` ```header {* Metis Example Featuring Binary Trees *} ``` paulson@23449 ` 9` blanchet@43197 ` 10` ```theory Binary_Tree ``` haftmann@27104 ` 11` ```imports Main ``` haftmann@27104 ` 12` ```begin ``` paulson@23449 ` 13` blanchet@50705 ` 14` ```declare [[metis_new_skolem]] ``` blanchet@42103 ` 15` blanchet@58310 ` 16` ```datatype 'a bt = ``` paulson@23449 ` 17` ``` Lf ``` paulson@23449 ` 18` ``` | Br 'a "'a bt" "'a bt" ``` paulson@23449 ` 19` haftmann@39246 ` 20` ```primrec n_nodes :: "'a bt => nat" where ``` haftmann@39246 ` 21` ``` "n_nodes Lf = 0" ``` haftmann@39246 ` 22` ```| "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)" ``` haftmann@39246 ` 23` haftmann@39246 ` 24` ```primrec n_leaves :: "'a bt => nat" where ``` haftmann@39246 ` 25` ``` "n_leaves Lf = Suc 0" ``` haftmann@39246 ` 26` ```| "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2" ``` paulson@23449 ` 27` haftmann@39246 ` 28` ```primrec depth :: "'a bt => nat" where ``` haftmann@39246 ` 29` ``` "depth Lf = 0" ``` haftmann@39246 ` 30` ```| "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))" ``` paulson@23449 ` 31` haftmann@39246 ` 32` ```primrec reflect :: "'a bt => 'a bt" where ``` haftmann@39246 ` 33` ``` "reflect Lf = Lf" ``` haftmann@39246 ` 34` ```| "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)" ``` paulson@23449 ` 35` haftmann@39246 ` 36` ```primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where ``` paulson@23449 ` 37` ``` "bt_map f Lf = Lf" ``` haftmann@39246 ` 38` ```| "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)" ``` paulson@23449 ` 39` haftmann@39246 ` 40` ```primrec preorder :: "'a bt => 'a list" where ``` paulson@23449 ` 41` ``` "preorder Lf = []" ``` haftmann@39246 ` 42` ```| "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)" ``` paulson@23449 ` 43` haftmann@39246 ` 44` ```primrec inorder :: "'a bt => 'a list" where ``` paulson@23449 ` 45` ``` "inorder Lf = []" ``` haftmann@39246 ` 46` ```| "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)" ``` paulson@23449 ` 47` haftmann@39246 ` 48` ```primrec postorder :: "'a bt => 'a list" where ``` paulson@23449 ` 49` ``` "postorder Lf = []" ``` haftmann@39246 ` 50` ```| "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]" ``` paulson@23449 ` 51` haftmann@39246 ` 52` ```primrec append :: "'a bt => 'a bt => 'a bt" where ``` haftmann@39246 ` 53` ``` "append Lf t = t" ``` haftmann@39246 ` 54` ```| "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)" ``` paulson@23449 ` 55` paulson@23449 ` 56` ```text {* \medskip BT simplification *} ``` paulson@23449 ` 57` paulson@23449 ` 58` ```lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t" ``` blanchet@36484 ` 59` ```proof (induct t) ``` blanchet@36487 ` 60` ``` case Lf thus ?case ``` blanchet@36487 ` 61` ``` proof - ``` wenzelm@53015 ` 62` ``` let "?p\<^sub>1 x\<^sub>1" = "x\<^sub>1 \ n_leaves (reflect (Lf::'a bt))" ``` wenzelm@53015 ` 63` ``` have "\ ?p\<^sub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1)) ``` wenzelm@53015 ` 64` ``` hence "\ ?p\<^sub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1)) ``` blanchet@36487 ` 65` ``` thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis ``` blanchet@36487 ` 66` ``` qed ``` blanchet@36484 ` 67` ```next ``` blanchet@36484 ` 68` ``` case (Br a t1 t2) thus ?case ``` haftmann@57512 ` 69` ``` by (metis n_leaves.simps(2) add.commute reflect.simps(2)) ``` blanchet@36484 ` 70` ```qed ``` paulson@23449 ` 71` paulson@23449 ` 72` ```lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t" ``` blanchet@36484 ` 73` ```proof (induct t) ``` blanchet@36484 ` 74` ``` case Lf thus ?case by (metis reflect.simps(1)) ``` blanchet@36484 ` 75` ```next ``` blanchet@36484 ` 76` ``` case (Br a t1 t2) thus ?case ``` haftmann@57512 ` 77` ``` by (metis add.commute n_nodes.simps(2) reflect.simps(2)) ``` blanchet@36484 ` 78` ```qed ``` paulson@23449 ` 79` paulson@23449 ` 80` ```lemma depth_reflect: "depth (reflect t) = depth t" ``` blanchet@36484 ` 81` ```apply (induct t) ``` blanchet@36484 ` 82` ``` apply (metis depth.simps(1) reflect.simps(1)) ``` haftmann@54864 ` 83` ```by (metis depth.simps(2) max.commute reflect.simps(2)) ``` paulson@23449 ` 84` paulson@23449 ` 85` ```text {* ``` blanchet@36484 ` 86` ```The famous relationship between the numbers of leaves and nodes. ``` paulson@23449 ` 87` ```*} ``` paulson@23449 ` 88` paulson@23449 ` 89` ```lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)" ``` blanchet@36484 ` 90` ```apply (induct t) ``` blanchet@36484 ` 91` ``` apply (metis n_leaves.simps(1) n_nodes.simps(1)) ``` blanchet@36484 ` 92` ```by auto ``` paulson@23449 ` 93` paulson@23449 ` 94` ```lemma reflect_reflect_ident: "reflect (reflect t) = t" ``` blanchet@36484 ` 95` ```apply (induct t) ``` blanchet@36484 ` 96` ``` apply (metis reflect.simps(1)) ``` blanchet@36484 ` 97` ```proof - ``` blanchet@36484 ` 98` ``` fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt" ``` blanchet@36484 ` 99` ``` assume A1: "reflect (reflect t1) = t1" ``` blanchet@36484 ` 100` ``` assume A2: "reflect (reflect t2) = t2" ``` blanchet@36484 ` 101` ``` have "\V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)" ``` blanchet@36484 ` 102` ``` using A1 by (metis reflect.simps(2)) ``` blanchet@36484 ` 103` ``` hence "\V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))" ``` blanchet@36484 ` 104` ``` by (metis reflect.simps(2)) ``` blanchet@36484 ` 105` ``` hence "\U. reflect (reflect (Br U t1 t2)) = Br U t1 t2" ``` blanchet@36484 ` 106` ``` using A2 by metis ``` blanchet@36484 ` 107` ``` thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast ``` blanchet@36484 ` 108` ```qed ``` paulson@23449 ` 109` paulson@23449 ` 110` ```lemma bt_map_ident: "bt_map (%x. x) = (%y. y)" ``` blanchet@43197 ` 111` ```apply (rule ext) ``` paulson@23449 ` 112` ```apply (induct_tac y) ``` blanchet@36484 ` 113` ``` apply (metis bt_map.simps(1)) ``` blanchet@36571 ` 114` ```by (metis bt_map.simps(2)) ``` paulson@23449 ` 115` haftmann@39246 ` 116` ```lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)" ``` paulson@23449 ` 117` ```apply (induct t) ``` haftmann@39246 ` 118` ``` apply (metis append.simps(1) bt_map.simps(1)) ``` haftmann@39246 ` 119` ```by (metis append.simps(2) bt_map.simps(2)) ``` paulson@23449 ` 120` paulson@23449 ` 121` ```lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)" ``` blanchet@36484 ` 122` ```apply (induct t) ``` blanchet@36484 ` 123` ``` apply (metis bt_map.simps(1)) ``` blanchet@36484 ` 124` ```by (metis bt_map.simps(2) o_eq_dest_lhs) ``` paulson@23449 ` 125` paulson@23449 ` 126` ```lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)" ``` blanchet@36484 ` 127` ```apply (induct t) ``` blanchet@36484 ` 128` ``` apply (metis bt_map.simps(1) reflect.simps(1)) ``` blanchet@36484 ` 129` ```by (metis bt_map.simps(2) reflect.simps(2)) ``` paulson@23449 ` 130` paulson@23449 ` 131` ```lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)" ``` blanchet@36484 ` 132` ```apply (induct t) ``` blanchet@55465 ` 133` ``` apply (metis bt_map.simps(1) list.map(1) preorder.simps(1)) ``` blanchet@36484 ` 134` ```by simp ``` paulson@23449 ` 135` paulson@23449 ` 136` ```lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)" ``` blanchet@36484 ` 137` ```proof (induct t) ``` blanchet@36484 ` 138` ``` case Lf thus ?case ``` blanchet@36484 ` 139` ``` proof - ``` blanchet@55465 ` 140` ``` have "map f [] = []" by (metis list.map(1)) ``` blanchet@36484 ` 141` ``` hence "map f [] = inorder Lf" by (metis inorder.simps(1)) ``` blanchet@36484 ` 142` ``` hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1)) ``` blanchet@36484 ` 143` ``` thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1)) ``` blanchet@36484 ` 144` ``` qed ``` blanchet@36484 ` 145` ```next ``` blanchet@36484 ` 146` ``` case (Br a t1 t2) thus ?case by simp ``` blanchet@36484 ` 147` ```qed ``` paulson@23449 ` 148` paulson@23449 ` 149` ```lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)" ``` blanchet@36484 ` 150` ```apply (induct t) ``` blanchet@36484 ` 151` ``` apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1)) ``` blanchet@36484 ` 152` ```by simp ``` paulson@23449 ` 153` paulson@23449 ` 154` ```lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t" ``` blanchet@36484 ` 155` ```apply (induct t) ``` blanchet@36484 ` 156` ``` apply (metis bt_map.simps(1) depth.simps(1)) ``` blanchet@36484 ` 157` ```by simp ``` paulson@23449 ` 158` paulson@23449 ` 159` ```lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t" ``` blanchet@36484 ` 160` ```apply (induct t) ``` blanchet@36484 ` 161` ``` apply (metis bt_map.simps(1) n_leaves.simps(1)) ``` blanchet@36484 ` 162` ```proof - ``` blanchet@36484 ` 163` ``` fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt" ``` blanchet@36484 ` 164` ``` assume A1: "n_leaves (bt_map f t1) = n_leaves t1" ``` blanchet@36484 ` 165` ``` assume A2: "n_leaves (bt_map f t2) = n_leaves t2" ``` blanchet@36484 ` 166` ``` have "\V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V" ``` blanchet@36484 ` 167` ``` using A1 by (metis n_leaves.simps(2)) ``` blanchet@36484 ` 168` ``` hence "\V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)" ``` blanchet@36484 ` 169` ``` by (metis bt_map.simps(2)) ``` blanchet@36484 ` 170` ``` hence F1: "\U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2" ``` blanchet@36484 ` 171` ``` using A2 by metis ``` blanchet@36484 ` 172` ``` have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)" ``` blanchet@36484 ` 173` ``` by (metis n_leaves.simps(2)) ``` blanchet@36484 ` 174` ``` thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)" ``` blanchet@36484 ` 175` ``` using F1 by metis ``` blanchet@36484 ` 176` ```qed ``` paulson@23449 ` 177` paulson@23449 ` 178` ```lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)" ``` blanchet@36484 ` 179` ```apply (induct t) ``` blanchet@36484 ` 180` ``` apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) ``` blanchet@36484 ` 181` ``` reflect.simps(1)) ``` haftmann@39246 ` 182` ```apply simp ``` haftmann@39246 ` 183` ```done ``` paulson@23449 ` 184` paulson@23449 ` 185` ```lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)" ``` blanchet@36484 ` 186` ```apply (induct t) ``` blanchet@36484 ` 187` ``` apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1)) ``` blanchet@36484 ` 188` ```by simp ``` blanchet@36484 ` 189` ```(* Slow: ``` blanchet@36484 ` 190` ```by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2) ``` blanchet@36484 ` 191` ``` reflect.simps(2) rev.simps(2) rev_append) ``` blanchet@36484 ` 192` ```*) ``` paulson@23449 ` 193` paulson@23449 ` 194` ```lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)" ``` blanchet@36484 ` 195` ```apply (induct t) ``` blanchet@36484 ` 196` ``` apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1) ``` blanchet@36484 ` 197` ``` reflect.simps(1)) ``` blanchet@36484 ` 198` ```by (metis preorder_reflect reflect_reflect_ident rev_swap) ``` paulson@23449 ` 199` paulson@23449 ` 200` ```text {* ``` blanchet@36484 ` 201` ```Analogues of the standard properties of the append function for lists. ``` paulson@23449 ` 202` ```*} ``` paulson@23449 ` 203` haftmann@39246 ` 204` ```lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)" ``` blanchet@36484 ` 205` ```apply (induct t1) ``` haftmann@39246 ` 206` ``` apply (metis append.simps(1)) ``` haftmann@39246 ` 207` ```by (metis append.simps(2)) ``` paulson@23449 ` 208` haftmann@39246 ` 209` ```lemma append_Lf2 [simp]: "append t Lf = t" ``` blanchet@36484 ` 210` ```apply (induct t) ``` haftmann@39246 ` 211` ``` apply (metis append.simps(1)) ``` haftmann@39246 ` 212` ```by (metis append.simps(2)) ``` blanchet@36484 ` 213` blanchet@36484 ` 214` ```declare max_add_distrib_left [simp] ``` paulson@23449 ` 215` haftmann@39246 ` 216` ```lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2" ``` blanchet@36484 ` 217` ```apply (induct t1) ``` haftmann@39246 ` 218` ``` apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1)) ``` blanchet@36484 ` 219` ```by simp ``` paulson@23449 ` 220` haftmann@39246 ` 221` ```lemma n_leaves_append [simp]: ``` haftmann@39246 ` 222` ``` "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2" ``` blanchet@36484 ` 223` ```apply (induct t1) ``` haftmann@39246 ` 224` ``` apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1) ``` huffman@45502 ` 225` ``` Suc_eq_plus1) ``` webertj@49962 ` 226` ```by (simp add: distrib_right) ``` paulson@23449 ` 227` haftmann@39246 ` 228` ```lemma (*bt_map_append:*) ``` haftmann@39246 ` 229` ``` "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)" ``` blanchet@36484 ` 230` ```apply (induct t1) ``` haftmann@39246 ` 231` ``` apply (metis append.simps(1) bt_map.simps(1)) ``` haftmann@39246 ` 232` ```by (metis bt_map_append) ``` paulson@23449 ` 233` paulson@23449 ` 234` ```end ```