[isabelle] Proving nth on a sorted list monotone



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





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