equal
deleted
inserted
replaced
6 section \<open>Chain-complete partial orders and their fixpoints\<close> |
6 section \<open>Chain-complete partial orders and their fixpoints\<close> |
7 |
7 |
8 theory Complete_Partial_Order |
8 theory Complete_Partial_Order |
9 imports Product_Type |
9 imports Product_Type |
10 begin |
10 begin |
11 |
|
12 subsection \<open>Monotone functions\<close> |
|
13 |
|
14 text \<open>Dictionary-passing version of \<^const>\<open>Orderings.mono\<close>.\<close> |
|
15 |
|
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))" |
|
18 |
|
19 lemma monotoneI[intro?]: "(\<And>x y. orda x y \<Longrightarrow> ordb (f x) (f y)) \<Longrightarrow> monotone orda ordb f" |
|
20 unfolding monotone_def by iprover |
|
21 |
|
22 lemma monotoneD[dest?]: "monotone orda ordb f \<Longrightarrow> orda x y \<Longrightarrow> ordb (f x) (f y)" |
|
23 unfolding monotone_def by iprover |
|
24 |
11 |
25 |
12 |
26 subsection \<open>Chains\<close> |
13 subsection \<open>Chains\<close> |
27 |
14 |
28 text \<open> |
15 text \<open> |