Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int



On 2/13/2014 9:14 AM, Ondřej Kunčar wrote:
The problem is addressed in 6ea67a791108.

To work with the repository, I was thinking I'd have to do something complex, but then I just downloaded the 2 changeset files and built the image. Also, thanks for the heads up on `minus` causing problems. That may not be applicable here, but I'm sure it'll come up in the future.

Dude expressions are applicable, and possibly Fabian Cancellera analogies, or maybe not, as I tend to confuse Czechoslovakia with the Swiss domain .ch, but we can say that the power of the lifting package can be compared to the size of André Greipel's thighs. As to the speed with which I instantiated my type as `linordered_semidom`, we can say that is comparable to the speed of Marcel Kittel.

There actually would have been a big snag, except for a recent tip by Andreas Lochbihler, to not use ==> in a structured proof, but to use `assume`. A proof goal was going all crazy when I would prove the step using ==>.

The numeral type class is also important, by Florain Haftmann and Brian Huffman. I haven't figured it out yet, but I know not to let my simp rules interfere with letting it do its job.

Having a set of constants for a number system is a big reason why one traditionally has to resort to using integers, rational numbers, and real numbers. It's rather radical to have a set of constants, the numerals, that are both abstract, due to polymorphism, but yet can be used concretely. If I never have to use the real numbers or rational numbers, because I can figure out how to get by with the numerals, that'll be fine with me.

Regards,
GB
















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