added lemmas
authornipkow
Sun, 17 Sep 2017 21:04:02 +0200
changeset 66661 d5bf4bdb4fb7
parent 66660 59acf5e73176
child 66662 bc3584f7ac0c
added lemmas
src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Sep 14 19:21:32 2017 +0200
+++ b/src/HOL/Library/Tree.thy	Sun Sep 17 21:04:02 2017 +0200
@@ -475,6 +475,12 @@
 lemma height_mirror[simp]: "height(mirror t) = height t"
 by (induction t) simp_all
 
+lemma min_height_mirror [simp]: "min_height (mirror t) = min_height t"
+by (induction t) simp_all  
+
+lemma ipl_mirror [simp]: "ipl (mirror t) = ipl t"
+by (induction t) simp_all
+
 lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)"
 by (induction t) simp_all