src/HOL/AxClasses/Group/GroupDefs.ML
changeset 2907 0e272e4c7cb2
parent 1899 0075a8d26a80
child 4091 771b1f6422a8
     1.1 --- a/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Apr 04 16:03:11 1997 +0200
     1.2 +++ b/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Apr 04 16:03:44 1997 +0200
     1.3 @@ -1,7 +1,3 @@
     1.4 -
     1.5 -open GroupDefs;
     1.6 -
     1.7 -
     1.8  (* bool *)
     1.9  
    1.10  (*this is really overkill - should be rather proven 'inline'*)
    1.11 @@ -18,9 +14,10 @@
    1.12  by (Fast_tac 1);
    1.13  qed "bool_right_unit";
    1.14  
    1.15 -goalw thy [times_bool_def, inv_bool_def, one_bool_def] "inv(x) * x = (1::bool)";
    1.16 +goalw thy [times_bool_def, inverse_bool_def, one_bool_def]
    1.17 +  "inverse(x) * x = (1::bool)";
    1.18  by (Fast_tac 1);
    1.19 -qed "bool_left_inv";
    1.20 +qed "bool_left_inverse";
    1.21  
    1.22  goalw thy [times_bool_def] "x * y = (y * (x::bool))";
    1.23  by (Fast_tac 1);
    1.24 @@ -31,7 +28,8 @@
    1.25  
    1.26  val prod_ss = simpset_of "Prod";
    1.27  
    1.28 -goalw thy [times_prod_def] "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))";
    1.29 +goalw thy [times_prod_def]
    1.30 +  "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))";
    1.31  by (simp_tac (prod_ss addsimps [assoc]) 1);
    1.32  qed "prod_assoc";
    1.33  
    1.34 @@ -45,9 +43,10 @@
    1.35  by (rtac (surjective_pairing RS sym) 1);
    1.36  qed "prod_right_unit";
    1.37  
    1.38 -goalw thy [times_prod_def, inv_prod_def, one_prod_def] "inv x * x = (1::'a::group*'b::group)";
    1.39 -by (simp_tac (prod_ss addsimps [left_inv]) 1);
    1.40 -qed "prod_left_inv";
    1.41 +goalw thy [times_prod_def, inverse_prod_def, one_prod_def]
    1.42 +  "inverse x * x = (1::'a::group*'b::group)";
    1.43 +by (simp_tac (prod_ss addsimps [left_inverse]) 1);
    1.44 +qed "prod_left_inverse";
    1.45  
    1.46  goalw thy [times_prod_def] "x * y = y * (x::'a::agroup*'b::agroup)";
    1.47  by (simp_tac (prod_ss addsimps [commut]) 1);
    1.48 @@ -74,11 +73,12 @@
    1.49  by (rtac Monoid.right_unit 1);
    1.50  qed "fun_right_unit";
    1.51  
    1.52 -goalw thy [times_fun_def, inv_fun_def, one_fun_def] "inv x * x = (1::'a => 'b::group)";
    1.53 +goalw thy [times_fun_def, inverse_fun_def, one_fun_def]
    1.54 +  "inverse x * x = (1::'a => 'b::group)";
    1.55  by (stac expand_fun_eq 1);
    1.56  by (rtac allI 1);
    1.57 -by (rtac left_inv 1);
    1.58 -qed "fun_left_inv";
    1.59 +by (rtac left_inverse 1);
    1.60 +qed "fun_left_inverse";
    1.61  
    1.62  goalw thy [times_fun_def] "x * y = y * (x::'a => 'b::agroup)";
    1.63  by (stac expand_fun_eq 1);