new material about summations and powers, along with some tweaks
authorpaulson <lp15@cam.ac.uk>
Mon Jan 21 14:44:23 2019 +0000 (5 months ago)
changeset 697007a92cbec7030
parent 69699 82f57315cade
child 69705 c9ea1e9916fb
child 69710 61372780515b
new material about summations and powers, along with some tweaks
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Weak_Morphisms.thy
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Embed_Measure.thy
src/HOL/Fun.thy
src/HOL/Groups_Big.thy
src/HOL/Int.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Finite_Map.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Nonstandard_Analysis/StarDef.thy
src/HOL/Power.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Sun Jan 20 17:15:49 2019 +0000
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Mon Jan 21 14:44:23 2019 +0000
     1.3 @@ -1991,7 +1991,7 @@
     1.4  definition somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.5    where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"
     1.6  
     1.7 -definition "SomeGcd G A = inf (division_rel G) A"
     1.8 +definition "SomeGcd G A = Lattice.inf (division_rel G) A"
     1.9  
    1.10  
    1.11  locale gcd_condition_monoid = comm_monoid_cancel +
     2.1 --- a/src/HOL/Algebra/Group.thy	Sun Jan 20 17:15:49 2019 +0000
     2.2 +++ b/src/HOL/Algebra/Group.thy	Mon Jan 21 14:44:23 2019 +0000
     2.3 @@ -781,18 +781,13 @@
     2.4      {h. h \<in> carrier G \<rightarrow> carrier H \<and>
     2.5        (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
     2.6  
     2.7 -
     2.8 -(* NEW ========================================================================== *)
     2.9 -lemma hom_trans:
    2.10 +lemma hom_compose:
    2.11    "\<lbrakk> f \<in> hom G H; g \<in> hom H I \<rbrakk> \<Longrightarrow> g \<circ> f \<in> hom G I"
    2.12    unfolding hom_def by (auto simp add: Pi_iff)
    2.13 -(* ============================================================================== *)
    2.14  
    2.15 -(* NEW ============================================================================ *)
    2.16  lemma (in group) hom_restrict:
    2.17    assumes "h \<in> hom G H" and "\<And>g. g \<in> carrier G \<Longrightarrow> h g = t g" shows "t \<in> hom G H"
    2.18    using assms unfolding hom_def by (auto simp add: Pi_iff)
    2.19 -(* ============================================================================== *)
    2.20  
    2.21  lemma (in group) hom_compose:
    2.22    "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
     3.1 --- a/src/HOL/Algebra/Lattice.thy	Sun Jan 20 17:15:49 2019 +0000
     3.2 +++ b/src/HOL/Algebra/Lattice.thy	Mon Jan 21 14:44:23 2019 +0000
     3.3 @@ -783,4 +783,7 @@
     3.4  
     3.5  end
     3.6  
     3.7 +hide_const (open) Lattice.inf
     3.8 +hide_const (open) Lattice.sup
     3.9 +
    3.10  end
     4.1 --- a/src/HOL/Algebra/Weak_Morphisms.thy	Sun Jan 20 17:15:49 2019 +0000
     4.2 +++ b/src/HOL/Algebra/Weak_Morphisms.thy	Mon Jan 21 14:44:23 2019 +0000
     4.3 @@ -220,7 +220,8 @@
     4.4    have the_elem_hom: "(\<lambda>x. the_elem (f ` x)) \<in> hom (G Mod H) (image_group f G)"
     4.5      using weak_group_morphism_is_iso[OF assms] by (simp add: iso_def)
     4.6    have hom: "(\<lambda>x. the_elem (f ` x)) \<circ> (#>) H \<in> hom G (image_group f G)"
     4.7 -    using hom_trans[OF H.r_coset_hom_Mod the_elem_hom] by simp
     4.8 +    using hom_compose[OF H.r_coset_hom_Mod the_elem_hom]
     4.9 +    using Group.hom_compose H.r_coset_hom_Mod the_elem_hom by blast
    4.10    have restrict: "\<And>a. a \<in> carrier G \<Longrightarrow> ((\<lambda>x. the_elem (f ` x)) \<circ> (#>) H) a = f a"
    4.11      using weak_group_morphism_range[OF assms] by auto
    4.12    show ?thesis
     5.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Sun Jan 20 17:15:49 2019 +0000
     5.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Mon Jan 21 14:44:23 2019 +0000
     5.3 @@ -2127,8 +2127,10 @@
     5.4    proof -
     5.5      have "r0 n \<ge> n" using \<open>strict_mono r0\<close> by (simp add: seq_suble)
     5.6      have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF \<open>r0 n \<ge> n\<close>], auto)
     5.7 -    then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
     5.8 -    then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
     5.9 +    then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" 
    5.10 +      using r0(2) less_le_trans by blast
    5.11 +    then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" 
    5.12 +      unfolding r_def by auto
    5.13      moreover have "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) = (\<integral>x. norm(u (r n) x) \<partial>M)"
    5.14        by (rule nn_integral_eq_integral, auto simp add: integrable_norm[OF assms(1)[of "r n"]])
    5.15      ultimately show ?thesis by (auto intro: ennreal_lessI)
     6.1 --- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Jan 20 17:15:49 2019 +0000
     6.2 +++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Jan 21 14:44:23 2019 +0000
     6.3 @@ -1770,7 +1770,6 @@
     6.4  
     6.5  lemmas swap_apply1 = swap_apply(1)
     6.6  lemmas swap_apply2 = swap_apply(2)
     6.7 -lemmas Zero_notin_Suc = zero_notin_Suc_image
     6.8  
     6.9  lemma pointwise_minimal_pointwise_maximal:
    6.10    fixes s :: "(nat \<Rightarrow> nat) set"
    6.11 @@ -2273,7 +2272,7 @@
    6.12      then have "a = enum 0"
    6.13        using \<open>a \<in> s\<close> na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
    6.14      then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
    6.15 -      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident Zero_notin_Suc in_enum_image subset_eq)
    6.16 +      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident zero_notin_Suc_image in_enum_image subset_eq)
    6.17      then have "enum 1 \<in> s - {a}"
    6.18        by auto
    6.19      then have "upd 0 = n"
     7.1 --- a/src/HOL/Analysis/Embed_Measure.thy	Sun Jan 20 17:15:49 2019 +0000
     7.2 +++ b/src/HOL/Analysis/Embed_Measure.thy	Mon Jan 21 14:44:23 2019 +0000
     7.3 @@ -149,7 +149,7 @@
     7.4    assumes [simp]: "inj f" "inj g"
     7.5    shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"
     7.6  proof-
     7.7 -  have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp)
     7.8 +  have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_compose)
     7.9    note measurable_embed_measure2[measurable]
    7.10    have "embed_measure (embed_measure M f) g =
    7.11              distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"
    7.12 @@ -158,7 +158,7 @@
    7.13    also have "... = embed_measure M (g \<circ> f)"
    7.14        by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)
    7.15           (auto simp: sets_embed_measure o_def image_image[symmetric]
    7.16 -               intro: inj_comp cong: distr_cong)
    7.17 +               intro: inj_compose cong: distr_cong)
    7.18    finally show ?thesis .
    7.19  qed
    7.20  
     8.1 --- a/src/HOL/Fun.thy	Sun Jan 20 17:15:49 2019 +0000
     8.2 +++ b/src/HOL/Fun.thy	Mon Jan 21 14:44:23 2019 +0000
     8.3 @@ -181,7 +181,7 @@
     8.4  lemma inj_on_strict_subset: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
     8.5    unfolding inj_on_def by blast
     8.6  
     8.7 -lemma inj_comp: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
     8.8 +lemma inj_compose: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
     8.9    by (simp add: inj_def)
    8.10  
    8.11  lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
     9.1 --- a/src/HOL/Groups_Big.thy	Sun Jan 20 17:15:49 2019 +0000
     9.2 +++ b/src/HOL/Groups_Big.thy	Mon Jan 21 14:44:23 2019 +0000
     9.3 @@ -503,6 +503,26 @@
     9.4    shows "F g A = F h B"
     9.5    using assms same_carrier [of C A B] by simp
     9.6  
     9.7 +lemma eq_general:
     9.8 +  assumes B: "\<And>y. y \<in> B \<Longrightarrow> \<exists>!x. x \<in> A \<and> h x = y" and A: "\<And>x. x \<in> A \<Longrightarrow> h x \<in> B \<and> \<gamma>(h x) = \<phi> x"
     9.9 +  shows "F \<phi> A = F \<gamma> B"
    9.10 +proof -
    9.11 +  have eq: "B = h ` A"
    9.12 +    by (auto dest: assms)
    9.13 +  have h: "inj_on h A"
    9.14 +    using assms by (blast intro: inj_onI)
    9.15 +  have "F \<phi> A = F (\<gamma> \<circ> h) A"
    9.16 +    using A by auto
    9.17 +  also have "\<dots> = F \<gamma> B"
    9.18 +    by (simp add: eq reindex h)
    9.19 +  finally show ?thesis .
    9.20 +qed
    9.21 +
    9.22 +lemma eq_general_inverses:
    9.23 +  assumes B: "\<And>y. y \<in> B \<Longrightarrow> k y \<in> A \<and> h(k y) = y" and A: "\<And>x. x \<in> A \<Longrightarrow> h x \<in> B \<and> k(h x) = x \<and> \<gamma>(h x) = \<phi> x"
    9.24 +  shows "F \<phi> A = F \<gamma> B"
    9.25 +  by (rule eq_general [where h=h]) (force intro: dest: A B)+
    9.26 +
    9.27  end
    9.28  
    9.29  
    10.1 --- a/src/HOL/Int.thy	Sun Jan 20 17:15:49 2019 +0000
    10.2 +++ b/src/HOL/Int.thy	Mon Jan 21 14:44:23 2019 +0000
    10.3 @@ -1441,7 +1441,7 @@
    10.4     apply auto
    10.5    done
    10.6  
    10.7 -lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
    10.8 +lemma infinite_UNIV_int [simp]: "\<not> finite (UNIV::int set)"
    10.9  proof
   10.10    assume "finite (UNIV::int set)"
   10.11    moreover have "inj (\<lambda>i::int. 2 * i)"
    11.1 --- a/src/HOL/Library/FSet.thy	Sun Jan 20 17:15:49 2019 +0000
    11.2 +++ b/src/HOL/Library/FSet.thy	Mon Jan 21 14:44:23 2019 +0000
    11.3 @@ -1302,7 +1302,7 @@
    11.4    moreover have "inj (inv fset_of_list)"
    11.5      using fset_of_list_surj by (rule surj_imp_inj_inv)
    11.6    ultimately have "inj (to_nat \<circ> inv fset_of_list)"
    11.7 -    by (rule inj_comp)
    11.8 +    by (rule inj_compose)
    11.9    thus "\<exists>to_nat::'a fset \<Rightarrow> nat. inj to_nat"
   11.10      by auto
   11.11  qed
    12.1 --- a/src/HOL/Library/Finite_Map.thy	Sun Jan 20 17:15:49 2019 +0000
    12.2 +++ b/src/HOL/Library/Finite_Map.thy	Mon Jan 21 14:44:23 2019 +0000
    12.3 @@ -1406,7 +1406,7 @@
    12.4    moreover have "inj (inv fmap_of_list)"
    12.5      using fmap_of_list_surj by (rule surj_imp_inj_inv)
    12.6    ultimately have "inj (to_nat \<circ> inv fmap_of_list)"
    12.7 -    by (rule inj_comp)
    12.8 +    by (rule inj_compose)
    12.9    thus "\<exists>to_nat::('a, 'b) fmap \<Rightarrow> nat. inj to_nat"
   12.10      by auto
   12.11  qed
    13.1 --- a/src/HOL/List.thy	Sun Jan 20 17:15:49 2019 +0000
    13.2 +++ b/src/HOL/List.thy	Mon Jan 21 14:44:23 2019 +0000
    13.3 @@ -1517,7 +1517,7 @@
    13.4      also have "\<dots> = Suc(card(Suc ` ?S))" using fin
    13.5        by (simp add: card_image)
    13.6      also have "\<dots> = card ?S'" using eq fin
    13.7 -      by (simp add:card_insert_if) (simp add:image_def)
    13.8 +      by (simp add:card_insert_if) 
    13.9      finally show ?thesis .
   13.10    next
   13.11      assume "\<not> p x"
    14.1 --- a/src/HOL/Nat.thy	Sun Jan 20 17:15:49 2019 +0000
    14.2 +++ b/src/HOL/Nat.thy	Mon Jan 21 14:44:23 2019 +0000
    14.3 @@ -1515,7 +1515,7 @@
    14.4    assumes "inj f"
    14.5    shows "inj (f^^n)"
    14.6  proof (induction n)
    14.7 -  case Suc thus ?case using inj_comp[OF assms Suc.IH] by (simp del: comp_apply)
    14.8 +  case Suc thus ?case using inj_compose[OF assms Suc.IH] by (simp del: comp_apply)
    14.9  qed simp
   14.10  
   14.11  lemma surj_fn[simp]:
    15.1 --- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Jan 20 17:15:49 2019 +0000
    15.2 +++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Jan 21 14:44:23 2019 +0000
    15.3 @@ -914,7 +914,7 @@
    15.4    have "inj (star_of :: 'a \<Rightarrow> 'a star)"
    15.5      by (rule injI) simp
    15.6    then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)"
    15.7 -    using inj_of_nat by (rule inj_comp)
    15.8 +    using inj_of_nat by (rule inj_compose)
    15.9    then show "inj (of_nat :: nat \<Rightarrow> 'a star)"
   15.10      by (simp add: comp_def)
   15.11  qed
    16.1 --- a/src/HOL/Power.thy	Sun Jan 20 17:15:49 2019 +0000
    16.2 +++ b/src/HOL/Power.thy	Mon Jan 21 14:44:23 2019 +0000
    16.3 @@ -501,6 +501,14 @@
    16.4      done
    16.5  qed
    16.6  
    16.7 +lemma power_decreasing_iff [simp]: "\<lbrakk>0 < b; b < 1\<rbrakk> \<Longrightarrow> b ^ m \<le> b ^ n \<longleftrightarrow> n \<le> m"
    16.8 +  using power_strict_decreasing [of m n b]
    16.9 +  by (auto intro: power_decreasing ccontr)
   16.10 +
   16.11 +lemma power_strict_decreasing_iff [simp]: "\<lbrakk>0 < b; b < 1\<rbrakk> \<Longrightarrow> b ^ m < b ^ n \<longleftrightarrow> n < m"
   16.12 +  using power_decreasing_iff [of b m n] unfolding le_less
   16.13 +  by (auto dest: power_strict_decreasing le_neq_implies_less)
   16.14 +
   16.15  lemma power_Suc_less_one: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
   16.16    using power_strict_decreasing [of 0 "Suc n" a] by simp
   16.17  
    17.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Jan 20 17:15:49 2019 +0000
    17.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jan 21 14:44:23 2019 +0000
    17.3 @@ -322,7 +322,7 @@
    17.4  instance real_algebra_1 < ring_char_0
    17.5  proof
    17.6    from inj_of_real inj_of_nat have "inj (of_real \<circ> of_nat)"
    17.7 -    by (rule inj_comp)
    17.8 +    by (rule inj_compose)
    17.9    then show "inj (of_nat :: nat \<Rightarrow> 'a)"
   17.10      by (simp add: comp_def)
   17.11  qed
    18.1 --- a/src/HOL/Set.thy	Sun Jan 20 17:15:49 2019 +0000
    18.2 +++ b/src/HOL/Set.thy	Mon Jan 21 14:44:23 2019 +0000
    18.3 @@ -1857,6 +1857,9 @@
    18.4  definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
    18.5    where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
    18.6  
    18.7 +lemma pairwise_trivial [simp]: "pairwise (\<lambda>i j. j \<noteq> i) I"
    18.8 +  by (auto simp: pairwise_def)
    18.9 +
   18.10  lemma pairwiseI [intro?]:
   18.11    "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y"
   18.12    using that by (simp add: pairwise_def)
    19.1 --- a/src/HOL/Set_Interval.thy	Sun Jan 20 17:15:49 2019 +0000
    19.2 +++ b/src/HOL/Set_Interval.thy	Mon Jan 21 14:44:23 2019 +0000
    19.3 @@ -683,7 +683,7 @@
    19.4  new elements get indices at the beginning. So it is used to transform
    19.5  \<^term>\<open>{..<Suc n}\<close> to \<^term>\<open>0::nat\<close> and \<^term>\<open>{..< n}\<close>.\<close>
    19.6  
    19.7 -lemma zero_notin_Suc_image: "0 \<notin> Suc ` A"
    19.8 +lemma zero_notin_Suc_image [simp]: "0 \<notin> Suc ` A"
    19.9    by auto
   19.10  
   19.11  lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})"