src/HOL/Integ/Numeral.thy
 author nipkow Wed Aug 18 11:09:40 2004 +0200 (2004-08-18) changeset 15140 322485b816ac parent 15131 c69542757a4d child 15620 8ccdc8bc66a2 permissions -rw-r--r--
import -> imports
```     1 (*  Title:	HOL/Integ/Numeral.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:	Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright	1994  University of Cambridge
```
```     5 *)
```
```     6
```
```     7 header{*Arithmetic on Binary Integers*}
```
```     8
```
```     9 theory Numeral
```
```    10 imports IntDef
```
```    11 files "Tools/numeral_syntax.ML"
```
```    12 begin
```
```    13
```
```    14 text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
```
```    15    Only qualified access Numeral.Pls and Numeral.Min is allowed.
```
```    16    We do not hide Bit because we need the BIT infix syntax.*}
```
```    17
```
```    18 text{*This formalization defines binary arithmetic in terms of the integers
```
```    19 rather than using a datatype. This avoids multiple representations (leading
```
```    20 zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
```
```    21 int_of_binary}, for the numerical interpretation.
```
```    22
```
```    23 The representation expects that @{text "(m mod 2)"} is 0 or 1,
```
```    24 even if m is negative;
```
```    25 For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
```
```    26 @{text "-5 = (-3)*2 + 1"}.
```
```    27 *}
```
```    28
```
```    29
```
```    30 typedef (Bin)
```
```    31   bin = "UNIV::int set"
```
```    32     by (auto)
```
```    33
```
```    34 constdefs
```
```    35   Pls :: "bin"
```
```    36    "Pls == Abs_Bin 0"
```
```    37
```
```    38   Min :: "bin"
```
```    39    "Min == Abs_Bin (- 1)"
```
```    40
```
```    41   Bit :: "[bin,bool] => bin"    (infixl "BIT" 90)
```
```    42    --{*That is, 2w+b*}
```
```    43    "w BIT b == Abs_Bin ((if b then 1 else 0) + Rep_Bin w + Rep_Bin w)"
```
```    44
```
```    45
```
```    46 axclass
```
```    47   number < type  -- {* for numeric types: nat, int, real, \dots *}
```
```    48
```
```    49 consts
```
```    50   number_of :: "bin => 'a::number"
```
```    51
```
```    52 syntax
```
```    53   "_Numeral" :: "num_const => 'a"    ("_")
```
```    54   Numeral0 :: 'a
```
```    55   Numeral1 :: 'a
```
```    56
```
```    57 translations
```
```    58   "Numeral0" == "number_of Numeral.Pls"
```
```    59   "Numeral1" == "number_of (Numeral.Pls BIT True)"
```
```    60
```
```    61
```
```    62 setup NumeralSyntax.setup
```
```    63
```
```    64 syntax (xsymbols)
```
```    65   "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
```
```    66 syntax (HTML output)
```
```    67   "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
```
```    68 syntax (output)
```
```    69   "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
```
```    70 translations
```
```    71   "x\<twosuperior>" == "x^2"
```
```    72   "x\<twosuperior>" <= "x^(2::nat)"
```
```    73
```
```    74
```
```    75 lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
```
```    76   -- {* Unfold all @{text let}s involving constants *}
```
```    77   by (simp add: Let_def)
```
```    78
```
```    79 lemma Let_0 [simp]: "Let 0 f == f 0"
```
```    80   by (simp add: Let_def)
```
```    81
```
```    82 lemma Let_1 [simp]: "Let 1 f == f 1"
```
```    83   by (simp add: Let_def)
```
```    84
```
```    85
```
```    86 constdefs
```
```    87   bin_succ  :: "bin=>bin"
```
```    88    "bin_succ w == Abs_Bin(Rep_Bin w + 1)"
```
```    89
```
```    90   bin_pred  :: "bin=>bin"
```
```    91    "bin_pred w == Abs_Bin(Rep_Bin w - 1)"
```
```    92
```
```    93   bin_minus  :: "bin=>bin"
```
```    94    "bin_minus w == Abs_Bin(- (Rep_Bin w))"
```
```    95
```
```    96   bin_add  :: "[bin,bin]=>bin"
```
```    97    "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
```
```    98
```
```    99   bin_mult  :: "[bin,bin]=>bin"
```
```   100    "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
```
```   101
```
```   102
```
```   103 lemmas Bin_simps =
```
```   104        bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
```
```   105        Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
```
```   106
```
```   107 text{*Removal of leading zeroes*}
```
```   108 lemma Pls_0_eq [simp]: "Numeral.Pls BIT False = Numeral.Pls"
```
```   109 by (simp add: Bin_simps)
```
```   110
```
```   111 lemma Min_1_eq [simp]: "Numeral.Min BIT True = Numeral.Min"
```
```   112 by (simp add: Bin_simps)
```
```   113
```
```   114 subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
```
```   115
```
```   116 lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT True"
```
```   117 by (simp add: Bin_simps)
```
```   118
```
```   119 lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
```
```   120 by (simp add: Bin_simps)
```
```   121
```
```   122 lemma bin_succ_1 [simp]: "bin_succ(w BIT True) = (bin_succ w) BIT False"
```
```   123 by (simp add: Bin_simps add_ac)
```
```   124
```
```   125 lemma bin_succ_0 [simp]: "bin_succ(w BIT False) = w BIT True"
```
```   126 by (simp add: Bin_simps add_ac)
```
```   127
```
```   128 lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
```
```   129 by (simp add: Bin_simps)
```
```   130
```
```   131 lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT False"
```
```   132 by (simp add: Bin_simps diff_minus)
```
```   133
```
```   134 lemma bin_pred_1 [simp]: "bin_pred(w BIT True) = w BIT False"
```
```   135 by (simp add: Bin_simps)
```
```   136
```
```   137 lemma bin_pred_0 [simp]: "bin_pred(w BIT False) = (bin_pred w) BIT True"
```
```   138 by (simp add: Bin_simps diff_minus add_ac)
```
```   139
```
```   140 lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
```
```   141 by (simp add: Bin_simps)
```
```   142
```
```   143 lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT True"
```
```   144 by (simp add: Bin_simps)
```
```   145
```
```   146 lemma bin_minus_1 [simp]:
```
```   147      "bin_minus (w BIT True) = bin_pred (bin_minus w) BIT True"
```
```   148 by (simp add: Bin_simps add_ac diff_minus)
```
```   149
```
```   150  lemma bin_minus_0 [simp]: "bin_minus(w BIT False) = (bin_minus w) BIT False"
```
```   151 by (simp add: Bin_simps)
```
```   152
```
```   153
```
```   154 subsection{*Binary Addition and Multiplication:
```
```   155          @{term bin_add} and @{term bin_mult}*}
```
```   156
```
```   157 lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
```
```   158 by (simp add: Bin_simps)
```
```   159
```
```   160 lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
```
```   161 by (simp add: Bin_simps diff_minus add_ac)
```
```   162
```
```   163 lemma bin_add_BIT_11 [simp]:
```
```   164      "bin_add (v BIT True) (w BIT True) = bin_add v (bin_succ w) BIT False"
```
```   165 by (simp add: Bin_simps add_ac)
```
```   166
```
```   167 lemma bin_add_BIT_10 [simp]:
```
```   168      "bin_add (v BIT True) (w BIT False) = (bin_add v w) BIT True"
```
```   169 by (simp add: Bin_simps add_ac)
```
```   170
```
```   171 lemma bin_add_BIT_0 [simp]:
```
```   172      "bin_add (v BIT False) (w BIT y) = bin_add v w BIT y"
```
```   173 by (simp add: Bin_simps add_ac)
```
```   174
```
```   175 lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
```
```   176 by (simp add: Bin_simps)
```
```   177
```
```   178 lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
```
```   179 by (simp add: Bin_simps diff_minus)
```
```   180
```
```   181 lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
```
```   182 by (simp add: Bin_simps)
```
```   183
```
```   184 lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
```
```   185 by (simp add: Bin_simps)
```
```   186
```
```   187 lemma bin_mult_1 [simp]:
```
```   188      "bin_mult (v BIT True) w = bin_add ((bin_mult v w) BIT False) w"
```
```   189 by (simp add: Bin_simps add_ac left_distrib)
```
```   190
```
```   191 lemma bin_mult_0 [simp]: "bin_mult (v BIT False) w = (bin_mult v w) BIT False"
```
```   192 by (simp add: Bin_simps left_distrib)
```
```   193
```
```   194
```
```   195
```
```   196 subsection{*Converting Numerals to Rings: @{term number_of}*}
```
```   197
```
```   198 axclass number_ring \<subseteq> number, comm_ring_1
```
```   199   number_of_eq: "number_of w = of_int (Rep_Bin w)"
```
```   200
```
```   201 lemma number_of_succ:
```
```   202      "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
```
```   203 by (simp add: number_of_eq Bin_simps)
```
```   204
```
```   205 lemma number_of_pred:
```
```   206      "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
```
```   207 by (simp add: number_of_eq Bin_simps)
```
```   208
```
```   209 lemma number_of_minus:
```
```   210      "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
```
```   211 by (simp add: number_of_eq Bin_simps)
```
```   212
```
```   213 lemma number_of_add:
```
```   214      "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
```
```   215 by (simp add: number_of_eq Bin_simps)
```
```   216
```
```   217 lemma number_of_mult:
```
```   218      "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
```
```   219 by (simp add: number_of_eq Bin_simps)
```
```   220
```
```   221 text{*The correctness of shifting.  But it doesn't seem to give a measurable
```
```   222   speed-up.*}
```
```   223 lemma double_number_of_BIT:
```
```   224      "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
```
```   225 by (simp add: number_of_eq Bin_simps left_distrib)
```
```   226
```
```   227 text{*Converting numerals 0 and 1 to their abstract versions*}
```
```   228 lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
```
```   229 by (simp add: number_of_eq Bin_simps)
```
```   230
```
```   231 lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
```
```   232 by (simp add: number_of_eq Bin_simps)
```
```   233
```
```   234 text{*Special-case simplification for small constants*}
```
```   235
```
```   236 text{*Unary minus for the abstract constant 1. Cannot be inserted
```
```   237   as a simprule until later: it is @{text number_of_Min} re-oriented!*}
```
```   238 lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
```
```   239 by (simp add: number_of_eq Bin_simps)
```
```   240
```
```   241
```
```   242 lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
```
```   243 by (simp add: numeral_m1_eq_minus_1)
```
```   244
```
```   245 lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
```
```   246 by (simp add: numeral_m1_eq_minus_1)
```
```   247
```
```   248 (*Negation of a coefficient*)
```
```   249 lemma minus_number_of_mult [simp]:
```
```   250      "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
```
```   251 by (simp add: number_of_minus)
```
```   252
```
```   253 text{*Subtraction*}
```
```   254 lemma diff_number_of_eq:
```
```   255      "number_of v - number_of w =
```
```   256       (number_of(bin_add v (bin_minus w))::'a::number_ring)"
```
```   257 by (simp add: diff_minus number_of_add number_of_minus)
```
```   258
```
```   259
```
```   260 lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
```
```   261 by (simp add: number_of_eq Bin_simps)
```
```   262
```
```   263 lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
```
```   264 by (simp add: number_of_eq Bin_simps)
```
```   265
```
```   266 lemma number_of_BIT:
```
```   267      "number_of(w BIT x) = (if x then 1 else (0::'a::number_ring)) +
```
```   268 	                   (number_of w) + (number_of w)"
```
```   269 by (simp add: number_of_eq Bin_simps)
```
```   270
```
```   271
```
```   272
```
```   273 subsection{*Equality of Binary Numbers*}
```
```   274
```
```   275 text{*First version by Norbert Voelker*}
```
```   276
```
```   277 lemma eq_number_of_eq:
```
```   278   "((number_of x::'a::number_ring) = number_of y) =
```
```   279    iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
```
```   280 by (simp add: iszero_def compare_rls number_of_add number_of_minus)
```
```   281
```
```   282 lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
```
```   283 by (simp add: iszero_def numeral_0_eq_0)
```
```   284
```
```   285 lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
```
```   286 by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
```
```   287
```
```   288
```
```   289 subsection{*Comparisons, for Ordered Rings*}
```
```   290
```
```   291 lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
```
```   292 proof -
```
```   293   have "a + a = (1+1)*a" by (simp add: left_distrib)
```
```   294   with zero_less_two [where 'a = 'a]
```
```   295   show ?thesis by force
```
```   296 qed
```
```   297
```
```   298 lemma le_imp_0_less:
```
```   299   assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
```
```   300 proof -
```
```   301   have "0 \<le> z" .
```
```   302   also have "... < z + 1" by (rule less_add_one)
```
```   303   also have "... = 1 + z" by (simp add: add_ac)
```
```   304   finally show "0 < 1 + z" .
```
```   305 qed
```
```   306
```
```   307 lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
```
```   308 proof (cases z rule: int_cases)
```
```   309   case (nonneg n)
```
```   310   have le: "0 \<le> z+z" by (simp add: nonneg add_increasing)
```
```   311   thus ?thesis using  le_imp_0_less [OF le]
```
```   312     by (auto simp add: add_assoc)
```
```   313 next
```
```   314   case (neg n)
```
```   315   show ?thesis
```
```   316   proof
```
```   317     assume eq: "1 + z + z = 0"
```
```   318     have "0 < 1 + (int n + int n)"
```
```   319       by (simp add: le_imp_0_less add_increasing)
```
```   320     also have "... = - (1 + z + z)"
```
```   321       by (simp add: neg add_assoc [symmetric])
```
```   322     also have "... = 0" by (simp add: eq)
```
```   323     finally have "0<0" ..
```
```   324     thus False by blast
```
```   325   qed
```
```   326 qed
```
```   327
```
```   328
```
```   329 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
```
```   330 lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
```
```   331 proof (unfold Ints_def)
```
```   332   assume "a \<in> range of_int"
```
```   333   then obtain z where a: "a = of_int z" ..
```
```   334   show ?thesis
```
```   335   proof
```
```   336     assume eq: "1 + a + a = 0"
```
```   337     hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
```
```   338     hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
```
```   339     with odd_nonzero show False by blast
```
```   340   qed
```
```   341 qed
```
```   342
```
```   343 lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
```
```   344 by (simp add: number_of_eq Ints_def)
```
```   345
```
```   346
```
```   347 lemma iszero_number_of_BIT:
```
```   348      "iszero (number_of (w BIT x)::'a) =
```
```   349       (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
```
```   350 by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff
```
```   351               Ints_odd_nonzero Ints_def)
```
```   352
```
```   353 lemma iszero_number_of_0:
```
```   354      "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) =
```
```   355       iszero (number_of w :: 'a)"
```
```   356 by (simp only: iszero_number_of_BIT simp_thms)
```
```   357
```
```   358 lemma iszero_number_of_1:
```
```   359      "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
```
```   360 by (simp only: iszero_number_of_BIT simp_thms)
```
```   361
```
```   362
```
```   363
```
```   364 subsection{*The Less-Than Relation*}
```
```   365
```
```   366 lemma less_number_of_eq_neg:
```
```   367     "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
```
```   368      = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
```
```   369 apply (subst less_iff_diff_less_0)
```
```   370 apply (simp add: neg_def diff_minus number_of_add number_of_minus)
```
```   371 done
```
```   372
```
```   373 text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
```
```   374   @{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
```
```   375 lemma not_neg_number_of_Pls:
```
```   376      "~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
```
```   377 by (simp add: neg_def numeral_0_eq_0)
```
```   378
```
```   379 lemma neg_number_of_Min:
```
```   380      "neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
```
```   381 by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
```
```   382
```
```   383 lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
```
```   384 proof -
```
```   385   have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
```
```   386   also have "... = (a < 0)"
```
```   387     by (simp add: mult_less_0_iff zero_less_two
```
```   388                   order_less_not_sym [OF zero_less_two])
```
```   389   finally show ?thesis .
```
```   390 qed
```
```   391
```
```   392 lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
```
```   393 proof (cases z rule: int_cases)
```
```   394   case (nonneg n)
```
```   395   thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
```
```   396                              le_imp_0_less [THEN order_less_imp_le])
```
```   397 next
```
```   398   case (neg n)
```
```   399   thus ?thesis by (simp del: int_Suc
```
```   400 			add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
```
```   401 qed
```
```   402
```
```   403 text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
```
```   404 lemma Ints_odd_less_0:
```
```   405      "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
```
```   406 proof (unfold Ints_def)
```
```   407   assume "a \<in> range of_int"
```
```   408   then obtain z where a: "a = of_int z" ..
```
```   409   hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
```
```   410     by (simp add: a)
```
```   411   also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
```
```   412   also have "... = (a < 0)" by (simp add: a)
```
```   413   finally show ?thesis .
```
```   414 qed
```
```   415
```
```   416 lemma neg_number_of_BIT:
```
```   417      "neg (number_of (w BIT x)::'a) =
```
```   418       neg (number_of w :: 'a::{ordered_idom,number_ring})"
```
```   419 by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
```
```   420               Ints_odd_less_0 Ints_def)
```
```   421
```
```   422
```
```   423 text{*Less-Than or Equals*}
```
```   424
```
```   425 text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
```
```   426 lemmas le_number_of_eq_not_less =
```
```   427        linorder_not_less [of "number_of w" "number_of v", symmetric,
```
```   428                           standard]
```
```   429
```
```   430 lemma le_number_of_eq:
```
```   431     "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
```
```   432      = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
```
```   433 by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
```
```   434
```
```   435
```
```   436 text{*Absolute value (@{term abs})*}
```
```   437
```
```   438 lemma abs_number_of:
```
```   439      "abs(number_of x::'a::{ordered_idom,number_ring}) =
```
```   440       (if number_of x < (0::'a) then -number_of x else number_of x)"
```
```   441 by (simp add: abs_if)
```
```   442
```
```   443
```
```   444 text{*Re-orientation of the equation nnn=x*}
```
```   445 lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
```
```   446 by auto
```
```   447
```
```   448
```
```   449
```
```   450
```
```   451 subsection{*Simplification of arithmetic operations on integer constants.*}
```
```   452
```
```   453 lemmas bin_arith_extra_simps =
```
```   454        number_of_add [symmetric]
```
```   455        number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
```
```   456        number_of_mult [symmetric]
```
```   457        diff_number_of_eq abs_number_of
```
```   458
```
```   459 text{*For making a minimal simpset, one must include these default simprules.
```
```   460   Also include @{text simp_thms} or at least @{term "(~False)=True"} *}
```
```   461 lemmas bin_arith_simps =
```
```   462        Pls_0_eq Min_1_eq
```
```   463        bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
```
```   464        bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
```
```   465        bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
```
```   466        bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
```
```   467        bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
```
```   468        bin_add_Pls_right bin_add_Min_right
```
```   469        abs_zero abs_one bin_arith_extra_simps
```
```   470
```
```   471 text{*Simplification of relational operations*}
```
```   472 lemmas bin_rel_simps =
```
```   473        eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
```
```   474        iszero_number_of_0 iszero_number_of_1
```
```   475        less_number_of_eq_neg
```
```   476        not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
```
```   477        neg_number_of_Min neg_number_of_BIT
```
```   478        le_number_of_eq
```
```   479
```
```   480 declare bin_arith_extra_simps [simp]
```
```   481 declare bin_rel_simps [simp]
```
```   482
```
```   483
```
```   484 subsection{*Simplification of arithmetic when nested to the right*}
```
```   485
```
```   486 lemma add_number_of_left [simp]:
```
```   487      "number_of v + (number_of w + z) =
```
```   488       (number_of(bin_add v w) + z::'a::number_ring)"
```
```   489 by (simp add: add_assoc [symmetric])
```
```   490
```
```   491 lemma mult_number_of_left [simp]:
```
```   492     "number_of v * (number_of w * z) =
```
```   493      (number_of(bin_mult v w) * z::'a::number_ring)"
```
```   494 by (simp add: mult_assoc [symmetric])
```
```   495
```
```   496 lemma add_number_of_diff1:
```
```   497     "number_of v + (number_of w - c) =
```
```   498      number_of(bin_add v w) - (c::'a::number_ring)"
```
```   499 by (simp add: diff_minus add_number_of_left)
```
```   500
```
```   501 lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
```
```   502      number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
```
```   503 apply (subst diff_number_of_eq [symmetric])
```
```   504 apply (simp only: compare_rls)
```
```   505 done
```
```   506
```
```   507 end
```