Discussion:
[isabelle] Eisbach: fold and named_theorems
(too old to reply)
Andreas Lochbihler
2016-08-11 07:06:33 UTC
Permalink
Raw Message
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
Andreas Lochbihler
2016-08-11 07:14:57 UTC
Permalink
Raw Message
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
Did you try “unfold relator_eq[symmetric]”? I don’t know how fold is implemented, so it may actually do this under the covers.
Post by Andreas Lochbihler
Dear Eisbach gurus,
method transfer_prover' = (fold relator_eq; transfer_prover)
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
Loading...