equal
deleted
inserted
replaced
1058 *) |
1058 *) |
1059 |
1059 |
1060 |
1060 |
1061 subsection \<open>Monotonicity\<close> |
1061 subsection \<open>Monotonicity\<close> |
1062 |
1062 |
1063 definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
|
1064 where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))" |
|
1065 |
|
1066 lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f" |
|
1067 unfolding monotone_def by iprover |
|
1068 |
|
1069 lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)" |
|
1070 unfolding monotone_def by iprover |
|
1071 |
|
1072 context order |
1063 context order |
1073 begin |
1064 begin |
1074 |
1065 |
1075 definition mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where |
1066 definition mono :: "('a \<Rightarrow> 'b::order) \<Rightarrow> bool" where |
1076 "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)" |
1067 "mono f \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)" |