Email Gateway (May 20 2022 at 19:59): Email Gateway (May 20 2022 at 19:59):From: Thomas Sewell <tals4@cam.ac.uk>
I've had a quick look. It does look like the goals are actually the same, apart from the fact that some variables are "orange" (i.e. fixed in Isar proof steps) in the failed version whereas they're "blue" (i.e. fixed at the lemma statement) in the other.
The good news is, "auto" in the successful proof can be replaced by "simp" followed by "clarify" followed by "simp", with the final simp doing the important work. The simplifier trace can be activated with using [[simp_trace]]. If you then copy the traces from the successful and failed attempts into other files, you can diff them, and see that roughly halfway through the successful proof the simplifier applies a rule called ECMP.fitEnvPar, whereas in the failed attempt the system applied an anonymous rule about "trans (_ || _)".
I don't really know what's going on. There is a difference between "blue" and "orange" variables internally, which might have an impact on term ordering, which the simplifier uses for some things. It's possible this leads to a different outcome in a situation where it has two rules and either of them can apply.
Maybe if you look at the simp traces, you can figure out what's happened. Sometimes you need to control the simplifier when it has a choice, e.g. by temporarily deleting some rules.
Good luck,
Thomas.
Email Gateway (May 20 2022 at 19:59):From: Peter Lammich <lammich@in.tum.de>
if your thy does not run with the current Isabelle version, you should
at least mention the Isabelle version you are using ... otherwise, no
one will be able/willing to reproduce your examples.
Are you sure the goal is actually the same, including types and sorts?
Peter
Email Gateway (May 20 2022 at 21:00):From: Li Yongjian <lyj238@gmail.com>
Dear experts:
In the attached German.thy file,
in lines 2163, 2173, and 2299, before Isabelle executes the proof command,
the proof goal is the same:
formEval (pre r) sk ⟹
fitEnv sk (env N) ⟹
r ∈ RecvReqE_refs N ⟹ fitEnv (trans1 (act r) sk) (env N),
we execute the same proof command: apply (unfold RecvReqE_refs_def
RecvReqE_ref_def,auto ).
For lines 2163, and 2173, the goal is solved, but for the last line, the
goal cann't be solved.
Why are there differences in the three executions.
regards
lyj
German.thy
ECMP.thy
Last updated: Jul 15 2022 at 23:21 UTC