Prove heapify_btu to be in linear time

[maxhaslbeck]

For our verification of correctness and running time of heapsort we use a sub program heapify_btu.
We prove that it runs in O(n log n) because this suffices to prove heapsort in O(n log n), but it actually is O(n)

isabelle_llvm_time/thys/examples/sorting/Sorting_Heapsort.thy

Lines 1741 to 1746 in 7176c81

	definition heapify_btu_cost :: "_ \<Rightarrow> ecost"
	where "heapify_btu_cost xs\<^sub>0 = cost ''call'' (enat (h - Suc l) + 1) + cost ''icmp_slt'' (enat (h - Suc l) + 1)
	+ cost ''if'' (enat (h - Suc l) + 1) + cost ''sub'' (enat (h - Suc l) +1)
	+ cost ''sift_down'' (enat (h - Suc l))"
	\<comment> \<open>TODO: heapify_btu actually is O(n), not O(n * log n) ! but we don't need it for heapsort in O(n*log n)\<close>

Prove that heapify_btu is a linear time algorithm.

A proof sketch can be found here: https://en.wikipedia.org/wiki/Binary_heap#Building_a_heap
An Intuitive explanation can be found following the Pseudocode in https://en.wikipedia.org/wiki/Heapsort#Pseudocode .

At the moment the cost of each sift_down operation is linear in the length of the slice h-l, but actually, that needs to be refined to be dependent on the position l' for which siftdown is called.

One would need to relax:

isabelle_llvm_time/thys/examples/sorting/Sorting_Heapsort.thy

Lines 1618 to 1621 in 7176c81

	definition Rsd where "Rsd i = TId(''sift_down'':=sift_down3_cost (Discrete.log i))"
	lemma sift_down3_refines_heapify_btu_step:
	shows "sift_down3 l' xs \<le> \<Down>Id( timerefine (Rsd (h-l)) (heapify_btu_step l' xs\<^sub>0 xs))"