# HG changeset patch
# User noschinl
# Date 1331561484 -3600
# Node ID 6242b4bc05bcb4421d392a9dd5e19999f5ed61aa
# Parent  bad72cba8a92030ae308f7af689e3acfe4a382fe
tuned simpset

diff -r bad72cba8a92 -r 6242b4bc05bc src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sun Mar 11 22:06:13 2012 +0100
+++ b/src/HOL/Complete_Lattices.thy	Mon Mar 12 15:11:24 2012 +0100
@@ -579,14 +579,14 @@
 definition
   "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
 
-lemma Inf_apply (* CANDIDATE [simp] *) [code]:
+lemma Inf_apply [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 (* CANDIDATE [simp] *) [code]:
+lemma Sup_apply [simp, code]:
   "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   by (simp add: Sup_fun_def)
 
@@ -595,11 +595,11 @@
 
 end
 
-lemma INF_apply (* CANDIDATE [simp] *):
+lemma INF_apply [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 (* CANDIDATE [simp] *):
+lemma SUP_apply [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 bad72cba8a92 -r 6242b4bc05bc src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Mar 11 22:06:13 2012 +0100
+++ b/src/HOL/Lattices.thy	Mon Mar 12 15:11:24 2012 +0100
@@ -650,14 +650,14 @@
 definition
   "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
 
-lemma inf_apply (* CANDIDATE [simp, code] *):
+lemma inf_apply [simp] (* CANDIDATE [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 (* CANDIDATE [simp, code] *):
+lemma sup_apply [simp] (* CANDIDATE [code] *):
   "(f \<squnion> g) x = f x \<squnion> g x"
   by (simp add: sup_fun_def)
 
@@ -677,7 +677,7 @@
 definition
   fun_Compl_def: "- A = (\<lambda>x. - A x)"
 
-lemma uminus_apply (* CANDIDATE [simp, code] *):
+lemma uminus_apply [simp] (* CANDIDATE [code] *):
   "(- A) x = - (A x)"
   by (simp add: fun_Compl_def)
 
@@ -691,7 +691,7 @@
 definition
   fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
 
-lemma minus_apply (* CANDIDATE [simp, code] *):
+lemma minus_apply [simp] (* CANDIDATE [code] *):
   "(A - B) x = A x - B x"
   by (simp add: fun_diff_def)
 
diff -r bad72cba8a92 -r 6242b4bc05bc src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sun Mar 11 22:06:13 2012 +0100
+++ b/src/HOL/Orderings.thy	Mon Mar 12 15:11:24 2012 +0100
@@ -1299,7 +1299,7 @@
 definition
   "\<bottom> = (\<lambda>x. \<bottom>)"
 
-lemma bot_apply (* CANDIDATE [simp, code] *):
+lemma bot_apply [simp] (* CANDIDATE [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 (* CANDIDATE [simp, code] *):
+lemma top_apply [simp] (* CANDIDATE [code] *):
   "\<top> x = \<top>"
   by (simp add: top_fun_def)
 
diff -r bad72cba8a92 -r 6242b4bc05bc src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Mar 11 22:06:13 2012 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 12 15:11:24 2012 +0100
@@ -10,9 +10,8 @@
 
 text {* A preliminary: classical rules for reasoning on predicates *}
 
-(* CANDIDATE declare predicate1I [Pure.intro!, intro!] *)
-declare predicate1D [Pure.dest?, dest?]
-(* CANDIDATE declare predicate1D [Pure.dest, dest] *)
+declare predicate1I [Pure.intro!, intro!]
+declare predicate1D [Pure.dest, dest]
 declare predicate2I [Pure.intro!, intro!]
 declare predicate2D [Pure.dest, dest]
 declare bot1E [elim!] 
@@ -602,7 +601,7 @@
   "R O (S \<union> T) = (R O S) \<union> (R O T)" 
   by auto
 
-lemma pred_comp_distrib (* CANDIDATE [simp] *):
+lemma pred_comp_distrib [simp]:
   "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
   by (fact rel_comp_distrib [to_pred])
 
@@ -610,7 +609,7 @@
   "(S \<union> T) O R = (S O R) \<union> (T O R)"
   by auto
 
-lemma pred_comp_distrib2 (* CANDIDATE [simp] *):
+lemma pred_comp_distrib2 [simp]:
   "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
   by (fact rel_comp_distrib2 [to_pred])
 
@@ -672,7 +671,7 @@
   "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P"
   by (cases yx) (simp, erule converse.cases, iprover)
 
-lemmas conversepE (* CANDIDATE [elim!] *) = conversep.cases
+lemmas conversepE [elim!] = conversep.cases
 
 lemma converse_iff [iff]:
   "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r"
@@ -828,10 +827,10 @@
 lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
   by auto
 
-lemma Domain_insert (* CANDIDATE [simp] *): "Domain (insert (a, b) r) = insert a (Domain r)"
+lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)"
   by blast
 
-lemma Range_insert (* CANDIDATE [simp] *): "Range (insert (a, b) r) = insert b (Range r)"
+lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)"
   by blast
 
 lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r"
diff -r bad72cba8a92 -r 6242b4bc05bc src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Mar 11 22:06:13 2012 +0100
+++ b/src/HOL/Set.thy	Mon Mar 12 15:11:24 2012 +0100
@@ -124,7 +124,8 @@
 qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
   bot_set_def top_set_def uminus_set_def minus_set_def
   less_le_not_le inf_compl_bot sup_compl_top sup_inf_distrib1 diff_eq
-  set_eqI fun_eq_iff)
+  set_eqI fun_eq_iff
+  del: inf_apply sup_apply bot_apply top_apply minus_apply uminus_apply)
 
 end
 
diff -r bad72cba8a92 -r 6242b4bc05bc src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Mar 11 22:06:13 2012 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Mar 12 15:11:24 2012 +0100
@@ -299,8 +299,7 @@
 lemma wfP_SUP:
   "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
   apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred])
-  apply (simp_all add: inf_set_def)
-  apply auto
+  apply simp_all
   done
 
 lemma wf_Union: