# HG changeset patch
# User nipkow
# Date 1582802296 -3600
# Node ID 059c55b617343f6c80842ffe920274cfafd5174f
# Parent  0e1b9b308d8f3f25c88fd5d3cbe8738f4258334d
removed dead lemma

diff -r 0e1b9b308d8f -r 059c55b61734 src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Wed Feb 26 23:49:16 2020 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Thu Feb 27 12:18:16 2020 +0100
@@ -445,20 +445,15 @@
 
 subsection \<open>Height-Size Relation\<close>
 
-text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
-
-lemma height_invers: 
-  "(height t = 0) = (t = Leaf)"
-  "avl t \<Longrightarrow> (height t = Suc n) = (\<exists> l a r . t = Node l (a,Suc n) r)"
-by (induction t) auto
+text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich, much simplified.\<close>
 
 text \<open>Any AVL tree of height \<open>n\<close> has at least \<open>fib (n+2)\<close> leaves:\<close>
 
 lemma avl_fib_bound: "avl t \<Longrightarrow> height t = n \<Longrightarrow> fib (n+2) \<le> size1 t"
 proof (induction n arbitrary: t rule: fib.induct)
-  case 1 thus ?case by (simp add: height_invers)
+  case 1 thus ?case by (simp)
 next
-  case 2 thus ?case by (cases t) (auto simp: height_invers)
+  case 2 thus ?case by (cases t) (auto)
 next
   case (3 h)
   from "3.prems" obtain l a r where