src/HOL/Relation.thy
changeset 46689 f559866a7aa2
parent 46664 1f6c140f9c72
child 46691 72d81e789106
     1.1 --- a/src/HOL/Relation.thy	Sat Feb 25 15:33:36 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Sun Feb 26 15:28:48 2012 +0100
     1.3 @@ -25,7 +25,9 @@
     1.4  
     1.5  subsection {* Classical rules for reasoning on predicates *}
     1.6  
     1.7 +(* CANDIDATE declare predicate1I [Pure.intro!, intro!] *)
     1.8  declare predicate1D [Pure.dest?, dest?]
     1.9 +(* CANDIDATE declare predicate1D [Pure.dest, dest] *)
    1.10  declare predicate2I [Pure.intro!, intro!]
    1.11  declare predicate2D [Pure.dest, dest]
    1.12  declare bot1E [elim!]
    1.13 @@ -70,11 +72,17 @@
    1.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)"
    1.15    by (simp add: subset_iff le_fun_def)
    1.16  
    1.17 -lemma bot_empty_eq: "\<bottom> = (\<lambda>x. x \<in> {})"
    1.18 +lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})"
    1.19 +  by (auto simp add: fun_eq_iff)
    1.20 +
    1.21 +lemma bot_empty_eq2 (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    1.22    by (auto simp add: fun_eq_iff)
    1.23  
    1.24 -lemma bot_empty_eq2: "\<bottom> = (\<lambda>x y. (x, y) \<in> {})"
    1.25 -  by (auto simp add: fun_eq_iff)
    1.26 +(* CANDIDATE lemma top_empty_eq [pred_set_conv]: "\<top> = (\<lambda>x. x \<in> UNIV)"
    1.27 +  by (auto simp add: fun_eq_iff) *)
    1.28 +
    1.29 +(* CANDIDATE lemma top_empty_eq2 [pred_set_conv]: "\<top> = (\<lambda>x y. (x, y) \<in> UNIV)"
    1.30 +  by (auto simp add: fun_eq_iff) *)
    1.31  
    1.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)"
    1.33    by (simp add: inf_fun_def)
    1.34 @@ -88,10 +96,10 @@
    1.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)"
    1.36    by (simp add: sup_fun_def)
    1.37  
    1.38 -lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    1.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))"
    1.40    by (simp add: INF_apply fun_eq_iff)
    1.41  
    1.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))"
    1.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))"
    1.44    by (simp add: INF_apply fun_eq_iff)
    1.45  
    1.46  lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
    1.47 @@ -946,3 +954,4 @@
    1.48    "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    1.49  
    1.50  end
    1.51 +