# HG changeset patch
# User haftmann
# Date 1330266528 -3600
# Node ID f559866a7aa280cfc03efdbb862f6bc53a9ae01d
# Parent  f4ce220d2799bffe92564c7d38e01a072a175372
marked candidates for rule declarations

diff -r f4ce220d2799 -r f559866a7aa2 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sat Feb 25 15:33:36 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy	Sun Feb 26 15:28:48 2012 +0100
@@ -582,14 +582,14 @@
 definition
   "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
 
-lemma Inf_apply [code]:
+lemma Inf_apply (* CANDIDATE [simp] *) [code]:
   "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   by (simp add: Inf_fun_def)
 
 definition
   "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
 
-lemma Sup_apply [code]:
+lemma Sup_apply (* CANDIDATE [simp] *) [code]:
   "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   by (simp add: Sup_fun_def)
 
@@ -598,11 +598,11 @@
 
 end
 
-lemma INF_apply:
+lemma INF_apply (* CANDIDATE [simp] *):
   "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
 
-lemma SUP_apply:
+lemma SUP_apply (* CANDIDATE [simp] *):
   "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
 
diff -r f4ce220d2799 -r f559866a7aa2 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sat Feb 25 15:33:36 2012 +0100
+++ b/src/HOL/Lattices.thy	Sun Feb 26 15:28:48 2012 +0100
@@ -649,14 +649,14 @@
 definition
   "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
 
-lemma inf_apply:
+lemma inf_apply (* CANDIDATE [simp, code] *):
   "(f \<sqinter> g) x = f x \<sqinter> g x"
   by (simp add: inf_fun_def)
 
 definition
   "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
 
-lemma sup_apply:
+lemma sup_apply (* CANDIDATE [simp, code] *):
   "(f \<squnion> g) x = f x \<squnion> g x"
   by (simp add: sup_fun_def)
 
@@ -676,7 +676,7 @@
 definition
   fun_Compl_def: "- A = (\<lambda>x. - A x)"
 
-lemma uminus_apply:
+lemma uminus_apply (* CANDIDATE [simp, code] *):
   "(- A) x = - (A x)"
   by (simp add: fun_Compl_def)
 
@@ -690,7 +690,7 @@
 definition
   fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
 
-lemma minus_apply:
+lemma minus_apply (* CANDIDATE [simp, code] *):
   "(A - B) x = A x - B x"
   by (simp add: fun_diff_def)
 
diff -r f4ce220d2799 -r f559866a7aa2 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat Feb 25 15:33:36 2012 +0100
+++ b/src/HOL/Orderings.thy	Sun Feb 26 15:28:48 2012 +0100
@@ -1299,7 +1299,7 @@
 definition
   "\<bottom> = (\<lambda>x. \<bottom>)"
 
-lemma bot_apply:
+lemma bot_apply (* CANDIDATE [simp, code] *):
   "\<bottom> x = \<bottom>"
   by (simp add: bot_fun_def)
 
@@ -1315,7 +1315,7 @@
   [no_atp]: "\<top> = (\<lambda>x. \<top>)"
 declare top_fun_def_raw [no_atp]
 
-lemma top_apply:
+lemma top_apply (* CANDIDATE [simp, code] *):
   "\<top> x = \<top>"
   by (simp add: top_fun_def)
 
diff -r f4ce220d2799 -r f559866a7aa2 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Feb 25 15:33:36 2012 +0100
+++ b/src/HOL/Relation.thy	Sun Feb 26 15:28:48 2012 +0100
@@ -25,7 +25,9 @@
 
 subsection {* Classical rules for reasoning on predicates *}
 
+(* CANDIDATE declare predicate1I [Pure.intro!, intro!] *)
 declare predicate1D [Pure.dest?, dest?]
+(* CANDIDATE declare predicate1D [Pure.dest, dest] *)
 declare predicate2I [Pure.intro!, intro!]
 declare predicate2D [Pure.dest, dest]
 declare bot1E [elim!]
@@ -70,11 +72,17 @@
 lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) \<le> (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
   by (simp add: subset_iff le_fun_def)
 
-lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
+lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})"
+  by (auto simp add: fun_eq_iff)
+
+lemma bot_empty_eq2 (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
   by (auto simp add: fun_eq_iff)
 
-lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
-  by (auto simp add: fun_eq_iff)
+(* CANDIDATE lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
+  by (auto simp add: fun_eq_iff) *)
+
+(* CANDIDATE lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
+  by (auto simp add: fun_eq_iff) *)
 
 lemma inf_Int_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<sqinter> (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
   by (simp add: inf_fun_def)
@@ -88,10 +96,10 @@
 lemma sup_Un_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) \<squnion> (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
   by (simp add: sup_fun_def)
 
-lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
+lemma INF_INT_eq (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
   by (simp add: INF_apply fun_eq_iff)
 
-lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
+lemma INF_INT_eq2 (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
   by (simp add: INF_apply fun_eq_iff)
 
 lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
@@ -946,3 +954,4 @@
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
 
 end
+