src/HOL/Word/Bit_Comparison.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 61799 4cf66f21b764
child 67120 491fd7f0b5df
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
     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