# [isabelle] definition using "function": proving pattern compatibility

Hello,
I would like to define the longest common postfix of a finite set of lists.
I tried the following:
definition l_c_p_2 :: "'a list => 'a list => 'a list"
-- "returns the longest common prefix of two lists"
where ...
function l_c_p :: "'a list set => 'a list"
where
"[| l ~: ls; ls ~= {}; finite ls |] ==> l_c_p ({l} Un ls) = l_c_p_2 l
(l_c_p ls)"
| "l_c_p {l} = l"
| "l_c_p {} = []"
| "~ finite ls ==> l_c_p ls = dontcare"
One of the things I have to solve to complete the definition is the
following:
"!! l ls la lsa x xa. [| l ~: ls; la ~: lsa; insert l ls = insert la lsa;
l_c_postfix l (l_c_p_test_sumC ls) ~= l_c_postfix la (l_c_p_test_sumC lsa);
x : ls; xa : lsa; finite ls; finite lsa |] ==> False"
Since there are no assumptions about l_c_p_sumC I can't prove the goal.
Is there a way to make it work? If not, how could I define l_c_p
differently?
Thanks,
Giuliano

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