--- 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 {})"
by (auto simp add: set_eq_iff)
-
+
+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"
by (simp add: comp_def inj_on_def)
--- 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"
-by (simp add: inv_into_def id_def)
+lemma inv_identity [simp]:
+ "inv (\<lambda>a. a) = (\<lambda>a. a)"
+ by (simp add: inv_def)
+
+lemma inv_id [simp]:
+ "inv id = id"
+ by (simp add: id_def)
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"
+ by (simp add: removeAll_filter_not_eq)
+
+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"
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)
--- 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"
- by (simp add: Fun.swap_def)
-
-lemma swap_apply2: "Fun.swap x y f y = f x"
- by (simp add: Fun.swap_def)
-
-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
+
lemma image_add_int_atLeastLessThan:
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
apply (auto simp add: image_def)
@@ -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})"
+ by (simp add: image_Suc_lessThan)
+ also have "\<dots> = (\<Sum>k<n. f (Suc k))"
+ by (simp add: setsum.reindex)
+ 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