src/HOL/Num.thy
changeset 52143 36ffe23b25f8
parent 51143 0a2371e7ced3
child 52187 1f7b3aadec69
     1.1 --- a/src/HOL/Num.thy	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/HOL/Num.thy	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -291,50 +291,54 @@
     1.4    "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
     1.5  
     1.6  parse_translation {*
     1.7 -let
     1.8 -  fun num_of_int n = if n > 0 then case IntInf.quotRem (n, 2)
     1.9 -     of (0, 1) => Syntax.const @{const_name One}
    1.10 -      | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
    1.11 -      | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n
    1.12 -    else raise Match;
    1.13 -  val pos = Syntax.const @{const_name numeral}
    1.14 -  val neg = Syntax.const @{const_name neg_numeral}
    1.15 -  val one = Syntax.const @{const_name Groups.one}
    1.16 -  val zero = Syntax.const @{const_name Groups.zero}
    1.17 -  fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
    1.18 -        c $ numeral_tr [t] $ u
    1.19 -    | numeral_tr [Const (num, _)] =
    1.20 -        let
    1.21 -          val {value, ...} = Lexicon.read_xnum num;
    1.22 -        in
    1.23 -          if value = 0 then zero else
    1.24 -          if value > 0
    1.25 -          then pos $ num_of_int value
    1.26 -          else neg $ num_of_int (~value)
    1.27 -        end
    1.28 -    | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.29 -in [("_Numeral", numeral_tr)] end
    1.30 +  let
    1.31 +    fun num_of_int n =
    1.32 +      if n > 0 then
    1.33 +        (case IntInf.quotRem (n, 2) of
    1.34 +          (0, 1) => Syntax.const @{const_name One}
    1.35 +        | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
    1.36 +        | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
    1.37 +      else raise Match
    1.38 +    val pos = Syntax.const @{const_name numeral}
    1.39 +    val neg = Syntax.const @{const_name neg_numeral}
    1.40 +    val one = Syntax.const @{const_name Groups.one}
    1.41 +    val zero = Syntax.const @{const_name Groups.zero}
    1.42 +    fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
    1.43 +          c $ numeral_tr [t] $ u
    1.44 +      | numeral_tr [Const (num, _)] =
    1.45 +          let
    1.46 +            val {value, ...} = Lexicon.read_xnum num;
    1.47 +          in
    1.48 +            if value = 0 then zero else
    1.49 +            if value > 0
    1.50 +            then pos $ num_of_int value
    1.51 +            else neg $ num_of_int (~value)
    1.52 +          end
    1.53 +      | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.54 +  in [("_Numeral", K numeral_tr)] end
    1.55  *}
    1.56  
    1.57 -typed_print_translation (advanced) {*
    1.58 -let
    1.59 -  fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
    1.60 -    | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
    1.61 -    | dest_num (Const (@{const_syntax One}, _)) = 1;
    1.62 -  fun num_tr' sign ctxt T [n] =
    1.63 -    let
    1.64 -      val k = dest_num n;
    1.65 -      val t' = Syntax.const @{syntax_const "_Numeral"} $
    1.66 -        Syntax.free (sign ^ string_of_int k);
    1.67 -    in
    1.68 -      case T of
    1.69 -        Type (@{type_name fun}, [_, T']) =>
    1.70 -          if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
    1.71 -          else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
    1.72 -      | T' => if T' = dummyT then t' else raise Match
    1.73 -    end;
    1.74 -in [(@{const_syntax numeral}, num_tr' ""),
    1.75 -    (@{const_syntax neg_numeral}, num_tr' "-")] end
    1.76 +typed_print_translation {*
    1.77 +  let
    1.78 +    fun dest_num (Const (@{const_syntax Bit0}, _) $ n) = 2 * dest_num n
    1.79 +      | dest_num (Const (@{const_syntax Bit1}, _) $ n) = 2 * dest_num n + 1
    1.80 +      | dest_num (Const (@{const_syntax One}, _)) = 1;
    1.81 +    fun num_tr' sign ctxt T [n] =
    1.82 +      let
    1.83 +        val k = dest_num n;
    1.84 +        val t' = Syntax.const @{syntax_const "_Numeral"} $
    1.85 +          Syntax.free (sign ^ string_of_int k);
    1.86 +      in
    1.87 +        (case T of
    1.88 +          Type (@{type_name fun}, [_, T']) =>
    1.89 +            if not (Printer.show_type_constraint ctxt) andalso can Term.dest_Type T' then t'
    1.90 +            else Syntax.const @{syntax_const "_constrain"} $ t' $ Syntax_Phases.term_of_typ ctxt T'
    1.91 +        | T' => if T' = dummyT then t' else raise Match)
    1.92 +      end;
    1.93 +  in
    1.94 +   [(@{const_syntax numeral}, num_tr' ""),
    1.95 +    (@{const_syntax neg_numeral}, num_tr' "-")]
    1.96 +  end
    1.97  *}
    1.98  
    1.99  ML_file "Tools/numeral.ML"