fixed document;
authorwenzelm
Thu Feb 21 11:05:20 2002 +0100 (2002-02-21)
changeset 129135ac498bffb6b
parent 12912 0e144958cf27
child 12914 71015f46b3c1
fixed document;
tuned;
src/HOL/Relation.thy
     1.1 --- a/src/HOL/Relation.thy	Thu Feb 21 10:25:00 2002 +0100
     1.2 +++ b/src/HOL/Relation.thy	Thu Feb 21 11:05:20 2002 +0100
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  theory Relation = Product_Type:
     1.6  
     1.7 +subsection {* Definitions *}
     1.8 +
     1.9  constdefs
    1.10    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_^-1)" [1000] 999)
    1.11    "r^-1 == {(y, x). (x, y) : r}"
    1.12 @@ -16,46 +18,46 @@
    1.13  
    1.14  constdefs
    1.15    rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
    1.16 -    "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    1.17 +  "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}"
    1.18 +
    1.19 +  fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
    1.20 +  "fun_rel_comp f R == {g. ALL x. (f x, g x) : R}"
    1.21  
    1.22    Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
    1.23 -    "r `` s == {y. ? x:s. (x,y):r}"
    1.24 +  "r `` s == {y. EX x:s. (x,y):r}"
    1.25  
    1.26    Id    :: "('a * 'a) set"  -- {* the identity relation *}
    1.27 -    "Id == {p. ? x. p = (x,x)}"
    1.28 +  "Id == {p. EX x. p = (x,x)}"
    1.29  
    1.30    diag  :: "'a set => ('a * 'a) set"  -- {* diagonal: identity over a set *}
    1.31 -    "diag(A) == UN x:A. {(x,x)}"
    1.32 -  
    1.33 +  "diag A == UN x:A. {(x,x)}"
    1.34 +
    1.35    Domain :: "('a * 'b) set => 'a set"
    1.36 -    "Domain(r) == {x. ? y. (x,y):r}"
    1.37 +  "Domain r == {x. EX y. (x,y):r}"
    1.38  
    1.39    Range  :: "('a * 'b) set => 'b set"
    1.40 -    "Range(r) == Domain(r^-1)"
    1.41 +  "Range r == Domain(r^-1)"
    1.42  
    1.43    Field :: "('a * 'a) set => 'a set"
    1.44 -    "Field r == Domain r Un Range r"
    1.45 +  "Field r == Domain r Un Range r"
    1.46  
    1.47    refl   :: "['a set, ('a * 'a) set] => bool"  -- {* reflexivity over a set *}
    1.48 -    "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)"
    1.49 +  "refl A r == r \<subseteq> A \<times> A & (ALL x: A. (x,x) : r)"
    1.50  
    1.51    sym    :: "('a * 'a) set => bool"  -- {* symmetry predicate *}
    1.52 -    "sym(r) == ALL x y. (x,y): r --> (y,x): r"
    1.53 +  "sym r == ALL x y. (x,y): r --> (y,x): r"
    1.54  
    1.55    antisym:: "('a * 'a) set => bool"  -- {* antisymmetry predicate *}
    1.56 -    "antisym(r) == ALL x y. (x,y):r --> (y,x):r --> x=y"
    1.57 +  "antisym r == ALL x y. (x,y):r --> (y,x):r --> x=y"
    1.58  
    1.59    trans  :: "('a * 'a) set => bool"  -- {* transitivity predicate *}
    1.60 -    "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
    1.61 +  "trans r == (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)"
    1.62  
    1.63    single_valued :: "('a * 'b) set => bool"
    1.64 -    "single_valued r == !x y. (x,y):r --> (!z. (x,z):r --> y=z)"
    1.65 -
    1.66 -  fun_rel_comp :: "['a => 'b, ('b * 'c) set] => ('a => 'c) set"
    1.67 -    "fun_rel_comp f R == {g. !x. (f x, g x) : R}"
    1.68 +  "single_valued r == ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z)"
    1.69  
    1.70    inv_image :: "('b * 'b) set => ('a => 'b) => ('a * 'a) set"
    1.71 -    "inv_image r f == {(x,y). (f(x), f(y)) : r}"
    1.72 +  "inv_image r f == {(x, y). (f x, f y) : r}"
    1.73  
    1.74  syntax
    1.75    reflexive :: "('a * 'a) set => bool"  -- {* reflexivity over a type *}
    1.76 @@ -63,7 +65,7 @@
    1.77    "reflexive" == "refl UNIV"
    1.78  
    1.79  
    1.80 -subsection {* Identity relation *}
    1.81 +subsection {* The identity relation *}
    1.82  
    1.83  lemma IdI [intro]: "(a, a) : Id"
    1.84    by (simp add: Id_def)
    1.85 @@ -85,7 +87,7 @@
    1.86    by (simp add: trans_def)
    1.87  
    1.88  
    1.89 -subsection {* Diagonal relation: identity restricted to some set *}
    1.90 +subsection {* Diagonal: identity over a set *}
    1.91  
    1.92  lemma diag_eqI: "a = b ==> a : A ==> (a, b) : diag A"
    1.93    by (simp add: diag_def)
    1.94 @@ -95,23 +97,23 @@
    1.95  
    1.96  lemma diagE [elim!]:
    1.97    "c : diag A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P"
    1.98 -  -- {* The general elimination rule *}
    1.99 +  -- {* The general elimination rule. *}
   1.100    by (unfold diag_def) (rules elim!: UN_E singletonE)
   1.101  
   1.102  lemma diag_iff: "((x, y) : diag A) = (x = y & x : A)"
   1.103    by blast
   1.104  
   1.105 -lemma diag_subset_Times: "diag A <= A <*> A"
   1.106 +lemma diag_subset_Times: "diag A \<subseteq> A \<times> A"
   1.107    by blast
   1.108  
   1.109  
   1.110  subsection {* Composition of two relations *}
   1.111  
   1.112 -lemma rel_compI [intro]: 
   1.113 +lemma rel_compI [intro]:
   1.114    "(a, b) : s ==> (b, c) : r ==> (a, c) : r O s"
   1.115    by (unfold rel_comp_def) blast
   1.116  
   1.117 -lemma rel_compE [elim!]: "xz : r O s ==>   
   1.118 +lemma rel_compE [elim!]: "xz : r O s ==>
   1.119    (!!x y z. xz = (x, z) ==> (x, y) : s ==> (y, z) : r  ==> P) ==> P"
   1.120    by (unfold rel_comp_def) (rules elim!: CollectE splitE exE conjE)
   1.121  
   1.122 @@ -128,25 +130,41 @@
   1.123  lemma O_assoc: "(R O S) O T = R O (S O T)"
   1.124    by blast
   1.125  
   1.126 -lemma trans_O_subset: "trans r ==> r O r <= r"
   1.127 +lemma trans_O_subset: "trans r ==> r O r \<subseteq> r"
   1.128    by (unfold trans_def) blast
   1.129  
   1.130 -lemma rel_comp_mono: "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)"
   1.131 +lemma rel_comp_mono: "r' \<subseteq> r ==> s' \<subseteq> s ==> (r' O s') \<subseteq> (r O s)"
   1.132    by blast
   1.133  
   1.134  lemma rel_comp_subset_Sigma:
   1.135 -  "[| s <= A <*> B;  r <= B <*> C |] ==> (r O s) <= A <*> C"
   1.136 +    "s \<subseteq> A \<times> B ==> r \<subseteq> B \<times> C ==> (r O s) \<subseteq> A \<times> C"
   1.137    by blast
   1.138  
   1.139 -subsection {* Natural deduction for refl(r) *}
   1.140 +
   1.141 +subsection {* Composition of function and relation *}
   1.142 +
   1.143 +lemma fun_rel_comp_mono: "A \<subseteq> B ==> fun_rel_comp f A \<subseteq> fun_rel_comp f B"
   1.144 +  by (unfold fun_rel_comp_def) fast
   1.145  
   1.146 -lemma reflI: "r <= A <*> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
   1.147 +lemma fun_rel_comp_unique:
   1.148 +  "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R"
   1.149 +  apply (unfold fun_rel_comp_def)
   1.150 +  apply (rule_tac a = "%x. THE y. (f x, y) : R" in ex1I)
   1.151 +  apply (fast dest!: theI')
   1.152 +  apply (fast intro: ext the1_equality [symmetric])
   1.153 +  done
   1.154 +
   1.155 +
   1.156 +subsection {* Reflexivity *}
   1.157 +
   1.158 +lemma reflI: "r \<subseteq> A \<times> A ==> (!!x. x : A ==> (x, x) : r) ==> refl A r"
   1.159    by (unfold refl_def) (rules intro!: ballI)
   1.160  
   1.161  lemma reflD: "refl A r ==> a : A ==> (a, a) : r"
   1.162    by (unfold refl_def) blast
   1.163  
   1.164 -subsection {* Natural deduction for antisym(r) *}
   1.165 +
   1.166 +subsection {* Antisymmetry *}
   1.167  
   1.168  lemma antisymI:
   1.169    "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r"
   1.170 @@ -155,7 +173,8 @@
   1.171  lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b"
   1.172    by (unfold antisym_def) rules
   1.173  
   1.174 -subsection {* Natural deduction for trans(r) *}
   1.175 +
   1.176 +subsection {* Transitivity *}
   1.177  
   1.178  lemma transI:
   1.179    "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
   1.180 @@ -164,21 +183,21 @@
   1.181  lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r"
   1.182    by (unfold trans_def) rules
   1.183  
   1.184 -subsection {* Natural deduction for r^-1 *}
   1.185  
   1.186 -lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a):r)"
   1.187 +subsection {* Converse *}
   1.188 +
   1.189 +lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)"
   1.190    by (simp add: converse_def)
   1.191  
   1.192 -lemma converseI: "(a,b):r ==> (b,a): r^-1"
   1.193 +lemma converseI: "(a, b) : r ==> (b, a) : r^-1"
   1.194    by (simp add: converse_def)
   1.195  
   1.196 -lemma converseD: "(a,b) : r^-1 ==> (b,a) : r"
   1.197 +lemma converseD: "(a,b) : r^-1 ==> (b, a) : r"
   1.198    by (simp add: converse_def)
   1.199  
   1.200 -(*More general than converseD, as it "splits" the member of the relation*)
   1.201 -
   1.202  lemma converseE [elim!]:
   1.203    "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P"
   1.204 +    -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *}
   1.205    by (unfold converse_def) (rules elim!: CollectE splitE bexE)
   1.206  
   1.207  lemma converse_converse [simp]: "(r^-1)^-1 = r"
   1.208 @@ -190,7 +209,7 @@
   1.209  lemma converse_Id [simp]: "Id^-1 = Id"
   1.210    by blast
   1.211  
   1.212 -lemma converse_diag [simp]: "(diag A) ^-1 = diag A"
   1.213 +lemma converse_diag [simp]: "(diag A)^-1 = diag A"
   1.214    by blast
   1.215  
   1.216  lemma refl_converse: "refl A r ==> refl A (converse r)"
   1.217 @@ -202,6 +221,7 @@
   1.218  lemma trans_converse: "trans (converse r) = trans r"
   1.219    by (unfold trans_def) blast
   1.220  
   1.221 +
   1.222  subsection {* Domain *}
   1.223  
   1.224  lemma Domain_iff: "(a : Domain r) = (EX y. (a, y) : r)"
   1.225 @@ -229,16 +249,16 @@
   1.226  lemma Domain_Un_eq: "Domain(A Un B) = Domain(A) Un Domain(B)"
   1.227    by blast
   1.228  
   1.229 -lemma Domain_Int_subset: "Domain(A Int B) <= Domain(A) Int Domain(B)"
   1.230 +lemma Domain_Int_subset: "Domain(A Int B) \<subseteq> Domain(A) Int Domain(B)"
   1.231    by blast
   1.232  
   1.233 -lemma Domain_Diff_subset: "Domain(A) - Domain(B) <= Domain(A - B)"
   1.234 +lemma Domain_Diff_subset: "Domain(A) - Domain(B) \<subseteq> Domain(A - B)"
   1.235    by blast
   1.236  
   1.237  lemma Domain_Union: "Domain (Union S) = (UN A:S. Domain A)"
   1.238    by blast
   1.239  
   1.240 -lemma Domain_mono: "r <= s ==> Domain r <= Domain s"
   1.241 +lemma Domain_mono: "r \<subseteq> s ==> Domain r \<subseteq> Domain s"
   1.242    by blast
   1.243  
   1.244  
   1.245 @@ -268,10 +288,10 @@
   1.246  lemma Range_Un_eq: "Range(A Un B) = Range(A) Un Range(B)"
   1.247    by blast
   1.248  
   1.249 -lemma Range_Int_subset: "Range(A Int B) <= Range(A) Int Range(B)"
   1.250 +lemma Range_Int_subset: "Range(A Int B) \<subseteq> Range(A) Int Range(B)"
   1.251    by blast
   1.252  
   1.253 -lemma Range_Diff_subset: "Range(A) - Range(B) <= Range(A - B)"
   1.254 +lemma Range_Diff_subset: "Range(A) - Range(B) \<subseteq> Range(A - B)"
   1.255    by blast
   1.256  
   1.257  lemma Range_Union: "Range (Union S) = (UN A:S. Range A)"
   1.258 @@ -282,20 +302,20 @@
   1.259  
   1.260  ML {* overload_1st_set "Relation.Image" *}
   1.261  
   1.262 -lemma Image_iff: "(b : r``A) = (EX x:A. (x,b):r)"
   1.263 +lemma Image_iff: "(b : r``A) = (EX x:A. (x, b) : r)"
   1.264    by (simp add: Image_def)
   1.265  
   1.266 -lemma Image_singleton: "r``{a} = {b. (a,b):r}"
   1.267 +lemma Image_singleton: "r``{a} = {b. (a, b) : r}"
   1.268    by (simp add: Image_def)
   1.269  
   1.270 -lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a,b):r)"
   1.271 +lemma Image_singleton_iff [iff]: "(b : r``{a}) = ((a, b) : r)"
   1.272    by (rule Image_iff [THEN trans]) simp
   1.273  
   1.274 -lemma ImageI [intro]: "[| (a,b): r;  a:A |] ==> b : r``A"
   1.275 +lemma ImageI [intro]: "(a, b) : r ==> a : A ==> b : r``A"
   1.276    by (unfold Image_def) blast
   1.277  
   1.278  lemma ImageE [elim!]:
   1.279 -  "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
   1.280 +    "b : r `` A ==> (!!x. (x, b) : r ==> x : A ==> P) ==> P"
   1.281    by (unfold Image_def) (rules elim!: CollectE bexE)
   1.282  
   1.283  lemma rev_ImageI: "a : A ==> (a, b) : r ==> b : r `` A"
   1.284 @@ -311,35 +331,36 @@
   1.285  lemma Image_diag [simp]: "diag A `` B = A Int B"
   1.286    by blast
   1.287  
   1.288 -lemma Image_Int_subset: "R `` (A Int B) <= R `` A Int R `` B"
   1.289 +lemma Image_Int_subset: "R `` (A Int B) \<subseteq> R `` A Int R `` B"
   1.290    by blast
   1.291  
   1.292  lemma Image_Un: "R `` (A Un B) = R `` A Un R `` B"
   1.293    by blast
   1.294  
   1.295 -lemma Image_subset: "r <= A <*> B ==> r``C <= B"
   1.296 +lemma Image_subset: "r \<subseteq> A \<times> B ==> r``C \<subseteq> B"
   1.297    by (rules intro!: subsetI elim!: ImageE dest!: subsetD SigmaD2)
   1.298  
   1.299  lemma Image_eq_UN: "r``B = (UN y: B. r``{y})"
   1.300    -- {* NOT suitable for rewriting *}
   1.301    by blast
   1.302  
   1.303 -lemma Image_mono: "[| r'<=r; A'<=A |] ==> (r' `` A') <= (r `` A)"
   1.304 +lemma Image_mono: "r' \<subseteq> r ==> A' \<subseteq> A ==> (r' `` A') \<subseteq> (r `` A)"
   1.305    by blast
   1.306  
   1.307  lemma Image_UN: "(r `` (UNION A B)) = (UN x:A.(r `` (B x)))"
   1.308    by blast
   1.309  
   1.310 -lemma Image_INT_subset: "(r `` (INTER A B)) <= (INT x:A.(r `` (B x)))"
   1.311 +lemma Image_INT_subset: "(r `` (INTER A B)) \<subseteq> (INT x:A.(r `` (B x)))"
   1.312    -- {* Converse inclusion fails *}
   1.313    by blast
   1.314  
   1.315 -lemma Image_subset_eq: "(r``A <= B) = (A <= - ((r^-1) `` (-B)))"
   1.316 +lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"
   1.317    by blast
   1.318  
   1.319 -subsection "single_valued"
   1.320  
   1.321 -lemma single_valuedI: 
   1.322 +subsection {* Single valued relations *}
   1.323 +
   1.324 +lemma single_valuedI:
   1.325    "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r"
   1.326    by (unfold single_valued_def)
   1.327  
   1.328 @@ -360,24 +381,9 @@
   1.329    by auto
   1.330  
   1.331  
   1.332 -subsection {* Composition of function and relation *}
   1.333 -
   1.334 -lemma fun_rel_comp_mono: "A <= B ==> fun_rel_comp f A <= fun_rel_comp f B"
   1.335 -  by (unfold fun_rel_comp_def) fast
   1.336 +subsection {* Inverse image *}
   1.337  
   1.338 -lemma fun_rel_comp_unique: 
   1.339 -  "ALL x. EX! y. (f x, y) : R ==> EX! g. g : fun_rel_comp f R"
   1.340 -  apply (unfold fun_rel_comp_def)
   1.341 -  apply (rule_tac a = "%x. THE y. (f x, y) : R" in ex1I)
   1.342 -  apply (fast dest!: theI')
   1.343 -  apply (fast intro: ext the1_equality [symmetric])
   1.344 -  done
   1.345 -
   1.346 -
   1.347 -subsection "inverse image"
   1.348 -
   1.349 -lemma trans_inv_image: 
   1.350 -  "trans r ==> trans (inv_image r f)"
   1.351 +lemma trans_inv_image: "trans r ==> trans (inv_image r f)"
   1.352    apply (unfold trans_def inv_image_def)
   1.353    apply (simp (no_asm))
   1.354    apply blast