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