src/HOL/ex/BT.thy
author lcp
Thu, 29 Jun 1995 16:16:24 +0200
changeset 1167 cbd32a0f2f41
child 1376 92f83b9d17e1
permissions -rw-r--r--
New theory and proofs including preorder, inorder, ..., initially from ZF/ex/BT. Demonstrates datatypes and primrec.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1167
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     1
(*  Title: 	HOL/ex/BT.thy
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     2
    ID:         $Id$
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     4
    Copyright   1995  University of Cambridge
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     5
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     6
Binary trees (based on the ZF version)
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     7
*)
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     8
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
     9
BT = List +
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    10
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    11
datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    12
  
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    13
consts
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    14
    n_nodes	:: "'a bt => nat"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    15
    n_leaves   	:: "'a bt => nat"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    16
    reflect 	:: "'a bt => 'a bt"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    17
    bt_map      :: "('a=>'b) => ('a bt => 'b bt)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    18
    preorder    :: "'a bt => 'a list"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    19
    inorder     :: "'a bt => 'a list"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    20
    postorder   :: "'a bt => 'a list"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    21
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    22
primrec n_nodes bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    23
  n_nodes_Lf "n_nodes (Lf) = 0"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    24
  n_nodes_Br "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    25
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    26
primrec n_leaves bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    27
  n_leaves_Lf "n_leaves (Lf) = Suc 0"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    28
  n_leaves_Br "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    29
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    30
primrec reflect bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    31
  reflect_Lf "reflect (Lf) = Lf"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    32
  reflect_Br "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    33
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    34
primrec bt_map bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    35
  bt_map_Lf  "bt_map f Lf = Lf"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    36
  bt_map_Br  "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    37
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    38
primrec preorder bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    39
  preorder_Lf "preorder (Lf) = []"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    40
  preorder_Br "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    41
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    42
primrec inorder bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    43
  inorder_Lf "inorder (Lf) = []"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    44
  inorder_Br "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    45
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    46
primrec postorder bt
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    47
  postorder_Lf "postorder (Lf) = []"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    48
  postorder_Br "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    49
cbd32a0f2f41 New theory and proofs including preorder, inorder, ..., initially
lcp
parents:
diff changeset
    50
end