src/HOL/Data_Structures/Tree2.thy
 author nipkow Mon Jun 11 16:29:27 2018 +0200 (14 months ago) changeset 68413 b56ed5010e69 parent 68411 d8363de26567 child 68998 818898556504 permissions -rw-r--r--
tuned order of arguments
```     1 theory Tree2
```
```     2 imports Main
```
```     3 begin
```
```     4
```
```     5 datatype ('a,'b) tree =
```
```     6   Leaf ("\<langle>\<rangle>") |
```
```     7   Node "('a,'b)tree" 'a 'b "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)")
```
```     8
```
```     9 fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
```
```    10 "inorder Leaf = []" |
```
```    11 "inorder (Node l a _ r) = inorder l @ a # inorder r"
```
```    12
```
```    13 fun height :: "('a,'b) tree \<Rightarrow> nat" where
```
```    14 "height Leaf = 0" |
```
```    15 "height (Node l a _ r) = max (height l) (height r) + 1"
```
```    16
```
```    17 fun set_tree :: "('a,'b) tree \<Rightarrow> 'a set" where
```
```    18 "set_tree Leaf = {}" |
```
```    19 "set_tree (Node l a _ r) = Set.insert a (set_tree l \<union> set_tree r)"
```
```    20
```
```    21 fun bst :: "('a::linorder,'b) tree \<Rightarrow> bool" where
```
```    22 "bst Leaf = True" |
```
```    23 "bst (Node l a _ r) = (bst l \<and> bst r \<and> (\<forall>x \<in> set_tree l. x < a) \<and> (\<forall>x \<in> set_tree r. a < x))"
```
```    24
```
```    25 definition size1 :: "('a,'b) tree \<Rightarrow> nat" where
```
```    26 "size1 t = size t + 1"
```
```    27
```
```    28 lemma size1_simps[simp]:
```
```    29   "size1 \<langle>\<rangle> = 1"
```
```    30   "size1 \<langle>l, x, u, r\<rangle> = size1 l + size1 r"
```
```    31 by (simp_all add: size1_def)
```
```    32
```
```    33 lemma size1_ge0[simp]: "0 < size1 t"
```
```    34 by (simp add: size1_def)
```
```    35
```
```    36 lemma finite_set_tree[simp]: "finite(set_tree t)"
```
```    37 by(induction t) auto
```
```    38
```
```    39 end
```