Re: [isabelle] Evaluation of record expressions

Dear Jasmin, 

Indeed, that was my fault. I work with custom theories where this symbol is treated as "<" (less relation) and I forgot to replace it. Hope you could somehow help me now. My goal is just to make isabelle split all possible cases as they are finite and then solve every case for itself. Thanks! 


Jasmin Blanchette <jasmin.blanchette at> schrieb:
>Dear Michael,
>Am 14.10.2013 um 15:01 schrieb Michael Vu < at>:
>> 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.

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