# HG changeset patch
# User haftmann
# Date 1254330288 -7200
# Node ID e43d761a742d56ebd9623550fd649b6503887873
# Parent  a92a18253f1e94228487feb5383d05ab9bdc5405# Parent  faf347097852985770103d862aeb46c3ac9b0cb1
merged

diff -r a92a18253f1e -r e43d761a742d src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Sep 30 15:00:43 2009 +0200
+++ b/src/HOL/Lattices.thy	Wed Sep 30 19:04:48 2009 +0200
@@ -535,6 +535,18 @@
 
 end
 
+lemma sup_boolI1:
+  "P \<Longrightarrow> P \<squnion> Q"
+  by (simp add: sup_bool_eq)
+
+lemma sup_boolI2:
+  "Q \<Longrightarrow> P \<squnion> Q"
+  by (simp add: sup_bool_eq)
+
+lemma sup_boolE:
+  "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
+  by (auto simp add: sup_bool_eq)
+
 
 subsection {* Fun as lattice *}
 
@@ -547,21 +559,14 @@
 definition
   sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
 
-instance
-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 proof
+qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)
 
 end
 
 instance "fun" :: (type, distrib_lattice) distrib_lattice
 proof
-qed (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
+qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
 
 instantiation "fun" :: (type, uminus) uminus
 begin
diff -r a92a18253f1e -r e43d761a742d src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Sep 30 15:00:43 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed Sep 30 19:04:48 2009 +0200
@@ -19,22 +19,7 @@
 
 subsection {* Predicates as (complete) lattices *}
 
-subsubsection {* @{const sup} on @{typ bool} *}
-
-lemma sup_boolI1:
-  "P \<Longrightarrow> P \<squnion> Q"
-  by (simp add: sup_bool_eq)
-
-lemma sup_boolI2:
-  "Q \<Longrightarrow> P \<squnion> Q"
-  by (simp add: sup_bool_eq)
-
-lemma sup_boolE:
-  "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: sup_bool_eq)
-
-
-subsubsection {* Equality and Subsets *}
+subsubsection {* Equality *}
 
 lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
   by (simp add: mem_def)
@@ -42,6 +27,9 @@
 lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
   by (simp add: expand_fun_eq mem_def)
 
+
+subsubsection {* Order relation *}
+
 lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
   by (simp add: mem_def)
 
@@ -63,9 +51,6 @@
 lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
   by (simp add: bot_fun_eq bot_bool_eq)
 
-
-subsubsection {* The empty set *}
-
 lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
   by (auto simp add: expand_fun_eq)