# 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: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Min N \<le> Min M"
-by(simp add:Finite_Set.Min_def min.fold1_antimono)
+  by (simp add: Min_def min.fold1_antimono)
 
 lemma Max_mono: "\<lbrakk> M \<subseteq> N; M \<noteq> {}; finite N \<rbrakk> \<Longrightarrow> Max M \<le> Max N"
-by(simp add:Max_def max.fold1_antimono)
+  by (simp add: Max_def max.fold1_antimono)
 
 lemma Min_le [simp]: "\<lbrakk> finite A; A \<noteq> {}; x \<in> A \<rbrakk> \<Longrightarrow> Min A \<le> 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))
   \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> 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))
   \<Longrightarrow> finite N \<Longrightarrow> N \<noteq> {} \<Longrightarrow> 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 \<longleftrightarrow> (\<forall>x\<Colon>'a\<Colon>finite \<in> UNIV. (f x \<Colon> 'b\<Colon>eq) = g x)"
   unfolding expand_fun_eq by auto
 
+lemma order_fun [code func]:
+  "f \<le> g \<longleftrightarrow> (\<forall>x\<Colon>'a\<Colon>finite \<in> UNIV. (f x \<Colon> 'b\<Colon>order) \<le> g x)"
+  "f < g \<longleftrightarrow> f \<le> g \<and> (\<exists>x\<Colon>'a\<Colon>finite \<in> UNIV. (f x \<Colon> 'b\<Colon>order) < g x)"
+  unfolding le_fun_def less_fun_def less_le
+  by (auto simp add: expand_fun_eq)
+
 end