Rodrigo Raya reported on isabelle-users (10-Jan-2020) the following unexpected failure of the method "algebra", e.g. in Isabelle2020:
theory Scratch imports Main begin lemma ideal_membership_2: fixes x0 x1 y0 y1 t :: "'b::idom" assumes "x0 ≠ 0" "y0 ≠ 0" "x1 ≠ 0" "y1 ≠ 0" shows "∃ q1 q2 q3 q4. y0^2 - x1^2 = q1*(-1 + x0^2 + y0^2 - t^2 * x0^2 * y0^2) + q2*(-1 + x1^2 + y1^2 - t^2 * x1^2 * y1^2) + q3*(x0 * y0 - x1 * y1) + q4*(x1 * y0 + x0 * y1)" using assms apply algebra (* Exception trace - exception Option raised (line 82 of "General/basics.ML") Groebner.ring_and_ideal_conv(10)solve_idealism (line 872 of "/home/makarius/isabelle/repos/src/HOL/Tools/groebner.ML") Groebner.ideal_tac(3)(2)poly_exists_tac (line 959 of "/home/makarius/isabelle/repos/src/HOL/Tools/groebner.ML") exception Option raised (line 82 of "General/basics.ML") *) end
Further details are unclear. Amine Chaieb is the expert on this tool.