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

Not quite. I also need it for int. I thought about using locales, but that would require me to also put the original theorems into a locale of their own; I'm not sure whether I want that. Also, in regard to what Peter said: I'm not really looking for a solution within the high level stuff of Isabelle, I was thinking of a solution in Isabelle/ML. My main problem is finding all the theorems that contain an occurrence of some pattern; if I knew how to do that, I could probably manage the rest myself with what little knowledge I have of Isabelle/ML. Cheers, Manuel On 02/18/2014 05:45 PM, Andreas Lochbihler wrote: > Hi Manuel, > > From your name "_nat", I guess that you just need this transformation > for natural numbers, so you can exploit the rewriting morphism of > interpretation. If you state more equations there, you get more > simplification. This also allows you to register the facts under the > same name with a prefix such as "nat.". Suffixes are not supported. > Here's a silly example. > > 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:*Makarius

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

**Re: [isabelle] Automatic derivation of specialised theorems***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Quickcheck-Narrowing
- Next by Date: [isabelle] “Programming in Isabelle/HOL”
- 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