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



As Tobias said, you have to declare an appropriate congruence rule for fun. The following works for me:

  declare conj_cong[fundef_cong]

Note that it is good not to have this rule in the default set of congruence rules, because if you add congruence rules, you get weaker induction rules. This is especially true for conj_cong when one defines recursive predicates with fun.

Andreas

On 29/02/16 07:56, Tobias Nipkow wrote:
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






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