--- a/NEWS Tue Jun 21 23:36:16 2022 +0200
+++ b/NEWS Wed Jun 22 14:52:27 2022 +0200
@@ -40,8 +40,18 @@
* Theory "HOL.Bit_Operations": rule bit_0 is not default [simp] any
longer. INCOMPATIBILITY.
+* Theory "HOL.Fun":
+ - Added predicate monotone_on and redefined monotone to be an
+ abbreviation. Lemma monotone_def is explicitly provided for backward
+ compatibility but its usage is discouraged. Minor INCOMPATIBILITY.
+ - Added lemmas.
+ monotone_onD
+ monotone_onI
+ monotone_on_empty[simp]
+ monotone_on_subset
+
* Theory "HOL.Relation":
- - Added predicate reflp_on and redefined reflp to ab an abbreviation.
+ - Added predicate reflp_on and redefined reflp to be an abbreviation.
Lemma reflp_def is explicitly provided for backward compatibility
but its usage is discouraged. Minor INCOMPATIBILITY.
- Added predicate totalp_on and abbreviation totalp.
@@ -92,6 +102,8 @@
image_mset_eq_plusD
image_mset_eq_plus_image_msetD
image_mset_filter_mset_swap
+ monotone_multp_multp_image_mset
+ monotone_on_multp_multp_image_mset
multp_image_mset_image_msetD
* Theory "HOL-Library.Sublist":
--- a/src/HOL/Fun.thy Tue Jun 21 23:36:16 2022 +0200
+++ b/src/HOL/Fun.thy Wed Jun 22 14:52:27 2022 +0200
@@ -927,8 +927,40 @@
then show False by blast
qed
+
subsection \<open>Monotonic functions over a set\<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))"
+
+abbreviation monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
+ where "monotone \<equiv> monotone_on UNIV"
+
+lemma monotone_def[no_atp]: "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
+ by (simp add: monotone_on_def)
+
+text \<open>Lemma @{thm [source] monotone_def} is provided for backward compatibility.\<close>
+
+lemma monotone_onI:
+ "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone_on A orda ordb f"
+ by (simp add: monotone_on_def)
+
+lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f"
+ by (rule monotone_onI)
+
+lemma monotone_onD:
+ "monotone_on A orda ordb f \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
+ by (simp add: monotone_on_def)
+
+lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
+ by (simp add: monotone_onD)
+
+lemma monotone_on_subset: "monotone_on A orda ordb f \<Longrightarrow> B \<subseteq> A \<Longrightarrow> monotone_on B orda ordb f"
+ by (auto intro: monotone_onI dest: monotone_onD)
+
+lemma monotone_on_empty[simp]: "monotone_on {} orda ordb f"
+ by (auto intro: monotone_onI dest: monotone_onD)
+
definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
lemma mono_onI:
--- a/src/HOL/Library/Complete_Partial_Order2.thy Tue Jun 21 23:36:16 2022 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Wed Jun 22 14:52:27 2022 +0200
@@ -373,9 +373,9 @@
| NONE => NONE
in
case Thm.term_of ct of
- t as Const (\<^const_name>\<open>ccpo.admissible\<close>, _) $ _ $ _ $ _ => mk_thm t
- | t as Const (\<^const_name>\<open>mcont\<close>, _) $ _ $ _ $ _ $ _ $ _ => mk_thm t
- | t as Const (\<^const_name>\<open>monotone\<close>, _) $ _ $ _ $ _ => mk_thm t
+ t as \<^Const_>\<open>ccpo.admissible _ for _ _ _\<close> => mk_thm t
+ | t as \<^Const_>\<open>mcont _ _ for _ _ _ _ _\<close> => mk_thm t
+ | t as \<^Const_>\<open>monotone_on _ _ for \<^Const_>\<open>Orderings.top _\<close> _ _ _\<close> => mk_thm t
| _ => NONE
end
handle THM _ => NONE
--- a/src/HOL/Library/Multiset.thy Tue Jun 21 23:36:16 2022 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Jun 22 14:52:27 2022 +0200
@@ -3191,6 +3191,54 @@
subsubsection \<open>Monotonicity\<close>
+lemma monotone_on_multp_multp_image_mset:
+ assumes "monotone_on A orda ordb f" and "transp orda"
+ shows "monotone_on {M. set_mset M \<subseteq> A} (multp orda) (multp ordb) (image_mset f)"
+proof (rule monotone_onI)
+ fix M1 M2
+ assume
+ M1_in: "M1 \<in> {M. set_mset M \<subseteq> A}" and
+ M2_in: "M2 \<in> {M. set_mset M \<subseteq> A}" and
+ M1_lt_M2: "multp orda M1 M2"
+
+ from multp_implies_one_step[OF \<open>transp orda\<close> M1_lt_M2] obtain I J K where
+ M2_eq: "M2 = I + J" and
+ M1_eq: "M1 = I + K" and
+ J_neq_mempty: "J \<noteq> {#}" and
+ ball_K_less: "\<forall>k\<in>#K. \<exists>x\<in>#J. orda k x"
+ by metis
+
+ have "multp ordb (image_mset f I + image_mset f K) (image_mset f I + image_mset f J)"
+ proof (intro one_step_implies_multp ballI)
+ show "image_mset f J \<noteq> {#}"
+ using J_neq_mempty by simp
+ next
+ fix k' assume "k'\<in>#image_mset f K"
+ then obtain k where "k' = f k" and k_in: "k \<in># K"
+ by auto
+ then obtain j where j_in: "j\<in>#J" and "orda k j"
+ using ball_K_less by auto
+
+ have "ordb (f k) (f j)"
+ proof (rule \<open>monotone_on A orda ordb f\<close>[THEN monotone_onD, OF _ _ \<open>orda k j\<close>])
+ show "k \<in> A"
+ using M1_eq M1_in k_in by auto
+ next
+ show "j \<in> A"
+ using M2_eq M2_in j_in by auto
+ qed
+ thus "\<exists>j\<in>#image_mset f J. ordb k' j"
+ using \<open>j \<in># J\<close> \<open>k' = f k\<close> by auto
+ qed
+ thus "multp ordb (image_mset f M1) (image_mset f M2)"
+ by (simp add: M1_eq M2_eq)
+qed
+
+lemma monotone_multp_multp_image_mset:
+ assumes "monotone orda ordb f" and "transp orda"
+ shows "monotone (multp orda) (multp ordb) (image_mset f)"
+ by (rule monotone_on_multp_multp_image_mset[OF assms, simplified])
+
lemma multp_image_mset_image_msetD:
assumes
"multp R (image_mset f A) (image_mset f B)" and
--- a/src/HOL/Orderings.thy Tue Jun 21 23:36:16 2022 +0200
+++ b/src/HOL/Orderings.thy Wed Jun 22 14:52:27 2022 +0200
@@ -1060,15 +1060,6 @@
subsection \<open>Monotonicity\<close>
-definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool"
- where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))"
-
-lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f"
- unfolding monotone_def by iprover
-
-lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
- unfolding monotone_def by iprover
-
context order
begin