Re: [isabelle] Undefined facts in skip_proofs mode
The skip-proof semantics are confusing though.
When processing a theorem, skip_proofs takes a theorem ending with "oops" as a valid theorem, and so if you have two versions
of a lemma in a single file, one that has been oopsed, and one later with the same name which is "done", then the second one fails
to be processed, which is unfortunate.
On 28 Jul 2014, at 11:39 pm, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
> Isn’t that as specified? The proofs are skipped, so Cons.hyps won’t be generated in the induct call.
> On 28 Jul 2014, at 3:21 pm, Lars Hupel <hupel at in.tum.de> wrote:
>> Cornelius and I noticed an oddity when using the system option
>> "skip_proofs". Consider this simple proof:
>> lemma "(xs::'a list) = xs"
>> proof (induct xs)
>> case Cons
>> thm Cons.hyps
>> from Cons show ?case by auto
>> qed auto
>> Notice the "thm" command in the middle. Without "skip_proofs", this goes
>> through fine. Enabling "skip_proofs" produces this message:
>> *** Undefined fact: "Cons.hyps" (line 8 of
>> *** At command "thm" (line 8 of "~/tmp/Skip_Proof/Skip_Proof.thy")
>> I have attached a session demonstrating the difference. Run with
>> $ isabelle build -d . -v Skip_Proof
>> Reproducible in all official releases since 2013-2.
> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
This archive was generated by a fusion of
Pipermail (Mailman edition) and