src/HOL/Library/Numeral_Type.thy
changeset 31021 53642251a04f
parent 30960 fec1a04b7220
child 31080 21ffc770ebc0
equal deleted inserted replaced
31020:9999a77590c3 31021:53642251a04f
   212   Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
   212   Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
   213 
   213 
   214 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
   214 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
   215 apply (intro_classes, unfold definitions)
   215 apply (intro_classes, unfold definitions)
   216 apply (simp_all add: Rep_simps zmod_simps ring_simps)
   216 apply (simp_all add: Rep_simps zmod_simps ring_simps)
   217 done
       
   218 
       
   219 lemma recpower: "OFCLASS('a, recpower_class)"
       
   220 apply (intro_classes, unfold definitions)
       
   221 apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc
       
   222                      mod_pos_pos_trivial size1)
       
   223 done
   217 done
   224 
   218 
   225 end
   219 end
   226 
   220 
   227 locale mod_ring = mod_type +
   221 locale mod_ring = mod_type +
   338 apply (rule times_bit1_def [unfolded Abs_bit1'_def])
   332 apply (rule times_bit1_def [unfolded Abs_bit1'_def])
   339 apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
   333 apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
   340 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
   334 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
   341 done
   335 done
   342 
   336 
   343 instance bit0 :: (finite) "{comm_ring_1,recpower}"
   337 instance bit0 :: (finite) comm_ring_1
   344   by (rule bit0.comm_ring_1 bit0.recpower)+
   338   by (rule bit0.comm_ring_1)+
   345 
   339 
   346 instance bit1 :: (finite) "{comm_ring_1,recpower}"
   340 instance bit1 :: (finite) comm_ring_1
   347   by (rule bit1.comm_ring_1 bit1.recpower)+
   341   by (rule bit1.comm_ring_1)+
   348 
   342 
   349 instantiation bit0 and bit1 :: (finite) number_ring
   343 instantiation bit0 and bit1 :: (finite) number_ring
   350 begin
   344 begin
   351 
   345 
   352 definition "(number_of w :: _ bit0) = of_int w"
   346 definition "(number_of w :: _ bit0) = of_int w"