--- 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 +
--- 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"
--- 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
--- 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
--- 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)
--- 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"
--- 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
--- 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)"
--- 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
--- 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)"
--- 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
--- 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
--- 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"
--- 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]:
--- 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
--- 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
--- 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
--- 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)
--- 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})"