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

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
--
http://peteg.org/

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