marked candidates for rule declarations
authorhaftmann
Sun Feb 26 15:28:48 2012 +0100 (2012-02-26)
changeset 46689f559866a7aa2
parent 46675 f4ce220d2799
child 46690 07f9732804ad
marked candidates for rule declarations
src/HOL/Complete_Lattices.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Sat Feb 25 15:33:36 2012 +0100
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Sun Feb 26 15:28:48 2012 +0100
     1.3 @@ -582,14 +582,14 @@
     1.4  definition
     1.5    "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
     1.6  
     1.7 -lemma Inf_apply [code]:
     1.8 +lemma Inf_apply (* CANDIDATE [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 [code]:
    1.16 +lemma Sup_apply (* CANDIDATE [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 @@ -598,11 +598,11 @@
    1.21  
    1.22  end
    1.23  
    1.24 -lemma INF_apply:
    1.25 +lemma INF_apply (* CANDIDATE [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:
    1.30 +lemma SUP_apply (* CANDIDATE [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	Sat Feb 25 15:33:36 2012 +0100
     2.2 +++ b/src/HOL/Lattices.thy	Sun Feb 26 15:28:48 2012 +0100
     2.3 @@ -649,14 +649,14 @@
     2.4  definition
     2.5    "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
     2.6  
     2.7 -lemma inf_apply:
     2.8 +lemma inf_apply (* CANDIDATE [simp, 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:
    2.16 +lemma sup_apply (* CANDIDATE [simp, code] *):
    2.17    "(f \<squnion> g) x = f x \<squnion> g x"
    2.18    by (simp add: sup_fun_def)
    2.19  
    2.20 @@ -676,7 +676,7 @@
    2.21  definition
    2.22    fun_Compl_def: "- A = (\<lambda>x. - A x)"
    2.23  
    2.24 -lemma uminus_apply:
    2.25 +lemma uminus_apply (* CANDIDATE [simp, code] *):
    2.26    "(- A) x = - (A x)"
    2.27    by (simp add: fun_Compl_def)
    2.28  
    2.29 @@ -690,7 +690,7 @@
    2.30  definition
    2.31    fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
    2.32  
    2.33 -lemma minus_apply:
    2.34 +lemma minus_apply (* CANDIDATE [simp, 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	Sat Feb 25 15:33:36 2012 +0100
     3.2 +++ b/src/HOL/Orderings.thy	Sun Feb 26 15:28:48 2012 +0100
     3.3 @@ -1299,7 +1299,7 @@
     3.4  definition
     3.5    "\<bottom> = (\<lambda>x. \<bottom>)"
     3.6  
     3.7 -lemma bot_apply:
     3.8 +lemma bot_apply (* CANDIDATE [simp, 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:
    3.17 +lemma top_apply (* CANDIDATE [simp, code] *):
    3.18    "\<top> x = \<top>"
    3.19    by (simp add: top_fun_def)
    3.20  
     4.1 --- a/src/HOL/Relation.thy	Sat Feb 25 15:33:36 2012 +0100
     4.2 +++ b/src/HOL/Relation.thy	Sun Feb 26 15:28:48 2012 +0100
     4.3 @@ -25,7 +25,9 @@
     4.4  
     4.5  subsection {* 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 predicate2I [Pure.intro!, intro!]
    4.11  declare predicate2D [Pure.dest, dest]
    4.12  declare bot1E [elim!]
    4.13 @@ -70,11 +72,17 @@
    4.14  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)"
    4.15    by (simp add: subset_iff le_fun_def)
    4.16  
    4.17 -lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    4.18 +lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})"
    4.19 +  by (auto simp add: fun_eq_iff)
    4.20 +
    4.21 +lemma bot_empty_eq2 (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    4.22    by (auto simp add: fun_eq_iff)
    4.23  
    4.24 -lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    4.25 -  by (auto simp add: fun_eq_iff)
    4.26 +(* CANDIDATE lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
    4.27 +  by (auto simp add: fun_eq_iff) *)
    4.28 +
    4.29 +(* CANDIDATE lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
    4.30 +  by (auto simp add: fun_eq_iff) *)
    4.31  
    4.32  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)"
    4.33    by (simp add: inf_fun_def)
    4.34 @@ -88,10 +96,10 @@
    4.35  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)"
    4.36    by (simp add: sup_fun_def)
    4.37  
    4.38 -lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    4.39 +lemma INF_INT_eq (* CANDIDATE [pred_set_conv] *): "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    4.40    by (simp add: INF_apply fun_eq_iff)
    4.41  
    4.42 -lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i. r i))"
    4.43 +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))"
    4.44    by (simp add: INF_apply fun_eq_iff)
    4.45  
    4.46  lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
    4.47 @@ -946,3 +954,4 @@
    4.48    "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    4.49  
    4.50  end
    4.51 +