# HG changeset patch
# User paulson
# Date 890063450 -3600
# Node ID a5dcd7e4a37d588483202bb2a4c4ca5ef67f01d9
# Parent  b855a7094195a7d225b6e33f03fd4713f7d84a28
inverse -> converse
[It is standard terminology and also used in ZF]

diff -r b855a7094195 -r a5dcd7e4a37d src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Finite.ML	Mon Mar 16 16:50:50 1998 +0100
@@ -191,15 +191,15 @@
   by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
   by (simp_tac (simpset() addsplits [expand_split]) 1);
  by (etac finite_imageI 1);
-by (simp_tac (simpset() addsimps [inverse_def,image_def]) 1);
+by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
 by Auto_tac;
  by (rtac bexI 1);
  by (assume_tac 2);
  by (Simp_tac 1);
 by (split_all_tac 1);
 by (Asm_full_simp_tac 1);
-qed "finite_inverse";
-AddIffs [finite_inverse];
+qed "finite_converse";
+AddIffs [finite_converse];
 
 section "Finite cardinality -- 'card'";
 
diff -r b855a7094195 -r a5dcd7e4a37d src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/IMP/Transition.ML	Mon Mar 16 16:50:50 1998 +0100
@@ -127,7 +127,7 @@
 goal Transition.thy
  "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
 \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
-by (etac inverse_rtrancl_induct2 1);
+by (etac converse_rtrancl_induct2 1);
 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
 by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
 qed_spec_mp "my_lemma1";
diff -r b855a7094195 -r a5dcd7e4a37d src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Integ/Equiv.ML	Mon Mar 16 16:50:50 1998 +0100
@@ -16,9 +16,9 @@
 
 (** first half: equiv A r ==> r^-1 O r = r **)
 
-goalw Equiv.thy [trans_def,sym_def,inverse_def]
+goalw Equiv.thy [trans_def,sym_def,converse_def]
     "!!r. [| sym(r); trans(r) |] ==> r^-1 O r <= r";
-by (blast_tac (claset() addSEs [inverseD]) 1);
+by (Blast_tac 1);
 qed "sym_trans_comp_subset";
 
 goalw Equiv.thy [refl_def]
diff -r b855a7094195 -r a5dcd7e4a37d src/HOL/Lambda/Commutation.ML
--- a/src/HOL/Lambda/Commutation.ML	Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Lambda/Commutation.ML	Mon Mar 16 16:50:50 1998 +0100
@@ -91,7 +91,7 @@
 by (safe_tac HOL_cs);
  by (blast_tac (HOL_cs addIs
       [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
-       rtrancl_inverseI, inverseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
+       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
 by (etac rtrancl_induct 1);
  by (Blast_tac 1);
 by (blast_tac (claset() delrules [rtrancl_refl] 
diff -r b855a7094195 -r a5dcd7e4a37d src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Relation.ML	Mon Mar 16 16:50:50 1998 +0100
@@ -87,22 +87,22 @@
 
 (** Natural deduction for r^-1 **)
 
-goalw thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
+goalw thy [converse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
 by (Simp_tac 1);
-qed "inverse_iff";
+qed "converse_iff";
 
-AddIffs [inverse_iff];
+AddIffs [converse_iff];
 
-goalw thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
+goalw thy [converse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
 by (Simp_tac 1);
-qed "inverseI";
+qed "converseI";
 
-goalw thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
+goalw thy [converse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
 by (Blast_tac 1);
-qed "inverseD";
+qed "converseD";
 
-(*More general than inverseD, as it "splits" the member of the relation*)
-qed_goalw "inverseE" thy [inverse_def]
+(*More general than converseD, as it "splits" the member of the relation*)
+qed_goalw "converseE" thy [converse_def]
     "[| yx : r^-1;  \
 \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
 \    |] ==> P"
@@ -111,21 +111,21 @@
     (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
     (assume_tac 1) ]);
 
-AddSEs [inverseE];
+AddSEs [converseE];
 
-goalw thy [inverse_def] "(r^-1)^-1 = r";
+goalw thy [converse_def] "(r^-1)^-1 = r";
 by (Blast_tac 1);
-qed "inverse_inverse";
-Addsimps [inverse_inverse];
+qed "converse_converse";
+Addsimps [converse_converse];
 
 goal thy "(r O s)^-1 = s^-1 O r^-1";
 by (Blast_tac 1);
-qed "inverse_comp";
+qed "converse_comp";
 
 goal thy "id^-1 = id";
 by (Blast_tac 1);
-qed "inverse_id";
-Addsimps [inverse_id];
+qed "converse_id";
+Addsimps [converse_id];
 
 (** Domain **)
 
@@ -153,14 +153,14 @@
 (** Range **)
 
 qed_goalw "RangeI" thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
- (fn _ => [ (etac (inverseI RS DomainI) 1) ]);
+ (fn _ => [ (etac (converseI RS DomainI) 1) ]);
 
 qed_goalw "RangeE" thy [Range_def]
     "[| b : Range(r);  !!x. (x,b): r ==> P |] ==> P"
  (fn major::prems=>
   [ (rtac (major RS DomainE) 1),
     (resolve_tac prems 1),
-    (etac inverseD 1) ]);
+    (etac converseD 1) ]);
 
 AddIs  [RangeI];
 AddSEs [RangeE];
diff -r b855a7094195 -r a5dcd7e4a37d src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Relation.thy	Mon Mar 16 16:50:50 1998 +0100
@@ -8,7 +8,7 @@
 consts
     id          :: "('a * 'a)set"               (*the identity relation*)
     O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
-    inverse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
+    converse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 999)
     "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
     Domain      :: "('a*'b) set => 'a set"
     Range       :: "('a*'b) set => 'b set"
@@ -17,7 +17,7 @@
 defs
     id_def        "id == {p. ? x. p = (x,x)}"
     comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
-    inverse_def   "r^-1 == {(y,x). (x,y):r}"
+    converse_def   "r^-1 == {(y,x). (x,y):r}"
     Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
     Range_def     "Range(r) == Domain(r^-1)"
     Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
diff -r b855a7094195 -r a5dcd7e4a37d src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/Trancl.ML	Mon Mar 16 16:50:50 1998 +0100
@@ -139,48 +139,48 @@
 Addsimps [rtrancl_reflcl];
 
 goal Trancl.thy "!!r. (x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
-by (rtac inverseI 1);
+by (rtac converseI 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_inverseD";
+qed "rtrancl_converseD";
 
 goal Trancl.thy "!!r. (x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
-by (dtac inverseD 1);
+by (dtac converseD 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
 by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_inverseI";
+qed "rtrancl_converseI";
 
 goal Trancl.thy "(r^-1)^* = (r^*)^-1";
-by (safe_tac (claset() addSIs [rtrancl_inverseI]));
+by (safe_tac (claset() addSIs [rtrancl_converseI]));
 by (res_inst_tac [("p","x")] PairE 1);
 by (hyp_subst_tac 1);
-by (etac rtrancl_inverseD 1);
-qed "rtrancl_inverse";
+by (etac rtrancl_converseD 1);
+qed "rtrancl_converse";
 
 val major::prems = goal Trancl.thy
     "[| (a,b) : r^*; P(b); \
 \       !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]  \
 \     ==> P(a)";
-by (rtac ((major RS inverseI RS rtrancl_inverseI) RS rtrancl_induct) 1);
+by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
 by (resolve_tac prems 1);
-by (blast_tac (claset() addIs prems addSDs[rtrancl_inverseD])1);
-qed "inverse_rtrancl_induct";
+by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
+qed "converse_rtrancl_induct";
 
 val prems = goal Trancl.thy
  "[| ((a,b),(c,d)) : r^*; P c d; \
 \    !!x y z u.[| ((x,y),(z,u)) : r;  ((z,u),(c,d)) : r^*;  P z u |] ==> P x y\
 \ |] ==> P a b";
 by (res_inst_tac[("R","P")]splitD 1);
-by (res_inst_tac[("P","split P")]inverse_rtrancl_induct 1);
+by (res_inst_tac[("P","split P")]converse_rtrancl_induct 1);
 by (resolve_tac prems 1);
 by (Simp_tac 1);
 by (resolve_tac prems 1);
 by (split_all_tac 1);
 by (Asm_full_simp_tac 1);
 by (REPEAT(ares_tac prems 1));
-qed "inverse_rtrancl_induct2";
+qed "converse_rtrancl_induct2";
 
 val major::prems = goal Trancl.thy
  "[| (x,z):r^*; \
@@ -188,7 +188,7 @@
 \    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
 \ |] ==> P";
 by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
-by (rtac (major RS inverse_rtrancl_induct) 2);
+by (rtac (major RS converse_rtrancl_induct) 2);
 by (blast_tac (claset() addIs prems) 2);
 by (blast_tac (claset() addIs prems) 2);
 by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
@@ -304,9 +304,9 @@
 qed "trancl_insert";
 
 goalw Trancl.thy [trancl_def] "(r^-1)^+ = (r^+)^-1";
-by (simp_tac (simpset() addsimps [rtrancl_inverse,inverse_comp]) 1);
-by (simp_tac (simpset() addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
-qed "trancl_inverse";
+by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
+by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq]) 1);
+qed "trancl_converse";
 
 
 val major::prems = goal Trancl.thy
diff -r b855a7094195 -r a5dcd7e4a37d src/HOL/WF.ML
--- a/src/HOL/WF.ML	Mon Mar 16 16:47:57 1998 +0100
+++ b/src/HOL/WF.ML	Mon Mar 16 16:50:50 1998 +0100
@@ -144,8 +144,8 @@
 AddIffs [acyclic_insert];
 
 goalw WF.thy [acyclic_def] "acyclic(r^-1) = acyclic r";
-by (simp_tac (simpset() addsimps [trancl_inverse]) 1);
-qed "acyclic_inverse";
+by (simp_tac (simpset() addsimps [trancl_converse]) 1);
+qed "acyclic_converse";
 
 (** cut **)