src/HOL/ex/BT.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 23236 91d71bde1112
child 39246 9e58f0499f57
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/BT.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1995  University of Cambridge
     5 
     6 Binary trees
     7 *)
     8 
     9 header {* Binary trees *}
    10 
    11 theory BT imports Main 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   append     :: "'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   "append Lf t = t"
    62   "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
    63 
    64 
    65 text {* \medskip BT simplification *}
    66 
    67 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
    68   apply (induct t)
    69    apply auto
    70   done
    71 
    72 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
    73   apply (induct t)
    74    apply auto
    75   done
    76 
    77 lemma depth_reflect: "depth (reflect t) = depth t"
    78   apply (induct t) 
    79    apply auto
    80   done
    81 
    82 text {*
    83   The famous relationship between the numbers of leaves and nodes.
    84 *}
    85 
    86 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
    87   apply (induct t)
    88    apply auto
    89   done
    90 
    91 lemma reflect_reflect_ident: "reflect (reflect t) = t"
    92   apply (induct t)
    93    apply auto
    94   done
    95 
    96 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
    97   apply (induct t)
    98    apply simp_all
    99   done
   100 
   101 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
   102   apply (induct t)
   103    apply simp_all
   104   done
   105 
   106 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
   107   apply (induct t)
   108    apply simp_all
   109   done
   110 
   111 lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
   112   apply (induct t)
   113    apply simp_all
   114   done
   115 
   116 lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
   117   apply (induct t)
   118    apply simp_all
   119   done
   120 
   121 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
   122   apply (induct t)
   123    apply (simp_all add: left_distrib)
   124   done
   125 
   126 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
   127   apply (induct t)
   128    apply simp_all
   129   done
   130 
   131 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
   132   apply (induct t)
   133    apply simp_all
   134   done
   135 
   136 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
   137   apply (induct t)
   138    apply simp_all
   139   done
   140 
   141 text {*
   142  Analogues of the standard properties of the append function for lists.
   143 *}
   144 
   145 lemma append_assoc [simp]:
   146      "append (append t1 t2) t3 = append t1 (append t2 t3)"
   147   apply (induct t1)
   148    apply simp_all
   149   done
   150 
   151 lemma append_Lf2 [simp]: "append t Lf = t"
   152   apply (induct t)
   153    apply simp_all
   154   done
   155 
   156 lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
   157   apply (induct t1)
   158    apply (simp_all add: max_add_distrib_left)
   159   done
   160 
   161 lemma n_leaves_append [simp]:
   162      "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
   163   apply (induct t1)
   164    apply (simp_all add: left_distrib)
   165   done
   166 
   167 lemma bt_map_append:
   168      "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
   169   apply (induct t1)
   170    apply simp_all
   171   done
   172 
   173 end