src/HOL/Relation.ML
changeset 4746 a5dcd7e4a37d
parent 4733 2c984ac036f5
child 4760 9cdbd5a1d25a
     1.1 --- a/src/HOL/Relation.ML	Mon Mar 16 16:47:57 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Mon Mar 16 16:50:50 1998 +0100
     1.3 @@ -87,22 +87,22 @@
     1.4  
     1.5  (** Natural deduction for r^-1 **)
     1.6  
     1.7 -goalw thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
     1.8 +goalw thy [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
     1.9  by (Simp_tac 1);
    1.10 -qed "inverse_iff";
    1.11 +qed "converse_iff";
    1.12  
    1.13 -AddIffs [inverse_iff];
    1.14 +AddIffs [converse_iff];
    1.15  
    1.16 -goalw thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
    1.17 +goalw thy [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
    1.18  by (Simp_tac 1);
    1.19 -qed "inverseI";
    1.20 +qed "converseI";
    1.21  
    1.22 -goalw thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
    1.23 +goalw thy [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
    1.24  by (Blast_tac 1);
    1.25 -qed "inverseD";
    1.26 +qed "converseD";
    1.27  
    1.28 -(*More general than inverseD, as it "splits" the member of the relation*)
    1.29 -qed_goalw "inverseE" thy [inverse_def]
    1.30 +(*More general than converseD, as it "splits" the member of the relation*)
    1.31 +qed_goalw "converseE" thy [converse_def]
    1.32      "[| yx : r^-1;  \
    1.33  \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
    1.34  \    |] ==> P"
    1.35 @@ -111,21 +111,21 @@
    1.36      (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
    1.37      (assume_tac 1) ]);
    1.38  
    1.39 -AddSEs [inverseE];
    1.40 +AddSEs [converseE];
    1.41  
    1.42 -goalw thy [inverse_def] "(r^-1)^-1 = r";
    1.43 +goalw thy [converse_def] "(r^-1)^-1 = r";
    1.44  by (Blast_tac 1);
    1.45 -qed "inverse_inverse";
    1.46 -Addsimps [inverse_inverse];
    1.47 +qed "converse_converse";
    1.48 +Addsimps [converse_converse];
    1.49  
    1.50  goal thy "(r O s)^-1 = s^-1 O r^-1";
    1.51  by (Blast_tac 1);
    1.52 -qed "inverse_comp";
    1.53 +qed "converse_comp";
    1.54  
    1.55  goal thy "id^-1 = id";
    1.56  by (Blast_tac 1);
    1.57 -qed "inverse_id";
    1.58 -Addsimps [inverse_id];
    1.59 +qed "converse_id";
    1.60 +Addsimps [converse_id];
    1.61  
    1.62  (** Domain **)
    1.63  
    1.64 @@ -153,14 +153,14 @@
    1.65  (** Range **)
    1.66  
    1.67  qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
    1.68 - (fn _ => [ (etac (inverseI RS DomainI) 1) ]);
    1.69 + (fn _ => [ (etac (converseI RS DomainI) 1) ]);
    1.70  
    1.71  qed_goalw "RangeE" thy [Range_def]
    1.72      "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P"
    1.73   (fn major::prems=>
    1.74    [ (rtac (major RS DomainE) 1),
    1.75      (resolve_tac prems 1),
    1.76 -    (etac inverseD 1) ]);
    1.77 +    (etac converseD 1) ]);
    1.78  
    1.79  AddIs  [RangeI];
    1.80  AddSEs [RangeE];