more lemmas
authornipkow
Fri Mar 31 17:21:36 2017 +0200 (2017-03-31)
changeset 65339c4531ddafe72
parent 65338 2ffda850f844
child 65340 8ec91f7eca37
more lemmas
src/HOL/Library/Tree.thy
     1.1 --- a/src/HOL/Library/Tree.thy	Thu Mar 23 17:20:47 2017 +0100
     1.2 +++ b/src/HOL/Library/Tree.thy	Fri Mar 31 17:21:36 2017 +0200
     1.3 @@ -93,6 +93,15 @@
     1.4    (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
     1.5  
     1.6  
     1.7 +subsection \<open>@{const map_tree}\<close>
     1.8 +
     1.9 +lemma map_tree_Leaf[simp]: "map_tree f t = Leaf \<longleftrightarrow> t = Leaf"
    1.10 +by (rule tree.map_disc_iff)
    1.11 +
    1.12 +lemma Leaf_map_tree[simp]: "Leaf = map_tree f t \<longleftrightarrow> t = Leaf"
    1.13 +by (cases t) auto
    1.14 +
    1.15 +
    1.16  subsection \<open>@{const size}\<close>
    1.17  
    1.18  lemma size1_simps[simp]:
    1.19 @@ -103,15 +112,15 @@
    1.20  lemma size1_ge0[simp]: "0 < size1 t"
    1.21  by (simp add: size1_def)
    1.22  
    1.23 -lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf"
    1.24 +lemma size_0_iff_Leaf[simp]: "size t = 0 \<longleftrightarrow> t = Leaf"
    1.25 +by(cases t) auto
    1.26 +
    1.27 +lemma Z_size_iff_Leaf[simp]: "0 = size t \<longleftrightarrow> t = Leaf"
    1.28  by(cases t) auto
    1.29  
    1.30  lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"
    1.31  by (cases t) auto
    1.32  
    1.33 -lemma finite_set_tree[simp]: "finite(set_tree t)"
    1.34 -by(induction t) auto
    1.35 -
    1.36  lemma size_map_tree[simp]: "size (map_tree f t) = size t"
    1.37  by (induction t) auto
    1.38  
    1.39 @@ -119,6 +128,18 @@
    1.40  by (simp add: size1_def)
    1.41  
    1.42  
    1.43 +subsection \<open>@{const set_tree}\<close>
    1.44 +
    1.45 +lemma set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf"
    1.46 +by (cases t) auto
    1.47 +
    1.48 +lemma empty_set_tree[simp]: "{} = set_tree t \<longleftrightarrow> t = Leaf"
    1.49 +by (cases t) auto
    1.50 +
    1.51 +lemma finite_set_tree[simp]: "finite(set_tree t)"
    1.52 +by(induction t) auto
    1.53 +
    1.54 +
    1.55  subsection \<open>@{const subtrees}\<close>
    1.56  
    1.57  lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t"
    1.58 @@ -133,7 +154,10 @@
    1.59  
    1.60  subsection \<open>@{const height} and @{const min_height}\<close>
    1.61  
    1.62 -lemma height_0_iff_Leaf: "height t = 0 \<longleftrightarrow> t = Leaf"
    1.63 +lemma height_0_iff_Leaf[simp]: "height t = 0 \<longleftrightarrow> t = Leaf"
    1.64 +by(cases t) auto
    1.65 +
    1.66 +lemma Z_height_iff_Leaf[simp]: "0 = height t \<longleftrightarrow> t = Leaf"
    1.67  by(cases t) auto
    1.68  
    1.69  lemma height_map_tree[simp]: "height (map_tree f t) = height t"
    1.70 @@ -370,6 +394,12 @@
    1.71  
    1.72  subsection "List of entries"
    1.73  
    1.74 +lemma inorder_Nil_iff[simp]: "inorder t = [] \<longleftrightarrow> t = Leaf"
    1.75 +by (cases t) auto
    1.76 +
    1.77 +lemma Nil_inorder_iff[simp]: "[] = inorder t \<longleftrightarrow> t = Leaf"
    1.78 +by (cases t) auto
    1.79 +
    1.80  lemma set_inorder[simp]: "set (inorder t) = set_tree t"
    1.81  by (induction t) auto
    1.82  
    1.83 @@ -432,6 +462,9 @@
    1.84  lemma mirror_Leaf[simp]: "mirror t = \<langle>\<rangle> \<longleftrightarrow> t = \<langle>\<rangle>"
    1.85  by (induction t) simp_all
    1.86  
    1.87 +lemma Leaf_mirror[simp]: "\<langle>\<rangle> = mirror t \<longleftrightarrow> t = \<langle>\<rangle>"
    1.88 +using mirror_Leaf by fastforce
    1.89 +
    1.90  lemma size_mirror[simp]: "size(mirror t) = size t"
    1.91  by (induction t) simp_all
    1.92