src/HOL/Word/Bit_Comparison.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 61799 4cf66f21b764 child 67120 491fd7f0b5df permissions -rw-r--r--
tuned proofs;
```     1 (*  Title:      HOL/Word/Bit_Comparison.thy
```
```     2     Author:     Stefan Berghofer
```
```     3     Copyright:  secunet Security Networks AG
```
```     4
```
```     5 Comparison on bit operations on integers.
```
```     6 *)
```
```     7
```
```     8 theory Bit_Comparison
```
```     9 imports Bits_Int
```
```    10 begin
```
```    11
```
```    12 lemma AND_lower [simp]:
```
```    13   fixes x :: int and y :: int
```
```    14   assumes "0 \<le> x"
```
```    15   shows "0 \<le> x AND y"
```
```    16   using assms
```
```    17 proof (induct x arbitrary: y rule: bin_induct)
```
```    18   case (3 bin bit)
```
```    19   show ?case
```
```    20   proof (cases y rule: bin_exhaust)
```
```    21     case (1 bin' bit')
```
```    22     from 3 have "0 \<le> bin"
```
```    23       by (cases bit) (simp_all add: Bit_def)
```
```    24     then have "0 \<le> bin AND bin'" by (rule 3)
```
```    25     with 1 show ?thesis
```
```    26       by simp (simp add: Bit_def)
```
```    27   qed
```
```    28 next
```
```    29   case 2
```
```    30   then show ?case by (simp only: Min_def)
```
```    31 qed simp
```
```    32
```
```    33 lemma OR_lower [simp]:
```
```    34   fixes x :: int and y :: int
```
```    35   assumes "0 \<le> x" "0 \<le> y"
```
```    36   shows "0 \<le> x OR y"
```
```    37   using assms
```
```    38 proof (induct x arbitrary: y rule: bin_induct)
```
```    39   case (3 bin bit)
```
```    40   show ?case
```
```    41   proof (cases y rule: bin_exhaust)
```
```    42     case (1 bin' bit')
```
```    43     from 3 have "0 \<le> bin"
```
```    44       by (cases bit) (simp_all add: Bit_def)
```
```    45     moreover from 1 3 have "0 \<le> bin'"
```
```    46       by (cases bit') (simp_all add: Bit_def)
```
```    47     ultimately have "0 \<le> bin OR bin'" by (rule 3)
```
```    48     with 1 show ?thesis
```
```    49       by simp (simp add: Bit_def)
```
```    50   qed
```
```    51 qed simp_all
```
```    52
```
```    53 lemma XOR_lower [simp]:
```
```    54   fixes x :: int and y :: int
```
```    55   assumes "0 \<le> x" "0 \<le> y"
```
```    56   shows "0 \<le> x XOR y"
```
```    57   using assms
```
```    58 proof (induct x arbitrary: y rule: bin_induct)
```
```    59   case (3 bin bit)
```
```    60   show ?case
```
```    61   proof (cases y rule: bin_exhaust)
```
```    62     case (1 bin' bit')
```
```    63     from 3 have "0 \<le> bin"
```
```    64       by (cases bit) (simp_all add: Bit_def)
```
```    65     moreover from 1 3 have "0 \<le> bin'"
```
```    66       by (cases bit') (simp_all add: Bit_def)
```
```    67     ultimately have "0 \<le> bin XOR bin'" by (rule 3)
```
```    68     with 1 show ?thesis
```
```    69       by simp (simp add: Bit_def)
```
```    70   qed
```
```    71 next
```
```    72   case 2
```
```    73   then show ?case by (simp only: Min_def)
```
```    74 qed simp
```
```    75
```
```    76 lemma AND_upper1 [simp]:
```
```    77   fixes x :: int and y :: int
```
```    78   assumes "0 \<le> x"
```
```    79   shows "x AND y \<le> x"
```
```    80   using assms
```
```    81 proof (induct x arbitrary: y rule: bin_induct)
```
```    82   case (3 bin bit)
```
```    83   show ?case
```
```    84   proof (cases y rule: bin_exhaust)
```
```    85     case (1 bin' bit')
```
```    86     from 3 have "0 \<le> bin"
```
```    87       by (cases bit) (simp_all add: Bit_def)
```
```    88     then have "bin AND bin' \<le> bin" by (rule 3)
```
```    89     with 1 show ?thesis
```
```    90       by simp (simp add: Bit_def)
```
```    91   qed
```
```    92 next
```
```    93   case 2
```
```    94   then show ?case by (simp only: Min_def)
```
```    95 qed simp
```
```    96
```
```    97 lemmas AND_upper1' [simp] = order_trans [OF AND_upper1]
```
```    98 lemmas AND_upper1'' [simp] = order_le_less_trans [OF AND_upper1]
```
```    99
```
```   100 lemma AND_upper2 [simp]:
```
```   101   fixes x :: int and y :: int
```
```   102   assumes "0 \<le> y"
```
```   103   shows "x AND y \<le> y"
```
```   104   using assms
```
```   105 proof (induct y arbitrary: x rule: bin_induct)
```
```   106   case (3 bin bit)
```
```   107   show ?case
```
```   108   proof (cases x rule: bin_exhaust)
```
```   109     case (1 bin' bit')
```
```   110     from 3 have "0 \<le> bin"
```
```   111       by (cases bit) (simp_all add: Bit_def)
```
```   112     then have "bin' AND bin \<le> bin" by (rule 3)
```
```   113     with 1 show ?thesis
```
```   114       by simp (simp add: Bit_def)
```
```   115   qed
```
```   116 next
```
```   117   case 2
```
```   118   then show ?case by (simp only: Min_def)
```
```   119 qed simp
```
```   120
```
```   121 lemmas AND_upper2' [simp] = order_trans [OF AND_upper2]
```
```   122 lemmas AND_upper2'' [simp] = order_le_less_trans [OF AND_upper2]
```
```   123
```
```   124 lemma OR_upper:
```
```   125   fixes x :: int and y :: int
```
```   126   assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
```
```   127   shows "x OR y < 2 ^ n"
```
```   128   using assms
```
```   129 proof (induct x arbitrary: y n rule: bin_induct)
```
```   130   case (3 bin bit)
```
```   131   show ?case
```
```   132   proof (cases y rule: bin_exhaust)
```
```   133     case (1 bin' bit')
```
```   134     show ?thesis
```
```   135     proof (cases n)
```
```   136       case 0
```
```   137       with 3 have "bin BIT bit = 0" by simp
```
```   138       then have "bin = 0" and "\<not> bit"
```
```   139         by (auto simp add: Bit_def split: if_splits) arith
```
```   140       then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
```
```   141         by simp
```
```   142     next
```
```   143       case (Suc m)
```
```   144       from 3 have "0 \<le> bin"
```
```   145         by (cases bit) (simp_all add: Bit_def)
```
```   146       moreover from 3 Suc have "bin < 2 ^ m"
```
```   147         by (cases bit) (simp_all add: Bit_def)
```
```   148       moreover from 1 3 Suc have "bin' < 2 ^ m"
```
```   149         by (cases bit') (simp_all add: Bit_def)
```
```   150       ultimately have "bin OR bin' < 2 ^ m" by (rule 3)
```
```   151       with 1 Suc show ?thesis
```
```   152         by simp (simp add: Bit_def)
```
```   153     qed
```
```   154   qed
```
```   155 qed simp_all
```
```   156
```
```   157 lemma XOR_upper:
```
```   158   fixes x :: int and y :: int
```
```   159   assumes "0 \<le> x" "x < 2 ^ n" "y < 2 ^ n"
```
```   160   shows "x XOR y < 2 ^ n"
```
```   161   using assms
```
```   162 proof (induct x arbitrary: y n rule: bin_induct)
```
```   163   case (3 bin bit)
```
```   164   show ?case
```
```   165   proof (cases y rule: bin_exhaust)
```
```   166     case (1 bin' bit')
```
```   167     show ?thesis
```
```   168     proof (cases n)
```
```   169       case 0
```
```   170       with 3 have "bin BIT bit = 0" by simp
```
```   171       then have "bin = 0" and "\<not> bit"
```
```   172         by (auto simp add: Bit_def split: if_splits) arith
```
```   173       then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
```
```   174         by simp
```
```   175     next
```
```   176       case (Suc m)
```
```   177       from 3 have "0 \<le> bin"
```
```   178         by (cases bit) (simp_all add: Bit_def)
```
```   179       moreover from 3 Suc have "bin < 2 ^ m"
```
```   180         by (cases bit) (simp_all add: Bit_def)
```
```   181       moreover from 1 3 Suc have "bin' < 2 ^ m"
```
```   182         by (cases bit') (simp_all add: Bit_def)
```
```   183       ultimately have "bin XOR bin' < 2 ^ m" by (rule 3)
```
```   184       with 1 Suc show ?thesis
```
```   185         by simp (simp add: Bit_def)
```
```   186     qed
```
```   187   qed
```
```   188 next
```
```   189   case 2
```
```   190   then show ?case by (simp only: Min_def)
```
```   191 qed simp
```
```   192
```
```   193 end
```