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