[isabelle] problem with polymorphism?



This was already discussed on the Nominal-Isabelle
mailing list [1]. 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. 

Christian

[1] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/nominal-isabelle

Randy Pollack writes:
 > 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.