Theory Sorting_Log2
theory Sorting_Log2
imports Sorting_Setup
begin
section ‹Count Leading Zeroes and Log2›
subsection ‹Explicit Implementation by Loop›
definition word_clz' :: "'a::len word ⇒ nat" where
"word_clz' x ≡ if x=0 then 0 else word_clz x"
lemma word_clz'_eq: "x≠0 ⟹ word_clz' x = word_clz x"
by (simp add: word_clz'_def)
lemma of_bl_eqZ:
"⟦ length xs = LENGTH ('a::len) ⟧ ⟹ (of_bl xs :: 'a word) = 0 ⟷ (xs = replicate LENGTH('a) False)"
apply auto
by (metis to_bl_0 to_bl_use_of_bl word_bl_Rep')
lemma cons_eq_replicate_conv: "x#xs = replicate n y ⟷ (∃n'. n=Suc n' ∧ x=y ∧ xs = replicate n' y)"
by (cases n; simp)
lemma replicate_eq_cons_conv: "x#xs = replicate n y ⟷ (∃n'. n=Suc n' ∧ x=y ∧ xs = replicate n' y)"
by (cases n; simp)
lemma append_eq_replicate_conv: "xs⇩1@xs⇩2 = replicate n x
⟷ (∃n⇩1 n⇩2. n=n⇩1+n⇩2 ∧ xs⇩1=replicate n⇩1 x ∧ xs⇩2=replicate n⇩2 x)"
apply (auto simp: replicate_add)
by (metis append_eq_append_conv length_append length_replicate replicate_add)
lemma Cons_butlast_replicate: "n>0 ⟹ x#butlast (replicate n x) = replicate n x"
by (induction n; auto)
lemma rev_bl_order_Nil_simps:
"rev_bl_order x xs [] ⟷ x ∧ xs=[]"
"rev_bl_order x [] xs ⟷ x ∧ xs=[]"
unfolding rev_bl_order_def
by auto
lemma rev_bl_order_all_false_conv: "rev_bl_order a xs (replicate n False) ⟷
a ∧ xs = replicate n False"
unfolding rev_bl_order_def
by auto
lemma rev_eq_replicate_conv: "rev xs = replicate n x ⟷ xs = replicate n x"
by (metis rev_replicate rev_rev_ident)
lemma sle_zero_bl_conv: "x ≤s 0 ⟷ hd (to_bl x) = True ∨ to_bl x = replicate (LENGTH('a)) False" for x :: "'a::len word"
apply (cases "to_bl x")
subgoal by simp
subgoal for a list
apply (simp add: word_sle_rbl map_last_def)
apply (subst rev_bl_order_rev_simp)
subgoal by (metis diff_Suc_1 length_Cons length_butlast length_rev length_to_bl_eq to_bl_0)
apply (cases a; simp)
apply (cases "LENGTH('a)"; simp)
apply (auto simp:
rev_bl_order_simps rev_bl_order_Nil_simps Cons_butlast_replicate rev_bl_order_all_false_conv
rev_eq_replicate_conv
)
done
done
lemma to_bl_eq_rep_False_conv: "to_bl x = replicate n False ⟷ x=0 ∧ n=LENGTH('a)" for x :: "'a::len word"
by (simp add: to_bl_use_of_bl)
lemma eq_z_to_bl_conv: "x=0 ⟷ to_bl x = replicate (LENGTH('a)) False" for x::"'a::len word"
by (auto simp: to_bl_eq_rep_False_conv)
lemma word_clz'_rec: "word_clz' x = (if x <=s 0 then 0 else 1 + word_clz' (x << 1))"
supply [simp del] = shiftl_of_Suc
apply (clarsimp simp: word_clz'_def word_clz_def)
apply (cases "to_bl x"; simp)
subgoal for a list
apply (auto simp: sle_zero_bl_conv to_bl_eq_rep_False_conv)
subgoal
by (auto simp: eq_z_to_bl_conv bl_shiftl cons_eq_replicate_conv append_eq_replicate_conv)
subgoal
apply (auto simp: eq_z_to_bl_conv bl_shiftl)
apply (subgoal_tac "True∈set list")
subgoal by simp
by (metis eq_zero_set_bl set_ConsD to_bl_0)
done
done
lemma word_clz'_rec2: "word_clz' x = (if 0 <s x then 1 + word_clz' (x << 1) else 0)"
by (meson signed.not_le word_clz'_rec)
lemma word_clz'_simps2:
"0 <s x ⟹ word_clz' x = 1 + word_clz' (x << 1)"
"¬(0 <s x) ⟹ word_clz' x = 0"
using word_clz'_rec2 by metis+
definition word_clz2 :: "'a::len2 word ⇒ nat nres"
where "word_clz2 x ≡ do {
(c,_) ← WHILET (λ(c,x). 0 <s x) (λ(c,x). do {
ASSERT (c + 1 < max_snat LENGTH('a));
RETURN (c+1,x << 1)
}) (0,x);
RETURN c
}"
lemma word_clz'_fits_snat: "word_clz' (x::'a::len2 word) < max_snat LENGTH('a)"
unfolding word_clz'_def using word_clz_nonzero_max[of x]
apply (auto simp: word_size max_snat_def)
by (meson le_def n_less_equal_power_2 nat_le_Suc_less_imp order_trans)
lemma word_clz2_refine: "word_clz2 x⇩0 ≤ RETURN (word_clz' x⇩0)"
unfolding word_clz2_def
supply [refine_vcg] = WHILET_rule[
where I="λ(c,x). word_clz' x⇩0 = c + word_clz' x"
and R="measure (word_clz' o snd)"
]
apply refine_vcg
using word_clz'_fits_snat[of x⇩0]
apply (auto simp: word_clz'_simps2)
done
lemma word_clz2_refine': "(word_clz2, RETURN o word_clz') ∈ Id → ⟨Id⟩nres_rel"
by (auto intro!: nres_relI simp: word_clz2_refine)
sepref_def word_clz'_impl is word_clz2 :: "(word_assn' TYPE('a::len2))⇧k →⇩a snat_assn' TYPE('a)"
unfolding word_clz2_def
apply (rewrite at "(_ + ⌑,_)" snat_const_fold[where 'a='a])
apply (rewrite at "(_ << ⌑)" snat_const_fold[where 'a='a])
apply (rewrite at "(⌑,_)" snat_const_fold[where 'a='a])
by sepref
export_llvm "word_clz'_impl :: 64 word ⇒ 64 word llM"
sepref_register word_clz word_clz'
lemmas [sepref_fr_rules] = word_clz'_impl.refine[FCOMP word_clz2_refine']
lemma word_clz_alt: "word_clz x = (if x=0 then size x else word_clz' x)"
unfolding word_clz'_def by (auto simp: word_size)
sepref_def word_clz_impl
is "RETURN o word_clz" :: "[λ_. LENGTH('a)>2]⇩a (word_assn' TYPE('a::len2))⇧k → snat_assn' TYPE('a)"
unfolding word_clz_alt
by sepref
export_llvm "word_clz_impl :: 64 word ⇒ _"
lemma word_clz_nonzero_max': "x≠0 ⟹ word_clz (x::'a::len2 word) < LENGTH('a)"
using word_clz_nonzero_max[of x] unfolding word_size
by simp
sepref_def word_log2_impl is
"RETURN o word_log2" :: "[λx. x>0 ∧ LENGTH('a)>2]⇩a (word_assn' TYPE('a::len2))⇧k → snat_assn' TYPE('a)"
unfolding word_log2_def word_size
apply (annot_snat_const "TYPE('a)")
supply [simp] = word_clz_nonzero_max'
by sepref
export_llvm "word_log2_impl :: 64 word ⇒ _"
subsection ‹Connection with \<^const>‹Discrete.log››
lemma discrete_log_ltI:
assumes "n≠0" "N≠0" "n<2^N"
shows "Discrete.log n < N"
using assms
by (metis Discrete.log_le_iff leD linorder_neqE_nat log_exp log_exp2_le order_less_le zero_order(3))
lemma unat_x_div_2_conv:
fixes x y :: "'a::len2 word"
shows "unat x div 2 = unat y ⟷ y = x div 2"
proof -
have A: "2 = unat (2::'a word)"
by (metis le_less_trans len2_simps(2) n_less_equal_power_2 of_nat_numeral unat_of_nat_len)
have B: "unat x div 2 = unat (x div 2)"
unfolding A
by (simp add: unat_div)
show ?thesis
by (auto simp: B dest: word_unat.Rep_eqD)
qed
lemma take_size_m1_to_bl:
fixes x :: "'a::len word"
shows "take (size x - Suc 0) (to_bl x) = butlast (to_bl x)"
by (simp add: butlast_conv_take word_size_bl)
lemma takeWhile_butlast_eqI: "⟦x∈set xs; ¬P x⟧ ⟹ takeWhile P (butlast xs) = takeWhile P xs"
by (metis append_Nil2 butlast.simps(2) butlast_append list.simps(3) split_list_last takeWhile_tail)
lemma takeWhile_butlast_eqI': "⟦∃x∈set xs. ¬P x⟧ ⟹ takeWhile P (butlast xs) = takeWhile P xs"
by (metis append_Nil2 butlast.simps(2) butlast_append list.simps(3) split_list_last takeWhile_tail)
lemma ex_True_in_set_conv: "(∃x∈S. x) ⟷ True∈S" by auto
lemma word_clz_rec:
fixes x :: "'a::len2 word"
shows "2≤x ⟹ word_clz (x div 2) = word_clz x + 1"
unfolding word_clz_def shiftr1_is_div_2[symmetric]
apply (auto simp: bl_shiftr word_size)
apply (subst bl_shiftr)
apply (simp add: word_size Suc_leI)
apply (auto simp: take_size_m1_to_bl)
apply (subst takeWhile_butlast_eqI')
apply (simp_all add: ex_True_in_set_conv)
apply (rule ccontr)
apply (simp only: eq_zero_set_bl[symmetric])
by (metis le_unat_uoi len2_simps(2) n_less_equal_power_2 of_nat_numeral unat_0 unat_of_nat_len word_le_0_iff zero_neq_numeral)
lemma word_clz_ge2_max: "2≤(x::'a::len2 word) ⟹ word_clz x + 1 < size x"
apply (simp only: word_clz_rec[symmetric] word_size)
apply (rule word_clz_nonzero_max[of "x div 2", unfolded word_size])
by (smt One_nat_def Suc_pred add.left_neutral add.right_neutral add_diff_cancel_left' add_diff_cancel_right' add_left_cancel diff_Suc_Suc div_less div_of_0_id div_self lessI less_eq_Suc_le less_one linorder_neqE_nat linorder_not_le mult.right_neutral not_numeral_le_zero numeral_2_eq_2 numeral_One numeral_le_one_iff order_less_le overflow_safe_hbound_check pos2 power.simps(1) power.simps(2) semiring_norm(69) unat_0 unat_div unat_eq_zero unat_gt_0 unat_x_div_2_conv word_clz_rec word_gt_0_no word_le_nat_alt zero_less_one zero_neq_one)
lemma word_log2_rec:
fixes x :: "'a::len2 word" shows "2≤x ⟹ word_log2 x = Suc (word_log2 (x div 2))"
apply (auto simp: word_log2_def word_size word_clz_rec)
using word_clz_ge2_max[unfolded word_size, of x]
by auto
lemma word_log2_is_discrete_log:
fixes x :: "'a::len2 word"
shows "word_log2 x = Discrete.log (unat x)"
apply (cases "x=0")
apply simp
subgoal proof -
assume "x ≠ 0"
hence "unat x > 0" by (simp add: unat_gt_0)
then show ?thesis
proof (induction "unat x" arbitrary: x rule: log_induct)
case one
hence "x=1" using word_unat_Rep_inject1 by auto
then show ?case
unfolding word_log2_def
by (auto simp: word_size)
next
case double
from double.hyps(2) have "Discrete.log (unat x div 2) = word_log2 (x div 2)"
by (metis unat_x_div_2_conv)
then show ?case
apply (subst log_rec, simp add: ‹2 ≤ unat x›)
apply simp
apply (subst word_log2_rec)
apply auto
using double.hyps(1) le_unat_uoi word_le_nat_alt by fastforce
qed
qed
done
lemma word_log2_refine_unat: "(word_log2, Discrete.log) ∈ unat_rel' TYPE('a::len2) → nat_rel"
using word_log2_is_discrete_log
by (fastforce simp: unat_rel_def unat.rel_def in_br_conv)
lemma word_log2_refine_snat: "(word_log2, Discrete.log) ∈ snat_rel' TYPE('a::len2) → nat_rel"
using word_log2_is_discrete_log
by (fastforce simp: snat_rel_def snat.rel_def in_br_conv snat_eq_unat)
sepref_register Discrete.log
lemmas discrete_log_unat_hnr[sepref_fr_rules] = word_log2_impl.refine[FCOMP word_log2_refine_unat]
lemmas discrete_log_snat_hnr[sepref_fr_rules] = word_log2_impl.refine[FCOMP word_log2_refine_snat]
end