[isabelle] problem with polymorphism?
Consider the following example, which I'm running in version 0.08 of
types names = "(name * name) list"
fixes a::name and G::names
assumes h:"a \<sharp> G"
shows "a \<sharp> map fst G"
proof (induct G, simp_all)
hence "a \<sharp> (::names)" by simp
This is accepted. The goal is
[| a \<sharp> ; a \<sharp> G |] ==> a \<sharp> 
Even though I have "show sorts" on,  is not shown with a type, but
we know that  in the hyps can be given type "::names" because the
line "hence ..." is accepted. However, this goal is not solved by
simp or auto, and in fact Isabelle refuses to give type "names" to 
in the conclusion, even though it came from induction over an
explicitely typed object, G. E.g.
thus "a \<sharp> (::names)"
is not accepted:
*** Local statement will fail to solve any pending goal
*** Failed attempt to solve goal by exported rule:
*** ((a \<sharp> ) ==> a \<sharp> 
*** At command "thus".
How can I do this proof?
This archive was generated by a fusion of
Pipermail (Mailman edition) and