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.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.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.47 +qed "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.59 +qed "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