src/HOL/Library/Numeral_Type.thy
 changeset 29998 19e1ef628b25 parent 29997 f6756c097c2d child 29999 da85a244e328
--- 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 \<Rightarrow> '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 \<Rightarrow> '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 \<Rightarrow> int"
"Abs_bit0 :: int \<Rightarrow> 'a::finite bit0"
apply (rule mod_type.intro)
-apply (rule 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 \<Rightarrow> int"
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
apply (rule mod_type.intro)
-apply (rule 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 \<Rightarrow> int"
"Abs_bit0 :: int \<Rightarrow> '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 \<Rightarrow> int"
"Abs_bit1 :: int \<Rightarrow> 'a::finite bit1"
..