Re: [isabelle] Undefined facts in skip_proofs mode



Isn’t that as specified? The proofs are skipped, so Cons.hyps won’t be generated in the induct call.

Cheers,
Gerwin

On 28 Jul 2014, at 3:21 pm, Lars Hupel <hupel at in.tum.de> wrote:

> Hello,
>
> 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
> "~/tmp/Skip_Proof/Skip_Proof.thy")
> *** 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.
>
> Cheers
> Lars
> <skip_proofs.zip>


________________________________

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 MHonArc.