more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
authorwenzelm
Fri Mar 07 11:46:26 2014 +0100 (2014-03-07)
changeset 55974c835a9379026
parent 55973 471a71017cfc
child 55975 9962ca0875c9
more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
src/HOL/Num.thy
src/HOL/Rat.thy
src/HOL/Tools/Ctr_Sugar/case_translation.ML
     1.1 --- a/src/HOL/Num.thy	Fri Mar 07 11:41:25 2014 +0100
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 07 11:46:26 2014 +0100
     1.3 @@ -285,14 +285,14 @@
     1.4      fun num_of_int n =
     1.5        if n > 0 then
     1.6          (case IntInf.quotRem (n, 2) of
     1.7 -          (0, 1) => Syntax.const @{const_name One}
     1.8 -        | (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
     1.9 -        | (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
    1.10 +          (0, 1) => Syntax.const @{const_syntax One}
    1.11 +        | (n, 0) => Syntax.const @{const_syntax Bit0} $ num_of_int n
    1.12 +        | (n, 1) => Syntax.const @{const_syntax Bit1} $ num_of_int n)
    1.13        else raise Match
    1.14 -    val numeral = Syntax.const @{const_name numeral}
    1.15 -    val uminus = Syntax.const @{const_name uminus}
    1.16 -    val one = Syntax.const @{const_name Groups.one}
    1.17 -    val zero = Syntax.const @{const_name Groups.zero}
    1.18 +    val numeral = Syntax.const @{const_syntax numeral}
    1.19 +    val uminus = Syntax.const @{const_syntax uminus}
    1.20 +    val one = Syntax.const @{const_syntax Groups.one}
    1.21 +    val zero = Syntax.const @{const_syntax Groups.zero}
    1.22      fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
    1.23            c $ numeral_tr [t] $ u
    1.24        | numeral_tr [Const (num, _)] =
    1.25 @@ -303,10 +303,10 @@
    1.26              if value > 0
    1.27              then numeral $ num_of_int value
    1.28              else if value = ~1 then uminus $ one
    1.29 -            else uminus $ (numeral $ num_of_int (~value))
    1.30 +            else uminus $ (numeral $ num_of_int (~ value))
    1.31            end
    1.32        | numeral_tr ts = raise TERM ("numeral_tr", ts);
    1.33 -  in [("_Numeral", K numeral_tr)] end
    1.34 +  in [(@{syntax_const "_Numeral"}, K numeral_tr)] end
    1.35  *}
    1.36  
    1.37  typed_print_translation {*
     2.1 --- a/src/HOL/Rat.thy	Fri Mar 07 11:41:25 2014 +0100
     2.2 +++ b/src/HOL/Rat.thy	Fri Mar 07 11:46:26 2014 +0100
     2.3 @@ -1155,12 +1155,16 @@
     2.4        let
     2.5          fun mk 1 = Syntax.const @{const_syntax Num.One}
     2.6            | mk i =
     2.7 -              let val (q, r) = Integer.div_mod i 2
     2.8 -              in HOLogic.mk_bit r $ (mk q) end;
     2.9 +              let
    2.10 +                val (q, r) = Integer.div_mod i 2;
    2.11 +                val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1};
    2.12 +              in Syntax.const bit $ (mk q) end;
    2.13        in
    2.14          if i = 0 then Syntax.const @{const_syntax Groups.zero}
    2.15          else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
    2.16 -        else Syntax.const @{const_syntax Groups.uminus} $ (Syntax.const @{const_syntax Num.numeral} $ mk (~i))
    2.17 +        else
    2.18 +          Syntax.const @{const_syntax Groups.uminus} $
    2.19 +            (Syntax.const @{const_syntax Num.numeral} $ mk (~ i))
    2.20        end;
    2.21  
    2.22      fun mk_frac str =
    2.23 @@ -1181,6 +1185,7 @@
    2.24  lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
    2.25    by simp
    2.26  
    2.27 +
    2.28  subsection {* Hiding implementation details *}
    2.29  
    2.30  hide_const (open) normalize positive
     3.1 --- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 11:41:25 2014 +0100
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Fri Mar 07 11:46:26 2014 +0100
     3.3 @@ -169,7 +169,7 @@
     3.4          fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
     3.5            | dest_case2 t = [t];
     3.6  
     3.7 -        val errt = if err then @{term True} else @{term False};
     3.8 +        val errt = Syntax.const (if err then @{const_syntax True} else @{const_syntax False});
     3.9        in
    3.10          Syntax.const @{const_syntax case_guard} $ errt $ t $
    3.11            (fold_rev