In particular, I'd appreciate hints, how to identify the culprit from the output created by
declare [[simp_trace_depth_limit=9]] declare [[simp_trace=true]]when I activate the outcommented base case in the function below and thus make the function package loop:
(* dvd for univariate polynomials *) function dvd_up :: "unipoly ? unipoly ? bool" (infixl "dvd'_up" 70) where (* FIXME this makes the function package loop ...... "[d] dvd_up [i] = (if (¦d¦ ? ¦i¦) & (i mod d = 0) then True else False)" |*) "d dvd_up p = (let d = drop_lc0 d; p = drop_lc0 p; d000 = (List.replicate (List.length p - List.length d) 0) @ d; quot = (lc p) div2 (lc d000); rest = drop_lc0 (p minus_up (d000 div_ups quot)) in if rest =  then True else (if quot ? 0 & List.length d ? List.length rest then d dvd_up rest else False))" by pat_completeness auto termination sorryI'd appreciate help not by a solution (like the one below -- thank you, Alex!), but by hints how to find the culprit for looping myself.
WaltherPS: The auxiliary functions are in the appendix. Of course, they are all checked, see
https://intra.ist.tugraz.at/hg/isa/raw-file/913483f0582b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy On 01/21/2013 11:04 PM, Alexander Krauss wrote:
In your concrete case, the simplifier loops because the equation for is_prime loops in the presence of the usual splitting of ifs. Thus, "by pat_completeness (simp del: is_prime.simps)" does the trick here.