When I try it in HOL Light on my machine it takes about 0.074 seconds,
which is around 250 million CPU cycles according to the clock speed
from "lscpu". This is the same order of magnitude that Dan was seeing.
On the whole, the procedures like INT_ARITH are mostly fast enough for
everyday
Hi Dan,
| Newbie question: In HOL Light (or in another variant of HOL if that has
| an easier answer), how should I define permutations of {0,1,...,n-1}?
There are a couple of HOL Light library files defining notions of
permutation, the first giving permutations on sets:
Yes, here's one explicit HOL Light realization of Konrad's solution:
let POLYNOMIAL_DEGREE_COEFFS =
let th = prove
(`?m c. !p. polynomial_function p
==> !x. p x = sum(0..m p) (\i. c p i * x pow i)`,
REWRITE_TAC[GSYM SKOLEM_THM] THEN
