Theory VEBT_Succ
theory VEBT_Succ imports VEBT_Insert VEBT_MinMax
begin
section ‹The Successor Operation›
definition is_succ_in_set :: "nat set ⇒ nat ⇒ nat ⇒ bool" where
"is_succ_in_set xs x y = (y ∈ xs ∧ y > x ∧ (∀ z ∈ xs. (z > x ⟶ z ≥ y)))"
context VEBT_internal begin
corollary succ_member: "is_succ_in_set (set_vebt' t) x y = (vebt_member t y ∧ y > x ∧ (∀ z. vebt_member t z ∧ z > x ⟶ z ≥ y))"
using is_succ_in_set_def set_vebt'_def by auto
subsection ‹Auxiliary Lemmas on Sets and Successorship›
lemma "finite (A:: nat set) ⟹ A ≠ {}⟹ Min A ∈ A"
by(induction A rule: finite.induct)(blast | meson Min_in finite_insert)+
lemma obtain_set_succ: assumes "(x::nat) < z " and "max_in_set A z" and "finite B" and "A=B" shows "∃ y. is_succ_in_set A x y"
proof-
have "{y ∈ A. y > x} ≠ {}"
using assms(1) assms(2) max_in_set_def by auto
have "Min {y ∈ A. y > x} ∈ {y ∈ A. y > x}"
by (metis (full_types) Collect_mem_eq ‹{y ∈ A. x < y} ≠ {}› assms(3) assms(4) eq_Min_iff finite_Collect_conjI)
have "i ∈ A⟹ i > x ⟹ i ≥ Min {y ∈ A. y > x} " for i
by (simp add: assms(3) assms(4))
have "is_succ_in_set A x (Min {y ∈ A. y > x})"
using is_succ_in_set_def ‹Min {y ∈ A. x < y} ∈ {y ∈ A. x < y}› ‹⋀i. ⟦i ∈ A; x < i⟧ ⟹ Min {y ∈ A. x < y} ≤ i› by blast
then show?thesis by auto
qed
lemma succ_none_empty: assumes "(∄ x. is_succ_in_set (xs) a x)" and "finite xs"shows "¬ (∃ x ∈ xs. ord_class.greater x a)"
proof-
have "∃ x ∈ xs. ord_class.greater x a ⟹ False"
proof-
assume "∃ x ∈ xs. ord_class.greater x a"
hence "{x ∈ xs. ord_class.greater x a} ≠ {}" by auto
have "Min {y ∈ xs. y > a} ∈ {y ∈ xs. y > a}"
by (metis (full_types) Collect_mem_eq Min_in ‹{x ∈ xs. a < x} ≠ {}› assms(2) finite_Collect_conjI)
have "i ∈ xs ⟹ ord_class.greater i a⟹
ord_class.greater_eq i (Min {y ∈ xs. ord_class.greater y a}) " for i
by (simp add: assms(2))
have "is_succ_in_set xs a (Min {y ∈ xs. y > a})"
using is_succ_in_set_def ‹Min {y ∈ xs. a < y} ∈ {y ∈ xs. a < y}› ‹⋀i. ⟦i ∈ xs; a < i⟧ ⟹ Min {y ∈ xs. a < y} ≤ i› by blast
then show False
using assms(1) by blast
qed
then show ?thesis by blast
qed
end
subsection ‹The actual Function›
context begin
interpretation VEBT_internal .
fun vebt_succ :: "VEBT ⇒ nat ⇒ nat option" where
"vebt_succ (Leaf _ b) 0 = (if b then Some 1 else None)"|
"vebt_succ (Leaf _ _) (Suc n) = None"|
"vebt_succ (Node None _ _ _) _ = None"|
"vebt_succ (Node _ 0 _ _) _ = None"|
"vebt_succ (Node _ (Suc 0) _ _) _ = None"|
"vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = (
if x < mi then (Some mi)
else (let l = low x (deg div 2); h = high x (deg div 2) in
if h < length treeList then
let maxlow = vebt_maxt (treeList ! h) in (
if maxlow ≠ None ∧ (Some l <⇩o maxlow) then
Some (2^(deg div 2)) *⇩o Some h +⇩o vebt_succ (treeList ! h) l
else let sc = vebt_succ summary h in
if sc = None then None
else Some (2^(deg div 2)) *⇩o sc +⇩o vebt_mint (treeList ! the sc) )
else None))"
end
subsection ‹Lemmas for Term Decomposition›
context VEBT_internal begin
lemma succ_min: assumes "deg ≥ 2" and "(x::nat) < mi" shows
"vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some mi"
by (metis add_2_eq_Suc assms(1) assms(2) le_add_diff_inverse vebt_succ.simps(6))
lemma succ_greatereq_min: assumes "deg ≥ 2" and "(x::nat) ≥ mi" shows
"vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = (let l = low x (deg div 2); h = high x (deg div 2) in
if h < length treeList then
let maxlow = vebt_maxt (treeList ! h) in
(if maxlow ≠ None ∧ (Some l <⇩o maxlow) then
Some (2^(deg div 2)) *⇩o Some h +⇩o vebt_succ (treeList ! h) l
else let sc = vebt_succ summary h in
if sc = None then None
else Some (2^(deg div 2)) *⇩o sc +⇩o vebt_mint (treeList ! the sc) )
else None)"
by (smt (verit) add_numeral_left arith_simps(1) assms(1) assms(2) le_add_diff_inverse not_less numerals(1) plus_1_eq_Suc vebt_succ.simps(6))
lemma succ_list_to_short: assumes "deg ≥ 2" and "x ≥ mi" and " high x (deg div 2) ≥ length treeList" shows
"vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = None"
using assms(1) assms(2) assms(3) succ_greatereq_min by auto
lemma succ_less_length_list: assumes "deg ≥ 2" and "x ≥ mi" and " high x (deg div 2) < length treeList" shows
"vebt_succ (Node (Some (mi, ma)) deg treeList summary) x =
(let l = low x (deg div 2); h = high x (deg div 2) ; maxlow = vebt_maxt (treeList ! h) in
(if maxlow ≠ None ∧ (Some l <⇩o maxlow) then
Some (2^(deg div 2)) *⇩o Some h +⇩o vebt_succ (treeList ! h) l
else let sc = vebt_succ summary h in
if sc = None then None
else Some (2^(deg div 2)) *⇩o sc +⇩o vebt_mint (treeList !the sc)))"
by (simp add: assms(1) assms(2) assms(3) succ_greatereq_min)
subsection ‹Correctness Proof›
theorem succ_corr: "invar_vebt t n ⟹ vebt_succ t x = Some sx == is_succ_in_set (set_vebt' t) x sx"
proof(induction t n arbitrary: x sx rule: invar_vebt.induct)
case (1 a b)
then show ?case proof(cases x)
case 0
then show ?thesis
by (simp add: succ_member)
next
case (Suc nat)
then show ?thesis proof(cases nat)
case 0
then show ?thesis
by (simp add: Suc succ_member)
next
case (Suc nat)
then show ?thesis by (metis (no_types) VEBT_Member.vebt_member.simps(1) Suc_eq_plus1 add_cancel_right_left le_add2 le_imp_less_Suc not_add_less2 not_less0 old.nat.exhaust option.distinct(1) option.simps(1) vebt_succ.simps(1) vebt_succ.simps(2) succ_member)
qed
qed
next
case (2 treeList n summary m deg)
then show ?case
by (simp add: succ_member)
next
case (3 treeList n summary m deg)
then show ?case
by (simp add: succ_member)
next
case (4 treeList n summary m deg mi ma)
hence "n = m" and "n ≥ 1" and "deg ≥ 2" and "deg = n + m"
apply blast+
using "4.hyps"(2) "4.hyps"(5) Suc_le_eq deg_not_0 apply auto[1]
using "4.hyps"(2) "4.hyps"(5) "4.hyps"(6) deg_not_0 apply fastforce
by (simp add: "4.hyps"(6))
hence "deg div 2 =n" and "length treeList = 2^n"
using add_self_div_2 apply blast by (simp add: "4.hyps"(4) "4.hyps"(5))
then show ?case proof(cases "x < mi")
case True
hence 0: "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some mi"
by (simp add: ‹2 ≤ deg› succ_min)
have 1:"mi = the (vebt_mint (Node (Some (mi, ma)) deg treeList summary))" by simp
hence "mi ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary)"
by (metis VEBT_Member.vebt_member.simps(5) ‹2 ≤ deg› add_numeral_left arith_simps(1) le_add_diff_inverse mem_Collect_eq numerals(1) plus_1_eq_Suc set_vebt'_def)
hence 2:"y ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary) ⟹ y ≥ x" for y
using "4.hyps"(9) True member_inv set_vebt'_def by fastforce
hence 3: "y ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary) ⟹ (y > mi ⟹ y ≥ x)" for y by blast
hence 4: "∀ y ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary). y > mi ⟶ y ≥ x" by blast
hence "is_succ_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x mi"
by (metis (mono_tags, lifting) "4.hyps"(9) True ‹mi ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary)› eq_iff less_imp_le_nat mem_Collect_eq member_inv succ_member set_vebt'_def)
then show ?thesis using 0
by (metis is_succ_in_set_def antisym_conv option.inject)
next
case False
hence "x ≥ mi"by simp
then show ?thesis
proof(cases "high x (deg div 2)< length treeList ")
case True
hence "high x n < 2^n ∧ low x n < 2^n"
by (simp add: ‹deg div 2 = n› ‹length treeList = 2 ^ n› low_def)
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
let ?maxlow = "vebt_maxt (treeList ! ?h)"
let ?sc = "vebt_succ summary ?h"
have 1:"vebt_succ (Node (Some (mi, ma)) deg treeList summary) x =
(if ?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow) then
Some (2^(deg div 2)) *⇩o Some ?h +⇩o vebt_succ (treeList ! ?h) ?l
else if ?sc = None then None
else Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList ! the ?sc))"
by (smt (verit) True ‹2 ≤ deg› ‹mi ≤ x› succ_less_length_list)
then show ?thesis
proof(cases "?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow)")
case True
then obtain maxl where 00:"Some maxl = ?maxlow ∧ ?l < maxl" by auto
have 01:"invar_vebt ((treeList ! ?h)) n ∧ (treeList ! ?h) ∈ set treeList "
by (simp add: "4.hyps"(1) ‹deg div 2 = n› ‹high x n < 2 ^ n ∧ low x n < 2 ^ n› ‹length treeList = 2 ^ n›)
have 02:"vebt_member ((treeList ! ?h)) maxl"
using "00" "01" maxt_member by auto
hence 03: "∃ y. y > ?l ∧ vebt_member ((treeList ! ?h)) y"
using "00" by blast
hence afinite: "finite (set_vebt' (treeList ! ?h)) "
using "01" set_vebt_finite by blast
then obtain succy where 04:"is_succ_in_set (set_vebt' (treeList ! ?h)) ?l succy"
using "00" "01" maxt_corr obtain_set_succ by fastforce
hence 05:"Some succy = vebt_succ (treeList ! ?h) ?l" using 4(1) 01 by force
hence "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some (2^(deg div 2)* ?h + succy) "
by (metis "1" True add_def mul_def option_shift.simps(3))
hence 06: "succy ∈ set_vebt' (treeList ! ?h)"
using "04" is_succ_in_set_def by blast
hence 07: "succy < 2^(deg div 2) ∧ ?h < 2^(deg div 2) ∧ deg div 2 + deg div 2 = deg"
using "01" "04" "4.hyps"(5) "4.hyps"(6) ‹high x n < 2 ^ n ∧ low x n < 2 ^ n› member_bound succ_member by auto
let ?y = "2^(deg div 2)* ?h + succy"
have 08: "vebt_member (treeList ! ?h) succy"
using "06" set_vebt'_def by auto
hence 09: "both_member_options (treeList ! ?h) succy"
using "01" both_member_options_equiv_member by blast
have 10: "high ?y (deg div 2) = ?h ∧ low ?y (deg div 2) = succy"
by (simp add: "07" high_inv low_inv mult.commute)
hence 11: "naive_member (treeList ! ?h) succy
⟹ naive_member (Node (Some (mi, ma)) deg treeList summary) ?y"
using naive_member.simps(3)[of "Some (mi, ma)" "deg-1" treeList summary ?y]
by (metis "07" "4.hyps"(4) "4.hyps"(5) One_nat_def Suc_pred ‹2 ≤ deg› ‹deg div 2 = n› add_gr_0 div_greater_zero_iff zero_less_numeral)
have 12: "?y ≥ mi ∧ ?y ≤ ma"
by (metis "01" "07" "09" "10" "4.hyps"(11) "4.hyps"(5) "4.hyps"(8) ‹deg div 2 = n› less_imp_le_nat)
hence 13: "membermima (treeList ! ?h) succy
⟹ membermima (Node (Some (mi, ma)) deg treeList summary) ?y"
using membermima.simps(4)[of mi ma "deg -1" treeList summary ?y]
apply(cases "?y = mi ∨ ?y = ma")
apply (metis "07" One_nat_def Suc_pred ‹2 ≤ deg› add_gr_0 div_greater_zero_iff zero_less_numeral)
by (metis "07" "10" "4.hyps"(4) "4.hyps"(5) One_nat_def Suc_pred ‹2 ≤ deg› ‹deg div 2 = n› add_gr_0 div_greater_zero_iff zero_less_numeral)
hence 14:"both_member_options (Node (Some (mi, ma)) deg treeList summary) ?y"
using "09" "11" both_member_options_def by blast
have 15: "vebt_member (Node (Some (mi, ma)) deg treeList summary) ?y"
proof (rule valid_member_both_member_options[OF _ 14])
show "invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg"
using "4.hyps" ‹length treeList = 2 ^ n› invar_vebt.intros(4) by auto
qed
have 16: "Some ?y = vebt_succ (Node (Some (mi, ma)) deg treeList summary) x"
by (simp add: ‹vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some (2 ^ (deg div 2) * high x (deg div 2) + succy)›)
have 17: "x = ?h * 2^(deg div 2) + ?l"
using bit_concat_def bit_split_inv by auto
have 18: "?y - x = ?h * 2^(deg div 2) + succy - ?h * 2^(deg div 2) - ?l "
by (metis "17" diff_diff_add mult.commute)
hence "?y -x > 0"
using "04" is_succ_in_set_def by auto
hence 19: "?y > x"
using zero_less_diff by blast
have 20: "z > x ⟹ vebt_member (Node (Some (mi, ma)) deg treeList summary) z ⟹ z≥ ?y " for z
proof-
assume "z > x" and "vebt_member (Node (Some (mi, ma)) deg treeList summary) z"
hence "high z (deg div 2) ≥ high x (deg div 2)"
by (simp add: div_le_mono high_def)
then show ?thesis proof(cases "high z (deg div 2) = high x (deg div 2)")
case True
hence "vebt_member (treeList ! ?h) (low z (deg div 2))"
using vebt_member.simps(5)[of mi ma "deg-2" treeList summary z]
by (metis "01" "07" "4.hyps"(11) "4.hyps"(5) False ‹deg div 2 = n› ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z› ‹x < z› both_member_options_equiv_member member_inv)
hence "succy ≤ low z (deg div 2)" using 04 unfolding is_succ_in_set_def
by (metis True ‹x < z› add_diff_cancel_left' bit_concat_def bit_split_inv diff_diff_left mem_Collect_eq set_vebt'_def zero_less_diff)
hence "?y ≤ z"
by (metis True add_le_cancel_left bit_concat_def bit_split_inv mult.commute)
then show ?thesis by blast
next
case False
hence "high z (deg div 2) > high ?y (deg div 2)"
using "10" ‹high x (deg div 2) ≤ high z (deg div 2)› by linarith
then show ?thesis
by (metis div_le_mono high_def nat_le_linear not_le)
qed
qed
hence "is_succ_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x ?y"
by (simp add: "15" "19" succ_member)
then show ?thesis using 16
by (metis eq_iff option.inject succ_member)
next
case False
hence i1:"?maxlow = None ∨ ¬ (Some ?l <⇩o ?maxlow)" by simp
hence 2: "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = (if ?sc = None then None
else Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList ! the ?sc))"
using "1" by auto
have " invar_vebt (treeList ! ?h) n"
using "4"(1) True by simp
hence 33:"∄ u. vebt_member (treeList ! ?h) u ∧ u > ?l"
proof(cases "?maxlow = None")
case True
then show ?thesis using maxt_corr_help_empty[of "treeList ! ?h" n]
by (simp add: ‹invar_vebt (treeList ! high x (deg div 2)) n› set_vebt'_def)
next
case False
obtain maxilow where "?maxlow =Some maxilow"
using False by blast
hence "maxilow ≤ ?l"
using "i1" by auto
then show ?thesis
by (meson ‹vebt_maxt (treeList ! high x (deg div 2)) = Some maxilow› ‹invar_vebt (treeList ! high x (deg div 2)) n› le_imp_less_Suc le_less_trans maxt_corr_help not_less_eq)
qed
then show ?thesis
proof(cases " ?sc = None")
case True
hence "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = None"
by (simp add: "2")
hence "∄ i. is_succ_in_set (set_vebt' summary) ?h i"
using "4.hyps"(3) True by force
hence "∄ i. i > ?h ∧ vebt_member summary i " using succ_none_empty[of "set_vebt' summary" ?h]
proof -
{ fix nn :: nat
have "∀n. ((is_succ_in_set (Collect (vebt_member summary)) (high x (deg div 2)) esk1_0 ∨ infinite (Collect (vebt_member summary))) ∨ n ∉ Collect (vebt_member summary)) ∨ ¬ high x (deg div 2) < n"
using ‹∄i. is_succ_in_set (set_vebt' summary) (high x (deg div 2)) i› succ_none_empty set_vebt'_def by auto
then have "¬ high x (deg div 2) < nn ∨ ¬ vebt_member summary nn"
using "4.hyps"(2) ‹∄i. is_succ_in_set (set_vebt' summary) (high x (deg div 2)) i› set_vebt'_def set_vebt_finite by auto }
then show ?thesis
by blast
qed
hence "(i > x ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i) ⟹ False" for i
proof-
fix i
assume "i > x ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i"
hence 20: "i = mi ∨ i = ma ∨ (high i (deg div 2) < length treeList
∧ vebt_member ( treeList ! (high i (deg div 2))) (low i (deg div 2)))" using
vebt_member.simps(5)[of mi ma "deg-2" treeList summary i]
using member_inv by blast
have "i ≠ mi"
using ‹mi ≤ x› ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› not_le by blast
hence "mi ≠ ma"
using ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› member_inv not_less_iff_gr_or_eq by blast
hence "i < 2^deg"
using "4.hyps"(10) ‹i ≠ mi› ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› member_inv by fastforce
hence aa:"i = ma ⟹ both_member_options( treeList ! (high i (deg div 2))) (low i (deg div 2))"
using "4.hyps"(11) "4.hyps"(2) "4.hyps"(5) "4.hyps"(6) ‹mi ≠ ma› deg_not_0 exp_split_high_low(1) by auto
hence abc:"invar_vebt (treeList ! (high i (deg div 2))) n"
using "4.hyps"(1) "4.hyps"(2) "4.hyps"(5) "4.hyps"(6) ‹deg div 2 = n› ‹i < 2 ^ deg›
‹length treeList = 2 ^ n› deg_not_0 exp_split_high_low(1) by simp
hence abd:"i = ma ⟹ vebt_member( treeList ! (high i (deg div 2))) (low i (deg div 2))"
using aa valid_member_both_member_options by blast
hence abe:"vebt_member( treeList ! (high i (deg div 2))) (low i (deg div 2))"
using "20" ‹i ≠ mi› by blast
hence abf:"both_member_options( treeList ! (high i (deg div 2))) (low i (deg div 2))"
using ‹invar_vebt (treeList ! high i (deg div 2)) n› both_member_options_equiv_member by blast
hence abg:"both_member_options summary (high i (deg div 2))"
by (metis "20" "4.hyps"(10) "4.hyps"(2) "4.hyps"(4) "4.hyps"(6) "4.hyps"(7) ‹2 ≤ deg› ‹deg div 2 = n› ‹i ≠ mi› deg_not_0 div_greater_zero_iff exp_split_high_low(1) zero_less_numeral)
hence abh:"vebt_member summary (high i (deg div 2))"
using "4.hyps"(2) valid_member_both_member_options by blast
have aaa:"(high i (deg div 2)) = (high x (deg div 2)) ⟹ vebt_member (treeList ! ?h) (low i (deg div 2))"
using ‹vebt_member (treeList ! high i (deg div 2)) (low i (deg div 2))› by auto
have abi:"(high i (deg div 2)) = (high x (deg div 2)) ⟹ low i (deg div 2) > ?l"
by (metis ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› add_le_cancel_left bit_concat_def bit_split_inv le_neq_implies_less less_imp_le_nat nat_neq_iff)
hence abj:"(high i (deg div 2)) = (high x (deg div 2)) ⟹ False" using 33 aaa by blast
hence abk:" (high i (deg div 2)) ∈ (set_vebt' summary) ∧ (high i (deg div 2)) > (high x (deg div 2)) "
by (metis (full_types) ‹vebt_member summary (high i (deg div 2))› ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› div_le_mono high_def le_less mem_Collect_eq set_vebt'_def)
then show ?thesis
using ‹¬ (∃i>high x (deg div 2). vebt_member summary i)› abh by blast
qed
then show ?thesis
using ‹vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = None› succ_member by auto
next
case False
hence "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x =
Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList ! the ?sc)"
by (simp add: False "2")
obtain sc where "?sc = Some sc"
using False by blast
hence "is_succ_in_set (set_vebt' summary) ?h sc"
using "4.hyps"(3) by blast
hence "vebt_member summary sc"
using succ_member by blast
hence "both_member_options summary sc"
using "4.hyps"(2) both_member_options_equiv_member by auto
hence "sc < 2^m"
using "4.hyps"(2) ‹vebt_member summary sc› member_bound by blast
hence "∃ miny. both_member_options (treeList ! sc) miny"
using "4.hyps"(7) ‹both_member_options summary sc› by blast
hence fgh:"set_vebt' (treeList ! sc) ≠ {}"
by (metis "4.hyps"(1) "4.hyps"(4) "4.hyps"(5) Collect_empty_eq_bot ‹deg div 2 = n› ‹sc < 2 ^ m› bot_empty_eq empty_iff nth_mem set_vebt'_def valid_member_both_member_options)
hence "invar_vebt (treeList ! the ?sc) n"
by (simp add: "4.hyps"(1) "4.hyps"(4) ‹sc < 2 ^ m› ‹vebt_succ summary (high x (deg div 2)) = Some sc›)
then obtain miny where "Some miny = vebt_mint (treeList ! sc)"
by (metis fgh Collect_empty_eq VEBT_Member.vebt_member.simps(2) vebt_buildup.simps(2) buildup_gives_empty vebt_mint.elims set_vebt'_def)
hence "Some miny = vebt_mint (treeList ! the ?sc)"
by (simp add: ‹vebt_succ summary (high x (deg div 2)) = Some sc›)
hence "min_in_set (set_vebt' (treeList ! the ?sc)) miny"
using ‹invar_vebt (treeList ! the (vebt_succ summary (high x (deg div 2)))) n› mint_corr by auto
hence scmem:"vebt_member (treeList ! the ?sc) miny"
using ‹Some miny = vebt_mint (treeList ! the (vebt_succ summary (high x (deg div 2))))› ‹invar_vebt (treeList ! the(vebt_succ summary (high x (deg div 2)))) n› mint_member by auto
let ?res = "Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList !the ?sc)"
obtain res where "res = the ?res" by blast
hence "res = 2^(deg div 2) * sc + miny"
by (metis ‹Some miny = vebt_mint (treeList ! the (vebt_succ summary (high x (deg div 2))))› ‹vebt_succ summary (high x (deg div 2)) = Some sc› add_def mul_def option.sel option_shift.simps(3))
have "high res (deg div 2) = sc"
by (metis ‹deg div 2 = n› ‹res = 2 ^ (deg div 2) * sc + miny› ‹invar_vebt (treeList ! the ?sc) n› high_inv member_bound mult.commute scmem)
hence "res > x"
by (metis is_succ_in_set_def ‹is_succ_in_set (set_vebt' summary) (high x (deg div 2)) sc› div_le_mono high_def not_le)
hence "res > mi"
using ‹mi ≤ x› le_less_trans by blast
hence "res ≤ ma"
proof(cases "high res n < high ma n")
case True
then show ?thesis
by (metis div_le_mono high_def leD nat_le_linear)
next
case False
hence "mi ≠ ma"
by (metis "4.hyps"(5) "4.hyps"(8) ‹∃miny. both_member_options (treeList ! sc) miny› ‹length treeList = 2 ^ n› ‹sc < 2 ^ m› nth_mem)
have "high res n < 2^m"
using ‹deg div 2 = n› ‹high res (deg div 2) = sc› ‹sc < 2 ^ m› by blast
hence " (∀x. high x n = high res n ∧ both_member_options (treeList ! (high res n)) (low x n) ⟶ mi < x ∧ x ≤ ma)" using 4(11)
using ‹mi ≠ ma› by blast
have "high res n = high res n ∧ both_member_options (treeList ! (high res n)) (low res n)"
by (metis ‹deg div 2 = n› ‹high res (deg div 2) = sc› ‹res = 2 ^ (deg div 2) * sc + miny› ‹vebt_succ summary (high x (deg div 2)) = Some sc› ‹invar_vebt (treeList ! the (vebt_succ summary (high x (deg div 2)))) n› both_member_options_equiv_member low_inv member_bound mult.commute option.sel scmem)
then show ?thesis
using ‹∀x. high x n = high res n ∧ both_member_options (treeList ! high res n) (low x n) ⟶ mi < x ∧ x ≤ ma› by blast
qed
hence "vebt_member (Node (Some (mi, ma)) deg treeList summary) (the ?res)" using vebt_member.simps(5)[of mi ma "deg-2" treeList summary res]
by (metis "4.hyps"(4) ‹2 ≤ deg› ‹deg div 2 = n› ‹high res (deg div 2) = sc› ‹mi < res› ‹res = 2 ^ (deg div 2) * sc + miny› ‹res = the (Some (2 ^ (deg div 2)) *⇩o vebt_succ summary (high x (deg div 2)) +⇩o vebt_mint (treeList ! the (vebt_succ summary (high x (deg div 2)))))› ‹sc < 2 ^ m› ‹vebt_succ summary (high x (deg div 2)) = Some sc› ‹invar_vebt (treeList ! the (vebt_succ summary (high x (deg div 2)))) n› add_2_eq_Suc leD le_add_diff_inverse low_inv member_bound mult.commute not_less_iff_gr_or_eq option.sel scmem)
have "(vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z > x) ⟹ z ≥ res" for z
proof-
fix z
assume "vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z > x"
hence 20: "z = mi ∨ z = ma ∨ (high z (deg div 2) < length treeList
∧ vebt_member ( treeList ! (high z (deg div 2))) (low z (deg div 2)))" using
vebt_member.simps(5)[of mi ma "deg-2" treeList summary z]
using member_inv by blast
have "z ≠ mi"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ x < z› ‹mi ≤ x› not_le by blast
hence "mi ≠ ma"
using ‹mi < res› ‹res ≤ ma› not_le by blast
hence "z < 2^deg"
using "4.hyps"(10) ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ x < z› ‹z ≠ mi› member_inv by fastforce
hence aa:"z = ma ⟹ both_member_options( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using "4.hyps"(11) "4.hyps"(2) "4.hyps"(5) "4.hyps"(6) ‹mi ≠ ma› deg_not_0 exp_split_high_low(1) by auto
hence abc:"invar_vebt (treeList ! (high z (deg div 2))) n"
using "4.hyps"(1) "4.hyps"(2) "4.hyps"(5) "4.hyps"(6) ‹deg div 2 = n› ‹z < 2 ^ deg› ‹length treeList = 2 ^ n› deg_not_0 exp_split_high_low(1) by simp
hence abd:"z = ma ⟹ vebt_member( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using aa valid_member_both_member_options by blast
hence abe:"vebt_member( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using "20" ‹z ≠ mi› by blast
hence abf:"both_member_options( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using ‹invar_vebt (treeList ! high z (deg div 2)) n› both_member_options_equiv_member by blast
hence abg:"both_member_options summary (high z (deg div 2))"
by (metis (full_types) "4.hyps"(5) "4.hyps"(6) "4.hyps"(7) ‹deg div 2 = n› ‹invar_vebt (treeList ! the (vebt_succ summary (high x (deg div 2)))) n› ‹z < 2 ^ deg› deg_not_0 exp_split_high_low(1))
hence abh:"vebt_member summary (high z (deg div 2))"
using "4.hyps"(2) valid_member_both_member_options by blast
have aaa:"(high z (deg div 2)) = (high x (deg div 2)) ⟹ vebt_member (treeList ! ?h) (low z (deg div 2))"
using abe by auto
have "high z(deg div 2)< sc ⟹ False"
proof-
assume "high z(deg div 2)< sc"
hence "vebt_member summary (high z(deg div 2))"
using abh by blast
have aaaa:"?h ≤ high z(deg div 2)"
by (simp add: ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ x < z› div_le_mono high_def less_imp_le_nat)
have bbbb:"?h ≥ high z(deg div 2)"
using ‹is_succ_in_set (set_vebt' summary) (high x (deg div 2)) sc› ‹high z (deg div 2) < sc› abh leD succ_member by auto
hence "?h = high z (deg div 2)"
using aaaa eq_iff by blast
hence "vebt_member (treeList ! ?h) (low z (deg div 2))"
using aaa by linarith
then show False
by (metis "33" ‹high x (deg div 2) = high z (deg div 2)› ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ x < z› add_diff_cancel_left' bit_concat_def bit_split_inv diff_diff_left zero_less_diff)
qed
hence "high z(deg div 2) ≥ sc"
using not_less by blast
then show " z ≥ res"
proof(cases "high z(deg div 2) = sc")
case True
hence "vebt_member (treeList ! (high z(deg div 2))) (low z (deg div 2))"
using abe by blast
have "low z (deg div 2) ≥ miny"
using True ‹min_in_set (set_vebt' (treeList ! the (vebt_succ summary (high x (deg div 2))))) miny› ‹vebt_succ summary (high x (deg div 2)) = Some sc› abe min_in_set_def set_vebt'_def by auto
hence "z ≥ res"
by (metis (full_types) True ‹res = 2 ^ (deg div 2) * sc + miny› add_le_cancel_left bit_concat_def bit_split_inv mult.commute)
then show ?thesis by simp
next
case False
hence "high z(deg div 2) > sc"
using ‹sc ≤ high z (deg div 2)› le_less by blast
then show ?thesis
by (metis ‹high res (deg div 2) = sc› div_le_mono high_def leD linear)
qed
qed
hence "is_succ_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x res"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) (the (Some (2 ^ (deg div 2)) *⇩o vebt_succ summary ?h +⇩o vebt_mint (treeList ! the (vebt_succ summary ?h))))›
‹res = the (Some (2 ^ (deg div 2)) *⇩o vebt_succ summary ?h +⇩o vebt_mint (treeList ! the (vebt_succ summary ?h)))› ‹x < res› succ_member by blast
moreover have "Some res = Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList ! the ?sc)"
by (metis ‹Some miny = vebt_mint (treeList !the (vebt_succ summary (high x (deg div 2))))› ‹res = 2 ^ (deg div 2) * sc + miny› ‹vebt_succ summary (high x (deg div 2)) = Some sc› add_def mul_def option_shift.simps(3))
ultimately show ?thesis
by (metis (mono_tags) is_succ_in_set_def ‹vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some (2 ^ (deg div 2)) *⇩o vebt_succ summary ?h +⇩o vebt_mint (treeList ! the (vebt_succ summary ?h))› eq_iff option.inject)
qed
qed
next
case False
hence 0:"vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = None"
by (simp add: ‹2 ≤ deg› ‹mi ≤ x› succ_greatereq_min)
have 1:"x ≥ 2^deg"
by (metis "4.hyps"(4) "4.hyps"(5) "4.hyps"(6) False ‹deg div 2 = n› high_def le_less_linear less_mult_imp_div_less mult_2 power2_eq_square power_even_eq)
hence "x ∉ set_vebt' (Node (Some (mi, ma)) deg treeList summary)"
using "4.hyps"(10) "4.hyps"(9) member_inv set_vebt'_def by fastforce
hence "∄ ss. is_succ_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x ss"
using "4.hyps"(10) 1 ‹mi ≤ x› member_inv succ_member by fastforce
then show ?thesis using 0 by auto
qed
qed
next
case (5 treeList n summary m deg mi ma)
hence "Suc n = m" and "deg = n + m" and "length treeList = 2^m ∧ invar_vebt summary m"
by blast +
hence "n ≥ 1"
using "5.hyps"(1) set_n_deg_not_0 by blast
hence "deg ≥ 2"
by (simp add: "5.hyps"(5) "5.hyps"(6))
hence "deg div 2 =n"
by (simp add: "5.hyps"(5) "5.hyps"(6))
then show ?case proof(cases "x < mi")
case True
hence 0: "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some mi"
by (simp add: ‹2 ≤ deg› succ_min)
have 1:"mi = the (vebt_mint (Node (Some (mi, ma)) deg treeList summary))" by simp
hence "mi ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary)"
by (metis VEBT_Member.vebt_member.simps(5) ‹2 ≤ deg› add_numeral_left arith_simps(1) le_add_diff_inverse mem_Collect_eq numerals(1) plus_1_eq_Suc set_vebt'_def)
hence 2:"y ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary) ⟹ y ≥ x" for y
using "5.hyps"(9) True member_inv set_vebt'_def by fastforce
hence 3: "y ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary) ⟹ (y > mi ⟹ y ≥ x)" for y by blast
hence 4: "∀ y ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary). y > mi ⟶ y ≥ x" by blast
hence "is_succ_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x mi"
by (metis (mono_tags, lifting) "5.hyps"(9) True ‹mi ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary)› eq_iff less_imp_le_nat mem_Collect_eq member_inv succ_member set_vebt'_def)
then show ?thesis using 0
by (metis is_succ_in_set_def antisym_conv option.inject)
next
case False
hence "x ≥ mi"by simp
then show ?thesis
proof(cases "high x (deg div 2)< length treeList ")
case True
hence "high x n < 2^m ∧ low x n < 2^n"
by (simp add: "5.hyps"(4) ‹deg div 2 = n› low_def)
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
let ?maxlow = "vebt_maxt (treeList ! ?h)"
let ?sc = "vebt_succ summary ?h"
have 1:"vebt_succ (Node (Some (mi, ma)) deg treeList summary) x =
(if ?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow) then
Some (2^(deg div 2)) *⇩o Some ?h +⇩o vebt_succ (treeList ! ?h) ?l
else if ?sc = None then None
else Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList ! the ?sc))"
by (smt (verit) True ‹2 ≤ deg› ‹mi ≤ x› succ_less_length_list)
then show ?thesis
proof(cases "?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow)")
case True
then obtain maxl where 00:"Some maxl = ?maxlow ∧ ?l < maxl" by auto
have 01:"invar_vebt ((treeList ! ?h)) n ∧ (treeList ! ?h) ∈ set treeList "
using "5.hyps"(1) "5.hyps"(4) ‹deg div 2 = n› ‹high x n < 2 ^ m ∧ low x n < 2 ^ n› by simp
have 02:"vebt_member ((treeList ! ?h)) maxl"
using "00" "01" maxt_member by auto
hence 03: "∃ y. y > ?l ∧ vebt_member ((treeList ! ?h)) y"
using "00" by blast
hence afinite: "finite (set_vebt' (treeList ! ?h)) "
using "01" set_vebt_finite by blast
then obtain succy where 04:"is_succ_in_set (set_vebt' (treeList ! ?h)) ?l succy"
using "00" "01" maxt_corr obtain_set_succ by fastforce
hence 05:"Some succy = vebt_succ (treeList ! ?h) ?l" using 5(1) 01 by force
hence "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some (2^(deg div 2)* ?h + succy) "
by (metis "1" True add_def mul_def option_shift.simps(3))
hence 06: "succy ∈ set_vebt' (treeList ! ?h)"
using "04" is_succ_in_set_def by blast
hence 07: "succy < 2^(deg div 2) ∧ ?h < 2^m ∧ Suc (deg div 2 + deg div 2 ) = deg"
using "01" "04" "5.hyps"(5) "5.hyps"(6) ‹high x n < 2 ^ m ∧ low x n < 2 ^ n› member_bound succ_member by auto
let ?y = "2^(deg div 2)* ?h + succy"
have 08: "vebt_member (treeList ! ?h) succy"
using "06" set_vebt'_def by auto
hence 09: "both_member_options (treeList ! ?h) succy"
using "01" both_member_options_equiv_member by blast
have 10: "high ?y (deg div 2) = ?h ∧ low ?y (deg div 2) = succy"
by (simp add: "07" high_inv low_inv mult.commute)
hence 11: "naive_member (treeList ! ?h) succy
⟹ naive_member (Node (Some (mi, ma)) deg treeList summary) ?y"
using naive_member.simps(3)[of "Some (mi, ma)" "deg-1" treeList summary ?y]
using "07" "5.hyps"(4) by auto
have 12: "?y ≥ mi ∧ ?y ≤ ma"
by (metis "01" "07" "09" "10" "5.hyps"(11) "5.hyps"(5) "5.hyps"(8) ‹deg div 2 = n› less_imp_le_nat)
hence 13: "membermima (treeList ! ?h) succy
⟹ membermima (Node (Some (mi, ma)) deg treeList summary) ?y"
using membermima.simps(4)[of mi ma "deg -1" treeList summary ?y]
apply(cases "?y = mi ∨ ?y = ma")
using "07" apply auto[1]
using "07" "10" "5.hyps"(4) by auto
hence 14:"both_member_options (Node (Some (mi, ma)) deg treeList summary) ?y"
using "09" "11" both_member_options_def by blast
have 15: "vebt_member (Node (Some (mi, ma)) deg treeList summary) ?y"
by (smt (verit) "07" "08" "10" "12" "5.hyps"(4) "5.hyps"(5) VEBT_Member.vebt_member.simps(5) One_nat_def Suc_1 Suc_le_eq Suc_pred ‹2 ≤ deg› ‹deg div 2 = n› add_gr_0 div_greater_zero_iff not_less zero_less_numeral)
have 16: "Some ?y = vebt_succ (Node (Some (mi, ma)) deg treeList summary) x"
by (simp add: ‹vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some (2 ^ (deg div 2) * high x (deg div 2) + succy)›)
have 17: "x = ?h * 2^(deg div 2) + ?l"
using bit_concat_def bit_split_inv by auto
have 18: "?y - x = ?h * 2^(deg div 2) + succy - ?h * 2^(deg div 2) - ?l "
by (metis "17" diff_diff_add mult.commute)
hence "?y -x > 0"
using "04" is_succ_in_set_def by auto
hence 19: "?y > x"
using zero_less_diff by blast
have 20: "z > x ⟹ vebt_member (Node (Some (mi, ma)) deg treeList summary) z ⟹ z≥ ?y " for z
proof-
assume "z > x" and "vebt_member (Node (Some (mi, ma)) deg treeList summary) z"
hence "high z (deg div 2) ≥ high x (deg div 2)"
by (simp add: div_le_mono high_def)
then show ?thesis
proof(cases "high z (deg div 2) = high x (deg div 2)")
case True
hence "vebt_member (treeList ! ?h) (low z (deg div 2))"
using vebt_member.simps(5)[of mi ma "deg-2" treeList summary z]
by (metis "01" "07" "5.hyps"(11) "5.hyps"(5) False ‹deg div 2 = n› ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z› ‹x < z› both_member_options_equiv_member member_inv)
hence "succy ≤ low z (deg div 2)" using 04 unfolding is_succ_in_set_def
by (metis True ‹x < z› add_diff_cancel_left' bit_concat_def bit_split_inv diff_diff_left mem_Collect_eq set_vebt'_def zero_less_diff)
hence "?y ≤ z"
by (metis "10" True bit_concat_def bit_split_inv nat_add_left_cancel_le)
then show ?thesis by blast
next
case False
hence "high z (deg div 2) > high ?y (deg div 2)"
using "10" ‹high x (deg div 2) ≤ high z (deg div 2)› by linarith
then show ?thesis
by (metis div_le_mono high_def nat_le_linear not_le)
qed
qed
hence "is_succ_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x ?y"
by (simp add: "15" "19" succ_member)
then show ?thesis using 16
by (metis eq_iff option.inject succ_member)
next
case False
hence i1:"?maxlow = None ∨ ¬ (Some ?l <⇩o ?maxlow)" by simp
hence 2: "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = (if ?sc = None then None
else Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList ! the ?sc))"
using "1" by auto
have " invar_vebt (treeList ! ?h) n"
using "5"(1) True by simp
hence 33:"∄ u. vebt_member (treeList ! ?h) u ∧ u > ?l"
proof(cases "?maxlow = None")
case True
then show ?thesis using maxt_corr_help_empty[of "treeList ! ?h" n]
by (simp add: ‹invar_vebt (treeList ! high x (deg div 2)) n› set_vebt'_def)
next
case False
obtain maxilow where "?maxlow =Some maxilow"
using False by blast
hence "maxilow ≤ ?l"
using "i1" by auto
then show ?thesis
by (meson ‹vebt_maxt (treeList ! high x (deg div 2)) = Some maxilow› ‹invar_vebt (treeList ! high x (deg div 2)) n› le_imp_less_Suc le_less_trans maxt_corr_help not_less_eq)
qed
then show ?thesis
proof(cases " ?sc = None")
case True
hence "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = None"
by (simp add: "2")
hence "∄ i. is_succ_in_set (set_vebt' summary) ?h i"
using "5.hyps"(3) True by force
hence "∄ i. i > ?h ∧ vebt_member summary i " using succ_none_empty[of "set_vebt' summary" ?h]
proof -
{ fix nn :: nat
have "∀n. ((is_succ_in_set (Collect (vebt_member summary)) (high x (deg div 2)) esk1_0 ∨ infinite (Collect (vebt_member summary))) ∨ n ∉ Collect (vebt_member summary)) ∨ ¬ high x (deg div 2) < n"
using ‹∄i. is_succ_in_set (set_vebt' summary) (high x (deg div 2)) i› succ_none_empty set_vebt'_def by auto
then have "¬ high x (deg div 2) < nn ∨ ¬ vebt_member summary nn"
using "5.hyps"(2) ‹∄i. is_succ_in_set (set_vebt' summary) (high x (deg div 2)) i› set_vebt'_def set_vebt_finite by auto }
then show ?thesis
by blast
qed
hence "(i > x ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i) ⟹ False" for i
proof-
fix i
assume "i > x ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i"
hence 20: "i = mi ∨ i = ma ∨ (high i (deg div 2) < length treeList
∧ vebt_member ( treeList ! (high i (deg div 2))) (low i (deg div 2)))" using
vebt_member.simps(5)[of mi ma "deg-2" treeList summary i]
using member_inv by blast
have "i ≠ mi"
using ‹mi ≤ x› ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› not_le by blast
hence "mi ≠ ma"
using ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› member_inv not_less_iff_gr_or_eq by blast
hence "i < 2^deg"
using "5.hyps"(10) ‹i ≠ mi› ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› member_inv by fastforce
hence aa:"i = ma ⟹ both_member_options( treeList ! (high i (deg div 2))) (low i (deg div 2))"
using "5.hyps"(11) "5.hyps"(2) "5.hyps"(6) ‹deg div 2 = n› ‹i ≠ mi› ‹invar_vebt (treeList ! high x (deg div 2)) n› deg_not_0 exp_split_high_low(1) by auto
hence abc:"invar_vebt (treeList ! (high i (deg div 2))) n"
using "5.hyps"(1) "5.hyps"(4) "5.hyps"(5) "5.hyps"(6)
‹deg div 2 = n› ‹i < 2 ^ deg› ‹invar_vebt (treeList ! high x (deg div 2)) n›
exp_split_high_low(1) [of i n ‹Suc n›] deg_not_0 by auto
hence abd:"i = ma ⟹ vebt_member( treeList ! (high i (deg div 2))) (low i (deg div 2))"
using aa valid_member_both_member_options by blast
hence abe:"vebt_member( treeList ! (high i (deg div 2))) (low i (deg div 2))"
using "20" ‹i ≠ mi› by blast
hence abf:"both_member_options( treeList ! (high i (deg div 2))) (low i (deg div 2))"
using ‹invar_vebt (treeList ! high i (deg div 2)) n› both_member_options_equiv_member by blast
hence abg:"both_member_options summary (high i (deg div 2))"
by (metis (full_types) "5.hyps"(5) "5.hyps"(6) "5.hyps"(7) ‹deg div 2 = n› ‹i < 2 ^ deg› abc deg_not_0 exp_split_high_low(1) zero_less_Suc)
hence abh:"vebt_member summary (high i (deg div 2))"
using "5.hyps"(2) valid_member_both_member_options by blast
have aaa:"(high i (deg div 2)) = (high x (deg div 2)) ⟹ vebt_member (treeList ! ?h) (low i (deg div 2))"
using ‹vebt_member (treeList ! high i (deg div 2)) (low i (deg div 2))› by auto
have abi:"(high i (deg div 2)) = (high x (deg div 2)) ⟹ low i (deg div 2) > ?l"
by (metis ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› add_le_cancel_left bit_concat_def bit_split_inv le_neq_implies_less less_imp_le_nat nat_neq_iff)
hence abj:"(high i (deg div 2)) = (high x (deg div 2)) ⟹ False" using 33 aaa by blast
hence abk:" (high i (deg div 2)) ∈ (set_vebt' summary) ∧ (high i (deg div 2)) > (high x (deg div 2)) "
by (metis (full_types) ‹vebt_member summary (high i (deg div 2))› ‹x < i ∧ vebt_member (Node (Some (mi, ma)) deg treeList summary) i› div_le_mono high_def le_less mem_Collect_eq set_vebt'_def)
then show ?thesis
using ‹¬ (∃i>high x (deg div 2). vebt_member summary i)› abh by blast
qed
then show ?thesis
using ‹vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = None› succ_member by auto
next
case False
hence "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x =
Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList ! the ?sc)"
by (simp add: False "2")
obtain sc where "?sc = Some sc"
using False by blast
hence "is_succ_in_set (set_vebt' summary) ?h sc"
using "5.hyps"(3) by blast
hence "vebt_member summary sc"
using succ_member by blast
hence "both_member_options summary sc"
using "5.hyps"(2) both_member_options_equiv_member by auto
hence "sc < 2^m"
using "5.hyps"(2) ‹vebt_member summary sc› member_bound by blast
hence "∃ miny. both_member_options (treeList ! sc) miny"
using "5.hyps"(7) ‹both_member_options summary sc› by blast
hence fgh:"set_vebt' (treeList ! sc) ≠ {}"
using "5.hyps"(1) "5.hyps"(4) ‹sc < 2 ^ m› valid_member_both_member_options [of ‹treeList ! sc›]
by (auto simp add: set_vebt'_def) (metis in_set_conv_nth)
hence "invar_vebt (treeList ! the ?sc) n"
by (simp add: "5.hyps"(1) "5.hyps"(4) ‹sc < 2 ^ m› ‹vebt_succ summary (high x (deg div 2)) = Some sc›)
then obtain miny where "Some miny = vebt_mint (treeList ! sc)"
by (metis fgh Collect_empty_eq VEBT_Member.vebt_member.simps(2) vebt_buildup.simps(2) buildup_gives_empty vebt_mint.elims set_vebt'_def)
hence "Some miny = vebt_mint (treeList ! the ?sc)"
by (simp add: ‹vebt_succ summary (high x (deg div 2)) = Some sc›)
hence "min_in_set (set_vebt' (treeList ! the ?sc)) miny"
using ‹invar_vebt (treeList ! the (vebt_succ summary (high x (deg div 2)))) n› mint_corr by auto
hence scmem:"vebt_member (treeList ! the ?sc) miny"
using ‹Some miny = vebt_mint (treeList ! the (vebt_succ summary (high x (deg div 2))))›
‹invar_vebt (treeList ! the (vebt_succ summary (high x (deg div 2)))) n› mint_member by auto
let ?res = "Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList ! the ?sc)"
obtain res where "res = the ?res" by blast
hence "res = 2^(deg div 2) * sc + miny"
by (metis ‹Some miny = vebt_mint (treeList ! sc)› ‹vebt_succ summary (high x (deg div 2)) = Some sc› add_shift mul_shift option.sel)
have "high res (deg div 2) = sc"
by (metis ‹deg div 2 = n› ‹res = 2 ^ (deg div 2) * sc + miny› ‹invar_vebt (treeList ! the ?sc) n› high_inv member_bound mult.commute scmem)
hence "res > x"
by (metis is_succ_in_set_def ‹is_succ_in_set (set_vebt' summary) (high x (deg div 2)) sc› div_le_mono high_def not_le)
hence "res > mi"
using ‹mi ≤ x› le_less_trans by blast
hence "res ≤ ma"
proof(cases "high res n < high ma n")
case True
then show ?thesis
by (metis div_le_mono high_def leD nat_le_linear)
next
case False
hence "mi ≠ ma"
by (metis "5.hyps"(4) "5.hyps"(8) ‹∃miny. both_member_options (treeList ! sc) miny› ‹sc < 2 ^ m› nth_mem)
have "high res n < 2^m"
using ‹deg div 2 = n› ‹high res (deg div 2) = sc› ‹sc < 2 ^ m› by blast
hence " (∀x. high x n = high res n ∧ both_member_options (treeList ! (high res n)) (low x n) ⟶ mi < x ∧ x ≤ ma)" using 5(11)
using ‹mi ≠ ma› by blast
have "high res n = high res n ∧ both_member_options (treeList ! (high res n)) (low res n)"
by (metis ‹deg div 2 = n› ‹high res (deg div 2) = sc› ‹res = 2 ^ (deg div 2) * sc + miny› ‹vebt_succ summary (high x (deg div 2)) = Some sc› ‹invar_vebt (treeList ! the (vebt_succ summary (high x (deg div 2)))) n› both_member_options_equiv_member low_inv member_bound mult.commute option.sel scmem)
then show ?thesis
using ‹∀x. high x n = high res n ∧ both_member_options (treeList ! high res n) (low x n) ⟶ mi < x ∧ x ≤ ma› by blast
qed
hence "vebt_member (Node (Some (mi, ma)) deg treeList summary) (the ?res)" using vebt_member.simps(5)[of mi ma "deg-2" treeList summary res]
by (metis "5.hyps"(4) ‹2 ≤ deg› ‹deg div 2 = n› ‹high res (deg div 2) = sc› ‹mi < res› ‹res = 2 ^ (deg div 2) * sc + miny› ‹res = the (Some (2 ^ (deg div 2)) *⇩o vebt_succ summary (high x (deg div 2)) +⇩o vebt_mint (treeList ! the (vebt_succ summary (high x (deg div 2)))))› ‹sc < 2 ^ m› ‹vebt_succ summary (high x (deg div 2)) = Some sc› ‹invar_vebt (treeList ! the (vebt_succ summary (high x (deg div 2)))) n› add_2_eq_Suc' le_add_diff_inverse2 less_imp_le low_inv member_bound mult.commute not_less option.sel scmem)
have "(vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z > x) ⟹ z ≥ res" for z
proof-
fix z
assume "vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z > x"
hence 20: "z = mi ∨ z = ma ∨ (high z (deg div 2) < length treeList
∧ vebt_member ( treeList ! (high z (deg div 2))) (low z (deg div 2)))" using
vebt_member.simps(5)[of mi ma "deg-2" treeList summary z]
using member_inv by blast
have "z ≠ mi"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ x < z› ‹mi ≤ x› not_le by blast
hence "mi ≠ ma"
using ‹mi < res› ‹res ≤ ma› not_le by blast
hence "z < 2^deg"
using "5.hyps"(10) ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ x < z› ‹z ≠ mi› member_inv by fastforce
hence aa:"z = ma ⟹ both_member_options( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using "5.hyps"(11) "5.hyps"(2) "5.hyps"(6) ‹deg div 2 = n› ‹mi ≠ ma› ‹invar_vebt (treeList ! high x (deg div 2)) n› deg_not_0 exp_split_high_low(1) by auto
hence abc:"invar_vebt (treeList ! (high z (deg div 2))) n"
by (metis "20" "5.hyps"(1) "5.hyps"(10) "5.hyps"(4) "5.hyps"(5) "5.hyps"(6) ‹deg div 2 = n› ‹invar_vebt (treeList ! the(vebt_succ summary (high x (deg div 2)))) n› ‹z ≠ mi› deg_not_0 exp_split_high_low(1) nth_mem zero_less_Suc)
hence abd:"z = ma ⟹ vebt_member( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using aa valid_member_both_member_options by blast
hence abe:"vebt_member( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using "20" ‹z ≠ mi› by blast
hence abf:"both_member_options( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using ‹invar_vebt (treeList ! high z (deg div 2)) n› both_member_options_equiv_member by blast
hence abg:"both_member_options summary (high z (deg div 2))"
by (metis (full_types) "5.hyps"(5) "5.hyps"(6) "5.hyps"(7) ‹deg div 2 = n› ‹invar_vebt (treeList ! the (vebt_succ summary (high x (deg div 2)))) n› ‹z < 2 ^ deg› deg_not_0 exp_split_high_low(1) zero_less_Suc)
hence abh:"vebt_member summary (high z (deg div 2))"
using "5.hyps"(2) valid_member_both_member_options by blast
have aaa:"(high z (deg div 2)) = (high x (deg div 2)) ⟹ vebt_member (treeList ! ?h) (low z (deg div 2))"
using abe by auto
have "high z(deg div 2)< sc ⟹ False"
proof-
assume "high z(deg div 2)< sc"
hence "vebt_member summary (high z(deg div 2))"
using abh by blast
have aaaa:"?h ≤ high z(deg div 2)"
by (simp add: ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ x < z› div_le_mono high_def less_imp_le_nat)
have bbbb:"?h ≥ high z(deg div 2)"
using ‹is_succ_in_set (set_vebt' summary) (high x (deg div 2)) sc› ‹high z (deg div 2) < sc› abh leD succ_member by auto
hence "?h = high z (deg div 2)"
using aaaa eq_iff by blast
hence "vebt_member (treeList ! ?h) (low z (deg div 2))"
using aaa by linarith
then show False
by (metis "33" ‹high x (deg div 2) = high z (deg div 2)› ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ x < z› add_diff_cancel_left' bit_concat_def bit_split_inv diff_diff_left zero_less_diff)
qed
hence "high z(deg div 2) ≥ sc"
using not_less by blast
then show " z ≥ res"
proof(cases "high z(deg div 2) = sc")
case True
hence "vebt_member (treeList ! (high z(deg div 2))) (low z (deg div 2))"
using abe by blast
have "low z (deg div 2) ≥ miny"
using True ‹min_in_set (set_vebt' (treeList ! the (vebt_succ summary (high x (deg div 2))))) miny› ‹vebt_succ summary (high x (deg div 2)) = Some sc› abe min_in_set_def set_vebt'_def by auto
hence "z ≥ res"
by (metis (full_types) True ‹res = 2 ^ (deg div 2) * sc + miny› add_le_cancel_left bit_concat_def bit_split_inv mult.commute)
then show ?thesis by simp
next
case False
hence "high z(deg div 2) > sc"
using ‹sc ≤ high z (deg div 2)› le_less by blast
then show ?thesis
by (metis ‹high res (deg div 2) = sc› div_le_mono high_def leD linear)
qed
qed
hence "is_succ_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x res"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) (the (Some (2 ^ (deg div 2)) *⇩o vebt_succ summary ?h +⇩o vebt_mint (treeList ! the (vebt_succ summary ?h))))›
‹res = the (Some (2 ^ (deg div 2)) *⇩o vebt_succ summary ?h +⇩o vebt_mint (treeList ! the (vebt_succ summary ?h)))› ‹x < res› succ_member by blast
moreover have "Some res = Some (2^(deg div 2)) *⇩o ?sc +⇩o vebt_mint (treeList ! the ?sc)"
by (metis ‹Some miny = vebt_mint (treeList ! the (vebt_succ summary (high x (deg div 2))))› ‹res = 2 ^ (deg div 2) * sc + miny› ‹vebt_succ summary (high x (deg div 2)) = Some sc› add_def mul_def option_shift.simps(3))
ultimately show ?thesis
by (metis (mono_tags) is_succ_in_set_def ‹vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some (2 ^ (deg div 2)) *⇩o vebt_succ summary ?h +⇩o vebt_mint (treeList ! the (vebt_succ summary ?h))› eq_iff option.inject)
qed
qed
next
case False
hence 0:"vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = None"
by (simp add: ‹2 ≤ deg› ‹mi ≤ x› succ_greatereq_min)
have 1:"x ≥ 2^deg"
by (metis "5.hyps"(4) "5.hyps"(5) "5.hyps"(6) False One_nat_def Suc_le_eq ‹1 ≤ n› ‹deg div 2 = n› exp_split_high_low(1) leI zero_less_Suc)
hence "x ∉ set_vebt' (Node (Some (mi, ma)) deg treeList summary)"
using "5.hyps"(10) "5.hyps"(9) member_inv set_vebt'_def by fastforce
hence "∄ ss. is_succ_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x ss"
using "5.hyps"(10) 1 ‹mi ≤ x› member_inv succ_member by fastforce
then show ?thesis using 0 by auto
qed
qed
qed
corollary succ_empty: assumes "invar_vebt t n "
shows " (vebt_succ t x = None) = ({y. vebt_member t y ∧ y > x} = {})"
proof
show " vebt_succ t x = None ⟹ {y. vebt_member t y ∧ x < y} = {}"
proof
show "vebt_succ t x = None ⟹ {y. vebt_member t y ∧ x < y} ⊆ {}"
proof-
assume "vebt_succ t x = None"
hence "∄ y. is_succ_in_set (set_vebt' t) x y"
using assms succ_corr by force
moreover hence "is_succ_in_set (set_vebt' t) x y ⟹ vebt_member t y ∧ x < y " for y by auto
ultimately show "{y. vebt_member t y ∧ x < y} ⊆ {}"
using assms succ_none_empty set_vebt'_def set_vebt_finite by auto
qed
show " vebt_succ t x = None ⟹ {} ⊆ {y. vebt_member t y ∧ x < y}" by simp
qed
show " {y. vebt_member t y ∧ x < y} = {} ⟹ vebt_succ t x = None"
proof-
assume "{y. vebt_member t y ∧ x < y} = {} "
hence "is_succ_in_set (set_vebt' t) x y ⟹ False" for y
using succ_member by auto
thus "vebt_succ t x = None"
by (meson assms not_Some_eq succ_corr)
qed
qed
theorem succ_correct: "invar_vebt t n ⟹ vebt_succ t x = Some sx ⟷is_succ_in_set (set_vebt t) x sx"
by (simp add: succ_corr set_vebt_set_vebt'_valid)
lemma "is_succ_in_set S x y ⟷ min_in_set {s . s ∈ S ∧ s > x} y"
using is_succ_in_set_def min_in_set_def by fastforce
lemma helpyd:"invar_vebt t n ⟹ vebt_succ t x = Some y ⟹ y < 2^n"
using member_bound succ_corr succ_member by blast
lemma geqmaxNone:
assumes "invar_vebt (Node (Some (mi, ma)) deg treeList summary) n ""x ≥ ma "
shows "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = None "
proof(rule ccontr)
assume "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x ≠ None"
then obtain y where "vebt_succ (Node (Some (mi, ma)) deg treeList summary) x = Some y" by auto
hence "y > ma ∧ y ∈ set_vebt' ((Node (Some (mi, ma)) deg treeList summary))"
by (smt (verit, ccfv_SIG) assms(1) assms(2) dual_order.strict_trans2 member_inv min_in_set_def vebt_mint.simps(3) mint_corr not_less_iff_gr_or_eq succ_corr succ_member)
then show False
by (metis assms(1) leD vebt_maxt.simps(3) maxt_corr_help mem_Collect_eq set_vebt'_def)
qed
end
end