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