some x-symbols and some new lemmas
authorpaulson
Wed Feb 26 10:44:16 2003 +0100 (2003-02-26)
changeset 138307f8c1b533e8b
parent 13829 af0218406395
child 13831 ab27b36aba99
some x-symbols and some new lemmas
src/HOL/Relation.thy
     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