*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] pattern compatibility: _ = _ foo_sumC _*From*: Walther Neuper <wneuper at ist.tugraz.at>*Date*: Sat, 13 Apr 2013 18:58:09 +0200*Cc*: Christian Sternagel <c.sternagel at gmail.com>*In-reply-to*: <51695185.8050105@gmail.com>*References*: <51691CB7.7000009@ist.tugraz.at> <51695185.8050105@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:15.0) Gecko/20120912 Thunderbird/15.0.1

Christian, thanks for reply ! Your suggestion ...

function (sequential) ... instead of just function ...does the trick (together with pat_completeness and auto).

goal (6 subgoals): 1. ?a x y xs aa xa ya xsa. (a, x # y # xs) = (aa, xa # ya # xsa) ? x # a # sep_sumC (a, y # xs) = xa # aa # sep_sumC (aa, ya # xsa)

4. ?a aa. (a, []) = (aa, []) ? [] = [] 5. ?a aa v. (a, []) = (aa, [v]) ? [] = [v] 6. ?a v aa va. (a, [v]) = (aa, [va]) ? [v] = [va]

a # sep_sumC (a, y # xs) = [] ? False

1. ?d p v vb vc ps. ([d], [p]) = (v # vb # vc, ps) ? ... 2. ?d p ds v vb vc. ([d], [p]) = (ds, v # vb # vc) ? ... 3. ?ps v vb vc psa. ([], ps) = (v # vb # vc, psa) ? ... 4. ?ds dsa v vb vc. (ds, []) = (dsa, v # vb # vc) ? ...

Walther [1] I am stuck with dvd for univariate polynomials:

"[d] dvd_unipoly [p] = ((¦d¦ ? ¦p¦) & (p mod d = 0))" | "ds dvd_unipoly ps = (let ds = drop_lc0 ds; ps = drop_lc0 ps; d000 = (List.replicate (List.length ps - List.length ds) 0) @ ds; quot = (lcoeff ps) div2 (lcoeff d000); rest = drop_lc0 (ps minus_up (d000 mult_ups quot)) in if rest = [] then True else

On 04/13/2013 05:52 PM, Walther Neuper wrote:Using the function package I cannot prove pattern compatibility with unary occurrence of "*_sumC" in the proof obligation, which I see happen quite often, e.g.[1]. Interestingly, the example on p.2 of the "Tutorial on Function Definition" is solved automatically by "fun", but "function" creates that kind of obligation, which is NOT provable "by auto": function sep :: "'a ? 'a list ? 'a list" where "sep a (x # y # xs) = x # a # sep a (y # xs)" | "sep a xs = xs" apply pat_completeness apply simp defer apply simp ------------------------------------------ proof (prove): step 4 goal (1 subgoal): 1. ?a x y xs aa xsa. (a, x # y # xs) = (aa, xsa) ? x # a # sep_sumC (a, y # xs) = xsa For learning how to prove this kind of obligations it seems very helpful to have the above example proved explicitly --- is there some of the experts, who could spend a few minutes on that, please ? WaltherPS: I scanned the documentation without findings: did I overlooksomething?And I scanned the mailing list with some findings [2/3, 4/5], but without coming to a clue. [1] the rhs of the conclusion contains dvd_up_sumC, the lhs does not; so one needs some properties of dvd_up_sumC for proving equality, e.g "dvd_up_sumC (ds, rest) = ds mod rest" (which easily can be proved under the assumptions given): 3. /\ d p ds ps. ([d], [p]) = (ds, ps) ==> (p mod d = 0) = (let ds = drop_lc0 ds; ps = drop_lc0 ps; d000 = replicate (length ps - length ds) 0 @ ds; quot = GCD_Poly_FP.lcoeff ps div2 GCD_Poly_FP.lcoeff d000; rest = drop_lc0 (ps minus_up (d000 mult_ups quot)) in if rest = [] then Trueelse if quot ? 0 ? length ds ? length rest thendvd_up_sumC (ds, rest) else False)

**References**:**[isabelle] pattern compatibility: _ = _ foo_sumC _***From:*Walther Neuper

**Re: [isabelle] pattern compatibility: _ = _ foo_sumC _***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] pattern compatibility: _ = _ foo_sumC _
- Next by Date: Re: [isabelle] What naming will cause potential errors?
- Previous by Thread: Re: [isabelle] pattern compatibility: _ = _ foo_sumC _
- Next by Thread: [isabelle] LFMTP'13: Call for papers
- Cl-isabelle-users April 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