[isabelle] Converting fixed variables to ?-wildcards



Assume I have some lemma in a locale

locale test = fixes A::"'a list set"
assumes [...]
begin
 [...]

 lemma test[simp]: "a at b\<in>A <--> a\<in>A & b\<in>A"

in order to apply this lemma also to lists of the form "a#as", outside a locale, I would usually do
 lemmas test'[simp] = test[of "[x]", simplified, standard]

the problem is, that standard does not only convert the fixed variable x to a wildcard variable ?x, but it also prefixes the lemma with an assumption "test A", because we are inside the locale. Instead of the desired
 "?x#?b\<in>A <--> [?x]\<in>A & b\<in>A",
I get
 "test A ==> ?x#?b\<in>A <--> [?x]\<in>A & b\<in>A"
and this lemma won't work as a simplification rule inside the locale context.

Is there a way to the fixed variables replaced by wildcards, but not getting this locale-assumption in front of the lemma (of course, without retyping and proving the special version of the lemma ;) ) ?

Regards,
 Peter






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