rename type pls to num0
authorhuffman
Wed Aug 22 18:53:54 2007 +0200 (2007-08-22)
changeset 24406d96eb21fc1bc
parent 24405 30887caeba62
child 24407 61b10ffb2549
rename type pls to num0
src/HOL/Library/Numeral_Type.thy
src/HOL/Word/Size.thy
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Wed Aug 22 17:58:37 2007 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Aug 22 18:53:54 2007 +0200
     1.3 @@ -79,7 +79,7 @@
     1.4  
     1.5  subsection {* Numeral Types *}
     1.6  
     1.7 -typedef (open) pls = "UNIV :: nat set" ..
     1.8 +typedef (open) num0 = "UNIV :: nat set" ..
     1.9  typedef (open) num1 = "UNIV :: unit set" ..
    1.10  typedef (open) 'a bit0 = "UNIV :: (bool * 'a) set" ..
    1.11  typedef (open) 'a bit1 = "UNIV :: (bool * 'a) option set" ..
    1.12 @@ -117,8 +117,8 @@
    1.13    unfolding type_definition.card [OF type_definition_bit1]
    1.14    by (simp only: card_prod card_option card_bool)
    1.15  
    1.16 -lemma card_pls: "CARD (pls) = 0"
    1.17 -  by (simp add: type_definition.card [OF type_definition_pls])
    1.18 +lemma card_num0: "CARD (num0) = 0"
    1.19 +  by (simp add: type_definition.card [OF type_definition_num0])
    1.20  
    1.21  lemmas card_univ_simps [simp] =
    1.22    card_unit
    1.23 @@ -130,7 +130,7 @@
    1.24    card_num1
    1.25    card_bit0
    1.26    card_bit1
    1.27 -  card_pls
    1.28 +  card_num0
    1.29  
    1.30  subsection {* Syntax *}
    1.31  
    1.32 @@ -142,13 +142,13 @@
    1.33  
    1.34  translations
    1.35    "_NumeralType1" == (type) "num1"
    1.36 -  "_NumeralType0" == (type) "pls"
    1.37 +  "_NumeralType0" == (type) "num0"
    1.38  
    1.39  parse_translation {*
    1.40  let
    1.41  
    1.42  val num1_const = Syntax.const "Numeral_Type.num1";
    1.43 -val pls_const = Syntax.const "Numeral_Type.pls";
    1.44 +val num0_const = Syntax.const "Numeral_Type.num0";
    1.45  val B0_const = Syntax.const "Numeral_Type.bit0";
    1.46  val B1_const = Syntax.const "Numeral_Type.bit1";
    1.47  
    1.48 @@ -157,7 +157,7 @@
    1.49      fun mk_bit n = if n = 0 then B0_const else B1_const;
    1.50      fun bin_of n =
    1.51        if n = 1 then num1_const
    1.52 -      else if n = 0 then pls_const
    1.53 +      else if n = 0 then num0_const
    1.54        else if n = ~1 then raise TERM ("negative type numeral", [])
    1.55        else
    1.56          let val (q, r) = IntInf.divMod (n, 2);
    1.57 @@ -176,7 +176,7 @@
    1.58  fun int_of [] = 0
    1.59    | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
    1.60  
    1.61 -fun bin_of (Const ("pls", _)) = []
    1.62 +fun bin_of (Const ("num0", _)) = []
    1.63    | bin_of (Const ("num1", _)) = [1]
    1.64    | bin_of (Const ("bit0", _) $ bs) = 0 :: bin_of bs
    1.65    | bin_of (Const ("bit1", _) $ bs) = 1 :: bin_of bs
     2.1 --- a/src/HOL/Word/Size.thy	Wed Aug 22 17:58:37 2007 +0200
     2.2 +++ b/src/HOL/Word/Size.thy	Wed Aug 22 18:53:54 2007 +0200
     2.3 @@ -25,18 +25,18 @@
     2.4  axclass len < len0
     2.5    len_gt_0 [iff]: "0 < len_of TYPE ('a :: len0)"
     2.6  
     2.7 -instance pls  :: len0 ..
     2.8 +instance num0  :: len0 ..
     2.9  instance num1 :: len0 ..
    2.10  instance bit0 :: (len0) len0 ..
    2.11  instance bit1 :: (len0) len0 ..
    2.12  
    2.13  defs (overloaded)
    2.14 -  len_pls:  "len_of (x::pls itself) == 0"
    2.15 +  len_num0: "len_of (x::num0 itself) == 0"
    2.16    len_num1: "len_of (x::num1 itself) == 1"
    2.17    len_bit0: "len_of (x::'a::len0 bit0 itself) == 2 * len_of TYPE ('a)"
    2.18    len_bit1: "len_of (x::'a::len0 bit1 itself) == 2 * len_of TYPE ('a) + 1"
    2.19  
    2.20 -lemmas len_of_numeral_defs [simp] = len_pls len_num1 len_bit0 len_bit1
    2.21 +lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
    2.22  
    2.23  instance num1 :: len by (intro_classes) simp
    2.24  instance bit0 :: (len) len by (intro_classes) simp