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