# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1548081863 0
# Node ID 7a92cbec7030fba1fb9bd4c6df193c5dde216a83
# Parent  82f57315cadeabf25ef8f934d6c3ee7d9ae886b2
new material about summations and powers, along with some tweaks

diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -1991,7 +1991,7 @@
 definition somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
   where "somelcm G a b = (SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b)"
 
-definition "SomeGcd G A = inf (division_rel G) A"
+definition "SomeGcd G A = Lattice.inf (division_rel G) A"
 
 
 locale gcd_condition_monoid = comm_monoid_cancel +
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Algebra/Group.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -781,18 +781,13 @@
     {h. h \<in> carrier G \<rightarrow> carrier H \<and>
       (\<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)}"
 
-
-(* NEW ========================================================================== *)
-lemma hom_trans:
+lemma hom_compose:
   "\<lbrakk> f \<in> hom G H; g \<in> hom H I \<rbrakk> \<Longrightarrow> g \<circ> f \<in> hom G I"
   unfolding hom_def by (auto simp add: Pi_iff)
-(* ============================================================================== *)
 
-(* NEW ============================================================================ *)
 lemma (in group) hom_restrict:
   assumes "h \<in> hom G H" and "\<And>g. g \<in> carrier G \<Longrightarrow> h g = t g" shows "t \<in> hom G H"
   using assms unfolding hom_def by (auto simp add: Pi_iff)
-(* ============================================================================== *)
 
 lemma (in group) hom_compose:
   "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Algebra/Lattice.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -783,4 +783,7 @@
 
 end
 
+hide_const (open) Lattice.inf
+hide_const (open) Lattice.sup
+
 end
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Algebra/Weak_Morphisms.thy
--- a/src/HOL/Algebra/Weak_Morphisms.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Algebra/Weak_Morphisms.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -220,7 +220,8 @@
   have the_elem_hom: "(\<lambda>x. the_elem (f ` x)) \<in> hom (G Mod H) (image_group f G)"
     using weak_group_morphism_is_iso[OF assms] by (simp add: iso_def)
   have hom: "(\<lambda>x. the_elem (f ` x)) \<circ> (#>) H \<in> hom G (image_group f G)"
-    using hom_trans[OF H.r_coset_hom_Mod the_elem_hom] by simp
+    using hom_compose[OF H.r_coset_hom_Mod the_elem_hom]
+    using Group.hom_compose H.r_coset_hom_Mod the_elem_hom by blast
   have restrict: "\<And>a. a \<in> carrier G \<Longrightarrow> ((\<lambda>x. the_elem (f ` x)) \<circ> (#>) H) a = f a"
     using weak_group_morphism_range[OF assms] by auto
   show ?thesis
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -2127,8 +2127,10 @@
   proof -
     have "r0 n \<ge> n" using \<open>strict_mono r0\<close> by (simp add: seq_suble)
     have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF \<open>r0 n \<ge> n\<close>], auto)
-    then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
-    then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
+    then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" 
+      using r0(2) less_le_trans by blast
+    then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" 
+      unfolding r_def by auto
     moreover have "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) = (\<integral>x. norm(u (r n) x) \<partial>M)"
       by (rule nn_integral_eq_integral, auto simp add: integrable_norm[OF assms(1)[of "r n"]])
     ultimately show ?thesis by (auto intro: ennreal_lessI)
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -1770,7 +1770,6 @@
 
 lemmas swap_apply1 = swap_apply(1)
 lemmas swap_apply2 = swap_apply(2)
-lemmas Zero_notin_Suc = zero_notin_Suc_image
 
 lemma pointwise_minimal_pointwise_maximal:
   fixes s :: "(nat \<Rightarrow> nat) set"
@@ -2273,7 +2272,7 @@
     then have "a = enum 0"
       using \<open>a \<in> s\<close> na by (subst enum_0_bot) (auto simp: le_less intro!: less[of a _ n])
     then have s_eq: "s - {a} = enum ` Suc ` {.. n}"
-      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident Zero_notin_Suc in_enum_image subset_eq)
+      using s_eq by (simp add: atMost_Suc_eq_insert_0 insert_ident zero_notin_Suc_image in_enum_image subset_eq)
     then have "enum 1 \<in> s - {a}"
       by auto
     then have "upd 0 = n"
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Analysis/Embed_Measure.thy
--- a/src/HOL/Analysis/Embed_Measure.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Analysis/Embed_Measure.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -149,7 +149,7 @@
   assumes [simp]: "inj f" "inj g"
   shows "embed_measure (embed_measure M f) g = embed_measure M (g \<circ> f)"
 proof-
-  have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_comp)
+  have [simp]: "inj (\<lambda>x. g (f x))" by (subst o_def[symmetric]) (auto intro: inj_compose)
   note measurable_embed_measure2[measurable]
   have "embed_measure (embed_measure M f) g =
             distr M (embed_measure (embed_measure M f) g) (g \<circ> f)"
@@ -158,7 +158,7 @@
   also have "... = embed_measure M (g \<circ> f)"
       by (subst (3) embed_measure_eq_distr, simp add: o_def, rule distr_cong)
          (auto simp: sets_embed_measure o_def image_image[symmetric]
-               intro: inj_comp cong: distr_cong)
+               intro: inj_compose cong: distr_cong)
   finally show ?thesis .
 qed
 
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Fun.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -181,7 +181,7 @@
 lemma inj_on_strict_subset: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
   unfolding inj_on_def by blast
 
-lemma inj_comp: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
+lemma inj_compose: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
   by (simp add: inj_def)
 
 lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Groups_Big.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -503,6 +503,26 @@
   shows "F g A = F h B"
   using assms same_carrier [of C A B] by simp
 
+lemma eq_general:
+  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"
+  shows "F \<phi> A = F \<gamma> B"
+proof -
+  have eq: "B = h ` A"
+    by (auto dest: assms)
+  have h: "inj_on h A"
+    using assms by (blast intro: inj_onI)
+  have "F \<phi> A = F (\<gamma> \<circ> h) A"
+    using A by auto
+  also have "\<dots> = F \<gamma> B"
+    by (simp add: eq reindex h)
+  finally show ?thesis .
+qed
+
+lemma eq_general_inverses:
+  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"
+  shows "F \<phi> A = F \<gamma> B"
+  by (rule eq_general [where h=h]) (force intro: dest: A B)+
+
 end
 
 
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Int.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -1441,7 +1441,7 @@
    apply auto
   done
 
-lemma infinite_UNIV_int: "\<not> finite (UNIV::int set)"
+lemma infinite_UNIV_int [simp]: "\<not> finite (UNIV::int set)"
 proof
   assume "finite (UNIV::int set)"
   moreover have "inj (\<lambda>i::int. 2 * i)"
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Library/FSet.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -1302,7 +1302,7 @@
   moreover have "inj (inv fset_of_list)"
     using fset_of_list_surj by (rule surj_imp_inj_inv)
   ultimately have "inj (to_nat \<circ> inv fset_of_list)"
-    by (rule inj_comp)
+    by (rule inj_compose)
   thus "\<exists>to_nat::'a fset \<Rightarrow> nat. inj to_nat"
     by auto
 qed
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Library/Finite_Map.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -1406,7 +1406,7 @@
   moreover have "inj (inv fmap_of_list)"
     using fmap_of_list_surj by (rule surj_imp_inj_inv)
   ultimately have "inj (to_nat \<circ> inv fmap_of_list)"
-    by (rule inj_comp)
+    by (rule inj_compose)
   thus "\<exists>to_nat::('a, 'b) fmap \<Rightarrow> nat. inj to_nat"
     by auto
 qed
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/List.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -1517,7 +1517,7 @@
     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
       by (simp add: card_image)
     also have "\<dots> = card ?S'" using eq fin
-      by (simp add:card_insert_if) (simp add:image_def)
+      by (simp add:card_insert_if) 
     finally show ?thesis .
   next
     assume "\<not> p x"
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Nat.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -1515,7 +1515,7 @@
   assumes "inj f"
   shows "inj (f^^n)"
 proof (induction n)
-  case Suc thus ?case using inj_comp[OF assms Suc.IH] by (simp del: comp_apply)
+  case Suc thus ?case using inj_compose[OF assms Suc.IH] by (simp del: comp_apply)
 qed simp
 
 lemma surj_fn[simp]:
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Nonstandard_Analysis/StarDef.thy
--- a/src/HOL/Nonstandard_Analysis/StarDef.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Nonstandard_Analysis/StarDef.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -914,7 +914,7 @@
   have "inj (star_of :: 'a \<Rightarrow> 'a star)"
     by (rule injI) simp
   then have "inj (star_of \<circ> of_nat :: nat \<Rightarrow> 'a star)"
-    using inj_of_nat by (rule inj_comp)
+    using inj_of_nat by (rule inj_compose)
   then show "inj (of_nat :: nat \<Rightarrow> 'a star)"
     by (simp add: comp_def)
 qed
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Power.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -501,6 +501,14 @@
     done
 qed
 
+lemma power_decreasing_iff [simp]: "\<lbrakk>0 < b; b < 1\<rbrakk> \<Longrightarrow> b ^ m \<le> b ^ n \<longleftrightarrow> n \<le> m"
+  using power_strict_decreasing [of m n b]
+  by (auto intro: power_decreasing ccontr)
+
+lemma power_strict_decreasing_iff [simp]: "\<lbrakk>0 < b; b < 1\<rbrakk> \<Longrightarrow> b ^ m < b ^ n \<longleftrightarrow> n < m"
+  using power_decreasing_iff [of b m n] unfolding le_less
+  by (auto dest: power_strict_decreasing le_neq_implies_less)
+
 lemma power_Suc_less_one: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
   using power_strict_decreasing [of 0 "Suc n" a] by simp
 
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -322,7 +322,7 @@
 instance real_algebra_1 < ring_char_0
 proof
   from inj_of_real inj_of_nat have "inj (of_real \<circ> of_nat)"
-    by (rule inj_comp)
+    by (rule inj_compose)
   then show "inj (of_nat :: nat \<Rightarrow> 'a)"
     by (simp add: comp_def)
 qed
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Set.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -1857,6 +1857,9 @@
 definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
 
+lemma pairwise_trivial [simp]: "pairwise (\<lambda>i j. j \<noteq> i) I"
+  by (auto simp: pairwise_def)
+
 lemma pairwiseI [intro?]:
   "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y"
   using that by (simp add: pairwise_def)
diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Set_Interval.thy	Mon Jan 21 14:44:23 2019 +0000
@@ -683,7 +683,7 @@
 new elements get indices at the beginning. So it is used to transform
 \<^term>\<open>{..<Suc n}\<close> to \<^term>\<open>0::nat\<close> and \<^term>\<open>{..< n}\<close>.\<close>
 
-lemma zero_notin_Suc_image: "0 \<notin> Suc ` A"
+lemma zero_notin_Suc_image [simp]: "0 \<notin> Suc ` A"
   by auto
 
 lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})"