author bulwahn Thu Nov 08 11:59:48 2012 +0100 (2012-11-08) changeset 50027 7747a9f4c358 parent 50026 d9871e5ea0e1 child 50028 d05f859558a0
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
 src/HOL/BNF/More_BNFs.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions src/HOL/Matrix_LP/Matrix.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy file | annotate | diff | revisions src/HOL/Number_Theory/Residues.thy file | annotate | diff | revisions src/HOL/Number_Theory/UniqueFactorization.thy file | annotate | diff | revisions src/HOL/Probability/Lebesgue_Integration.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/BNF/More_BNFs.thy	Thu Nov 08 11:59:47 2012 +0100
1.2 +++ b/src/HOL/BNF/More_BNFs.thy	Thu Nov 08 11:59:48 2012 +0100
1.3 @@ -707,7 +707,7 @@
1.4  shows "b = b'"
1.5  proof-
1.6    have "finite ?A'" using f unfolding multiset_def by auto
1.7 -  hence "?A' \<noteq> {}" using 1 setsum_gt_0_iff by auto
1.8 +  hence "?A' \<noteq> {}" using 1 by (auto simp add: setsum_gt_0_iff)
1.9    thus ?thesis using 2 by auto
1.10  qed
1.11
1.12 @@ -722,7 +722,7 @@
1.13    let ?B = "{b. h2 b = c \<and> 0 < setsum f (?As b)}"
1.14    have 0: "{?As b | b.  b \<in> ?B} = ?As ` ?B" by auto
1.15    have "\<And> b. finite (?As b)" using f unfolding multiset_def by simp
1.16 -  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
1.17 +  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
1.18    hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
1.19    have "setsum f ?A = setsum (setsum f) {?As b | b.  b \<in> ?B}"
1.20    unfolding A apply(rule setsum_Union_disjoint)
1.21 @@ -749,7 +749,7 @@
1.22    (is "finite {b. 0 < setsum f (?As b)}")
1.23    proof- let ?B = "{b. 0 < setsum f (?As b)}"
1.24      have "\<And> b. finite (?As b)" using assms unfolding multiset_def by simp
1.25 -    hence B: "?B = {b. ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
1.26 +    hence B: "?B = {b. ?As b \<noteq> {}}" by (auto simp add: setsum_gt_0_iff)
1.27      hence "?B \<subseteq> h ` ?A" by auto
1.28      thus ?thesis using finite_surj[OF fin] by auto
1.29    qed
1.30 @@ -769,7 +769,7 @@
1.31    have "\<And> b. finite {a. h a = b \<and> 0 < f a}" (is "\<And> b. finite (?As b)")
1.32    using f unfolding multiset_def by auto
1.33    thus "{b. 0 < setsum f (?As b)} = h ` {a. 0 < f a}"
1.34 -  using setsum_gt_0_iff by auto
1.35 +  by (auto simp add:  setsum_gt_0_iff)
1.36  qed
1.37
1.38  lemma mmap_image:
```
```     2.1 --- a/src/HOL/List.thy	Thu Nov 08 11:59:47 2012 +0100
2.2 +++ b/src/HOL/List.thy	Thu Nov 08 11:59:48 2012 +0100
2.3 @@ -4026,7 +4026,7 @@
2.4   (is "finite ?S")
2.5  proof-
2.6    have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
2.7 -  thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
2.8 +  thus ?thesis by (auto intro!: finite_lists_length_eq[OF `finite A`] simp only:)
2.9  qed
2.10
2.11  lemma card_lists_length_le:
```
```     3.1 --- a/src/HOL/Matrix_LP/Matrix.thy	Thu Nov 08 11:59:47 2012 +0100
3.2 +++ b/src/HOL/Matrix_LP/Matrix.thy	Thu Nov 08 11:59:48 2012 +0100
3.3 @@ -214,26 +214,8 @@
3.4    ultimately show "finite {x. x < Suc n}" by (simp)
3.5  qed
3.6
3.7 -lemma finite_natarray2: "finite {pos. (fst pos) < (m::nat) & (snd pos) < (n::nat)}"
3.8 -  apply (induct m)
3.9 -  apply (simp+)
3.10 -  proof -
3.11 -    fix m::nat
3.12 -    let ?s0 = "{pos. fst pos < m & snd pos < n}"
3.13 -    let ?s1 = "{pos. fst pos < (Suc m) & snd pos < n}"
3.14 -    let ?sd = "{pos. fst pos = m & snd pos < n}"
3.15 -    assume f0: "finite ?s0"
3.16 -    have f1: "finite ?sd"
3.17 -    proof -
3.18 -      let ?f = "% x. (m, x)"
3.19 -      have "{pos. fst pos = m & snd pos < n} = ?f ` {x. x < n}" by (rule set_eqI, simp add: image_def, auto)
3.20 -      moreover have "finite {x. x < n}" by (simp add: finite_natarray1)
3.21 -      ultimately show "finite {pos. fst pos = m & snd pos < n}" by (simp)
3.22 -    qed
3.23 -    have su: "?s0 \<union> ?sd = ?s1" by (rule set_eqI, simp, arith)
3.24 -    from f0 f1 have "finite (?s0 \<union> ?sd)" by (rule finite_UnI)
3.25 -    with su show "finite ?s1" by (simp)
3.26 -qed
3.27 +lemma finite_natarray2: "finite {(x, y). x < (m::nat) & y < (n::nat)}"
3.28 +by simp
3.29
3.30  lemma RepAbs_matrix:
3.31    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)
3.32 @@ -243,8 +225,8 @@
3.33  proof -
3.34    from aem obtain m where a: "! j i. m <= j \<longrightarrow> x j i = 0" by (blast)
3.35    from aen obtain n where b: "! j i. n <= i \<longrightarrow> x j i = 0" by (blast)
3.36 -  let ?u = "{pos. x (fst pos) (snd pos) \<noteq> 0}"
3.37 -  let ?v = "{pos. fst pos < m & snd pos < n}"
3.38 +  let ?u = "{(i, j). x i j \<noteq> 0}"
3.39 +  let ?v = "{(i, j). i < m & j < n}"
3.40    have c: "!! (m::nat) a. ~(m <= a) \<Longrightarrow> a < m" by (arith)
3.41    from a b have "(?u \<inter> (-?v)) = {}"
3.42      apply (simp)
3.43 @@ -254,7 +236,9 @@
3.44      by (rule c, auto)+
3.45    then have d: "?u \<subseteq> ?v" by blast
3.46    moreover have "finite ?v" by (simp add: finite_natarray2)
3.47 -  ultimately show "finite ?u" by (rule finite_subset)
3.48 +  moreover have "{pos. x (fst pos) (snd pos) \<noteq> 0} = ?u" by auto
3.49 +  ultimately show "finite {pos. x (fst pos) (snd pos) \<noteq> 0}"
3.50 +    by (metis (lifting) finite_subset)
3.51  qed
3.52
3.53  definition apply_infmatrix :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a infmatrix \<Rightarrow> 'b infmatrix" where
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Nov 08 11:59:47 2012 +0100
4.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Nov 08 11:59:48 2012 +0100
4.3 @@ -693,6 +693,7 @@
4.4
4.5  subsection {* The lemmas about simplices that we need. *}
4.6
4.7 +(* FIXME: These are clones of lemmas in Library/FuncSet *)
4.8  lemma card_funspace': assumes "finite s" "finite t" "card s = m" "card t = n"
4.9    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) = _")
4.10    using assms apply - proof(induct m arbitrary: s)
4.11 @@ -731,7 +732,7 @@
4.12    case True
4.13    have "card ?S = (card t) ^ (card s)"
4.14      using assms by (auto intro!: card_funspace)
4.15 -  thus ?thesis using True by (auto intro: card_ge_0_finite)
4.16 +  thus ?thesis using True by (rule_tac card_ge_0_finite) simp
4.17  next
4.18    case False hence "t = {}" using `finite t` by auto
4.19    show ?thesis
```
```     5.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu Nov 08 11:59:47 2012 +0100
5.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu Nov 08 11:59:48 2012 +0100
5.3 @@ -131,8 +131,10 @@
5.4  lemma finite [iff]: "finite (carrier R)"
5.5    by (subst res_carrier_eq, auto)
5.6
5.7 +declare [[simproc del: finite_Collect]]
5.8  lemma finite_Units [iff]: "finite (Units R)"
5.9 -  by (subst res_units_eq, auto)
5.10 +  by (subst res_units_eq) auto
5.12
5.13  (* The function a -> a mod m maps the integers to the
5.14     residue classes. The following lemmas show that this mapping
```
```     6.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Nov 08 11:59:47 2012 +0100
6.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Nov 08 11:59:48 2012 +0100
6.3 @@ -421,6 +421,7 @@
6.4    apply auto
6.5    done
6.6
6.7 +declare [[simproc del: finite_Collect]]
6.8  lemma prime_factors_characterization_int: "S = {p. 0 < f (p::int)} \<Longrightarrow>
6.9      finite S \<Longrightarrow> (ALL p:S. prime p) \<Longrightarrow> n = (PROD p:S. p ^ f p) \<Longrightarrow>
6.10        prime_factors n = S"
6.11 @@ -893,5 +894,7 @@
6.12    apply auto
6.13    done
6.14
6.16 +
6.17  end
6.18
```
```     7.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Nov 08 11:59:47 2012 +0100
7.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Nov 08 11:59:48 2012 +0100
7.3 @@ -2657,6 +2657,7 @@
7.4    "simple_function (point_measure A f) g \<longleftrightarrow> finite (g ` A)"
7.6
7.7 +declare [[simproc del: finite_Collect]]
7.8  lemma emeasure_point_measure:
7.9    assumes A: "finite {a\<in>X. 0 < f a}" "X \<subseteq> A"
7.10    shows "emeasure (point_measure A f) X = (\<Sum>a|a\<in>X \<and> 0 < f a. f a)"
7.11 @@ -2667,6 +2668,7 @@
7.12      by (simp add: emeasure_density positive_integral_count_space ereal_zero_le_0_iff
7.13                    point_measure_def indicator_def)
7.14  qed