New theorems; tidied
authorpaulson
Tue Mar 03 15:12:25 1998 +0100 (1998-03-03)
changeset 467359d80bacee62
parent 4672 9d55bc687e1e
child 4674 248b876c2fa8
New theorems; tidied
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Tue Mar 03 15:11:26 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Tue Mar 03 15:12:25 1998 +0100
     1.3 @@ -8,11 +8,11 @@
     1.4  
     1.5  (** Identity relation **)
     1.6  
     1.7 -goalw Relation.thy [id_def] "(a,a) : id";  
     1.8 +goalw thy [id_def] "(a,a) : id";  
     1.9  by (Blast_tac 1);
    1.10  qed "idI";
    1.11  
    1.12 -val major::prems = goalw Relation.thy [id_def]
    1.13 +val major::prems = goalw thy [id_def]
    1.14      "[| p: id;  !!x.[| p = (x,x) |] ==> P  \
    1.15  \    |] ==>  P";  
    1.16  by (rtac (major RS CollectE) 1);
    1.17 @@ -20,7 +20,7 @@
    1.18  by (eresolve_tac prems 1);
    1.19  qed "idE";
    1.20  
    1.21 -goalw Relation.thy [id_def] "(a,b):id = (a=b)";
    1.22 +goalw thy [id_def] "(a,b):id = (a=b)";
    1.23  by (Blast_tac 1);
    1.24  qed "pair_in_id_conv";
    1.25  Addsimps [pair_in_id_conv];
    1.26 @@ -28,13 +28,13 @@
    1.27  
    1.28  (** Composition of two relations **)
    1.29  
    1.30 -goalw Relation.thy [comp_def]
    1.31 +goalw thy [comp_def]
    1.32      "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    1.33  by (Blast_tac 1);
    1.34  qed "compI";
    1.35  
    1.36  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    1.37 -val prems = goalw Relation.thy [comp_def]
    1.38 +val prems = goalw thy [comp_def]
    1.39      "[| xz : r O s;  \
    1.40  \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
    1.41  \    |] ==> P";
    1.42 @@ -43,7 +43,7 @@
    1.43       ORELSE ares_tac prems 1));
    1.44  qed "compE";
    1.45  
    1.46 -val prems = goal Relation.thy
    1.47 +val prems = goal thy
    1.48      "[| (a,c) : r O s;  \
    1.49  \       !!y. [| (a,y):s;  (y,c):r |] ==> P \
    1.50  \    |] ==> P";
    1.51 @@ -54,45 +54,55 @@
    1.52  AddIs [compI, idI];
    1.53  AddSEs [compE, idE];
    1.54  
    1.55 -goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    1.56 +goal thy "R O id = R";
    1.57 +by (Fast_tac 1);
    1.58 +qed "R_O_id";
    1.59 +
    1.60 +goal thy "id O R = R";
    1.61 +by (Fast_tac 1);
    1.62 +qed "id_O_R";
    1.63 +
    1.64 +Addsimps [R_O_id,id_O_R];
    1.65 +
    1.66 +goal thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    1.67  by (Blast_tac 1);
    1.68  qed "comp_mono";
    1.69  
    1.70 -goal Relation.thy
    1.71 +goal thy
    1.72      "!!r s. [| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
    1.73  by (Blast_tac 1);
    1.74  qed "comp_subset_Sigma";
    1.75  
    1.76  (** Natural deduction for trans(r) **)
    1.77  
    1.78 -val prems = goalw Relation.thy [trans_def]
    1.79 +val prems = goalw thy [trans_def]
    1.80      "(!! x y z. [| (x,y):r;  (y,z):r |] ==> (x,z):r) ==> trans(r)";
    1.81  by (REPEAT (ares_tac (prems@[allI,impI]) 1));
    1.82  qed "transI";
    1.83  
    1.84 -goalw Relation.thy [trans_def]
    1.85 +goalw thy [trans_def]
    1.86      "!!r. [| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
    1.87  by (Blast_tac 1);
    1.88  qed "transD";
    1.89  
    1.90  (** Natural deduction for r^-1 **)
    1.91  
    1.92 -goalw Relation.thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
    1.93 +goalw thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
    1.94  by (Simp_tac 1);
    1.95  qed "inverse_iff";
    1.96  
    1.97  AddIffs [inverse_iff];
    1.98  
    1.99 -goalw Relation.thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
   1.100 +goalw thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
   1.101  by (Simp_tac 1);
   1.102  qed "inverseI";
   1.103  
   1.104 -goalw Relation.thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
   1.105 +goalw thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
   1.106  by (Blast_tac 1);
   1.107  qed "inverseD";
   1.108  
   1.109  (*More general than inverseD, as it "splits" the member of the relation*)
   1.110 -qed_goalw "inverseE" Relation.thy [inverse_def]
   1.111 +qed_goalw "inverseE" thy [inverse_def]
   1.112      "[| yx : r^-1;  \
   1.113  \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
   1.114  \    |] ==> P"
   1.115 @@ -103,30 +113,30 @@
   1.116  
   1.117  AddSEs [inverseE];
   1.118  
   1.119 -goalw Relation.thy [inverse_def] "(r^-1)^-1 = r";
   1.120 +goalw thy [inverse_def] "(r^-1)^-1 = r";
   1.121  by (Blast_tac 1);
   1.122  qed "inverse_inverse";
   1.123  Addsimps [inverse_inverse];
   1.124  
   1.125 -goal Relation.thy "(r O s)^-1 = s^-1 O r^-1";
   1.126 +goal thy "(r O s)^-1 = s^-1 O r^-1";
   1.127  by (Blast_tac 1);
   1.128  qed "inverse_comp";
   1.129  
   1.130 -goal Relation.thy "id^-1 = id";
   1.131 +goal thy "id^-1 = id";
   1.132  by (Blast_tac 1);
   1.133  qed "inverse_id";
   1.134  Addsimps [inverse_id];
   1.135  
   1.136  (** Domain **)
   1.137  
   1.138 -qed_goalw "Domain_iff" Relation.thy [Domain_def]
   1.139 +qed_goalw "Domain_iff" thy [Domain_def]
   1.140      "a: Domain(r) = (EX y. (a,y): r)"
   1.141   (fn _=> [ (Blast_tac 1) ]);
   1.142  
   1.143 -qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)"
   1.144 +qed_goal "DomainI" thy "!!a b r. (a,b): r ==> a: Domain(r)"
   1.145   (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
   1.146  
   1.147 -qed_goal "DomainE" Relation.thy
   1.148 +qed_goal "DomainE" thy
   1.149      "[| a : Domain(r);  !!y. (a,y): r ==> P |] ==> P"
   1.150   (fn prems=>
   1.151    [ (rtac (Domain_iff RS iffD1 RS exE) 1),
   1.152 @@ -142,10 +152,10 @@
   1.153  
   1.154  (** Range **)
   1.155  
   1.156 -qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
   1.157 +qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
   1.158   (fn _ => [ (etac (inverseI RS DomainI) 1) ]);
   1.159  
   1.160 -qed_goalw "RangeE" Relation.thy [Range_def]
   1.161 +qed_goalw "RangeE" thy [Range_def]
   1.162      "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P"
   1.163   (fn major::prems=>
   1.164    [ (rtac (major RS DomainE) 1),
   1.165 @@ -162,20 +172,26 @@
   1.166  
   1.167  (*** Image of a set under a relation ***)
   1.168  
   1.169 -qed_goalw "Image_iff" Relation.thy [Image_def]
   1.170 +qed_goalw "Image_iff" thy [Image_def]
   1.171      "b : r^^A = (? x:A. (x,b):r)"
   1.172   (fn _ => [ Blast_tac 1 ]);
   1.173  
   1.174 -qed_goal "Image_singleton_iff" Relation.thy
   1.175 +qed_goalw "Image_singleton" thy [Image_def]
   1.176 +    "r^^{a} = {b. (a,b):r}"
   1.177 + (fn _ => [ Blast_tac 1 ]);
   1.178 +
   1.179 +qed_goal "Image_singleton_iff" thy
   1.180      "(b : r^^{a}) = ((a,b):r)"
   1.181   (fn _ => [ rtac (Image_iff RS trans) 1,
   1.182              Blast_tac 1 ]);
   1.183  
   1.184 -qed_goalw "ImageI" Relation.thy [Image_def]
   1.185 +AddIffs [Image_singleton_iff];
   1.186 +
   1.187 +qed_goalw "ImageI" thy [Image_def]
   1.188      "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
   1.189   (fn _ => [ (Blast_tac 1)]);
   1.190  
   1.191 -qed_goalw "ImageE" Relation.thy [Image_def]
   1.192 +qed_goalw "ImageE" thy [Image_def]
   1.193      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
   1.194   (fn major::prems=>
   1.195    [ (rtac (major RS CollectE) 1),
   1.196 @@ -187,7 +203,7 @@
   1.197  AddSEs [ImageE];
   1.198  
   1.199  
   1.200 -qed_goal "Image_empty" Relation.thy
   1.201 +qed_goal "Image_empty" thy
   1.202      "R^^{} = {}"
   1.203   (fn _ => [ Blast_tac 1 ]);
   1.204  
   1.205 @@ -199,27 +215,21 @@
   1.206  
   1.207  Addsimps [Image_id];
   1.208  
   1.209 -qed_goal "Image_Int_subset" Relation.thy
   1.210 +qed_goal "Image_Int_subset" thy
   1.211      "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
   1.212   (fn _ => [ Blast_tac 1 ]);
   1.213  
   1.214 -qed_goal "Image_Un" Relation.thy
   1.215 +qed_goal "Image_Un" thy
   1.216      "R ^^ (A Un B) = R ^^ A Un R ^^ B"
   1.217   (fn _ => [ Blast_tac 1 ]);
   1.218  
   1.219  
   1.220 -qed_goal "Image_subset" Relation.thy
   1.221 +qed_goal "Image_subset" thy
   1.222      "!!A B r. r <= A Times B ==> r^^C <= B"
   1.223   (fn _ =>
   1.224    [ (rtac subsetI 1),
   1.225      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
   1.226  
   1.227 -goal Relation.thy "R O id = R";
   1.228 -by (Fast_tac 1);
   1.229 -qed "R_O_id";
   1.230 -
   1.231 -goal Relation.thy "id O R = R";
   1.232 -by (Fast_tac 1);
   1.233 -qed "id_O_R";
   1.234 -
   1.235 -Addsimps [R_O_id,id_O_R];
   1.236 +goal thy "f-``(r^-1 ^^ {x}) = (UN y: r^-1 ^^ {x}. f-``{y})";
   1.237 +by (Blast_tac 1);
   1.238 +qed "vimage_inverse_Image";