src/HOL/ex/Classpackage.thy
 author haftmann Fri Jul 21 14:47:44 2006 +0200 (2006-07-21) changeset 20178 e56fa3c8b1f1 parent 20106 a3d4b4eb35b9 child 20187 af47971ea304 permissions -rw-r--r--
1 (*  ID:         \$Id\$
2     Author:     Florian Haftmann, TU Muenchen
3 *)
5 header {* Test and Examples for Pure/Tools/class_package.ML *}
7 theory Classpackage
8 imports Main
9 begin
11 class semigroup =
12   fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
13   assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
15 instance nat :: semigroup
16   "m \<otimes> n \<equiv> m + n"
17 proof
18   fix m n q :: nat
19   from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp
20 qed
22 instance int :: semigroup
23   "k \<otimes> l \<equiv> k + l"
24 proof
25   fix k l j :: int
26   from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp
27 qed
29 instance (type) list :: semigroup
30   "xs \<otimes> ys \<equiv> xs @ ys"
31 proof
32   fix xs ys zs :: "'a list"
33   show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)"
34   proof -
35     from semigroup_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
36     thus ?thesis by simp
37   qed
38 qed
40 class monoidl = semigroup +
41   fixes one :: 'a ("\<^loc>\<one>")
42   assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x"
44 instance monoidl_num_def: nat :: monoidl and int :: monoidl
45   "\<one> \<equiv> 0"
46   "\<one> \<equiv> 0"
47 proof
48   fix n :: nat
49   from monoidl_num_def show "\<one> \<otimes> n = n" by simp
50 next
51   fix k :: int
52   from monoidl_num_def show "\<one> \<otimes> k = k" by simp
53 qed
55 instance (type) list :: monoidl
56   "\<one> \<equiv> []"
57 proof
58   fix xs :: "'a list"
59   show "\<one> \<otimes> xs = xs"
60   proof -
61     from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
62     moreover from monoidl_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
63     ultimately show ?thesis by simp
64   qed
65 qed
67 class monoid = monoidl +
68   assumes neutr: "x \<^loc>\<otimes> \<^loc>\<one> = x"
70 instance monoid_list_def: (type) list :: monoid
71 proof
72   fix xs :: "'a list"
73   show "xs \<otimes> \<one> = xs"
74   proof -
75     from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" .
76     moreover from monoid_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp
77     ultimately show ?thesis by simp
78   qed
79 qed
81 class monoid_comm = monoid +
82   assumes comm: "x \<^loc>\<otimes> y = y \<^loc>\<otimes> x"
84 instance monoid_comm_num_def: nat :: monoid_comm and int :: monoid_comm
85 proof
86   fix n :: nat
87   from monoid_comm_num_def show "n \<otimes> \<one> = n" by simp
88 next
89   fix n m :: nat
90   from monoid_comm_num_def show "n \<otimes> m = m \<otimes> n" by simp
91 next
92   fix k :: int
93   from monoid_comm_num_def show "k \<otimes> \<one> = k" by simp
94 next
95   fix k l :: int
96   from monoid_comm_num_def show "k \<otimes> l = l \<otimes> k" by simp
97 qed
99 definition (in monoid)
100   units :: "'a set"
101   units_def: "units = { y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one> }"
103 lemma (in monoid) inv_obtain:
104   assumes ass: "x \<in> units"
105   obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
106 proof -
107   from ass units_def obtain y
108     where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" by auto
109   thus ?thesis ..
110 qed
112 lemma (in monoid) inv_unique:
113   assumes eq: "y \<^loc>\<otimes> x = \<^loc>\<one>" "x \<^loc>\<otimes> y' = \<^loc>\<one>"
114   shows "y = y'"
115 proof -
116   from eq neutr have "y = y \<^loc>\<otimes> (x \<^loc>\<otimes> y')" by simp
117   also with assoc have "... = (y \<^loc>\<otimes> x) \<^loc>\<otimes> y'" by simp
118   also with eq neutl have "... = y'" by simp
119   finally show ?thesis .
120 qed
122 lemma (in monoid) units_inv_comm:
123   assumes inv: "x \<^loc>\<otimes> y = \<^loc>\<one>"
124     and G: "x \<in> units"
125   shows "y \<^loc>\<otimes> x = \<^loc>\<one>"
126 proof -
127   from G inv_obtain obtain z
128     where z_choice: "z \<^loc>\<otimes> x = \<^loc>\<one>" by blast
129   from inv neutl neutr have "x \<^loc>\<otimes> y \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<one>" by simp
130   with assoc have "z \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> x = z \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<one>" by simp
131   with neutl z_choice show ?thesis by simp
132 qed
134 consts
135   reduce :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
137 primrec
138   "reduce f g 0 x = g"
139   "reduce f g (Suc n) x = f x (reduce f g n x)"
141 definition (in monoid)
142   npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
143   npow_def_prim: "npow n x = reduce (op \<^loc>\<otimes>) \<^loc>\<one> n x"
145 abbreviation (in monoid)
146   abbrev_npow :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
147   "x \<^loc>\<up> n \<equiv> npow n x"
149 lemma (in monoid) npow_def:
150   "x \<^loc>\<up> 0 = \<^loc>\<one>"
151   "x \<^loc>\<up> Suc n = x \<^loc>\<otimes> x \<^loc>\<up> n"
152 using npow_def_prim by simp_all
154 lemma (in monoid) nat_pow_one:
155   "\<^loc>\<one> \<^loc>\<up> n = \<^loc>\<one>"
156 using npow_def neutl by (induct n) simp_all
158 lemma (in monoid) nat_pow_mult:
159   "npow n x \<^loc>\<otimes> npow m x = npow (n + m) x"
160 proof (induct n)
161   case 0 with neutl npow_def show ?case by simp
162 next
163   case (Suc n) with Suc.hyps assoc npow_def show ?case by simp
164 qed
166 lemma (in monoid) nat_pow_pow:
167   "npow n (npow m x) = npow (n * m) x"
168 using npow_def nat_pow_mult by (induct n) simp_all
170 class group = monoidl +
171   fixes inv :: "'a \<Rightarrow> 'a" ("\<^loc>\<div> _" [81] 80)
172   assumes invl: "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>"
174 class group_comm = group + monoid_comm
176 instance group_comm_int_def: int :: group_comm
177   "\<div> k \<equiv> - (k\<Colon>int)"
178 proof
179   fix k :: int
180   from group_comm_int_def show "\<div> k \<otimes> k = \<one>" by simp
181 qed
183 lemma (in group) cancel:
184   "(x \<^loc>\<otimes> y = x \<^loc>\<otimes> z) = (y = z)"
185 proof
186   fix x y z :: 'a
187   assume eq: "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z"
188   hence "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> z)" by simp
189   with assoc have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> z" by simp
190   with neutl invl show "y = z" by simp
191 next
192   fix x y z :: 'a
193   assume eq: "y = z"
194   thus "x \<^loc>\<otimes> y = x \<^loc>\<otimes> z" by simp
195 qed
197 lemma (in group) neutr:
198   "x \<^loc>\<otimes> \<^loc>\<one> = x"
199 proof -
200   from invl have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" by simp
201   with assoc [symmetric] neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<one>) = \<^loc>\<div> x \<^loc>\<otimes> x" by simp
202   with cancel show ?thesis by simp
203 qed
205 lemma (in group) invr:
206   "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>"
207 proof -
208   from neutl invl have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x" by simp
209   with neutr have "\<^loc>\<div> x \<^loc>\<otimes> x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
210   with assoc have "\<^loc>\<div> x \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> x \<^loc>\<otimes> \<^loc>\<one> " by simp
211   with cancel show ?thesis ..
212 qed
214 interpretation group < monoid
215 proof -
216   fix x :: "'a"
217   from neutr show "x \<^loc>\<otimes> \<^loc>\<one> = x" .
218 qed
220 instance group < monoid
221 proof
222   fix x :: "'a\<Colon>group"
223   from group.neutr show "x \<otimes> \<one> = x" .
224 qed
226 lemma (in group) all_inv [intro]:
227   "(x\<Colon>'a) \<in> monoid.units (op \<^loc>\<otimes>) \<^loc>\<one>"
228   unfolding units_def
229 proof -
230   fix x :: "'a"
231   from invl invr have "\<^loc>\<div> x \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<one>" .
232   then obtain y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>" ..
233   hence "\<exists>y\<Colon>'a. y \<^loc>\<otimes> x = \<^loc>\<one> \<and> x \<^loc>\<otimes> y = \<^loc>\<one>" by blast
234   thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}" by simp
235 qed
237 lemma (in group) cancer:
238   "(y \<^loc>\<otimes> x = z \<^loc>\<otimes> x) = (y = z)"
239 proof
240   assume eq: "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x"
241   with assoc [symmetric] have "y \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x) = z \<^loc>\<otimes> (x \<^loc>\<otimes> \<^loc>\<div> x)" by (simp del: invr)
242   with invr neutr show "y = z" by simp
243 next
244   assume eq: "y = z"
245   thus "y \<^loc>\<otimes> x = z \<^loc>\<otimes> x" by simp
246 qed
248 lemma (in group) inv_one:
249   "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one>"
250 proof -
251   from neutl have "\<^loc>\<div> \<^loc>\<one> = \<^loc>\<one> \<^loc>\<otimes> (\<^loc>\<div> \<^loc>\<one>)" ..
252   moreover from invr have "... = \<^loc>\<one>" by simp
253   finally show ?thesis .
254 qed
256 lemma (in group) inv_inv:
257   "\<^loc>\<div> (\<^loc>\<div> x) = x"
258 proof -
259   from invl invr neutr
260     have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x = x \<^loc>\<otimes> \<^loc>\<div> x \<^loc>\<otimes> x" by simp
261   with assoc [symmetric]
262     have "\<^loc>\<div> (\<^loc>\<div> x) \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x) = x \<^loc>\<otimes> (\<^loc>\<div> x \<^loc>\<otimes> x)" by simp
263   with invl neutr show ?thesis by simp
264 qed
266 lemma (in group) inv_mult_group:
267   "\<^loc>\<div> (x \<^loc>\<otimes> y) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x"
268 proof -
269   from invl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> y) = \<^loc>\<one>" by simp
270   with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y = \<^loc>\<one>" by simp
271   with neutl have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> x \<^loc>\<otimes> y \<^loc>\<otimes> \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
272   with assoc have "\<^loc>\<div> (x \<^loc>\<otimes> y) \<^loc>\<otimes> (x \<^loc>\<otimes> (y \<^loc>\<otimes> \<^loc>\<div> y) \<^loc>\<otimes> \<^loc>\<div> x) = \<^loc>\<div> y \<^loc>\<otimes> \<^loc>\<div> x" by simp
273   with invr neutr show ?thesis by simp
274 qed
276 lemma (in group) inv_comm:
277   "x \<^loc>\<otimes> \<^loc>\<div> x = \<^loc>\<div> x \<^loc>\<otimes> x"
278 using invr invl by simp
280 definition (in group)
281   pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a"
282   pow_def: "pow k x = (if k < 0 then \<^loc>\<div> (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat (-k)) x)
283     else (monoid.npow (op \<^loc>\<otimes>) \<^loc>\<one> (nat k) x))"
285 abbreviation (in group)
286   abbrev_pow :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75)
287   "x \<^loc>\<up> k \<equiv> pow k x"
289 lemma (in group) int_pow_zero:
290   "x \<^loc>\<up> (0\<Colon>int) = \<^loc>\<one>"
291 using npow_def pow_def by simp
293 lemma (in group) int_pow_one:
294   "\<^loc>\<one> \<^loc>\<up> (k\<Colon>int) = \<^loc>\<one>"
295 using pow_def nat_pow_one inv_one by simp
297 instance group_prod_def: (group, group) * :: group
298   mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in
299               (x1 \<otimes> y1, x2 \<otimes> y2)"
300   mult_one_def: "\<one> \<equiv> (\<one>, \<one>)"
301   mult_inv_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)"
302 by default (simp_all add: split_paired_all group_prod_def assoc neutl invl)
304 instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm
305 by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm)
307 definition
308   "x = ((2\<Colon>nat) \<otimes> \<one> \<otimes> 3, (2\<Colon>int) \<otimes> \<one> \<otimes> \<div> 3, [1\<Colon>nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
309   "y = (2 \<Colon> int, \<div> 2 \<Colon> int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
311 code_generate "op \<otimes>" \<one> inv