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