src/HOL/Tools/Groebner_Basis/groebner.ML
 changeset 24913 eb6fd8f78d56 parent 24630 351a308ab58d child 25251 759bffe1d416
equal inserted replaced
24912:52bc004950c4 24913:eb6fd8f78d56
`   355 (* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)`
`   355 (* Prove a polynomial is in ideal generated by others, using Grobner basis.  *)`
`   356 (* ------------------------------------------------------------------------- *)`
`   356 (* ------------------------------------------------------------------------- *)`
`   357 `
`   357 `
`   358 fun grobner_ideal vars pols pol =`
`   358 fun grobner_ideal vars pols pol =`
`   359   let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in`
`   359   let val (pol',h) = reduce (grobner pols) (grob_neg pol,Start(~1)) in`
`   360   if not (null pol) then error "grobner_ideal: not in the ideal" else`
`   360   if not (null pol') then error "grobner_ideal: not in the ideal" else`
`   361   resolve_proof vars h end;`
`   361   resolve_proof vars h end;`
`   362 `
`   362 `
`   363 (* ------------------------------------------------------------------------- *)`
`   363 (* ------------------------------------------------------------------------- *)`
`   364 (* Produce Strong Nullstellensatz certificate for a power of pol.            *)`
`   364 (* Produce Strong Nullstellensatz certificate for a power of pol.            *)`
`   365 (* ------------------------------------------------------------------------- *)`
`   365 (* ------------------------------------------------------------------------- *)`