Theory BTree_ImpSplit
theory BTree_ImpSplit
imports
BTree_ImpSet
BTree_Split
Imperative_Loops
begin
section "Imperative split operations"
text "So far, we have only given a functional specification of a possible split.
We will now provide imperative split functions that refine the functional specification.
However, rather than tracing the execution of the abstract specification,
the imperative versions are implemented using while-loops."
subsection "Linear split"
text "The linear split is the most simple split function for binary trees.
It serves a good example on how to use while-loops in Imperative/HOL
and how to prove Hoare-Triples about its application using loop invariants."
definition lin_split :: "('a::heap × 'b::{heap,linorder}) pfarray ⇒ 'b ⇒ nat Heap"
where
"lin_split ≡ λ (a,n) p. do {
i ← heap_WHILET
(λi. if i<n then do {
(_,s) ← Array.nth a i;
return (s<p)
} else return False)
(λi. return (i+1))
0;
return i
}"
lemma lin_split_rule: "
< is_pfa c xs (a,n)>
lin_split (a,n) p
<λi. is_pfa c xs (a,n) * ↑(i≤n ∧ (∀j<i. snd (xs!j) < p) ∧ (i<n ⟶ snd (xs!i)≥p))>⇩t"
unfolding lin_split_def
supply R = heap_WHILET_rule''[where
R = "measure (λi. n - i)"
and I = "λi. is_pfa c xs (a,n) * ↑(i≤n ∧ (∀j<i. snd (xs!j) < p))"
and b = "λi. i<n ∧ snd (xs!i) < p"
and Q="λi. is_pfa c xs (a,n) * ↑(i≤n ∧ (∀j<i. snd (xs!j) < p) ∧ (i<n ⟶ snd (xs!i)≥p))"
]
thm R
apply (sep_auto decon: R simp: less_Suc_eq is_pfa_def) []
apply (metis nth_take snd_eqD)
apply (metis nth_take snd_eqD)
apply (sep_auto simp: is_pfa_def less_Suc_eq)+
apply (metis nth_take)
apply(sep_auto simp: is_pfa_def)
apply (metis le_simps(3) less_Suc_eq less_le_trans nth_take)
apply(sep_auto simp: is_pfa_def)+
done
subsection "Binary split"
text "To obtain an efficient B-Tree implementation, we prefer a binary split
function.
To explore the searching procedure
and the resulting proof, we first implement the split on singleton arrays."
definition bin'_split :: "'b::{heap,linorder} array_list ⇒ 'b ⇒ nat Heap"
where
"bin'_split ≡ λ(a,n) p. do {
(low',high') ← heap_WHILET
(λ(low,high). return (low < high))
(λ(low,high). let mid = ((low + high) div 2) in
do {
s ← Array.nth a mid;
if p < s then
return (low, mid)
else if p > s then
return (mid+1, high)
else return (mid,mid)
})
(0::nat,n);
return low'
}"
thm sorted_wrt_nth_less
lemma bin'_split_rule: "
sorted_less xs ⟹
< is_pfa c xs (a,n)>
bin'_split (a,n) p
<λl. is_pfa c xs (a,n) * ↑(l ≤ n ∧ (∀j<l. xs!j < p) ∧ (l<n ⟶ xs!l≥p)) >⇩t"
unfolding bin'_split_def
supply R = heap_WHILET_rule''[where
R = "measure (λ(l,h). h-l)"
and I = "λ(l,h). is_pfa c xs (a,n) * ↑(l≤h ∧ h ≤ n ∧ (∀j<l. xs!j < p) ∧ (h<n ⟶ xs!h≥p))"
and b = "λ(l,h). l<h"
and Q="λ(l,h). is_pfa c xs (a,n) * ↑(l ≤ n ∧ (∀j<l. xs!j < p) ∧ (l<n ⟶ xs!l≥p))"
]
thm R
apply (sep_auto decon: R simp: less_Suc_eq is_pfa_def) []
subgoal for l' aa l'a aaa ba j
proof -
assume 0: "n ≤ length l'a"
assume a: "l'a ! ((aa + n) div 2) < p"
moreover assume "aa < n"
ultimately have b: "((aa+n)div 2) < n"
by linarith
then have "(take n l'a) ! ((aa + n) div 2) < p"
using a by auto
moreover assume "sorted_less (take n l'a)"
ultimately have "⋀j. j < (aa+n)div 2 ⟹ (take n l'a) ! j < (take n l'a) ! ((aa + n) div 2)"
using
sorted_wrt_nth_less[where ?P="(<)" and xs="(take n l'a)" and ?j="((aa + n) div 2)"]
a b "0" by auto
moreover fix j assume "j < (aa+n) div 2"
ultimately show "l'a ! j < p" using "0" b
using ‹take n l'a ! ((aa + n) div 2) < p› dual_order.strict_trans by auto
qed
subgoal for l' aa b l'a aaa ba j
proof -
assume t0: "n ≤ length l'a"
assume t1: "aa < b"
assume a: "l'a ! ((aa + b) div 2) < p"
moreover assume "b ≤ n"
ultimately have b: "((aa+b)div 2) < n" using t1
by linarith
then have "(take n l'a) ! ((aa + b) div 2) < p"
using a by auto
moreover assume "sorted_less (take n l'a)"
ultimately have "⋀j. j < (aa+b)div 2 ⟹ (take n l'a) ! j < (take n l'a) ! ((aa + b) div 2)"
using
sorted_wrt_nth_less[where ?P="(<)" and xs="(take n l'a)" and ?j="((aa + b) div 2)"]
a b t0 by auto
moreover fix j assume "j < (aa+b) div 2"
ultimately show "l'a ! j < p" using t0 b
using ‹take n l'a ! ((aa + b) div 2) < p› dual_order.strict_trans by auto
qed
apply sep_auto
apply (metis le_less nth_take)
apply (metis le_less nth_take)
apply sep_auto
subgoal for l' aa l'a aaa ba j
proof -
assume t0: "aa < n"
assume t1: " n ≤ length l'a"
assume t4: "sorted_less (take n l'a)"
assume t5: "j < (aa + n) div 2"
have "(aa+n) div 2 < n" using t0 by linarith
then have "(take n l'a) ! j < (take n l'a) ! ((aa + n) div 2)"
using t0 sorted_wrt_nth_less[where xs="take n l'a" and ?j="((aa + n) div 2)"]
t1 t4 t5 by auto
then show ?thesis
using ‹(aa + n) div 2 < n› t5 by auto
qed
subgoal for l' aa b l'a aaa ba j
proof -
assume t0: "aa < b"
assume t1: " n ≤ length l'a"
assume t3: "b ≤ n"
assume t4: "sorted_less (take n l'a)"
assume t5: "j < (aa + b) div 2"
have "(aa+b) div 2 < n" using t3 t0 by linarith
then have "(take n l'a) ! j < (take n l'a) ! ((aa + b) div 2)"
using t0 sorted_wrt_nth_less[where xs="take n l'a" and ?j="((aa + b) div 2)"]
t1 t4 t5 by auto
then show ?thesis
using ‹(aa + b) div 2 < n› t5 by auto
qed
apply (metis nth_take order_mono_setup.refl)
apply sep_auto
apply (sep_auto simp add: is_pfa_def)
done
text "Then, using the same loop invariant, a binary split for B-tree-like arrays
is derived in a straightforward manner."
definition bin_split :: "('a::heap × 'b::{heap,linorder}) pfarray ⇒ 'b ⇒ nat Heap"
where
"bin_split ≡ λ(a,n) p. do {
(low',high') ← heap_WHILET
(λ(low,high). return (low < high))
(λ(low,high). let mid = ((low + high) div 2) in
do {
(_,s) ← Array.nth a mid;
if p < s then
return (low, mid)
else if p > s then
return (mid+1, high)
else return (mid,mid)
})
(0::nat,n);
return low'
}"
thm nth_take
lemma nth_take_eq: "take n ls = take n ls' ⟹ i < n ⟹ ls!i = ls'!i"
by (metis nth_take)
lemma map_snd_sorted_less: "⟦sorted_less (map snd xs); i < j; j < length xs⟧
⟹ snd (xs ! i) < snd (xs ! j)"
by (metis (mono_tags, opaque_lifting) length_map less_trans nth_map sorted_wrt_iff_nth_less)
lemma map_snd_sorted_lesseq: "⟦sorted_less (map snd xs); i ≤ j; j < length xs⟧
⟹ snd (xs ! i) ≤ snd (xs ! j)"
by (metis eq_iff less_imp_le map_snd_sorted_less order.not_eq_order_implies_strict)
lemma bin_split_rule: "
sorted_less (map snd xs) ⟹
< is_pfa c xs (a,n)>
bin_split (a,n) p
<λl. is_pfa c xs (a,n) * ↑(l ≤ n ∧ (∀j<l. snd(xs!j) < p) ∧ (l<n ⟶ snd(xs!l)≥p)) >⇩t"
unfolding bin_split_def
supply R = heap_WHILET_rule''[where
R = "measure (λ(l,h). h-l)"
and I = "λ(l,h). is_pfa c xs (a,n) * ↑(l≤h ∧ h ≤ n ∧ (∀j<l. snd (xs!j) < p) ∧ (h<n ⟶ snd (xs!h)≥p))"
and b = "λ(l,h). l<h"
and Q="λ(l,h). is_pfa c xs (a,n) * ↑(l ≤ n ∧ (∀j<l. snd (xs!j) < p) ∧ (l<n ⟶ snd (xs!l)≥p))"
]
thm R
apply (sep_auto decon: R simp: less_Suc_eq is_pfa_def) []
apply(auto dest!: sndI nth_take_eq[of n _ _ "(_ + _) div 2"])[]
apply(auto dest!: sndI nth_take_eq[of n _ _ "(_ + _) div 2"])[]
apply (sep_auto dest!: sndI )
subgoal for ls i ls' _ _ j
using map_snd_sorted_lesseq[of "take n ls'" j "(i + n) div 2"]
less_mult_imp_div_less apply(auto)[]
done
subgoal for ls i j ls' _ _ j'
using map_snd_sorted_lesseq[of "take n ls'" j' "(i + j) div 2"]
less_mult_imp_div_less apply(auto)[]
done
apply sep_auto
subgoal for ls i ls' _ _ j
using map_snd_sorted_less[of "take n ls'" j "(i + n) div 2"]
less_mult_imp_div_less
apply(auto)[]
done
subgoal for ls i j ls' _ _ j'
using map_snd_sorted_less[of "take n ls'" j' "(i + j) div 2"]
less_mult_imp_div_less
apply(auto)[]
done
apply (metis le_less nth_take_eq)
apply sep_auto
apply (sep_auto simp add: is_pfa_def)
done
subsection "Refinement of an abstract split"
text "We provide a certain abstract split function
that is particularly easy to analyse. The idea of this function is due to Peter Lammich."
definition "abs_split xs x = (takeWhile (λ(_,s). s<x) xs, dropWhile (λ(_,s). s<x) xs)"