author haftmann Sat Jul 02 08:41:05 2016 +0200 (2016-07-02) changeset 63365 5340fb6633d0 parent 63364 4fa441c2f20c child 63366 209c4cbbc4cd
more theorems
 src/HOL/Complete_Lattices.thy file | annotate | diff | revisions src/HOL/Finite_Set.thy file | annotate | diff | revisions src/HOL/Fun.thy file | annotate | diff | revisions src/HOL/Hilbert_Choice.thy file | annotate | diff | revisions src/HOL/List.thy file | annotate | diff | revisions src/HOL/MacLaurin.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy file | annotate | diff | revisions src/HOL/Series.thy file | annotate | diff | revisions src/HOL/Set.thy file | annotate | diff | revisions src/HOL/Set_Interval.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Complete_Lattices.thy	Sat Jul 02 08:41:05 2016 +0200
1.2 +++ b/src/HOL/Complete_Lattices.thy	Sat Jul 02 08:41:05 2016 +0200
1.3 @@ -1402,7 +1402,26 @@
1.4  lemma UNION_fun_upd:
1.5    "UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
1.6    by (auto simp add: set_eq_iff)
1.7 -
1.8 +
1.9 +lemma bij_betw_Pow:
1.10 +  assumes "bij_betw f A B"
1.11 +  shows "bij_betw (image f) (Pow A) (Pow B)"
1.12 +proof -
1.13 +  from assms have "inj_on f A"
1.14 +    by (rule bij_betw_imp_inj_on)
1.15 +  then have "inj_on f (\<Union>Pow A)"
1.16 +    by simp
1.17 +  then have "inj_on (image f) (Pow A)"
1.18 +    by (rule inj_on_image)
1.19 +  then have "bij_betw (image f) (Pow A) (image f ` Pow A)"
1.20 +    by (rule inj_on_imp_bij_betw)
1.21 +  moreover from assms have "f ` A = B"
1.22 +    by (rule bij_betw_imp_surj_on)
1.23 +  then have "image f ` Pow A = Pow B"
1.24 +    by (rule image_Pow_surj)
1.25 +  ultimately show ?thesis by simp
1.26 +qed
1.27 +
1.28
1.29  subsubsection \<open>Complement\<close>
1.30
```
```     2.1 --- a/src/HOL/Finite_Set.thy	Sat Jul 02 08:41:05 2016 +0200
2.2 +++ b/src/HOL/Finite_Set.thy	Sat Jul 02 08:41:05 2016 +0200
2.3 @@ -1250,6 +1250,10 @@
2.4    "card A = 0 \<longleftrightarrow> A = {} \<or> \<not> finite A"
2.5    by auto
2.6
2.7 +lemma card_range_greater_zero:
2.8 +  "finite (range f) \<Longrightarrow> card (range f) > 0"
2.9 +  by (rule ccontr) (simp add: card_eq_0_iff)
2.10 +
2.11  lemma card_gt_0_iff:
2.12    "0 < card A \<longleftrightarrow> A \<noteq> {} \<and> finite A"
2.13    by (simp add: neq0_conv [symmetric] card_eq_0_iff)
```
```     3.1 --- a/src/HOL/Fun.thy	Sat Jul 02 08:41:05 2016 +0200
3.2 +++ b/src/HOL/Fun.thy	Sat Jul 02 08:41:05 2016 +0200
3.3 @@ -213,6 +213,20 @@
3.4  lemma inj_onD: "inj_on f A \<Longrightarrow> f x = f y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y"
3.5    unfolding inj_on_def by blast
3.6
3.7 +lemma inj_on_subset:
3.8 +  assumes "inj_on f A"
3.9 +  assumes "B \<subseteq> A"
3.10 +  shows "inj_on f B"
3.11 +proof (rule inj_onI)
3.12 +  fix a b
3.13 +  assume "a \<in> B" and "b \<in> B"
3.14 +  with assms have "a \<in> A" and "b \<in> A"
3.15 +    by auto
3.16 +  moreover assume "f a = f b"
3.17 +  ultimately show "a = b" using assms
3.18 +    by (auto dest: inj_onD)
3.19 +qed
3.20 +
3.21  lemma comp_inj_on: "inj_on f A \<Longrightarrow> inj_on g (f ` A) \<Longrightarrow> inj_on (g \<circ> f) A"
3.22    by (simp add: comp_def inj_on_def)
3.23
```
```     4.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Jul 02 08:41:05 2016 +0200
4.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Jul 02 08:41:05 2016 +0200
4.3 @@ -129,8 +129,13 @@
4.4  apply (fast intro: someI2)
4.5  done
4.6
4.7 -lemma inv_id [simp]: "inv id = id"
4.8 -by (simp add: inv_into_def id_def)
4.9 +lemma inv_identity [simp]:
4.10 +  "inv (\<lambda>a. a) = (\<lambda>a. a)"
4.11 +  by (simp add: inv_def)
4.12 +
4.13 +lemma inv_id [simp]:
4.14 +  "inv id = id"
4.15 +  by (simp add: id_def)
4.16
4.17  lemma inv_into_f_f [simp]:
4.18    "[| inj_on f A;  x : A |] ==> inv_into A f (f x) = x"
```
```     5.1 --- a/src/HOL/List.thy	Sat Jul 02 08:41:05 2016 +0200
5.2 +++ b/src/HOL/List.thy	Sat Jul 02 08:41:05 2016 +0200
5.3 @@ -3933,6 +3933,14 @@
5.4    map f (removeAll x xs) = removeAll (f x) (map f xs)"
5.5  by (rule map_removeAll_inj_on, erule subset_inj_on, rule subset_UNIV)
5.6
5.7 +lemma length_removeAll_less_eq [simp]:
5.8 +  "length (removeAll x xs) \<le> length xs"
5.9 +  by (simp add: removeAll_filter_not_eq)
5.10 +
5.11 +lemma length_removeAll_less [termination_simp]:
5.12 +  "x \<in> set xs \<Longrightarrow> length (removeAll x xs) < length xs"
5.13 +  by (auto dest: length_filter_less simp add: removeAll_filter_not_eq)
5.14 +
5.15
5.16  subsubsection \<open>@{const replicate}\<close>
5.17
```
```     6.1 --- a/src/HOL/MacLaurin.thy	Sat Jul 02 08:41:05 2016 +0200
6.2 +++ b/src/HOL/MacLaurin.thy	Sat Jul 02 08:41:05 2016 +0200
6.3 @@ -50,7 +50,8 @@
6.4      unfolding atLeast0LessThan[symmetric] by auto
6.5    have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) =
6.6        (\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)))"
6.7 -    unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
6.8 +    unfolding intvl
6.9 +    by (subst setsum.insert) (auto simp add: setsum.reindex)
6.10    moreover
6.11    have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
6.12      by (metis add_pos_pos fact_gt_zero less_add_same_cancel1 less_add_same_cancel2 less_numeral_extra(3) mult_less_0_iff of_nat_less_0_iff)
```
```     7.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Jul 02 08:41:05 2016 +0200
7.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Jul 02 08:41:05 2016 +0200
7.3 @@ -46,23 +46,11 @@
7.4    apply (metis member_remove remove_def)
7.5    done
7.6
7.7 -lemma swap_apply1: "Fun.swap x y f x = f y"
7.8 -  by (simp add: Fun.swap_def)
7.9 -
7.10 -lemma swap_apply2: "Fun.swap x y f y = f x"
7.11 -  by (simp add: Fun.swap_def)
7.12 -
7.13 -lemma lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
7.14 -  by auto
7.15 -
7.16 -lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
7.17 -  by auto
7.18 -
7.19 -lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
7.20 -  apply auto
7.21 -  apply (case_tac x)
7.22 -  apply auto
7.23 -  done
7.24 +lemmas swap_apply1 = swap_apply(1)
7.25 +lemmas swap_apply2 = swap_apply(2)
7.26 +lemmas lessThan_empty_iff = Iio_eq_empty_iff_nat
7.27 +lemmas Zero_notin_Suc = zero_notin_Suc_image
7.28 +lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0
7.29
7.30  lemma setsum_union_disjoint':
7.31    assumes "finite A"
```
```     8.1 --- a/src/HOL/Series.thy	Sat Jul 02 08:41:05 2016 +0200
8.2 +++ b/src/HOL/Series.thy	Sat Jul 02 08:41:05 2016 +0200
8.3 @@ -283,9 +283,6 @@
8.4
8.5  subsection \<open>Infinite summability on topological monoids\<close>
8.6
8.7 -lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
8.8 -  by auto
8.9 -
8.10  context
8.11    fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
8.12  begin
8.13 @@ -296,7 +293,8 @@
8.14    have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0"
8.15      using assms by (auto intro!: tendsto_add simp: sums_def)
8.16    moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
8.17 -    unfolding lessThan_Suc_eq_insert_0 by (simp add: Zero_notin_Suc ac_simps setsum.reindex)
8.18 +    unfolding lessThan_Suc_eq_insert_0
8.19 +      by (simp add: ac_simps setsum_atLeast1_atMost_eq image_Suc_lessThan)
8.20    ultimately show ?thesis
8.21      by (auto simp add: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
8.22  qed
8.23 @@ -338,7 +336,7 @@
8.24    have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
8.25      by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
8.26    also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
8.27 -    by (simp add: ac_simps setsum.reindex image_iff lessThan_Suc_eq_insert_0)
8.28 +    by (simp add: ac_simps lessThan_Suc_eq_insert_0 image_Suc_lessThan setsum_atLeast1_atMost_eq)
8.29    also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s"
8.30    proof
8.31      assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
```
```     9.1 --- a/src/HOL/Set.thy	Sat Jul 02 08:41:05 2016 +0200
9.2 +++ b/src/HOL/Set.thy	Sat Jul 02 08:41:05 2016 +0200
9.3 @@ -83,6 +83,11 @@
9.4  lemma set_eq_iff: "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
9.5    by (auto intro:set_eqI)
9.6
9.7 +lemma Collect_eqI:
9.8 +  assumes "\<And>x. P x = Q x"
9.9 +  shows "Collect P = Collect Q"
9.10 +  using assms by (auto intro: set_eqI)
9.11 +
9.12  text \<open>Lifting of predicate class instances\<close>
9.13
9.14  instantiation set :: (type) boolean_algebra
9.15 @@ -973,6 +978,11 @@
9.16  lemma range_composition: "range (\<lambda>x. f (g x)) = f ` range g"
9.17    by auto
9.18
9.19 +lemma range_eq_singletonD:
9.20 +  assumes "range f = {a}"
9.21 +  shows "f x = a"
9.22 +  using assms by auto
9.23 +
9.24
9.25  subsubsection \<open>Some rules with \<open>if\<close>\<close>
9.26
9.27 @@ -1860,6 +1870,24 @@
9.28  lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
9.29    by blast
9.30
9.31 +lemma in_image_insert_iff:
9.32 +  assumes "\<And>C. C \<in> B \<Longrightarrow> x \<notin> C"
9.33 +  shows "A \<in> insert x ` B \<longleftrightarrow> x \<in> A \<and> A - {x} \<in> B" (is "?P \<longleftrightarrow> ?Q")
9.34 +proof
9.35 +  assume ?P then show ?Q
9.36 +    using assms by auto
9.37 +next
9.38 +  assume ?Q
9.39 +  then have "x \<in> A" and "A - {x} \<in> B"
9.40 +    by simp_all
9.41 +  from \<open>A - {x} \<in> B\<close> have "insert x (A - {x}) \<in> insert x ` B"
9.42 +    by (rule imageI)
9.43 +  also from \<open>x \<in> A\<close>
9.44 +  have "insert x (A - {x}) = A"
9.45 +    by auto
9.46 +  finally show ?P .
9.47 +qed
9.48 +
9.49  hide_const (open) member not_member
9.50
9.51  lemmas equalityI = subset_antisym
9.52 @@ -1920,4 +1948,3 @@
9.53  \<close>
9.54
9.55  end
9.56 -
```
```    10.1 --- a/src/HOL/Set_Interval.thy	Sat Jul 02 08:41:05 2016 +0200
10.2 +++ b/src/HOL/Set_Interval.thy	Sat Jul 02 08:41:05 2016 +0200
10.3 @@ -14,7 +14,7 @@
10.4  section \<open>Set intervals\<close>
10.5
10.6  theory Set_Interval
10.7 -imports Lattices_Big Nat_Transfer
10.8 +imports Lattices_Big Divides Nat_Transfer
10.9  begin
10.10
10.11  context ord
10.12 @@ -901,6 +901,16 @@
10.13    qed
10.14  qed
10.15
10.16 +corollary image_Suc_lessThan:
10.17 +  "Suc ` {..<n} = {1..n}"
10.18 +  using image_add_atLeastLessThan [of 1 0 n]
10.19 +  by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
10.20 +
10.21 +corollary image_Suc_atMost:
10.22 +  "Suc ` {..n} = {1..Suc n}"
10.23 +  using image_add_atLeastLessThan [of 1 0 "Suc n"]
10.24 +  by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
10.25 +
10.26  corollary image_Suc_atLeastAtMost[simp]:
10.27    "Suc ` {i..j} = {Suc i..Suc j}"
10.28  using image_add_atLeastAtMost[where k="Suc 0"] by simp
10.29 @@ -909,6 +919,14 @@
10.30    "Suc ` {i..<j} = {Suc i..<Suc j}"
10.31  using image_add_atLeastLessThan[where k="Suc 0"] by simp
10.32
10.33 +lemma atLeast1_lessThan_eq_remove0:
10.34 +  "{Suc 0..<n} = {..<n} - {0}"
10.35 +  by auto
10.36 +
10.37 +lemma atLeast1_atMost_eq_remove0:
10.38 +  "{Suc 0..n} = {..n} - {0}"
10.39 +  by auto
10.40 +
10.42      "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
10.43    apply (auto simp add: image_def)
10.44 @@ -1146,6 +1164,12 @@
10.45  lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
10.46    by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
10.47
10.48 +lemma subset_eq_range_finite:
10.49 +  fixes n :: nat
10.50 +  assumes "N \<subseteq> {..<n}"
10.51 +  shows "finite N"
10.52 +  using assms finite_lessThan by (rule finite_subset)
10.53 +
10.54  lemma ex_bij_betw_nat_finite:
10.55    "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
10.56  apply(drule finite_imp_nat_seg_image_inj_on)
10.57 @@ -1156,6 +1180,18 @@
10.58    "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
10.59  by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
10.60
10.61 +lemma bij_betw_nat_finite:
10.62 +  assumes "finite A"
10.63 +  obtains f where "bij_betw f {..<card A} A"
10.64 +proof -
10.65 +  from assms obtain f where "bij_betw f {0..<card A} A"
10.66 +    by (blast dest: ex_bij_betw_nat_finite)
10.67 +  also have "{0..<card A} = {..<card A}"
10.68 +    by auto
10.69 +  finally show thesis using that
10.70 +    by blast
10.71 +qed
10.72 +
10.73  lemma finite_same_card_bij:
10.74    "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
10.75  apply(drule ex_bij_betw_finite_nat)
10.76 @@ -1200,6 +1236,17 @@
10.77    ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
10.78  qed (insert assms, auto)
10.79
10.80 +lemma subset_eq_range_card:
10.81 +  fixes n :: nat
10.82 +  assumes "N \<subseteq> {..<n}"
10.83 +  shows "card N \<le> n"
10.84 +proof -
10.85 +  from assms finite_lessThan have "card N \<le> card {..<n}"
10.86 +    using card_mono by blast
10.87 +  then show ?thesis by simp
10.88 +qed
10.89 +
10.90 +
10.91  subsection \<open>Intervals of integers\<close>
10.92
10.93  lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
10.94 @@ -1665,11 +1712,15 @@
10.95       "(\<Sum>i\<le>n. (\<Sum>j<i. a i j)) = (\<Sum>j<n. \<Sum>i = Suc j..n. a i j)"
10.96    by (induction n) (auto simp: setsum.distrib)
10.97
10.98 -lemma setsum_zero_power' [simp]:
10.99 -  fixes c :: "nat \<Rightarrow> 'a::field"
10.100 -  shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
10.101 -  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
10.102 -  by auto
10.103 +lemma setsum_atLeast1_atMost_eq:
10.104 +  "setsum f {Suc 0..n} = (\<Sum>k<n. f (Suc k))"
10.105 +proof -
10.106 +  have "setsum f {Suc 0..n} = setsum f (Suc ` {..<n})"
10.107 +    by (simp add: image_Suc_lessThan)
10.108 +  also have "\<dots> = (\<Sum>k<n. f (Suc k))"
10.109 +    by (simp add: setsum.reindex)
10.110 +  finally show ?thesis .
10.111 +qed
10.112
10.113
10.114  subsection \<open>Telescoping\<close>
10.115 @@ -1923,6 +1974,29 @@
10.116  qed
10.117
10.118
10.119 +subsection \<open>Division remainder\<close>
10.120 +
10.121 +lemma range_mod:
10.122 +  fixes n :: nat
10.123 +  assumes "n > 0"
10.124 +  shows "range (\<lambda>m. m mod n) = {0..<n}" (is "?A = ?B")
10.125 +proof (rule set_eqI)
10.126 +  fix m
10.127 +  show "m \<in> ?A \<longleftrightarrow> m \<in> ?B"
10.128 +  proof
10.129 +    assume "m \<in> ?A"
10.130 +    with assms show "m \<in> ?B"
10.131 +      by auto
10.132 +  next
10.133 +    assume "m \<in> ?B"
10.134 +    moreover have "m mod n \<in> ?A"
10.135 +      by (rule rangeI)
10.136 +    ultimately show "m \<in> ?A"
10.137 +      by simp
10.138 +  qed
10.139 +qed
10.140 +
10.141 +
10.142  subsection \<open>Efficient folding over intervals\<close>
10.143
10.144  function fold_atLeastAtMost_nat where
```
```    11.1 --- a/src/HOL/Transcendental.thy	Sat Jul 02 08:41:05 2016 +0200
11.2 +++ b/src/HOL/Transcendental.thy	Sat Jul 02 08:41:05 2016 +0200
11.3 @@ -272,7 +272,8 @@
11.4      have "?s sums y" using sums_if'[OF \<open>f sums y\<close>] .
11.5      from this[unfolded sums_def, THEN LIMSEQ_Suc]
11.6      have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
11.7 -      by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum.reindex if_eq sums_def cong del: if_cong)
11.8 +      by (simp add: lessThan_Suc_eq_insert_0 setsum_atLeast1_atMost_eq image_Suc_lessThan
11.9 +        if_eq sums_def cong del: if_cong)
11.10    }
11.11    from sums_add[OF g_sums this] show ?thesis unfolding if_sum .
11.12  qed
```