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