converse -> ^-1

--- a/src/HOL/Finite.ML	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/Finite.ML	Tue Jun 17 09:01:56 1997 +0200
@@ -174,22 +174,22 @@
 qed "finite_Pow_iff";
 AddIffs [finite_Pow_iff];
 
-goal Finite.thy "finite(converse r) = finite r";
-by(subgoal_tac "converse r = (%(x,y).(y,x))``r" 1);
+goal Finite.thy "finite(r^-1) = finite r";
+by(subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
  by(Asm_simp_tac 1);
  br iffI 1;
   be (rewrite_rule [inj_onto_def] finite_imageD) 1;
   by(simp_tac (!simpset setloop (split_tac[expand_split])) 1);
  be finite_imageI 1;
-by(simp_tac (!simpset addsimps [converse_def,image_def]) 1);
+by(simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
 by(Auto_tac());
  br bexI 1;
  ba 2;
  by(Simp_tac 1);
 by(split_all_tac 1);
 by(Asm_full_simp_tac 1);
-qed "finite_converse";
-AddIffs [finite_converse];
+qed "finite_inverse";
+AddIffs [finite_inverse];
 
 section "Finite cardinality -- 'card'";
 

--- a/src/HOL/IMP/Transition.ML	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/IMP/Transition.ML	Tue Jun 17 09:01:56 1997 +0200
@@ -128,7 +128,7 @@
 goal Transition.thy
  "!!c1. (c1,s1) -*-> (SKIP,s2) ==> \
 \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
-by (etac converse_rtrancl_induct2 1);
+by (etac inverse_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";

--- a/src/HOL/Integ/Equiv.ML	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/Integ/Equiv.ML	Tue Jun 17 09:01:56 1997 +0200
@@ -12,22 +12,22 @@
 
 Delrules [equalityI];
 
-(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
+(*** Suppes, Theorem 70: r is an equiv relation iff r^-1 O r = r ***)
 
-(** first half: equiv A r ==> converse(r) O r = r **)
+(** first half: equiv A r ==> r^-1 O r = r **)
 
-goalw Equiv.thy [trans_def,sym_def,converse_def]
-    "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r";
-by (fast_tac (!claset addSEs [converseD]) 1);
+goalw Equiv.thy [trans_def,sym_def,inverse_def]
+    "!!r. [| sym(r); trans(r) |] ==> r^-1 O r <= r";
+by (fast_tac (!claset addSEs [inverseD]) 1);
 qed "sym_trans_comp_subset";
 
 goalw Equiv.thy [refl_def]
-    "!!A r. refl A r ==> r <= converse(r) O r";
+    "!!A r. refl A r ==> r <= r^-1 O r";
 by (fast_tac (!claset addIs [compI]) 1);
 qed "refl_comp_subset";
 
 goalw Equiv.thy [equiv_def]
-    "!!A r. equiv A r ==> converse(r) O r = r";
+    "!!A r. equiv A r ==> r^-1 O r = r";
 by (rtac equalityI 1);
 by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1
      ORELSE etac conjE 1));
@@ -35,7 +35,7 @@
 
 (*second half*)
 goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def]
-    "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
+    "!!A r. [| r^-1 O r = r;  Domain(r) = A |] ==> equiv A r";
 by (etac equalityE 1);
 by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
 by (Step_tac 1);

--- a/src/HOL/Lambda/Commutation.ML	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Tue Jun 17 09:01:56 1997 +0200
@@ -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_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
+       rtrancl_inverseI, inverseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
 by (etac rtrancl_induct 1);
  by (Blast_tac 1);
 by (Blast.depth_tac (!claset delrules [rtrancl_refl] 

--- a/src/HOL/Lambda/Commutation.thy	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/Lambda/Commutation.thy	Tue Jun 17 09:01:56 1997 +0200
@@ -21,7 +21,7 @@
   diamond_def "diamond R   == commute R R"
 
   Church_Rosser_def "Church_Rosser(R) ==   
-  !x y. (x,y) : (R Un converse(R))^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
+  !x y. (x,y) : (R Un R^-1)^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
 
 translations
   "confluent R" == "diamond(R^*)"

--- a/src/HOL/Relation.ML	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/Relation.ML	Tue Jun 17 09:01:56 1997 +0200
@@ -75,25 +75,25 @@
 by (Blast_tac 1);
 qed "transD";
 
-(** Natural deduction for converse(r) **)
+(** Natural deduction for r^-1 **)
 
-goalw Relation.thy [converse_def] "!!a b r. ((a,b):converse r) = ((b,a):r)";
+goalw Relation.thy [inverse_def] "!!a b r. ((a,b): r^-1) = ((b,a):r)";
 by (Simp_tac 1);
-qed "converse_iff";
+qed "inverse_iff";
 
-AddIffs [converse_iff];
+AddIffs [inverse_iff];
 
-goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
+goalw Relation.thy [inverse_def] "!!a b r. (a,b):r ==> (b,a): r^-1";
 by (Simp_tac 1);
-qed "converseI";
+qed "inverseI";
 
-goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
+goalw Relation.thy [inverse_def] "!!a b r. (a,b) : r^-1 ==> (b,a) : r";
 by (Blast_tac 1);
-qed "converseD";
+qed "inverseD";
 
-(*More general than converseD, as it "splits" the member of the relation*)
-qed_goalw "converseE" Relation.thy [converse_def]
-    "[| yx : converse(r);  \
+(*More general than inverseD, as it "splits" the member of the relation*)
+qed_goalw "inverseE" Relation.thy [inverse_def]
+    "[| yx : r^-1;  \
 \       !!x y. [| yx=(y,x);  (x,y):r |] ==> P \
 \    |] ==> P"
  (fn [major,minor]=>
@@ -101,16 +101,16 @@
     (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
     (assume_tac 1) ]);
 
-AddSEs [converseE];
+AddSEs [inverseE];
 
-goalw Relation.thy [converse_def] "converse(converse R) = R";
+goalw Relation.thy [inverse_def] "(r^-1)^-1 = r";
 by (Blast_tac 1);
-qed "converse_converse";
-Addsimps [converse_converse];
+qed "inverse_inverse";
+Addsimps [inverse_inverse];
 
-goal Relation.thy "converse(r O s) = converse s O converse r";
+goal Relation.thy "(r O s)^-1 = s^-1 O r^-1";
 by(Blast_tac 1);
-qed "converse_comp";
+qed "inverse_comp";
 
 (** Domain **)
 
@@ -133,14 +133,14 @@
 (** Range **)
 
 qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.(a,b): r ==> b : Range(r)"
- (fn _ => [ (etac (converseI RS DomainI) 1) ]);
+ (fn _ => [ (etac (inverseI RS DomainI) 1) ]);
 
 qed_goalw "RangeE" Relation.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 converseD 1) ]);
+    (etac inverseD 1) ]);
 
 AddIs  [RangeI];
 AddSEs [RangeE];

--- a/src/HOL/Relation.thy	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/Relation.thy	Tue Jun 17 09:01:56 1997 +0200
@@ -9,7 +9,7 @@
     id          :: "('a * 'a)set"               (*the identity relation*)
     O           :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60)
     trans       :: "('a * 'a)set => bool"       (*transitivity predicate*)
-    converse    :: "('a*'b) set => ('b*'a) set"
+    inverse    :: "('a*'b) set => ('b*'a) set"     ("(_^-1)" [1000] 1000)
     "^^"        :: "[('a*'b) set,'a set] => 'b set" (infixl 90)
     Domain      :: "('a*'b) set => 'a set"
     Range       :: "('a*'b) set => 'b set"
@@ -17,8 +17,8 @@
     id_def        "id == {p. ? x. p = (x,x)}"
     comp_def      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
     trans_def     "trans(r) == (!x y z. (x,y):r --> (y,z):r --> (x,z):r)"
-    converse_def  "converse(r) == {(y,x). (x,y):r}"
+    inverse_def   "r^-1 == {(y,x). (x,y):r}"
     Domain_def    "Domain(r) == {x. ? y. (x,y):r}"
-    Range_def     "Range(r) == Domain(converse(r))"
+    Range_def     "Range(r) == Domain(r^-1)"
     Image_def     "r ^^ s == {y. ? x:s. (x,y):r}"
 end

--- a/src/HOL/Trancl.ML	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/Trancl.ML	Tue Jun 17 09:01:56 1997 +0200
@@ -138,49 +138,49 @@
 qed "rtrancl_reflcl";
 Addsimps [rtrancl_reflcl];
 
-goal Trancl.thy "!!r. (x,y) : (converse r)^* ==> (x,y) : converse(r^*)";
-by (rtac converseI 1);
+goal Trancl.thy "!!r. (x,y) : (r^-1)^* ==> (x,y) : (r^*)^-1";
+by (rtac inverseI 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
 by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_converseD";
+qed "rtrancl_inverseD";
 
-goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
-by (dtac converseD 1);
+goal Trancl.thy "!!r. (x,y) : (r^*)^-1 ==> (x,y) : (r^-1)^*";
+by (dtac inverseD 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
 by (blast_tac (!claset addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "rtrancl_converseI";
+qed "rtrancl_inverseI";
 
-goal Trancl.thy "(converse r)^* = converse(r^*)";
-by (safe_tac (!claset addSIs [rtrancl_converseI]));
+goal Trancl.thy "(r^-1)^* = (r^*)^-1";
+by (safe_tac (!claset addSIs [rtrancl_inverseI]));
 by (res_inst_tac [("p","x")] PairE 1);
 by (hyp_subst_tac 1);
-by (etac rtrancl_converseD 1);
-qed "rtrancl_converse";
+by (etac rtrancl_inverseD 1);
+qed "rtrancl_inverse";
 
 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 converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
+by (rtac ((major RS inverseI RS rtrancl_inverseI) RS rtrancl_induct) 1);
 by (resolve_tac prems 1);
-by (blast_tac (!claset addIs prems addSDs[rtrancl_converseD])1);
-qed "converse_rtrancl_induct";
+by (blast_tac (!claset addIs prems addSDs[rtrancl_inverseD])1);
+qed "inverse_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")]converse_rtrancl_induct 1);
+by (res_inst_tac[("P","split P")]inverse_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 "converse_rtrancl_induct2";
+qed "inverse_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 converse_rtrancl_induct) 2);
+by (rtac (major RS inverse_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,10 +304,10 @@
       impOfSubs rtrancl_mono, trancl_mono]) 1);
 qed "trancl_insert";
 
-goalw Trancl.thy [trancl_def] "(converse r)^+ = converse(r^+)";
-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";
+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";
 
 
 val major::prems = goal Trancl.thy

--- a/src/HOL/WF.ML	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/WF.ML	Tue Jun 17 09:01:56 1997 +0200
@@ -141,9 +141,9 @@
 qed "acyclic_insert";
 AddIffs [acyclic_insert];
 
-goalw WF.thy [acyclic_def] "acyclic(converse r) = acyclic r";
-by(simp_tac (!simpset addsimps [trancl_converse]) 1);
-qed "acyclic_converse";
+goalw WF.thy [acyclic_def] "acyclic(r^-1) = acyclic r";
+by(simp_tac (!simpset addsimps [trancl_inverse]) 1);
+qed "acyclic_inverse";
 
 (** cut **)
 

--- a/src/HOL/ex/mesontest2.ML	Mon Jun 16 14:25:33 1997 +0200
+++ b/src/HOL/ex/mesontest2.ML	Tue Jun 17 09:01:56 1997 +0200
@@ -2986,9 +2986,9 @@
 \  (! Y Z X. member(Z::'a,cross_product(X::'a,Y)) --> member(first(Z),X)) &     \
 \  (! X Z Y. member(Z::'a,cross_product(X::'a,Y)) --> member(second(Z),Y)) &    \
 \  (! X Z Y. little_set(Z) & ordered_pair_predicate(Z) & member(first(Z),X) & member(second(Z),Y) --> member(Z::'a,cross_product(X::'a,Y))) &   \
-\  (! X Z. member(Z::'a,converse(X)) --> ordered_pair_predicate(Z)) &       \
-\  (! Z X. member(Z::'a,converse(X)) --> member(ordered_pair(second(Z),first(Z)),X)) &      \
-\  (! Z X. little_set(Z) & ordered_pair_predicate(Z) & member(ordered_pair(second(Z),first(Z)),X) --> member(Z::'a,converse(X))) &  \
+\  (! X Z. member(Z::'a,X^-1) --> ordered_pair_predicate(Z)) &       \
+\  (! Z X. member(Z::'a,X^-1) --> member(ordered_pair(second(Z),first(Z)),X)) &      \
+\  (! Z X. little_set(Z) & ordered_pair_predicate(Z) & member(ordered_pair(second(Z),first(Z)),X) --> member(Z::'a,X^-1)) &  \
 \  (! Z X. member(Z::'a,rotate_right(X)) --> little_set(f9(Z::'a,X))) & \
 \  (! Z X. member(Z::'a,rotate_right(X)) --> little_set(f10(Z::'a,X))) &        \
 \  (! Z X. member(Z::'a,rotate_right(X)) --> little_set(f11(Z::'a,X))) &        \
@@ -3056,8 +3056,8 @@
 \  (! Z. little_set(Z) & ordered_pair_predicate(Z) & equal(first(Z),second(Z)) --> member(Z::'a,identity_relation)) &       \
 \  (! X Y. equal(restrict(X::'a,Y),intersection(X::'a,cross_product(Y::'a,universal_set)))) &       \
 \  (! Xf. one_to_one_function(Xf) --> function(Xf)) &   \
-\  (! Xf. one_to_one_function(Xf) --> function(converse(Xf))) & \
-\  (! Xf. function(Xf) & function(converse(Xf)) --> one_to_one_function(Xf)) &  \
+\  (! Xf. one_to_one_function(Xf) --> function(Xf^-1)) & \
+\  (! Xf. function(Xf) & function(Xf^-1) --> one_to_one_function(Xf)) &  \
 \  (! Z Xf Y. member(Z::'a,apply(Xf::'a,Y)) --> ordered_pair_predicate(f28(Z::'a,Xf,Y))) &  \
 \  (! Z Y Xf. member(Z::'a,apply(Xf::'a,Y)) --> member(f28(Z::'a,Xf,Y),Xf)) &       \
 \  (! Z Xf Y. member(Z::'a,apply(Xf::'a,Y)) --> equal(first(f28(Z::'a,Xf,Y)),Y)) &  \
@@ -3159,7 +3159,7 @@
 \  (! S' T'. equal(S'::'a,T') --> equal(complement(S'),complement(T'))) &   \
 \  (! U V W. equal(U::'a,V) --> equal(composition(U::'a,W),composition(V::'a,W))) & \
 \  (! X Z Y. equal(X::'a,Y) --> equal(composition(Z::'a,X),composition(Z::'a,Y))) & \
-\  (! A1 B1. equal(A1::'a,B1) --> equal(converse(A1),converse(B1))) &       \
+\  (! A1 B1. equal(A1::'a,B1) --> equal(A1^-1,B1^-1)) &       \
 \  (! C1 D1 E1. equal(C1::'a,D1) --> equal(cross_product(C1::'a,E1),cross_product(D1::'a,E1))) &    \
 \  (! F1 H1 G1. equal(F1::'a,G1) --> equal(cross_product(H1::'a,F1),cross_product(H1::'a,G1))) &    \
 \  (! I1 J1. equal(I1::'a,J1) --> equal(domain_of(I1),domain_of(J1))) &     \