inf/sup_absorb are no default simp rules any longer
authorhaftmann
Wed Sep 23 08:25:51 2009 +0200 (2009-09-23)
changeset 32698be4b248616c0
parent 32697 72e8608dce54
child 32699 250b4d8342ca
inf/sup_absorb are no default simp rules any longer
src/HOL/Finite_Set.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Sep 22 15:39:46 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Sep 23 08:25:51 2009 +0200
     1.3 @@ -1565,7 +1565,7 @@
     1.4    apply (rule finite_subset)
     1.5    prefer 2
     1.6    apply assumption
     1.7 -  apply auto
     1.8 +  apply (auto simp add: sup_absorb2)
     1.9  done
    1.10  
    1.11  lemma setsum_right_distrib: 
     2.1 --- a/src/HOL/Library/Euclidean_Space.thy	Tue Sep 22 15:39:46 2009 +0200
     2.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Sep 23 08:25:51 2009 +0200
     2.3 @@ -3649,7 +3649,7 @@
     2.4      from setsum_restrict_set[OF fS, of "\<lambda>v. u v *s v" S', symmetric] SS'
     2.5      have "setsum (\<lambda>v. ?u v *s v) S = setsum (\<lambda>v. u v *s v) S'"
     2.6        unfolding cond_value_iff cond_application_beta
     2.7 -      by (simp add: cond_value_iff cong del: if_weak_cong)
     2.8 +      by (simp add: cond_value_iff inf_absorb2 cong del: if_weak_cong)
     2.9      hence "setsum (\<lambda>v. ?u v *s v) S = y" by (metis u)
    2.10      hence "y \<in> ?rhs" by auto}
    2.11    moreover
     3.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Sep 22 15:39:46 2009 +0200
     3.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Wed Sep 23 08:25:51 2009 +0200
     3.3 @@ -99,7 +99,7 @@
     3.4  
     3.5  lemma Diff_Diff_Int: "A - (A - B) = A \<inter> B" by blast
     3.6  lemma openin_closedin_eq: "openin U S \<longleftrightarrow> S \<subseteq> topspace U \<and> closedin U (topspace U - S)"
     3.7 -  apply (auto simp add: closedin_def Diff_Diff_Int)
     3.8 +  apply (auto simp add: closedin_def Diff_Diff_Int inf_absorb2)
     3.9    apply (metis openin_subset subset_eq)
    3.10    done
    3.11