*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Converting fixed variables to ?-wildcards*From*: Makarius <makarius at sketis.net>*Date*: Thu, 12 Jun 2008 22:24:11 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20080612115415.6b08kzyb6w4ckoc4@webmail.pdx.edu>*References*: <484FF0DD.3090700@uni-muenster.de> <48507CBA.1070603@rsise.anu.edu.au> <20080612115415.6b08kzyb6w4ckoc4@webmail.pdx.edu>

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

**References**:**[isabelle] Converting fixed variables to ?-wildcards***From:*Peter Lammich

**Re: [isabelle] Converting fixed variables to ?-wildcards***From:*Jeremy Dawson

**Re: [isabelle] Converting fixed variables to ?-wildcards***From:*Brian Huffman

- Previous by Date: [isabelle] AMAST'08 Call for Participation
- Next by Date: Re: [isabelle] Defining finite list functions recursively
- Previous by Thread: Re: [isabelle] Converting fixed variables to ?-wildcards
- Next by Thread: [isabelle] Defining finite list functions recursively
- Cl-isabelle-users June 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list