src/HOL/AxClasses/Group.thy
 changeset 11072 8f47967ecc80 parent 10681 ec76e17f73c5 child 12338 de0f4a63baa5
```     1.1 --- a/src/HOL/AxClasses/Group.thy	Mon Feb 05 20:33:50 2001 +0100
1.2 +++ b/src/HOL/AxClasses/Group.thy	Mon Feb 05 20:34:05 2001 +0100
1.3 @@ -10,7 +10,7 @@
1.4
1.5  consts
1.6    times :: "'a => 'a => 'a"    (infixl "[*]" 70)
1.7 -  inverse :: "'a => 'a"
1.8 +  invers :: "'a => 'a"
1.9    one :: 'a
1.10
1.11
1.12 @@ -24,7 +24,7 @@
1.13
1.14  axclass group < semigroup
1.15    left_unit:    "one [*] x = x"
1.16 -  left_inverse: "inverse x [*] x = one"
1.17 +  left_inverse: "invers x [*] x = one"
1.18
1.19  axclass agroup < group
1.20    commute: "x [*] y = y [*] x"
1.21 @@ -32,21 +32,21 @@
1.22
1.23  subsection {* Abstract reasoning *}
1.24
1.25 -theorem group_right_inverse: "x [*] inverse x = (one::'a::group)"
1.26 +theorem group_right_inverse: "x [*] invers x = (one::'a::group)"
1.27  proof -
1.28 -  have "x [*] inverse x = one [*] (x [*] inverse x)"
1.29 +  have "x [*] invers x = one [*] (x [*] invers x)"
1.30      by (simp only: group.left_unit)
1.31 -  also have "... = one [*] x [*] inverse x"
1.32 +  also have "... = one [*] x [*] invers x"
1.33      by (simp only: semigroup.assoc)
1.34 -  also have "... = inverse (inverse x) [*] inverse x [*] x [*] inverse x"
1.35 +  also have "... = invers (invers x) [*] invers x [*] x [*] invers x"
1.36      by (simp only: group.left_inverse)
1.37 -  also have "... = inverse (inverse x) [*] (inverse x [*] x) [*] inverse x"
1.38 +  also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x"
1.39      by (simp only: semigroup.assoc)
1.40 -  also have "... = inverse (inverse x) [*] one [*] inverse x"
1.41 +  also have "... = invers (invers x) [*] one [*] invers x"
1.42      by (simp only: group.left_inverse)
1.43 -  also have "... = inverse (inverse x) [*] (one [*] inverse x)"
1.44 +  also have "... = invers (invers x) [*] (one [*] invers x)"
1.45      by (simp only: semigroup.assoc)
1.46 -  also have "... = inverse (inverse x) [*] inverse x"
1.47 +  also have "... = invers (invers x) [*] invers x"
1.48      by (simp only: group.left_unit)
1.49    also have "... = one"
1.50      by (simp only: group.left_inverse)
1.51 @@ -55,9 +55,9 @@
1.52
1.53  theorem group_right_unit: "x [*] one = (x::'a::group)"
1.54  proof -
1.55 -  have "x [*] one = x [*] (inverse x [*] x)"
1.56 +  have "x [*] one = x [*] (invers x [*] x)"
1.57      by (simp only: group.left_inverse)
1.58 -  also have "... = x [*] inverse x [*] x"
1.59 +  also have "... = x [*] invers x [*] x"
1.60      by (simp only: semigroup.assoc)
1.61    also have "... = one [*] x"
1.62      by (simp only: group_right_inverse)
1.63 @@ -92,7 +92,7 @@
1.64