Re: [isabelle] pattern compatibility: _ = _ foo_sumC _



Dear Walter,

  function (sequential) ...

instead of just

  function ...

does the trick (together with pat_completeness and auto). Without the sequential option the defining equations must be disjoint and complete. See also "isabelle doc functions".

cheers

chris

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 ?

Walther


PS: I scanned the documentation without findings: did I overlook something?
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 True
            else if quot ? 0 ? length ds ? length rest then dvd_up_sumC
(ds, rest) else False)

[2]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-March/msg00023.html

[3]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-March/msg00026.html

[4]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-February/msg00001.html

[5]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-February/msg00002.html









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