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