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