equal
deleted
inserted
replaced
473 by (simp add: size1_def) |
473 by (simp add: size1_def) |
474 |
474 |
475 lemma height_mirror[simp]: "height(mirror t) = height t" |
475 lemma height_mirror[simp]: "height(mirror t) = height t" |
476 by (induction t) simp_all |
476 by (induction t) simp_all |
477 |
477 |
|
478 lemma min_height_mirror [simp]: "min_height (mirror t) = min_height t" |
|
479 by (induction t) simp_all |
|
480 |
|
481 lemma ipl_mirror [simp]: "ipl (mirror t) = ipl t" |
|
482 by (induction t) simp_all |
|
483 |
478 lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)" |
484 lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)" |
479 by (induction t) simp_all |
485 by (induction t) simp_all |
480 |
486 |
481 lemma map_mirror: "map_tree f (mirror t) = mirror (map_tree f t)" |
487 lemma map_mirror: "map_tree f (mirror t) = mirror (map_tree f t)" |
482 by (induction t) simp_all |
488 by (induction t) simp_all |