equal
deleted
inserted
replaced
255 instantiation |
255 instantiation |
256 bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}" |
256 bit0 and bit1 :: (finite) "{zero,one,plus,times,uminus,minus,power}" |
257 begin |
257 begin |
258 |
258 |
259 definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where |
259 definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where |
260 "Abs_bit0' x = Abs_bit0 (x mod (2 * int CARD('a)))" |
260 "Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))" |
261 |
261 |
262 definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where |
262 definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where |
263 "Abs_bit1' x = Abs_bit1 (x mod (1 + 2 * int CARD('a)))" |
263 "Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))" |
264 |
264 |
265 definition "0 = Abs_bit0 0" |
265 definition "0 = Abs_bit0 0" |
266 definition "1 = Abs_bit0 1" |
266 definition "1 = Abs_bit0 1" |
267 definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)" |
267 definition "x + y = Abs_bit0' (Rep_bit0 x + Rep_bit0 y)" |
268 definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)" |
268 definition "x * y = Abs_bit0' (Rep_bit0 x * Rep_bit0 y)" |
281 instance .. |
281 instance .. |
282 |
282 |
283 end |
283 end |
284 |
284 |
285 interpretation bit0!: |
285 interpretation bit0!: |
286 mod_type "2 * int CARD('a::finite)" |
286 mod_type "int CARD('a::finite bit0)" |
287 "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
287 "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
288 "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
288 "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
289 apply (rule mod_type.intro) |
289 apply (rule mod_type.intro) |
290 apply (rule type_definition_bit0) |
290 apply (simp add: int_mult type_definition_bit0) |
|
291 apply simp |
291 using card_finite_pos [where ?'a='a] apply arith |
292 using card_finite_pos [where ?'a='a] apply arith |
292 apply (rule zero_bit0_def) |
293 apply (rule zero_bit0_def) |
293 apply (rule one_bit0_def) |
294 apply (rule one_bit0_def) |
294 apply (rule plus_bit0_def [unfolded Abs_bit0'_def]) |
295 apply (rule plus_bit0_def [unfolded Abs_bit0'_def]) |
295 apply (rule times_bit0_def [unfolded Abs_bit0'_def]) |
296 apply (rule times_bit0_def [unfolded Abs_bit0'_def]) |
297 apply (rule uminus_bit0_def [unfolded Abs_bit0'_def]) |
298 apply (rule uminus_bit0_def [unfolded Abs_bit0'_def]) |
298 apply (rule power_bit0_def [unfolded Abs_bit0'_def]) |
299 apply (rule power_bit0_def [unfolded Abs_bit0'_def]) |
299 done |
300 done |
300 |
301 |
301 interpretation bit1!: |
302 interpretation bit1!: |
302 mod_type "1 + 2 * int CARD('a::finite)" |
303 mod_type "int CARD('a::finite bit1)" |
303 "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
304 "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
304 "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
305 "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
305 apply (rule mod_type.intro) |
306 apply (rule mod_type.intro) |
306 apply (rule type_definition_bit1) |
307 apply (simp add: int_mult type_definition_bit1) |
307 apply simp |
308 apply simp |
308 apply (rule zero_bit1_def) |
309 apply (rule zero_bit1_def) |
309 apply (rule one_bit1_def) |
310 apply (rule one_bit1_def) |
310 apply (rule plus_bit1_def [unfolded Abs_bit1'_def]) |
311 apply (rule plus_bit1_def [unfolded Abs_bit1'_def]) |
311 apply (rule times_bit1_def [unfolded Abs_bit1'_def]) |
312 apply (rule times_bit1_def [unfolded Abs_bit1'_def]) |
331 qed (rule number_of_bit0_def number_of_bit1_def)+ |
332 qed (rule number_of_bit0_def number_of_bit1_def)+ |
332 |
333 |
333 end |
334 end |
334 |
335 |
335 interpretation bit0!: |
336 interpretation bit0!: |
336 mod_ring "2 * int CARD('a::finite)" |
337 mod_ring "int CARD('a::finite bit0)" |
337 "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
338 "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int" |
338 "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
339 "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0" |
339 .. |
340 .. |
340 |
341 |
341 interpretation bit1!: |
342 interpretation bit1!: |
342 mod_ring "1 + 2 * int CARD('a::finite)" |
343 mod_ring "int CARD('a::finite bit1)" |
343 "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
344 "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int" |
344 "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
345 "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1" |
345 .. |
346 .. |
346 |
347 |
347 text {* Set up cases, induction, and arithmetic *} |
348 text {* Set up cases, induction, and arithmetic *} |