# HG changeset patch # User haftmann # Date 1185283250 -7200 # Node ID e65254ce5019d7973505ab1dfe997c6625786d38 # Parent b188cac107ad2520f6426160388311270e4a5b10 tuned diff -r b188cac107ad -r e65254ce5019 src/HOL/ex/Classpackage.thy --- a/src/HOL/ex/Classpackage.thy Tue Jul 24 15:20:49 2007 +0200 +++ b/src/HOL/ex/Classpackage.thy Tue Jul 24 15:20:50 2007 +0200 @@ -26,6 +26,11 @@ from mult_int_def show "k \ l \ j = k \ (l \ j)" by simp qed +instance * :: (semigroup, semigroup) semigroup + mult_prod_def: "x \ y \ let (x1, x2) = x; (y1, y2) = y in + (x1 \ y1, x2 \ y2)" +by default (simp_all add: split_paired_all mult_prod_def assoc) + instance list :: (type) semigroup "xs \ ys \ xs @ ys" proof @@ -52,6 +57,10 @@ from mult_int_def one_int_def show "\ \ k = k" by simp qed +instance * :: (monoidl, monoidl) monoidl + one_prod_def: "\ \ (\, \)" +by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl) + instance list :: (type) monoidl "\ \ []" proof @@ -66,47 +75,13 @@ class monoid = monoidl + assumes neutr: "x \<^loc>\ \<^loc>\ = x" - -instance list :: (type) monoid -proof - fix xs :: "'a list" - show "xs \ \ = xs" - proof - - from mult_list_def have "\xs ys\'a list. xs \ ys \ xs @ ys" . - moreover from one_list_def have "\ \ []\'a list" by simp - ultimately show ?thesis by simp - qed -qed - -class monoid_comm = monoid + - assumes comm: "x \<^loc>\ y = y \<^loc>\ x" - -instance nat :: monoid_comm and int :: monoid_comm -proof - fix n :: nat - from mult_nat_def one_nat_def show "n \ \ = n" by simp -next - fix n m :: nat - from mult_nat_def show "n \ m = m \ n" by simp -next - fix k :: int - from mult_int_def one_int_def show "k \ \ = k" by simp -next - fix k l :: int - from mult_int_def show "k \ l = l \ k" by simp -qed - -context monoid begin definition units :: "'a set" where "units = {y. \x. x \<^loc>\ y = \<^loc>\ \ y \<^loc>\ x = \<^loc>\}" -end - -context monoid -begin +end context monoid begin lemma inv_obtain: assumes "x \ units" @@ -139,66 +114,75 @@ with neutl z_choice show ?thesis by simp qed -end - -consts - reduce :: "('a \ 'a \ 'a) \ 'a \ nat \ 'a \ 'a" - -primrec - "reduce f g 0 x = g" - "reduce f g (Suc n) x = f x (reduce f g n x)" +fun + npow :: "nat \ 'a \ 'a" +where + "npow 0 x = \<^loc>\" + | "npow (Suc n) x = x \<^loc>\ npow n x" -context monoid -begin - -definition - npow :: "nat \ 'a \ 'a" where - npow_def_prim: "npow n x = reduce (op \<^loc>\) \<^loc>\ n x" - -end - -context monoid -begin +end context monoid begin abbreviation npow_syn :: "'a \ nat \ 'a" (infix "\<^loc>\" 75) where "x \<^loc>\ n \ npow n x" -lemma npow_def: - "x \<^loc>\ 0 = \<^loc>\" - "x \<^loc>\ Suc n = x \<^loc>\ x \<^loc>\ n" -using npow_def_prim by simp_all - lemma nat_pow_one: "\<^loc>\ \<^loc>\ n = \<^loc>\" -using npow_def neutl by (induct n) simp_all +using neutl by (induct n) simp_all lemma nat_pow_mult: "x \<^loc>\ n \<^loc>\ x \<^loc>\ m = x \<^loc>\ (n + m)" proof (induct n) - case 0 with neutl npow_def show ?case by simp + case 0 with neutl show ?case by simp next - case (Suc n) with Suc.hyps assoc npow_def show ?case by simp + case (Suc n) with Suc.hyps assoc show ?case by simp qed lemma nat_pow_pow: "(x \<^loc>\ m) \<^loc>\ n = x \<^loc>\ (n * m)" -using npow_def nat_pow_mult by (induct n) simp_all +using nat_pow_mult by (induct n) simp_all end +instance * :: (monoid, monoid) monoid +by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.mult_one.neutr) + +instance list :: (type) monoid +proof + fix xs :: "'a list" + show "xs \ \ = xs" + proof - + from mult_list_def have "\xs ys\'a list. xs \ ys \ xs @ ys" . + moreover from one_list_def have "\ \ []\'a list" by simp + ultimately show ?thesis by simp + qed +qed + +class monoid_comm = monoid + + assumes comm: "x \<^loc>\ y = y \<^loc>\ x" + +instance nat :: monoid_comm and int :: monoid_comm +proof + fix n :: nat + from mult_nat_def one_nat_def show "n \ \ = n" by simp +next + fix n m :: nat + from mult_nat_def show "n \ m = m \ n" by simp +next + fix k :: int + from mult_int_def one_int_def show "k \ \ = k" by simp +next + fix k l :: int + from mult_int_def show "k \ l = l \ k" by simp +qed + +instance * :: (monoid_comm, monoid_comm) monoid_comm +by default (simp_all add: split_paired_all mult_prod_def comm) + class group = monoidl + fixes inv :: "'a \ 'a" ("\<^loc>\
_" [81] 80) assumes invl: "\<^loc>\
x \<^loc>\ x = \<^loc>\" - -class group_comm = group + monoid_comm +begin -instance int :: group_comm - "\
k \ - (k\int)" -proof - fix k :: int - from mult_int_def one_int_def inv_int_def show "\
k \ k = \" by simp -qed - -lemma (in group) cancel: +lemma cancel: "(x \<^loc>\ y = x \<^loc>\ z) = (y = z)" proof fix x y z :: 'a @@ -212,7 +196,7 @@ thus "x \<^loc>\ y = x \<^loc>\ z" by simp qed -lemma (in group) neutr: +lemma neutr: "x \<^loc>\ \<^loc>\ = x" proof - from invl have "\<^loc>\
x \<^loc>\ x = \<^loc>\" by simp @@ -220,7 +204,7 @@ with cancel show ?thesis by simp qed -lemma (in group) invr: +lemma invr: "x \<^loc>\ \<^loc>\
x = \<^loc>\" proof - from neutl invl have "\<^loc>\
x \<^loc>\ x \<^loc>\ \<^loc>\
x = \<^loc>\
x" by simp @@ -229,14 +213,20 @@ with cancel show ?thesis .. qed +end + instance advanced group < monoid proof unfold_locales fix x from neutr show "x \<^loc>\ \<^loc>\ = x" . qed +hide const npow -lemma (in group) all_inv [intro]: - "(x\'a) \ monoid.units (op \<^loc>\) \<^loc>\" +context group +begin + +lemma all_inv [intro]: + "(x\'a) \ units" unfolding units_def proof - fix x :: "'a" @@ -246,7 +236,7 @@ thus "x \ {y\'a. \x\'a. x \<^loc>\ y = \<^loc>\ \ y \<^loc>\ x = \<^loc>\}" by simp qed -lemma (in group) cancer: +lemma cancer: "(y \<^loc>\ x = z \<^loc>\ x) = (y = z)" proof assume eq: "y \<^loc>\ x = z \<^loc>\ x" @@ -257,7 +247,7 @@ thus "y \<^loc>\ x = z \<^loc>\ x" by simp qed -lemma (in group) inv_one: +lemma inv_one: "\<^loc>\
\<^loc>\ = \<^loc>\" proof - from neutl have "\<^loc>\
\<^loc>\ = \<^loc>\ \<^loc>\ (\<^loc>\
\<^loc>\)" .. @@ -265,7 +255,7 @@ finally show ?thesis . qed -lemma (in group) inv_inv: +lemma inv_inv: "\<^loc>\
(\<^loc>\
x) = x" proof - from invl invr neutr @@ -275,7 +265,7 @@ with invl neutr show ?thesis by simp qed -lemma (in group) inv_mult_group: +lemma inv_mult_group: "\<^loc>\
(x \<^loc>\ y) = \<^loc>\
y \<^loc>\ \<^loc>\
x" proof - from invl have "\<^loc>\
(x \<^loc>\ y) \<^loc>\ (x \<^loc>\ y) = \<^loc>\" by simp @@ -285,52 +275,52 @@ with invr neutr show ?thesis by simp qed -lemma (in group) inv_comm: +lemma inv_comm: "x \<^loc>\ \<^loc>\
x = \<^loc>\
x \<^loc>\ x" using invr invl by simp -definition (in group) - pow :: "int \ 'a \ 'a" where - "pow k x = (if k < 0 then \<^loc>\
(monoid.npow (op \<^loc>\) \<^loc>\ (nat (-k)) x) - else (monoid.npow (op \<^loc>\) \<^loc>\ (nat k) x))" +definition + pow :: "int \ 'a \ 'a" +where + "pow k x = (if k < 0 then \<^loc>\
(npow (nat (-k)) x) + else (npow (nat k) x))" + +end context group begin -abbreviation (in group) - pow_syn :: "'a \ int \ 'a" (infix "\<^loc>\" 75) where - "x \<^loc>\ k \ pow k x" +abbreviation + pow_syn :: "'a \ int \ 'a" (infix "\<^loc>\\" 75) +where + "x \<^loc>\\ k \ pow k x" -lemma (in group) int_pow_zero: - "x \<^loc>\ (0\int) = \<^loc>\" -using npow_def pow_def by simp +lemma int_pow_zero: + "x \<^loc>\\ (0\int) = \<^loc>\" +using pow_def by simp -lemma (in group) int_pow_one: - "\<^loc>\ \<^loc>\ (k\int) = \<^loc>\" +lemma int_pow_one: + "\<^loc>\ \<^loc>\\ (k\int) = \<^loc>\" using pow_def nat_pow_one inv_one by simp -instance * :: (semigroup, semigroup) semigroup - mult_prod_def: "x \ y \ let (x1, x2) = x; (y1, y2) = y in - (x1 \ y1, x2 \ y2)" -by default (simp_all add: split_paired_all mult_prod_def assoc) - -instance * :: (monoidl, monoidl) monoidl - one_prod_def: "\ \ (\, \)" -by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl) - -instance * :: (monoid, monoid) monoid -by default (simp_all add: split_paired_all mult_prod_def one_prod_def monoid_class.mult_one.neutr) - -instance * :: (monoid_comm, monoid_comm) monoid_comm -by default (simp_all add: split_paired_all mult_prod_def comm) +end instance * :: (group, group) group inv_prod_def: "\
x \ let (x1, x2) = x in (\
x1, \
x2)" by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl) +class group_comm = group + monoid_comm + +instance int :: group_comm + "\
k \ - (k\int)" +proof + fix k :: int + from mult_int_def one_int_def inv_int_def show "\
k \ k = \" by simp +qed + instance * :: (group_comm, group_comm) group_comm by default (simp_all add: split_paired_all mult_prod_def comm) - definition - "X a b c = (a \ \ \ b, a \ \ \ b, [a, b] \ \ \ [a, b, c])" + "X a b c = (a \ \ \ b, a \ \ \ b, npow 3 [a, b] \ \ \ [a, b, c])" + definition "Y a b c = (a, \
a) \ \ \ \
(b, \
c)"