adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
authorbulwahn
Thu Nov 08 11:59:48 2012 +0100 (2012-11-08)
changeset 500277747a9f4c358
parent 50026 d9871e5ea0e1
child 50028 d05f859558a0
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
src/HOL/BNF/More_BNFs.thy
src/HOL/List.thy
src/HOL/Matrix_LP/Matrix.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Probability/Lebesgue_Integration.thy
     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.11 +declare [[simproc add: finite_Collect]]
    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.15 +declare [[simproc add: finite_Collect]]
    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.5    by (simp add: point_measure_def)
     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
    7.15 +declare [[simproc add: finite_Collect]]
    7.16  
    7.17  lemma emeasure_point_measure_finite:
    7.18    "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)"