src/HOL/Relation.thy
changeset 46884 154dc6ec0041
parent 46883 eec472dae593
child 46981 d54cea5b64e4
     1.1 --- a/src/HOL/Relation.thy	Mon Mar 12 15:12:22 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Mar 12 21:41:11 2012 +0100
     1.3 @@ -96,40 +96,40 @@
     1.4    by (simp add: sup_fun_def)
     1.5  
     1.6  lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
     1.7 -  by (simp add: fun_eq_iff Inf_apply)
     1.8 +  by (simp add: fun_eq_iff)
     1.9  
    1.10  lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
    1.11 -  by (simp add: fun_eq_iff INF_apply)
    1.12 +  by (simp add: fun_eq_iff)
    1.13  
    1.14  lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)"
    1.15 -  by (simp add: fun_eq_iff Inf_apply INF_apply)
    1.16 +  by (simp add: fun_eq_iff)
    1.17  
    1.18  lemma INF_Int_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Inter>S)"
    1.19 -  by (simp add: fun_eq_iff INF_apply)
    1.20 +  by (simp add: fun_eq_iff)
    1.21  
    1.22  lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)"
    1.23 -  by (simp add: fun_eq_iff Sup_apply)
    1.24 +  by (simp add: fun_eq_iff)
    1.25  
    1.26  lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
    1.27 -  by (simp add: fun_eq_iff SUP_apply)
    1.28 +  by (simp add: fun_eq_iff)
    1.29  
    1.30  lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)"
    1.31 -  by (simp add: fun_eq_iff Sup_apply SUP_apply)
    1.32 +  by (simp add: fun_eq_iff)
    1.33  
    1.34  lemma SUP_Sup_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> i)) = (\<lambda>x y. (x, y) \<in> \<Union>S)"
    1.35 -  by (simp add: fun_eq_iff SUP_apply)
    1.36 +  by (simp add: fun_eq_iff)
    1.37  
    1.38  lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i. r i))"
    1.39 -  by (simp add: INF_apply fun_eq_iff)
    1.40 +  by (simp add: fun_eq_iff)
    1.41  
    1.42  lemma INF_INT_eq2 [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Inter>i\<in>S. r i))"
    1.43 -  by (simp add: INF_apply fun_eq_iff)
    1.44 +  by (simp add: 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 -  by (simp add: SUP_apply fun_eq_iff)
    1.48 +  by (simp add: fun_eq_iff)
    1.49  
    1.50  lemma SUP_UN_eq2 [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i\<in>S. r i))"
    1.51 -  by (simp add: SUP_apply fun_eq_iff)
    1.52 +  by (simp add: fun_eq_iff)
    1.53  
    1.54  
    1.55  
    1.56 @@ -818,7 +818,7 @@
    1.57    by blast
    1.58  
    1.59  lemma Field_insert [simp]: "Field (insert (a, b) r) = {a, b} \<union> Field r"
    1.60 -  by (auto simp add: Field_def Domain_insert Range_insert)
    1.61 +  by (auto simp add: Field_def)
    1.62  
    1.63  lemma Domain_iff: "a \<in> Domain r \<longleftrightarrow> (\<exists>y. (a, y) \<in> r)"
    1.64    by blast
    1.65 @@ -884,10 +884,10 @@
    1.66    by auto
    1.67  
    1.68  lemma finite_Domain: "finite r \<Longrightarrow> finite (Domain r)"
    1.69 -  by (induct set: finite) (auto simp add: Domain_insert)
    1.70 +  by (induct set: finite) auto
    1.71  
    1.72  lemma finite_Range: "finite r \<Longrightarrow> finite (Range r)"
    1.73 -  by (induct set: finite) (auto simp add: Range_insert)
    1.74 +  by (induct set: finite) auto
    1.75  
    1.76  lemma finite_Field: "finite r \<Longrightarrow> finite (Field r)"
    1.77    by (simp add: Field_def finite_Domain finite_Range)