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 \<noteq> n_leaves (reflect (Lf::'a bt))"
blanchet@36487
    65
    have "\<not> ?p\<^isub>1 (Suc 0)" by (metis reflect.simps(1) n_leaves.simps(1))
blanchet@36487
    66
    hence "\<not> ?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 "\<And>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 "\<And>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 "\<And>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 "\<And>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 "\<And>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: "\<And>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