Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/AxClasses/Group/GroupInsts.thy
author paulson
Tue, 16 Jul 1996 15:49:46 +0200
changeset 1868 836950047d85
parent 1247 18b1441fb603
child 2907 0e272e4c7cb2
permissions -rw-r--r--
Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML

(*  Title:      GroupInsts.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Some concrete instantiations: 'structures' and 'functors'.
*)

GroupInsts = GroupDefs +


(* bool *)

instance
  bool :: semigroup                     (bool_assoc)
instance
  bool :: monoid                        (bool_assoc, bool_left_unit, bool_right_unit)
instance
  bool :: group                         (bool_left_unit, bool_left_inv)
instance
  bool :: agroup                        (bool_commut)


(* cartesian products *)

instance
  "*" :: (semigroup, semigroup) semigroup       (prod_assoc)
instance
  "*" :: (monoid, monoid) monoid                (prod_assoc, prod_left_unit, prod_right_unit)
instance
  "*" :: (group, group) group                   (prod_left_unit, prod_left_inv)
instance
  "*" :: (agroup, agroup) agroup                (prod_commut)


(* function spaces *)

instance
  fun :: (term, semigroup) semigroup            (fun_assoc)
instance
  fun :: (term, monoid) monoid                  (fun_assoc, fun_left_unit, fun_right_unit)
instance
  fun :: (term, group) group                    (fun_left_unit, fun_left_inv)
instance
  fun :: (term, agroup) agroup                  (fun_commut)

end
isabelle