added lemmas
authornipkow
Sun Sep 17 21:04:02 2017 +0200 (21 months ago)
changeset 66659d5bf4bdb4fb7
parent 66658 59acf5e73176
child 66660 bc3584f7ac0c
added lemmas
src/HOL/Library/Tree.thy
     1.1 --- a/src/HOL/Library/Tree.thy	Thu Sep 14 19:21:32 2017 +0200
     1.2 +++ b/src/HOL/Library/Tree.thy	Sun Sep 17 21:04:02 2017 +0200
     1.3 @@ -475,6 +475,12 @@
     1.4  lemma height_mirror[simp]: "height(mirror t) = height t"
     1.5  by (induction t) simp_all
     1.6  
     1.7 +lemma min_height_mirror [simp]: "min_height (mirror t) = min_height t"
     1.8 +by (induction t) simp_all  
     1.9 +
    1.10 +lemma ipl_mirror [simp]: "ipl (mirror t) = ipl t"
    1.11 +by (induction t) simp_all
    1.12 +
    1.13  lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)"
    1.14  by (induction t) simp_all
    1.15