src/ZF/int_arith.ML
changeset 35112 ff6f60e6ab85
parent 35020 862a20ffa8e2
child 35123 e286d5df187a
     1.1 --- a/src/ZF/int_arith.ML	Thu Feb 11 22:03:37 2010 +0100
     1.2 +++ b/src/ZF/int_arith.ML	Thu Feb 11 22:06:37 2010 +0100
     1.3 @@ -7,15 +7,40 @@
     1.4  structure Int_Numeral_Simprocs =
     1.5  struct
     1.6  
     1.7 +(* abstract syntax operations *)
     1.8 +
     1.9 +fun mk_bit 0 = @{term "0"}
    1.10 +  | mk_bit 1 = @{term "succ(0)"}
    1.11 +  | mk_bit _ = sys_error "mk_bit";
    1.12 +
    1.13 +fun dest_bit @{term "0"} = 0
    1.14 +  | dest_bit @{term "succ(0)"} = 1
    1.15 +  | dest_bit _ = raise Match;
    1.16 +
    1.17 +fun mk_bin i =
    1.18 +  let
    1.19 +    fun term_of [] = @{term Pls}
    1.20 +      | term_of [~1] = @{term Min}
    1.21 +      | term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b;
    1.22 +  in term_of (NumeralSyntax.make_binary i) end;
    1.23 +
    1.24 +fun dest_bin tm =
    1.25 +  let
    1.26 +    fun bin_of @{term Pls} = []
    1.27 +      | bin_of @{term Min} = [~1]
    1.28 +      | bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
    1.29 +      | bin_of _ = sys_error "dest_bin";
    1.30 +  in NumeralSyntax.dest_binary (bin_of tm) end;
    1.31 +
    1.32 +
    1.33  (*Utilities*)
    1.34  
    1.35 -fun mk_numeral n = @{const integ_of} $ NumeralSyntax.mk_bin n;
    1.36 +fun mk_numeral i = @{const integ_of} $ mk_bin i;
    1.37  
    1.38  (*Decodes a binary INTEGER*)
    1.39  fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
    1.40 -     (NumeralSyntax.dest_bin w
    1.41 -      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    1.42 -  | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    1.43 +     (dest_bin w handle SYS_ERROR _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    1.44 +  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    1.45  
    1.46  fun find_first_numeral past (t::terms) =
    1.47          ((dest_numeral t, rev past @ terms)