--- /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";
--- /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
--- /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";
--- /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
--- /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
--- /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
--- /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
--- /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";
--- /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
--- /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.
--- /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
--- /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";
+
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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
--- /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";
--- /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
--- /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
--- /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
--- /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";
--- /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