equal
deleted
inserted
replaced
25 struct |
25 struct |
26 fun dest_bit (Const (@{const_name False}, _)) = 0 |
26 fun dest_bit (Const (@{const_name False}, _)) = 0 |
27 | dest_bit (Const (@{const_name 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 (@{type_name nat}, _))) = 0 |
30 fun dest_binary (Const (@{const_name Algebras.zero}, Type (@{type_name nat}, _))) = 0 |
31 | dest_binary (Const (@{const_name HOL.one}, Type (@{type_name nat}, _))) = 1 |
31 | dest_binary (Const (@{const_name Algebras.one}, Type (@{type_name nat}, _))) = 1 |
32 | dest_binary (Const (@{const_name 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} |