src/HOL/Data_Structures/Tree2.thy
changeset 68413 b56ed5010e69
parent 68411 d8363de26567
child 68998 818898556504
     1.1 --- a/src/HOL/Data_Structures/Tree2.thy	Mon Jun 11 08:15:43 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/Tree2.thy	Mon Jun 11 16:29:27 2018 +0200
     1.3 @@ -4,30 +4,30 @@
     1.4  
     1.5  datatype ('a,'b) tree =
     1.6    Leaf ("\<langle>\<rangle>") |
     1.7 -  Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)")
     1.8 +  Node "('a,'b)tree" 'a 'b "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)")
     1.9  
    1.10  fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
    1.11  "inorder Leaf = []" |
    1.12 -"inorder (Node _ l a r) = inorder l @ a # inorder r"
    1.13 +"inorder (Node l a _ r) = inorder l @ a # inorder r"
    1.14  
    1.15  fun height :: "('a,'b) tree \<Rightarrow> nat" where
    1.16  "height Leaf = 0" |
    1.17 -"height (Node _ l a r) = max (height l) (height r) + 1"
    1.18 +"height (Node l a _ r) = max (height l) (height r) + 1"
    1.19  
    1.20  fun set_tree :: "('a,'b) tree \<Rightarrow> 'a set" where
    1.21  "set_tree Leaf = {}" |
    1.22 -"set_tree (Node _ l x r) = Set.insert x (set_tree l \<union> set_tree r)"
    1.23 +"set_tree (Node l a _ r) = Set.insert a (set_tree l \<union> set_tree r)"
    1.24  
    1.25  fun bst :: "('a::linorder,'b) tree \<Rightarrow> bool" where
    1.26  "bst Leaf = True" |
    1.27 -"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))"
    1.28 +"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))"
    1.29  
    1.30  definition size1 :: "('a,'b) tree \<Rightarrow> nat" where
    1.31  "size1 t = size t + 1"
    1.32  
    1.33  lemma size1_simps[simp]:
    1.34    "size1 \<langle>\<rangle> = 1"
    1.35 -  "size1 \<langle>u, l, x, r\<rangle> = size1 l + size1 r"
    1.36 +  "size1 \<langle>l, x, u, r\<rangle> = size1 l + size1 r"
    1.37  by (simp_all add: size1_def)
    1.38  
    1.39  lemma size1_ge0[simp]: "0 < size1 t"