tuned syntax; more candidates
authorhaftmann
Wed Mar 07 21:34:36 2012 +0100 (2012-03-07)
changeset 4683385619a872ab5
parent 46828 b1d15637381a
child 46834 a5fa1dc55945
tuned syntax; more candidates
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Wed Mar 07 16:13:49 2012 +0100
     1.2 +++ b/src/HOL/Relation.thy	Wed Mar 07 21:34:36 2012 +0100
     1.3 @@ -60,16 +60,16 @@
     1.4  
     1.5  subsubsection {* Conversions between set and predicate relations *}
     1.6  
     1.7 -lemma pred_equals_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R = S)"
     1.8 +lemma pred_equals_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S) \<longleftrightarrow> R = S"
     1.9    by (simp add: set_eq_iff fun_eq_iff)
    1.10  
    1.11 -lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) \<longleftrightarrow> (R = S)"
    1.12 +lemma pred_equals_eq2 [pred_set_conv]: "(\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S) \<longleftrightarrow> R = S"
    1.13    by (simp add: set_eq_iff fun_eq_iff)
    1.14  
    1.15 -lemma pred_subset_eq [pred_set_conv]: "((\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S)) \<longleftrightarrow> (R \<subseteq> S)"
    1.16 +lemma pred_subset_eq [pred_set_conv]: "(\<lambda>x. x \<in> R) \<le> (\<lambda>x. x \<in> S) \<longleftrightarrow> R \<subseteq> S"
    1.17    by (simp add: subset_iff le_fun_def)
    1.18  
    1.19 -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.20 +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.21    by (simp add: subset_iff le_fun_def)
    1.22  
    1.23  lemma bot_empty_eq (* CANDIDATE [pred_set_conv] *): "\<bottom> = (\<lambda>x. x \<in> {})"
    1.24 @@ -96,12 +96,54 @@
    1.25  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.26    by (simp add: sup_fun_def)
    1.27  
    1.28 +lemma Inf_INT_eq [pred_set_conv]: "\<Sqinter>S = (\<lambda>x. x \<in> INTER S Collect)"
    1.29 +  by (simp add: fun_eq_iff Inf_apply)
    1.30 +
    1.31 +(* CANDIDATE
    1.32 +lemma INF_Int_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Inter>S)"
    1.33 +  by (simp add: fun_eq_iff INF_apply)
    1.34 +
    1.35 +lemma Inf_INT_eq2 [pred_set_conv]: "\<Sqinter>S = (\<lambda>x y. (x, y) \<in> INTER (prod_case ` S) Collect)"
    1.36 +  by (simp add: fun_eq_iff Inf_apply INF_apply)
    1.37 +
    1.38 +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.39 +  by (simp add: fun_eq_iff INF_apply)
    1.40 +
    1.41 +lemma Sup_SUP_eq [pred_set_conv]: "\<Squnion>S = (\<lambda>x. x \<in> UNION S Collect)"
    1.42 +  by (simp add: fun_eq_iff Sup_apply)
    1.43 +
    1.44 +lemma SUP_Sup_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> i)) = (\<lambda>x. x \<in> \<Union>S)"
    1.45 +  by (simp add: fun_eq_iff SUP_apply)
    1.46 +
    1.47 +lemma Sup_SUP_eq2 [pred_set_conv]: "\<Squnion>S = (\<lambda>x y. (x, y) \<in> UNION (prod_case ` S) Collect)"
    1.48 +  by (simp add: fun_eq_iff Sup_apply SUP_apply)
    1.49 +
    1.50 +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.51 +  by (simp add: fun_eq_iff SUP_apply)
    1.52 +*)
    1.53 +
    1.54 +(* CANDIDATE prefer those generalized versions:
    1.55 +lemma INF_INT_eq [pred_set_conv]: "(\<Sqinter>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Inter>i\<in>S. r i))"
    1.56 +  by (simp add: INF_apply fun_eq_iff)
    1.57 +
    1.58 +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.59 +  by (simp add: INF_apply fun_eq_iff)
    1.60 +*)
    1.61 +
    1.62  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.63    by (simp add: INF_apply fun_eq_iff)
    1.64  
    1.65  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.66    by (simp add: INF_apply fun_eq_iff)
    1.67  
    1.68 +(* CANDIDATE prefer those generalized versions:
    1.69 +lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i\<in>S. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i\<in>S. r i))"
    1.70 +  by (simp add: SUP_apply fun_eq_iff)
    1.71 +
    1.72 +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.73 +  by (simp add: SUP_apply fun_eq_iff)
    1.74 +*)
    1.75 +
    1.76  lemma SUP_UN_eq [pred_set_conv]: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
    1.77    by (simp add: SUP_apply fun_eq_iff)
    1.78