# HG changeset patch
# User haftmann
# Date 1312481499 -7200
# Node ID bc45393f497be6549cf668c7367585af3f3a3957
# Parent  cb768f4ceaf9074c2b5bc26fe6d95fbb0e4356cd
more fine-granular instantiation

diff -r cb768f4ceaf9 -r bc45393f497b src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Thu Aug 04 19:29:52 2011 +0200
+++ b/src/HOL/Predicate.thy	Thu Aug 04 20:11:39 2011 +0200
@@ -431,7 +431,7 @@
   "x \<in> (op =) y \<longleftrightarrow> x = y"
   by (auto simp add: mem_def)
 
-instantiation pred :: (type) complete_boolean_algebra
+instantiation pred :: (type) complete_lattice
 begin
 
 definition
@@ -482,6 +482,22 @@
   "eval (\<Squnion>A) = SUPR A eval"
   by (simp add: Sup_pred_def)
 
+instance proof
+qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def)
+
+end
+
+lemma eval_INFI [simp]:
+  "eval (INFI A f) = INFI A (eval \<circ> f)"
+  by (unfold INFI_def) simp
+
+lemma eval_SUPR [simp]:
+  "eval (SUPR A f) = SUPR A (eval \<circ> f)"
+  by (unfold SUPR_def) simp
+
+instantiation pred :: (type) complete_boolean_algebra
+begin
+
 definition
   "- P = Pred (- eval P)"
 
@@ -497,18 +513,10 @@
   by (simp add: minus_pred_def)
 
 instance proof
-qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def uminus_apply minus_apply)
+qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply)
 
 end
 
-lemma eval_INFI [simp]:
-  "eval (INFI A f) = INFI A (eval \<circ> f)"
-  by (unfold INFI_def) simp
-
-lemma eval_SUPR [simp]:
-  "eval (SUPR A f) = SUPR A (eval \<circ> f)"
-  by (unfold SUPR_def) simp
-
 definition single :: "'a \<Rightarrow> 'a pred" where
   "single x = Pred ((op =) x)"