Re: [isabelle] Automatic derivation of specialised theorems

Point taken.

The context is the following, modified GCD theory, in particular the
lemmas in euclidean_semiring_gcd:

The problem is that the general theorems in euclidean_semiring_gcd
contain statements such as "is_unit x", "associated x y",
"normalisation_factor x", "euclidean_size x". However:

- for nat, these simplify to "x = 1", "x = y", "1", and "x", respectively
- For int, they simplify to "abs x = 1", "abs x = abs y", "sgn x", and
"abs x", respectively
- for 'a poly, they simplify to "x ? 0 ? degree x = 0", "associated x
y", "coeff (degree x) x", and "degree x", respectively

Also, expressions such as "x div normalisation_factor x" simplify
accordingly to "x" for nat and "abs x" for int.

Of course, one would like to have a general theorem stating that "gcd
(x::'a::euclidean_semiring) 0 = x div normalisation_factor x", but also
specialised ones saying "gcd (x::nat) 0 = x" and "gcd (x::int) 0 = abs x".

I think locales can do most of those (although I'm not quite sure how to
set it up exactly), but some things, but some things, such as
automatically discarding trivial assumptions like "normalisation_factor
x = 1" for x :: nat are, to my knowledge, not possible with locales.


On 28/02/14 13:58, Makarius wrote:
> 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
> 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.