# HG changeset patch
# User wenzelm
# Date 958994961 -7200
# Node ID af5e09b6c20834dd91e00dfc778d6cf72a5b696d
# Parent d00b01ed85396c1c255a2d91c4fc6f2aad858b4e
new Isar version;
diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy
--- a/src/HOL/AxClasses/Tutorial/BoolGroupInsts.thy Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: HOL/AxClasses/Tutorial/BoolGroupInsts.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Define overloaded constants "<*>", "inverse", "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)"
- inverse_bool_def "inverse 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 d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Group.ML
--- a/src/HOL/AxClasses/Tutorial/Group.ML Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-(* Title: HOL/AxClasses/Tutorial/Group.ML
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Some basic theorems of group theory.
-*)
-
-fun sub r = standard (r RS subst);
-fun ssub r = standard (r RS ssubst);
-
-
-Goal "x <*> inverse x = (1::'a::group)";
-by (rtac (sub left_unit) 1);
-back();
-by (rtac (sub assoc) 1);
-by (rtac (sub left_inverse) 1);
-back();
-back();
-by (rtac (ssub assoc) 1);
-back();
-by (rtac (ssub left_inverse) 1);
-by (rtac (ssub assoc) 1);
-by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inverse) 1);
-by (rtac refl 1);
-qed "right_inverse";
-
-
-Goal "x <*> 1 = (x::'a::group)";
-by (rtac (sub left_inverse) 1);
-by (rtac (sub assoc) 1);
-by (rtac (ssub right_inverse) 1);
-by (rtac (ssub left_unit) 1);
-by (rtac refl 1);
-qed "right_unit";
-
-
-Goal "e <*> x = x --> e = (1::'a::group)";
-by (rtac impI 1);
-by (rtac (sub right_unit) 1);
-back();
-by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
-by (rtac (sub assoc) 1);
-by (rtac arg_cong 1);
-back();
-by (assume_tac 1);
-qed "strong_one_unit";
-
-
-Goal "EX! e. ALL x. e <*> x = (x::'a::group)";
-by (rtac ex1I 1);
-by (rtac allI 1);
-by (rtac left_unit 1);
-by (rtac mp 1);
-by (rtac strong_one_unit 1);
-by (etac allE 1);
-by (assume_tac 1);
-qed "ex1_unit";
-
-
-Goal "ALL x. EX! e. e <*> x = (x::'a::group)";
-by (rtac allI 1);
-by (rtac ex1I 1);
-by (rtac left_unit 1);
-by (rtac (strong_one_unit RS mp) 1);
-by (assume_tac 1);
-qed "ex1_unit'";
-
-
-Goal "y <*> x = 1 --> y = inverse (x::'a::group)";
-by (rtac impI 1);
-by (rtac (sub right_unit) 1);
-back();
-back();
-by (rtac (sub right_unit) 1);
-by (res_inst_tac [("x", "x")] (sub right_inverse) 1);
-by (rtac (sub assoc) 1);
-by (rtac (sub assoc) 1);
-by (rtac arg_cong 1);
-back();
-by (rtac (ssub left_inverse) 1);
-by (assume_tac 1);
-qed "one_inverse";
-
-
-Goal "ALL x. EX! y. y <*> x = (1::'a::group)";
-by (rtac allI 1);
-by (rtac ex1I 1);
-by (rtac left_inverse 1);
-by (rtac mp 1);
-by (rtac one_inverse 1);
-by (assume_tac 1);
-qed "ex1_inverse";
-
-
-Goal "inverse (x <*> y) = inverse y <*> inverse (x::'a::group)";
-by (rtac sym 1);
-by (rtac mp 1);
-by (rtac one_inverse 1);
-by (rtac (ssub assoc) 1);
-by (rtac (sub assoc) 1);
-back();
-by (rtac (ssub left_inverse) 1);
-by (rtac (ssub left_unit) 1);
-by (rtac (ssub left_inverse) 1);
-by (rtac refl 1);
-qed "inverse_product";
-
-
-Goal "inverse (inverse x) = (x::'a::group)";
-by (rtac sym 1);
-by (rtac (one_inverse RS mp) 1);
-by (rtac (ssub right_inverse) 1);
-by (rtac refl 1);
-qed "inverse_inv";
-
diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Group.thy
--- a/src/HOL/AxClasses/Tutorial/Group.thy Mon May 22 13:20:47 2000 +0200
+++ b/src/HOL/AxClasses/Tutorial/Group.thy Mon May 22 13:29:21 2000 +0200
@@ -1,31 +1,129 @@
(* Title: HOL/AxClasses/Tutorial/Group.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-
-Define classes "semigroup", "group", "agroup".
*)
-Group = Sigs +
+theory Group = Main:;
+
+subsection {* Monoids and Groups *};
-(* semigroups *)
+consts
+ times :: "'a => 'a => 'a" (infixl "[*]" 70)
+ inverse :: "'a => 'a"
+ one :: 'a;
+
axclass
- semigroup < term
- assoc "(x <*> y) <*> z = x <*> (y <*> z)"
+ monoid < "term"
+ assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
+ left_unit: "one [*] x = x"
+ right_unit: "x [*] one = x";
-(* groups *)
+axclass
+ semigroup < "term"
+ assoc: "(x [*] y) [*] z = x [*] (y [*] z)";
axclass
group < semigroup
- left_unit "1 <*> x = x"
- left_inverse "inverse x <*> x = 1"
-
-
-(* abelian groups *)
+ left_unit: "one [*] x = x"
+ left_inverse: "inverse x [*] x = one";
axclass
agroup < group
- commut "x <*> y = y <*> x"
+ commute: "x [*] y = y [*] x";
+
+
+subsection {* Abstract reasoning *};
+
+theorem group_right_inverse: "x [*] inverse x = (one::'a::group)";
+proof -;
+ have "x [*] inverse x = one [*] (x [*] inverse x)";
+ by (simp only: group.left_unit);
+ also; have "... = one [*] x [*] inverse x";
+ by (simp only: semigroup.assoc);
+ also; have "... = inverse (inverse x) [*] inverse x [*] x [*] inverse x";
+ by (simp only: group.left_inverse);
+ also; have "... = inverse (inverse x) [*] (inverse x [*] x) [*] inverse x";
+ by (simp only: semigroup.assoc);
+ also; have "... = inverse (inverse x) [*] one [*] inverse x";
+ by (simp only: group.left_inverse);
+ also; have "... = inverse (inverse x) [*] (one [*] inverse x)";
+ by (simp only: semigroup.assoc);
+ also; have "... = inverse (inverse x) [*] inverse x";
+ by (simp only: group.left_unit);
+ also; have "... = one";
+ by (simp only: group.left_inverse);
+ finally; show ?thesis; .;
+qed;
+
+theorem group_right_unit: "x [*] one = (x::'a::group)";
+proof -;
+ have "x [*] one = x [*] (inverse x [*] x)";
+ by (simp only: group.left_inverse);
+ also; have "... = x [*] inverse x [*] x";
+ by (simp only: semigroup.assoc);
+ also; have "... = one [*] x";
+ by (simp only: group_right_inverse);
+ also; have "... = x";
+ by (simp only: group.left_unit);
+ finally; show ?thesis; .;
+qed;
+
+
+subsection {* Abstract instantiation *};
-end
+instance monoid < semigroup;
+proof intro_classes;
+ fix x y z :: "'a::monoid";
+ show "x [*] y [*] z = x [*] (y [*] z)";
+ by (rule monoid.assoc);
+qed;
+
+instance group < monoid;
+proof intro_classes;
+ fix x y z :: "'a::group";
+ show "x [*] y [*] z = x [*] (y [*] z)";
+ by (rule semigroup.assoc);
+ show "one [*] x = x";
+ by (rule group.left_unit);
+ show "x [*] one = x";
+ by (rule group_right_unit);
+qed;
+
+
+subsection {* Concrete instantiation \label{sec:inst-arity} *};
+
+defs
+ times_bool_def: "x [*] y == x ~= (y::bool)"
+ inverse_bool_def: "inverse x == x::bool"
+ unit_bool_def: "one == False";
+
+instance bool :: agroup;
+proof (intro_classes,
+ unfold times_bool_def inverse_bool_def unit_bool_def);
+ fix x y z;
+ show "((x ~= y) ~= z) = (x ~= (y ~= z))"; by blast;
+ show "(False ~= x) = x"; by blast;
+ show "(x ~= x) = False"; by blast;
+ show "(x ~= y) = (y ~= x)"; by blast;
+qed;
+
+
+subsection {* Lifting and Functors *};
+
+defs
+ times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)";
+
+instance * :: (semigroup, semigroup) semigroup;
+proof (intro_classes, unfold times_prod_def);
+ fix p q r :: "'a::semigroup * 'b::semigroup";
+ show
+ "(fst (fst p [*] fst q, snd p [*] snd q) [*] fst r,
+ snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) =
+ (fst p [*] fst (fst q [*] fst r, snd q [*] snd r),
+ snd p [*] snd (fst q [*] fst r, snd q [*] snd r))";
+ by (simp add: semigroup.assoc);
+qed;
+
+end;
diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Monoid.thy
--- a/src/HOL/AxClasses/Tutorial/Monoid.thy Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(* 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 d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/MonoidGroupInsts.thy
--- a/src/HOL/AxClasses/Tutorial/MonoidGroupInsts.thy Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* 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 d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/ProdGroupInsts.thy
--- a/src/HOL/AxClasses/Tutorial/ProdGroupInsts.thy Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* 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
- {| SIMPSET' (fn ss => simp_tac (ss addsimps [assoc])) 1 |}
-
-end
diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Product.thy
--- a/src/HOL/AxClasses/Tutorial/Product.thy Mon May 22 13:20:47 2000 +0200
+++ b/src/HOL/AxClasses/Tutorial/Product.thy Mon May 22 13:29:21 2000 +0200
@@ -1,17 +1,18 @@
(* 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 +
+theory Product = Main:;
axclass
- product < term
-
+ product < "term";
consts
- "<*>" :: "['a::product, 'a] => 'a" (infixl 70)
+ product :: "'a::product => 'a => 'a" (infixl "[*]" 70);
-end
+instance bool :: product;
+ by intro_classes;
+defs
+ product_bool_def: "x [*] y == x & y";
+
+end;
diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/ProductInsts.thy
--- a/src/HOL/AxClasses/Tutorial/ProductInsts.thy Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* 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 d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Tutorial/README.html Mon May 22 13:29:21 2000 +0200
@@ -0,0 +1,17 @@
+
+
+
+
+HOL/AxClasses/Tutorial
+
+
+
+HOL/AxClasses/Tutorial
+
+These are the HOL examples of the tutorial Using Axiomatic Type
+Classes in Isabelle. See also FOL/ex/NatClass for the natural
+number example.
+
+
+
diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/ROOT.ML
--- a/src/HOL/AxClasses/Tutorial/ROOT.ML Mon May 22 13:20:47 2000 +0200
+++ b/src/HOL/AxClasses/Tutorial/ROOT.ML Mon May 22 13:29:21 2000 +0200
@@ -1,34 +1,4 @@
-(* 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/.)
-*)
-
-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 d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Semigroup.thy
--- a/src/HOL/AxClasses/Tutorial/Semigroup.thy Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* 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 d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Semigroups.thy
--- a/src/HOL/AxClasses/Tutorial/Semigroups.thy Mon May 22 13:20:47 2000 +0200
+++ b/src/HOL/AxClasses/Tutorial/Semigroups.thy Mon May 22 13:29:21 2000 +0200
@@ -1,32 +1,20 @@
(* Title: HOL/AxClasses/Tutorial/Semigroups.thy
ID: $Id$
Author: Markus Wenzel, TU Muenchen
-
-Semigroups with different 'signatures'.
*)
-Semigroups = HOL +
+theory Semigroups = Main:;
consts
- "<+>" :: "['a, 'a] => 'a" (infixl 65)
- "<*>" :: "['a, 'a] => 'a" (infixl 70)
-
-constdefs
- assoc :: "(['a, 'a] => 'a) => bool"
- "assoc f == ALL x y z. f (f x y) z = f x (f y z)"
-
-
-(* semigroups with op <+> *)
-
+ times :: "'a => 'a => 'a" (infixl "[*]" 70);
axclass
- plus_sg < term
- plus_assoc "assoc (op <+>)"
-
-
-(* semigroups with op <*> *)
+ semigroup < "term"
+ assoc: "(x [*] y) [*] z = x [*] (y [*] z)";
+consts
+ plus :: "'a => 'a => 'a" (infixl "[+]" 70);
axclass
- times_sg < term
- times_assoc "assoc (op <*>)"
+ plus_semigroup < "term"
+ assoc: "(x [+] y) [+] z = x [+] (y [+] z)";
-end
+end;
diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Sigs.thy
--- a/src/HOL/AxClasses/Tutorial/Sigs.thy Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* 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)
- inverse :: "'a => 'a"
- "1" :: "'a" ("1")
-
-end
diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Xor.ML
--- a/src/HOL/AxClasses/Tutorial/Xor.ML Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* 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 []);
-by (rewrite_goals_tac
- [Xor.prod_bool_def,Xor.inverse_bool_def, Xor.unit_bool_def]);
-by (ALLGOALS (Fast_tac));
-qed "bool_in_agroup";
diff -r d00b01ed8539 -r af5e09b6c208 src/HOL/AxClasses/Tutorial/Xor.thy
--- a/src/HOL/AxClasses/Tutorial/Xor.thy Mon May 22 13:20:47 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: HOL/AxClasses/Tutorial/Xor.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Define overloaded constants "<*>", "inverse", "1" on type "bool".
-*)
-
-Xor = Group +
-
-defs
- prod_bool_def "x <*> y == x ~= (y::bool)"
- inverse_bool_def "inverse x == x::bool"
- unit_bool_def "1 == False"
-
-end