tuned ML bindings;
authorwenzelm
Fri Aug 10 18:21:25 2007 +0200 (2007-08-10)
changeset 242279b226b56e9a9
parent 24226 86f228ce1aef
child 24228 9e2234f2aff1
tuned ML bindings;
src/HOL/ex/Binary.thy
     1.1 --- a/src/HOL/ex/Binary.thy	Fri Aug 10 17:10:09 2007 +0200
     1.2 +++ b/src/HOL/ex/Binary.thy	Fri Aug 10 18:21:25 2007 +0200
     1.3 @@ -21,6 +21,8 @@
     1.4    unfolding bit_def by simp_all
     1.5  
     1.6  ML {*
     1.7 +structure Binary =
     1.8 +struct
     1.9    fun dest_bit (Const ("False", _)) = 0
    1.10      | dest_bit (Const ("True", _)) = 1
    1.11      | dest_bit t = raise TERM ("dest_bit", [t]);
    1.12 @@ -42,6 +44,7 @@
    1.13          else
    1.14            let val (q, r) = IntInf.divMod (n, 2)
    1.15            in @{term bit} $ mk_binary q $ mk_bit (IntInf.toInt r) end;
    1.16 +end
    1.17  *}
    1.18  
    1.19  
    1.20 @@ -124,7 +127,7 @@
    1.21    fun binary_proc proc ss ct =
    1.22      (case Thm.term_of ct of
    1.23        _ $ t $ u =>
    1.24 -      (case try (pairself (`dest_binary)) (t, u) of
    1.25 +      (case try (pairself (`Binary.dest_binary)) (t, u) of
    1.26          SOME args => proc (Simplifier.the_context ss) args
    1.27        | NONE => NONE)
    1.28      | _ => NONE);
    1.29 @@ -133,34 +136,34 @@
    1.30  val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
    1.31    let val k = n - m in
    1.32      if k >= 0 then
    1.33 -      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))])
    1.34 +      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (Binary.mk_binary k))])
    1.35      else
    1.36        SOME (@{thm binary_less_eq(2)} OF
    1.37 -        [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))])
    1.38 +        [prove ctxt (t == plus (plus u (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
    1.39    end);
    1.40  
    1.41  val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
    1.42    let val k = m - n in
    1.43      if k >= 0 then
    1.44 -      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))])
    1.45 +      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
    1.46      else
    1.47        SOME (@{thm binary_less(2)} OF
    1.48 -        [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))])
    1.49 +        [prove ctxt (u == plus (plus t (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
    1.50    end);
    1.51  
    1.52  val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
    1.53    let val k = m - n in
    1.54      if k >= 0 then
    1.55 -      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))])
    1.56 +      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
    1.57      else
    1.58 -      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))])
    1.59 +      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (Binary.mk_binary (~ k)))])
    1.60    end);
    1.61  
    1.62  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
    1.63    if n = 0 then NONE
    1.64    else
    1.65      let val (k, l) = IntInf.divMod (m, n)
    1.66 -    in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end);
    1.67 +    in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end);
    1.68  
    1.69  end;
    1.70  *}
    1.71 @@ -199,7 +202,7 @@
    1.72        let
    1.73          val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
    1.74          val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
    1.75 -      in syntax_consts (mk_binary n) end
    1.76 +      in syntax_consts (Binary.mk_binary n) end
    1.77    | binary_tr ts = raise TERM ("binary_tr", ts);
    1.78  
    1.79  in [("_Binary", binary_tr)] end