src/HOL/ex/BT.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 49962 a8cc904a6820
child 58249 180f1b3508ed
permissions -rw-r--r--
introduce order topology
     1 (*  Title:      HOL/ex/BT.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1995  University of Cambridge
     4 
     5 Binary trees
     6 *)
     7 
     8 header {* Binary trees *}
     9 
    10 theory BT imports Main begin
    11 
    12 datatype 'a bt =
    13     Lf
    14   | Br 'a  "'a bt"  "'a bt"
    15 
    16 primrec n_nodes :: "'a bt => nat" where
    17   "n_nodes Lf = 0"
    18 | "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
    19 
    20 primrec n_leaves :: "'a bt => nat" where
    21   "n_leaves Lf = Suc 0"
    22 | "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
    23 
    24 primrec depth :: "'a bt => nat" where
    25   "depth Lf = 0"
    26 | "depth (Br a t1 t2) = Suc (max (depth t1) (depth t2))"
    27 
    28 primrec reflect :: "'a bt => 'a bt" where
    29   "reflect Lf = Lf"
    30 | "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
    31 
    32 primrec bt_map :: "('a => 'b) => ('a bt => 'b bt)" where
    33   "bt_map f Lf = Lf"
    34 | "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
    35 
    36 primrec preorder :: "'a bt => 'a list" where
    37   "preorder Lf = []"
    38 | "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
    39 
    40 primrec inorder :: "'a bt => 'a list" where
    41   "inorder Lf = []"
    42 | "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
    43 
    44 primrec postorder :: "'a bt => 'a list" where
    45   "postorder Lf = []"
    46 | "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
    47 
    48 primrec append :: "'a bt => 'a bt => 'a bt" where
    49   "append Lf t = t"
    50 | "append (Br a t1 t2) t = Br a (append t1 t) (append t2 t)"
    51 
    52 text {* \medskip BT simplification *}
    53 
    54 lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
    55   apply (induct t)
    56    apply auto
    57   done
    58 
    59 lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
    60   apply (induct t)
    61    apply auto
    62   done
    63 
    64 lemma depth_reflect: "depth (reflect t) = depth t"
    65   apply (induct t) 
    66    apply auto
    67   done
    68 
    69 text {*
    70   The famous relationship between the numbers of leaves and nodes.
    71 *}
    72 
    73 lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
    74   apply (induct t)
    75    apply auto
    76   done
    77 
    78 lemma reflect_reflect_ident: "reflect (reflect t) = t"
    79   apply (induct t)
    80    apply auto
    81   done
    82 
    83 lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
    84   apply (induct t)
    85    apply simp_all
    86   done
    87 
    88 lemma preorder_bt_map: "preorder (bt_map f t) = map f (preorder t)"
    89   apply (induct t)
    90    apply simp_all
    91   done
    92 
    93 lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
    94   apply (induct t)
    95    apply simp_all
    96   done
    97 
    98 lemma postorder_bt_map: "postorder (bt_map f t) = map f (postorder t)"
    99   apply (induct t)
   100    apply simp_all
   101   done
   102 
   103 lemma depth_bt_map [simp]: "depth (bt_map f t) = depth t"
   104   apply (induct t)
   105    apply simp_all
   106   done
   107 
   108 lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
   109   apply (induct t)
   110    apply (simp_all add: distrib_right)
   111   done
   112 
   113 lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
   114   apply (induct t)
   115    apply simp_all
   116   done
   117 
   118 lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
   119   apply (induct t)
   120    apply simp_all
   121   done
   122 
   123 lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
   124   apply (induct t)
   125    apply simp_all
   126   done
   127 
   128 text {*
   129  Analogues of the standard properties of the append function for lists.
   130 *}
   131 
   132 lemma append_assoc [simp]:
   133      "append (append t1 t2) t3 = append t1 (append t2 t3)"
   134   apply (induct t1)
   135    apply simp_all
   136   done
   137 
   138 lemma append_Lf2 [simp]: "append t Lf = t"
   139   apply (induct t)
   140    apply simp_all
   141   done
   142 
   143 lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
   144   apply (induct t1)
   145    apply (simp_all add: max_add_distrib_left)
   146   done
   147 
   148 lemma n_leaves_append [simp]:
   149      "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
   150   apply (induct t1)
   151    apply (simp_all add: distrib_right)
   152   done
   153 
   154 lemma bt_map_append:
   155      "bt_map f (append t1 t2) = append (bt_map f t1) (bt_map f t2)"
   156   apply (induct t1)
   157    apply simp_all
   158   done
   159 
   160 end