*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Automatic derivation of specialised theorems*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 28 Feb 2014 15:49:22 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <alpine.LSU.2.11.1402281356180.30878@macbroy20.informatik.tu-muenchen.de>*References*: <5303710B.3000500@in.tum.de> <53038E45.5060805@inf.ethz.ch> <530395FA.1070803@in.tum.de> <alpine.LSU.2.11.1402281356180.30878@macbroy20.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Point taken. The context is the following, modified GCD theory, in particular the lemmas in euclidean_semiring_gcd: http://shodan.linuxd.org/paste/Fl46bj4E 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. Cheers, Manuel 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 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

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

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

- Previous by Date: Re: [isabelle] Automatic derivation of specialised theorems
- Next by Date: Re: [isabelle] Code-equations for multisets
- Previous by Thread: Re: [isabelle] Automatic derivation of specialised theorems
- Next by Thread: [isabelle] “Programming in Isabelle/HOL”
- 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