src/HOL/Library/Numeral_Type.thy
changeset 29998 19e1ef628b25
parent 29997 f6756c097c2d
child 29999 da85a244e328
equal deleted inserted replaced
29997:f6756c097c2d 29998:19e1ef628b25
   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 *}