more theorems
authorhaftmann
Sat Jul 02 08:41:05 2016 +0200 (2016-07-02)
changeset 633655340fb6633d0
parent 63364 4fa441c2f20c
child 63366 209c4cbbc4cd
more theorems
src/HOL/Complete_Lattices.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Hilbert_Choice.thy
src/HOL/List.thy
src/HOL/MacLaurin.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Series.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
src/HOL/Transcendental.thy
     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.41  lemma image_add_int_atLeastLessThan:
   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