Many thanks for your analysis. It looks like an interaction involving "fix" and bound variables.
But we need to move the discussion to [email protected]. Larry On 2 Aug 2011, at 22:55, Brian Huffman wrote: > On Tue, Aug 2, 2011 at 2:10 PM, Bertram Felgenhauer > <[email protected]> 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 > _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
