Re: [isabelle] Eisbach: fold and named_theorems



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


On 11/08/16 09:03, Peter Gammie wrote:
Did you try âunfold relator_eq[symmetric]â? I donât know how fold is implemented, so it may actually do this under the covers.

On 11 Aug 2016, at 16:59, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:

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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.