summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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