Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Self-container simproc for word numeral normal...

view this post on Zulip Email Gateway (Apr 22 2025 at 17:36):

From: Florian Haftmann <florian.haftmann@cit.tum.de>
See now
https://foss.heptapod.net/isa-afp/afp-devel/-/commit/fc1ef1c2cc6701b9e9d24304867366b4041f3f2d
for an attempt of a self-contained simproc.

Florian

Am 15.04.25 um 09:53 schrieb Florian Haftmann:

Hi Ike,

thanks for figuring that out.

As far I can see, the best solution is to disregard
word_eq_numeral_iff_iszero [simp] and calculate equality on word values
in the same manner as <= and < is calculated by default in HOL-
Library.Word.

@list Any objections?

* Swap out word_eq_numeral_iff_iszero for word_unat_eq_iff[where ?     v=‹numeral _› and ?w=‹numeral _›]. This avoids the subtraction – it
    normalizes the words, then compares them as naturals.

I have also tried to modify the simpset used by unsigned_word to a
completely determined one. This speeds up the normalization procedure
itself about 3x, but is still very slow in conjunction with word_eq_numeral_iff_iszero. For reference, I ended up with something
like val ss = simpset_of (put_simpset HOL_ss @{context} addsimps @{thms bintrunc_numeral len_bit0 len_num1 One_nat_def mult_Suc_right mult_0_right add.right_neutral mult_num_simps numeral_times_numeral pred_numeral_simps bin_last_numeral_simps of_bool_eq Num.BitM.simps numeral_div_numeral divmod_cancel divmod_trivial prod.case prod.sel div_0 take_bit_0 times_int_code mult_1_right add.left_neutral one_plus_numeral add_num_simps minus_numeral_div_numeral minus_one_div_numeral Parity.adjust_div_eq odd_neg_numeral1 numeral_One one_neq_zero bintrunc_Suc_numeral of_int_numeral}).

By »completely determined« you mean static, with no effect of later simp
declarations? This would indeed by interesting to be included by default.

@list Opinions?

Cheers,
    Florian

OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc

Last updated: May 06 2025 at 08:28 UTC