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 [...]
> 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]

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])


	Makarius





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