# HG changeset patch
# User wenzelm
# Date 809958456 -7200
# Node ID 18b1441fb603855660e33fb00b44033cfc8b6860
# Parent  706cfddca75c59c5b0116133376a713dd6eac583
Various axiomatic type class demos;

diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Group/Group.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group/Group.ML	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,132 @@
+(*  Title:      HOL/AxClasses/Group/Group.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some basic theorems of group theory.
+*)
+
+open Group;
+
+fun sub r = standard (r RS subst);
+fun ssub r = standard (r RS ssubst);
+
+
+goal thy "x * inv x = (1::'a::group)";
+br (sub left_unit) 1;
+back();
+br (sub assoc) 1;
+br (sub left_inv) 1;
+back();
+back();
+br (ssub assoc) 1;
+back();
+br (ssub left_inv) 1;
+br (ssub assoc) 1;
+br (ssub left_unit) 1;
+br (ssub left_inv) 1;
+br refl 1;
+qed "right_inv";
+
+
+goal thy "x * 1 = (x::'a::group)";
+br (sub left_inv) 1;
+br (sub assoc) 1;
+br (ssub right_inv) 1;
+br (ssub left_unit) 1;
+br refl 1;
+qed "right_unit";
+
+
+goal thy "e * x = x --> e = (1::'a::group)";
+br impI 1;
+br (sub right_unit) 1;
+back();
+by (res_inst_tac [("x", "x")] (sub right_inv) 1);
+br (sub assoc) 1;
+br arg_cong 1;
+back();
+ba 1;
+qed "strong_one_unit";
+
+
+goal thy "EX! e. ALL x. e * x = (x::'a::group)";
+br ex1I 1;
+br allI 1;
+br left_unit 1;
+br mp 1;
+br strong_one_unit 1;
+be allE 1;
+ba 1;
+qed "ex1_unit";
+
+
+goal thy "ALL x. EX! e. e * x = (x::'a::group)";
+br allI 1;
+br ex1I 1;
+br left_unit 1;
+br (strong_one_unit RS mp) 1;
+ba 1;
+qed "ex1_unit'";
+
+
+goal thy "inj (op * (x::'a::group))";
+br injI 1;
+br (sub left_unit) 1;
+back();
+br (sub left_unit) 1;
+by (res_inst_tac [("x", "x")] (sub left_inv) 1);
+br (ssub assoc) 1;
+back();
+br (ssub assoc) 1;
+br arg_cong 1;
+back();
+ba 1;
+qed "inj_times";
+
+
+goal thy "y * x = 1 --> y = inv (x::'a::group)";
+br impI 1;
+br (sub right_unit) 1;
+back();
+back();
+br (sub right_unit) 1;
+by (res_inst_tac [("x", "x")] (sub right_inv) 1);
+br (sub assoc) 1;
+br (sub assoc) 1;
+br arg_cong 1;
+back();
+br (ssub left_inv) 1;
+ba 1;
+qed "one_inv";
+
+
+goal thy "ALL x. EX! y. y * x = (1::'a::group)";
+br allI 1;
+br ex1I 1;
+br left_inv 1;
+br mp 1;
+br one_inv 1;
+ba 1;
+qed "ex1_inv";
+
+
+goal thy "inv (x * y) = inv y * inv (x::'a::group)";
+br sym 1;
+br mp 1;
+br one_inv 1;
+br (ssub assoc) 1;
+br (sub assoc) 1;
+back();
+br (ssub left_inv) 1;
+br (ssub left_unit) 1;
+br (ssub left_inv) 1;
+br refl 1;
+qed "inv_times";
+
+
+goal thy "inv (inv x) = (x::'a::group)";
+br sym 1;
+br (one_inv RS mp) 1;
+br (ssub right_inv) 1;
+br refl 1;
+qed "inv_inv";
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Group/Group.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group/Group.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,29 @@
+(*  Title:      Group.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+*)
+
+Group = Sigs + Set +
+
+(* semigroups *)
+
+axclass
+  semigroup < times
+  assoc         "(x * y) * z = x * (y * z)"
+
+
+(* groups *)
+
+axclass
+  group < one, inv, semigroup
+  left_unit     "1 * x = x"
+  left_inv      "inv x * x = 1"
+
+
+(* abelian groups *)
+
+axclass
+  agroup < group
+  commut        "x * y = y * x"
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Group/GroupDefs.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,85 @@
+
+open GroupDefs;
+
+
+(* bool *)
+
+(*this is really overkill - should be rather proven 'inline'*)
+
+goalw thy [times_bool_def] "(x * y) * z = x * (y * (z::bool))";
+by (fast_tac HOL_cs 1);
+qed "bool_assoc";
+
+goalw thy [times_bool_def, one_bool_def] "1 * x = (x::bool)";
+by (fast_tac HOL_cs 1);
+qed "bool_left_unit";
+
+goalw thy [times_bool_def, one_bool_def] "x * 1 = (x::bool)";
+by (fast_tac HOL_cs 1);
+qed "bool_right_unit";
+
+goalw thy [times_bool_def, inv_bool_def, one_bool_def] "inv(x) * x = (1::bool)";
+by (fast_tac HOL_cs 1);
+qed "bool_left_inv";
+
+goalw thy [times_bool_def] "x * y = (y * (x::bool))";
+by (fast_tac HOL_cs 1);
+qed "bool_commut";
+
+
+(* cartesian products *)
+
+goalw thy [times_prod_def] "(x * y) * z = x * (y * (z::'a::semigroup*'b::semigroup))";
+by (simp_tac (prod_ss addsimps [assoc]) 1);
+qed "prod_assoc";
+
+goalw thy [times_prod_def, one_prod_def] "1 * x = (x::'a::monoid*'b::monoid)";
+by (simp_tac (prod_ss addsimps [Monoid.left_unit]) 1);
+br (surjective_pairing RS sym) 1;
+qed "prod_left_unit";
+
+goalw thy [times_prod_def, one_prod_def] "x * 1 = (x::'a::monoid*'b::monoid)";
+by (simp_tac (prod_ss addsimps [Monoid.right_unit]) 1);
+br (surjective_pairing RS sym) 1;
+qed "prod_right_unit";
+
+goalw thy [times_prod_def, inv_prod_def, one_prod_def] "inv x * x = (1::'a::group*'b::group)";
+by (simp_tac (prod_ss addsimps [left_inv]) 1);
+qed "prod_left_inv";
+
+goalw thy [times_prod_def] "x * y = y * (x::'a::agroup*'b::agroup)";
+by (simp_tac (prod_ss addsimps [commut]) 1);
+qed "prod_commut";
+
+
+(* function spaces *)
+
+goalw thy [times_fun_def] "(x * y) * z = x * (y * (z::'a => 'b::semigroup))";
+by (stac expand_fun_eq 1);
+br allI 1;
+br assoc 1;
+qed "fun_assoc";
+
+goalw thy [times_fun_def, one_fun_def] "1 * x = (x::'a => 'b::monoid)";
+by (stac expand_fun_eq 1);
+br allI 1;
+br Monoid.left_unit 1;
+qed "fun_left_unit";
+
+goalw thy [times_fun_def, one_fun_def] "x * 1 = (x::'a => 'b::monoid)";
+by (stac expand_fun_eq 1);
+br allI 1;
+br Monoid.right_unit 1;
+qed "fun_right_unit";
+
+goalw thy [times_fun_def, inv_fun_def, one_fun_def] "inv x * x = (1::'a => 'b::group)";
+by (stac expand_fun_eq 1);
+br allI 1;
+br left_inv 1;
+qed "fun_left_inv";
+
+goalw thy [times_fun_def] "x * y = y * (x::'a => 'b::agroup)";
+by (stac expand_fun_eq 1);
+br allI 1;
+br commut 1;
+qed "fun_commut";
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Group/GroupDefs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group/GroupDefs.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,41 @@
+(*  Title:      GroupDefs.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+*)
+
+GroupDefs = MonoidGroupInsts + Prod + Fun +
+
+
+(* bool *)
+
+instance
+  bool :: {times, inv, one}
+
+defs
+  times_bool_def        "x * y == (x ~= y)"
+  inv_bool_def          "inv x == (x::bool)"
+  one_bool_def          "1 == False"
+
+
+(* cartesian products *)
+
+instance
+  "*" :: (term, term) {times, inv, one}
+
+defs
+  times_prod_def        "p * q == (fst p * fst q, snd p * snd q)"
+  inv_prod_def          "inv p == (inv (fst p), inv (snd p))"
+  one_prod_def          "1 == (1, 1)"
+
+
+(* function spaces *)
+
+instance
+  fun :: (term, term) {times, inv, one}
+
+defs
+  times_fun_def         "f * g == (%x. f x * g x)"
+  inv_fun_def           "inv f == (%x. inv (f x))"
+  one_fun_def           "1 == (%x. 1)"
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Group/GroupInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group/GroupInsts.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,46 @@
+(*  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
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Group/Monoid.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group/Monoid.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Monoid.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+*)
+
+Monoid = Sigs +
+
+(* monoids *)
+
+axclass
+  monoid < times, one
+  assoc         "(x * y) * z = x * (y * z)"
+  left_unit     "1 * x = x"
+  right_unit    "x * 1 = x"
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Group/MonoidGroupInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group/MonoidGroupInsts.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,22 @@
+(*  Title:      MonoidGroupInsts.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some class inclusions or 'abstract instantiations'.
+*)
+
+MonoidGroupInsts = Group + Monoid +
+
+
+(* monoids are semigroups *)
+
+instance
+  monoid < semigroup            (Monoid.assoc)
+
+
+(* groups are monoids *)
+
+instance
+  group < monoid                (assoc, left_unit, right_unit)
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Group/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group/ROOT.ML	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,27 @@
+(*  Title:      HOL/AxClasses/Group/ROOT.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+(* FIXME comment *)
+Elementary algebra via axiomatic type classes.
+*)
+
+reset HOL_quantifiers;
+set show_types;
+set show_sorts;
+
+(*disable bug compatibility*)
+reset force_strip_shyps;
+
+set force_strip_shyps;(* FIXME tmp hack *)
+
+
+use_thy "Sigs";
+
+use_thy "Monoid";
+use_thy "Group";
+
+use_thy "MonoidGroupInsts";
+
+use_thy "GroupDefs";
+use_thy "GroupInsts";
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Group/Sigs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group/Sigs.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,18 @@
+(*  Title:      Sigs.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+*)
+
+Sigs = HOL +
+
+axclass
+  inv < term
+
+axclass
+  one < term
+
+consts
+  "inv" :: "'a::inv => 'a"
+  "1"   :: "'a::one"                    ("1")
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/README	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,11 @@
+
+$id$
+
+This directory contains some axiomatic type class demos.
+
+
+  Tutorial/     Some simple axclass demos that go along with the paper
+                "Using Axiomatic Type Classes in Isabelle --- a
+                tutorial".
+
+  Group/        Basic group theory with axiomatic type classes.
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,23 @@
+(*  Title:      HOL/AxClasses/Tutorial/BoolGroupInsts.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Define overloaded constants "<*>", "inv", "1" on type "bool"
+appropriately, then prove that this forms a group.
+*)
+
+BoolGroupInsts = Group +
+
+(* bool as abelian group *)
+
+defs
+  prod_bool_def "x <*> y == x ~= (y::bool)"
+  inv_bool_def  "inv x   == x::bool"
+  unit_bool_def "1       == False"
+
+instance
+  bool :: agroup                {| ALLGOALS (fast_tac HOL_cs) |}
+  (*"instance" automatically uses above defs, 
+    the remaining goals are proven 'inline'*)
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Group.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Group.ML	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,118 @@
+(*  Title:      HOL/AxClasses/Tutorial/Group.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some basic theorems of group theory.
+*)
+
+open Group;
+
+fun sub r = standard (r RS subst);
+fun ssub r = standard (r RS ssubst);
+
+
+goal Group.thy "x <*> inv x = (1::'a::group)";
+br (sub left_unit) 1;
+back();
+br (sub assoc) 1;
+br (sub left_inv) 1;
+back();
+back();
+br (ssub assoc) 1;
+back();
+br (ssub left_inv) 1;
+br (ssub assoc) 1;
+br (ssub left_unit) 1;
+br (ssub left_inv) 1;
+br refl 1;
+qed "right_inv";
+
+
+goal Group.thy "x <*> 1 = (x::'a::group)";
+br (sub left_inv) 1;
+br (sub assoc) 1;
+br (ssub right_inv) 1;
+br (ssub left_unit) 1;
+br refl 1;
+qed "right_unit";
+
+
+goal Group.thy "e <*> x = x --> e = (1::'a::group)";
+br impI 1;
+br (sub right_unit) 1;
+back();
+by (res_inst_tac [("x", "x")] (sub right_inv) 1);
+br (sub assoc) 1;
+br arg_cong 1;
+back();
+ba 1;
+qed "strong_one_unit";
+
+
+goal Group.thy "EX! e. ALL x. e <*> x = (x::'a::group)";
+br ex1I 1;
+br allI 1;
+br left_unit 1;
+br mp 1;
+br strong_one_unit 1;
+be allE 1;
+ba 1;
+qed "ex1_unit";
+
+
+goal Group.thy "ALL x. EX! e. e <*> x = (x::'a::group)";
+br allI 1;
+br ex1I 1;
+br left_unit 1;
+br (strong_one_unit RS mp) 1;
+ba 1;
+qed "ex1_unit'";
+
+
+goal Group.thy "y <*> x = 1 --> y = inv (x::'a::group)";
+br impI 1;
+br (sub right_unit) 1;
+back();
+back();
+br (sub right_unit) 1;
+by (res_inst_tac [("x", "x")] (sub right_inv) 1);
+br (sub assoc) 1;
+br (sub assoc) 1;
+br arg_cong 1;
+back();
+br (ssub left_inv) 1;
+ba 1;
+qed "one_inv";
+
+
+goal Group.thy "ALL x. EX! y. y <*> x = (1::'a::group)";
+br allI 1;
+br ex1I 1;
+br left_inv 1;
+br mp 1;
+br one_inv 1;
+ba 1;
+qed "ex1_inv";
+
+
+goal Group.thy "inv (x <*> y) = inv y <*> inv (x::'a::group)";
+br sym 1;
+br mp 1;
+br one_inv 1;
+br (ssub assoc) 1;
+br (sub assoc) 1;
+back();
+br (ssub left_inv) 1;
+br (ssub left_unit) 1;
+br (ssub left_inv) 1;
+br refl 1;
+qed "inv_product";
+
+
+goal Group.thy "inv (inv x) = (x::'a::group)";
+br sym 1;
+br (one_inv RS mp) 1;
+br (ssub right_inv) 1;
+br refl 1;
+qed "inv_inv";
+
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Group.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Group.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,31 @@
+(*  Title:      HOL/AxClasses/Tutorial/Group.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Define classes "semigroup", "group", "agroup".
+*)
+
+Group = Sigs +
+
+(* semigroups *)
+
+axclass
+  semigroup < term
+  assoc         "(x <*> y) <*> z = x <*> (y <*> z)"
+
+
+(* groups *)
+
+axclass
+  group < semigroup
+  left_unit     "1 <*> x = x"
+  left_inv      "inv x <*> x = 1"
+
+
+(* abelian groups *)
+
+axclass
+  agroup < group
+  commut        "x <*> y = y <*> x"
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Monoid.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Monoid.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,18 @@
+(*  Title:      HOL/AxClasses/Tutorial/Monoid.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Define class "monoid".
+*)
+
+Monoid = Sigs +
+
+(* monoids *)
+
+axclass
+  monoid < term
+  assoc         "(x <*> y) <*> z = x <*> (y <*> z)"
+  left_unit     "1 <*> x = x"
+  right_unit    "x <*> 1 = x"
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/MonoidGroupInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/MonoidGroupInsts.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,22 @@
+(*  Title:      HOL/AxClass/Tutorial/MonoidGroupInsts.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Add derived class inclusions monoid < semigroup and group < monoid to
+type signature -- some kind of 'abstract instantiations'.
+*)
+
+MonoidGroupInsts = Monoid + Group +
+
+(* monoids are semigroups *)
+
+instance
+  monoid < semigroup            (Monoid.assoc)
+
+
+(* groups are monoids *)
+
+instance
+  group < monoid                (assoc, left_unit, right_unit)
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/ProdGroupInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/ProdGroupInsts.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,20 @@
+(*  Title:      HOL/AxClasses/Tutorial/ProdGroupInsts.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Lift constant "<*>" to cartesian products, then prove that the
+'functor' "*" maps semigroups into semigroups.
+*)
+
+ProdGroupInsts = Prod + Group +
+
+(* direct products of semigroups *)
+
+defs
+  prod_prod_def "p <*> q == (fst p <*> fst q, snd p <*> snd q)"
+
+instance
+  "*" :: (semigroup, semigroup) semigroup
+    {| simp_tac (prod_ss addsimps [assoc]) 1 |}
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Product.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Product.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,17 @@
+(*  Title:      HOL/AxClasses/Tutorial/Product.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Define a 'syntactic' class "product" that is logically equivalent to
+"term".
+*)
+
+Product = HOL +
+
+axclass
+  product < term
+
+consts
+  "<*>" :: "['a::product, 'a] => 'a"      (infixl 70)
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/ProductInsts.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/ProductInsts.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,19 @@
+(*  Title:      HOL/AxClasses/Tutorial/ProductInsts.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Instantiate the 'syntactic' class "product", then define "<*>" on type
+"bool".
+
+Note: This may look like Haskell-instance, but is not quite the same!
+*)
+
+ProductInsts = Product +
+
+instance
+  bool :: product
+
+defs
+  prod_bool_def "x <*> y  == x & y::bool"
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/ROOT.ML	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,35 @@
+(*  Title:      HOL/AxClasses/Tutorial/ROOT.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some simple axclass demos that go along with the paper "Using
+Axiomatic Type Classes in Isabelle --- a tutorial".  (The NatClass
+example resides in directory FOL/ex/.)
+*)
+
+reset HOL_quantifiers;
+set show_types;
+set show_sorts;
+
+
+(* Semigroups *)
+
+use_thy "Semigroup";
+use_thy "Semigroups";
+
+
+(* Basic group theory *)
+
+use_thy "Sigs";
+use_thy "Monoid";
+use_thy "Group";
+use_thy "MonoidGroupInsts";
+use_thy "Xor";
+use_thy "BoolGroupInsts";
+use_thy "ProdGroupInsts";
+
+
+(* Syntactic classes *)
+
+use_thy "Product";
+use_thy "ProductInsts";
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Semigroup.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Semigroup.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,17 @@
+(*  Title:      HOL/AxClasses/Tutorial/Semigroup.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Define class "semigroup".
+*)
+
+Semigroup = HOL +
+
+consts
+  "<*>"         :: "['a, 'a] => 'a"             (infixl 70)
+
+axclass
+  semigroup < term
+  assoc         "(x <*> y) <*> z = x <*> (y <*> z)"
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Semigroups.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Semigroups.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,32 @@
+(*  Title:      HOL/AxClasses/Tutorial/Semigroups.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Semigroups with different 'signatures'.
+*)
+
+Semigroups = HOL +
+
+consts
+  "<+>"         :: "['a, 'a] => 'a"             (infixl 65)
+  "<*>"         :: "['a, 'a] => 'a"             (infixl 70)
+  assoc         :: "(['a, 'a] => 'a) => bool"
+
+defs
+  assoc_def     "assoc f == ALL x y z. f (f x y) z = f x (f y z)"
+
+
+(* semigroups with op <+> *)
+
+axclass
+  plus_sg < term
+  plus_assoc    "assoc (op <+>)"
+
+
+(* semigroups with op <*> *)
+
+axclass
+  times_sg < term
+  times_assoc   "assoc (op <*>)"
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Sigs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Sigs.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,15 @@
+(*  Title:      HOL/AxClasses/Tutorial/Sigs.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Some polymorphic constants for the 'signature' parts of axclasses.
+*)
+
+Sigs = HOL +
+
+consts
+  "<*>"         :: "['a, 'a] => 'a"             (infixl 70)
+  "inv"         :: "'a => 'a"
+  "1"           :: "'a"                         ("1")
+
+end
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Xor.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Xor.ML	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,14 @@
+(*  Title:      HOL/AxClasses/Tutorial/Xor.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Proof the instantiation theorem bool :: agroup by hand.
+*)
+
+open AxClass;
+
+goal_arity Xor.thy ("bool", [], "agroup");
+by (axclass_tac Xor.thy []);
+by (rewrite_goals_tac [Xor.prod_bool_def, Xor.inv_bool_def, Xor.unit_bool_def]);
+by (ALLGOALS (fast_tac HOL_cs));
+qed "bool_in_agroup";
diff -r 706cfddca75c -r 18b1441fb603 src/HOL/AxClasses/Tutorial/Xor.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/Xor.thy	Fri Sep 01 14:27:36 1995 +0200
@@ -0,0 +1,15 @@
+(*  Title:      HOL/AxClasses/Tutorial/Xor.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Define overloaded constants "<*>", "inv", "1" on type "bool".
+*)
+
+Xor = Group +
+
+defs
+  prod_bool_def "x <*> y == x ~= (y::bool)"
+  inv_bool_def  "inv x   == x::bool"
+  unit_bool_def "1       == False"
+
+end