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.