# HG changeset patch
# User traytel
# Date 1385710005 -3600
# Node ID 31afce809794e0f08272a0ed211113ec980be813
# Parent  6593e06445e67e7708131db599efbc9effc68049
set_comprehension_pointfree simproc causes to many surprises if enabled by default

diff -r 6593e06445e6 -r 31afce809794 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Nov 28 22:03:41 2013 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Nov 29 08:26:45 2013 +0100
@@ -18,6 +18,8 @@
 
 simproc_setup finite_Collect ("finite (Collect P)") = {* K Set_Comprehension_Pointfree.simproc *}
 
+declare [[simproc del: finite_Collect]]
+
 lemma finite_induct [case_names empty insert, induct set: finite]:
   -- {* Discharging @{text "x \<notin> F"} entails extra work. *}
   assumes "finite F"
diff -r 6593e06445e6 -r 31afce809794 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Thu Nov 28 22:03:41 2013 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Fri Nov 29 08:26:45 2013 +0100
@@ -131,10 +131,8 @@
 lemma finite [iff]: "finite (carrier R)"
   by (subst res_carrier_eq, auto)
 
-declare [[simproc del: finite_Collect]]
 lemma finite_Units [iff]: "finite (Units R)"
   by (subst res_units_eq) auto
-declare [[simproc add: finite_Collect]]
 
 (* The function a -> a mod m maps the integers to the
    residue classes. The following lemmas show that this mapping
diff -r 6593e06445e6 -r 31afce809794 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Nov 28 22:03:41 2013 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Nov 29 08:26:45 2013 +0100
@@ -359,7 +359,6 @@
   apply auto
   done
 
-declare [[simproc del: finite_Collect]]
 lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow> 
     finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
       prime_factors n = S"
@@ -832,7 +831,5 @@
   apply auto
   done
 
-declare [[simproc add: finite_Collect]]
-
 end
 
diff -r 6593e06445e6 -r 31afce809794 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Nov 28 22:03:41 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Nov 29 08:26:45 2013 +0100
@@ -2860,7 +2860,6 @@
   "simple_function (point_measure A f) g \<longleftrightarrow> finite (g ` A)"
   by (simp add: point_measure_def)
 
-declare [[simproc del: finite_Collect]]
 lemma emeasure_point_measure:
   assumes A: "finite {a\<in>X. 0 < f a}" "X \<subseteq> A"
   shows "emeasure (point_measure A f) X = (\<Sum>a|a\<in>X \<and> 0 < f a. f a)"
@@ -2871,7 +2870,6 @@
     by (simp add: emeasure_density positive_integral_count_space ereal_zero_le_0_iff
                   point_measure_def indicator_def)
 qed
-declare [[simproc add: finite_Collect]]
 
 lemma emeasure_point_measure_finite:
   "finite A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (point_measure A f) X = (\<Sum>a\<in>X. f a)"
diff -r 6593e06445e6 -r 31afce809794 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Nov 28 22:03:41 2013 +0100
+++ b/src/HOL/Relation.thy	Fri Nov 29 08:26:45 2013 +0100
@@ -760,7 +760,8 @@
   by (auto simp: total_on_def)
 
 lemma finite_converse [iff]: "finite (r^-1) = finite r"  
-  unfolding converse_def conversep_iff by (auto elim: finite_imageD simp: inj_on_def)
+  unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
+  by (auto elim: finite_imageD simp: inj_on_def)
 
 lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
   by (auto simp add: fun_eq_iff)
diff -r 6593e06445e6 -r 31afce809794 src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy
--- a/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Thu Nov 28 22:03:41 2013 +0100
+++ b/src/HOL/ex/Set_Comprehension_Pointfree_Tests.thy	Fri Nov 29 08:26:45 2013 +0100
@@ -9,6 +9,8 @@
 imports Main
 begin
 
+declare [[simproc add: finite_Collect]]
+
 lemma
   "finite (UNIV::'a set) ==> finite {p. EX x::'a. p = (x, x)}"
   by simp
@@ -114,6 +116,8 @@
    = finite ((\<lambda>(b :: ?'B, a:: ?'A). Pair_Rep a b) ` (UNIV \<times> UNIV))"
   by simp
 
+declare [[simproc del: finite_Collect]]
+
 
 section {* Testing simproc in code generation *}