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›

datatype ppolynomial =
    Const nat |
    Param nat |
    Var   nat |
    Sum  ppolynomial ppolynomial (infixl ‹❙+› 65) |
    NatDiff ppolynomial ppolynomial (infixl ‹❙-› 65) |
    Prod ppolynomial ppolynomial (infixl ‹❙*› 70)

fun ppeval :: "ppolynomial ⇒ assignment ⇒ assignment ⇒ nat"  where
    "ppeval (Const c) p v = c" |
    "ppeval (Param x) p v = p x" |
    "ppeval (Var x) p v = v x" |
    "ppeval (D1 ❙+ D2) p v = (ppeval D1 p v) + (ppeval D2 p v)" |
    (* The next line lifts subtraction of type "nat ⇒ nat ⇒ nat" *)
    "ppeval (D1 ❙- D2) p v = (ppeval D1 p v) - (ppeval D2 p v)" |
    "ppeval (D1 ❙* D2) p v = (ppeval D1 p v) * (ppeval D2 p v)"

definition Sq_pp (‹_ ❙^❙2› [99] 75) where "Sq_pp P = P ❙* P"

definition is_dioph_set :: "nat set ⇒ bool" where
    "is_dioph_set A = (∃P1 P2::ppolynomial. ∀a. (a ∈ A)
                                            ⟷ (∃v. ppeval P1 (λx. a) v = ppeval P2 (λx. a) v))"

datatype polynomial =
    Const nat |
    Param nat |
    Sum  polynomial polynomial (infixl ‹[+]› 65) |
    NatDiff polynomial polynomial (infixl ‹[-]› 65) |
    Prod polynomial polynomial (infixl ‹[*]› 70)

fun peval :: "polynomial ⇒ assignment ⇒ nat"  where
    "peval (Const c) p = c" |
    "peval (Param x) p = p x" |
    "peval (Sum D1 D2) p = (peval D1 p) + (peval D2 p)" |
    (* The next line lifts subtraction of type "nat ⇒ nat ⇒ nat" *)
    "peval (NatDiff D1 D2) p = (peval D1 p) - (peval D2 p)" |
    "peval (Prod D1 D2) p = (peval D1 p) * (peval D2 p)"

definition sq_p :: "polynomial ⇒ polynomial" (‹_ [^2]› [99] 75) where "sq_p P = P [*] P"

definition zero_p :: "polynomial" (‹❙0›) where "zero_p = Const 0"
definition one_p :: "polynomial" (‹❙1›) where "one_p = Const 1"

lemma sq_p_eval: "peval (P[^2]) p = (peval P p)^2"
  unfolding sq_p_def by (simp add: power2_eq_square)

fun convert :: "polynomial ⇒ ppolynomial"  where
    "convert (Const c) = (ppolynomial.Const c)" |
    "convert (Param x) = (ppolynomial.Param x)" |
    "convert (D1 [+] D2) = (convert D1) ❙+ (convert D2)" |
    "convert (D1 [-] D2) = (convert D1) ❙- (convert D2)" |
    "convert (D1 [*] D2) = (convert D1) ❙* (convert D2)"

lemma convert_eval: "peval P a = ppeval (convert P) a v" (* implicit for all v *)
  by (induction P, auto)

definition list_eval :: "polynomial list ⇒ assignment ⇒ (nat ⇒ nat)" where
    "list_eval PL a = nth (map (λx. peval x a) PL)"

end