Email Gateway (Aug 18 2022 at 10:53): Email Gateway (Aug 18 2022 at 10:53):From: Peter Vincent Homeier <palantir@trustworthytools.com>
(Note: This is a repaired version of this previous question, where
expressions pasted from Proof General now have the Ascii expansions.
The X-symbols did not copy well.)
I am having difficulty understanding how to make total recursive
function definitions in Isabelle/HOL when the termination argument
needs more information than just the well-founded measure to be
proven. As an example, consider the example from the Tutorial,
section 3.5.2, page 49:
recdef qs "measure length"
"qs [] = []"
"qs (x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter
(\<lambda>y. x<y) xs)"
(hints recdef_simp: less_Suc_eq_le)
This of course works as the tutorial shows. What is not clear is how
in general one arrives at the correct set of hints. In this case, I
thought it would be even easier to prove termination for this if I
proved the expression in the original error message:
*** Bad final proof state:
*** ALL x xs. length [y:xs. y <= x] < Suc (length xs)
*** 1. ALL x xs. length [y:xs. y <= x] < Suc (length xs)
*** 1 unsolved goals!
*** Proof failed!
*** At command "recdef".
So I set this up as a lemma and proved it:
lemma tst [simp]:
"length length [y:xs. y <= x] < Suc (length xs)"
apply(simp add: less_Suc_eq_le)
done
and then tried using "tst" as the hint in place of "less_Suc_eq_le":
recdef qs "measure length"
"qs [] = []"
"qs (x#xs) = qs(filter (\<lambda>y. y\<le>x) xs) @ [x] @ qs(filter
(\<lambda>y. x<y) xs)"
(hints recdef_simp: tst)
*** Bad final proof state:
*** ALL x xs. length (filter (op < x) xs) < Suc (length xs)
*** 1. ALL x xs. length (filter (op < x) xs) < Suc (length xs)
*** 1 unsolved goals!
*** Proof failed!
*** At command "recdef".
According to the error message, the hint supplied is exactly what was
requested. What is going wrong here?
Peter
Email Gateway (Aug 18 2022 at 10:54):From: Tobias Nipkow <nipkow@in.tum.de>
You supplied a lemma for <=, which fixed the first recursive call, but
now a similar lemma for < is needed. Your two "Bad final proof states"
are different.
Tobias
Peter Vincent Homeier schrieb:
Last updated: Nov 21 2024 at 12:39 UTC