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



On Thu, 12 Jun 2008, Brian Huffman wrote:

> Quoting Jeremy Dawson <jeremy at rsise.anu.edu.au>:
> 
> >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
> 
> 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")];
> *}

Note that anything modeled after the old "standard" only works in a global 
context.  In fact, fixed variables cannot be generalized without leaving 
the context, which is not allowed an attribute anyway.  So strictly 
speaking, the "standard" attribute is a legacy feature, despite its rather 
misleading name.


Going back to the original motivation, the demand for generalizing 
variables was coming from fact declarations like this:

lemmas a = b [of x]

Here x is an undeclared free variable, and there is no official way to 
ever get rid of it.  What you actually want is to say that x should be 
fixed in the context of the statement, such that it becomes arbitrary in 
the result.  I.e. something analogous to

lemma a: fixes x shows B x ...

or

lemma a: shows B x ...

where the fixing is implicit.

Neither form is available for compact fact expressions, without an 
explicit statement.  There are some plans for a more uniform way to put 
arbitrary statements (definitions and theorems) into a auxiliary context, 
with local fixes and assumes just like the special form for long theorem 
statements.  At the moment we are still very busy to struggle with 
old-style global operations showing up in unexpected corners ...


	Makarius





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