# 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 , 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

 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..

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.

 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.