src/HOL/Library/Numeral_Type.thy
changeset 24406 d96eb21fc1bc
parent 24332 e3a2b75b1cf9
child 24407 61b10ffb2549
     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