*To*: Manuel Eberl <eberlm at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Automatic derivation of specialised theorems*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 18 Feb 2014 17:45:57 +0100*In-reply-to*: <5303710B.3000500@in.tum.de>*References*: <5303710B.3000500@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Hi Manuel,

class foo = div + fixes foo :: "'a => 'a" begin lemma foo: "x div foo x = y" sorry end interpretation nat!: foo "op *" "op div" "op mod" "id :: nat => nat" where "!!x :: nat. x div id x == x" sorry thm nat.foo Best, Andreas On 18/02/14 15:41, Manuel Eberl wrote:

Hallo, I currently have the following situation: I have a number of theorems in some typeclass that contain terms such as “x div foo x” (where foo is a function constant and x is a free variable) For particular instantiations of this typeclass, “x div foo x” often has a much easier form. Say, for instance, I have a theorem “(?x::nat) div foo ?x = ?x” I would therefore like to do the following for any theorem that contains “?x div foo ?x” as a subterm: 1. replace every occurrence of “x div foo x” in the theorem with “?x” (i.e. just replace lhs of equation with rhs everywhere) 2. perform some simplification, possibly with a restricted simpset 3. register the new theorem under the name of the old one, plus the suffix “_nat” Are there any existing mechanisms for something like this? If not, how should I proceed? For instance, how do I get a list of all theorems containing such a pattern? (All of this will be done only in the theory where the type class instance was first derived, so this is a very “local” operation, the number of theorems affected is not very large) Cheers, Manuel

**Follow-Ups**:**Re: [isabelle] Automatic derivation of specialised theorems***From:*Manuel Eberl

**References**:**[isabelle] Automatic derivation of specialised theorems***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Automatic derivation of specialised theorems
- Next by Date: Re: [isabelle] Quickcheck-Narrowing
- Previous by Thread: Re: [isabelle] Automatic derivation of specialised theorems
- Next by Thread: Re: [isabelle] Automatic derivation of specialised theorems
- Cl-isabelle-users February 2014 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