[isabelle] problem with polymorphism?



Consider the following example, which I'm running in version 0.08 of
Nominal Isabelle.

  theory example
  imports Nominal
  begin

  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?

Best,
Randy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.