src/HOL/Library/Numeral_Type.thy
changeset 52143 36ffe23b25f8
parent 51288 be7e9a675ec9
child 52147 9943f8067f11
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -324,7 +324,7 @@
     1.4  code_datatype Num0
     1.5  
     1.6  instantiation num0 :: equal begin
     1.7 -definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool" 
     1.8 +definition equal_num0 :: "num0 \<Rightarrow> num0 \<Rightarrow> bool"
     1.9    where "equal_num0 = op ="
    1.10  instance by intro_classes (simp add: equal_num0_def)
    1.11  end
    1.12 @@ -351,7 +351,7 @@
    1.13  definition "enum_class.enum_ex P = P (1 :: num1)"
    1.14  instance
    1.15    by intro_classes
    1.16 -     (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def, 
    1.17 +     (auto simp add: enum_num1_def enum_all_num1_def enum_ex_num1_def num1_eq_iff Ball_def,
    1.18        (metis (full_types) num1_eq_iff)+)
    1.19  end
    1.20  
    1.21 @@ -477,47 +477,49 @@
    1.22    (type) "0" == (type) "num0"
    1.23  
    1.24  parse_translation {*
    1.25 -let
    1.26 -  fun mk_bintype n =
    1.27 -    let
    1.28 -      fun mk_bit 0 = Syntax.const @{type_syntax bit0}
    1.29 -        | mk_bit 1 = Syntax.const @{type_syntax bit1};
    1.30 -      fun bin_of n =
    1.31 -        if n = 1 then Syntax.const @{type_syntax num1}
    1.32 -        else if n = 0 then Syntax.const @{type_syntax num0}
    1.33 -        else if n = ~1 then raise TERM ("negative type numeral", [])
    1.34 -        else
    1.35 -          let val (q, r) = Integer.div_mod n 2;
    1.36 -          in mk_bit r $ bin_of q end;
    1.37 -    in bin_of n end;
    1.38 +  let
    1.39 +    fun mk_bintype n =
    1.40 +      let
    1.41 +        fun mk_bit 0 = Syntax.const @{type_syntax bit0}
    1.42 +          | mk_bit 1 = Syntax.const @{type_syntax bit1};
    1.43 +        fun bin_of n =
    1.44 +          if n = 1 then Syntax.const @{type_syntax num1}
    1.45 +          else if n = 0 then Syntax.const @{type_syntax num0}
    1.46 +          else if n = ~1 then raise TERM ("negative type numeral", [])
    1.47 +          else
    1.48 +            let val (q, r) = Integer.div_mod n 2;
    1.49 +            in mk_bit r $ bin_of q end;
    1.50 +      in bin_of n end;
    1.51  
    1.52 -  fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
    1.53 -    | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.54 +    fun numeral_tr [Free (str, _)] = mk_bintype (the (Int.fromString str))
    1.55 +      | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.56  
    1.57 -in [(@{syntax_const "_NumeralType"}, numeral_tr)] end;
    1.58 +  in [(@{syntax_const "_NumeralType"}, K numeral_tr)] end;
    1.59  *}
    1.60  
    1.61  print_translation {*
    1.62 -let
    1.63 -  fun int_of [] = 0
    1.64 -    | int_of (b :: bs) = b + 2 * int_of bs;
    1.65 +  let
    1.66 +    fun int_of [] = 0
    1.67 +      | int_of (b :: bs) = b + 2 * int_of bs;
    1.68  
    1.69 -  fun bin_of (Const (@{type_syntax num0}, _)) = []
    1.70 -    | bin_of (Const (@{type_syntax num1}, _)) = [1]
    1.71 -    | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
    1.72 -    | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
    1.73 -    | bin_of t = raise TERM ("bin_of", [t]);
    1.74 +    fun bin_of (Const (@{type_syntax num0}, _)) = []
    1.75 +      | bin_of (Const (@{type_syntax num1}, _)) = [1]
    1.76 +      | bin_of (Const (@{type_syntax bit0}, _) $ bs) = 0 :: bin_of bs
    1.77 +      | bin_of (Const (@{type_syntax bit1}, _) $ bs) = 1 :: bin_of bs
    1.78 +      | bin_of t = raise TERM ("bin_of", [t]);
    1.79  
    1.80 -  fun bit_tr' b [t] =
    1.81 -        let
    1.82 -          val rev_digs = b :: bin_of t handle TERM _ => raise Match
    1.83 -          val i = int_of rev_digs;
    1.84 -          val num = string_of_int (abs i);
    1.85 -        in
    1.86 -          Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
    1.87 -        end
    1.88 -    | bit_tr' b _ = raise Match;
    1.89 -in [(@{type_syntax bit0}, bit_tr' 0), (@{type_syntax bit1}, bit_tr' 1)] end;
    1.90 +    fun bit_tr' b [t] =
    1.91 +          let
    1.92 +            val rev_digs = b :: bin_of t handle TERM _ => raise Match
    1.93 +            val i = int_of rev_digs;
    1.94 +            val num = string_of_int (abs i);
    1.95 +          in
    1.96 +            Syntax.const @{syntax_const "_NumeralType"} $ Syntax.free num
    1.97 +          end
    1.98 +      | bit_tr' b _ = raise Match;
    1.99 +  in
   1.100 +   [(@{type_syntax bit0}, K (bit_tr' 0)),
   1.101 +    (@{type_syntax bit1}, K (bit_tr' 1))] end;
   1.102  *}
   1.103  
   1.104  subsection {* Examples *}