--- 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)
--- 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)
--- 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)
--- 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"
--- 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
--- 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: