equal
deleted
inserted
replaced
415 "monotone orda (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))" |
415 "monotone orda (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))" |
416 by(auto simp add: monotone_def fun_ord_def) |
416 by(auto simp add: monotone_def fun_ord_def) |
417 |
417 |
418 context preorder begin |
418 context preorder begin |
419 |
419 |
420 lemma transp_le [simp, cont_intro]: "transp (\<le>)" |
420 declare transp_le[cont_intro] |
421 by(rule transpI)(rule order_trans) |
|
422 |
421 |
423 lemma monotone_const [simp, cont_intro]: "monotone ord (\<le>) (\<lambda>_. c)" |
422 lemma monotone_const [simp, cont_intro]: "monotone ord (\<le>) (\<lambda>_. c)" |
424 by(rule monotoneI) simp |
423 by(rule monotoneI) simp |
425 |
424 |
426 end |
425 end |