1.1 --- a/src/HOL/Predicate.thy	Thu Aug 04 19:29:52 2011 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Thu Aug 04 20:11:39 2011 +0200
     1.3 @@ -431,7 +431,7 @@
     1.4    "x \<in> (op =) y \<longleftrightarrow> x = y"
     1.5    by (auto simp add: mem_def)
     1.6  
     1.7 -instantiation pred :: (type) complete_boolean_algebra
     1.8 +instantiation pred :: (type) complete_lattice
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -482,6 +482,22 @@
    1.13    "eval (\<Squnion>A) = SUPR A eval"
    1.14    by (simp add: Sup_pred_def)
    1.15  
    1.16 +instance proof
    1.17 +qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def)
    1.18 +
    1.19 +end
    1.20 +
    1.21 +lemma eval_INFI [simp]:
    1.22 +  "eval (INFI A f) = INFI A (eval \<circ> f)"
    1.23 +  by (unfold INFI_def) simp
    1.24 +
    1.25 +lemma eval_SUPR [simp]:
    1.26 +  "eval (SUPR A f) = SUPR A (eval \<circ> f)"
    1.27 +  by (unfold SUPR_def) simp
    1.28 +
    1.29 +instantiation pred :: (type) complete_boolean_algebra
    1.30 +begin
    1.31 +
    1.32  definition
    1.33    "- P = Pred (- eval P)"
    1.34  
    1.35 @@ -497,18 +513,10 @@
    1.36    by (simp add: minus_pred_def)
    1.37  
    1.38  instance proof
    1.39 -qed (auto intro!: pred_eqI simp add: less_eq_pred_def less_pred_def uminus_apply minus_apply)
    1.40 +qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply)
    1.41  
    1.42  end
    1.43  
    1.44 -lemma eval_INFI [simp]:
    1.45 -  "eval (INFI A f) = INFI A (eval \<circ> f)"
    1.46 -  by (unfold INFI_def) simp
    1.47 -
    1.48 -lemma eval_SUPR [simp]:
    1.49 -  "eval (SUPR A f) = SUPR A (eval \<circ> f)"
    1.50 -  by (unfold SUPR_def) simp
    1.51 -
    1.52  definition single :: "'a \<Rightarrow> 'a pred" where
    1.53    "single x = Pred ((op =) x)"
    1.54