Re: [isabelle] Automatic derivation of specialised theorems



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
>>
>





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