--- 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 *}