# Re: [isabelle] Converting fixed variables to ?-wildcards

Quoting Jeremy Dawson <jeremy at rsise.anu.edu.au>:

Peter Lammich wrote:

`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

Peter,
I've never tried doing this inside a locale, but, to turn free
variables into ?-variables,
without doing the other stuff that standard does, I have used
(gen_all o forall_intr_frees), thus
val mp' = "[| P --> Q; P |] ==> Q" : Thm.thm

(gen_all o forall_intr_frees) mp';

val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : Thm.thm
Jeremy

`If you want to use this from Isar, it is actually pretty easy to
``define your own theorem attributes, given a function of type thm -> thm:
`
setup {*
Attrib.add_attributes
[("wildcard",
Attrib.no_args (Thm.rule_attribute (K (gen_all o forall_intr_frees))),
"replace fixed variables by wildcards")];
*}
You can use it like this:
thm mp [of R S]

"[| R --> S; R |] ==> S"

thm mp [of R S, wildcard]

"[| ?R --> ?S; ?R |] ==> ?S"

thm mp [of "x = y", wildcard]

"[| ?x2 = ?y2 --> ?Q; ?x2 = ?y2 |] ==> ?Q"

`The "standard" attribute is defined very similarly to this; the code
``is in Pure/Isar/attrib.ML:
`
val standard = no_args (Thm.rule_attribute (K Drule.standard));
It refers to the function Drule.standard from Pure/drule.ML:
val standard' =
implies_intr_hyps
#> forall_intr_frees
#> `Thm.maxidx_of
#-> (fn maxidx =>
Thm.forall_elim_vars (maxidx + 1)
#> Thm.strip_shyps
#> zero_var_indexes
#> Thm.varifyT);
val standard =
flexflex_unique
#> standard'
#> Thm.close_derivation;

`As you can see, the "standard" attribute does quite a few things. One
``other feature of "standard" you might want to add to "wildcard" would
``be to zero the variable indexes, to avoid the problem with the third
``example above.
`
- Brian

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