author paulson Wed Feb 26 10:44:16 2003 +0100 (2003-02-26) changeset 13830 7f8c1b533e8b parent 13829 af0218406395 child 13831 ab27b36aba99
some x-symbols and some new lemmas
 src/HOL/Relation.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Relation.thy	Tue Feb 25 19:08:15 2003 +0100
1.2 +++ b/src/HOL/Relation.thy	Wed Feb 26 10:44:16 2003 +0100
1.3 @@ -27,7 +27,7 @@
1.4    "Id == {p. EX x. p = (x,x)}"
1.5
1.6    diag  :: "'a set => ('a * 'a) set"  -- {* diagonal: identity over a set *}
1.7 -  "diag A == UN x:A. {(x,x)}"
1.8 +  "diag A == \<Union>x\<in>A. {(x,x)}"
1.9
1.10    Domain :: "('a * 'b) set => 'a set"
1.11    "Domain r == {x. EX y. (x,y):r}"
1.12 @@ -36,7 +36,7 @@
1.13    "Range r == Domain(r^-1)"
1.14
1.15    Field :: "('a * 'a) set => 'a set"
1.16 -  "Field r == Domain r Un Range r"
1.17 +  "Field r == Domain r \<union> Range r"
1.18
1.19    refl   :: "['a set, ('a * 'a) set] => bool"  -- {* reflexivity over a set *}
1.20    "refl A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
1.21 @@ -232,16 +232,16 @@
1.22  lemma Domain_diag [simp]: "Domain (diag A) = A"
1.23    by blast
1.24
1.25 -lemma Domain_Un_eq: "Domain(A Un B) = Domain(A) Un Domain(B)"
1.26 +lemma Domain_Un_eq: "Domain(A \<union> B) = Domain(A) \<union> Domain(B)"
1.27    by blast
1.28
1.29 -lemma Domain_Int_subset: "Domain(A Int B) \<subseteq> Domain(A) Int Domain(B)"
1.30 +lemma Domain_Int_subset: "Domain(A \<inter> B) \<subseteq> Domain(A) \<inter> Domain(B)"
1.31    by blast
1.32
1.33  lemma Domain_Diff_subset: "Domain(A) - Domain(B) \<subseteq> Domain(A - B)"
1.34    by blast
1.35
1.36 -lemma Domain_Union: "Domain (Union S) = (UN A:S. Domain A)"
1.37 +lemma Domain_Union: "Domain (Union S) = (\<Union>A\<in>S. Domain A)"
1.38    by blast
1.39
1.40  lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
1.41 @@ -271,16 +271,16 @@
1.42  lemma Range_diag [simp]: "Range (diag A) = A"
1.43    by auto
1.44
1.45 -lemma Range_Un_eq: "Range(A Un B) = Range(A) Un Range(B)"
1.46 +lemma Range_Un_eq: "Range(A \<union> B) = Range(A) \<union> Range(B)"
1.47    by blast
1.48
1.49 -lemma Range_Int_subset: "Range(A Int B) \<subseteq> Range(A) Int Range(B)"
1.50 +lemma Range_Int_subset: "Range(A \<inter> B) \<subseteq> Range(A) \<inter> Range(B)"
1.51    by blast
1.52
1.53  lemma Range_Diff_subset: "Range(A) - Range(B) \<subseteq> Range(A - B)"
1.54    by blast
1.55
1.56 -lemma Range_Union: "Range (Union S) = (UN A:S. Range A)"
1.57 +lemma Range_Union: "Range (Union S) = (\<Union>A\<in>S. Range A)"
1.58    by blast
1.59
1.60
1.61 @@ -312,13 +312,17 @@
1.62  lemma Image_Id [simp]: "Id `` A = A"
1.63    by blast
1.64
1.65 -lemma Image_diag [simp]: "diag A `` B = A Int B"
1.66 +lemma Image_diag [simp]: "diag A `` B = A \<inter> B"
1.67 +  by blast
1.68 +
1.69 +lemma Image_Int_subset: "R `` (A \<inter> B) \<subseteq> R `` A \<inter> R `` B"
1.70    by blast
1.71
1.72 -lemma Image_Int_subset: "R `` (A Int B) \<subseteq> R `` A Int R `` B"
1.73 -  by blast
1.74 +lemma Image_Int_eq:
1.75 +     "single_valued (converse R) ==> R `` (A \<inter> B) = R `` A \<inter> R `` B"
1.76 +  by (simp add: single_valued_def, blast)
1.77
1.78 -lemma Image_Un: "R `` (A Un B) = R `` A Un R `` B"
1.79 +lemma Image_Un: "R `` (A \<union> B) = R `` A \<union> R `` B"
1.80    by blast
1.81
1.82  lemma Un_Image: "(R \<union> S) `` A = R `` A \<union> S `` A"
1.83 @@ -327,19 +331,26 @@
1.84  lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
1.85    by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
1.86
1.87 -lemma Image_eq_UN: "r``B = (UN y: B. r``{y})"
1.88 +lemma Image_eq_UN: "r``B = (\<Union>y\<in> B. r``{y})"
1.89    -- {* NOT suitable for rewriting *}
1.90    by blast
1.91
1.92  lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)"
1.93    by blast
1.94
1.95 -lemma Image_UN: "(r `` (UNION A B)) = (UN x:A.(r `` (B x)))"
1.96 +lemma Image_UN: "(r `` (UNION A B)) = (\<Union>x\<in>A. r `` (B x))"
1.97 +  by blast
1.98 +
1.99 +lemma Image_INT_subset: "(r `` INTER A B) \<subseteq> (\<Inter>x\<in>A. r `` (B x))"
1.100    by blast
1.101
1.102 -lemma Image_INT_subset: "(r `` (INTER A B)) \<subseteq> (INT x:A.(r `` (B x)))"
1.103 -  -- {* Converse inclusion fails *}
1.104 -  by blast
1.105 +text{*Converse inclusion requires some assumptions*}
1.106 +lemma Image_INT_eq:
1.107 +     "[|single_valued (r\<inverse>); A\<noteq>{}|] ==> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
1.108 +apply (rule equalityI)
1.109 + apply (rule Image_INT_subset)
1.110 +apply  (simp add: single_valued_def, blast)
1.111 +done
1.112
1.113  lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
1.114    by blast
```