| changeset 70745 | be8e617b6eb3 |
| parent 70744 | b605c9cf82a2 |
| child 70755 | 3fb16bed5d6c |
| 70744:b605c9cf82a2 | 70745:be8e617b6eb3 |
|---|---|
37 by (simp add: size1_size) |
37 by (simp add: size1_size) |
38 |
38 |
39 lemma finite_set_tree[simp]: "finite(set_tree t)" |
39 lemma finite_set_tree[simp]: "finite(set_tree t)" |
40 by(induction t) auto |
40 by(induction t) auto |
41 |
41 |
42 lemma set_tree_empty: "set_tree t = {} \<longleftrightarrow> t = Leaf" |
42 lemma eq_set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf" |
43 by (cases t) auto |
43 by (cases t) auto |
44 |
44 |
45 end |
45 end |