# Re: [isabelle] partial functions: is f_rel too weak too?

This looks like another case of a missing congruence rule. This congreunce rule would express that your set comprehension only makes calls to f where B has become smaller. Grep for fundef_cong in the sources to see many examples. You may have to introduce an auxiliary constant to hide the complex set comprehension.
```
Tobias

On 29/02/2016 07:33, Peter Gammie wrote:
```
```Hi,

Consider this function and proof attempt:

function f :: "'a::finite set \<Rightarrow> 'a set \<Rightarrow> 'a list set" where
"f C B =
(if B = {} then {[]}
else if B \<subseteq> C
then {c # cs |c cs. c \<in> B \<and> cs \<in> f {} (B - {c})}
else {})"
by pat_completeness auto

lemma f_termination:
shows "f_dom (C, B)"
proof(induct t \<equiv> "card B" arbitrary: B C)
case (Suc i B C) then show ?case
apply -
apply (rule accpI)
apply (erule f_rel.cases)

Intuitively this function terminates because we keep removing elements of B from B. However f_rel does not seem to note that c is drawn from B in the recursion. (domintros is too weak, as is apparently well-known.)

Any tips?

In my use case f is actually only partially defined.

cheers,
peter

```
```
```

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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