# HG changeset patch # User huffman # Date 1235092272 28800 # Node ID 19e1ef628b25e902895b165b2bd4183c6033de3c # Parent f6756c097c2d3b0bb60f35fe7a7edbf3d4ae5c81 nicer induction/cases rules for numeral types diff -r f6756c097c2d -r 19e1ef628b25 src/HOL/Library/Numeral_Type.thy --- a/src/HOL/Library/Numeral_Type.thy Thu Feb 19 16:51:46 2009 -0800 +++ b/src/HOL/Library/Numeral_Type.thy Thu Feb 19 17:11:12 2009 -0800 @@ -257,10 +257,10 @@ begin definition Abs_bit0' :: "int \ 'a bit0" where - "Abs_bit0' x = Abs_bit0 (x mod (2 * int CARD('a)))" + "Abs_bit0' x = Abs_bit0 (x mod int CARD('a bit0))" definition Abs_bit1' :: "int \ 'a bit1" where - "Abs_bit1' x = Abs_bit1 (x mod (1 + 2 * int CARD('a)))" + "Abs_bit1' x = Abs_bit1 (x mod int CARD('a bit1))" definition "0 = Abs_bit0 0" definition "1 = Abs_bit0 1" @@ -283,11 +283,12 @@ end interpretation bit0!: - mod_type "2 * int CARD('a::finite)" + mod_type "int CARD('a::finite bit0)" "Rep_bit0 :: 'a::finite bit0 \ int" "Abs_bit0 :: int \ 'a::finite bit0" apply (rule mod_type.intro) -apply (rule type_definition_bit0) +apply (simp add: int_mult type_definition_bit0) +apply simp using card_finite_pos [where ?'a='a] apply arith apply (rule zero_bit0_def) apply (rule one_bit0_def) @@ -299,11 +300,11 @@ done interpretation bit1!: - mod_type "1 + 2 * int CARD('a::finite)" + mod_type "int CARD('a::finite bit1)" "Rep_bit1 :: 'a::finite bit1 \ int" "Abs_bit1 :: int \ 'a::finite bit1" apply (rule mod_type.intro) -apply (rule type_definition_bit1) +apply (simp add: int_mult type_definition_bit1) apply simp apply (rule zero_bit1_def) apply (rule one_bit1_def) @@ -333,13 +334,13 @@ end interpretation bit0!: - mod_ring "2 * int CARD('a::finite)" + mod_ring "int CARD('a::finite bit0)" "Rep_bit0 :: 'a::finite bit0 \ int" "Abs_bit0 :: int \ 'a::finite bit0" .. interpretation bit1!: - mod_ring "1 + 2 * int CARD('a::finite)" + mod_ring "int CARD('a::finite bit1)" "Rep_bit1 :: 'a::finite bit1 \ int" "Abs_bit1 :: int \ 'a::finite bit1" ..