--- a/src/HOL/Orderings.thy Wed May 25 14:39:46 2022 +0200
+++ b/src/HOL/Orderings.thy Wed May 25 15:49:12 2022 +0200
@@ -1069,30 +1069,43 @@
lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)"
unfolding monotone_def by iprover
+lemma monotoneE:
+ fixes f :: "'a \<Rightarrow> 'b::order"
+ assumes "monotone orda ordb f"
+ assumes "orda x y"
+ obtains "ordb (f x) (f y)"
+proof
+ from assms show "ordb (f x) (f y)" by (simp add: monotone_def)
+qed
+
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)"
+abbreviation mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
+ "mono \<equiv> monotone (\<le>) (\<le>)"
+
+lemma mono_def: "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)"
+ unfolding monotone_def by (rule refl)
+
+text \<open>@{thm [source] mono_def} is provided for backward compatibility with theories written when
+@{const mono} was a proper definition instead of an abbreviation of @{const monotone}.\<close>
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
+ by (rule monotoneI)
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
+ by (rule monotoneD)
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
+ using assms by (rule monotoneE)
definition antimono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
"antimono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<ge> f y)"
@@ -1116,17 +1129,23 @@
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)"
+abbreviation strict_mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where
+ "strict_mono \<equiv> monotone (<) (<)"
+
+lemma strict_mono_def: "strict_mono f \<longleftrightarrow> (\<forall>x y. x < y \<longrightarrow> f x < f y)"
+ by (simp add: monotone_def)
+
+text \<open>@{thm [source] strict_mono_def} is provided for backward compatibility with theories written
+when @{const strict_mono} was a proper definition instead of an abbreviation of @{const monotone}.\<close>
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
+ using assms by (rule monotoneI)
lemma strict_monoD [dest?]:
"strict_mono f \<Longrightarrow> x < y \<Longrightarrow> f x < f y"
- unfolding strict_mono_def by auto
+ by (rule monotoneD)
lemma strict_mono_mono [dest?]:
assumes "strict_mono f"
--- a/src/HOL/Tools/inductive.ML Wed May 25 14:39:46 2022 +0200
+++ b/src/HOL/Tools/inductive.ML Wed May 25 15:49:12 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>Orderings.monotone predT predT for
+ \<^Const>\<open>Orderings.ord_class.less_eq predT\<close> \<^Const>\<open>Orderings.ord_class.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