Re: [isabelle] Proving nth on a sorted list monotone
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.
Sigurd Torkel Meldgaard schrieb:
> 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]:
> "sorted (xs::int list)"
> shows "xs ≠  ⟶ mono (λ a . xs ! a)"
> proof (induct xs rule: sorted.induct)
> case 1 show ?case by simp
> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and