src/HOL/ex/BT.thy
author paulson
Thu Apr 27 12:09:32 2006 +0200 (2006-04-27)
changeset 19478 25778eacbe21
parent 16417 9bc16273c2d4
child 19526 90fb9e092e66
permissions -rw-r--r--
some new functions
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
wenzelm@11024
     6
Binary trees (based on the ZF version).
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"
paulson@19478
    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@19478
    38
  "depth (Br a t1 t2) = 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
paulson@19478
    61
  "append Lf t = t"
paulson@19478
    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@19478
    78
  apply (induct t)
paulson@19478
    79
   apply (simp_all add: max_ac)
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
wenzelm@11024
   101
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
wenzelm@11024
   102
  apply (induct t)
wenzelm@11024
   103
   apply simp_all
wenzelm@11024
   104
  done
wenzelm@11024
   105
wenzelm@11024
   106
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
wenzelm@11024
   107
  apply (induct t)
wenzelm@11024
   108
   apply simp_all
wenzelm@11024
   109
  done
wenzelm@11024
   110
wenzelm@11024
   111
lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
wenzelm@11024
   112
  apply (induct t)
wenzelm@11024
   113
   apply simp_all
wenzelm@11024
   114
  done
wenzelm@11024
   115
wenzelm@11024
   116
lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
wenzelm@11024
   117
  apply (induct t)
wenzelm@11024
   118
   apply simp_all
wenzelm@11024
   119
  done
wenzelm@11024
   120
paulson@19478
   121
text {*
paulson@19478
   122
 Analogues of the standard properties of the append function for lists.
paulson@19478
   123
*}
paulson@19478
   124
paulson@19478
   125
lemma append_assoc [simp]:
paulson@19478
   126
     "append (append t1 t2) t3 = append t1 (append t2 t3)"
paulson@19478
   127
  apply (induct t1)
paulson@19478
   128
   apply simp_all
paulson@19478
   129
  done
paulson@19478
   130
paulson@19478
   131
lemma append_Lf2 [simp]: "append t Lf = t"
paulson@19478
   132
  apply (induct t)
paulson@19478
   133
   apply simp_all
paulson@19478
   134
  done
paulson@19478
   135
paulson@19478
   136
lemma max_add_distrib_left:
paulson@19478
   137
  fixes z :: "'a::pordered_ab_semigroup_add_imp_le"
paulson@19478
   138
  shows  "(max x y) + z = max (x+z) (y+z)"
paulson@19478
   139
apply (rule max_of_mono [THEN sym])
paulson@19478
   140
apply clarify
paulson@19478
   141
apply (rule add_le_cancel_right)
paulson@19478
   142
done
paulson@19478
   143
paulson@19478
   144
lemma depth_append [simp]: "depth (append t1 t2) = depth t1 + depth t2"
paulson@19478
   145
  apply (induct t1)
paulson@19478
   146
   apply (simp_all add: max_add_distrib_left)
paulson@19478
   147
  done
paulson@19478
   148
paulson@19478
   149
lemma n_leaves_append [simp]:
paulson@19478
   150
     "n_leaves (append t1 t2) = n_leaves t1 * n_leaves t2"
paulson@19478
   151
  apply (induct t1)
paulson@19478
   152
   apply (simp_all add: left_distrib)
paulson@19478
   153
  done
paulson@19478
   154
lcp@1167
   155
end