src/HOL/ex/BT.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 16417 9bc16273c2d4
child 19478 25778eacbe21
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
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
wenzelm@11024
    18
  n_nodes :: "'a bt => nat"
wenzelm@11024
    19
  n_leaves :: "'a bt => nat"
wenzelm@11024
    20
  reflect :: "'a bt => 'a bt"
wenzelm@11024
    21
  bt_map :: "('a => 'b) => ('a bt => 'b bt)"
wenzelm@11024
    22
  preorder :: "'a bt => 'a list"
wenzelm@11024
    23
  inorder :: "'a bt => 'a list"
wenzelm@11024
    24
  postorder :: "'a bt => 'a list"
lcp@1167
    25
berghofe@5184
    26
primrec
berghofe@1896
    27
  "n_nodes (Lf) = 0"
wenzelm@11024
    28
  "n_nodes (Br a t1 t2) = Suc (n_nodes t1 + n_nodes t2)"
lcp@1167
    29
berghofe@5184
    30
primrec
berghofe@1896
    31
  "n_leaves (Lf) = Suc 0"
berghofe@1896
    32
  "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
lcp@1167
    33
berghofe@5184
    34
primrec
berghofe@1896
    35
  "reflect (Lf) = Lf"
berghofe@1896
    36
  "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
lcp@1167
    37
berghofe@5184
    38
primrec
berghofe@1896
    39
  "bt_map f Lf = Lf"
berghofe@1896
    40
  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
lcp@1167
    41
berghofe@5184
    42
primrec
berghofe@1896
    43
  "preorder (Lf) = []"
berghofe@1896
    44
  "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
lcp@1167
    45
berghofe@5184
    46
primrec
berghofe@1896
    47
  "inorder (Lf) = []"
berghofe@1896
    48
  "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
lcp@1167
    49
berghofe@5184
    50
primrec
berghofe@1896
    51
  "postorder (Lf) = []"
berghofe@1896
    52
  "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
lcp@1167
    53
wenzelm@11024
    54
wenzelm@11024
    55
text {* \medskip BT simplification *}
wenzelm@11024
    56
wenzelm@11024
    57
lemma n_leaves_reflect: "n_leaves (reflect t) = n_leaves t"
wenzelm@11024
    58
  apply (induct t)
wenzelm@11024
    59
   apply auto
wenzelm@11024
    60
  done
wenzelm@11024
    61
wenzelm@11024
    62
lemma n_nodes_reflect: "n_nodes (reflect t) = n_nodes t"
wenzelm@11024
    63
  apply (induct t)
wenzelm@11024
    64
   apply auto
wenzelm@11024
    65
  done
wenzelm@11024
    66
wenzelm@11024
    67
text {*
wenzelm@11024
    68
  The famous relationship between the numbers of leaves and nodes.
wenzelm@11024
    69
*}
wenzelm@11024
    70
wenzelm@11024
    71
lemma n_leaves_nodes: "n_leaves t = Suc (n_nodes t)"
wenzelm@11024
    72
  apply (induct t)
wenzelm@11024
    73
   apply auto
wenzelm@11024
    74
  done
wenzelm@11024
    75
wenzelm@11024
    76
lemma reflect_reflect_ident: "reflect (reflect t) = t"
wenzelm@11024
    77
  apply (induct t)
wenzelm@11024
    78
   apply auto
wenzelm@11024
    79
  done
wenzelm@11024
    80
wenzelm@11024
    81
lemma bt_map_reflect: "bt_map f (reflect t) = reflect (bt_map f t)"
wenzelm@11024
    82
  apply (induct t)
wenzelm@11024
    83
   apply simp_all
wenzelm@11024
    84
  done
wenzelm@11024
    85
wenzelm@11024
    86
lemma inorder_bt_map: "inorder (bt_map f t) = map f (inorder t)"
wenzelm@11024
    87
  apply (induct t)
wenzelm@11024
    88
   apply simp_all
wenzelm@11024
    89
  done
wenzelm@11024
    90
wenzelm@11024
    91
lemma preorder_reflect: "preorder (reflect t) = rev (postorder t)"
wenzelm@11024
    92
  apply (induct t)
wenzelm@11024
    93
   apply simp_all
wenzelm@11024
    94
  done
wenzelm@11024
    95
wenzelm@11024
    96
lemma inorder_reflect: "inorder (reflect t) = rev (inorder t)"
wenzelm@11024
    97
  apply (induct t)
wenzelm@11024
    98
   apply simp_all
wenzelm@11024
    99
  done
wenzelm@11024
   100
wenzelm@11024
   101
lemma postorder_reflect: "postorder (reflect t) = rev (preorder t)"
wenzelm@11024
   102
  apply (induct t)
wenzelm@11024
   103
   apply simp_all
wenzelm@11024
   104
  done
wenzelm@11024
   105
lcp@1167
   106
end