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  
    1.65  defs (overloaded)
    1.66    times_bool_def:   "x [*] y == x ~= (y::bool)"
    1.67 -  inverse_bool_def: "inverse x == x::bool"
    1.68 +  inverse_bool_def: "invers x == x::bool"
    1.69    unit_bool_def:    "one == False"
    1.70  
    1.71  instance bool :: agroup