Email Gateway (Aug 22 2022 at 16:29): Email Gateway (Aug 22 2022 at 16:29):From: Makarius <makarius@sketis.net>
OK. I am definitely interested in more details. Even Windows deserves a
fully working Isabelle setup.
Concerning the original subject: Florian Haftmann has applied the
following change already:
http://isabelle.in.tum.de/repos/isabelle/rev/f37bf261bdf6
Makarius
Email Gateway (Aug 22 2022 at 16:33):From: Thomas.Sewell@data61.csiro.au
Hello isabelle-users.
I've noticed that there are a couple of proofs which use the smt method
in the HOL-Word theories now. Actually a colleague noticed this, because
there's some kind of compatibility problem with z3 on his machine, and
so HOL-Word isn't building.
My understanding was that smt was to be avoided for proofs committed to
HOL, HOL-Library etc so that users do not strictly require the SMT
solvers to operate correctly. Has that policy changed, or was this an
oversight?
Specifically, the two instances were introduced by c32926df and look like:
isabelle/src/HOL/Word/Misc_Numeric.thy: by (smt mod_pos_pos_trivial
zero_less_power)
isabelle/src/HOL/Word/Bit_Representation.thy: apply (smt pos_zmod_mult_2
zle2p)
For reference, these proofs can be done differently like this:
lemma one_mod_exp_eq_one [simp]: "1 mod (2 * 2 ^ n) = (1::int)"
using power_strict_increasing[where a="2 :: int" and n=0 and N="Suc n"]
by (simp add: mod_pos_pos_trivial)
lemma sbintrunc_mod2p: "sbintrunc n w = (w + 2 ^ n) mod 2 ^ (Suc n) - 2 ^ n"
apply (induct n arbitrary: w)
apply (auto simp add: bin_last_odd bin_rest_def Bit_def emep1[symmetric]
mult_mod_right
elim!: evenE oddE intro: arg_cong2[where f="op mod"])
done
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 16:33):From: Makarius <makarius@sketis.net>
Can you elaborate on this? The ambition is that all bundled Isabelle
tools work everywhere under all circumstances. To improve the
approximation of that limit point, we need concrete problem reports.
Makarius
Last updated: Apr 19 2024 at 01:05 UTC