src/HOL/Library/Tree.thy
changeset 62650 7e6bb43e7217
parent 62202 e5bc7cbb0bcc
child 63036 1ba3aacfa4d3
equal deleted inserted replaced
62649:d23be25c0835 62650:7e6bb43e7217
    21 
    21 
    22 lemma size1_simps[simp]:
    22 lemma size1_simps[simp]:
    23   "size1 \<langle>\<rangle> = 1"
    23   "size1 \<langle>\<rangle> = 1"
    24   "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
    24   "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r"
    25 by (simp_all add: size1_def)
    25 by (simp_all add: size1_def)
       
    26 
       
    27 lemma size1_ge0[simp]: "0 < size1 t"
       
    28 by (simp add: size1_def)
    26 
    29 
    27 lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf"
    30 lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf"
    28 by(cases t) auto
    31 by(cases t) auto
    29 
    32 
    30 lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"
    33 lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"