src/HOL/Metis_Examples/Binary_Tree.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 63167 0909deb8059b permissions -rw-r--r--
executable domain membership checks
```     1 (*  Title:      HOL/Metis_Examples/Binary_Tree.thy
```
```     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
```
```     3     Author:     Jasmin Blanchette, TU Muenchen
```
```     4
```
```     5 Metis example featuring binary trees.
```
```     6 *)
```
```     7
```
```     8 section \<open>Metis Example Featuring Binary Trees\<close>
```
```     9
```
```    10 theory Binary_Tree
```
```    11 imports Main
```
```    12 begin
```
```    13
```
```    14 declare [[metis_new_skolem]]
```
```    15
```
```    16 datatype 'a bt =
```
```    17     Lf
```
```    18   | Br 'a  "'a bt"  "'a bt"
```
```    19
```
```    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"
```
```    27
```
```    28 primrec depth :: "'a bt => nat" where
```
```    29   "depth Lf = 0"
```
```    30 | "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
```
```    31
```
```    32 primrec reflect :: "'a bt => 'a bt" where
```
```    33   "reflect Lf = Lf"
```
```    34 | "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
```
```    35
```
```    36 primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
```
```    37   "bt_map f Lf = Lf"
```
```    38 | "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
```
```    39
```
```    40 primrec preorder :: "'a bt => 'a list" where
```
```    41   "preorder Lf = []"
```
```    42 | "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
```
```    43
```
```    44 primrec inorder :: "'a bt => 'a list" where
```
```    45   "inorder Lf = []"
```
```    46 | "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
```
```    47
```
```    48 primrec postorder :: "'a bt => 'a list" where
```
```    49   "postorder Lf = []"
```
```    50 | "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
```
```    51
```
```    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)"
```
```    55
```
```    56 text \<open>\medskip BT simplification\<close>
```
```    57
```
```    58 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
```
```    59 proof (induct t)
```
```    60   case Lf thus ?case
```
```    61   proof -
```
```    62     let "?p\<^sub>1 x\<^sub>1" = "x\<^sub>1 \<noteq> n_leaves (reflect (Lf::'a bt))"
```
```    63     have "\<not> ?p\<^sub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1))
```
```    64     hence "\<not> ?p\<^sub>1 (n_leaves (Lf::'a bt))" by (metis n_leaves.simps(1))
```
```    65     thus "n_leaves (reflect (Lf::'a bt)) = n_leaves (Lf::'a bt)" by metis
```
```    66   qed
```
```    67 next
```
```    68   case (Br a t1 t2) thus ?case
```
```    69     by (metis n_leaves.simps(2) add.commute reflect.simps(2))
```
```    70 qed
```
```    71
```
```    72 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
```
```    73 proof (induct t)
```
```    74   case Lf thus ?case by (metis reflect.simps(1))
```
```    75 next
```
```    76   case (Br a t1 t2) thus ?case
```
```    77     by (metis add.commute n_nodes.simps(2) reflect.simps(2))
```
```    78 qed
```
```    79
```
```    80 lemma depth_reflect: "depth (reflect t) = depth t"
```
```    81 apply (induct t)
```
```    82  apply (metis depth.simps(1) reflect.simps(1))
```
```    83 by (metis depth.simps(2) max.commute reflect.simps(2))
```
```    84
```
```    85 text \<open>
```
```    86 The famous relationship between the numbers of leaves and nodes.
```
```    87 \<close>
```
```    88
```
```    89 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
```
```    90 apply (induct t)
```
```    91  apply (metis n_leaves.simps(1) n_nodes.simps(1))
```
```    92 by auto
```
```    93
```
```    94 lemma reflect_reflect_ident: "reflect (reflect t) = t"
```
```    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
```
```   109
```
```   110 lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
```
```   111 apply (rule ext)
```
```   112 apply (induct_tac y)
```
```   113  apply (metis bt_map.simps(1))
```
```   114 by (metis bt_map.simps(2))
```
```   115
```
```   116 lemma bt_map_append: "bt_map f (append t u) = append (bt_map f t) (bt_map f u)"
```
```   117 apply (induct t)
```
```   118  apply (metis append.simps(1) bt_map.simps(1))
```
```   119 by (metis append.simps(2) bt_map.simps(2))
```
```   120
```
```   121 lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
```
```   122 apply (induct t)
```
```   123  apply (metis bt_map.simps(1))
```
```   124 by (metis bt_map.simps(2) o_eq_dest_lhs)
```
```   125
```
```   126 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
```
```   127 apply (induct t)
```
```   128  apply (metis bt_map.simps(1) reflect.simps(1))
```
```   129 by (metis bt_map.simps(2) reflect.simps(2))
```
```   130
```
```   131 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
```
```   132 apply (induct t)
```
```   133  apply (metis bt_map.simps(1) list.map(1) preorder.simps(1))
```
```   134 by simp
```
```   135
```
```   136 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
```
```   137 proof (induct t)
```
```   138   case Lf thus ?case
```
```   139   proof -
```
```   140     have "map f [] = []" by (metis list.map(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
```
```   148
```
```   149 lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
```
```   150 apply (induct t)
```
```   151  apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1))
```
```   152 by simp
```
```   153
```
```   154 lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
```
```   155 apply (induct t)
```
```   156  apply (metis bt_map.simps(1) depth.simps(1))
```
```   157 by simp
```
```   158
```
```   159 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
```
```   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
```
```   177
```
```   178 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
```
```   179 apply (induct t)
```
```   180  apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
```
```   181               reflect.simps(1))
```
```   182 apply simp
```
```   183 done
```
```   184
```
```   185 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
```
```   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 *)
```
```   193
```
```   194 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
```
```   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)
```
```   199
```
```   200 text \<open>
```
```   201 Analogues of the standard properties of the append function for lists.
```
```   202 \<close>
```
```   203
```
```   204 lemma append_assoc [simp]: "append (append t1 t2) t3 = append t1 (append t2 t3)"
```
```   205 apply (induct t1)
```
```   206  apply (metis append.simps(1))
```
```   207 by (metis append.simps(2))
```
```   208
```
```   209 lemma append_Lf2 [simp]: "append t Lf = t"
```
```   210 apply (induct t)
```
```   211  apply (metis append.simps(1))
```
```   212 by (metis append.simps(2))
```
```   213
```
```   214 declare max_add_distrib_left [simp]
```
```   215
```
```   216 lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
```
```   217 apply (induct t1)
```
```   218  apply (metis append.simps(1) depth.simps(1) plus_nat.simps(1))
```
```   219 by simp
```
```   220
```
```   221 lemma n_leaves_append [simp]:
```
```   222      "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
```
```   223 apply (induct t1)
```
```   224  apply (metis append.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
```
```   225               Suc_eq_plus1)
```
```   226 by (simp add: distrib_right)
```
```   227
```
```   228 lemma (*bt_map_append:*)
```
```   229      "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
```
```   230 apply (induct t1)
```
```   231  apply (metis append.simps(1) bt_map.simps(1))
```
```   232 by (metis bt_map_append)
```
```   233
```
```   234 end
```