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; |