author haftmann Sat, 02 Jul 2016 08:41:05 +0200 changeset 63365 5340fb6633d0 parent 63364 4fa441c2f20c child 63366 209c4cbbc4cd
more theorems
 src/HOL/Complete_Lattices.thy file | annotate | diff | comparison | revisions src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Fun.thy file | annotate | diff | comparison | revisions src/HOL/Hilbert_Choice.thy file | annotate | diff | comparison | revisions src/HOL/List.thy file | annotate | diff | comparison | revisions src/HOL/MacLaurin.thy file | annotate | diff | comparison | revisions src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy file | annotate | diff | comparison | revisions src/HOL/Series.thy file | annotate | diff | comparison | revisions src/HOL/Set.thy file | annotate | diff | comparison | revisions src/HOL/Set_Interval.thy file | annotate | diff | comparison | revisions src/HOL/Transcendental.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Complete_Lattices.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Complete_Lattices.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -1402,7 +1402,26 @@
lemma UNION_fun_upd:
"UNION J (A(i := B)) = UNION (J - {i}) A \<union> (if i \<in> J then B else {})"
-
+
+lemma bij_betw_Pow:
+  assumes "bij_betw f A B"
+  shows "bij_betw (image f) (Pow A) (Pow B)"
+proof -
+  from assms have "inj_on f A"
+    by (rule bij_betw_imp_inj_on)
+  then have "inj_on f (\<Union>Pow A)"
+    by simp
+  then have "inj_on (image f) (Pow A)"
+    by (rule inj_on_image)
+  then have "bij_betw (image f) (Pow A) (image f ` Pow A)"
+    by (rule inj_on_imp_bij_betw)
+  moreover from assms have "f ` A = B"
+    by (rule bij_betw_imp_surj_on)
+  then have "image f ` Pow A = Pow B"
+    by (rule image_Pow_surj)
+  ultimately show ?thesis by simp
+qed
+

subsubsection \<open>Complement\<close>
```
```--- a/src/HOL/Finite_Set.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -1250,6 +1250,10 @@
"card A = 0 \<longleftrightarrow> A = {} \<or> \<not> finite A"
by auto

+lemma card_range_greater_zero:
+  "finite (range f) \<Longrightarrow> card (range f) > 0"
+  by (rule ccontr) (simp add: card_eq_0_iff)
+
lemma card_gt_0_iff:
"0 < card A \<longleftrightarrow> A \<noteq> {} \<and> finite A"
by (simp add: neq0_conv [symmetric] card_eq_0_iff) ```
```--- a/src/HOL/Fun.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Fun.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -213,6 +213,20 @@
lemma inj_onD: "inj_on f A \<Longrightarrow> f x = f y \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x = y"
unfolding inj_on_def by blast

+lemma inj_on_subset:
+  assumes "inj_on f A"
+  assumes "B \<subseteq> A"
+  shows "inj_on f B"
+proof (rule inj_onI)
+  fix a b
+  assume "a \<in> B" and "b \<in> B"
+  with assms have "a \<in> A" and "b \<in> A"
+    by auto
+  moreover assume "f a = f b"
+  ultimately show "a = b" using assms
+    by (auto dest: inj_onD)
+qed
+
lemma comp_inj_on: "inj_on f A \<Longrightarrow> inj_on g (f ` A) \<Longrightarrow> inj_on (g \<circ> f) A"
```
```--- a/src/HOL/Hilbert_Choice.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -129,8 +129,13 @@
apply (fast intro: someI2)
done

-lemma inv_id [simp]: "inv id = id"
+lemma inv_identity [simp]:
+  "inv (\<lambda>a. a) = (\<lambda>a. a)"
+
+lemma inv_id [simp]:
+  "inv id = id"

lemma inv_into_f_f [simp]:
"[| inj_on f A;  x : A |] ==> inv_into A f (f x) = x"```
```--- a/src/HOL/List.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/List.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -3933,6 +3933,14 @@
map f (removeAll x xs) = removeAll (f x) (map f xs)"
by (rule map_removeAll_inj_on, erule subset_inj_on, rule subset_UNIV)

+lemma length_removeAll_less_eq [simp]:
+  "length (removeAll x xs) \<le> length xs"
+
+lemma length_removeAll_less [termination_simp]:
+  "x \<in> set xs \<Longrightarrow> length (removeAll x xs) < length xs"
+  by (auto dest: length_filter_less simp add: removeAll_filter_not_eq)
+

subsubsection \<open>@{const replicate}\<close>
```
```--- a/src/HOL/MacLaurin.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/MacLaurin.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -50,7 +50,8 @@
unfolding atLeast0LessThan[symmetric] by auto
have "(\<Sum>x<n - m. real x * t ^ (x - Suc 0) * diff (m + x) 0 / (fact x)) =
(\<Sum>x<n - Suc m. real (Suc x) * t ^ x * diff (Suc m + x) 0 / (fact (Suc x)))"
-    unfolding intvl atLeast0LessThan by (subst setsum.insert) (auto simp: setsum.reindex)
+    unfolding intvl
+    by (subst setsum.insert) (auto simp add: setsum.reindex)
moreover
have fact_neq_0: "\<And>x. (fact x) + real x * (fact x) \<noteq> 0"
```--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -46,23 +46,11 @@
apply (metis member_remove remove_def)
done

-lemma swap_apply1: "Fun.swap x y f x = f y"
-
-lemma swap_apply2: "Fun.swap x y f y = f x"
-
-lemma lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
-  by auto
-
-lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
-  by auto
-
-lemma atMost_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})"
-  apply auto
-  apply (case_tac x)
-  apply auto
-  done
+lemmas swap_apply1 = swap_apply(1)
+lemmas swap_apply2 = swap_apply(2)
+lemmas lessThan_empty_iff = Iio_eq_empty_iff_nat
+lemmas Zero_notin_Suc = zero_notin_Suc_image
+lemmas atMost_Suc_eq_insert_0 = Iic_Suc_eq_insert_0

lemma setsum_union_disjoint':
assumes "finite A"```
```--- a/src/HOL/Series.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Series.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -283,9 +283,6 @@

subsection \<open>Infinite summability on topological monoids\<close>

-lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
-  by auto
-
context
fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
begin
@@ -296,7 +293,8 @@
have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0"
using assms by (auto intro!: tendsto_add simp: sums_def)
moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
-    unfolding lessThan_Suc_eq_insert_0 by (simp add: Zero_notin_Suc ac_simps setsum.reindex)
+    unfolding lessThan_Suc_eq_insert_0
+      by (simp add: ac_simps setsum_atLeast1_atMost_eq image_Suc_lessThan)
ultimately show ?thesis
by (auto simp add: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
qed
@@ -338,7 +336,7 @@
have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
-    by (simp add: ac_simps setsum.reindex image_iff lessThan_Suc_eq_insert_0)
+    by (simp add: ac_simps lessThan_Suc_eq_insert_0 image_Suc_lessThan setsum_atLeast1_atMost_eq)
also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s"
proof
assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"```
```--- a/src/HOL/Set.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Set.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -83,6 +83,11 @@
lemma set_eq_iff: "A = B \<longleftrightarrow> (\<forall>x. x \<in> A \<longleftrightarrow> x \<in> B)"
by (auto intro:set_eqI)

+lemma Collect_eqI:
+  assumes "\<And>x. P x = Q x"
+  shows "Collect P = Collect Q"
+  using assms by (auto intro: set_eqI)
+
text \<open>Lifting of predicate class instances\<close>

instantiation set :: (type) boolean_algebra
@@ -973,6 +978,11 @@
lemma range_composition: "range (\<lambda>x. f (g x)) = f ` range g"
by auto

+lemma range_eq_singletonD:
+  assumes "range f = {a}"
+  shows "f x = a"
+  using assms by auto
+

subsubsection \<open>Some rules with \<open>if\<close>\<close>

@@ -1860,6 +1870,24 @@
lemma Int_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> False) \<Longrightarrow> A \<inter> B = {}"
by blast

+lemma in_image_insert_iff:
+  assumes "\<And>C. C \<in> B \<Longrightarrow> x \<notin> C"
+  shows "A \<in> insert x ` B \<longleftrightarrow> x \<in> A \<and> A - {x} \<in> B" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P then show ?Q
+    using assms by auto
+next
+  assume ?Q
+  then have "x \<in> A" and "A - {x} \<in> B"
+    by simp_all
+  from \<open>A - {x} \<in> B\<close> have "insert x (A - {x}) \<in> insert x ` B"
+    by (rule imageI)
+  also from \<open>x \<in> A\<close>
+  have "insert x (A - {x}) = A"
+    by auto
+  finally show ?P .
+qed
+
hide_const (open) member not_member

lemmas equalityI = subset_antisym
@@ -1920,4 +1948,3 @@
\<close>

end
-```
```--- a/src/HOL/Set_Interval.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -14,7 +14,7 @@
section \<open>Set intervals\<close>

theory Set_Interval
-imports Lattices_Big Nat_Transfer
+imports Lattices_Big Divides Nat_Transfer
begin

context ord
@@ -901,6 +901,16 @@
qed
qed

+corollary image_Suc_lessThan:
+  "Suc ` {..<n} = {1..n}"
+  using image_add_atLeastLessThan [of 1 0 n]
+  by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
+
+corollary image_Suc_atMost:
+  "Suc ` {..n} = {1..Suc n}"
+  using image_add_atLeastLessThan [of 1 0 "Suc n"]
+  by (auto simp add: lessThan_Suc_atMost atLeast0LessThan)
+
corollary image_Suc_atLeastAtMost[simp]:
"Suc ` {i..j} = {Suc i..Suc j}"
using image_add_atLeastAtMost[where k="Suc 0"] by simp
@@ -909,6 +919,14 @@
"Suc ` {i..<j} = {Suc i..<Suc j}"
using image_add_atLeastLessThan[where k="Suc 0"] by simp

+lemma atLeast1_lessThan_eq_remove0:
+  "{Suc 0..<n} = {..<n} - {0}"
+  by auto
+
+lemma atLeast1_atMost_eq_remove0:
+  "{Suc 0..n} = {..n} - {0}"
+  by auto
+
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
@@ -1146,6 +1164,12 @@
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)

+lemma subset_eq_range_finite:
+  fixes n :: nat
+  assumes "N \<subseteq> {..<n}"
+  shows "finite N"
+  using assms finite_lessThan by (rule finite_subset)
+
lemma ex_bij_betw_nat_finite:
"finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
apply(drule finite_imp_nat_seg_image_inj_on)
@@ -1156,6 +1180,18 @@
"finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)

+lemma bij_betw_nat_finite:
+  assumes "finite A"
+  obtains f where "bij_betw f {..<card A} A"
+proof -
+  from assms obtain f where "bij_betw f {0..<card A} A"
+    by (blast dest: ex_bij_betw_nat_finite)
+  also have "{0..<card A} = {..<card A}"
+    by auto
+  finally show thesis using that
+    by blast
+qed
+
lemma finite_same_card_bij:
"finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
apply(drule ex_bij_betw_finite_nat)
@@ -1200,6 +1236,17 @@
ultimately show "(\<exists>f. inj_on f A \<and> f ` A \<le> B)" by blast
qed (insert assms, auto)

+lemma subset_eq_range_card:
+  fixes n :: nat
+  assumes "N \<subseteq> {..<n}"
+  shows "card N \<le> n"
+proof -
+  from assms finite_lessThan have "card N \<le> card {..<n}"
+    using card_mono by blast
+  then show ?thesis by simp
+qed
+
+
subsection \<open>Intervals of integers\<close>

lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"
@@ -1665,11 +1712,15 @@
"(\<Sum>i\<le>n. (\<Sum>j<i. a i j)) = (\<Sum>j<n. \<Sum>i = Suc j..n. a i j)"
by (induction n) (auto simp: setsum.distrib)

-lemma setsum_zero_power' [simp]:
-  fixes c :: "nat \<Rightarrow> 'a::field"
-  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)"
-  using setsum_zero_power [of "\<lambda>i. c i / d i" A]
-  by auto
+lemma setsum_atLeast1_atMost_eq:
+  "setsum f {Suc 0..n} = (\<Sum>k<n. f (Suc k))"
+proof -
+  have "setsum f {Suc 0..n} = setsum f (Suc ` {..<n})"
+  also have "\<dots> = (\<Sum>k<n. f (Suc k))"
+  finally show ?thesis .
+qed

subsection \<open>Telescoping\<close>
@@ -1923,6 +1974,29 @@
qed

+subsection \<open>Division remainder\<close>
+
+lemma range_mod:
+  fixes n :: nat
+  assumes "n > 0"
+  shows "range (\<lambda>m. m mod n) = {0..<n}" (is "?A = ?B")
+proof (rule set_eqI)
+  fix m
+  show "m \<in> ?A \<longleftrightarrow> m \<in> ?B"
+  proof
+    assume "m \<in> ?A"
+    with assms show "m \<in> ?B"
+      by auto
+  next
+    assume "m \<in> ?B"
+    moreover have "m mod n \<in> ?A"
+      by (rule rangeI)
+    ultimately show "m \<in> ?A"
+      by simp
+  qed
+qed
+
+
subsection \<open>Efficient folding over intervals\<close>

function fold_atLeastAtMost_nat where```
```--- a/src/HOL/Transcendental.thy	Sat Jul 02 08:41:05 2016 +0200
+++ b/src/HOL/Transcendental.thy	Sat Jul 02 08:41:05 2016 +0200
@@ -272,7 +272,8 @@
have "?s sums y" using sums_if'[OF \<open>f sums y\<close>] .
from this[unfolded sums_def, THEN LIMSEQ_Suc]
have "(\<lambda> n. if even n then f (n div 2) else 0) sums y"
-      by (simp add: lessThan_Suc_eq_insert_0 image_iff setsum.reindex if_eq sums_def cong del: if_cong)
+      by (simp add: lessThan_Suc_eq_insert_0 setsum_atLeast1_atMost_eq image_Suc_lessThan
+        if_eq sums_def cong del: if_cong)
}
from sums_add[OF g_sums this] show ?thesis unfolding if_sum .
qed```