*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Automatic derivation of specialised theorems*From*: Makarius <makarius at sketis.net>*Date*: Fri, 28 Feb 2014 13:58:26 +0100 (CET)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <530395FA.1070803@in.tum.de>*References*: <5303710B.3000500@in.tum.de> <53038E45.5060805@inf.ethz.ch> <530395FA.1070803@in.tum.de>*User-agent*: Alpine 2.11 (LSU 23 2013-08-11)

On Tue, 18 Feb 2014, Manuel Eberl wrote:

Not quite. I also need it for int. I thought about using locales, butthat would require me to also put the original theorems into a locale oftheir own; I'm not sure whether I want that.Also, in regard to what Peter said: I'm not really looking for asolution within the high level stuff of Isabelle, I was thinking of asolution in Isabelle/ML. My main problem is finding all the theoremsthat contain an occurrence of some pattern; if I knew how to do that, Icould probably manage the rest myself with what little knowledge I haveof Isabelle/ML.On 02/18/2014 05:45 PM, Andreas Lochbihler wrote: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

Makarius

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

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

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

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

- Previous by Date: [isabelle] CICM 2014: Extended Deadline March 14th, 2014
- Next by Date: Re: [isabelle] Automatic derivation of specialised theorems
- 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