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

```Christian,

```
```function (sequential) ...

function ...

```
does the trick (together with pat_completeness and auto).
```
```
helped me to pin down my problem: "function (sequential) sep ... " creates these obligations for pattern compatibility:
```
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)
```
2. ?a x y xs aa. (a, x # y # xs) = (aa, []) ? x # a # sep_sumC (a, y # xs) = [] 3. ?a x y xs aa v. (a, x # y # xs) = (aa, [v]) ? x # a # sep_sumC (a, y # xs) = [v]
```     4. ?a aa. (a, []) = (aa, []) ? [] = []
5. ?a aa v. (a, []) = (aa, [v]) ? [] = [v]
6. ?a v aa va. (a, [v]) = (aa, [va]) ? [v] = [va]

```
My interest was for 'mixed' obligations like 3./4. above, where "_sumC" occurs only once: I wanted to prove the equalities (which is impossible without knowledge about "_sumC") under the assumptions.
```
```
Now I see (thanks to your help!), that these obligations are proved using the fact that the *assumptions*, "(a, x # y # xs) = (aa, [])" and "(a, x # y # xs) = (aa, [v])", *are not satisfiable* ('ex falso qodlibet'). The simplifier knows theorems like "List.inject", "List.distinct_2" etc good enough to end up with
```
a # sep_sumC (a, y # xs) = [] ? False

```
In the case of the function I am trying to define [1], I get 15 obligations: the 11 'non-mixed' obligations are solved "by simp" (which each takes a few seconds for each). However, the 4 'mixed' obligations cannot be proved "by simp" (which loop somewhere I can not yet identify in the trace), although they all have non-satisfiable assumptions...
```
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) ? ...

```
So, instead of tweaking the simplifier, it seems to suffice to show the assumptions not satisfiable ;-))) ... thanks a lot !!!
```
Walther

[1] I am stuck with dvd for univariate polynomials:
```
function (sequential) dvd_unipoly :: "unipoly ? unipoly ? bool" (infixl "dvd'_unipoly" 70) where
```      "[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
```
if quot ? 0 & List.length ds ? List.length rest then ds dvd_unipoly rest else False)"
```

```
```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)
```

```

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