*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] *_sumC generated by function package*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Fri, 08 Feb 2013 17:20:35 +0100*In-reply-to*: <50FDBB5C.20500@in.tum.de>*References*: <50FD7742.6090002@ist.tugraz.at> <50FDBB5C.20500@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:15.0) Gecko/20120912 Thunderbird/15.0.1

declare [[simp_trace_depth_limit=9]] declare [[simp_trace=true]]

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

Walther

[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 foris_prime loops in the presence of the usual splitting of ifs.Thus, "by pat_completeness (simp del: is_prime.simps)" does the trickhere.

**Attachment:
GCD_Poly_Test3.thy**

- Previous by Date: Re: [isabelle] Isabelle2013-RC3 available for testing
- Next by Date: Re: [isabelle] Isabelle2013-RC3 available for testing
- Previous by Thread: Re: [isabelle] Generating .tex from .thy without a proper session
- Next by Thread: [isabelle] Record field names and accessing other constants
- Cl-isabelle-users February 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list