Email Gateway (Aug 22 2022 at 13:58): Email Gateway (Aug 22 2022 at 13:58):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Eisbach gurus,
I'd like to define a method the following method using Eisbach:
method transfer_prover' = (fold relator_eq; transfer_prover)
Unfortunately, I get an exception at the method declaration time (both with Isabelle2016
and 1e7c5bbea36d):
exception THM 0 raised (line 884 of "thm.ML"):
symmetric
TERM _
The problem seems to be the named_theorems "relator_eq" which I am passing to the method
"fold", as the following minimal testcase shows
method bar = (fold One_nat_def) (* works *)
named_theorems test
declare One_nat_def[test]
method foo = (fold test) (* fails *)
Why can't I use "fold" with named_theorems in Eisbach method definitions?
Best,
Andreas
Email Gateway (Aug 22 2022 at 13:58):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Peter,
Indeed, "unfold relator_eq[symmetric]" works in the method definition, but "fold
relator_eq" does not. Weird. I always considered fold and unfold to be the same up to the
orientation of the equation.
Thanks,
Andreas
Last updated: Apr 25 2024 at 20:15 UTC