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



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:
> 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.