Theory M3_Polynomial

theory M3_Polynomial
  imports Pi_Relations Polynomials.MPoly_Type_Univariate
          "../MPoly_Utils/Poly_Extract" "../MPoly_Utils/Poly_Degree"
begin

subsection ‹The Matiyasevich-Robinson-Polynomial›

text ‹For any appropriately typed function fn, we introduce the syntax
        ‹fn π ≡ fn A1 A2 A3 S T R n›, as well as ‹(λπ. e) ≡ (λA1 A2 A3 S T R n. e)›.›

syntax "pi" :: "(int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int) ⇒ int" ("_ π" [1000] 1000)
syntax "pi_fn" :: "(int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int) ⇒ int" ("λπ. _" [0] 0)
parse_translation ‹
  [
    (
      \<^syntax_const>‹pi›,
      fn ctxt => fn args =>
        list_comb (
          args |> hd,
          ["A⇩1", "A⇩2", "A⇩3", "S", "T", "R", "n"] |> map (fn name => Free (name, @{typ int}))
        )
    ),
    (
      \<^syntax_const>‹pi_fn›,
      fn ctxt => fn args =>
        ["A⇩1", "A⇩2", "A⇩3", "S", "T", "R", "n"]
          |> List.foldr (fn (name, r) => Abs (name, @{typ int}, r)) (args |> hd)
    )
  ]
›

locale section5 = section5_given + section5_variables
begin

definition X⇩0 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int" where
  "X⇩0 π = 1 + A⇩1^2 + A⇩2^2 + A⇩3^2"
definition I⇩0 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int" where
  "I⇩0 π = (X⇩0 π)^3"
definition U⇩0 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int" where
  "U⇩0 π = S^2 * (2 * R - 1)"
definition V⇩0 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int" where
  "V⇩0 π = S^2 * n + T^2"

poly_extract X⇩0
poly_extract I⇩0
poly_extract U⇩0
poly_extract V⇩0


definition M3 :: "int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int ⇒ int" where
  "M3 A⇩1 A⇩2 A⇩3 S T R n =
    (
      ((
        (
          (
            ((V⇩0 π) - (U⇩0 π) * (I⇩0 π) - (U⇩0 π) * T^2)^2
              + (U⇩0 π)^2 * A⇩1
              + (U⇩0 π)^2 * A⇩2 * (X⇩0 π)^2
              - (U⇩0 π)^2 * A⇩3 * (X⇩0 π)^4
          )
        )^2 
          + 4 * (U⇩0 π)^2 * (V⇩0 π - U⇩0 π * I⇩0 π - U⇩0 π * T^2)^2 * A⇩1
          - 4 * (U⇩0 π)^2 * (V⇩0 π - U⇩0 π * I⇩0 π - U⇩0 π * T^2)^2 * A⇩2 * (X⇩0 π)^2
          - 4 * (U⇩0 π)^4 * A⇩1 * A⇩2 * (X⇩0 π)^2
      )^2)
        - A⇩1 * (U⇩0 π * (
          4
            * (V⇩0 π - U⇩0 π * I⇩0 π - U⇩0 π * T^2)
            * (
              ((V⇩0 π - U⇩0 π * I⇩0 π - U⇩0 π * T^2))^2
                + (U⇩0 π)^2 * A⇩1
                + (U⇩0 π)^2 * A⇩2 * (X⇩0 π)^2
                - (U⇩0 π)^2 * A⇩3 * (X⇩0 π)^4
              )
                - 8
                  * (U⇩0 π)^2
                  * (V⇩0 π - U⇩0 π * I⇩0 π - U⇩0 π * T^2)
                  * A⇩2
                  * (X⇩0 π)^2
        ))^2
    )
"

poly_extract M3

end

end