Theory Gaussian_Integers_Test

(*
  File:     Gaussian_Integers_Test.thy
  Author:   Manuel Eberl, TU München

  Test of code generation for executable factorisation algorithm for Gaussian integers
*)
theory Gaussian_Integers_Test
imports
  Gaussian_Integers
  "Polynomial_Factorization.Prime_Factorization"
  "HOL-Library.Code_Target_Numeral"
begin

text ‹
  Lastly, we apply our factorisation algorithm to some simple examples:
›

(*<*)
context
  includes gauss_int_notation
begin
(*>*)

value "(1234 + 5678 * 𝗂⇩ℤ) mod (321 + 654 * 𝗂⇩ℤ)"
value "prime_factors (1 + 3 * 𝗂⇩ℤ)"
value "prime_factors (4830 + 1610 * 𝗂⇩ℤ)"

(*<*)
end
(*>*)

end