Re: [isabelle] Bug in the algebra method for ideal membership



Hi,

>>
>> 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

I am not an Isabelle expert but did you try if this

lemma ideal_membership_2:
  fixes x0 x1 y0 y1 t z0 :: "'b::idom"
  shows "∃ q0 q1 q2 q3 q4.
          y0^2 - x1^2 =
              q0*(1 + x0 * y0 * x1 * y1 * z0) +
              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)
        "

succeeds. If it succeeds this means that there is a problem with
how degenerated cases (_ ≠ 0) are handled.

--
Laurent




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.