src/HOL/Relation.ML
changeset 1985 84cf16192e03
parent 1842 a9c36056d320
child 2031 03a843f0f447
     1.1 --- a/src/HOL/Relation.ML	Thu Sep 12 10:36:51 1996 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Sep 12 10:40:05 1996 +0200
     1.3 @@ -1,21 +1,15 @@
     1.4  (*  Title:      Relation.ML
     1.5      ID:         $Id$
     1.6 -    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
     1.7 -                Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 -    Copyright   1994 Universita' di Firenze
     1.9 -    Copyright   1993  University of Cambridge
    1.10 +    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
    1.11 +    Copyright   1996  University of Cambridge
    1.12  *)
    1.13  
    1.14 -val RSLIST = curry (op MRS);
    1.15 -
    1.16  open Relation;
    1.17  
    1.18  (** Identity relation **)
    1.19  
    1.20  goalw Relation.thy [id_def] "(a,a) : id";  
    1.21 -by (rtac CollectI 1);
    1.22 -by (rtac exI 1);
    1.23 -by (rtac refl 1);
    1.24 +by (Fast_tac 1);
    1.25  qed "idI";
    1.26  
    1.27  val major::prems = goalw Relation.thy [id_def]
    1.28 @@ -34,9 +28,9 @@
    1.29  
    1.30  (** Composition of two relations **)
    1.31  
    1.32 -val prems = goalw Relation.thy [comp_def]
    1.33 -    "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    1.34 -by (fast_tac (!claset addIs prems) 1);
    1.35 +goalw Relation.thy [comp_def]
    1.36 +    "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    1.37 +by (Fast_tac 1);
    1.38  qed "compI";
    1.39  
    1.40  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    1.41 @@ -45,7 +39,8 @@
    1.42  \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
    1.43  \    |] ==> P";
    1.44  by (cut_facts_tac prems 1);
    1.45 -by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 ORELSE ares_tac prems 1));
    1.46 +by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
    1.47 +     ORELSE ares_tac prems 1));
    1.48  qed "compE";
    1.49  
    1.50  val prems = goal Relation.thy
    1.51 @@ -59,15 +54,12 @@
    1.52  AddIs [compI, idI];
    1.53  AddSEs [compE, idE];
    1.54  
    1.55 -val comp_cs = prod_cs addIs [compI, idI] addSEs [compE, idE];
    1.56 -
    1.57  goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    1.58  by (Fast_tac 1);
    1.59  qed "comp_mono";
    1.60  
    1.61  goal Relation.thy
    1.62 -    "!!r s. [| s <= A Times B;  r <= B Times C |] ==> \
    1.63 -\           (r O s) <= A Times C";
    1.64 +    "!!r s. [| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
    1.65  by (Fast_tac 1);
    1.66  qed "comp_subset_Sigma";
    1.67  
    1.68 @@ -78,14 +70,19 @@
    1.69  by (REPEAT (ares_tac (prems@[allI,impI]) 1));
    1.70  qed "transI";
    1.71  
    1.72 -val major::prems = goalw Relation.thy [trans_def]
    1.73 -    "[| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
    1.74 -by (cut_facts_tac [major] 1);
    1.75 -by (fast_tac (!claset addIs prems) 1);
    1.76 +goalw Relation.thy [trans_def]
    1.77 +    "!!r. [| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
    1.78 +by (Fast_tac 1);
    1.79  qed "transD";
    1.80  
    1.81  (** Natural deduction for converse(r) **)
    1.82  
    1.83 +goalw Relation.thy [converse_def] "!!a b r. ((a,b):converse r) = ((b,a):r)";
    1.84 +by (Simp_tac 1);
    1.85 +qed "converse_iff";
    1.86 +
    1.87 +AddIffs [converse_iff];
    1.88 +
    1.89  goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
    1.90  by (Simp_tac 1);
    1.91  qed "converseI";
    1.92 @@ -94,6 +91,7 @@
    1.93  by (Fast_tac 1);
    1.94  qed "converseD";
    1.95  
    1.96 +(*More general than converseD, as it "splits" the member of the relation*)
    1.97  qed_goalw "converseE" Relation.thy [converse_def]
    1.98      "[| yx : converse(r);  \
    1.99  \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
   1.100 @@ -103,11 +101,7 @@
   1.101      (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
   1.102      (assume_tac 1) ]);
   1.103  
   1.104 -AddSIs [converseI];
   1.105 -AddSEs [converseD,converseE];
   1.106 -
   1.107 -val converse_cs = comp_cs addSIs [converseI]
   1.108 -                          addSEs [converseD,converseE];
   1.109 +AddSEs [converseE];
   1.110  
   1.111  goalw Relation.thy [converse_def] "converse(converse R) = R";
   1.112  by(Fast_tac 1);
   1.113 @@ -128,6 +122,9 @@
   1.114    [ (rtac (Domain_iff RS iffD1 RS exE) 1),
   1.115      (REPEAT (ares_tac prems 1)) ]);
   1.116  
   1.117 +AddIs  [DomainI];
   1.118 +AddSEs [DomainE];
   1.119 +
   1.120  (** Range **)
   1.121  
   1.122  qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
   1.123 @@ -140,11 +137,14 @@
   1.124      (resolve_tac prems 1),
   1.125      (etac converseD 1) ]);
   1.126  
   1.127 +AddIs  [RangeI];
   1.128 +AddSEs [RangeE];
   1.129 +
   1.130  (*** Image of a set under a relation ***)
   1.131  
   1.132  qed_goalw "Image_iff" Relation.thy [Image_def]
   1.133      "b : r^^A = (? x:A. (x,b):r)"
   1.134 - (fn _ => [ fast_tac (!claset addIs [RangeI]) 1 ]);
   1.135 + (fn _ => [ Fast_tac 1 ]);
   1.136  
   1.137  qed_goal "Image_singleton_iff" Relation.thy
   1.138      "(b : r^^{a}) = ((a,b):r)"
   1.139 @@ -153,40 +153,31 @@
   1.140  
   1.141  qed_goalw "ImageI" Relation.thy [Image_def]
   1.142      "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
   1.143 - (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
   1.144 -            (resolve_tac [conjI ] 1),
   1.145 -            (rtac RangeI 1),
   1.146 -            (REPEAT (Fast_tac 1))]);
   1.147 + (fn _ => [ (Fast_tac 1)]);
   1.148  
   1.149  qed_goalw "ImageE" Relation.thy [Image_def]
   1.150      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
   1.151   (fn major::prems=>
   1.152    [ (rtac (major RS CollectE) 1),
   1.153 -    (safe_tac (!claset)),
   1.154 -    (etac RangeE 1),
   1.155 +    (Step_tac 1),
   1.156      (rtac (hd prems) 1),
   1.157      (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
   1.158  
   1.159 +AddIs  [ImageI];
   1.160 +AddSEs [ImageE];
   1.161 +
   1.162  qed_goal "Image_subset" Relation.thy
   1.163      "!!A B r. r <= A Times B ==> r^^C <= B"
   1.164   (fn _ =>
   1.165    [ (rtac subsetI 1),
   1.166      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
   1.167  
   1.168 -AddSIs [converseI]; 
   1.169 -AddIs  [ImageI, DomainI, RangeI];
   1.170 -AddSEs [ImageE, DomainE, RangeE];
   1.171 -
   1.172 -val rel_cs = converse_cs addSIs [converseI] 
   1.173 -                         addIs  [ImageI, DomainI, RangeI]
   1.174 -                         addSEs [ImageE, DomainE, RangeE];
   1.175 -
   1.176  goal Relation.thy "R O id = R";
   1.177 -by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
   1.178 +by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
   1.179  qed "R_O_id";
   1.180  
   1.181  goal Relation.thy "id O R = R";
   1.182 -by(fast_tac (!claset addIs [set_ext] addbefore (split_all_tac 1)) 1);
   1.183 +by (fast_tac (!claset addbefore (split_all_tac 1)) 1);
   1.184  qed "id_O_R";
   1.185  
   1.186  Addsimps [R_O_id,id_O_R];