--- a/NEWS Tue Jul 05 09:44:38 2022 +0200
+++ b/NEWS Sat Jun 25 13:21:27 2022 +0200
@@ -53,8 +53,14 @@
compatibility but its usage is discouraged. Minor INCOMPATIBILITY.
- Changed argument order of mono_on and strict_mono_on to uniformize
with monotone_on and the general "characterizing set at the beginning
- of predicates" preference. Also change them to be abbreviation of
- monotone_of. Minor INCOMPATIBILITY
+ of predicates" preference. Also change them to be abbreviations
+ of monotone_of. Lemmas mono_on_def and strict_mono_on_def are
+ explicitly provided for backward compatibility but their usage is
+ discouraged. INCOMPATIBILITY.
+ - Move mono, strict_mono, and relevant lemmas to Fun theory. Also change
+ them to be abbreviations of mono_on and strict_mono_on. Lemmas
+ mono_def and strict_mono_def, are explicitly provided for backward
+ compatibility but their usage is discouraged. Minor INCOMPATIBILITY.
- Added lemmas.
monotone_onD
monotone_onI
--- a/src/Doc/Main/Main_Doc.thy Tue Jul 05 09:44:38 2022 +0200
+++ b/src/Doc/Main/Main_Doc.thy Sat Jun 25 13:21:27 2022 +0200
@@ -58,8 +58,6 @@
\<^const>\<open>Orderings.max\<close> & \<^typeof>\<open>Orderings.max\<close>\\
@{const[source] top} & \<^typeof>\<open>Orderings.top\<close>\\
@{const[source] bot} & \<^typeof>\<open>Orderings.bot\<close>\\
-\<^const>\<open>Orderings.mono\<close> & \<^typeof>\<open>Orderings.mono\<close>\\
-\<^const>\<open>Orderings.strict_mono\<close> & \<^typeof>\<open>Orderings.strict_mono\<close>\\
\end{tabular}
\subsubsection*{Syntax}
@@ -152,6 +150,12 @@
\<^const>\<open>Fun.surj\<close> & \<^typeof>\<open>Fun.surj\<close>\\
\<^const>\<open>Fun.bij\<close> & \<^typeof>\<open>Fun.bij\<close>\\
\<^const>\<open>Fun.bij_betw\<close> & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\
+\<^const>\<open>Fun.monotone_on\<close> & \<^typeof>\<open>Fun.monotone_on\<close>\\
+\<^const>\<open>Fun.monotone\<close> & \<^typeof>\<open>Fun.monotone\<close>\\
+\<^const>\<open>Fun.mono_on\<close> & \<^typeof>\<open>Fun.mono_on\<close>\\
+\<^const>\<open>Fun.mono\<close> & \<^typeof>\<open>Fun.mono\<close>\\
+\<^const>\<open>Fun.strict_mono_on\<close> & \<^typeof>\<open>Fun.strict_mono_on\<close>\\
+\<^const>\<open>Fun.strict_mono\<close> & \<^typeof>\<open>Fun.strict_mono\<close>\\
\<^const>\<open>Fun.fun_upd\<close> & \<^typeof>\<open>Fun.fun_upd\<close>\\
\end{tabular}
--- a/src/HOL/Fun.thy Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Fun.thy Sat Jun 25 13:21:27 2022 +0200
@@ -590,9 +590,6 @@
lemma (in ordered_ab_group_add) inj_uminus[simp, intro]: "inj_on uminus A"
by (auto intro!: inj_onI)
-lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
- by (auto intro!: inj_onI dest: strict_mono_eq)
-
lemma bij_betw_byWitness:
assumes left: "\<forall>a \<in> A. f' (f a) = a"
and right: "\<forall>a' \<in> A'. f (f' a') = a'"
@@ -931,7 +928,7 @@
qed
-subsection \<open>Monotonic functions over a set\<close>
+subsection \<open>Monotonicity\<close>
definition monotone_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
where "monotone_on A orda ordb f \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. orda x y \<longrightarrow> ordb (f x) (f y))"
@@ -980,39 +977,45 @@
using mono_f[THEN monotone_onD] by simp
qed
-abbreviation mono_on :: "('a :: ord) set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+
+subsubsection \<open>Specializations For @{class ord} Type Class And More\<close>
+
+context ord begin
+
+abbreviation mono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
where "mono_on A \<equiv> monotone_on A (\<le>) (\<le>)"
-lemma mono_on_def: "mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s)"
+abbreviation strict_mono_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
+ where "strict_mono_on A \<equiv> monotone_on A (<) (<)"
+
+lemma mono_on_def[no_atp]: "mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s)"
by (auto simp add: monotone_on_def)
+lemma strict_mono_on_def[no_atp]:
+ "strict_mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s)"
+ by (auto simp add: monotone_on_def)
+
+text \<open>Lemmas @{thm [source] mono_on_def} and @{thm [source] strict_mono_on_def} are provided for
+backward compatibility.\<close>
+
lemma mono_onI:
"(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r \<le> s \<Longrightarrow> f r \<le> f s) \<Longrightarrow> mono_on A f"
by (rule monotone_onI)
-lemma mono_onD:
- "\<lbrakk>mono_on A f; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
+lemma strict_mono_onI:
+ "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on A f"
+ by (rule monotone_onI)
+
+lemma mono_onD: "\<lbrakk>mono_on A f; r \<in> A; s \<in> A; r \<le> s\<rbrakk> \<Longrightarrow> f r \<le> f s"
by (rule monotone_onD)
-lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on A f"
- unfolding mono_def mono_on_def by auto
+lemma strict_mono_onD: "\<lbrakk>strict_mono_on A f; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
+ by (rule monotone_onD)
lemma mono_on_subset: "mono_on A f \<Longrightarrow> B \<subseteq> A \<Longrightarrow> mono_on B f"
by (rule monotone_on_subset)
-abbreviation strict_mono_on :: "('a :: ord) set \<Rightarrow> ('a \<Rightarrow> 'b :: ord) \<Rightarrow> bool"
- where "strict_mono_on A \<equiv> monotone_on A (<) (<)"
-
-lemma strict_mono_on_def: "strict_mono_on A f \<longleftrightarrow> (\<forall>r s. r \<in> A \<and> s \<in> A \<and> r < s \<longrightarrow> f r < f s)"
- by (auto simp add: monotone_on_def)
-
-lemma strict_mono_onI:
- "(\<And>r s. r \<in> A \<Longrightarrow> s \<in> A \<Longrightarrow> r < s \<Longrightarrow> f r < f s) \<Longrightarrow> strict_mono_on A f"
- by (rule monotone_onI)
-
-lemma strict_mono_onD:
- "\<lbrakk>strict_mono_on A f; r \<in> A; s \<in> A; r < s\<rbrakk> \<Longrightarrow> f r < f s"
- by (rule monotone_onD)
+end
lemma mono_on_greaterD:
assumes "mono_on A g" "x \<in> A" "y \<in> A" "g x > (g (y::_::linorder) :: _ :: linorder)"
@@ -1024,6 +1027,136 @@
with assms(4) show False by simp
qed
+context order begin
+
+abbreviation mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool"
+ where "mono \<equiv> mono_on UNIV"
+
+abbreviation strict_mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool"
+ where "strict_mono \<equiv> strict_mono_on UNIV"
+
+lemma mono_def[no_atp]: "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
+ by (simp add: monotone_on_def)
+
+lemma strict_mono_def[no_atp]: "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
+ by (simp add: monotone_on_def)
+
+text \<open>Lemmas @{thm [source] mono_def} and @{thm [source] strict_mono_def} are provided for backward
+compatibility.\<close>
+
+lemma monoI [intro?]: "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
+ by (rule monotoneI)
+
+lemma strict_monoI [intro?]: "(\<And>x y. x < y \<Longrightarrow> f x < f y) \<Longrightarrow> strict_mono f"
+ by (rule monotoneI)
+
+lemma monoD [dest?]: "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+ by (rule monotoneD)
+
+lemma strict_monoD [dest?]: "strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
+ by (rule monotoneD)
+
+lemma monoE:
+ assumes "mono f"
+ assumes "x \<le> y"
+ obtains "f x \<le> f y"
+proof
+ from assms show "f x \<le> f y" by (simp add: mono_def)
+qed
+
+lemma mono_imp_mono_on: "mono f \<Longrightarrow> mono_on A f"
+ by (rule monotone_on_subset[OF _ subset_UNIV])
+
+lemma strict_mono_mono [dest?]:
+ assumes "strict_mono f"
+ shows "mono f"
+proof (rule monoI)
+ fix x y
+ assume "x \<le> y"
+ show "f x \<le> f y"
+ proof (cases "x = y")
+ case True then show ?thesis by simp
+ next
+ case False with \<open>x \<le> y\<close> have "x < y" by simp
+ with assms strict_monoD have "f x < f y" by auto
+ then show ?thesis by simp
+
+ qed
+qed
+
+end
+
+context linorder begin
+
+lemma mono_invE:
+ fixes f :: "'a \<Rightarrow> 'b::order"
+ assumes "mono f"
+ assumes "f x < f y"
+ obtains "x \<le> y"
+proof
+ show "x \<le> y"
+ proof (rule ccontr)
+ assume "\<not> x \<le> y"
+ then have "y \<le> x" by simp
+ with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
+ with \<open>f x < f y\<close> show False by simp
+ qed
+qed
+
+lemma mono_strict_invE:
+ fixes f :: "'a \<Rightarrow> 'b::order"
+ assumes "mono f"
+ assumes "f x < f y"
+ obtains "x < y"
+proof
+ show "x < y"
+ proof (rule ccontr)
+ assume "\<not> x < y"
+ then have "y \<le> x" by simp
+ with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
+ with \<open>f x < f y\<close> show False by simp
+ qed
+qed
+
+lemma strict_mono_eq:
+ assumes "strict_mono f"
+ shows "f x = f y \<longleftrightarrow> x = y"
+proof
+ assume "f x = f y"
+ show "x = y" proof (cases x y rule: linorder_cases)
+ case less with assms strict_monoD have "f x < f y" by auto
+ with \<open>f x = f y\<close> show ?thesis by simp
+ next
+ case equal then show ?thesis .
+ next
+ case greater with assms strict_monoD have "f y < f x" by auto
+ with \<open>f x = f y\<close> show ?thesis by simp
+ qed
+qed simp
+
+lemma strict_mono_less_eq:
+ assumes "strict_mono f"
+ shows "f x \<le> f y \<longleftrightarrow> x \<le> y"
+proof
+ assume "x \<le> y"
+ with assms strict_mono_mono monoD show "f x \<le> f y" by auto
+next
+ assume "f x \<le> f y"
+ show "x \<le> y" proof (rule ccontr)
+ assume "\<not> x \<le> y" then have "y < x" by simp
+ with assms strict_monoD have "f y < f x" by auto
+ with \<open>f x \<le> f y\<close> show False by simp
+ qed
+qed
+
+lemma strict_mono_less:
+ assumes "strict_mono f"
+ shows "f x < f y \<longleftrightarrow> x < y"
+ using assms
+ by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
+
+end
+
lemma strict_mono_inv:
fixes f :: "('a::linorder) \<Rightarrow> ('b::linorder)"
assumes "strict_mono f" and "surj f" and inv: "\<And>x. g (f x) = x"
@@ -1064,6 +1197,50 @@
"strict_mono_on A (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) \<Longrightarrow> mono_on A f"
by (rule mono_onI, rule strict_mono_on_leD)
+lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
+ unfolding mono_def le_fun_def by auto
+
+lemma mono_add:
+ fixes a :: "'a::ordered_ab_semigroup_add"
+ shows "mono ((+) a)"
+ by (simp add: add_left_mono monoI)
+
+lemma (in semilattice_inf) mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B"
+ for f :: "'a \<Rightarrow> 'b::semilattice_inf"
+ by (auto simp add: mono_def intro: Lattices.inf_greatest)
+
+lemma (in semilattice_sup) mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)"
+ for f :: "'a \<Rightarrow> 'b::semilattice_sup"
+ by (auto simp add: mono_def intro: Lattices.sup_least)
+
+lemma (in linorder) min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
+ by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
+
+lemma (in linorder) max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
+ by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
+
+lemma (in linorder) strict_mono_imp_inj_on: "strict_mono f \<Longrightarrow> inj_on f A"
+ by (auto intro!: inj_onI dest: strict_mono_eq)
+
+lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
+ by (fact mono_inf)
+
+lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
+ by (fact mono_sup)
+
+
+subsubsection \<open>Least value operator\<close>
+
+lemma Least_mono: "mono f \<Longrightarrow> \<exists>x\<in>S. \<forall>y\<in>S. x \<le> y \<Longrightarrow> (LEAST y. y \<in> f ` S) = f (LEAST x. x \<in> S)"
+ for f :: "'a::order \<Rightarrow> 'b::order"
+ \<comment> \<open>Courtesy of Stephan Merz\<close>
+ apply clarify
+ apply (erule_tac P = "\<lambda>x. x \<in> S" in LeastI2_order)
+ apply fast
+ apply (rule LeastI2_order)
+ apply (auto elim: monoD intro!: order_antisym)
+ done
+
subsection \<open>Setup\<close>
--- a/src/HOL/Groups.thy Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Groups.thy Sat Jun 25 13:21:27 2022 +0200
@@ -639,11 +639,6 @@
end
-lemma mono_add:
- fixes a :: "'a::ordered_ab_semigroup_add"
- shows "mono ((+) a)"
- by (simp add: add_left_mono monoI)
-
text \<open>Strict monotonicity in both arguments\<close>
class strict_ordered_ab_semigroup_add = ordered_ab_semigroup_add +
assumes add_strict_mono: "a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d"
--- a/src/HOL/Lattices.thy Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Lattices.thy Sat Jun 25 13:21:27 2022 +0200
@@ -220,9 +220,6 @@
lemma inf_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<le> c \<sqinter> d"
by (fast intro: inf_greatest le_infI1 le_infI2)
-lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<le> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
- by (auto simp add: mono_def intro: Lattices.inf_greatest)
-
end
context semilattice_sup
@@ -249,9 +246,6 @@
lemma sup_mono: "a \<le> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<le> c \<squnion> d"
by (fast intro: sup_least le_supI1 le_supI2)
-lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<le> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
- by (auto simp add: mono_def intro: Lattices.sup_least)
-
end
@@ -610,12 +604,6 @@
\<open>P (max a b) \<longleftrightarrow> (b = a \<longrightarrow> P a) \<and> (a < b \<longrightarrow> P b) \<and> (b < a \<longrightarrow> P a)\<close>
by (cases a b rule: linorder_cases) auto
-lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder"
- by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
-
-lemma max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" for f :: "'a \<Rightarrow> 'b::linorder"
- by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
-
end
lemma max_of_antimono: "antimono f \<Longrightarrow> max (f x) (f y) = f (min x y)"
--- a/src/HOL/Orderings.thy Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Orderings.thy Sat Jun 25 13:21:27 2022 +0200
@@ -1063,28 +1063,6 @@
context order
begin
-definition mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
- "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
-
-lemma monoI [intro?]:
- fixes f :: "'a \<Rightarrow> 'b::order"
- shows "(\<And>x y. x \<le> y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> mono f"
- unfolding mono_def by iprover
-
-lemma monoD [dest?]:
- fixes f :: "'a \<Rightarrow> 'b::order"
- shows "mono f \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
- unfolding mono_def by iprover
-
-lemma monoE:
- fixes f :: "'a \<Rightarrow> 'b::order"
- assumes "mono f"
- assumes "x \<le> y"
- obtains "f x \<le> f y"
-proof
- from assms show "f x \<le> f y" by (simp add: mono_def)
-qed
-
definition antimono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
"antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
@@ -1107,107 +1085,6 @@
from assms show "f x \<ge> f y" by (simp add: antimono_def)
qed
-definition strict_mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
- "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
-
-lemma strict_monoI [intro?]:
- assumes "\<And>x y. x < y \<Longrightarrow> f x < f y"
- shows "strict_mono f"
- using assms unfolding strict_mono_def by auto
-
-lemma strict_monoD [dest?]:
- "strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
- unfolding strict_mono_def by auto
-
-lemma strict_mono_mono [dest?]:
- assumes "strict_mono f"
- shows "mono f"
-proof (rule monoI)
- fix x y
- assume "x \<le> y"
- show "f x \<le> f y"
- proof (cases "x = y")
- case True then show ?thesis by simp
- next
- case False with \<open>x \<le> y\<close> have "x < y" by simp
- with assms strict_monoD have "f x < f y" by auto
- then show ?thesis by simp
-
- qed
-qed
-
-end
-
-context linorder
-begin
-
-lemma mono_invE:
- fixes f :: "'a \<Rightarrow> 'b::order"
- assumes "mono f"
- assumes "f x < f y"
- obtains "x \<le> y"
-proof
- show "x \<le> y"
- proof (rule ccontr)
- assume "\<not> x \<le> y"
- then have "y \<le> x" by simp
- with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
- with \<open>f x < f y\<close> show False by simp
- qed
-qed
-
-lemma mono_strict_invE:
- fixes f :: "'a \<Rightarrow> 'b::order"
- assumes "mono f"
- assumes "f x < f y"
- obtains "x < y"
-proof
- show "x < y"
- proof (rule ccontr)
- assume "\<not> x < y"
- then have "y \<le> x" by simp
- with \<open>mono f\<close> obtain "f y \<le> f x" by (rule monoE)
- with \<open>f x < f y\<close> show False by simp
- qed
-qed
-
-lemma strict_mono_eq:
- assumes "strict_mono f"
- shows "f x = f y \<longleftrightarrow> x = y"
-proof
- assume "f x = f y"
- show "x = y" proof (cases x y rule: linorder_cases)
- case less with assms strict_monoD have "f x < f y" by auto
- with \<open>f x = f y\<close> show ?thesis by simp
- next
- case equal then show ?thesis .
- next
- case greater with assms strict_monoD have "f y < f x" by auto
- with \<open>f x = f y\<close> show ?thesis by simp
- qed
-qed simp
-
-lemma strict_mono_less_eq:
- assumes "strict_mono f"
- shows "f x \<le> f y \<longleftrightarrow> x \<le> y"
-proof
- assume "x \<le> y"
- with assms strict_mono_mono monoD show "f x \<le> f y" by auto
-next
- assume "f x \<le> f y"
- show "x \<le> y" proof (rule ccontr)
- assume "\<not> x \<le> y" then have "y < x" by simp
- with assms strict_monoD have "f y < f x" by auto
- with \<open>f x \<le> f y\<close> show False by simp
- qed
-qed
-
-lemma strict_mono_less:
- assumes "strict_mono f"
- shows "f x < f y \<longleftrightarrow> x < y"
- using assms
- by (auto simp add: less_le Orderings.less_le strict_mono_eq strict_mono_less_eq)
-
end
@@ -1614,9 +1491,6 @@
lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
by (rule le_funE)
-lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
- unfolding mono_def le_fun_def by auto
-
subsection \<open>Order on unary and binary predicates\<close>
--- a/src/HOL/Set.thy Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Set.thy Sat Jun 25 13:21:27 2022 +0200
@@ -666,9 +666,6 @@
lemma IntE [elim!]: "c \<in> A \<inter> B \<Longrightarrow> (c \<in> A \<Longrightarrow> c \<in> B \<Longrightarrow> P) \<Longrightarrow> P"
by simp
-lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
- by (fact mono_inf)
-
subsubsection \<open>Binary union\<close>
@@ -700,9 +697,6 @@
lemma insert_def: "insert a B = {x. x = a} \<union> B"
by (simp add: insert_compr Un_def)
-lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
- by (fact mono_sup)
-
subsubsection \<open>Set difference\<close>
@@ -1808,19 +1802,6 @@
qed
-subsubsection \<open>Least value operator\<close>
-
-lemma Least_mono: "mono f \<Longrightarrow> \<exists>x\<in>S. \<forall>y\<in>S. x \<le> y \<Longrightarrow> (LEAST y. y \<in> f ` S) = f (LEAST x. x \<in> S)"
- for f :: "'a::order \<Rightarrow> 'b::order"
- \<comment> \<open>Courtesy of Stephan Merz\<close>
- apply clarify
- apply (erule_tac P = "\<lambda>x. x \<in> S" in LeastI2_order)
- apply fast
- apply (rule LeastI2_order)
- apply (auto elim: monoD intro!: order_antisym)
- done
-
-
subsubsection \<open>Monad operation\<close>
definition bind :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
--- a/src/HOL/Tools/inductive.ML Tue Jul 05 09:44:38 2022 +0200
+++ b/src/HOL/Tools/inductive.ML Sat Jun 25 13:21:27 2022 +0200
@@ -399,7 +399,8 @@
(if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt
[] []
(HOLogic.mk_Trueprop
- (Const (\<^const_name>\<open>Orderings.mono\<close>, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
+ (\<^Const>\<open>monotone_on predT predT for
+ \<^Const>\<open>top \<^Type>\<open>set predT\<close>\<close> \<^Const>\<open>less_eq predT\<close> \<^Const>\<open>less_eq predT\<close> fp_fun\<close>))
(fn _ => EVERY [resolve_tac ctxt @{thms monoI} 1,
REPEAT (resolve_tac ctxt [@{thm le_funI}, @{thm le_boolI'}] 1),
REPEAT (FIRST