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