# 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 {*
[("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.