Re: [isabelle] Converting fixed variables to ?-wildcards
On Wed, 11 Jun 2008, Peter Lammich wrote:
> Assume I have some lemma in a locale
> locale test = fixes A::"'a list set"
> assumes [...]
> 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]
Such forward inferences via "simplified" and "standard" as part of fact
declarations do not work well within general local theory targets. You
have already encountered the inherent global nature of "standard". The
"simplified" rule has other potential problems, when transforming locale
results by interpretation, or even just when re-entering the locale
context in a different theory, because the simplification process is
repeated within different dynamic contexts each time!
> 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 ;) ) ?
I am not aware of any sane way, apart from the canonical one:
lemma test': "x # b : A <-> [x] : A & b : A"
by (rule test [of "[x]", simplified])
This archive was generated by a fusion of
Pipermail (Mailman edition) and