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

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