src/HOL/MetisExamples/BT.thy
author nipkow
Wed Jun 24 09:41:14 2009 +0200 (2009-06-24)
changeset 31790 05c92381363c
parent 29782 02e76245e5af
child 32864 a226f29d4bdc
permissions -rw-r--r--
corrected and unified thm names
paulson@23449
     1
(*  Title:      HOL/MetisTest/BT.thy
paulson@23449
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@23449
     3
paulson@23449
     4
Testing the metis method
paulson@23449
     5
*)
paulson@23449
     6
paulson@23449
     7
header {* Binary trees *}
paulson@23449
     8
haftmann@27104
     9
theory BT
haftmann@27104
    10
imports Main
haftmann@27104
    11
begin
paulson@23449
    12
paulson@23449
    13
paulson@23449
    14
datatype 'a bt =
paulson@23449
    15
    Lf
paulson@23449
    16
  | Br 'a  "'a bt"  "'a bt"
paulson@23449
    17
paulson@23449
    18
consts
paulson@23449
    19
  n_nodes   :: "'a bt => nat"
paulson@23449
    20
  n_leaves  :: "'a bt => nat"
paulson@23449
    21
  depth     :: "'a bt => nat"
paulson@23449
    22
  reflect   :: "'a bt => 'a bt"
paulson@23449
    23
  bt_map    :: "('a => 'b) => ('a bt => 'b bt)"
paulson@23449
    24
  preorder  :: "'a bt => 'a list"
paulson@23449
    25
  inorder   :: "'a bt => 'a list"
paulson@23449
    26
  postorder :: "'a bt => 'a list"
paulson@23449
    27
  appnd    :: "'a bt => 'a bt => 'a bt"
paulson@23449
    28
paulson@23449
    29
primrec
paulson@23449
    30
  "n_nodes Lf = 0"
paulson@23449
    31
  "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
paulson@23449
    32
paulson@23449
    33
primrec
paulson@23449
    34
  "n_leaves Lf = Suc 0"
paulson@23449
    35
  "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
paulson@23449
    36
paulson@23449
    37
primrec
paulson@23449
    38
  "depth Lf = 0"
paulson@23449
    39
  "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
paulson@23449
    40
paulson@23449
    41
primrec
paulson@23449
    42
  "reflect Lf = Lf"
paulson@23449
    43
  "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
paulson@23449
    44
paulson@23449
    45
primrec
paulson@23449
    46
  "bt_map f Lf = Lf"
paulson@23449
    47
  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
paulson@23449
    48
paulson@23449
    49
primrec
paulson@23449
    50
  "preorder Lf = []"
paulson@23449
    51
  "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
paulson@23449
    52
paulson@23449
    53
primrec
paulson@23449
    54
  "inorder Lf = []"
paulson@23449
    55
  "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
paulson@23449
    56
paulson@23449
    57
primrec
paulson@23449
    58
  "postorder Lf = []"
paulson@23449
    59
  "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
paulson@23449
    60
paulson@23449
    61
primrec
paulson@23449
    62
  "appnd Lf t = t"
paulson@23449
    63
  "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)"
paulson@23449
    64
paulson@23449
    65
paulson@23449
    66
text {* \medskip BT simplification *}
paulson@23449
    67
wenzelm@28592
    68
ML {*AtpWrapper.problem_name := "BT__n_leaves_reflect"*}
paulson@23449
    69
lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
paulson@23449
    70
  apply (induct t)
paulson@23449
    71
  apply (metis add_right_cancel n_leaves.simps(1) reflect.simps(1))
paulson@23449
    72
  apply (metis add_commute n_leaves.simps(2) reflect.simps(2))
paulson@23449
    73
  done
paulson@23449
    74
wenzelm@28592
    75
ML {*AtpWrapper.problem_name := "BT__n_nodes_reflect"*}
paulson@23449
    76
lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
paulson@23449
    77
  apply (induct t)
paulson@23449
    78
  apply (metis reflect.simps(1))
paulson@23449
    79
  apply (metis n_nodes.simps(2) nat_add_commute reflect.simps(2))
paulson@23449
    80
  done
paulson@23449
    81
wenzelm@28592
    82
ML {*AtpWrapper.problem_name := "BT__depth_reflect"*}
paulson@23449
    83
lemma depth_reflect: "depth (reflect t) = depth t"
paulson@23449
    84
  apply (induct t)
paulson@23449
    85
  apply (metis depth.simps(1) reflect.simps(1))
haftmann@29511
    86
  apply (metis depth.simps(2) min_max.sup_commute reflect.simps(2))
paulson@23449
    87
  done
paulson@23449
    88
paulson@23449
    89
text {*
paulson@23449
    90
  The famous relationship between the numbers of leaves and nodes.
paulson@23449
    91
*}
paulson@23449
    92
wenzelm@28592
    93
ML {*AtpWrapper.problem_name := "BT__n_leaves_nodes"*}
paulson@23449
    94
lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
paulson@23449
    95
  apply (induct t)
paulson@23449
    96
  apply (metis n_leaves.simps(1) n_nodes.simps(1))
paulson@23449
    97
  apply auto
paulson@23449
    98
  done
paulson@23449
    99
wenzelm@28592
   100
ML {*AtpWrapper.problem_name := "BT__reflect_reflect_ident"*}
paulson@23449
   101
lemma reflect_reflect_ident: "reflect (reflect t) = t"
paulson@23449
   102
  apply (induct t)
paulson@23449
   103
  apply (metis add_right_cancel reflect.simps(1));
haftmann@27104
   104
  apply (metis reflect.simps(2))
paulson@23449
   105
  done
paulson@23449
   106
wenzelm@28592
   107
ML {*AtpWrapper.problem_name := "BT__bt_map_ident"*}
paulson@23449
   108
lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
paulson@23449
   109
apply (rule ext) 
paulson@23449
   110
apply (induct_tac y)
paulson@23449
   111
  apply (metis bt_map.simps(1))
paulson@23449
   112
txt{*BUG involving flex-flex pairs*}
paulson@23449
   113
(*  apply (metis bt_map.simps(2)) *)
paulson@23449
   114
apply auto
paulson@23449
   115
done
paulson@23449
   116
paulson@23449
   117
wenzelm@28592
   118
ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*}
paulson@23449
   119
lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)"
paulson@23449
   120
apply (induct t)
paulson@23449
   121
  apply (metis appnd.simps(1) bt_map.simps(1))
paulson@23449
   122
  apply (metis appnd.simps(2) bt_map.simps(2))  (*slow!!*)
paulson@23449
   123
done
paulson@23449
   124
paulson@23449
   125
wenzelm@28592
   126
ML {*AtpWrapper.problem_name := "BT__bt_map_compose"*}
paulson@23449
   127
lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
paulson@23449
   128
apply (induct t) 
paulson@23449
   129
  apply (metis bt_map.simps(1))
paulson@23449
   130
txt{*Metis runs forever*}
paulson@23449
   131
(*  apply (metis bt_map.simps(2) o_apply)*)
paulson@23449
   132
apply auto
paulson@23449
   133
done
paulson@23449
   134
paulson@23449
   135
wenzelm@28592
   136
ML {*AtpWrapper.problem_name := "BT__bt_map_reflect"*}
paulson@23449
   137
lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
paulson@23449
   138
  apply (induct t)
paulson@23449
   139
  apply (metis add_right_cancel bt_map.simps(1) reflect.simps(1))
paulson@23449
   140
  apply (metis add_right_cancel bt_map.simps(2) reflect.simps(2))
paulson@23449
   141
  done
paulson@23449
   142
wenzelm@28592
   143
ML {*AtpWrapper.problem_name := "BT__preorder_bt_map"*}
paulson@23449
   144
lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
paulson@23449
   145
  apply (induct t)
paulson@23449
   146
  apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
paulson@23449
   147
   apply simp
paulson@23449
   148
  done
paulson@23449
   149
wenzelm@28592
   150
ML {*AtpWrapper.problem_name := "BT__inorder_bt_map"*}
paulson@23449
   151
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
paulson@23449
   152
  apply (induct t)
paulson@23449
   153
  apply (metis bt_map.simps(1) inorder.simps(1) map.simps(1))
paulson@23449
   154
  apply simp
paulson@23449
   155
  done
paulson@23449
   156
wenzelm@28592
   157
ML {*AtpWrapper.problem_name := "BT__postorder_bt_map"*}
paulson@23449
   158
lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
paulson@23449
   159
  apply (induct t)
paulson@23449
   160
  apply (metis bt_map.simps(1) map.simps(1) postorder.simps(1))
paulson@23449
   161
   apply simp
paulson@23449
   162
  done
paulson@23449
   163
wenzelm@28592
   164
ML {*AtpWrapper.problem_name := "BT__depth_bt_map"*}
paulson@23449
   165
lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
paulson@23449
   166
  apply (induct t)
paulson@23449
   167
  apply (metis bt_map.simps(1) depth.simps(1))
paulson@23449
   168
   apply simp
paulson@23449
   169
  done
paulson@23449
   170
wenzelm@28592
   171
ML {*AtpWrapper.problem_name := "BT__n_leaves_bt_map"*}
paulson@23449
   172
lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
paulson@23449
   173
  apply (induct t)
nipkow@31790
   174
  apply (metis One_nat_def Suc_eq_plus1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
paulson@25457
   175
  apply (metis bt_map.simps(2) n_leaves.simps(2))
paulson@23449
   176
  done
paulson@23449
   177
paulson@23449
   178
wenzelm@28592
   179
ML {*AtpWrapper.problem_name := "BT__preorder_reflect"*}
paulson@23449
   180
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
paulson@23449
   181
  apply (induct t)
paulson@23449
   182
  apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev_is_Nil_conv)
haftmann@29782
   183
  apply (metis append_Nil Cons_eq_append_conv postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append rev_rev_ident)
paulson@23449
   184
  done
paulson@23449
   185
wenzelm@28592
   186
ML {*AtpWrapper.problem_name := "BT__inorder_reflect"*}
paulson@23449
   187
lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
paulson@23449
   188
  apply (induct t)
paulson@23449
   189
  apply (metis inorder.simps(1) reflect.simps(1) rev.simps(1))
paulson@23449
   190
  apply simp
paulson@23449
   191
  done
paulson@23449
   192
wenzelm@28592
   193
ML {*AtpWrapper.problem_name := "BT__postorder_reflect"*}
paulson@23449
   194
lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
paulson@23449
   195
  apply (induct t)
paulson@23449
   196
  apply (metis postorder.simps(1) preorder.simps(1) reflect.simps(1) rev.simps(1))
paulson@25457
   197
  apply (metis Cons_eq_appendI postorder.simps(2) preorder.simps(2) reflect.simps(2) rev.simps(2) rev_append self_append_conv2)
paulson@23449
   198
  done
paulson@23449
   199
paulson@23449
   200
text {*
paulson@23449
   201
 Analogues of the standard properties of the append function for lists.
paulson@23449
   202
*}
paulson@23449
   203
wenzelm@28592
   204
ML {*AtpWrapper.problem_name := "BT__appnd_assoc"*}
paulson@23449
   205
lemma appnd_assoc [simp]:
paulson@23449
   206
     "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
paulson@23449
   207
  apply (induct t1)
paulson@23449
   208
  apply (metis appnd.simps(1))
paulson@23449
   209
  apply (metis appnd.simps(2))
paulson@23449
   210
  done
paulson@23449
   211
wenzelm@28592
   212
ML {*AtpWrapper.problem_name := "BT__appnd_Lf2"*}
paulson@23449
   213
lemma appnd_Lf2 [simp]: "appnd t Lf = t"
paulson@23449
   214
  apply (induct t)
paulson@23449
   215
  apply (metis appnd.simps(1))
paulson@23449
   216
  apply (metis appnd.simps(2))
paulson@23449
   217
  done
paulson@23449
   218
wenzelm@28592
   219
ML {*AtpWrapper.problem_name := "BT__depth_appnd"*}
paulson@23449
   220
  declare max_add_distrib_left [simp]
paulson@23449
   221
lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
paulson@23449
   222
  apply (induct t1)
paulson@23449
   223
  apply (metis add_0 appnd.simps(1) depth.simps(1))
paulson@23449
   224
apply (simp add: ); 
paulson@23449
   225
  done
paulson@23449
   226
wenzelm@28592
   227
ML {*AtpWrapper.problem_name := "BT__n_leaves_appnd"*}
paulson@23449
   228
lemma n_leaves_appnd [simp]:
paulson@23449
   229
     "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
paulson@23449
   230
  apply (induct t1)
paulson@23449
   231
  apply (metis One_nat_def appnd.simps(1) less_irrefl less_linear n_leaves.simps(1) nat_mult_1) 
paulson@23449
   232
  apply (simp add: left_distrib)
paulson@23449
   233
  done
paulson@23449
   234
wenzelm@28592
   235
ML {*AtpWrapper.problem_name := "BT__bt_map_appnd"*}
wenzelm@26312
   236
lemma (*bt_map_appnd:*)
paulson@23449
   237
     "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
paulson@23449
   238
  apply (induct t1)
paulson@23449
   239
  apply (metis appnd.simps(1) bt_map_appnd)
paulson@23449
   240
  apply (metis bt_map_appnd)
paulson@23449
   241
  done
paulson@23449
   242
paulson@23449
   243
end