tuned simpset
authornoschinl
Mon Mar 12 15:11:24 2012 +0100 (2012-03-12)
changeset 468826242b4bc05bc
parent 46872 bad72cba8a92
child 46883 eec472dae593
tuned simpset
src/HOL/Complete_Lattices.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
src/HOL/Relation.thy
src/HOL/Set.thy
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Sun Mar 11 22:06:13 2012 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Mon Mar 12 15:11:24 2012 +0100
     1.3 @@ -579,14 +579,14 @@
     1.4  definition
     1.5    "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
     1.6  
     1.7 -lemma Inf_apply (* CANDIDATE [simp] *) [code]:
     1.8 +lemma Inf_apply [simp, code]:
     1.9    "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
    1.10    by (simp add: Inf_fun_def)
    1.11  
    1.12  definition
    1.13    "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
    1.14  
    1.15 -lemma Sup_apply (* CANDIDATE [simp] *) [code]:
    1.16 +lemma Sup_apply [simp, code]:
    1.17    "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
    1.18    by (simp add: Sup_fun_def)
    1.19  
    1.20 @@ -595,11 +595,11 @@
    1.21  
    1.22  end
    1.23  
    1.24 -lemma INF_apply (* CANDIDATE [simp] *):
    1.25 +lemma INF_apply [simp]:
    1.26    "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
    1.27    by (auto intro: arg_cong [of _ _ Inf] simp add: INF_def Inf_apply)
    1.28  
    1.29 -lemma SUP_apply (* CANDIDATE [simp] *):
    1.30 +lemma SUP_apply [simp]:
    1.31    "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
    1.32    by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
    1.33  
     2.1 --- a/src/HOL/Lattices.thy	Sun Mar 11 22:06:13 2012 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Mon Mar 12 15:11:24 2012 +0100
     2.3 @@ -650,14 +650,14 @@
     2.4  definition
     2.5    "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
     2.6  
     2.7 -lemma inf_apply (* CANDIDATE [simp, code] *):
     2.8 +lemma inf_apply [simp] (* CANDIDATE [code] *):
     2.9    "(f \<sqinter> g) x = f x \<sqinter> g x"
    2.10    by (simp add: inf_fun_def)
    2.11  
    2.12  definition
    2.13    "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    2.14  
    2.15 -lemma sup_apply (* CANDIDATE [simp, code] *):
    2.16 +lemma sup_apply [simp] (* CANDIDATE [code] *):
    2.17    "(f \<squnion> g) x = f x \<squnion> g x"
    2.18    by (simp add: sup_fun_def)
    2.19  
    2.20 @@ -677,7 +677,7 @@
    2.21  definition
    2.22    fun_Compl_def: "- A = (\<lambda>x. - A x)"
    2.23  
    2.24 -lemma uminus_apply (* CANDIDATE [simp, code] *):
    2.25 +lemma uminus_apply [simp] (* CANDIDATE [code] *):
    2.26    "(- A) x = - (A x)"
    2.27    by (simp add: fun_Compl_def)
    2.28  
    2.29 @@ -691,7 +691,7 @@
    2.30  definition
    2.31    fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
    2.32  
    2.33 -lemma minus_apply (* CANDIDATE [simp, code] *):
    2.34 +lemma minus_apply [simp] (* CANDIDATE [code] *):
    2.35    "(A - B) x = A x - B x"
    2.36    by (simp add: fun_diff_def)
    2.37  
     3.1 --- a/src/HOL/Orderings.thy	Sun Mar 11 22:06:13 2012 +0100
     3.2 +++ b/src/HOL/Orderings.thy	Mon Mar 12 15:11:24 2012 +0100
     3.3 @@ -1299,7 +1299,7 @@
     3.4  definition
     3.5    "\<bottom> = (\<lambda>x. \<bottom>)"
     3.6  
     3.7 -lemma bot_apply (* CANDIDATE [simp, code] *):
     3.8 +lemma bot_apply [simp] (* CANDIDATE [code] *):
     3.9    "\<bottom> x = \<bottom>"
    3.10    by (simp add: bot_fun_def)
    3.11  
    3.12 @@ -1315,7 +1315,7 @@
    3.13    [no_atp]: "\<top> = (\<lambda>x. \<top>)"
    3.14  declare top_fun_def_raw [no_atp]
    3.15  
    3.16 -lemma top_apply (* CANDIDATE [simp, code] *):
    3.17 +lemma top_apply [simp] (* CANDIDATE [code] *):
    3.18    "\<top> x = \<top>"
    3.19    by (simp add: top_fun_def)
    3.20  
     4.1 --- a/src/HOL/Relation.thy	Sun Mar 11 22:06:13 2012 +0100
     4.2 +++ b/src/HOL/Relation.thy	Mon Mar 12 15:11:24 2012 +0100
     4.3 @@ -10,9 +10,8 @@
     4.4  
     4.5  text {* A preliminary: classical rules for reasoning on predicates *}
     4.6  
     4.7 -(* CANDIDATE declare predicate1I [Pure.intro!, intro!] *)
     4.8 -declare predicate1D [Pure.dest?, dest?]
     4.9 -(* CANDIDATE declare predicate1D [Pure.dest, dest] *)
    4.10 +declare predicate1I [Pure.intro!, intro!]
    4.11 +declare predicate1D [Pure.dest, dest]
    4.12  declare predicate2I [Pure.intro!, intro!]
    4.13  declare predicate2D [Pure.dest, dest]
    4.14  declare bot1E [elim!] 
    4.15 @@ -602,7 +601,7 @@
    4.16    "R O (S \<union> T) = (R O S) \<union> (R O T)" 
    4.17    by auto
    4.18  
    4.19 -lemma pred_comp_distrib (* CANDIDATE [simp] *):
    4.20 +lemma pred_comp_distrib [simp]:
    4.21    "R OO (S \<squnion> T) = R OO S \<squnion> R OO T"
    4.22    by (fact rel_comp_distrib [to_pred])
    4.23  
    4.24 @@ -610,7 +609,7 @@
    4.25    "(S \<union> T) O R = (S O R) \<union> (T O R)"
    4.26    by auto
    4.27  
    4.28 -lemma pred_comp_distrib2 (* CANDIDATE [simp] *):
    4.29 +lemma pred_comp_distrib2 [simp]:
    4.30    "(S \<squnion> T) OO R = S OO R \<squnion> T OO R"
    4.31    by (fact rel_comp_distrib2 [to_pred])
    4.32  
    4.33 @@ -672,7 +671,7 @@
    4.34    "yx \<in> r\<inverse> \<Longrightarrow> (\<And>x y. yx = (y, x) \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> P) \<Longrightarrow> P"
    4.35    by (cases yx) (simp, erule converse.cases, iprover)
    4.36  
    4.37 -lemmas conversepE (* CANDIDATE [elim!] *) = conversep.cases
    4.38 +lemmas conversepE [elim!] = conversep.cases
    4.39  
    4.40  lemma converse_iff [iff]:
    4.41    "(a, b) \<in> r\<inverse> \<longleftrightarrow> (b, a) \<in> r"
    4.42 @@ -828,10 +827,10 @@
    4.43  lemma Range_empty_iff: "Range r = {} \<longleftrightarrow> r = {}"
    4.44    by auto
    4.45  
    4.46 -lemma Domain_insert (* CANDIDATE [simp] *): "Domain (insert (a, b) r) = insert a (Domain r)"
    4.47 +lemma Domain_insert [simp]: "Domain (insert (a, b) r) = insert a (Domain r)"
    4.48    by blast
    4.49  
    4.50 -lemma Range_insert (* CANDIDATE [simp] *): "Range (insert (a, b) r) = insert b (Range r)"
    4.51 +lemma Range_insert [simp]: "Range (insert (a, b) r) = insert b (Range r)"
    4.52    by blast
    4.53  
    4.54  lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r"
     5.1 --- a/src/HOL/Set.thy	Sun Mar 11 22:06:13 2012 +0100
     5.2 +++ b/src/HOL/Set.thy	Mon Mar 12 15:11:24 2012 +0100
     5.3 @@ -124,7 +124,8 @@
     5.4  qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
     5.5    bot_set_def top_set_def uminus_set_def minus_set_def
     5.6    less_le_not_le inf_compl_bot sup_compl_top sup_inf_distrib1 diff_eq
     5.7 -  set_eqI fun_eq_iff)
     5.8 +  set_eqI fun_eq_iff
     5.9 +  del: inf_apply sup_apply bot_apply top_apply minus_apply uminus_apply)
    5.10  
    5.11  end
    5.12  
     6.1 --- a/src/HOL/Wellfounded.thy	Sun Mar 11 22:06:13 2012 +0100
     6.2 +++ b/src/HOL/Wellfounded.thy	Mon Mar 12 15:11:24 2012 +0100
     6.3 @@ -299,8 +299,7 @@
     6.4  lemma wfP_SUP:
     6.5    "\<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)"
     6.6    apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred])
     6.7 -  apply (simp_all add: inf_set_def)
     6.8 -  apply auto
     6.9 +  apply simp_all
    6.10    done
    6.11  
    6.12  lemma wf_Union: