Re: [isabelle] Evaluation of record expressions



Dear Michael,

Am 14.10.2013 um 15:01 schrieb Michael Vu <michael.vu at rwth-aachen.de>:

> Is there nobody with a clue? 

No, we are all clueless. ;)

I presume you refer to the first question you posted some time ago. First of all, the theory snippet you pasted into your email cannot be parsed back by Isabelle (importing "Complex_Complex"). The parser chokes on "⊩". That makes it harder for us to help you.

Second, there is no silver bullet in Isabelle that will prove finite goals. (I'm taking your claim at face value; being unable to parse the formula you sent, I cannot infer the types and check finiteness.) The closest thing to it is Nitpick, but you would have to trust it as an oracle. See e.g. my paper [1] for an instance where we used Nitpick for exhaustive verification.

I presume that a properly set up "blast" or "auto" might be able to finish the job. Sometimes it's just a matter of adding a few intro, elim, or split rules; perhaps one of the experts could help you, once they are given a self-contained example.

Regards,

Jasmin

[1] http://www21.in.tum.de/~blanchet/ppdp2011-cpp-mem.pdf





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