summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Fri, 24 Apr 2020 13:16:42 +0000 | |

changeset 71800 | 35a951ed2e82 |

parent 71799 | e00712b4e2c2 |

child 71801 | 49d8d8ad7e43 |

documentation of relevant ideas

--- a/src/HOL/ex/Bit_Operations.thy Fri Apr 24 13:16:41 2020 +0000 +++ b/src/HOL/ex/Bit_Operations.thy Fri Apr 24 13:16:42 2020 +0000 @@ -606,4 +606,72 @@ lifting_update natural.lifting lifting_forget natural.lifting + +subsection \<open>Key ideas of bit operations\<close> + +subsection \<open>Key ideas of bit operations\<close> + +text \<open> + When formalizing bit operations, it is tempting to represent + bit values as explicit lists over a binary type. This however + is a bad idea, mainly due to the inherent ambiguities in + representation concerning repeating leading bits. + + Hence this approach avoids such explicit lists altogether + following an algebraic path: + + \<^item> Bit values are represented by numeric types: idealized + unbounded bit values can be represented by type \<^typ>\<open>int\<close>, + bounded bit values by quotient types over \<^typ>\<open>int\<close>. + + \<^item> (A special case are idealized unbounded bit values ending + in @{term [source] 0} which can be represented by type \<^typ>\<open>nat\<close> but + only support a restricted set of operations). + + \<^item> From this idea follows that + + \<^item> multiplication by \<^term>\<open>2 :: int\<close> is a bit shift to the left and + + \<^item> division by \<^term>\<open>2 :: int\<close> is a bit shift to the right. + + \<^item> Concerning bounded bit values, iterated shifts to the left + may result in eliminating all bits by shifting them all + beyond the boundary. The property \<^prop>\<open>(2 :: int) ^ n \<noteq> 0\<close> + represents that \<^term>\<open>n\<close> is \<^emph>\<open>not\<close> beyond that boundary. + + \<^item> The projection on a single bit is then @{thm bit_def [where ?'a = int, no_vars]}. + + \<^item> This leads to the most fundamental properties of bit values: + + \<^item> Equality rule: @{thm bit_eqI [where ?'a = int, no_vars]} + + \<^item> Induction rule: @{thm bits_induct [where ?'a = int, no_vars]} + + \<^item> Typical operations are characterized as follows: + + \<^item> Singleton \<^term>\<open>n\<close>th bit: \<^term>\<open>(2 :: int) ^ n\<close> + + \<^item> Bit mask upto bit \<^term>\<open>n\<close>: \<^term>\<open>(2 :: int) ^ n - 1\<close> + + \<^item> Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]} + + \<^item> Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]} + + \<^item> Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]} + + \<^item> Negation: @{thm bit_not_iff [where ?'a = int, no_vars]} + + \<^item> And: @{thm bit_and_iff [where ?'a = int, no_vars]} + + \<^item> Or: @{thm bit_or_iff [where ?'a = int, no_vars]} + + \<^item> Xor: @{thm bit_xor_iff [where ?'a = int, no_vars]} + + \<^item> Set a single bit: @{thm set_bit_def [where ?'a = int, no_vars]} + + \<^item> Unset a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]} + + \<^item> Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]} +\<close> + end