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