[isabelle] problem with polymorphism?
This was already discussed on the Nominal-Isabelle
mailing list . One problem is that the goal
a#(::(name * name) list) ==> a#(::name list)
cannot be proved by assumption, because the empty-list
has different types in the premise and conclusion.
Randy Pollack writes:
> Consider the following example, which I'm running in version 0.08 of
> Nominal Isabelle.
> theory example
> imports Nominal
> atom_decl name
> types names = "(name * name) list"
> lemma fresh_cxt_list:
> fixes a::name and G::names
> assumes h:"a \<sharp> G"
> shows "a \<sharp> map fst G"
> using h
> proof (induct G, simp_all)
> case Nil
> 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