src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Fri Mar 16 21:32:08 2007 +0100
+++ b/src/HOL/Fun.thy	Fri Mar 16 21:32:09 2007 +0100
@@ -454,13 +454,17 @@
 by (simp add: bij_def)
 
 
-subsection {* Order on functions *}
+subsection {* Order and lattice on functions *}
+
+instance "fun" :: (type, ord) ord
+  le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
+  less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
+
+instance "fun" :: (type, preorder) preorder
+  by default (auto simp add: le_fun_def less_fun_def intro: order_trans)
 
 instance "fun" :: (type, order) order
-  le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
-  less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g"
-  by default
-    (auto simp add: le_fun_def less_fun_def intro: order_trans, rule ext, auto intro: order_antisym)
+  by default (rule ext, auto simp add: le_fun_def less_fun_def intro: order_antisym)
 
 lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
   unfolding le_fun_def by simp
@@ -471,7 +475,61 @@
 lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   unfolding le_fun_def by simp
 
-instance "fun" :: (type, ord) ord ..
+text {*
+  Handy introduction and elimination rules for @{text "\<le>"}
+  on unary and binary predicates
+*}
+
+lemma predicate1I [Pure.intro!, intro!]:
+  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
+  shows "P \<le> Q"
+  apply (rule le_funI)
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
+  apply (erule le_funE)
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma predicate2I [Pure.intro!, intro!]:
+  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
+  shows "P \<le> Q"
+  apply (rule le_funI)+
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
+  apply (erule le_funE)+
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
+  by (rule predicate1D)
+
+lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
+  by (rule predicate2D)
+
+instance "fun" :: (type, lattice) lattice
+  inf_fun_eq: "inf f g \<equiv> (\<lambda>x. inf (f x) (g x))"
+  sup_fun_eq: "sup f g \<equiv> (\<lambda>x. sup (f x) (g x))"
+apply intro_classes
+unfolding inf_fun_eq sup_fun_eq
+apply (auto intro: le_funI)
+apply (rule le_funI)
+apply (auto dest: le_funD)
+apply (rule le_funI)
+apply (auto dest: le_funD)
+done
+
+instance "fun" :: (type, distrib_lattice) distrib_lattice
+  by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
 
 
 subsection {* Code generator setup *}