# HG changeset patch # User haftmann # Date 1173426357 -3600 # Node ID c252770ae2d0e38acc2b61e720bcc9d2687535cd # Parent 8a54121216871f08174d26b1d7437e52912d2e03 moved order on functions here diff -r 8a5412121687 -r c252770ae2d0 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Fri Mar 09 08:45:55 2007 +0100 +++ b/src/HOL/Finite_Set.thy Fri Mar 09 08:45:57 2007 +0100 @@ -2447,10 +2447,10 @@ by(fastsimp simp: Max_def max_def) lemma Min_antimono: "\ M \ N; M \ {}; finite N \ \ Min N \ Min M" -by(simp add:Finite_Set.Min_def min.fold1_antimono) + by (simp add: Min_def min.fold1_antimono) lemma Max_mono: "\ M \ N; M \ {}; finite N \ \ Max M \ Max N" -by(simp add:Max_def max.fold1_antimono) + by (simp add: Max_def max.fold1_antimono) lemma Min_le [simp]: "\ finite A; A \ {}; x \ A \ \ Min A \ x" by(simp add: Min_def min.fold1_belowI) @@ -2502,12 +2502,12 @@ lemma hom_Min_commute: "(!!x y::'a::linorder. h(min x y) = min (h x) (h y::'a)) \ finite N \ N \ {} \ h(Min N) = Min(h ` N)" -by(simp add:Finite_Set.Min_def min.hom_fold1_commute) + by (simp add: Min_def min.hom_fold1_commute) lemma hom_Max_commute: "(!!x y::'a::linorder. h(max x y) = max (h x) (h y::'a)) \ finite N \ N \ {} \ h(Max N) = Max(h ` N)" -by(simp add:Max_def max.hom_fold1_commute) + by( simp add: Max_def max.hom_fold1_commute) lemma add_Min_commute: fixes k::"'a::{pordered_ab_semigroup_add,linorder}" @@ -2628,7 +2628,7 @@ qed -subsection {* Equality on functions *} +subsection {* Equality and order on functions *} instance "fun" :: (finite, eq) eq .. @@ -2636,4 +2636,10 @@ "f = g \ (\x\'a\finite \ UNIV. (f x \ 'b\eq) = g x)" unfolding expand_fun_eq by auto +lemma order_fun [code func]: + "f \ g \ (\x\'a\finite \ UNIV. (f x \ 'b\order) \ g x)" + "f < g \ f \ g \ (\x\'a\finite \ UNIV. (f x \ 'b\order) < g x)" + unfolding le_fun_def less_fun_def less_le + by (auto simp add: expand_fun_eq) + end