src/HOL/Tools/numeral_syntax.ML
changeset 13491 ddf6ae639f21
parent 13110 ca8cd110f769
child 13495 af27202d6d1c
equal deleted inserted replaced
13490:44bdc150211b 13491:ddf6ae639f21
    27 
    27 
    28 fun prefix_len _ [] = 0
    28 fun prefix_len _ [] = 0
    29   | prefix_len pred (x :: xs) =
    29   | prefix_len pred (x :: xs) =
    30       if pred x then 1 + prefix_len pred xs else 0;
    30       if pred x then 1 + prefix_len pred xs else 0;
    31 
    31 
    32 (*we consider all "spellings"; Min is likely to be declared elsewhere*)
    32 fun bin_of (Const ("bin.Pls", _)) = []
    33 fun bin_of (Const ("Pls", _)) = []
       
    34   | bin_of (Const ("bin.Pls", _)) = []
       
    35   | bin_of (Const ("Numeral.bin.Pls", _)) = []
    33   | bin_of (Const ("Numeral.bin.Pls", _)) = []
    36   | bin_of (Const ("Min", _)) = [~1]
       
    37   | bin_of (Const ("bin.Min", _)) = [~1]
    34   | bin_of (Const ("bin.Min", _)) = [~1]
    38   | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
    35   | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
    39   | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
       
    40   | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    36   | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    41   | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    37   | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
    42   | bin_of _ = raise Match;
    38   | bin_of _ = raise Match;
    43 
    39 
    44 val dest_bin = HOLogic.int_of o bin_of;
    40 val dest_bin = HOLogic.int_of o bin_of;
    76 
    72 
    77 
    73 
    78 (* theory setup *)
    74 (* theory setup *)
    79 
    75 
    80 val setup =
    76 val setup =
    81  [Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    77  [Theory.hide_consts false
       
    78     ["Numeral.bin.Pls", "Numeral.bin.Min"],
       
    79 Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
    82   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    80   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
    83 
    81 
    84 
    82 
    85 end;
    83 end;