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

```Dear Walter,

function (sequential) ...

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.