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

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.


	Makarius




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