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