author desharna Wed, 25 May 2022 15:49:12 +0200 changeset 75960 15483f001222 parent 75959 84e6f9b542e2
redefined order.{,strict_}mono as abbreviations of monotone
 src/HOL/Orderings.thy file | annotate | diff | comparison | revisions src/HOL/Tools/inductive.ML file | annotate | diff | comparison | revisions
```--- 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)"
+
+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```