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 *)
     6 
     7 theory Group = Main:
     8 
     9 subsection {* Monoids and Groups *}
    10 
    11 consts
    12   times :: "'a => 'a => 'a"    (infixl "[*]" 70)
    13   invers :: "'a => 'a"
    14   one :: 'a
    15 
    16 
    17 axclass monoid < "term"
    18   assoc:      "(x [*] y) [*] z = x [*] (y [*] z)"
    19   left_unit:  "one [*] x = x"
    20   right_unit: "x [*] one = x"
    21 
    22 axclass semigroup < "term"
    23   assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
    24 
    25 axclass group < semigroup
    26   left_unit:    "one [*] x = x"
    27   left_inverse: "invers x [*] x = one"
    28 
    29 axclass agroup < group
    30   commute: "x [*] y = y [*] x"
    31 
    32 
    33 subsection {* Abstract reasoning *}
    34 
    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
    55 
    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
    68 
    69 
    70 subsection {* Abstract instantiation *}
    71 
    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
    78 
    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
    89 
    90 
    91 subsection {* Concrete instantiation *}
    92 
    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"
    97 
    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
   107 
   108 
   109 subsection {* Lifting and Functors *}
   110 
   111 defs (overloaded)
   112   times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)"
   113 
   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
   124 
   125 end