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
wenzelm@10134
     1
(*  Title:      HOL/AxClasses/Group.thy
wenzelm@10134
     2
    ID:         $Id$
wenzelm@10134
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10681
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@10134
     5
*)
wenzelm@10134
     6
wenzelm@10134
     7
theory Group = Main:
wenzelm@10134
     8
wenzelm@10134
     9
subsection {* Monoids and Groups *}
wenzelm@10134
    10
wenzelm@10134
    11
consts
wenzelm@10134
    12
  times :: "'a => 'a => 'a"    (infixl "[*]" 70)
wenzelm@11072
    13
  invers :: "'a => 'a"
wenzelm@10134
    14
  one :: 'a
wenzelm@10134
    15
wenzelm@10134
    16
wenzelm@10134
    17
axclass monoid < "term"
wenzelm@10134
    18
  assoc:      "(x [*] y) [*] z = x [*] (y [*] z)"
wenzelm@10134
    19
  left_unit:  "one [*] x = x"
wenzelm@10134
    20
  right_unit: "x [*] one = x"
wenzelm@10134
    21
wenzelm@10134
    22
axclass semigroup < "term"
wenzelm@10134
    23
  assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
wenzelm@10134
    24
wenzelm@10134
    25
axclass group < semigroup
wenzelm@10134
    26
  left_unit:    "one [*] x = x"
wenzelm@11072
    27
  left_inverse: "invers x [*] x = one"
wenzelm@10134
    28
wenzelm@10134
    29
axclass agroup < group
wenzelm@10134
    30
  commute: "x [*] y = y [*] x"
wenzelm@10134
    31
wenzelm@10134
    32
wenzelm@10134
    33
subsection {* Abstract reasoning *}
wenzelm@10134
    34
wenzelm@11072
    35
theorem group_right_inverse: "x [*] invers x = (one::'a::group)"
wenzelm@10134
    36
proof -
wenzelm@11072
    37
  have "x [*] invers x = one [*] (x [*] invers x)"
wenzelm@10134
    38
    by (simp only: group.left_unit)
wenzelm@11072
    39
  also have "... = one [*] x [*] invers x"
wenzelm@10134
    40
    by (simp only: semigroup.assoc)
wenzelm@11072
    41
  also have "... = invers (invers x) [*] invers x [*] x [*] invers x"
wenzelm@10134
    42
    by (simp only: group.left_inverse)
wenzelm@11072
    43
  also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x"
wenzelm@10134
    44
    by (simp only: semigroup.assoc)
wenzelm@11072
    45
  also have "... = invers (invers x) [*] one [*] invers x"
wenzelm@10134
    46
    by (simp only: group.left_inverse)
wenzelm@11072
    47
  also have "... = invers (invers x) [*] (one [*] invers x)"
wenzelm@10134
    48
    by (simp only: semigroup.assoc)
wenzelm@11072
    49
  also have "... = invers (invers x) [*] invers x"
wenzelm@10134
    50
    by (simp only: group.left_unit)
wenzelm@10134
    51
  also have "... = one"
wenzelm@10134
    52
    by (simp only: group.left_inverse)
wenzelm@10134
    53
  finally show ?thesis .
wenzelm@10134
    54
qed
wenzelm@10134
    55
wenzelm@10134
    56
theorem group_right_unit: "x [*] one = (x::'a::group)"
wenzelm@10134
    57
proof -
wenzelm@11072
    58
  have "x [*] one = x [*] (invers x [*] x)"
wenzelm@10134
    59
    by (simp only: group.left_inverse)
wenzelm@11072
    60
  also have "... = x [*] invers x [*] x"
wenzelm@10134
    61
    by (simp only: semigroup.assoc)
wenzelm@10134
    62
  also have "... = one [*] x"
wenzelm@10134
    63
    by (simp only: group_right_inverse)
wenzelm@10134
    64
  also have "... = x"
wenzelm@10134
    65
    by (simp only: group.left_unit)
wenzelm@10134
    66
  finally show ?thesis .
wenzelm@10134
    67
qed
wenzelm@10134
    68
wenzelm@10134
    69
wenzelm@10134
    70
subsection {* Abstract instantiation *}
wenzelm@10134
    71
wenzelm@10134
    72
instance monoid < semigroup
wenzelm@10134
    73
proof intro_classes
wenzelm@10134
    74
  fix x y z :: "'a::monoid"
wenzelm@10134
    75
  show "x [*] y [*] z = x [*] (y [*] z)"
wenzelm@10134
    76
    by (rule monoid.assoc)
wenzelm@10134
    77
qed
wenzelm@10134
    78
wenzelm@10134
    79
instance group < monoid
wenzelm@10134
    80
proof intro_classes
wenzelm@10134
    81
  fix x y z :: "'a::group"
wenzelm@10134
    82
  show "x [*] y [*] z = x [*] (y [*] z)"
wenzelm@10134
    83
    by (rule semigroup.assoc)
wenzelm@10134
    84
  show "one [*] x = x"
wenzelm@10134
    85
    by (rule group.left_unit)
wenzelm@10134
    86
  show "x [*] one = x"
wenzelm@10134
    87
    by (rule group_right_unit)
wenzelm@10134
    88
qed
wenzelm@10134
    89
wenzelm@10134
    90
wenzelm@10134
    91
subsection {* Concrete instantiation *}
wenzelm@10134
    92
wenzelm@10134
    93
defs (overloaded)
wenzelm@10134
    94
  times_bool_def:   "x [*] y == x ~= (y::bool)"
wenzelm@11072
    95
  inverse_bool_def: "invers x == x::bool"
wenzelm@10134
    96
  unit_bool_def:    "one == False"
wenzelm@10134
    97
wenzelm@10134
    98
instance bool :: agroup
wenzelm@10134
    99
proof (intro_classes,
wenzelm@10134
   100
    unfold times_bool_def inverse_bool_def unit_bool_def)
wenzelm@10134
   101
  fix x y z
wenzelm@10134
   102
  show "((x ~= y) ~= z) = (x ~= (y ~= z))" by blast
wenzelm@10134
   103
  show "(False ~= x) = x" by blast
wenzelm@10134
   104
  show "(x ~= x) = False" by blast
wenzelm@10134
   105
  show "(x ~= y) = (y ~= x)" by blast
wenzelm@10134
   106
qed
wenzelm@10134
   107
wenzelm@10134
   108
wenzelm@10134
   109
subsection {* Lifting and Functors *}
wenzelm@10134
   110
wenzelm@10134
   111
defs (overloaded)
wenzelm@10134
   112
  times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)"
wenzelm@10134
   113
wenzelm@10134
   114
instance * :: (semigroup, semigroup) semigroup
wenzelm@10134
   115
proof (intro_classes, unfold times_prod_def)
wenzelm@10134
   116
  fix p q r :: "'a::semigroup * 'b::semigroup"
wenzelm@10134
   117
  show
wenzelm@10134
   118
    "(fst (fst p [*] fst q, snd p [*] snd q) [*] fst r,
wenzelm@10134
   119
      snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) =
wenzelm@10134
   120
       (fst p [*] fst (fst q [*] fst r, snd q [*] snd r),
wenzelm@10134
   121
        snd p [*] snd (fst q [*] fst r, snd q [*] snd r))"
wenzelm@10134
   122
    by (simp add: semigroup.assoc)
wenzelm@10134
   123
qed
wenzelm@10134
   124
wenzelm@10134
   125
end