Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] problem with polymorphism?

Email Gateway (Aug 18 2022 at 10:23):

From: Christian Urban <urbanc@in.tum.de>
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

Last updated: May 03 2024 at 12:27 UTC