Re: [isabelle] pattern compatibility: _ = _ foo_sumC _
function (sequential) ...
instead of just
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".
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..
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"
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 ?
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.
 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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and