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.


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

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.


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

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