src/HOL/Metis_Examples/BT.thy
author blanchet
Tue Apr 27 18:07:51 2010 +0200 (2010-04-27)
changeset 36484 134ac130a8ed
parent 33027 9cf389429f6d
child 36487 50fd056cc3ce
permissions -rw-r--r--
redid the proofs with the latest Sledgehammer;
both an exercise and (for a few proofs) a demonstration of the new Isar proof code
     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 datatype 'a bt =
    14     Lf
    15   | Br 'a  "'a bt"  "'a bt"
    16 
    17 consts
    18   n_nodes   :: "'a bt => nat"
    19   n_leaves  :: "'a bt => nat"
    20   depth     :: "'a bt => nat"
    21   reflect   :: "'a bt => 'a bt"
    22   bt_map    :: "('a => 'b) => ('a bt => 'b bt)"
    23   preorder  :: "'a bt => 'a list"
    24   inorder   :: "'a bt => 'a list"
    25   postorder :: "'a bt => 'a list"
    26   appnd    :: "'a bt => 'a bt => 'a bt"
    27 
    28 primrec
    29   "n_nodes Lf = 0"
    30   "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
    31 
    32 primrec
    33   "n_leaves Lf = Suc 0"
    34   "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
    35 
    36 primrec
    37   "depth Lf = 0"
    38   "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
    39 
    40 primrec
    41   "reflect Lf = Lf"
    42   "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
    43 
    44 primrec
    45   "bt_map f Lf = Lf"
    46   "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
    47 
    48 primrec
    49   "preorder Lf = []"
    50   "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
    51 
    52 primrec
    53   "inorder Lf = []"
    54   "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
    55 
    56 primrec
    57   "postorder Lf = []"
    58   "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
    59 
    60 primrec
    61   "appnd Lf t = t"
    62   "appnd (Br a t1 t2) t = Br a (appnd t1 t) (appnd t2 t)"
    63 
    64 
    65 text {* \medskip BT simplification *}
    66 
    67 declare [[ atp_problem_prefix = "BT__n_leaves_reflect" ]]
    68 
    69 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
    70 proof (induct t)
    71   case Lf thus ?case by (metis reflect.simps(1))
    72 next
    73   case (Br a t1 t2) thus ?case
    74     by (metis class_semiring.add_c n_leaves.simps(2) reflect.simps(2))
    75 qed
    76 
    77 declare [[ atp_problem_prefix = "BT__n_nodes_reflect" ]]
    78 
    79 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
    80 proof (induct t)
    81   case Lf thus ?case by (metis reflect.simps(1))
    82 next
    83   case (Br a t1 t2) thus ?case
    84     by (metis class_semiring.semiring_rules(24) n_nodes.simps(2) reflect.simps(2))
    85 qed
    86 
    87 declare [[ atp_problem_prefix = "BT__depth_reflect" ]]
    88 
    89 lemma depth_reflect: "depth (reflect t) = depth t"
    90 apply (induct t)
    91  apply (metis depth.simps(1) reflect.simps(1))
    92 by (metis depth.simps(2) min_max.inf_sup_aci(5) reflect.simps(2))
    93 
    94 text {*
    95 The famous relationship between the numbers of leaves and nodes.
    96 *}
    97 
    98 declare [[ atp_problem_prefix = "BT__n_leaves_nodes" ]]
    99 
   100 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
   101 apply (induct t)
   102  apply (metis n_leaves.simps(1) n_nodes.simps(1))
   103 by auto
   104 
   105 declare [[ atp_problem_prefix = "BT__reflect_reflect_ident" ]]
   106 
   107 lemma reflect_reflect_ident: "reflect (reflect t) = t"
   108 apply (induct t)
   109  apply (metis reflect.simps(1))
   110 proof -
   111   fix a :: 'a and t1 :: "'a bt" and t2 :: "'a bt"
   112   assume A1: "reflect (reflect t1) = t1"
   113   assume A2: "reflect (reflect t2) = t2"
   114   have "\<And>V U. reflect (Br U V (reflect t1)) = Br U t1 (reflect V)"
   115     using A1 by (metis reflect.simps(2))
   116   hence "\<And>V U. Br U t1 (reflect (reflect V)) = reflect (reflect (Br U t1 V))"
   117     by (metis reflect.simps(2))
   118   hence "\<And>U. reflect (reflect (Br U t1 t2)) = Br U t1 t2"
   119     using A2 by metis
   120   thus "reflect (reflect (Br a t1 t2)) = Br a t1 t2" by blast
   121 qed
   122 
   123 declare [[ atp_problem_prefix = "BT__bt_map_ident" ]]
   124 
   125 lemma bt_map_ident: "bt_map (%x. x) = (%y. y)"
   126 apply (rule ext) 
   127 apply (induct_tac y)
   128  apply (metis bt_map.simps(1))
   129 by (metis COMBI_def bt_map.simps(2))
   130 
   131 declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]]
   132 
   133 lemma bt_map_appnd: "bt_map f (appnd t u) = appnd (bt_map f t) (bt_map f u)"
   134 apply (induct t)
   135  apply (metis appnd.simps(1) bt_map.simps(1))
   136 by (metis appnd.simps(2) bt_map.simps(2))
   137 
   138 declare [[ atp_problem_prefix = "BT__bt_map_compose" ]]
   139 
   140 lemma bt_map_compose: "bt_map (f o g) t = bt_map f (bt_map g t)"
   141 apply (induct t)
   142  apply (metis bt_map.simps(1))
   143 by (metis bt_map.simps(2) o_eq_dest_lhs)
   144 
   145 declare [[ atp_problem_prefix = "BT__bt_map_reflect" ]]
   146 
   147 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
   148 apply (induct t)
   149  apply (metis bt_map.simps(1) reflect.simps(1))
   150 by (metis bt_map.simps(2) reflect.simps(2))
   151 
   152 declare [[ atp_problem_prefix = "BT__preorder_bt_map" ]]
   153 
   154 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
   155 apply (induct t)
   156  apply (metis bt_map.simps(1) map.simps(1) preorder.simps(1))
   157 by simp
   158 
   159 declare [[ atp_problem_prefix = "BT__inorder_bt_map" ]]
   160 
   161 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
   162 proof (induct t)
   163   case Lf thus ?case
   164   proof -
   165     have "map f [] = []" by (metis map.simps(1))
   166     hence "map f [] = inorder Lf" by (metis inorder.simps(1))
   167     hence "inorder (bt_map f Lf) = map f []" by (metis bt_map.simps(1))
   168     thus "inorder (bt_map f Lf) = map f (inorder Lf)" by (metis inorder.simps(1))
   169   qed
   170 next
   171   case (Br a t1 t2) thus ?case by simp
   172 qed
   173 
   174 declare [[ atp_problem_prefix = "BT__postorder_bt_map" ]]
   175 
   176 lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
   177 apply (induct t)
   178  apply (metis Nil_is_map_conv bt_map.simps(1) postorder.simps(1))
   179 by simp
   180 
   181 declare [[ atp_problem_prefix = "BT__depth_bt_map" ]]
   182 
   183 lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
   184 apply (induct t)
   185  apply (metis bt_map.simps(1) depth.simps(1))
   186 by simp
   187 
   188 declare [[ atp_problem_prefix = "BT__n_leaves_bt_map" ]]
   189 
   190 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
   191 apply (induct t)
   192  apply (metis bt_map.simps(1) n_leaves.simps(1))
   193 proof -
   194   fix a :: 'b and t1 :: "'b bt" and t2 :: "'b bt"
   195   assume A1: "n_leaves (bt_map f t1) = n_leaves t1"
   196   assume A2: "n_leaves (bt_map f t2) = n_leaves t2"
   197   have "\<And>V U. n_leaves (Br U (bt_map f t1) V) = n_leaves t1 + n_leaves V"
   198     using A1 by (metis n_leaves.simps(2))
   199   hence "\<And>V U. n_leaves (bt_map f (Br U t1 V)) = n_leaves t1 + n_leaves (bt_map f V)"
   200     by (metis bt_map.simps(2))
   201   hence F1: "\<And>U. n_leaves (bt_map f (Br U t1 t2)) = n_leaves t1 + n_leaves t2"
   202     using A2 by metis
   203   have "n_leaves t1 + n_leaves t2 = n_leaves (Br a t1 t2)"
   204     by (metis n_leaves.simps(2))
   205   thus "n_leaves (bt_map f (Br a t1 t2)) = n_leaves (Br a t1 t2)"
   206     using F1 by metis
   207 qed
   208 
   209 declare [[ atp_problem_prefix = "BT__preorder_reflect" ]]
   210 
   211 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
   212 apply (induct t)
   213  apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
   214               reflect.simps(1))
   215 by (metis append.simps(1) append.simps(2) postorder.simps(2) preorder.simps(2)
   216           reflect.simps(2) rev.simps(2) rev_append rev_swap)
   217 
   218 declare [[ atp_problem_prefix = "BT__inorder_reflect" ]]
   219 
   220 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
   221 apply (induct t)
   222  apply (metis Nil_is_rev_conv inorder.simps(1) reflect.simps(1))
   223 by simp
   224 (* Slow:
   225 by (metis append.simps(1) append_eq_append_conv2 inorder.simps(2)
   226           reflect.simps(2) rev.simps(2) rev_append)
   227 *)
   228 
   229 declare [[ atp_problem_prefix = "BT__postorder_reflect" ]]
   230 
   231 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
   232 apply (induct t)
   233  apply (metis Nil_is_rev_conv postorder.simps(1) preorder.simps(1)
   234               reflect.simps(1))
   235 by (metis preorder_reflect reflect_reflect_ident rev_swap)
   236 
   237 text {*
   238 Analogues of the standard properties of the append function for lists.
   239 *}
   240 
   241 declare [[ atp_problem_prefix = "BT__appnd_assoc" ]]
   242 
   243 lemma appnd_assoc [simp]: "appnd (appnd t1 t2) t3 = appnd t1 (appnd t2 t3)"
   244 apply (induct t1)
   245  apply (metis appnd.simps(1))
   246 by (metis appnd.simps(2))
   247 
   248 declare [[ atp_problem_prefix = "BT__appnd_Lf2" ]]
   249 
   250 lemma appnd_Lf2 [simp]: "appnd t Lf = t"
   251 apply (induct t)
   252  apply (metis appnd.simps(1))
   253 by (metis appnd.simps(2))
   254 
   255 declare max_add_distrib_left [simp]
   256 
   257 declare [[ atp_problem_prefix = "BT__depth_appnd" ]]
   258 
   259 lemma depth_appnd [simp]: "depth (appnd t1 t2) = depth t1 + depth t2"
   260 apply (induct t1)
   261  apply (metis appnd.simps(1) depth.simps(1) plus_nat.simps(1))
   262 by simp
   263 
   264 declare [[ atp_problem_prefix = "BT__n_leaves_appnd" ]]
   265 
   266 lemma n_leaves_appnd [simp]:
   267      "n_leaves (appnd t1 t2) = n_leaves t1 * n_leaves t2"
   268 apply (induct t1)
   269  apply (metis appnd.simps(1) n_leaves.simps(1) nat_mult_1 plus_nat.simps(1)
   270               semiring_norm(111))
   271 by (simp add: left_distrib)
   272 
   273 declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]]
   274 
   275 lemma (*bt_map_appnd:*)
   276      "bt_map f (appnd t1 t2) = appnd (bt_map f t1) (bt_map f t2)"
   277 apply (induct t1)
   278  apply (metis appnd.simps(1) bt_map.simps(1))
   279 by (metis bt_map_appnd)
   280 
   281 end