# HG changeset patch
# User haftmann
# Date 1467441665 -7200
# Node ID 5340fb6633d09dcd5a57b50f17638421be71c7f5
# Parent  4fa441c2f20cdc88c1a52f62288c0ab069eec8ef
more theorems

diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/Complete_Lattices.thy
--- 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>
 
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/Finite_Set.thy
--- 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) 
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/Fun.thy
--- 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)
 
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/Hilbert_Choice.thy
--- 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"
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/List.thy
--- 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>
 
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/MacLaurin.thy
--- 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)
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- 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"
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/Series.thy
--- 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"
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/Set.thy
--- 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
-
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/Set_Interval.thy
--- 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
diff -r 4fa441c2f20c -r 5340fb6633d0 src/HOL/Transcendental.thy
--- 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