21 unfolding bit_def by simp_all |
21 unfolding bit_def by simp_all |
22 |
22 |
23 ML {* |
23 ML {* |
24 structure Binary = |
24 structure Binary = |
25 struct |
25 struct |
26 fun dest_bit (Const ("False", _)) = 0 |
26 fun dest_bit (Const (@{const_name False}, _)) = 0 |
27 | dest_bit (Const ("True", _)) = 1 |
27 | dest_bit (Const (@{const_name True}, _)) = 1 |
28 | dest_bit t = raise TERM ("dest_bit", [t]); |
28 | dest_bit t = raise TERM ("dest_bit", [t]); |
29 |
29 |
30 fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0 |
30 fun dest_binary (Const (@{const_name HOL.zero}, Type (@{type_name nat}, _))) = 0 |
31 | dest_binary (Const (@{const_name HOL.one}, Type ("nat", _))) = 1 |
31 | dest_binary (Const (@{const_name HOL.one}, Type (@{type_name nat}, _))) = 1 |
32 | dest_binary (Const ("Binary.bit", _) $ bs $ b) = 2 * dest_binary bs + dest_bit b |
32 | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b |
33 | dest_binary t = raise TERM ("dest_binary", [t]); |
33 | dest_binary t = raise TERM ("dest_binary", [t]); |
34 |
34 |
35 fun mk_bit 0 = @{term False} |
35 fun mk_bit 0 = @{term False} |
36 | mk_bit 1 = @{term True} |
36 | mk_bit 1 = @{term True} |
37 | mk_bit _ = raise TERM ("mk_bit", []); |
37 | mk_bit _ = raise TERM ("mk_bit", []); |