*To*: Bertram Felgenhauer <bertram.felgenhauer at googlemail.com>*Subject*: Re: [isabelle] Odd failure to match local statement with pending goal.*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 2 Aug 2011 14:55:07 -0700*Cc*: Lars Noschinski <noschinl at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20110802211001.GA2459@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>*References*: <20110727112106.GA2460@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f> <4E3165D3.9080306@in.tum.de> <20110802211001.GA2459@24f89f8c-e6a1-4e75-85ee-bb8a3743bb9f>*Sender*: huffman.brian.c at gmail.com

On Tue, Aug 2, 2011 at 2:10 PM, Bertram Felgenhauer <bertram.felgenhauer at googlemail.com> wrote: > Hi, > >> As Larry stated, this is indeed a strange problem. I tried to find a >> minimal example; here is what I came up with: >> >> ------------------- >> lemma >> shows "⋀c d. d ∈ Z ⟹ x = c ⟹ >> ∃e. e ∈ {_. ∃e. e ∈ Z ∧ y = e}" >> apply (unfold mem_Collect_eq) >> proof - >> fix s t >> assume "x = s" and "t ∈ Z" >> then show "∃s t. t ∈ Z ∧ y = t" >> sorry >> qed >> ------------------- >> The show statement fails with > [...] > > So do we know whether this is an obscure feature or possibly a bug? > (If it's a feature I'd love to hear the underlying story.) It certainly looks like a bug to me. I don't have an idea yet of why it happens, but I found an even smaller example. I constrained everything to type "nat" just to rule out any weirdness with polymorphism. Note the repeated bound variable name in the goal (the argument to Q is the second "c", which pretty-prints as "ca"). This seems to be necessary to make the error happen. lemma shows "⋀(a::nat) (b::nat). P a b ⟹ ∀(c::nat) (c::nat). Q c" proof - fix s t :: nat assume "P s t" thus "∀(s::nat) (t::nat). Q t" (* Local statement will fail to refine... *) Swapping the order of the bound variable names in the conclusion also gives the same error: thus "∀(t::nat) (s::nat). Q s" Just about any other modification to the lemma or proof that I could think of seems to make it work again. - Brian

**References**:**Re: [isabelle] Odd failure to match local statement with pending goal.***From:*Bertram Felgenhauer

- Previous by Date: Re: [isabelle] Odd failure to match local statement with pending goal.
- Next by Date: [isabelle] Get an ML value from a theory context
- Previous by Thread: Re: [isabelle] Odd failure to match local statement with pending goal.
- Next by Thread: Re: [isabelle] Odd failure to match local statement with pending goal.
- Cl-isabelle-users August 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list