equal
deleted
inserted
replaced
9 imports Product_Type |
9 imports Product_Type |
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>Monotone functions\<close> |
12 subsection \<open>Monotone functions\<close> |
13 |
13 |
14 text \<open>Dictionary-passing version of @{const Orderings.mono}.\<close> |
14 text \<open>Dictionary-passing version of \<^const>\<open>Orderings.mono\<close>.\<close> |
15 |
15 |
16 definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
16 definition monotone :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" |
17 where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))" |
17 where "monotone orda ordb f \<longleftrightarrow> (\<forall>x y. orda x y \<longrightarrow> ordb (f x) (f y))" |
18 |
18 |
19 lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f" |
19 lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f" |