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