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