1 (* ID: $Id$ |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Test and examples for Isar class package *} |
|
6 |
|
7 theory Classpackage |
|
8 imports List |
|
9 begin |
|
10 |
|
11 class semigroup = type + |
|
12 fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<otimes>" 70) |
|
13 assumes assoc: "x \<otimes> y \<otimes> z = x \<otimes> (y \<otimes> z)" |
|
14 |
|
15 instance nat :: semigroup |
|
16 "m \<otimes> n \<equiv> (m\<Colon>nat) + n" |
|
17 proof |
|
18 fix m n q :: nat |
|
19 from mult_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp |
|
20 qed |
|
21 |
|
22 instance int :: semigroup |
|
23 "k \<otimes> l \<equiv> (k\<Colon>int) + l" |
|
24 proof |
|
25 fix k l j :: int |
|
26 from mult_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp |
|
27 qed |
|
28 |
|
29 instance * :: (semigroup, semigroup) semigroup |
|
30 mult_prod_def: "x \<otimes> y \<equiv> let (x1, x2) = x; (y1, y2) = y in |
|
31 (x1 \<otimes> y1, x2 \<otimes> y2)" |
|
32 by default (simp_all add: split_paired_all mult_prod_def assoc) |
|
33 |
|
34 instance list :: (type) semigroup |
|
35 "xs \<otimes> ys \<equiv> xs @ ys" |
|
36 proof |
|
37 fix xs ys zs :: "'a list" |
|
38 show "xs \<otimes> ys \<otimes> zs = xs \<otimes> (ys \<otimes> zs)" |
|
39 proof - |
|
40 from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . |
|
41 thus ?thesis by simp |
|
42 qed |
|
43 qed |
|
44 |
|
45 class monoidl = semigroup + |
|
46 fixes one :: 'a ("\<one>") |
|
47 assumes neutl: "\<one> \<otimes> x = x" |
|
48 |
|
49 instance nat :: monoidl and int :: monoidl |
|
50 "\<one> \<equiv> (0\<Colon>nat)" |
|
51 "\<one> \<equiv> (0\<Colon>int)" |
|
52 proof |
|
53 fix n :: nat |
|
54 from mult_nat_def one_nat_def show "\<one> \<otimes> n = n" by simp |
|
55 next |
|
56 fix k :: int |
|
57 from mult_int_def one_int_def show "\<one> \<otimes> k = k" by simp |
|
58 qed |
|
59 |
|
60 instance * :: (monoidl, monoidl) monoidl |
|
61 one_prod_def: "\<one> \<equiv> (\<one>, \<one>)" |
|
62 by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutl) |
|
63 |
|
64 instance list :: (type) monoidl |
|
65 "\<one> \<equiv> []" |
|
66 proof |
|
67 fix xs :: "'a list" |
|
68 show "\<one> \<otimes> xs = xs" |
|
69 proof - |
|
70 from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . |
|
71 moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp |
|
72 ultimately show ?thesis by simp |
|
73 qed |
|
74 qed |
|
75 |
|
76 class monoid = monoidl + |
|
77 assumes neutr: "x \<otimes> \<one> = x" |
|
78 begin |
|
79 |
|
80 definition |
|
81 units :: "'a set" where |
|
82 "units = {y. \<exists>x. x \<otimes> y = \<one> \<and> y \<otimes> x = \<one>}" |
|
83 |
|
84 lemma inv_obtain: |
|
85 assumes "x \<in> units" |
|
86 obtains y where "y \<otimes> x = \<one>" and "x \<otimes> y = \<one>" |
|
87 proof - |
|
88 from assms units_def obtain y |
|
89 where "y \<otimes> x = \<one>" and "x \<otimes> y = \<one>" by auto |
|
90 thus ?thesis .. |
|
91 qed |
|
92 |
|
93 lemma inv_unique: |
|
94 assumes "y \<otimes> x = \<one>" "x \<otimes> y' = \<one>" |
|
95 shows "y = y'" |
|
96 proof - |
|
97 from assms neutr have "y = y \<otimes> (x \<otimes> y')" by simp |
|
98 also with assoc have "... = (y \<otimes> x) \<otimes> y'" by simp |
|
99 also with assms neutl have "... = y'" by simp |
|
100 finally show ?thesis . |
|
101 qed |
|
102 |
|
103 lemma units_inv_comm: |
|
104 assumes inv: "x \<otimes> y = \<one>" |
|
105 and G: "x \<in> units" |
|
106 shows "y \<otimes> x = \<one>" |
|
107 proof - |
|
108 from G inv_obtain obtain z |
|
109 where z_choice: "z \<otimes> x = \<one>" by blast |
|
110 from inv neutl neutr have "x \<otimes> y \<otimes> x = x \<otimes> \<one>" by simp |
|
111 with assoc have "z \<otimes> x \<otimes> y \<otimes> x = z \<otimes> x \<otimes> \<one>" by simp |
|
112 with neutl z_choice show ?thesis by simp |
|
113 qed |
|
114 |
|
115 fun |
|
116 npow :: "nat \<Rightarrow> 'a \<Rightarrow> 'a" |
|
117 where |
|
118 "npow 0 x = \<one>" |
|
119 | "npow (Suc n) x = x \<otimes> npow n x" |
|
120 |
|
121 abbreviation |
|
122 npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<up>" 75) where |
|
123 "x \<up> n \<equiv> npow n x" |
|
124 |
|
125 lemma nat_pow_one: |
|
126 "\<one> \<up> n = \<one>" |
|
127 using neutl by (induct n) simp_all |
|
128 |
|
129 lemma nat_pow_mult: "x \<up> n \<otimes> x \<up> m = x \<up> (n + m)" |
|
130 proof (induct n) |
|
131 case 0 with neutl show ?case by simp |
|
132 next |
|
133 case (Suc n) with Suc.hyps assoc show ?case by simp |
|
134 qed |
|
135 |
|
136 lemma nat_pow_pow: "(x \<up> m) \<up> n = x \<up> (n * m)" |
|
137 using nat_pow_mult by (induct n) simp_all |
|
138 |
|
139 end |
|
140 |
|
141 instance * :: (monoid, monoid) monoid |
|
142 by default (simp_all add: split_paired_all mult_prod_def one_prod_def neutr) |
|
143 |
|
144 instance list :: (type) monoid |
|
145 proof |
|
146 fix xs :: "'a list" |
|
147 show "xs \<otimes> \<one> = xs" |
|
148 proof - |
|
149 from mult_list_def have "\<And>xs ys\<Colon>'a list. xs \<otimes> ys \<equiv> xs @ ys" . |
|
150 moreover from one_list_def have "\<one> \<equiv> []\<Colon>'a list" by simp |
|
151 ultimately show ?thesis by simp |
|
152 qed |
|
153 qed |
|
154 |
|
155 class monoid_comm = monoid + |
|
156 assumes comm: "x \<otimes> y = y \<otimes> x" |
|
157 |
|
158 instance nat :: monoid_comm and int :: monoid_comm |
|
159 proof |
|
160 fix n :: nat |
|
161 from mult_nat_def one_nat_def show "n \<otimes> \<one> = n" by simp |
|
162 next |
|
163 fix n m :: nat |
|
164 from mult_nat_def show "n \<otimes> m = m \<otimes> n" by simp |
|
165 next |
|
166 fix k :: int |
|
167 from mult_int_def one_int_def show "k \<otimes> \<one> = k" by simp |
|
168 next |
|
169 fix k l :: int |
|
170 from mult_int_def show "k \<otimes> l = l \<otimes> k" by simp |
|
171 qed |
|
172 |
|
173 instance * :: (monoid_comm, monoid_comm) monoid_comm |
|
174 by default (simp_all add: split_paired_all mult_prod_def comm) |
|
175 |
|
176 class group = monoidl + |
|
177 fixes inv :: "'a \<Rightarrow> 'a" ("\<div> _" [81] 80) |
|
178 assumes invl: "\<div> x \<otimes> x = \<one>" |
|
179 begin |
|
180 |
|
181 lemma cancel: |
|
182 "(x \<otimes> y = x \<otimes> z) = (y = z)" |
|
183 proof |
|
184 fix x y z :: 'a |
|
185 assume eq: "x \<otimes> y = x \<otimes> z" |
|
186 hence "\<div> x \<otimes> (x \<otimes> y) = \<div> x \<otimes> (x \<otimes> z)" by simp |
|
187 with assoc have "\<div> x \<otimes> x \<otimes> y = \<div> x \<otimes> x \<otimes> z" by simp |
|
188 with neutl invl show "y = z" by simp |
|
189 next |
|
190 fix x y z :: 'a |
|
191 assume eq: "y = z" |
|
192 thus "x \<otimes> y = x \<otimes> z" by simp |
|
193 qed |
|
194 |
|
195 subclass monoid |
|
196 proof unfold_locales |
|
197 fix x |
|
198 from invl have "\<div> x \<otimes> x = \<one>" by simp |
|
199 with assoc [symmetric] neutl invl have "\<div> x \<otimes> (x \<otimes> \<one>) = \<div> x \<otimes> x" by simp |
|
200 with cancel show "x \<otimes> \<one> = x" by simp |
|
201 qed |
|
202 |
|
203 end context group begin |
|
204 |
|
205 find_theorems name: neut |
|
206 |
|
207 lemma invr: |
|
208 "x \<otimes> \<div> x = \<one>" |
|
209 proof - |
|
210 from neutl invl have "\<div> x \<otimes> x \<otimes> \<div> x = \<div> x" by simp |
|
211 with neutr have "\<div> x \<otimes> x \<otimes> \<div> x = \<div> x \<otimes> \<one> " by simp |
|
212 with assoc have "\<div> x \<otimes> (x \<otimes> \<div> x) = \<div> x \<otimes> \<one> " by simp |
|
213 with cancel show ?thesis .. |
|
214 qed |
|
215 |
|
216 lemma all_inv [intro]: |
|
217 "(x\<Colon>'a) \<in> units" |
|
218 unfolding units_def |
|
219 proof - |
|
220 fix x :: "'a" |
|
221 from invl invr have "\<div> x \<otimes> x = \<one>" and "x \<otimes> \<div> x = \<one>" . |
|
222 then obtain y where "y \<otimes> x = \<one>" and "x \<otimes> y = \<one>" .. |
|
223 hence "\<exists>y\<Colon>'a. y \<otimes> x = \<one> \<and> x \<otimes> y = \<one>" by blast |
|
224 thus "x \<in> {y\<Colon>'a. \<exists>x\<Colon>'a. x \<otimes> y = \<one> \<and> y \<otimes> x = \<one>}" by simp |
|
225 qed |
|
226 |
|
227 lemma cancer: |
|
228 "(y \<otimes> x = z \<otimes> x) = (y = z)" |
|
229 proof |
|
230 assume eq: "y \<otimes> x = z \<otimes> x" |
|
231 with assoc [symmetric] have "y \<otimes> (x \<otimes> \<div> x) = z \<otimes> (x \<otimes> \<div> x)" by (simp del: invr) |
|
232 with invr neutr show "y = z" by simp |
|
233 next |
|
234 assume eq: "y = z" |
|
235 thus "y \<otimes> x = z \<otimes> x" by simp |
|
236 qed |
|
237 |
|
238 lemma inv_one: |
|
239 "\<div> \<one> = \<one>" |
|
240 proof - |
|
241 from neutl have "\<div> \<one> = \<one> \<otimes> (\<div> \<one>)" .. |
|
242 moreover from invr have "... = \<one>" by simp |
|
243 finally show ?thesis . |
|
244 qed |
|
245 |
|
246 lemma inv_inv: |
|
247 "\<div> (\<div> x) = x" |
|
248 proof - |
|
249 from invl invr neutr |
|
250 have "\<div> (\<div> x) \<otimes> \<div> x \<otimes> x = x \<otimes> \<div> x \<otimes> x" by simp |
|
251 with assoc [symmetric] |
|
252 have "\<div> (\<div> x) \<otimes> (\<div> x \<otimes> x) = x \<otimes> (\<div> x \<otimes> x)" by simp |
|
253 with invl neutr show ?thesis by simp |
|
254 qed |
|
255 |
|
256 lemma inv_mult_group: |
|
257 "\<div> (x \<otimes> y) = \<div> y \<otimes> \<div> x" |
|
258 proof - |
|
259 from invl have "\<div> (x \<otimes> y) \<otimes> (x \<otimes> y) = \<one>" by simp |
|
260 with assoc have "\<div> (x \<otimes> y) \<otimes> x \<otimes> y = \<one>" by simp |
|
261 with neutl have "\<div> (x \<otimes> y) \<otimes> x \<otimes> y \<otimes> \<div> y \<otimes> \<div> x = \<div> y \<otimes> \<div> x" by simp |
|
262 with assoc have "\<div> (x \<otimes> y) \<otimes> (x \<otimes> (y \<otimes> \<div> y) \<otimes> \<div> x) = \<div> y \<otimes> \<div> x" by simp |
|
263 with invr neutr show ?thesis by simp |
|
264 qed |
|
265 |
|
266 lemma inv_comm: |
|
267 "x \<otimes> \<div> x = \<div> x \<otimes> x" |
|
268 using invr invl by simp |
|
269 |
|
270 definition |
|
271 pow :: "int \<Rightarrow> 'a \<Rightarrow> 'a" |
|
272 where |
|
273 "pow k x = (if k < 0 then \<div> (npow (nat (-k)) x) |
|
274 else (npow (nat k) x))" |
|
275 |
|
276 abbreviation |
|
277 pow_syn :: "'a \<Rightarrow> int \<Rightarrow> 'a" (infix "\<up>\<up>" 75) |
|
278 where |
|
279 "x \<up>\<up> k \<equiv> pow k x" |
|
280 |
|
281 lemma int_pow_zero: |
|
282 "x \<up>\<up> (0\<Colon>int) = \<one>" |
|
283 using pow_def by simp |
|
284 |
|
285 lemma int_pow_one: |
|
286 "\<one> \<up>\<up> (k\<Colon>int) = \<one>" |
|
287 using pow_def nat_pow_one inv_one by simp |
|
288 |
|
289 end |
|
290 |
|
291 instance * :: (group, group) group |
|
292 inv_prod_def: "\<div> x \<equiv> let (x1, x2) = x in (\<div> x1, \<div> x2)" |
|
293 by default (simp_all add: split_paired_all mult_prod_def one_prod_def inv_prod_def invl) |
|
294 |
|
295 class group_comm = group + monoid_comm |
|
296 |
|
297 instance int :: group_comm |
|
298 "\<div> k \<equiv> - (k\<Colon>int)" |
|
299 proof |
|
300 fix k :: int |
|
301 from mult_int_def one_int_def inv_int_def show "\<div> k \<otimes> k = \<one>" by simp |
|
302 qed |
|
303 |
|
304 instance * :: (group_comm, group_comm) group_comm |
|
305 by default (simp_all add: split_paired_all mult_prod_def comm) |
|
306 |
|
307 definition |
|
308 "X a b c = (a \<otimes> \<one> \<otimes> b, a \<otimes> \<one> \<otimes> b, npow 3 [a, b] \<otimes> \<one> \<otimes> [a, b, c])" |
|
309 |
|
310 definition |
|
311 "Y a b c = (a, \<div> a) \<otimes> \<one> \<otimes> \<div> (b, \<div> pow (-3) c)" |
|
312 |
|
313 definition "x1 = X (1::nat) 2 3" |
|
314 definition "x2 = X (1::int) 2 3" |
|
315 definition "y2 = Y (1::int) 2 3" |
|
316 |
|
317 export_code x1 x2 y2 pow in SML module_name Classpackage |
|
318 in OCaml file - |
|
319 in Haskell file - |
|
320 |
|
321 end |
|