Email Gateway (Aug 22 2022 at 12:43): Email Gateway (Aug 22 2022 at 12:43):From: Peter Gammie <peteg42@gmail.com>
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
Email Gateway (Aug 22 2022 at 12:43):From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s
Email Gateway (Aug 22 2022 at 12:44):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 12:59):From: Peter Gammie <peteg42@gmail.com>
Thanks Tobias and Andreas.
declare conj_cong[fundef_cong]
indeed does the job.
(A pointer from Section 8 of the functions manual to Section 10 would have helped me in this instance.)
cheers,
peter
Last updated: Nov 21 2024 at 12:39 UTC