Re: [isabelle] Automatic derivation of specialised theorems
On Tue, 18 Feb 2014, Manuel Eberl wrote:
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
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
interpretation nat!: foo "op *" "op div" "op mod" "id :: nat => nat"
where "!!x :: nat. x div id x == x" sorry
I've found this approach by Andreas quite nice. What is wrong about
putting your original theorems into a locale?
Without any further context of the actual application, it is hard to tell
what you actually need, in contrast to what you think you want.
This archive was generated by a fusion of
Pipermail (Mailman edition) and