Re: [isabelle] *_sumC generated by function package



Sorry for not coming with my problem cut down to a minimal example --- my problem is the mass of tracing output from the simplifier.

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 sorry

I'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.

Walther


PS: The auxiliary functions are in the appendix. Of course, they are all checked, see

[1]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.

Attachment: GCD_Poly_Test3.thy
Description: application/extension-thy



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