--- a/src/HOL/Library/Numeral_Type.thy Wed Aug 22 17:58:37 2007 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Wed Aug 22 18:53:54 2007 +0200
@@ -79,7 +79,7 @@
subsection {* Numeral Types *}
-typedef (open) pls = "UNIV :: nat set" ..
+typedef (open) num0 = "UNIV :: nat set" ..
typedef (open) num1 = "UNIV :: unit set" ..
typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" ..
typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" ..
@@ -117,8 +117,8 @@
unfolding type_definition.card [OF type_definition_bit1]
by (simp only: card_prod card_option card_bool)
-lemma card_pls: "CARD (pls) = 0"
- by (simp add: type_definition.card [OF type_definition_pls])
+lemma card_num0: "CARD (num0) = 0"
+ by (simp add: type_definition.card [OF type_definition_num0])
lemmas card_univ_simps [simp] =
card_unit
@@ -130,7 +130,7 @@
card_num1
card_bit0
card_bit1
- card_pls
+ card_num0
subsection {* Syntax *}
@@ -142,13 +142,13 @@
translations
"_NumeralType1" == (type) "num1"
- "_NumeralType0" == (type) "pls"
+ "_NumeralType0" == (type) "num0"
parse_translation {*
let
val num1_const = Syntax.const "Numeral_Type.num1";
-val pls_const = Syntax.const "Numeral_Type.pls";
+val num0_const = Syntax.const "Numeral_Type.num0";
val B0_const = Syntax.const "Numeral_Type.bit0";
val B1_const = Syntax.const "Numeral_Type.bit1";
@@ -157,7 +157,7 @@
fun mk_bit n = if n = 0 then B0_const else B1_const;
fun bin_of n =
if n = 1 then num1_const
- else if n = 0 then pls_const
+ else if n = 0 then num0_const
else if n = ~1 then raise TERM ("negative type numeral", [])
else
let val (q, r) = IntInf.divMod (n, 2);
@@ -176,7 +176,7 @@
fun int_of [] = 0
| int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
-fun bin_of (Const ("pls", _)) = []
+fun bin_of (Const ("num0", _)) = []
| bin_of (Const ("num1", _)) = [1]
| bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
| bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
--- a/src/HOL/Word/Size.thy Wed Aug 22 17:58:37 2007 +0200
+++ b/src/HOL/Word/Size.thy Wed Aug 22 18:53:54 2007 +0200
@@ -25,18 +25,18 @@
axclass len < len0
len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
-instance pls :: len0 ..
+instance num0 :: len0 ..
instance num1 :: len0 ..
instance bit0 :: (len0) len0 ..
instance bit1 :: (len0) len0 ..
defs (overloaded)
- len_pls: "len_of (x::pls itself) == 0"
+ len_num0: "len_of (x::num0 itself) == 0"
len_num1: "len_of (x::num1 itself) == 1"
len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
-lemmas len_of_numeral_defs [simp] = len_pls len_num1 len_bit0 len_bit1
+lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
instance num1 :: len by (intro_classes) simp
instance bit0 :: (len) len by (intro_classes) simp