nicer induction/cases rules for numeral types
authorhuffman
Thu Feb 19 17:11:12 2009 -0800 (2009-02-19)
changeset 2999819e1ef628b25
parent 29997 f6756c097c2d
child 29999 da85a244e328
nicer induction/cases rules for numeral types
src/HOL/Library/Numeral_Type.thy
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Thu Feb 19 16:51:46 2009 -0800
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Thu Feb 19 17:11:12 2009 -0800
     1.3 @@ -257,10 +257,10 @@
     1.4  begin
     1.5  
     1.6  definition Abs_bit0' :: "int \<Rightarrow> 'a bit0" where
     1.7 -  "Abs_bit0' x = Abs_bit0 (x mod (2 * int CARD('a)))"
     1.8 +  "Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))"
     1.9  
    1.10  definition Abs_bit1' :: "int \<Rightarrow> 'a bit1" where
    1.11 -  "Abs_bit1' x = Abs_bit1 (x mod (1 + 2 * int CARD('a)))"
    1.12 +  "Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))"
    1.13  
    1.14  definition "0 = Abs_bit0 0"
    1.15  definition "1 = Abs_bit0 1"
    1.16 @@ -283,11 +283,12 @@
    1.17  end
    1.18  
    1.19  interpretation bit0!:
    1.20 -  mod_type "2 * int CARD('a::finite)"
    1.21 +  mod_type "int CARD('a::finite bit0)"
    1.22             "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
    1.23             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
    1.24  apply (rule mod_type.intro)
    1.25 -apply (rule type_definition_bit0)
    1.26 +apply (simp add: int_mult type_definition_bit0)
    1.27 +apply simp
    1.28  using card_finite_pos [where ?'a='a] apply arith
    1.29  apply (rule zero_bit0_def)
    1.30  apply (rule one_bit0_def)
    1.31 @@ -299,11 +300,11 @@
    1.32  done
    1.33  
    1.34  interpretation bit1!:
    1.35 -  mod_type "1 + 2 * int CARD('a::finite)"
    1.36 +  mod_type "int CARD('a::finite bit1)"
    1.37             "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
    1.38             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
    1.39  apply (rule mod_type.intro)
    1.40 -apply (rule type_definition_bit1)
    1.41 +apply (simp add: int_mult type_definition_bit1)
    1.42  apply simp
    1.43  apply (rule zero_bit1_def)
    1.44  apply (rule one_bit1_def)
    1.45 @@ -333,13 +334,13 @@
    1.46  end
    1.47  
    1.48  interpretation bit0!:
    1.49 -  mod_ring "2 * int CARD('a::finite)"
    1.50 +  mod_ring "int CARD('a::finite bit0)"
    1.51             "Rep_bit0 :: 'a::finite bit0 \<Rightarrow> int"
    1.52             "Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
    1.53    ..
    1.54  
    1.55  interpretation bit1!:
    1.56 -  mod_ring "1 + 2 * int CARD('a::finite)"
    1.57 +  mod_ring "int CARD('a::finite bit1)"
    1.58             "Rep_bit1 :: 'a::finite bit1 \<Rightarrow> int"
    1.59             "Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
    1.60    ..