tuned proofs
authorkuncar
Thu Oct 18 15:52:32 2012 +0200 (2012-10-18)
changeset 49928e3f0a92de280
parent 49927 cde0a46b4224
child 49929 70300f1b6835
tuned proofs
src/HOL/Library/RBT_Set.thy
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Oct 18 15:52:31 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Oct 18 15:52:32 2012 +0200
     1.3 @@ -140,18 +140,14 @@
     1.4  lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
     1.5  by (auto simp: not_Some_eq[THEN iffD1])
     1.6  
     1.7 +lemma Set_set_keys: "Set x = dom (lookup x)" 
     1.8 +by (auto simp: Set_def)
     1.9 +
    1.10  lemma finite_Set [simp, intro!]: "finite (Set x)"
    1.11 -proof -
    1.12 -  have "Set x = dom (lookup x)" by (auto simp: Set_def)
    1.13 -  then show ?thesis by simp
    1.14 -qed
    1.15 +by (simp add: Set_set_keys)
    1.16  
    1.17  lemma set_keys: "Set t = set(keys t)"
    1.18 -proof -
    1.19 - have "\<And>k. ((k, ()) \<in> set (entries t)) = (k \<in> set (keys t))" 
    1.20 -    by (simp add: keys_entries)
    1.21 -  then show ?thesis by (auto simp: lookup_in_tree Set_def)
    1.22 -qed
    1.23 +by (simp add: Set_set_keys lookup_keys)
    1.24  
    1.25  subsection {* fold and filter *}
    1.26