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



Hi Giuliano,

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?

Not without going into the ugly internals of the definition process, which I would not recommend.

If not, how could I define l_c_p
differently?

In such cases it is often easier to give a "purely logical" definition using definite description in the style of
"l_c_p S = (THE xs.
  (ALL ys : s. is_suffix xs ys)
   & (EX ys : s. ALL x. ~ is_suffix (x # xs) ys))"

Then you can derive the recursive equations.

Alternatively you could try to use the fold combinator for finite sets defined in HOL/Finite_Set.thy.

Hope this helps,

Alex





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