author haftmann Wed Mar 07 21:34:36 2012 +0100 (2012-03-07) changeset 46833 85619a872ab5 parent 46828 b1d15637381a child 46834 a5fa1dc55945
tuned syntax; more candidates
 src/HOL/Relation.thy file | annotate | diff | revisions
```     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.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
```