# HG changeset patch
# User wenzelm
# Date 970590656 -7200
# Node ID 537206cc738f55d833fc946f5896f653f8feb2c1
# Parent e187dacd248f04ff02e481d13ebf48f925b2a5a1
moved axclass tutorial examples to top dir;
diff -r e187dacd248f -r 537206cc738f src/HOL/AxClasses/Group.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Group.thy Tue Oct 03 18:30:56 2000 +0200
@@ -0,0 +1,124 @@
+(* Title: HOL/AxClasses/Group.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+theory Group = Main:
+
+subsection {* Monoids and Groups *}
+
+consts
+ times :: "'a => 'a => 'a" (infixl "[*]" 70)
+ inverse :: "'a => 'a"
+ one :: 'a
+
+
+axclass monoid < "term"
+ assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
+ left_unit: "one [*] x = x"
+ right_unit: "x [*] one = x"
+
+axclass semigroup < "term"
+ assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
+
+axclass group < semigroup
+ left_unit: "one [*] x = x"
+ left_inverse: "inverse x [*] x = one"
+
+axclass agroup < group
+ 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 *}
+
+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 *}
+
+defs (overloaded)
+ 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 (overloaded)
+ 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 e187dacd248f -r 537206cc738f src/HOL/AxClasses/Product.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Product.thy Tue Oct 03 18:30:56 2000 +0200
@@ -0,0 +1,20 @@
+(* Title: HOL/AxClasses/Product.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+theory Product = Main:
+
+axclass product < "term"
+
+consts
+ product :: "'a::product => 'a => 'a" (infixl "[*]" 70)
+
+
+instance bool :: product
+ by intro_classes
+
+defs (overloaded)
+ product_bool_def: "x [*] y == x & y"
+
+end
diff -r e187dacd248f -r 537206cc738f src/HOL/AxClasses/README.html
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/README.html Tue Oct 03 18:30:56 2000 +0200
@@ -0,0 +1,17 @@
+
+
+
+
+HOL/AxClasses
+
+
+
+HOL/AxClasses
+
+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 e187dacd248f -r 537206cc738f src/HOL/AxClasses/ROOT.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/ROOT.ML Tue Oct 03 18:30:56 2000 +0200
@@ -0,0 +1,4 @@
+
+time_use_thy "Semigroups";
+time_use_thy "Group";
+time_use_thy "Product";
diff -r e187dacd248f -r 537206cc738f src/HOL/AxClasses/Semigroups.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/AxClasses/Semigroups.thy Tue Oct 03 18:30:56 2000 +0200
@@ -0,0 +1,21 @@
+(* Title: HOL/AxClasses/Semigroups.thy
+ ID: $Id$
+ Author: Markus Wenzel, TU Muenchen
+*)
+
+theory Semigroups = Main:
+
+consts
+ times :: "'a => 'a => 'a" (infixl "[*]" 70)
+
+axclass semigroup < "term"
+ assoc: "(x [*] y) [*] z = x [*] (y [*] z)"
+
+
+consts
+ plus :: "'a => 'a => 'a" (infixl "[+]" 70)
+
+axclass plus_semigroup < "term"
+ assoc: "(x [+] y) [+] z = x [+] (y [+] z)"
+
+end