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