# HG changeset patch
# User bulwahn
# Date 1352372388 -3600
# Node ID 7747a9f4c3587cdfd12e1ff8bd2b5e68fc3a55c9
# Parent  d9871e5ea0e1ec4c72c7d6c8d40c9532c218c97f
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs

diff -r d9871e5ea0e1 -r 7747a9f4c358 src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Thu Nov 08 11:59:48 2012 +0100
@@ -707,7 +707,7 @@
 shows "b = b'"
 proof-
   have "finite ?A'" using f unfolding multiset_def by auto
-  hence "?A' \<noteq> {}" using 1 setsum_gt_0_iff by auto
+  hence "?A' \<noteq> {}" using 1 by (auto simp add: setsum_gt_0_iff)
   thus ?thesis using 2 by auto
 qed
 
@@ -722,7 +722,7 @@
   let ?B = "{b. h2 b = c \<and> 0 < setsum f (?As b)}"
   have 0: "{?As b | b.  b \<in> ?B} = ?As ` ?B" by auto
   have "\<And> b. finite (?As b)" using f unfolding multiset_def by simp
-  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
+  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
   hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
   have "setsum f ?A = setsum (setsum f) {?As b | b.  b \<in> ?B}"
   unfolding A apply(rule setsum_Union_disjoint)
@@ -749,7 +749,7 @@
   (is "finite {b. 0 < setsum f (?As b)}")
   proof- let ?B = "{b. 0 < setsum f (?As b)}"
     have "\<And> b. finite (?As b)" using assms unfolding multiset_def by simp
-    hence B: "?B = {b. ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
+    hence B: "?B = {b. ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
     hence "?B \<subseteq> h ` ?A" by auto
     thus ?thesis using finite_surj[OF fin] by auto
   qed
@@ -769,7 +769,7 @@
   have "\<And> b. finite {a. h a = b \<and> 0 < f a}" (is "\<And> b. finite (?As b)")
   using f unfolding multiset_def by auto
   thus "{b. 0 < setsum f (?As b)} = h ` {a. 0 < f a}"
-  using setsum_gt_0_iff by auto
+  by (auto simp add:  setsum_gt_0_iff)
 qed
 
 lemma mmap_image:
diff -r d9871e5ea0e1 -r 7747a9f4c358 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/List.thy	Thu Nov 08 11:59:48 2012 +0100
@@ -4026,7 +4026,7 @@
  (is "finite ?S")
 proof-
   have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
-  thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
+  thus ?thesis by (auto intro!: finite_lists_length_eq[OF `finite A`] simp only:)
 qed
 
 lemma card_lists_length_le:
diff -r d9871e5ea0e1 -r 7747a9f4c358 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy	Thu Nov 08 11:59:48 2012 +0100
@@ -214,26 +214,8 @@
   ultimately show "finite {x. x < Suc n}" by (simp)
 qed
 
-lemma finite_natarray2: "finite {pos. (fst pos) < (m::nat) & (snd pos) < (n::nat)}"
-  apply (induct m)
-  apply (simp+)
-  proof -
-    fix m::nat
-    let ?s0 = "{pos. fst pos < m & snd pos < n}"
-    let ?s1 = "{pos. fst pos < (Suc m) & snd pos < n}"
-    let ?sd = "{pos. fst pos = m & snd pos < n}"
-    assume f0: "finite ?s0"
-    have f1: "finite ?sd"
-    proof -
-      let ?f = "% x. (m, x)"
-      have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_eqI, simp add: image_def, auto)
-      moreover have "finite {x. x < n}" by (simp add: finite_natarray1)
-      ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp)
-    qed
-    have su: "?s0 \<union> ?sd = ?s1" by (rule set_eqI, simp, arith)
-    from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI)
-    with su show "finite ?s1" by (simp)
-qed
+lemma finite_natarray2: "finite {(x, y). x < (m::nat) & y < (n::nat)}"
+by simp
 
 lemma RepAbs_matrix:
   assumes aem: "? m. ! j i. m <= j \<longrightarrow> x j i = 0" (is ?em) and aen:"? n. ! j i. (n <= i \<longrightarrow> x j i = 0)" (is ?en)
@@ -243,8 +225,8 @@
 proof -
   from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast)
   from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast)
-  let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}"
-  let ?v = "{pos. fst pos < m & snd pos < n}"
+  let ?u = "{(i, j). x i j \<noteq> 0}"
+  let ?v = "{(i, j). i < m & j < n}"
   have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)
   from a b have "(?u \<inter> (-?v)) = {}"
     apply (simp)
@@ -254,7 +236,9 @@
     by (rule c, auto)+
   then have d: "?u \<subseteq> ?v" by blast
   moreover have "finite ?v" by (simp add: finite_natarray2)
-  ultimately show "finite ?u" by (rule finite_subset)
+  moreover have "{pos. x (fst pos) (snd pos) \<noteq> 0} = ?u" by auto
+  ultimately show "finite {pos. x (fst pos) (snd pos) \<noteq> 0}"
+    by (metis (lifting) finite_subset)
 qed
 
 definition apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix" where
diff -r d9871e5ea0e1 -r 7747a9f4c358 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Nov 08 11:59:48 2012 +0100
@@ -693,6 +693,7 @@
 
 subsection {* The lemmas about simplices that we need. *}
 
+(* FIXME: These are clones of lemmas in Library/FuncSet *) 
 lemma card_funspace': assumes "finite s" "finite t" "card s = m" "card t = n"
   shows "card {f. (\<forall>x\<in>s. f x \<in> t) \<and> (\<forall>x\<in>UNIV - s. f x = d)} = n ^ m" (is "card (?M s) = _")
   using assms apply - proof(induct m arbitrary: s)
@@ -731,7 +732,7 @@
   case True
   have "card ?S = (card t) ^ (card s)"
     using assms by (auto intro!: card_funspace)
-  thus ?thesis using True by (auto intro: card_ge_0_finite)
+  thus ?thesis using True by (rule_tac card_ge_0_finite) simp
 next
   case False hence "t = {}" using `finite t` by auto
   show ?thesis
diff -r d9871e5ea0e1 -r 7747a9f4c358 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Thu Nov 08 11:59:48 2012 +0100
@@ -131,8 +131,10 @@
 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)
+  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 d9871e5ea0e1 -r 7747a9f4c358 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Nov 08 11:59:48 2012 +0100
@@ -421,6 +421,7 @@
   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"
@@ -893,5 +894,7 @@
   apply auto
   done
 
+declare [[simproc add: finite_Collect]]
+
 end
 
diff -r d9871e5ea0e1 -r 7747a9f4c358 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Nov 08 11:59:47 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Nov 08 11:59:48 2012 +0100
@@ -2657,6 +2657,7 @@
   "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)"
@@ -2667,6 +2668,7 @@
     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)"