--- a/src/HOL/ex/Classpackage.thy Wed Aug 15 08:57:40 2007 +0200
+++ b/src/HOL/ex/Classpackage.thy Wed Aug 15 08:57:41 2007 +0200
@@ -143,7 +143,7 @@
end
instance * :: (monoid, monoid) monoid
-by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.mult_one.neutr)
+by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutr)
instance list :: (type) monoid
proof
@@ -220,7 +220,16 @@
fix x
from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
qed
-hide const npow
+
+hide const npow (*FIXME*)
+lemmas neutr = monoid_class.mult_one.neutr
+lemmas inv_obtain = monoid_class.inv_obtain
+lemmas inv_unique = monoid_class.inv_unique
+lemmas nat_pow_mult = monoid_class.nat_pow_mult
+lemmas nat_pow_one = monoid_class.nat_pow_one
+lemmas nat_pow_pow = monoid_class.nat_pow_pow
+lemmas units_def = monoid_class.units_def
+lemmas mult_one_def = monoid_class.units_inv_comm
context group
begin
@@ -285,7 +294,12 @@
"pow k x = (if k < 0 then \<^loc>\<div> (npow (nat (-k)) x)
else (npow (nat k) x))"
-end context group begin
+end
+
+(*FIXME*)
+lemmas pow_def [code func] = pow_def [folded monoid_class.npow]
+
+context group begin
abbreviation
pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>\<up>" 75)
@@ -322,7 +336,7 @@
"X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, npow 3 [a, b] \<otimes> \<one> \<otimes> [a, b, c])"
definition
- "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> c)"
+ "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> pow (-3) c)"
definition "x1 = X (1::nat) 2 3"
definition "x2 = X (1::int) 2 3"