# HG changeset patch
# User nipkow
# Date 860162624 -7200
# Node ID 0e272e4c7cb254f4c13bd4fc2f2d9774ba3716d0
# Parent  171dedbc9bdba1558cb67e0731c13d8adebc72aa
inv -> inverse

diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Group/Group.ML
--- a/src/HOL/AxClasses/Group/Group.ML	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Group/Group.ML	Fri Apr 04 16:03:44 1997 +0200
@@ -11,27 +11,27 @@
 fun ssub r = standard (r RS ssubst);
 
 
-goal thy "x * inv x = (1::'a::group)";
+goal thy "x * inverse x = (1::'a::group)";
 by (rtac (sub left_unit) 1);
 back();
 by (rtac (sub assoc) 1);
-by (rtac (sub left_inv) 1);
+by (rtac (sub left_inverse) 1);
 back();
 back();
 by (rtac (ssub assoc) 1);
 back();
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (rtac (ssub assoc) 1);
 by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (rtac refl 1);
-qed "right_inv";
+qed "right_inverse";
 
 
 goal thy "x * 1 = (x::'a::group)";
-by (rtac (sub left_inv) 1);
+by (rtac (sub left_inverse) 1);
 by (rtac (sub assoc) 1);
-by (rtac (ssub right_inv) 1);
+by (rtac (ssub right_inverse) 1);
 by (rtac (ssub left_unit) 1);
 by (rtac refl 1);
 qed "right_unit";
@@ -41,7 +41,7 @@
 by (rtac impI 1);
 by (rtac (sub right_unit) 1);
 back();
-by (res_inst_tac [("x", "x")] (sub right_inv) 1);
+by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
 by (rtac (sub assoc) 1);
 by (rtac arg_cong 1);
 back();
@@ -74,7 +74,7 @@
 by (rtac (sub left_unit) 1);
 back();
 by (rtac (sub left_unit) 1);
-by (res_inst_tac [("x", "x")] (sub left_inv) 1);
+by (res_inst_tac [("x", "x")] (sub left_inverse) 1);
 by (rtac (ssub assoc) 1);
 back();
 by (rtac (ssub assoc) 1);
@@ -84,49 +84,49 @@
 qed "inj_times";
 
 
-goal thy "y * x = 1 --> y = inv (x::'a::group)";
+goal thy "y * x = 1 --> y = inverse (x::'a::group)";
 by (rtac impI 1);
 by (rtac (sub right_unit) 1);
 back();
 back();
 by (rtac (sub right_unit) 1);
-by (res_inst_tac [("x", "x")] (sub right_inv) 1);
+by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
 by (rtac (sub assoc) 1);
 by (rtac (sub assoc) 1);
 by (rtac arg_cong 1);
 back();
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (assume_tac 1);
-qed "one_inv";
+qed "one_inverse";
 
 
 goal thy "ALL x. EX! y. y * x = (1::'a::group)";
 by (rtac allI 1);
 by (rtac ex1I 1);
-by (rtac left_inv 1);
+by (rtac left_inverse 1);
 by (rtac mp 1);
-by (rtac one_inv 1);
+by (rtac one_inverse 1);
 by (assume_tac 1);
-qed "ex1_inv";
+qed "ex1_inverse";
 
 
-goal thy "inv (x * y) = inv y * inv (x::'a::group)";
+goal thy "inverse (x * y) = inverse y * inverse (x::'a::group)";
 by (rtac sym 1);
 by (rtac mp 1);
-by (rtac one_inv 1);
+by (rtac one_inverse 1);
 by (rtac (ssub assoc) 1);
 by (rtac (sub assoc) 1);
 back();
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (rtac refl 1);
-qed "inv_times";
+qed "inverse_times";
 
 
-goal thy "inv (inv x) = (x::'a::group)";
+goal thy "inverse (inverse x) = (x::'a::group)";
 by (rtac sym 1);
-by (rtac (one_inv RS mp) 1);
-by (rtac (ssub right_inv) 1);
+by (rtac (one_inverse RS mp) 1);
+by (rtac (ssub right_inverse) 1);
 by (rtac refl 1);
-qed "inv_inv";
+qed "inverse_inverse";
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Group/Group.thy
--- a/src/HOL/AxClasses/Group/Group.thy	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Group/Group.thy	Fri Apr 04 16:03:44 1997 +0200
@@ -3,7 +3,7 @@
     Author:     Markus Wenzel, TU Muenchen
 *)
 
-Group = Sigs + Set +
+Group = Sigs + Fun +
 
 (* semigroups *)
 
@@ -15,9 +15,9 @@
 (* groups *)
 
 axclass
-  group < one, inv, semigroup
+  group < one, inverse, semigroup
   left_unit     "1 * x = x"
-  left_inv      "inv x * x = 1"
+  left_inverse  "inverse x * x = 1"
 
 
 (* abelian groups *)
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Group/GroupDefs.ML
--- a/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Apr 04 16:03:44 1997 +0200
@@ -1,7 +1,3 @@
-
-open GroupDefs;
-
-
 (* bool *)
 
 (*this is really overkill - should be rather proven 'inline'*)
@@ -18,9 +14,10 @@
 by (Fast_tac 1);
 qed "bool_right_unit";
 
-goalw thy [times_bool_def, inv_bool_def, one_bool_def] "inv(x) * x = (1::bool)";
+goalw thy [times_bool_def, inverse_bool_def, one_bool_def]
+  "inverse(x) * x = (1::bool)";
 by (Fast_tac 1);
-qed "bool_left_inv";
+qed "bool_left_inverse";
 
 goalw thy [times_bool_def] "x * y = (y * (x::bool))";
 by (Fast_tac 1);
@@ -31,7 +28,8 @@
 
 val prod_ss = simpset_of "Prod";
 
-goalw thy [times_prod_def] "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))";
+goalw thy [times_prod_def]
+  "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))";
 by (simp_tac (prod_ss addsimps [assoc]) 1);
 qed "prod_assoc";
 
@@ -45,9 +43,10 @@
 by (rtac (surjective_pairing RS sym) 1);
 qed "prod_right_unit";
 
-goalw thy [times_prod_def, inv_prod_def, one_prod_def] "inv x * x = (1::'a::group*'b::group)";
-by (simp_tac (prod_ss addsimps [left_inv]) 1);
-qed "prod_left_inv";
+goalw thy [times_prod_def, inverse_prod_def, one_prod_def]
+  "inverse x * x = (1::'a::group*'b::group)";
+by (simp_tac (prod_ss addsimps [left_inverse]) 1);
+qed "prod_left_inverse";
 
 goalw thy [times_prod_def] "x * y = y * (x::'a::agroup*'b::agroup)";
 by (simp_tac (prod_ss addsimps [commut]) 1);
@@ -74,11 +73,12 @@
 by (rtac Monoid.right_unit 1);
 qed "fun_right_unit";
 
-goalw thy [times_fun_def, inv_fun_def, one_fun_def] "inv x * x = (1::'a => 'b::group)";
+goalw thy [times_fun_def, inverse_fun_def, one_fun_def]
+  "inverse x * x = (1::'a => 'b::group)";
 by (stac expand_fun_eq 1);
 by (rtac allI 1);
-by (rtac left_inv 1);
-qed "fun_left_inv";
+by (rtac left_inverse 1);
+qed "fun_left_inverse";
 
 goalw thy [times_fun_def] "x * y = y * (x::'a => 'b::agroup)";
 by (stac expand_fun_eq 1);
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Group/GroupDefs.thy
--- a/src/HOL/AxClasses/Group/GroupDefs.thy	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Group/GroupDefs.thy	Fri Apr 04 16:03:44 1997 +0200
@@ -9,33 +9,33 @@
 (* bool *)
 
 instance
-  bool :: {times, inv, one}
+  bool :: {times, inverse, one}
 
 defs
   times_bool_def        "x * y == (x ~= y)"
-  inv_bool_def          "inv x == (x::bool)"
+  inverse_bool_def      "inverse x == (x::bool)"
   one_bool_def          "1 == False"
 
 
 (* cartesian products *)
 
 instance
-  "*" :: (term, term) {times, inv, one}
+  "*" :: (term, term) {times, inverse, one}
 
 defs
   times_prod_def        "p * q == (fst p * fst q, snd p * snd q)"
-  inv_prod_def          "inv p == (inv (fst p), inv (snd p))"
+  inverse_prod_def      "inverse p == (inverse (fst p), inverse (snd p))"
   one_prod_def          "1 == (1, 1)"
 
 
 (* function spaces *)
 
 instance
-  fun :: (term, term) {times, inv, one}
+  fun :: (term, term) {times, inverse, one}
 
 defs
   times_fun_def         "f * g == (%x. f x * g x)"
-  inv_fun_def           "inv f == (%x. inv (f x))"
+  inverse_fun_def       "inverse f == (%x. inverse (f x))"
   one_fun_def           "1 == (%x. 1)"
 
 end
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Group/GroupInsts.thy
--- a/src/HOL/AxClasses/Group/GroupInsts.thy	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Group/GroupInsts.thy	Fri Apr 04 16:03:44 1997 +0200
@@ -11,36 +11,36 @@
 (* bool *)
 
 instance
-  bool :: semigroup                     (bool_assoc)
+  bool :: semigroup              (bool_assoc)
 instance
-  bool :: monoid                        (bool_assoc, bool_left_unit, bool_right_unit)
+  bool :: monoid                 (bool_assoc, bool_left_unit, bool_right_unit)
 instance
-  bool :: group                         (bool_left_unit, bool_left_inv)
+  bool :: group                  (bool_left_unit, bool_left_inverse)
 instance
-  bool :: agroup                        (bool_commut)
+  bool :: agroup                 (bool_commut)
 
 
 (* cartesian products *)
 
 instance
-  "*" :: (semigroup, semigroup) semigroup       (prod_assoc)
+  "*" :: (semigroup, semigroup) semigroup   (prod_assoc)
 instance
-  "*" :: (monoid, monoid) monoid                (prod_assoc, prod_left_unit, prod_right_unit)
+  "*" :: (monoid, monoid) monoid  (prod_assoc, prod_left_unit, prod_right_unit)
 instance
-  "*" :: (group, group) group                   (prod_left_unit, prod_left_inv)
+  "*" :: (group, group) group               (prod_left_unit, prod_left_inverse)
 instance
-  "*" :: (agroup, agroup) agroup                (prod_commut)
+  "*" :: (agroup, agroup) agroup            (prod_commut)
 
 
 (* function spaces *)
 
 instance
-  fun :: (term, semigroup) semigroup            (fun_assoc)
+  fun :: (term, semigroup) semigroup        (fun_assoc)
 instance
-  fun :: (term, monoid) monoid                  (fun_assoc, fun_left_unit, fun_right_unit)
+  fun :: (term, monoid) monoid       (fun_assoc, fun_left_unit, fun_right_unit)
 instance
-  fun :: (term, group) group                    (fun_left_unit, fun_left_inv)
+  fun :: (term, group) group                (fun_left_unit, fun_left_inverse)
 instance
-  fun :: (term, agroup) agroup                  (fun_commut)
+  fun :: (term, agroup) agroup              (fun_commut)
 
 end
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Group/Sigs.thy
--- a/src/HOL/AxClasses/Group/Sigs.thy	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Group/Sigs.thy	Fri Apr 04 16:03:44 1997 +0200
@@ -6,13 +6,13 @@
 Sigs = HOL +
 
 axclass
-  inv < term
+  inverse < term
 
 axclass
   one < term
 
 consts
-  "inv" :: "'a::inv => 'a"
-  "1"   :: "'a::one"                    ("1")
+  inverse :: 'a::inverse => 'a
+  "1"     :: 'a::one                    ("1")
 
 end
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy
--- a/src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy	Fri Apr 04 16:03:44 1997 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Define overloaded constants "<*>", "inv", "1" on type "bool"
+Define overloaded constants "<*>", "inverse", "1" on type "bool"
 appropriately, then prove that this forms a group.
 *)
 
@@ -11,9 +11,9 @@
 (* bool as abelian group *)
 
 defs
-  prod_bool_def "x <*> y == x ~= (y::bool)"
-  inv_bool_def  "inv x   == x::bool"
-  unit_bool_def "1       == False"
+  prod_bool_def     "x <*> y   == x ~= (y::bool)"
+  inverse_bool_def  "inverse x == x::bool"
+  unit_bool_def     "1         == False"
 
 instance
   bool :: agroup                {| ALLGOALS (fast_tac HOL_cs) |}
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Tutorial/Group.ML
--- a/src/HOL/AxClasses/Tutorial/Group.ML	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Tutorial/Group.ML	Fri Apr 04 16:03:44 1997 +0200
@@ -11,27 +11,27 @@
 fun ssub r = standard (r RS ssubst);
 
 
-goal Group.thy "x <*> inv x = (1::'a::group)";
+goal Group.thy "x <*> inverse x = (1::'a::group)";
 by (rtac (sub left_unit) 1);
 back();
 by (rtac (sub assoc) 1);
-by (rtac (sub left_inv) 1);
+by (rtac (sub left_inverse) 1);
 back();
 back();
 by (rtac (ssub assoc) 1);
 back();
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (rtac (ssub assoc) 1);
 by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (rtac refl 1);
-qed "right_inv";
+qed "right_inverse";
 
 
 goal Group.thy "x <*> 1 = (x::'a::group)";
-by (rtac (sub left_inv) 1);
+by (rtac (sub left_inverse) 1);
 by (rtac (sub assoc) 1);
-by (rtac (ssub right_inv) 1);
+by (rtac (ssub right_inverse) 1);
 by (rtac (ssub left_unit) 1);
 by (rtac refl 1);
 qed "right_unit";
@@ -41,7 +41,7 @@
 by (rtac impI 1);
 by (rtac (sub right_unit) 1);
 back();
-by (res_inst_tac [("x", "x")] (sub right_inv) 1);
+by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
 by (rtac (sub assoc) 1);
 by (rtac arg_cong 1);
 back();
@@ -69,50 +69,50 @@
 qed "ex1_unit'";
 
 
-goal Group.thy "y <*> x = 1 --> y = inv (x::'a::group)";
+goal Group.thy "y <*> x = 1 --> y = inverse (x::'a::group)";
 by (rtac impI 1);
 by (rtac (sub right_unit) 1);
 back();
 back();
 by (rtac (sub right_unit) 1);
-by (res_inst_tac [("x", "x")] (sub right_inv) 1);
+by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
 by (rtac (sub assoc) 1);
 by (rtac (sub assoc) 1);
 by (rtac arg_cong 1);
 back();
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (assume_tac 1);
-qed "one_inv";
+qed "one_inverse";
 
 
 goal Group.thy "ALL x. EX! y. y <*> x = (1::'a::group)";
 by (rtac allI 1);
 by (rtac ex1I 1);
-by (rtac left_inv 1);
+by (rtac left_inverse 1);
 by (rtac mp 1);
-by (rtac one_inv 1);
+by (rtac one_inverse 1);
 by (assume_tac 1);
-qed "ex1_inv";
+qed "ex1_inverse";
 
 
-goal Group.thy "inv (x <*> y) = inv y <*> inv (x::'a::group)";
+goal Group.thy "inverse (x <*> y) = inverse y <*> inverse (x::'a::group)";
 by (rtac sym 1);
 by (rtac mp 1);
-by (rtac one_inv 1);
+by (rtac one_inverse 1);
 by (rtac (ssub assoc) 1);
 by (rtac (sub assoc) 1);
 back();
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inv) 1);
+by (rtac (ssub left_inverse) 1);
 by (rtac refl 1);
-qed "inv_product";
+qed "inverse_product";
 
 
-goal Group.thy "inv (inv x) = (x::'a::group)";
+goal Group.thy "inverse (inverse x) = (x::'a::group)";
 by (rtac sym 1);
-by (rtac (one_inv RS mp) 1);
-by (rtac (ssub right_inv) 1);
+by (rtac (one_inverse RS mp) 1);
+by (rtac (ssub right_inverse) 1);
 by (rtac refl 1);
-qed "inv_inv";
+qed "inverse_inv";
 
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Tutorial/Group.thy
--- a/src/HOL/AxClasses/Tutorial/Group.thy	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Tutorial/Group.thy	Fri Apr 04 16:03:44 1997 +0200
@@ -19,7 +19,7 @@
 axclass
   group < semigroup
   left_unit     "1 <*> x = x"
-  left_inv      "inv x <*> x = 1"
+  left_inverse  "inverse x <*> x = 1"
 
 
 (* abelian groups *)
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Tutorial/Sigs.thy
--- a/src/HOL/AxClasses/Tutorial/Sigs.thy	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Tutorial/Sigs.thy	Fri Apr 04 16:03:44 1997 +0200
@@ -9,7 +9,7 @@
 
 consts
   "<*>"         :: "['a, 'a] => 'a"             (infixl 70)
-  "inv"         :: "'a => 'a"
+  inverse       :: "'a => 'a"
   "1"           :: "'a"                         ("1")
 
 end
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Tutorial/Xor.ML
--- a/src/HOL/AxClasses/Tutorial/Xor.ML	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Tutorial/Xor.ML	Fri Apr 04 16:03:44 1997 +0200
@@ -9,6 +9,7 @@
 
 goal_arity Xor.thy ("bool", [], "agroup");
 by (axclass_tac Xor.thy []);
-by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
+by (rewrite_goals_tac
+      [Xor.prod_bool_def,Xor.inverse_bool_def, Xor.unit_bool_def]);
 by (ALLGOALS (Fast_tac));
 qed "bool_in_agroup";
diff -r 171dedbc9bdb -r 0e272e4c7cb2 src/HOL/AxClasses/Tutorial/Xor.thy
--- a/src/HOL/AxClasses/Tutorial/Xor.thy	Fri Apr 04 16:03:11 1997 +0200
+++ b/src/HOL/AxClasses/Tutorial/Xor.thy	Fri Apr 04 16:03:44 1997 +0200
@@ -2,14 +2,14 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Define overloaded constants "<*>", "inv", "1" on type "bool".
+Define overloaded constants "<*>", "inverse", "1" on type "bool".
 *)
 
 Xor = Group +
 
 defs
-  prod_bool_def "x <*> y == x ~= (y::bool)"
-  inv_bool_def  "inv x   == x::bool"
-  unit_bool_def "1       == False"
+  prod_bool_def     "x <*> y   == x ~= (y::bool)"
+  inverse_bool_def  "inverse x == x::bool"
+  unit_bool_def     "1         == False"
 
 end