Email Gateway (Aug 22 2022 at 18:09): Email Gateway (Aug 22 2022 at 18:09):From: Jørgen Villadsen <jovi@dtu.dk>
Hi,
Attached file suggests the following Isar proof which does not parse in Isabelle2017 and Isabelle2018-RC3:
Isar proof (0.0 ms):
proof -
have "map e x3_ = map e' x3_"
using Pre by auto
then show ?thesis
using semantics.simps(1) by presburger
qed
It works with by smt.
Any thoughts?
Best regards, Jørgen
Problem.thy
Email Gateway (Aug 22 2022 at 18:10):From: Peter Lammich <lammich@in.tum.de>
Hi Jorgen
Unfortunately, this is a well-known problem: The Isar proof generator
seems not to be aware of internal variable names (ending with "_").
These cannot be parsed.
Solution: Explicitly give proper names to your variables, eg:
proof (induct p arbitrary: e e')
case (Pre x1 x2 x3) then show ?case using map_cong free.simps(1)
semantics.simps(1) sledgehammer
proof -
have "map e x3 = map e' x3"
using Pre.prems by force
then show ?thesis
using semantics.simps(1) by presburger
qed
Email Gateway (Aug 22 2022 at 18:12):From: Jørgen Villadsen <jovi@dtu.dk>
Thanks. A warning would have been helpful... :-)
Jørgen
Last updated: Nov 21 2024 at 12:39 UTC