equal
deleted
inserted
replaced
23 definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))" |
23 definition "img_ord f ord = (\<lambda>x y. ord (f x) (f y))" |
24 definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))" |
24 definition "img_lub f g Lub = (\<lambda>A. g (Lub (f ` A)))" |
25 |
25 |
26 lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)" |
26 lemma call_mono[partial_function_mono]: "monotone (fun_ord ord) ord (\<lambda>f. f t)" |
27 by (rule monotoneI) (auto simp: fun_ord_def) |
27 by (rule monotoneI) (auto simp: fun_ord_def) |
|
28 |
|
29 lemma let_mono[partial_function_mono]: |
|
30 "(\<And>x. monotone orda ordb (\<lambda>f. b f x)) |
|
31 \<Longrightarrow> monotone orda ordb (\<lambda>f. Let t (b f))" |
|
32 by (simp add: Let_def) |
28 |
33 |
29 lemma if_mono[partial_function_mono]: "monotone orda ordb F |
34 lemma if_mono[partial_function_mono]: "monotone orda ordb F |
30 \<Longrightarrow> monotone orda ordb G |
35 \<Longrightarrow> monotone orda ordb G |
31 \<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)" |
36 \<Longrightarrow> monotone orda ordb (\<lambda>f. if c then F f else G f)" |
32 unfolding monotone_def by simp |
37 unfolding monotone_def by simp |