Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving nth on a sorted list monotone

Email Gateway (Aug 18 2022 at 13:30):

From: Sigurd Torkel Meldgaard <stm@cs.au.dk>
Hi Isabelle-users

I am stumblingly trying to prove that nth is monotone on a sorted
list, I got this far:

lemma sorted_mono[simp]:
assumes
"sorted (xs::int list)"
shows "xs ≠ [] ⟶ mono (λ a . xs ! a)"
proof (induct xs rule: sorted.induct)
case 1 show ?case by simp
next
case (2 element) show ?case
proof (simp add: mono_def)

And here I am stuck, do I have to explicitly assume that the indices
are within the length of xs, or how does a proof with a partial
function work?

All the best

/Sigurd

Email Gateway (Aug 18 2022 at 13:31):

From: Tobias Nipkow <nipkow@in.tum.de>
HOL is a logic of total functions. nth xs i is defined, but unless i <
length xs, you have no idea what the value is. Hence you can only prove
monotonicity with that precondition.

Best
Tobias

Sigurd Torkel Meldgaard schrieb:

Email Gateway (Aug 18 2022 at 13:31):

From: Tobias Nipkow <nipkow@in.tum.de>
It's a useful thm, hence I just proved and added it to List.thy:

lemma sorted_nth_mono:
"sorted xs ==> i <= j ==> j < length xs ==> xs!i <= xs!j"
by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)

Thanks
Tobias

Sigurd Torkel Meldgaard schrieb:

Last updated: May 03 2024 at 04:19 UTC