--- 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";
--- 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 *)
--- 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);
--- 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
--- 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
--- 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
--- 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) |}
--- 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";
--- 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 *)
--- 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
--- 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";
--- 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