[isabelle] Converting fixed variables to ?-wildcards
Assume I have some lemma in a locale
locale test = fixes A::"'a list set"
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
"?x#?b\<in>A <--> [?x]\<in>A & b\<in>A",
"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
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 ;) ) ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and