equal
deleted
inserted
replaced
599 *} |
599 *} |
600 |
600 |
601 |
601 |
602 subsubsection {* Monotonicity *} |
602 subsubsection {* Monotonicity *} |
603 |
603 |
604 constdefs |
604 locale mono = |
605 mono :: "['a::ord => 'b::ord] => bool" |
605 fixes f |
606 "mono f == ALL A B. A <= B --> f A <= f B" |
606 assumes mono: "A <= B ==> f A <= f B" |
607 |
607 |
608 lemma monoI [intro?]: "(!!A B. A <= B ==> f A <= f B) ==> mono f" |
608 lemmas monoI [intro?] = mono.intro [OF mono_axioms.intro] |
609 by (unfold mono_def) rules |
609 and monoD [dest?] = mono.mono |
610 |
610 |
611 lemma monoD [dest?]: "mono f ==> A <= B ==> f A <= f B" |
611 lemma mono_def: "mono f == ALL A B. A <= B --> f A <= f B" |
612 by (unfold mono_def) rules |
612 -- compatibility |
|
613 by (simp only: atomize_eq mono_def mono_axioms_def) |
|
614 |
613 |
615 |
614 constdefs |
616 constdefs |
615 min :: "['a::ord, 'a] => 'a" |
617 min :: "['a::ord, 'a] => 'a" |
616 "min a b == (if a <= b then a else b)" |
618 "min a b == (if a <= b then a else b)" |
617 max :: "['a::ord, 'a] => 'a" |
619 max :: "['a::ord, 'a] => 'a" |