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

src/HOL/AxClasses/Group.thy

author | wenzelm |

Mon Feb 05 20:34:05 2001 +0100 (2001-02-05) | |

changeset 11072 | 8f47967ecc80 |

parent 10681 | ec76e17f73c5 |

child 12338 | de0f4a63baa5 |

permissions | -rw-r--r-- |

tuned

1 (* Title: HOL/AxClasses/Group.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 License: GPL (GNU GENERAL PUBLIC LICENSE)

5 *)

7 theory Group = Main:

9 subsection {* Monoids and Groups *}

11 consts

12 times :: "'a => 'a => 'a" (infixl "[*]" 70)

13 invers :: "'a => 'a"

14 one :: 'a

17 axclass monoid < "term"

18 assoc: "(x [*] y) [*] z = x [*] (y [*] z)"

19 left_unit: "one [*] x = x"

20 right_unit: "x [*] one = x"

22 axclass semigroup < "term"

23 assoc: "(x [*] y) [*] z = x [*] (y [*] z)"

25 axclass group < semigroup

26 left_unit: "one [*] x = x"

27 left_inverse: "invers x [*] x = one"

29 axclass agroup < group

30 commute: "x [*] y = y [*] x"

33 subsection {* Abstract reasoning *}

35 theorem group_right_inverse: "x [*] invers x = (one::'a::group)"

36 proof -

37 have "x [*] invers x = one [*] (x [*] invers x)"

38 by (simp only: group.left_unit)

39 also have "... = one [*] x [*] invers x"

40 by (simp only: semigroup.assoc)

41 also have "... = invers (invers x) [*] invers x [*] x [*] invers x"

42 by (simp only: group.left_inverse)

43 also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x"

44 by (simp only: semigroup.assoc)

45 also have "... = invers (invers x) [*] one [*] invers x"

46 by (simp only: group.left_inverse)

47 also have "... = invers (invers x) [*] (one [*] invers x)"

48 by (simp only: semigroup.assoc)

49 also have "... = invers (invers x) [*] invers x"

50 by (simp only: group.left_unit)

51 also have "... = one"

52 by (simp only: group.left_inverse)

53 finally show ?thesis .

54 qed

56 theorem group_right_unit: "x [*] one = (x::'a::group)"

57 proof -

58 have "x [*] one = x [*] (invers x [*] x)"

59 by (simp only: group.left_inverse)

60 also have "... = x [*] invers x [*] x"

61 by (simp only: semigroup.assoc)

62 also have "... = one [*] x"

63 by (simp only: group_right_inverse)

64 also have "... = x"

65 by (simp only: group.left_unit)

66 finally show ?thesis .

67 qed

70 subsection {* Abstract instantiation *}

72 instance monoid < semigroup

73 proof intro_classes

74 fix x y z :: "'a::monoid"

75 show "x [*] y [*] z = x [*] (y [*] z)"

76 by (rule monoid.assoc)

77 qed

79 instance group < monoid

80 proof intro_classes

81 fix x y z :: "'a::group"

82 show "x [*] y [*] z = x [*] (y [*] z)"

83 by (rule semigroup.assoc)

84 show "one [*] x = x"

85 by (rule group.left_unit)

86 show "x [*] one = x"

87 by (rule group_right_unit)

88 qed

91 subsection {* Concrete instantiation *}

93 defs (overloaded)

94 times_bool_def: "x [*] y == x ~= (y::bool)"

95 inverse_bool_def: "invers x == x::bool"

96 unit_bool_def: "one == False"

98 instance bool :: agroup

99 proof (intro_classes,

100 unfold times_bool_def inverse_bool_def unit_bool_def)

101 fix x y z

102 show "((x ~= y) ~= z) = (x ~= (y ~= z))" by blast

103 show "(False ~= x) = x" by blast

104 show "(x ~= x) = False" by blast

105 show "(x ~= y) = (y ~= x)" by blast

106 qed

109 subsection {* Lifting and Functors *}

111 defs (overloaded)

112 times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)"

114 instance * :: (semigroup, semigroup) semigroup

115 proof (intro_classes, unfold times_prod_def)

116 fix p q r :: "'a::semigroup * 'b::semigroup"

117 show

118 "(fst (fst p [*] fst q, snd p [*] snd q) [*] fst r,

119 snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) =

120 (fst p [*] fst (fst q [*] fst r, snd q [*] snd r),

121 snd p [*] snd (fst q [*] fst r, snd q [*] snd r))"

122 by (simp add: semigroup.assoc)

123 qed

125 end