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