# Theory Parametric_Polynomials

section ‹Diophantine Equations›
theory Parametric_Polynomials
imports Main
abbrevs ++ = "❙**+**" and
-- = "❙**-**" and
** = "❙*****" and
00 = "❙**0**" and
11 = "❙**1**"
begin
subsection ‹Parametric Polynomials›
text ‹This section defines parametric polynomials and builds up the infrastructure to later prove
that a given predicate or relation is Diophantine. The formalization follows
\<^cite>‹"h10lecturenotes"›.›
type_synonym assignment = "nat ⇒ nat"
text ‹Definition of parametric polynomials with natural number coefficients and their evaluation
function›