Theory VEBT_Delete
theory VEBT_Delete imports VEBT_Pred VEBT_Succ
begin
section ‹Deletion›
subsection ‹Function Definition›
context begin
interpretation VEBT_internal .
fun vebt_delete :: "VEBT ⇒ nat ⇒ VEBT" where
"vebt_delete (Leaf a b) 0 = Leaf False b"|
"vebt_delete (Leaf a b) (Suc 0) = Leaf a False"|
"vebt_delete (Leaf a b) (Suc (Suc n)) = Leaf a b"|
"vebt_delete (Node None deg treeList summary) _ = (Node None deg treeList summary)"|
"vebt_delete (Node (Some (mi, ma)) 0 trLst smry) x = (Node (Some (mi, ma)) 0 trLst smry) "|
"vebt_delete (Node (Some (mi, ma)) (Suc 0) tr sm) x = (Node (Some (mi, ma)) (Suc 0) tr sm) "|
"vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(
if (x < mi ∨ x > ma) then (Node (Some (mi, ma)) deg treeList summary)
else if (x = mi ∧ x = ma) then (Node None deg treeList summary)
else let xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2)
+ the (vebt_mint (treeList ! the (vebt_mint summary)))
else x);
minn = (if x = mi then xn else mi);
l = low xn (deg div 2);
h = high xn (deg div 2) in
if h < length treeList
then(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in
if minNull newnode
then( let sn = vebt_delete summary h in(
Node (Some (minn, if xn = ma then
(let maxs = vebt_maxt sn in (
if maxs = None
then minn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))))
else ma)) deg newlist sn))
else (Node (Some (minn, (if xn = ma
then h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
else ma))) deg newlist summary ))
else (Node (Some (mi, ma)) deg treeList summary))"
end
subsection ‹Auxiliary Lemmas›
context VEBT_internal begin
context begin
lemma delt_out_of_range:
assumes "x < mi ∨ x > ma" and "deg ≥ 2"
shows
"vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(Node (Some (mi, ma)) deg treeList summary)"
using vebt_delete.simps(7)[of mi ma "deg-2" treeList summary x]
by (metis add_2_eq_Suc assms(1) assms(2) le_add_diff_inverse)
lemma del_single_cont:
assumes "x = mi ∧ x = ma" and "deg ≥ 2"
shows "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (Node None deg treeList summary)"
using vebt_delete.simps(7)[of mi ma "deg-2" treeList summary x]
by (metis add_2_eq_Suc assms(1) assms(2) le_add_diff_inverse nat_less_le)
lemma del_in_range:
assumes "x ≥ mi ∧ x ≤ ma" and "mi ≠ ma" and "deg ≥ 2"
shows
" vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ( let xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2)
+ the (vebt_mint (treeList ! the (vebt_mint summary)))
else x);
minn = (if x = mi then xn else mi);
l = low xn (deg div 2);
h = high xn (deg div 2) in
if h < length treeList
then(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode] in
if minNull newnode
then(
let sn = vebt_delete summary h in
(Node (Some (minn, if xn = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then minn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma))
deg newlist sn)
)else
(Node (Some (minn, (if xn = ma then
h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
else ma)))
deg newlist summary )
)else
(Node (Some (mi, ma)) deg treeList summary))"
using vebt_delete.simps(7)[of mi ma "deg-2" treeList summary x]
by (smt (z3) add_2_eq_Suc assms(1) assms(2) assms(3) leD le_add_diff_inverse)
lemma del_x_not_mia:
assumes "x > mi ∧ x ≤ ma" and "mi ≠ ma" and "deg ≥ 2" and "high x (deg div 2) = h" and
"low x (deg div 2) = l"and "high x (deg div 2) < length treeList"
shows
" vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode] in
if minNull newnode
then(
let sn = vebt_delete summary h in
(Node (Some (mi, if x = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then mi
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma))
deg newlist sn)
)else
(Node (Some (mi, (if x = ma then
h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
else ma)))
deg newlist summary )
)"
using del_in_range[of mi x ma deg treeList summary] unfolding Let_def
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) nat_less_le by fastforce
lemma del_x_not_mi:
assumes "x > mi ∧ x ≤ ma" and "mi ≠ ma" and "deg ≥ 2" and "high x (deg div 2) = h" and
"low x (deg div 2) = l"and " newnode = vebt_delete (treeList ! h) l"
and "newlist = treeList[h:= newnode]" and "high x (deg div 2) < length treeList"
shows
" vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (
if minNull newnode
then(
let sn = vebt_delete summary h in
(Node (Some (mi, if x = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then mi
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma))
deg newlist sn)
)else
(Node (Some (mi, (if x = ma then
h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
else ma)))
deg newlist summary )
)" using del_x_not_mia[of mi x ma deg h l treeList summary]
by (smt (z3) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8))
lemma del_x_not_mi_new_node_nil:
assumes "x > mi ∧ x ≤ ma" and "mi ≠ ma" and "deg ≥ 2" and "high x (deg div 2) = h" and
"low x (deg div 2) = l"and " newnode = vebt_delete (treeList ! h) l" and "minNull newnode " and
"sn = vebt_delete summary h" and "newlist =treeList[h:= newnode]" and "high x (deg div 2) < length treeList"
shows
" vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (Node (Some (mi, if x = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then mi
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma)) deg newlist sn)"
using del_x_not_mi[of mi x ma deg h l newnode treeList]
by (metis assms(1) assms(10) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9))
lemma del_x_not_mi_newnode_not_nil:
assumes "x > mi ∧ x ≤ ma" and "mi ≠ ma" and "deg ≥ 2" and "high x (deg div 2) = h" and
"low x (deg div 2) = l"and " newnode = vebt_delete (treeList ! h) l" and "¬ minNull newnode " and
"newlist = treeList[h:= newnode]" and"high x (deg div 2) < length treeList"
shows
" vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
(Node (Some (mi, (if x = ma then
h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
else ma)))
deg newlist summary )"
using del_x_not_mi[of mi x ma deg h l newnode treeList newlist summary]
using assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9) by auto
lemma del_x_mia: assumes "x = mi ∧ x < ma" and "mi ≠ ma" and "deg ≥ 2"
shows "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(
let xn = the (vebt_mint summary) * 2^(deg div 2)
+ the (vebt_mint (treeList ! the (vebt_mint summary)));
minn = xn;
l = low xn (deg div 2);
h = high xn (deg div 2) in
if h < length treeList
then(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in
if minNull newnode
then(
let sn = vebt_delete summary h in
(Node (Some (minn, if xn = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then minn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma))
deg newlist sn)
)else
(Node (Some (minn, (if xn = ma then
h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
else ma)))
deg newlist summary )
)else
(Node (Some (mi, ma)) deg treeList summary)
)"
using del_in_range[of mi x ma deg treeList summary]
using assms(1) assms(3) nat_less_le order_refl by fastforce
lemma del_x_mi:
assumes "x = mi ∧ x < ma" and "mi ≠ ma" and "deg ≥ 2" and "high xn (deg div 2) = h" and
"xn = the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) "
"low xn (deg div 2) = l"and "high xn (deg div 2) < length treeList"
shows
"vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in
if minNull newnode
then(
let sn = vebt_delete summary h in
(Node (Some (xn, if xn = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then xn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma))
deg newlist sn)
)else
(Node (Some (xn, (if xn = ma then
h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
else ma)))
deg newlist summary ))
"
using del_x_mia[of x mi ma deg treeList summary]
by (smt (z3) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7))
lemma del_x_mi_lets_in:
assumes "x = mi ∧ x < ma" and "mi ≠ ma" and "deg ≥ 2" and "high xn (deg div 2) = h" and
"xn = the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) "
"low xn (deg div 2) = l"and "high xn (deg div 2) < length treeList" and
" newnode = vebt_delete (treeList ! h) l" and " newlist = treeList[h:= newnode]"
shows "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =( if minNull newnode
then(
let sn = vebt_delete summary h in
(Node (Some (xn, if xn = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then xn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma))
deg newlist sn)
)else
(Node (Some (xn, (if xn = ma then
h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
else ma)))
deg newlist summary ))"
using del_x_mi[of x mi ma deg xn h summary treeList l]
by (smt (z3) assms(1) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9))
lemma del_x_mi_lets_in_minNull:
assumes "x = mi ∧ x < ma" and "mi ≠ ma" and "deg ≥ 2" and "high xn (deg div 2) = h" and
"xn = the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) "
"low xn (deg div 2) = l"and "high xn (deg div 2) < length treeList" and
"newnode = vebt_delete (treeList ! h) l" and " newlist =treeList[h:= newnode]" and
"minNull newnode " and " sn = vebt_delete summary h"
shows
"vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
(Node (Some (xn, if xn = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then xn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma)) deg newlist sn)"
using del_x_mi_lets_in[of x mi ma deg xn h summary treeList l newnode newlist]
by (metis assms(1) assms(10) assms(11) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9))
lemma del_x_mi_lets_in_not_minNull:
assumes "x = mi ∧ x < ma" and "mi ≠ ma" and "deg ≥ 2" and "high xn (deg div 2) = h" and
"xn = the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) "
"low xn (deg div 2) = l"and "high xn (deg div 2) < length treeList" and
" newnode = vebt_delete (treeList ! h) l" and " newlist = treeList[h:= newnode]" and
"¬minNull newnode "
shows
"vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
(Node (Some (xn, (if xn = ma then
h * 2^(deg div 2) + the( vebt_maxt (newlist ! h))
else ma)))
deg newlist summary )"
using del_x_mi_lets_in[of x mi ma deg xn h summary treeList l newnode newlist]
by (meson assms(1) assms(10) assms(2) assms(3) assms(4) assms(5) assms(6) assms(7) assms(8) assms(9))
theorem dele_bmo_cont_corr:"invar_vebt t n ⟹ (both_member_options (vebt_delete t x) y ⟷ x ≠ y ∧ both_member_options t y)"
proof(induction t n arbitrary: x y rule: invar_vebt.induct)
case (1 a b)
have "(both_member_options (vebt_delete (Leaf a b) x) y) ⟹ (x ≠ y ∧ both_member_options (Leaf a b) y)"
by (metis One_nat_def both_member_options_def vebt_buildup.cases vebt_delete.simps(1) vebt_delete.simps(2) vebt_delete.simps(3) membermima.simps(1) naive_member.simps(1))
moreover have "(x ≠ y ∧ both_member_options (Leaf a b) y) ⟹(both_member_options (vebt_delete (Leaf a b) x) y)"
by (metis One_nat_def both_member_options_def vebt_buildup.cases vebt_delete.simps(1) vebt_delete.simps(2) vebt_delete.simps(3) membermima.simps(1) naive_member.simps(1))
ultimately show ?case by blast
next
case (2 treeList n summary m deg)
hence "deg ≥ 2"
by (metis Suc_leI deg_not_0 dual_order.strict_trans2 less_add_same_cancel1 numerals(2))
hence " (vebt_delete (Node None deg treeList summary) x) = (Node None deg treeList summary)" by simp
moreover have "¬vebt_member (Node None deg treeList summary) y" by simp
moreover hence "¬both_member_options (Node None deg treeList summary) y"
using invar_vebt.intros(2)[of treeList n summary m deg] 2
by (metis valid_member_both_member_options)
moreover hence "¬both_member_options (vebt_delete (Node None deg treeList summary) x) y" by simp
ultimately show ?case
by force
next
case (3 treeList n summary m deg)
hence "deg ≥ 2"
by (metis One_nat_def add_mono le_add1 numeral_2_eq_2 plus_1_eq_Suc set_n_deg_not_0)
hence " (vebt_delete (Node None deg treeList summary) x) = (Node None deg treeList summary)" by simp
moreover have "¬vebt_member (Node None deg treeList summary) y" by simp
moreover hence "¬both_member_options (Node None deg treeList summary) y"
using invar_vebt.intros(3)[of treeList n summary m deg] 3
by (metis valid_member_both_member_options)
moreover hence "¬both_member_options (vebt_delete (Node None deg treeList summary) x) y" by simp
ultimately show ?case
by force
next
case (4 treeList n summary m deg mi ma)
hence tvalid: "invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg"
using invar_vebt.intros(4)[of treeList n summary m deg mi ma] by simp
hence "mi ≤ ma" and "deg div 2 = n" and "ma ≤ 2^deg" using 4
by (auto simp add: "4.hyps"(3) "4.hyps"(4))
hence dp:"deg ≥ 2"
using "4.hyps"(1) "4.hyps"(3) deg_not_0 div_greater_zero_iff by blast
then show ?case proof(cases "x <mi ∨ x > ma")
case True
hence "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (Node (Some (mi, ma)) deg treeList summary)"
using delt_out_of_range[of x mi ma deg treeList summary] ‹2 ≤ deg› by blast
then show ?thesis
by (metis "4.hyps"(7) True tvalid leD member_inv not_less_iff_gr_or_eq valid_member_both_member_options)
next
case False
hence "mi ≤ x ∧ x ≤ ma" by simp
hence "x < 2^deg"
using "4.hyps"(8) order.strict_trans1 by blast
then show ?thesis
proof(cases "x = mi ∧ x = ma")
case True
hence "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (Node None deg treeList summary)"
using del_single_cont[of x mi ma deg treeList summary] ‹2 ≤ deg› by blast
moreover hence "invar_vebt (Node None deg treeList summary) deg"
using "4"(4) "4.IH"(1) "4.hyps"(1) "4.hyps"(3) "4.hyps"(4) True mi_eq_ma_no_ch tvalid invar_vebt.intros(2) by force
moreover hence "¬ vebt_member (Node None deg treeList summary) y" by simp
moreover hence "¬both_member_options (Node None deg treeList summary) y"
using calculation(2) valid_member_both_member_options by blast
then show ?thesis
by (metis True calculation(1) member_inv not_less_iff_gr_or_eq tvalid valid_member_both_member_options)
next
case False
hence mimapr:"mi < ma"
by (metis "4.hyps"(7) ‹mi ≤ x ∧ x ≤ ma› le_antisym nat_less_le)
then show ?thesis
proof(cases "x ≠ mi")
case True
hence xmi:"x ≠ mi" by simp
let ?h ="high x n"
let ?l = "low x n"
have "?h < length treeList"
using "4"(10) "4"(4) "4.hyps"(1) "4.hyps"(3) "4.hyps"(4) ‹mi ≤ x ∧ x ≤ ma› deg_not_0 exp_split_high_low(1) by auto
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:= ?newnode]"
have "length treeList = length ?newlist" by simp
hence hprolist: "?newlist ! ?h = ?newnode"
by (meson ‹high x n < length treeList› nth_list_update_eq)
have nothprolist: "i ≠ ?h ∧ i < 2^m ⟹ ?newlist ! i = treeList ! i" for i by auto
then show ?thesis
proof(cases "minNull ?newnode")
case True
let ?sn = "vebt_delete summary ?h"
let ?newma= "(if x = ma then (let maxs = vebt_maxt ?sn in (if maxs = None
then mi
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (?newlist ! the maxs))
)
)
else ma)"
let ?delsimp =" (Node (Some (mi, ?newma)) deg ?newlist ?sn)"
have "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ?delsimp"
using del_x_not_mi_new_node_nil[of mi x ma deg ?h ?l ?newnode treeList ?sn summary ?newlist]
by (metis True ‹2 ≤ deg› ‹deg div 2 = n› ‹high x n < length treeList› ‹mi < ma› ‹mi ≤ x ∧ x ≤ ma› ‹x ≠ mi› less_not_refl3 order.not_eq_order_implies_strict)
moreover have "both_member_options (?delsimp) y ⟹ (x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)"
proof-
assume "both_member_options (?delsimp) y"
hence "y = mi ∨ y = ?newma ∨
(both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist)"
using both_member_options_from_complete_tree_to_child[of deg mi ?newma ?newlist ?sn y] dp
by (smt (z3) Suc_1 Suc_le_D both_member_options_def membermima.simps(4) naive_member.simps(3))
moreover have "y = mi ⟹ ?thesis"
by (meson ‹x ≠ mi› both_member_options_equiv_member vebt_mint.simps(3) mint_member tvalid)
moreover have "y = ?newma ⟹ ?thesis"
proof-
assume "y = ?newma"
show ?thesis
proof(cases "x = ma")
case True
let ?maxs = "vebt_maxt ?sn"
have "?newma = (if ?maxs = None then mi
else 2 ^ (deg div 2) * the ?maxs + the (vebt_maxt
((treeList[(high x n):= vebt_delete (treeList ! (high x n)) (low x n)]) !
the ?maxs)))" using True by force
then show ?thesis
proof(cases "?maxs = None ")
case True
then show ?thesis
using ‹(if x = ma then let maxs = vebt_maxt (vebt_delete summary (high x n)) in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (treeList [high x n := vebt_delete (treeList ! high x n) (low x n)] ! the maxs)) else ma) = (if vebt_maxt (vebt_delete summary (high x n)) = None then mi else 2 ^ (deg div 2) * the (vebt_maxt (vebt_delete summary (high x n))) + the (vebt_maxt (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! the (vebt_maxt (vebt_delete summary (high x n))))))› ‹y = (if x = ma then let maxs = vebt_maxt (vebt_delete summary (high x n)) in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (treeList [high x n := vebt_delete (treeList ! high x n) (low x n)] ! the maxs)) else ma)› calculation(2) by presburger
next
case False
then obtain maxs where "Some maxs = ?maxs" by force
hence "both_member_options ?sn maxs"
by (simp add: maxbmo)
hence "both_member_options summary maxs ∧ maxs ≠ ?h"
using "4.IH"(2) by blast
hence "?newlist ! the ?maxs = treeList ! maxs"
by (metis "4.hyps"(1) ‹Some maxs = vebt_maxt (vebt_delete summary (high x n))› option.sel member_bound nothprolist valid_member_both_member_options)
have "maxs < 2^m"
using "4.hyps"(1) ‹both_member_options summary maxs ∧ maxs ≠ high x n› member_bound valid_member_both_member_options by blast
hence "the (vebt_maxt (?newlist ! the ?maxs)) = the (vebt_maxt (treeList ! maxs))"
by (simp add: ‹treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! the (vebt_maxt (vebt_delete summary (high x n))) = treeList ! maxs›)
have "∃ z. both_member_options(treeList ! maxs) z"
by (simp add: "4.hyps"(5) ‹both_member_options summary maxs ∧ maxs ≠ high x n› ‹maxs < 2 ^ m›)
moreover have "invar_vebt (treeList ! maxs) n" using 4
by (metis ‹maxs < 2 ^ m› inthall member_def)
ultimately obtain maxi where "Some maxi = (vebt_maxt (treeList ! maxs))"
by (metis empty_Collect_eq maxt_corr_help_empty not_None_eq set_vebt'_def valid_member_both_member_options)
hence "maxi < 2^n"
by (metis ‹invar_vebt (treeList ! maxs) n› maxt_member member_bound)
hence "both_member_options (treeList ! maxs) maxi"
using ‹Some maxi = vebt_maxt (treeList ! maxs)› maxbmo by presburger
hence "2 ^ (deg div 2) * the ?maxs + the
(vebt_maxt (?newlist ! the ?maxs)) = 2^n * maxs + maxi "
by (metis ‹Some maxi = vebt_maxt (treeList ! maxs)› ‹Some maxs = vebt_maxt (vebt_delete summary (high x n))› ‹deg div 2 = n› ‹the (vebt_maxt (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! the (vebt_maxt (vebt_delete summary (high x n))))) = the (vebt_maxt (treeList ! maxs))› option.sel)
hence "y = 2^n * maxs + maxi"
using False True ‹y = (if x = ma then let maxs = vebt_maxt (vebt_delete summary (high x n)) in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (treeList [high x n := vebt_delete (treeList ! high x n) (low x n)] ! the maxs)) else ma)› by fastforce
hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
by (metis "4.hyps"(2) Suc_1 ‹both_member_options (treeList ! maxs) maxi› ‹deg div 2 = n› ‹maxi < 2 ^ n› ‹maxs < 2 ^ m› add_leD1 both_member_options_from_chilf_to_complete_tree dp high_inv low_inv mult.commute plus_1_eq_Suc)
moreover hence "y ≠ x"
by (metis ‹both_member_options summary maxs ∧ maxs ≠ high x n› ‹maxi < 2 ^ n› ‹y = 2 ^ n * maxs + maxi› high_inv mult.commute)
ultimately show ?thesis by force
qed
next
case False
hence "?newma = ma" by simp
moreover hence "y ≠ x"
using False ‹y = ?newma› by presburger
then show ?thesis
by (metis False ‹y =?newma› both_member_options_equiv_member vebt_maxt.simps(3) maxt_member tvalid)
qed
qed
moreover have "(both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist) ⟹ ?thesis"
proof-
assume assm:"both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist"
show ?thesis
proof(cases "(high y (deg div 2)) = ?h")
case True
hence "both_member_options ?newnode (low y (deg div 2)) " using hprolist by (metis assm)
moreover hence "invar_vebt (treeList ! (high y (deg div 2))) n"
by (metis "4.IH"(1) True ‹high x n < length treeList› inthall member_def)
ultimately have "both_member_options (treeList ! ?h) (low y (deg div 2)) ∧ (low y (deg div 2)) ≠ (low x (deg div 2))"
by (metis "4.IH"(1) ‹deg div 2 = n› ‹high x n < length treeList› inthall member_def)
then show ?thesis
by (metis Suc_1 True ‹high x n < length treeList› add_leD1 both_member_options_from_chilf_to_complete_tree dp plus_1_eq_Suc)
next
case False
hence "x ≠ y"
using ‹deg div 2 = n› by blast
moreover hence "(?newlist ! (high y (deg div 2))) = treeList ! (high y (deg div 2))" using nothprolist
using "4.hyps"(2) False ‹length treeList = length ?newlist› assm by presburger
moreover hence "both_member_options (treeList ! (high y (deg div 2)) ) (low y (deg div 2))"
using assm by presburger
moreover hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
by (metis One_nat_def Suc_leD ‹length treeList = length ?newlist› assm both_member_options_from_chilf_to_complete_tree dp numeral_2_eq_2)
ultimately show ?thesis by blast
qed
qed
ultimately show ?thesis by fastforce
qed
moreover have " (x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y) ⟹ both_member_options (?delsimp) y"
proof-
assume "(x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)"
hence aa:"x ≠ y" and bb:"y = mi ∨ y = ma ∨ (both_member_options (treeList ! (high y n)) (low y n) ∧ high y n < length treeList)"
apply auto[1] by (metis Suc_1 ‹deg div 2 = n› ‹x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y› add_leD1 both_member_options_from_complete_tree_to_child member_inv plus_1_eq_Suc tvalid valid_member_both_member_options)
show "both_member_options (?delsimp) y"
proof-
have "y = mi ⟹both_member_options (?delsimp) y"
by (metis Suc_1 Suc_le_D both_member_options_def dp membermima.simps(4))
moreover have "y = ma ⟹ both_member_options (?delsimp) y"
using aa maxbmo vebt_maxt.simps(3) by presburger
moreover have "both_member_options (treeList ! (high y n)) (low y n) ⟹both_member_options (?delsimp) y "
proof-
assume assmy: "both_member_options (treeList ! (high y n)) (low y n)"
then show "both_member_options (?delsimp) y "
proof(cases "high y n = ?h")
case True
moreover hence "?newlist ! (high y n) = ?newnode"
using hprolist by auto
hence 0:"invar_vebt (treeList !(high y n)) n" using 4
by (metis True ‹high x n < length treeList› inthall member_def)
moreover have 1:"low y n ≠ low x n"
by (metis True aa bit_split_inv)
moreover have 11:" (treeList !(high y n)) ∈ set treeList"
by (metis True ‹high x n < length treeList› inthall member_def)
ultimately have " (∀ xa. both_member_options ?newnode xa =
((low x n) ≠ xa ∧ both_member_options (treeList ! ?h) xa))"
by (simp add: "4.IH"(1))
hence "((low x n) ≠ xa ∧ both_member_options (treeList ! ?h) xa) ⟹ both_member_options ?newnode xa" for xa by blast
moreover have "((low x n) ≠ (low y n) ∧ both_member_options (treeList ! ?h) (low y n))" using 1
using True assmy by presburger
ultimately have "both_member_options ?newnode (low y n)" by blast
then show ?thesis
by (metis One_nat_def Suc_leD True ‹deg div 2 = n› ‹high x n < length treeList› ‹length treeList = length ?newlist› both_member_options_from_chilf_to_complete_tree dp hprolist numerals(2))
next
case False
hence "?newlist ! (high y n) = treeList ! (high y n)" by auto
hence "both_member_options (?newlist !(high y n)) (low y n)"
using assmy by presburger
then show ?thesis
by (smt (z3) Suc_1 Suc_le_D ‹deg div 2 = n› ‹length treeList = length ?newlist› aa add_leD1 bb both_member_options_def both_member_options_from_chilf_to_complete_tree dp membermima.simps(4) plus_1_eq_Suc)
qed
qed
ultimately show ?thesis using bb by fastforce
qed
qed
ultimately show ?thesis by metis
next
case False
hence notemp:"∃ z. both_member_options ?newnode z"
using not_min_Null_member by auto
let ?newma = "(if x = ma then
?h * 2^(deg div 2) + the( vebt_maxt (?newlist ! ?h))
else ma)"
let ?delsimp =" (Node (Some (mi, ?newma)) deg ?newlist summary)"
have "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ?delsimp"
using del_x_not_mi_newnode_not_nil[of mi x ma deg ?h ?l ?newnode treeList ?newlist summary] False xmi mimapr
using ‹deg div 2 = n› ‹high x n < length treeList› ‹mi ≤ x ∧ x ≤ ma› dp nat_less_le plus_1_eq_Suc by fastforce
moreover have "both_member_options ?delsimp y
⟹ x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
proof-
assume ssms: "both_member_options ?delsimp y "
hence aaaa: "y = mi ∨ y = ?newma ∨ (both_member_options (?newlist ! (high y n)) (low y n) ∧ high y n < length ?newlist)"
by (smt (z3) Suc_1 Suc_le_D ‹deg div 2 = n› both_member_options_def dp membermima.simps(4) naive_member.simps(3))
show " x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
proof-
have "y = mi ⟹?thesis"
by (metis Suc_1 Suc_le_D both_member_options_def dp membermima.simps(4) xmi)
moreover have " y = ?newma ⟹ ?thesis"
proof-
assume "y = ?newma"
show ?thesis
proof(cases "x = ma")
case True
hence "?newma =?h * 2 ^ (deg div 2) +the(vebt_maxt(?newlist ! ?h))"
by metis
have "?newlist ! ?h = ?newnode" using hprolist by blast
obtain maxi where maxidef:"Some maxi = vebt_maxt(?newlist ! ?h)"
by (metis False hprolist vebt_maxt.elims minNull.simps(1) minNull.simps(4))
have aa:"invar_vebt (treeList ! ?h) n"
by (metis "4.IH"(1) ‹high x n < length treeList› inthall member_def)
moreover hence ab:"maxi ≠ ?l ∧ both_member_options ?newnode maxi"
by (metis "4.IH"(1) ‹high x n < length treeList› hprolist inthall maxbmo maxidef member_def)
ultimately have ac:"maxi ≠ ?l ∧ both_member_options (treeList ! ?h) maxi"
by (metis "4.IH"(1) ‹high x n < length treeList› inthall member_def)
hence ad:"maxi < 2^n"
using ‹invar_vebt (treeList ! high x n) n› member_bound valid_member_both_member_options by blast
then show ?thesis
by (metis Suc_1 ‹(if x = ma then high x n * 2 ^ (deg div 2) + the (vebt_maxt (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! high x n)) else ma) = high x n * 2 ^ (deg div 2) + the (vebt_maxt (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! high x n))› ‹deg div 2 = n› ‹high x n < length treeList› ‹y = (if x = ma then high x n * 2 ^ (deg div 2) + the (vebt_maxt (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! high x n)) else ma)› ac add_leD1 both_member_options_from_chilf_to_complete_tree dp option.sel high_inv low_inv maxidef plus_1_eq_Suc)
next
case False
then show ?thesis
by (simp add: ‹y = ?newma› maxbmo)
qed
qed
moreover have "both_member_options (?newlist ! (high y n)) (low y n) ⟹ ?thesis"
proof-
assume assmy:"both_member_options (?newlist ! (high y n)) (low y n)"
then show ?thesis
proof(cases "high y n = ?h")
case True
hence "?newlist ! (high y n) = ?newnode"
using hprolist by presburger
have "invar_vebt (treeList ! ?h) n"
by (metis "4.IH"(1) ‹high x n < length treeList› inthall member_def)
hence "low y n ≠ ?l ∧ both_member_options (treeList ! ?h ) (low y n)"
by (metis "4.IH"(1) True ‹high x n < length treeList› assmy hprolist inthall member_def)
then show ?thesis
by (metis Suc_1 True ‹deg div 2 = n› ‹high x n < length treeList› add_leD1 both_member_options_from_chilf_to_complete_tree dp plus_1_eq_Suc)
next
case False
hence "?newlist ! (high y n) = treeList !(high y n)" by auto
then show ?thesis
by (metis False Suc_1 ‹deg div 2 = n› ‹length treeList = length ?newlist› aaaa add_leD1 both_member_options_from_chilf_to_complete_tree calculation(1) calculation(2) dp plus_1_eq_Suc)
qed
qed
ultimately show ?thesis
using aaaa by fastforce
qed
qed
moreover have "(x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)⟹
both_member_options ?delsimp y"
proof-
assume assm: "x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
hence abcv:"y = mi ∨ y = ma ∨ ( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n))"
by (metis Suc_1 ‹deg div 2 = n› add_leD1 both_member_options_from_complete_tree_to_child member_inv plus_1_eq_Suc tvalid valid_member_both_member_options)
thus " both_member_options ?delsimp y"
proof-
have "y = mi ⟹ ?thesis"
by (metis Suc_1 Suc_le_D both_member_options_def dp membermima.simps(4))
moreover have " y = ma ⟹ ?thesis"
using assm maxbmo vebt_maxt.simps(3) by presburger
moreover have " both_member_options (treeList ! (high y n)) (low y n) ⟹ ?thesis"
proof-
assume myass: "both_member_options (treeList ! (high y n)) (low y n) "
thus ?thesis
proof(cases "high y n = ?h")
case True
hence "low y n ≠ ?l"
by (metis assm bit_split_inv)
hence pp:"?newlist ! ?h = ?newnode"
using hprolist by blast
hence "invar_vebt (treeList ! ?h) n"
by (metis "4.IH"(1) ‹high x n < length treeList› inthall member_def)
hence "both_member_options ?newnode (low y n)"
by (metis "4.IH"(1) True ‹high x n < length treeList› ‹low y n ≠ low x n› in_set_member inthall myass)
then show ?thesis
by (metis One_nat_def Suc_leD True ‹deg div 2 = n› ‹high x n < length treeList› ‹length treeList = length ?newlist› both_member_options_from_chilf_to_complete_tree dp numerals(2) pp)
next
case False
hence pp:"?newlist ! (high y n) = treeList ! (high y n)" using nothprolist by auto
then show ?thesis
by (metis Suc_1 ‹deg div 2 = n› ‹length treeList = length (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)])› add_leD1 assm both_member_options_from_chilf_to_complete_tree calculation(1) calculation(2) member_inv myass plus_1_eq_Suc tvalid valid_member_both_member_options)
qed
qed
then show ?thesis
by (metis Suc_1 Suc_leD ‹deg div 2 = n› assm both_member_options_from_complete_tree_to_child calculation(1) calculation(2) dp)
qed
qed
ultimately show ?thesis by metis
qed
next
case False
hence "x = mi" by simp
have "both_member_options summary (high ma n)"
by (metis "4"(10) "4"(11) "4"(7) "4.hyps"(4) div_eq_0_iff Suc_leI Suc_le_D div_exp_eq dual_order.irrefl high_def mimapr nat.simps(3))
hence "vebt_member summary (high ma n)"
using "4.hyps"(1) valid_member_both_member_options by blast
obtain summin where "Some summin = vebt_mint summary"
by (metis "4.hyps"(1) ‹vebt_member summary (high ma n)› empty_Collect_eq mint_corr_help_empty not_None_eq set_vebt'_def)
hence "∃ z . both_member_options (treeList ! summin) z"
by (metis "4.hyps"(1) "4.hyps"(5) both_member_options_equiv_member member_bound mint_member)
moreover have "invar_vebt (treeList ! summin) n"
by (metis "4"(4) "4.IH"(1) "4.hyps"(1) ‹Some summin = vebt_mint summary› member_bound mint_member nth_mem)
ultimately obtain lx where "Some lx = vebt_mint (treeList ! summin)"
by (metis empty_Collect_eq mint_corr_help_empty not_None_eq set_vebt'_def valid_member_both_member_options)
let ?xn = "summin*2^n + lx"
have "?xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2)
+ the (vebt_mint (treeList ! the (vebt_mint summary)))
else x)"
by (metis False ‹Some lx = vebt_mint (treeList ! summin)› ‹Some summin = vebt_mint summary› ‹deg div 2 = n› option.sel)
have "vebt_member (treeList ! summin) lx"
using ‹Some lx = vebt_mint (treeList ! summin)› ‹invar_vebt (treeList ! summin) n› mint_member by auto
moreover have "summin < 2^m"
by (metis "4.hyps"(1) ‹Some summin = vebt_mint summary› member_bound mint_member)
ultimately have xnin: "both_member_options (Node (Some (mi, ma)) deg treeList summary) ?xn"
by (metis "4.hyps"(2) Suc_1 ‹deg div 2 = n› ‹invar_vebt (treeList ! summin) n› add_leD1 both_member_options_equiv_member both_member_options_from_chilf_to_complete_tree dp high_inv low_inv member_bound plus_1_eq_Suc)
let ?h ="high ?xn n"
let ?l = "low ?xn n"
have "?xn < 2^deg"
by (smt (verit, ccfv_SIG) "4.hyps"(1) "4.hyps"(4) div_eq_0_iff ‹Some lx = vebt_mint (treeList ! summin)› ‹Some summin = vebt_mint summary› ‹invar_vebt (treeList ! summin) n› div_exp_eq high_def high_inv le_0_eq member_bound mint_member not_numeral_le_zero power_not_zero)
hence "?h < length treeList"
using "4.hyps"(2) "4.hyps"(3) "4.hyps"(4) ‹invar_vebt (treeList ! summin) n› deg_not_0 exp_split_high_low(1) by metis
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:= ?newnode]"
have "length treeList = length ?newlist" by simp
hence hprolist: "?newlist ! ?h = ?newnode"
by (meson ‹high (summin * 2 ^ n + lx) n < length treeList› nth_list_update)
have nothprolist: "i ≠ ?h ∧ i < 2^m ⟹ ?newlist ! i = treeList ! i" for i by simp
have firstsimp: "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = (take ?h treeList @ [ newnode]@drop (?h+1) treeList)in
if minNull newnode
then(
let sn = vebt_delete summary ?h in
(Node (Some (?xn, if ?xn = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then ?xn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma))
deg newlist sn)
)else
(Node (Some (?xn, (if ?xn = ma then
?h * 2^(deg div 2) + the( vebt_maxt (newlist ! ?h))
else ma)))
deg newlist summary ))"
using del_x_mi[of x mi ma deg ?xn ?h summary treeList ?l]
by (smt (z3) ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹summin * 2 ^ n + lx = (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x)› ‹x = mi› add.commute append_Cons append_Nil dp mimapr nat_less_le plus_1_eq_Suc upd_conv_take_nth_drop)
have minxnrel: "?xn ≠ mi"
by (metis "4.hyps"(2) "4.hyps"(9) ‹high (summin * 2 ^ n + lx) n < length treeList› ‹vebt_member (treeList ! summin) lx› ‹invar_vebt (treeList ! summin) n› both_member_options_equiv_member high_inv less_not_refl low_inv member_bound mimapr)
then show ?thesis
proof(cases "minNull ?newnode")
case True
let ?sn = "vebt_delete summary ?h"
let ?newma= "(if ?xn= ma then (let maxs = vebt_maxt ?sn in
(if maxs = None
then ?xn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (?newlist ! the maxs))
)
)
else ma)"
let ?delsimp =" (Node (Some (?xn, ?newma)) deg ?newlist ?sn)"
have "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ?delsimp"
using del_x_mi_lets_in_minNull[of x mi ma deg ?xn ?h summary treeList ?l ?newnode ?newlist ?sn] False True ‹deg div 2 = n› ‹?h < length treeList› ‹summin * 2 ^ n + lx = (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x)› dp less_not_refl3 mimapr by fastforce
moreover have "both_member_options (?delsimp) y ⟹ (x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)"
proof-
assume "both_member_options (?delsimp) y"
hence "y = ?xn ∨ y = ?newma ∨
(both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist)"
using both_member_options_from_complete_tree_to_child[of deg mi ?newma ?newlist ?sn y] dp
by (smt (z3) Suc_1 Suc_le_D both_member_options_def membermima.simps(4) naive_member.simps(3))
moreover have "y = ?xn ⟹ ?thesis"
by (metis "4.hyps"(9) False ‹vebt_member (treeList ! summin) lx› ‹summin < 2 ^ m› ‹invar_vebt (treeList ! summin) n› both_member_options_equiv_member high_inv less_not_refl low_inv member_bound mimapr xnin)
moreover have "y = ?newma ⟹ ?thesis"
proof-
assume asmt: "y = ?newma"
show ?thesis
proof(cases "?xn = ma")
case True
let ?maxs = "vebt_maxt ?sn"
have newmaext:"?newma = (if ?maxs = None then ?xn
else 2 ^ (deg div 2) * the ?maxs + the (vebt_maxt
( ?newlist ! the ?maxs)))" using True by force
then show ?thesis
proof(cases "?maxs = None ")
case True
hence aa:"?newma = ?xn" using newmaext by auto
hence bb: "?newma ≠ x"
using False minxnrel by presburger
hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) ?xn"
using xnin newmaext minxnrel asmt by simp
moreover have "?xn = y" using aa asmt by simp
ultimately have "both_member_options (Node (Some (mi, ma)) deg treeList summary) y" by simp
then show ?thesis using bb
using ‹summin * 2 ^ n + lx = y› ‹y = ?xn ⟹ x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y› by blast
next
case False
then obtain maxs where "Some maxs = ?maxs" by force
hence "both_member_options ?sn maxs"
by (simp add: maxbmo)
hence "both_member_options summary maxs ∧ maxs ≠ ?h"
using "4.IH"(2) by blast
hence "?newlist ! the ?maxs = treeList ! maxs"
by (metis "4.hyps"(1) ‹Some maxs = vebt_maxt (vebt_delete summary (high (summin * 2 ^ n + lx) n))› option.sel member_bound nothprolist valid_member_both_member_options)
have "maxs < 2^m"
using "4.hyps"(1) ‹both_member_options summary maxs ∧ maxs ≠ high (summin * 2 ^ n + lx) n› member_bound valid_member_both_member_options by blast
hence "the (vebt_maxt (?newlist ! the ?maxs)) = the (vebt_maxt (treeList ! maxs))"
using ‹?newlist ! the (vebt_maxt ?sn) = treeList ! maxs› by presburger
have "∃ z. both_member_options(treeList ! maxs) z"
using "4.hyps"(5) ‹both_member_options summary maxs ∧ maxs ≠?h› ‹maxs < 2 ^ m› by blast
moreover have "invar_vebt (treeList ! maxs) n" using 4
by (metis ‹maxs < 2 ^ m› inthall member_def)
ultimately obtain maxi where "Some maxi = (vebt_maxt (treeList ! maxs))"
by (metis empty_Collect_eq maxt_corr_help_empty not_None_eq set_vebt'_def valid_member_both_member_options)
hence "maxi < 2^n"
by (metis ‹invar_vebt (treeList ! maxs) n› maxt_member member_bound)
hence "both_member_options (treeList ! maxs) maxi"
using ‹Some maxi = vebt_maxt (treeList ! maxs)› maxbmo by presburger
hence "2 ^ (deg div 2) * the ?maxs + the
(vebt_maxt (?newlist ! the ?maxs)) = 2^n * maxs + maxi "
by (metis ‹Some maxi = vebt_maxt (treeList ! maxs)› ‹Some maxs = vebt_maxt ?sn› ‹deg div 2 = n› ‹the (vebt_maxt (?newlist ! the (vebt_maxt ?sn))) = the (vebt_maxt (treeList ! maxs))› option.sel)
hence "?newma = 2^n * maxs + maxi"
using False True by auto
hence "y = 2^n * maxs + maxi" using asmt by simp
hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
by (metis "4.hyps"(2) Suc_1 ‹both_member_options (treeList ! maxs) maxi› ‹deg div 2 = n› ‹maxi < 2 ^ n› ‹maxs < 2 ^ m› add_leD1 both_member_options_from_chilf_to_complete_tree dp high_inv low_inv mult.commute plus_1_eq_Suc)
moreover hence "y ≠ x"
by (metis "4.hyps"(9) True ‹Some maxi = vebt_maxt (treeList ! maxs)› ‹maxi < 2 ^ n› ‹maxs < 2 ^ m› ‹x = mi› ‹y = 2 ^ n * maxs + maxi› high_inv less_not_refl low_inv maxbmo minxnrel mult.commute)
ultimately show ?thesis by force
qed
next
case False
hence "?newma = ma" by simp
moreover hence "mi ≠ ma"
using mimapr by blast
moreover hence "y ≠ x"
using False ‹y = ?newma› ‹x = mi› by auto
then show ?thesis
by (metis False ‹y =?newma› both_member_options_equiv_member vebt_maxt.simps(3) maxt_member tvalid)
qed
qed
moreover have "(both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist) ⟹ ?thesis"
proof-
assume assm:"both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist"
show ?thesis
proof(cases "(high y (deg div 2)) = ?h")
case True
hence 000:"both_member_options ?newnode (low y (deg div 2)) " using hprolist by (metis assm)
hence 001:"invar_vebt (treeList ! (high y (deg div 2))) n"
using True ‹vebt_member (treeList ! summin) lx› ‹invar_vebt (treeList ! summin) n› high_inv member_bound by presburger
then show ?thesis
proof(cases "low y n = ?l")
case True
hence "y = ?xn"
by (metis "000" "4.IH"(1) ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› inthall member_def)
then show ?thesis
using calculation(2) by blast
next
case False
hence "both_member_options (treeList ! ?h) (low y (deg div 2)) ∧ (low y (deg div 2)) ≠ (low ?xn (deg div 2))"
using "4.IH"(1) ‹deg div 2 = n› ‹high ?xn n < length treeList› inthall member_def
by (metis "000")
then show ?thesis
by (metis "4.hyps"(2) "4.hyps"(9) Suc_1 Suc_leD True ‹deg div 2 = n› ‹length treeList = length ?newlist› ‹x = mi› assm both_member_options_from_chilf_to_complete_tree dp less_not_refl mimapr)
qed
next
case False
hence "x ≠ y"
by (metis "4.hyps"(2) "4.hyps"(9) ‹deg div 2 = n› ‹length treeList = length ?newlist› ‹x = mi› assm less_not_refl mimapr nothprolist)
moreover hence "(?newlist ! (high y (deg div 2))) = treeList ! (high y (deg div 2))" using nothprolist
using "4.hyps"(2) False ‹length treeList = length ?newlist› assm by presburger
moreover hence "both_member_options (treeList ! (high y (deg div 2)) ) (low y (deg div 2))"
using assm by presburger
moreover hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
by (metis One_nat_def Suc_leD ‹length treeList = length ?newlist› assm both_member_options_from_chilf_to_complete_tree dp numeral_2_eq_2)
ultimately show ?thesis by blast
qed
qed
ultimately show ?thesis by fastforce
qed
moreover have "(x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)⟹
both_member_options ?delsimp y"
proof-
assume assm: "x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
hence abcv:"y = mi ∨ y = ma ∨ ( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n))"
by (metis Suc_1 ‹deg div 2 = n› add_leD1 both_member_options_from_complete_tree_to_child member_inv plus_1_eq_Suc tvalid valid_member_both_member_options)
thus " both_member_options ?delsimp y"
proof-
have "y = mi ⟹ ?thesis"
using False assm by force
moreover have " y = ma ⟹ ?thesis"
by (smt (z3) Suc_le_D both_member_options_def dp membermima.simps(4) nat_1_add_1 plus_1_eq_Suc)
moreover have " both_member_options (treeList ! (high y n)) (low y n) ⟹ ?thesis"
proof-
assume myass: "both_member_options (treeList ! (high y n)) (low y n) "
thus ?thesis
proof(cases "high y n = ?h")
case True
hence "high y n = ?h" by simp
then show ?thesis
proof(cases "low y n = ?l")
case True
hence "y = ?xn"
by (metis ‹high y n = high (summin * 2 ^ n + lx) n› bit_split_inv)
then show ?thesis
by (metis Suc_le_D both_member_options_def dp membermima.simps(4) nat_1_add_1 plus_1_eq_Suc)
next
case False
hence "low y n ≠ ?l"
by (metis assm bit_split_inv)
hence pp:"?newlist ! ?h = ?newnode"
using hprolist by blast
hence "invar_vebt (treeList ! ?h) n"
using ‹vebt_member (treeList ! summin) lx› ‹invar_vebt (treeList ! summin) n› high_inv member_bound by presburger
hence "both_member_options ?newnode (low y n)"
using "4.IH"(1) False True ‹high (summin * 2 ^ n + lx) n < length treeList› myass by auto
then show ?thesis
by (metis True ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹length treeList = length ?newlist› add_leD1 both_member_options_from_chilf_to_complete_tree dp nat_1_add_1 pp)
qed
next
case False
hence pp:"?newlist ! (high y n) = treeList ! (high y n)" using nothprolist abcv
by (metis "4.hyps"(1) "4.hyps"(3) "4.hyps"(4) assm deg_not_0 exp_split_high_low(1) member_bound tvalid valid_member_both_member_options)
then show ?thesis
by (metis One_nat_def Suc_leD ‹deg div 2 = n› ‹length treeList = length ?newlist› abcv both_member_options_from_chilf_to_complete_tree calculation(1) calculation(2) dp numerals(2))
qed
qed
then show ?thesis
using abcv calculation(1) calculation(2) by fastforce
qed
qed
ultimately show ?thesis by metis
next
case False
hence notemp:"∃ z. both_member_options ?newnode z"
using not_min_Null_member by auto
let ?newma = "(if ?xn = ma then
?h * 2^(deg div 2) + the( vebt_maxt (?newlist ! ?h))
else ma)"
let ?delsimp =" (Node (Some (?xn, ?newma)) deg ?newlist summary)"
have "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ?delsimp"
using del_x_mi_lets_in_not_minNull[of x mi ma deg ?xn ?h summary treeList ?l ?newnode ?newlist]
by (metis "4.hyps"(3) "4.hyps"(4) False ‹Some lx = vebt_mint (treeList ! summin)› ‹Some summin = vebt_mint summary› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹x = mi› add_self_div_2 dp option.sel less_not_refl mimapr)
moreover have "both_member_options ?delsimp y
⟹ x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
proof-
assume ssms: "both_member_options ?delsimp y "
hence aaaa: "y = ?xn ∨ y = ?newma ∨ (both_member_options (?newlist ! (high y n)) (low y n) ∧ high y n < length ?newlist)"
by (smt (z3) Suc_1 Suc_le_D ‹deg div 2 = n› both_member_options_def dp membermima.simps(4) naive_member.simps(3))
show " x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
proof-
have "y = ?xn ⟹?thesis"
using ‹x = mi› minxnrel xnin by blast
moreover have " y = ?newma ⟹ ?thesis"
proof-
assume "y = ?newma"
show ?thesis
proof(cases "?xn = ma")
case True
hence aaa:"?newma =?h * 2 ^ (deg div 2) +the(vebt_maxt(?newlist ! ?h))"
by metis
have "?newlist ! ?h = ?newnode" using hprolist by blast
obtain maxi where maxidef:"Some maxi = vebt_maxt(?newlist ! ?h)"
by (metis False hprolist vebt_maxt.elims minNull.simps(1) minNull.simps(4))
have aa:"invar_vebt (treeList ! ?h) n"
by (metis "4.IH"(1) ‹high ?xn n < length treeList› inthall member_def)
moreover hence ab:"maxi ≠ ?l ∧ both_member_options ?newnode maxi"
by (metis "4.IH"(1) ‹high ?xn n < length treeList› hprolist inthall maxbmo maxidef member_def)
ultimately have ac:"maxi ≠ ?l ∧ both_member_options (treeList ! ?h) maxi"
by (metis "4.IH"(1) ‹high ?xn n < length treeList› inthall member_def)
hence ad:"maxi < 2^n"
by (meson aa member_bound valid_member_both_member_options)
then show ?thesis using Suc_1 aaa ‹y = ?newma› ac add_leD1
by (metis "4.hyps"(2) "4.hyps"(9) Suc_leD ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹x = mi› both_member_options_from_chilf_to_complete_tree dp option.sel high_inv less_not_refl low_inv maxidef mimapr)
next
case False
then show ?thesis
by (metis ‹mi ≤ x ∧ x ≤ ma› ‹x = mi› ‹y = ?newma› both_member_options_equiv_member leD vebt_maxt.simps(3) maxt_member mimapr tvalid)
qed
qed
moreover have "(both_member_options (?newlist ! (high y n)) (low y n)∧ high y n < length ?newlist) ⟹ ?thesis"
proof-
assume assmy:"(both_member_options (?newlist ! (high y n)) (low y n)∧ high y n < length ?newlist)"
then show ?thesis
proof(cases "high y n = ?h")
case True
hence "?newlist ! (high y n) = ?newnode"
using hprolist by presburger
have "invar_vebt (treeList ! ?h) n"
by (metis "4.IH"(1) ‹high ?xn n < length treeList› inthall member_def)
then show ?thesis
proof(cases "low y n= ?l")
case True
hence "y = ?xn"
using "4.IH"(1) ‹high (summin * 2 ^ n + lx) n < length treeList› ‹treeList [high (summin * 2 ^ n + lx) n := vebt_delete (treeList ! high (summin * 2 ^ n + lx) n) (low (summin * 2 ^ n + lx) n)] ! high y n = vebt_delete (treeList ! high (summin * 2 ^ n + lx) n) (low (summin * 2 ^ n + lx) n)› assmy by force
then show ?thesis
using calculation(1) by blast
next
case False
hence "low y n ≠ ?l ∧ both_member_options (treeList ! ?h ) (low y n)" using assmy
by (metis "4.IH"(1) "4.hyps"(2) ‹?newlist ! high y n = vebt_delete (treeList ! high (summin * 2 ^ n + lx) n) (low (summin * 2 ^ n + lx) n)› ‹vebt_member (treeList ! summin) lx› ‹summin < 2 ^ m› high_inv inthall member_bound member_def)
then show ?thesis
by (metis "4.hyps"(2) "4.hyps"(9) Suc_1 Suc_leD True ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹mi ≤ x ∧ x ≤ ma› ‹x = mi› both_member_options_from_chilf_to_complete_tree dp leD mimapr)
qed
next
case False
hence "?newlist ! (high y n) = treeList !(high y n)"
by (smt (z3) "4.hyps"(1) "4.hyps"(2) "4.hyps"(3) "4.hyps"(4) "4.hyps"(8) ‹length treeList = length ?newlist› ‹ma ≤ 2 ^ deg› aaaa calculation(2) deg_not_0 exp_split_high_low(1) less_le_trans member_inv mimapr nothprolist tvalid valid_member_both_member_options)
hence "both_member_options (treeList !(high y n)) (low y n)"
using assmy by presburger
moreover have "x ≠ y"
by (metis "4.hyps"(1) "4.hyps"(4) "4.hyps"(9) ‹invar_vebt (treeList ! summin) n› ‹x < 2 ^ deg› ‹x = mi› calculation deg_not_0 exp_split_high_low(1) mimapr not_less_iff_gr_or_eq)
moreover have "high y n < length ?newlist" using assmy by blast
moreover hence "high y n < length treeList"
using ‹length treeList = length ?newlist› by presburger
ultimately show ?thesis
by (metis One_nat_def Suc_leD ‹deg div 2 = n› both_member_options_from_chilf_to_complete_tree dp numerals(2))
qed
qed
ultimately show ?thesis
using aaaa by fastforce
qed
qed
moreover have "(x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)⟹
both_member_options ?delsimp y"
proof-
assume assm: "x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
hence abcv:"y = mi ∨ y = ma ∨ ( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n))"
by (metis Suc_1 ‹deg div 2 = n› add_leD1 both_member_options_from_complete_tree_to_child member_inv plus_1_eq_Suc tvalid valid_member_both_member_options)
thus " both_member_options ?delsimp y"
proof-
have "y = mi ⟹ ?thesis"
using ‹x = mi› assm by blast
moreover have " y = ma ⟹ ?thesis"
by (smt (z3) Suc_1 Suc_le_D both_member_options_def dp membermima.simps(4))
moreover have " ( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n))
⟹ ?thesis"
proof-
assume myass: "( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n)) "
thus ?thesis
proof(cases "high y n = ?h")
case True
then show ?thesis
proof(cases "low y n = ?l")
case True
then show ?thesis
by (smt (z3) Suc_1 Suc_le_D ‹deg div 2 = n› ‹length treeList = length (treeList [high (summin * 2 ^ n + lx) n := vebt_delete (treeList ! high (summin * 2 ^ n + lx) n) (low (summin * 2 ^ n + lx) n)])› add_leD1 bit_split_inv both_member_options_def both_member_options_from_chilf_to_complete_tree dp membermima.simps(4) myass nth_list_update_neq plus_1_eq_Suc)
next
case False
hence "low y n ≠ ?l" by simp
hence pp:"?newlist ! ?h = ?newnode"
using hprolist by blast
hence "invar_vebt (treeList ! ?h) n"
by (metis "4.IH"(1) ‹high ?xn n < length treeList› inthall member_def)
hence "both_member_options ?newnode (low y n)"
by (metis "4.IH"(1) True ‹high ?xn n < length treeList› ‹low y n ≠ low ?xn n› in_set_member inthall myass)
then show ?thesis
by (metis One_nat_def Suc_leD True ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹length treeList = length ?newlist› both_member_options_from_chilf_to_complete_tree dp numerals(2) pp)
qed
next
case False
have pp:"?newlist ! (high y n) = treeList ! (high y n)"
using nothprolist[of "high y n"] False
by (metis "4.hyps"(1) "4.hyps"(3) "4.hyps"(4) assm deg_not_0 exp_split_high_low(1) member_bound tvalid valid_member_both_member_options)
then show ?thesis
by (metis One_nat_def Suc_leD ‹deg div 2 = n› ‹length treeList = length ?newlist› abcv both_member_options_from_chilf_to_complete_tree calculation(1) calculation(2) dp numerals(2))
qed
qed
then show ?thesis
using abcv calculation(1) calculation(2) by fastforce
qed
qed
ultimately show ?thesis by metis
qed
qed
qed
qed
next
case (5 treeList n summary m deg mi ma)
hence tvalid: "invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg"
using invar_vebt.intros(5)[of treeList n summary m deg mi ma] by simp
hence "mi ≤ ma" and "deg div 2 = n" and "ma ≤ 2^deg" using 5
by (auto simp add: "5.hyps"(3) "5.hyps"(4))
hence dp:"deg ≥ 2"
by (meson vebt_maxt.simps(3) maxt_member member_inv tvalid)
hence nmpr:"n≥ 1 ∧ m = Suc n"
using "5.hyps"(3) ‹deg div 2 = n› by linarith
then show ?case proof(cases "x <mi ∨ x > ma")
case True
hence "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (Node (Some (mi, ma)) deg treeList summary)"
using delt_out_of_range[of x mi ma deg treeList summary] ‹2 ≤ deg› by blast
then show ?thesis
by (metis "5.hyps"(7) True tvalid leD member_inv not_less_iff_gr_or_eq valid_member_both_member_options)
next
case False
hence "mi ≤ x ∧ x ≤ ma" by simp
hence xdegrel:"x < 2^deg"
using "5.hyps"(8) order.strict_trans1 by blast
then show ?thesis
proof(cases "x = mi ∧ x = ma")
case True
hence "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = (Node None deg treeList summary)"
using del_single_cont[of x mi ma deg treeList summary] ‹2 ≤ deg› by blast
moreover hence "invar_vebt (Node None deg treeList summary) deg"
using "5"(4) "5.IH"(1) "5.hyps"(1) "5.hyps"(3) "5.hyps"(4) True mi_eq_ma_no_ch
tvalid invar_vebt.intros(3) by force
moreover hence "¬ vebt_member (Node None deg treeList summary) y" by simp
moreover hence "¬both_member_options (Node None deg treeList summary) y"
using calculation(2) valid_member_both_member_options by blast
then show ?thesis
by (metis True calculation(1) member_inv not_less_iff_gr_or_eq tvalid valid_member_both_member_options)
next
case False
hence mimapr:"mi < ma"
by (metis "5.hyps"(7) ‹mi ≤ x ∧ x ≤ ma› le_antisym nat_less_le)
then show ?thesis
proof(cases "x ≠ mi")
case True
hence xmi:"x ≠ mi" by simp
let ?h ="high x n"
let ?l = "low x n"
have "?h < length treeList" using xdegrel 5
by (metis ‹deg div 2 = n› deg_not_0 div_greater_zero_iff dp exp_split_high_low(1) zero_less_numeral)
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:=?newnode]"
have "length treeList = length ?newlist" by simp
hence hprolist: "?newlist ! ?h = ?newnode"
by (meson ‹high x n < length treeList› nth_list_update_eq)
have nothprolist: "i ≠ ?h ∧ i < 2^m ⟹ ?newlist ! i = treeList ! i" for i by simp
then show ?thesis
proof(cases "minNull ?newnode")
case True
let ?sn = "vebt_delete summary ?h"
let ?newma= "(if x = ma then (let maxs = vebt_maxt ?sn in
(if maxs = None
then mi
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (?newlist ! the maxs))
)
)
else ma)"
let ?delsimp =" (Node (Some (mi, ?newma)) deg ?newlist ?sn)"
have "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ?delsimp"
using del_x_not_mi_new_node_nil[of mi x ma deg ?h ?l ?newnode treeList ?sn summary ?newlist]
by (metis True ‹2 ≤ deg› ‹deg div 2 = n› ‹high x n < length treeList› ‹mi < ma› ‹mi ≤ x ∧ x ≤ ma› ‹x ≠ mi› less_not_refl3 order.not_eq_order_implies_strict)
moreover have "both_member_options (?delsimp) y ⟹ (x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)"
proof-
assume "both_member_options (?delsimp) y"
hence "y = mi ∨ y = ?newma ∨
(both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist)"
using both_member_options_from_complete_tree_to_child[of deg mi ?newma ?newlist ?sn y] dp
by (smt (z3) Suc_1 Suc_le_D both_member_options_def membermima.simps(4) naive_member.simps(3))
moreover have "y = mi ⟹ ?thesis"
by (meson ‹x ≠ mi› both_member_options_equiv_member vebt_mint.simps(3) mint_member tvalid)
moreover have "y = ?newma ⟹ ?thesis"
proof-
assume "y = ?newma"
show ?thesis
proof(cases "x = ma")
case True
let ?maxs = "vebt_maxt ?sn"
have newmapropy:"?newma = (if ?maxs = None then mi
else 2 ^ (deg div 2) * the ?maxs + the (vebt_maxt
(?newlist !
the ?maxs)))" using True by force
then show ?thesis
proof(cases "?maxs = None ")
case True
then show ?thesis
using ‹y = (if x = ma then let maxs = vebt_maxt (vebt_delete summary (high x n)) in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (treeList [high x n := vebt_delete (treeList ! high x n) (low x n)] ! the maxs)) else ma)› calculation(2) newmapropy by presburger
next
case False
then obtain maxs where "Some maxs = ?maxs" by force
hence "both_member_options ?sn maxs"
by (simp add: maxbmo)
hence "both_member_options summary maxs ∧ maxs ≠ ?h"
using "5.IH"(2) by blast
hence "?newlist ! the ?maxs = treeList ! maxs"
by (metis "5.hyps"(1) ‹Some maxs = vebt_maxt (vebt_delete summary (high x n))› option.sel member_bound nothprolist valid_member_both_member_options)
have "maxs < 2^m"
using "5.hyps"(1) ‹both_member_options summary maxs ∧ maxs ≠ high x n› member_bound valid_member_both_member_options by blast
hence "the (vebt_maxt (?newlist ! the ?maxs)) = the (vebt_maxt (treeList ! maxs))"
by (metis ‹Some maxs = vebt_maxt (vebt_delete summary (high x n))› ‹both_member_options summary maxs ∧ maxs ≠ high x n› option.sel nth_list_update_neq)
have "∃ z. both_member_options(treeList ! maxs) z"
by (simp add: "5.hyps"(5) ‹both_member_options summary maxs ∧ maxs ≠ high x n› ‹maxs < 2 ^ m›)
moreover have "invar_vebt (treeList ! maxs) n" using 5
by (metis ‹maxs < 2 ^ m› inthall member_def)
ultimately obtain maxi where "Some maxi = (vebt_maxt (treeList ! maxs))"
by (metis empty_Collect_eq maxt_corr_help_empty not_None_eq set_vebt'_def valid_member_both_member_options)
hence "maxi < 2^n"
by (metis ‹invar_vebt (treeList ! maxs) n› maxt_member member_bound)
hence "both_member_options (treeList ! maxs) maxi"
using ‹Some maxi = vebt_maxt (treeList ! maxs)› maxbmo by presburger
hence "2 ^ (deg div 2) * the ?maxs + the
(vebt_maxt (?newlist ! the ?maxs)) = 2^n * maxs + maxi "
by (metis ‹Some maxi = vebt_maxt (treeList ! maxs)› ‹Some maxs = vebt_maxt (vebt_delete summary (high x n))› ‹deg div 2 = n› ‹the (vebt_maxt (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! the (vebt_maxt (vebt_delete summary (high x n))))) = the (vebt_maxt (treeList ! maxs))› option.sel)
hence "y = 2^n * maxs + maxi"
using False ‹y = (if x = ma then let maxs = vebt_maxt (vebt_delete summary (high x n)) in if maxs = None then mi else 2 ^ (deg div 2) * the maxs + the (vebt_maxt (treeList [high x n := vebt_delete (treeList ! high x n) (low x n)] ! the maxs)) else ma)› newmapropy by presburger
hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
by (metis "5.hyps"(2) Suc_1 ‹both_member_options (treeList ! maxs) maxi› ‹deg div 2 = n› ‹maxi < 2 ^ n› ‹maxs < 2 ^ m› add_leD1 both_member_options_from_chilf_to_complete_tree dp high_inv low_inv mult.commute plus_1_eq_Suc)
moreover hence "y ≠ x"
by (metis ‹both_member_options summary maxs ∧ maxs ≠ high x n› ‹maxi < 2 ^ n› ‹y = 2 ^ n * maxs + maxi› high_inv mult.commute)
ultimately show ?thesis by force
qed
next
case False
hence "?newma = ma" by simp
moreover hence "y ≠ x"
using False ‹y = ?newma› by presburger
then show ?thesis
by (metis False ‹y =?newma› both_member_options_equiv_member vebt_maxt.simps(3) maxt_member tvalid)
qed
qed
moreover have "(both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist) ⟹ ?thesis"
proof-
assume assm:"both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist"
show ?thesis
proof(cases "(high y (deg div 2)) = ?h")
case True
hence "both_member_options ?newnode (low y (deg div 2)) " using hprolist by (metis assm)
moreover hence "invar_vebt (treeList ! (high y (deg div 2))) n"
by (metis "5.IH"(1) True ‹high x n < length treeList› inthall member_def)
ultimately have "both_member_options (treeList ! ?h) (low y (deg div 2)) ∧ (low y (deg div 2)) ≠ (low x (deg div 2))"
by (metis "5.IH"(1) ‹deg div 2 = n› ‹high x n < length treeList› inthall member_def)
then show ?thesis
by (metis Suc_1 True ‹high x n < length treeList› add_leD1 both_member_options_from_chilf_to_complete_tree dp plus_1_eq_Suc)
next
case False
hence "x ≠ y"
using ‹deg div 2 = n› by blast
moreover hence "(?newlist ! (high y (deg div 2))) = treeList ! (high y (deg div 2))" using nothprolist
using "5.hyps"(2) False ‹length treeList = length ?newlist› assm by presburger
moreover hence "both_member_options (treeList ! (high y (deg div 2)) ) (low y (deg div 2))"
using assm by presburger
moreover hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
by (metis One_nat_def Suc_leD ‹length treeList = length ?newlist› assm both_member_options_from_chilf_to_complete_tree dp numeral_2_eq_2)
ultimately show ?thesis by blast
qed
qed
ultimately show ?thesis by fastforce
qed
moreover have " (x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y) ⟹ both_member_options (?delsimp) y"
proof-
assume "(x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)"
hence aa:"x ≠ y" and bb:"y = mi ∨ y = ma ∨ (both_member_options (treeList ! (high y n)) (low y n) ∧ high y n < length treeList)"
apply auto[1] by (metis Suc_1 ‹deg div 2 = n› ‹x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y› add_leD1 both_member_options_from_complete_tree_to_child member_inv plus_1_eq_Suc tvalid valid_member_both_member_options)
show "both_member_options (?delsimp) y"
proof-
have "y = mi ⟹both_member_options (?delsimp) y"
by (metis Suc_1 Suc_le_D both_member_options_def dp membermima.simps(4))
moreover have "y = ma ⟹ both_member_options (?delsimp) y"
using aa maxbmo vebt_maxt.simps(3) by presburger
moreover have "both_member_options (treeList ! (high y n)) (low y n) ⟹both_member_options (?delsimp) y "
proof-
assume assmy: "both_member_options (treeList ! (high y n)) (low y n)"
then show "both_member_options (?delsimp) y "
proof(cases "high y n = ?h")
case True
moreover hence "?newlist ! (high y n) = ?newnode"
using hprolist by auto
hence 0:"invar_vebt (treeList !(high y n)) n" using 5
by (metis True ‹high x n < length treeList› inthall member_def)
moreover have 1:"low y n ≠ low x n"
by (metis True aa bit_split_inv)
moreover have 11:" (treeList !(high y n)) ∈ set treeList"
by (metis True ‹high x n < length treeList› inthall member_def)
ultimately have " (∀ xa. both_member_options ?newnode xa =
((low x n) ≠ xa ∧ both_member_options (treeList ! ?h) xa))"
by (simp add: "5.IH"(1))
hence "((low x n) ≠ xa ∧ both_member_options (treeList ! ?h) xa) ⟹ both_member_options ?newnode xa" for xa by blast
moreover have "((low x n) ≠ (low y n) ∧ both_member_options (treeList ! ?h) (low y n))" using 1
using True assmy by presburger
ultimately have "both_member_options ?newnode (low y n)" by blast
then show ?thesis
by (metis One_nat_def Suc_leD True ‹deg div 2 = n› ‹high x n < length treeList› ‹length treeList = length ?newlist› both_member_options_from_chilf_to_complete_tree dp hprolist numerals(2))
next
case False
hence "?newlist ! (high y n) = treeList ! (high y n)" by auto
hence "both_member_options (?newlist !(high y n)) (low y n)"
using assmy by presburger
then show ?thesis
by (smt (z3) Suc_1 Suc_le_D ‹deg div 2 = n› ‹length treeList = length ?newlist› aa add_leD1 bb both_member_options_def both_member_options_from_chilf_to_complete_tree dp membermima.simps(4) plus_1_eq_Suc)
qed
qed
ultimately show ?thesis using bb by fastforce
qed
qed
ultimately show ?thesis by metis
next
case False
hence notemp:"∃ z. both_member_options ?newnode z"
using not_min_Null_member by auto
let ?newma = "(if x = ma then
?h * 2^(deg div 2) + the( vebt_maxt (?newlist ! ?h))
else ma)"
let ?delsimp =" (Node (Some (mi, ?newma)) deg ?newlist summary)"
have "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ?delsimp"
using del_x_not_mi_newnode_not_nil[of mi x ma deg ?h ?l ?newnode treeList ?newlist summary] False xmi mimapr
using ‹deg div 2 = n› ‹high x n < length treeList› ‹mi ≤ x ∧ x ≤ ma› dp nat_less_le plus_1_eq_Suc by fastforce
moreover have "both_member_options ?delsimp y
⟹ x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
proof-
assume ssms: "both_member_options ?delsimp y "
hence aaaa: "y = mi ∨ y = ?newma ∨ (both_member_options (?newlist ! (high y n)) (low y n) ∧ high y n < length ?newlist)"
by (smt (z3) Suc_1 Suc_le_D ‹deg div 2 = n› both_member_options_def dp membermima.simps(4) naive_member.simps(3))
show " x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
proof-
have "y = mi ⟹?thesis"
by (metis Suc_1 Suc_le_D both_member_options_def dp membermima.simps(4) xmi)
moreover have " y = ?newma ⟹ ?thesis"
proof-
assume "y = ?newma"
show ?thesis
proof(cases "x = ma")
case True
hence "?newma =?h * 2 ^ (deg div 2) +the(vebt_maxt(?newlist ! ?h))"
by metis
have "?newlist ! ?h = ?newnode" using hprolist by blast
obtain maxi where maxidef:"Some maxi = vebt_maxt(?newlist ! ?h)"
by (metis False hprolist vebt_maxt.elims minNull.simps(1) minNull.simps(4))
have aa:"invar_vebt (treeList ! ?h) n"
by (metis "5.IH"(1) ‹high x n < length treeList› inthall member_def)
moreover hence ab:"maxi ≠ ?l ∧ both_member_options ?newnode maxi"
by (metis "5.IH"(1) ‹high x n < length treeList› hprolist inthall maxbmo maxidef member_def)
ultimately have ac:"maxi ≠ ?l ∧ both_member_options (treeList ! ?h) maxi"
by (metis "5.IH"(1) ‹high x n < length treeList› inthall member_def)
hence ad:"maxi < 2^n"
using ‹invar_vebt (treeList ! high x n) n› member_bound valid_member_both_member_options by blast
then show ?thesis
by (metis Suc_1 ‹(if x = ma then high x n * 2 ^ (deg div 2) + the (vebt_maxt (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! high x n)) else ma) = high x n * 2 ^ (deg div 2) + the (vebt_maxt (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! high x n))› ‹deg div 2 = n› ‹high x n < length treeList› ‹y = (if x = ma then high x n * 2 ^ (deg div 2) + the (vebt_maxt (treeList[high x n := vebt_delete (treeList ! high x n) (low x n)] ! high x n)) else ma)› ac add_leD1 both_member_options_from_chilf_to_complete_tree dp option.sel high_inv low_inv maxidef plus_1_eq_Suc)
next
case False
then show ?thesis
by (simp add: ‹y = ?newma› maxbmo)
qed
qed
moreover have "both_member_options (?newlist ! (high y n)) (low y n) ⟹ ?thesis"
proof-
assume assmy:"both_member_options (?newlist ! (high y n)) (low y n)"
then show ?thesis
proof(cases "high y n = ?h")
case True
hence "?newlist ! (high y n) = ?newnode"
using hprolist by presburger
have "invar_vebt (treeList ! ?h) n"
by (metis "5.IH"(1) ‹high x n < length treeList› inthall member_def)
hence "low y n ≠ ?l ∧ both_member_options (treeList ! ?h ) (low y n)"
by (metis "5.IH"(1) True ‹high x n < length treeList› assmy hprolist inthall member_def)
then show ?thesis
by (metis Suc_1 True ‹deg div 2 = n› ‹high x n < length treeList› add_leD1 both_member_options_from_chilf_to_complete_tree dp plus_1_eq_Suc)
next
case False
hence "?newlist ! (high y n) = treeList !(high y n)" by auto
then show ?thesis
by (metis False Suc_1 ‹deg div 2 = n› ‹length treeList = length ?newlist› aaaa add_leD1 both_member_options_from_chilf_to_complete_tree calculation(1) calculation(2) dp plus_1_eq_Suc)
qed
qed
ultimately show ?thesis
using aaaa by fastforce
qed
qed
moreover have "(x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)⟹
both_member_options ?delsimp y"
proof-
assume assm: "x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
hence abcv:"y = mi ∨ y = ma ∨ ( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n))"
by (metis Suc_1 ‹deg div 2 = n› add_leD1 both_member_options_from_complete_tree_to_child member_inv plus_1_eq_Suc tvalid valid_member_both_member_options)
thus " both_member_options ?delsimp y"
proof-
have "y = mi ⟹ ?thesis"
by (metis Suc_1 Suc_le_D both_member_options_def dp membermima.simps(4))
moreover have " y = ma ⟹ ?thesis"
using assm maxbmo vebt_maxt.simps(3) by presburger
moreover have " both_member_options (treeList ! (high y n)) (low y n) ⟹ ?thesis"
proof-
assume myass: "both_member_options (treeList ! (high y n)) (low y n) "
thus ?thesis
proof(cases "high y n = ?h")
case True
hence "low y n ≠ ?l"
by (metis assm bit_split_inv)
hence pp:"?newlist ! ?h = ?newnode"
using hprolist by blast
hence "invar_vebt (treeList ! ?h) n"
by (metis "5.IH"(1) ‹high x n < length treeList› inthall member_def)
hence "both_member_options ?newnode (low y n)"
by (metis "5.IH"(1) True ‹high x n < length treeList› ‹low y n ≠ low x n› in_set_member inthall myass)
then show ?thesis
by (metis One_nat_def Suc_leD True ‹deg div 2 = n› ‹high x n < length treeList› ‹length treeList = length ?newlist› both_member_options_from_chilf_to_complete_tree dp numerals(2) pp)
next
case False
hence pp:"?newlist ! (high y n) = treeList ! (high y n)" using nothprolist abcv by auto
then show ?thesis
by (metis One_nat_def Suc_leD ‹deg div 2 = n› ‹length treeList = length ?newlist› abcv both_member_options_from_chilf_to_complete_tree calculation(1) calculation(2) dp numerals(2))
qed
qed
then show ?thesis
using abcv calculation(1) calculation(2) by fastforce
qed
qed
ultimately show ?thesis by metis
qed
next
case False
hence "x = mi" by simp
have "both_member_options summary (high ma n)"
by (metis "5"(10) "5"(11) "5"(7) "5.hyps"(4) div_eq_0_iff Suc_leI Suc_le_D div_exp_eq dual_order.irrefl high_def mimapr nat.simps(3))
hence "vebt_member summary (high ma n)"
using "5.hyps"(1) valid_member_both_member_options by blast
obtain summin where "Some summin = vebt_mint summary"
by (metis "5.hyps"(1) ‹vebt_member summary (high ma n)› empty_Collect_eq mint_corr_help_empty not_None_eq set_vebt'_def)
hence "∃ z . both_member_options (treeList ! summin) z"
by (metis "5.hyps"(1) "5.hyps"(5) both_member_options_equiv_member member_bound mint_member)
moreover have "invar_vebt (treeList ! summin) n"
by (metis "5.IH"(1) "5.hyps"(1) "5.hyps"(2) ‹Some summin = vebt_mint summary› member_bound mint_member nth_mem)
ultimately obtain lx where "Some lx = vebt_mint (treeList ! summin)"
by (metis empty_Collect_eq mint_corr_help_empty not_None_eq set_vebt'_def valid_member_both_member_options)
let ?xn = "summin*2^n + lx"
have "?xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2)
+ the (vebt_mint (treeList ! the (vebt_mint summary)))
else x)"
by (metis False ‹Some lx = vebt_mint (treeList ! summin)› ‹Some summin = vebt_mint summary› ‹deg div 2 = n› option.sel)
have "vebt_member (treeList ! summin) lx"
using ‹Some lx = vebt_mint (treeList ! summin)› ‹invar_vebt (treeList ! summin) n› mint_member by auto
moreover have "summin < 2^m"
by (metis "5.hyps"(1) ‹Some summin = vebt_mint summary› member_bound mint_member)
ultimately have xnin: "both_member_options (Node (Some (mi, ma)) deg treeList summary) ?xn"
by (metis "5.hyps"(2) Suc_1 ‹deg div 2 = n› ‹invar_vebt (treeList ! summin) n› add_leD1 both_member_options_equiv_member both_member_options_from_chilf_to_complete_tree dp high_inv low_inv member_bound plus_1_eq_Suc)
let ?h ="high ?xn n"
let ?l = "low ?xn n"
have "?xn < 2^deg"
by (smt (verit, ccfv_SIG) "5.hyps"(1) "5.hyps"(4) div_eq_0_iff ‹Some lx = vebt_mint (treeList ! summin)› ‹Some summin = vebt_mint summary› ‹invar_vebt (treeList ! summin) n› div_exp_eq high_def high_inv le_0_eq member_bound mint_member not_numeral_le_zero power_not_zero)
hence "?h < length treeList"
using "5.hyps"(2) ‹vebt_member (treeList ! summin) lx› ‹summin < 2 ^ m› ‹invar_vebt (treeList ! summin) n› high_inv member_bound by presburger
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:= ?newnode]"
have "length treeList = length ?newlist" by simp
hence hprolist: "?newlist ! ?h = ?newnode"
by (meson ‹high (summin * 2 ^ n + lx) n < length treeList› nth_list_update)
have nothprolist: "i ≠ ?h ∧ i < 2^m ⟹ ?newlist ! i = treeList ! i" for i by simp
have firstsimp: "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = treeList[?h:= ?newnode] in
if minNull newnode
then(
let sn = vebt_delete summary ?h in
(Node (Some (?xn, if ?xn = ma then (let maxs = vebt_maxt sn in
(if maxs = None
then ?xn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (newlist ! the maxs))
)
)
else ma))
deg newlist sn)
)else
(Node (Some (?xn, (if ?xn = ma then
?h * 2^(deg div 2) + the( vebt_maxt (newlist ! ?h))
else ma)))
deg newlist summary ))"
using del_x_mi[of x mi ma deg ?xn ?h summary treeList ?l]
‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList›
‹summin * 2 ^ n + lx = (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) +
the (vebt_mint (treeList ! the (vebt_mint summary))) else x)› ‹x = mi› dp mimapr nat_less_le by smt
have minxnrel: "?xn ≠ mi"
by (metis "5.hyps"(2) "5.hyps"(9) ‹high (summin * 2 ^ n + lx) n < length treeList› ‹vebt_member (treeList ! summin) lx› ‹invar_vebt (treeList ! summin) n› both_member_options_equiv_member high_inv less_not_refl low_inv member_bound mimapr)
then show ?thesis
proof(cases "minNull ?newnode")
case True
let ?sn = "vebt_delete summary ?h"
let ?newma= "(if ?xn= ma then (let maxs = vebt_maxt ?sn in
(if maxs = None
then ?xn
else 2^(deg div 2) * the maxs
+ the (vebt_maxt (?newlist ! the maxs))
)
)
else ma)"
let ?delsimp =" (Node (Some (?xn, ?newma)) deg ?newlist ?sn)"
have "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ?delsimp"
using del_x_mi_lets_in_minNull[of x mi ma deg ?xn ?h summary treeList ?l ?newnode ?newlist ?sn] False True ‹deg div 2 = n› ‹?h < length treeList› ‹summin * 2 ^ n + lx = (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x)› dp less_not_refl3 mimapr by fastforce
moreover have "both_member_options (?delsimp) y ⟹ (x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)"
proof-
assume "both_member_options (?delsimp) y"
hence "y = ?xn ∨ y = ?newma ∨
(both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist)"
using both_member_options_from_complete_tree_to_child[of deg mi ?newma ?newlist ?sn y] dp
by (smt (z3) Suc_1 Suc_le_D both_member_options_def membermima.simps(4) naive_member.simps(3))
moreover have "y = ?xn ⟹ ?thesis"
by (metis "5.hyps"(9) False ‹vebt_member (treeList ! summin) lx› ‹summin < 2 ^ m› ‹invar_vebt (treeList ! summin) n› both_member_options_equiv_member high_inv less_not_refl low_inv member_bound mimapr xnin)
moreover have "y = ?newma ⟹ ?thesis"
proof-
assume asmt: "y = ?newma"
show ?thesis
proof(cases "?xn = ma")
case True
let ?maxs = "vebt_maxt ?sn"
have newmaext:"?newma = (if ?maxs = None then ?xn
else 2 ^ (deg div 2) * the ?maxs + the (vebt_maxt
( ?newlist ! the ?maxs)))" using True by force
then show ?thesis
proof(cases "?maxs = None ")
case True
hence aa:"?newma = ?xn" using newmaext by auto
hence bb: "?newma ≠ x"
using False minxnrel by presburger
hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) ?xn"
using xnin newmaext minxnrel asmt by simp
moreover have "?xn = y" using aa asmt by simp
ultimately have "both_member_options (Node (Some (mi, ma)) deg treeList summary) y" by simp
then show ?thesis using bb
using ‹summin * 2 ^ n + lx = y› ‹y = ?xn ⟹ x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y› by blast
next
case False
then obtain maxs where "Some maxs = ?maxs" by force
hence "both_member_options ?sn maxs"
by (simp add: maxbmo)
hence "both_member_options summary maxs ∧ maxs ≠ ?h"
using "5.IH"(2) by blast
hence "?newlist ! the ?maxs = treeList ! maxs"
by (metis "5.hyps"(1) ‹Some maxs = vebt_maxt (vebt_delete summary (high (summin * 2 ^ n + lx) n))› option.sel member_bound nothprolist valid_member_both_member_options)
have "maxs < 2^m"
using "5.hyps"(1) ‹both_member_options summary maxs ∧ maxs ≠ high (summin * 2 ^ n + lx) n› member_bound valid_member_both_member_options by blast
hence "the (vebt_maxt (?newlist ! the ?maxs)) = the (vebt_maxt (treeList ! maxs))"
using ‹?newlist ! the (vebt_maxt ?sn) = treeList ! maxs› by presburger
have "∃ z. both_member_options(treeList ! maxs) z"
using "5.hyps"(5) ‹both_member_options summary maxs ∧ maxs ≠?h› ‹maxs < 2 ^ m› by blast
moreover have "invar_vebt (treeList ! maxs) n" using 5
by (metis ‹maxs < 2 ^ m› inthall member_def)
ultimately obtain maxi where "Some maxi = (vebt_maxt (treeList ! maxs))"
by (metis empty_Collect_eq maxt_corr_help_empty not_None_eq set_vebt'_def valid_member_both_member_options)
hence "maxi < 2^n"
by (metis ‹invar_vebt (treeList ! maxs) n› maxt_member member_bound)
hence "both_member_options (treeList ! maxs) maxi"
using ‹Some maxi = vebt_maxt (treeList ! maxs)› maxbmo by presburger
hence "2 ^ (deg div 2) * the ?maxs + the
(vebt_maxt (?newlist ! the ?maxs)) = 2^n * maxs + maxi "
by (metis ‹Some maxi = vebt_maxt (treeList ! maxs)› ‹Some maxs = vebt_maxt ?sn› ‹deg div 2 = n› ‹the (vebt_maxt (?newlist ! the (vebt_maxt ?sn))) = the (vebt_maxt (treeList ! maxs))› option.sel)
hence "?newma = 2^n * maxs + maxi"
using False True by auto
hence "y = 2^n * maxs + maxi" using asmt by simp
hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
by (metis "5.hyps"(2) Suc_1 ‹both_member_options (treeList ! maxs) maxi› ‹deg div 2 = n› ‹maxi < 2 ^ n› ‹maxs < 2 ^ m› add_leD1 both_member_options_from_chilf_to_complete_tree dp high_inv low_inv mult.commute plus_1_eq_Suc)
moreover hence "y ≠ x"
by (metis "5.hyps"(9) True ‹Some maxi = vebt_maxt (treeList ! maxs)› ‹maxi < 2 ^ n› ‹maxs < 2 ^ m› ‹x = mi› ‹y = 2 ^ n * maxs + maxi› high_inv less_not_refl low_inv maxbmo minxnrel mult.commute)
ultimately show ?thesis by force
qed
next
case False
hence "?newma = ma" by simp
moreover hence "mi ≠ ma"
using mimapr by blast
moreover hence "y ≠ x"
using False ‹y = ?newma› ‹x = mi› by auto
then show ?thesis
by (metis False ‹y =?newma› both_member_options_equiv_member vebt_maxt.simps(3) maxt_member tvalid)
qed
qed
moreover have "(both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist) ⟹ ?thesis"
proof-
assume assm:"both_member_options (?newlist ! (high y (deg div 2))) (low y (deg div 2)) ∧ (high y (deg div 2)) < length ?newlist"
show ?thesis
proof(cases "(high y (deg div 2)) = ?h")
case True
hence 000:"both_member_options ?newnode (low y (deg div 2)) " using hprolist by (metis assm)
hence 001:"invar_vebt (treeList ! (high y (deg div 2))) n"
using True ‹vebt_member (treeList ! summin) lx› ‹invar_vebt (treeList ! summin) n› high_inv member_bound by presburger
then show ?thesis
proof(cases "low y n = ?l")
case True
hence "y = ?xn"
by (metis "000" "5.IH"(1) ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› inthall member_def)
then show ?thesis
using calculation(2) by blast
next
case False
hence "both_member_options (treeList ! ?h) (low y (deg div 2)) ∧ (low y (deg div 2)) ≠ (low ?xn (deg div 2))"
using "5.IH"(1) ‹deg div 2 = n› ‹high ?xn n < length treeList› inthall member_def
by (metis "000")
then show ?thesis
by (metis "5.hyps"(2) "5.hyps"(9) Suc_1 Suc_leD True ‹deg div 2 = n› ‹length treeList = length ?newlist› ‹x = mi› assm both_member_options_from_chilf_to_complete_tree dp less_not_refl mimapr)
qed
next
case False
hence "x ≠ y"
by (metis "5.hyps"(2) "5.hyps"(9) ‹deg div 2 = n› ‹length treeList = length ?newlist› ‹x = mi› assm less_not_refl mimapr nothprolist)
moreover hence "(?newlist ! (high y (deg div 2))) = treeList ! (high y (deg div 2))" using nothprolist
using "5.hyps"(2) False ‹length treeList = length ?newlist› assm by presburger
moreover hence "both_member_options (treeList ! (high y (deg div 2)) ) (low y (deg div 2))"
using assm by presburger
moreover hence "both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
by (metis One_nat_def Suc_leD ‹length treeList = length ?newlist› assm both_member_options_from_chilf_to_complete_tree dp numeral_2_eq_2)
ultimately show ?thesis by blast
qed
qed
ultimately show ?thesis by fastforce
qed
moreover have "(x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)⟹
both_member_options ?delsimp y"
proof-
assume assm: "x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
hence abcv:"y = mi ∨ y = ma ∨ ( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n))"
by (metis Suc_1 ‹deg div 2 = n› add_leD1 both_member_options_from_complete_tree_to_child member_inv plus_1_eq_Suc tvalid valid_member_both_member_options)
thus " both_member_options ?delsimp y"
proof-
have "y = mi ⟹ ?thesis"
using False assm by force
moreover have " y = ma ⟹ ?thesis"
by (smt (z3) Suc_le_D both_member_options_def dp membermima.simps(4) nat_1_add_1 plus_1_eq_Suc)
moreover have " both_member_options (treeList ! (high y n)) (low y n) ⟹ ?thesis"
proof-
assume myass: "both_member_options (treeList ! (high y n)) (low y n) "
thus ?thesis
proof(cases "high y n = ?h")
case True
hence "high y n = ?h" by simp
then show ?thesis
proof(cases "low y n = ?l")
case True
hence "y = ?xn"
by (metis ‹high y n = high (summin * 2 ^ n + lx) n› bit_split_inv)
then show ?thesis
by (metis Suc_le_D both_member_options_def dp membermima.simps(4) nat_1_add_1 plus_1_eq_Suc)
next
case False
hence "low y n ≠ ?l"
by (metis assm bit_split_inv)
hence pp:"?newlist ! ?h = ?newnode"
using hprolist by blast
hence "invar_vebt (treeList ! ?h) n"
using ‹vebt_member (treeList ! summin) lx› ‹invar_vebt (treeList ! summin) n› high_inv member_bound by presburger
hence "both_member_options ?newnode (low y n)"
using "5.IH"(1) False True ‹high (summin * 2 ^ n + lx) n < length treeList› myass by force
then show ?thesis
by (metis True ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹length treeList = length ?newlist› add_leD1 both_member_options_from_chilf_to_complete_tree dp nat_1_add_1 pp)
qed
next
case False
hence pp:"?newlist ! (high y n) = treeList ! (high y n)" using nothprolist abcv by auto
then show ?thesis
by (metis One_nat_def Suc_leD ‹deg div 2 = n› ‹length treeList = length ?newlist› abcv both_member_options_from_chilf_to_complete_tree calculation(1) calculation(2) dp numerals(2))
qed
qed
then show ?thesis
using abcv calculation(1) calculation(2) by fastforce
qed
qed
ultimately show ?thesis by metis
next
case False
hence notemp:"∃ z. both_member_options ?newnode z"
using not_min_Null_member by auto
let ?newma = "(if ?xn = ma then
?h * 2^(deg div 2) + the( vebt_maxt (?newlist ! ?h))
else ma)"
let ?delsimp =" (Node (Some (?xn, ?newma)) deg ?newlist summary)"
have "vebt_delete (Node (Some (mi, ma)) deg treeList summary) x = ?delsimp"
using del_x_mi_lets_in_not_minNull[of x mi ma deg ?xn ?h summary treeList ?l ?newnode ?newlist]
using False ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹summin * 2 ^ n + lx = (if x = mi then the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary))) else x)› ‹x = mi› dp mimapr nat_less_le by fastforce
moreover have "both_member_options ?delsimp y
⟹ x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
proof-
assume ssms: "both_member_options ?delsimp y "
hence aaaa: "y = ?xn ∨ y = ?newma ∨ (both_member_options (?newlist ! (high y n)) (low y n) ∧ high y n < length ?newlist)"
by (smt (z3) Suc_1 Suc_le_D ‹deg div 2 = n› both_member_options_def dp membermima.simps(4) naive_member.simps(3))
show " x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
proof-
have "y = ?xn ⟹?thesis"
using ‹x = mi› minxnrel xnin by blast
moreover have " y = ?newma ⟹ ?thesis"
proof-
assume "y = ?newma"
show ?thesis
proof(cases "?xn = ma")
case True
hence aaa:"?newma =?h * 2 ^ (deg div 2) +the(vebt_maxt(?newlist ! ?h))"
by metis
have "?newlist ! ?h = ?newnode" using hprolist by blast
obtain maxi where maxidef:"Some maxi = vebt_maxt(?newlist ! ?h)"
by (metis False hprolist vebt_maxt.elims minNull.simps(1) minNull.simps(4))
have aa:"invar_vebt (treeList ! ?h) n"
by (metis "5.IH"(1) ‹high ?xn n < length treeList› inthall member_def)
moreover hence ab:"maxi ≠ ?l ∧ both_member_options ?newnode maxi"
by (metis "5.IH"(1) ‹high ?xn n < length treeList› hprolist inthall maxbmo maxidef member_def)
ultimately have ac:"maxi ≠ ?l ∧ both_member_options (treeList ! ?h) maxi"
by (metis "5.IH"(1) ‹high ?xn n < length treeList› inthall member_def)
hence ad:"maxi < 2^n"
using ‹invar_vebt (treeList ! high ?xn n) n› member_bound valid_member_both_member_options by blast
then show ?thesis using Suc_1 aaa ‹y = ?newma› ac add_leD1
both_member_options_from_chilf_to_complete_tree dp option.sel high_inv low_inv maxidef plus_1_eq_Suc
by (metis (no_types, lifting) True ‹Some lx = vebt_mint (treeList ! summin)›
‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList›
‹vebt_member (treeList ! summin) lx› ‹invar_vebt (treeList ! summin) n›
‹x = mi› leD member_bound mimapr mint_corr_help nat_add_left_cancel_le
valid_member_both_member_options)
next
case False
then show ?thesis
by (metis ‹mi ≤ x ∧ x ≤ ma› ‹x = mi› ‹y = ?newma› both_member_options_equiv_member leD vebt_maxt.simps(3) maxt_member mimapr tvalid)
qed
qed
moreover have "(both_member_options (?newlist ! (high y n)) (low y n)∧ high y n < length ?newlist) ⟹ ?thesis"
proof-
assume assmy:"(both_member_options (?newlist ! (high y n)) (low y n)∧ high y n < length ?newlist)"
then show ?thesis
proof(cases "high y n = ?h")
case True
hence "?newlist ! (high y n) = ?newnode"
using hprolist by presburger
have "invar_vebt (treeList ! ?h) n"
by (metis "5.IH"(1) ‹high ?xn n < length treeList› inthall member_def)
then show ?thesis
proof(cases "low y n= ?l")
case True
hence "y = ?xn"
using "5.IH"(1) ‹high (summin * 2 ^ n + lx) n < length treeList› ‹treeList [high (summin * 2 ^ n + lx) n := vebt_delete (treeList ! high (summin * 2 ^ n + lx) n) (low (summin * 2 ^ n + lx) n)] ! high y n = vebt_delete (treeList ! high (summin * 2 ^ n + lx) n) (low (summin * 2 ^ n + lx) n)› assmy by force
then show ?thesis
using calculation(1) by blast
next
case False
hence "low y n ≠ ?l ∧ both_member_options (treeList ! ?h ) (low y n)" using assmy
by (metis "5.IH"(1) "5.hyps"(2) ‹?newlist ! high y n = vebt_delete (treeList ! high (summin * 2 ^ n + lx) n) (low (summin * 2 ^ n + lx) n)› ‹vebt_member (treeList ! summin) lx› ‹summin < 2 ^ m› high_inv inthall member_bound member_def)
then show ?thesis
by (metis "5.hyps"(2) "5.hyps"(9) Suc_1 Suc_leD True ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹mi ≤ x ∧ x ≤ ma› ‹x = mi› both_member_options_from_chilf_to_complete_tree dp leD mimapr)
qed
next
case False
hence "?newlist ! (high y n) = treeList !(high y n)"
using "5.hyps"(2) ‹length treeList = length ?newlist› assmy nothprolist by presburger
hence "both_member_options (treeList !(high y n)) (low y n)"
using assmy by presburger
moreover have "x ≠ y"
by (metis "5.hyps"(1) "5.hyps"(4) "5.hyps"(9) ‹invar_vebt (treeList ! summin) n› ‹x < 2 ^ deg› ‹x = mi› calculation deg_not_0 exp_split_high_low(1) mimapr not_less_iff_gr_or_eq)
moreover have "high y n < length ?newlist" using assmy by blast
moreover hence "high y n < length treeList"
using ‹length treeList = length ?newlist› by presburger
ultimately show ?thesis
by (metis One_nat_def Suc_leD ‹deg div 2 = n› both_member_options_from_chilf_to_complete_tree dp numerals(2))
qed
qed
ultimately show ?thesis
using aaaa by fastforce
qed
qed
moreover have "(x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y)⟹
both_member_options ?delsimp y"
proof-
assume assm: "x ≠ y ∧ both_member_options (Node (Some (mi, ma)) deg treeList summary) y"
hence abcv:"y = mi ∨ y = ma ∨ ( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n))"
by (metis Suc_1 ‹deg div 2 = n› add_leD1 both_member_options_from_complete_tree_to_child member_inv plus_1_eq_Suc tvalid valid_member_both_member_options)
thus " both_member_options ?delsimp y"
proof-
have "y = mi ⟹ ?thesis"
using ‹x = mi› assm by blast
moreover have " y = ma ⟹ ?thesis"
by (smt (z3) Suc_1 Suc_le_D both_member_options_def dp membermima.simps(4))
moreover have " ( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n))
⟹ ?thesis"
proof-
assume myass: "( high y n < length treeList ∧ both_member_options (treeList ! (high y n)) (low y n)) "
thus ?thesis
proof(cases "high y n = ?h")
case True
then show ?thesis
proof(cases "low y n = ?l")
case True
then show ?thesis
by (smt (z3) "5.hyps"(3) "5.hyps"(4) Suc_1 ‹deg div 2 = n› ‹length treeList = length (treeList [high (summin * 2 ^ n + lx) n := vebt_delete (treeList ! high (summin * 2 ^ n + lx) n) (low (summin * 2 ^ n + lx) n)])› add_Suc_right add_leD1 bit_split_inv both_member_options_def both_member_options_from_chilf_to_complete_tree dp membermima.simps(4) myass nth_list_update_neq plus_1_eq_Suc)
next
case False
hence "low y n ≠ ?l" by simp
hence pp:"?newlist ! ?h = ?newnode"
using hprolist by blast
hence "invar_vebt (treeList ! ?h) n"
by (metis "5.IH"(1) ‹high ?xn n < length treeList› inthall member_def)
hence "both_member_options ?newnode (low y n)"
by (metis "5.IH"(1) True ‹high ?xn n < length treeList› ‹low y n ≠ low ?xn n› in_set_member inthall myass)
then show ?thesis
by (metis One_nat_def Suc_leD True ‹deg div 2 = n› ‹high (summin * 2 ^ n + lx) n < length treeList› ‹length treeList = length ?newlist› both_member_options_from_chilf_to_complete_tree dp numerals(2) pp)
qed
next
case False
have pp:"?newlist ! (high y n) = treeList ! (high y n)"
using nothprolist[of "high y n"] False "5.hyps"(2) myass by presburger
then show ?thesis
by (metis One_nat_def Suc_leD ‹deg div 2 = n› ‹length treeList = length ?newlist› abcv both_member_options_from_chilf_to_complete_tree calculation(1) calculation(2) dp numerals(2))
qed
qed
then show ?thesis
using abcv calculation(1) calculation(2) by fastforce
qed
qed
ultimately show ?thesis by metis
qed
qed
qed
qed
qed
end
corollary "invar_vebt t n ⟹ both_member_options t x ⟹ x ≠ y ⟹ both_member_options (vebt_delete t y) x"
using dele_bmo_cont_corr by blast
corollary "invar_vebt t n ⟹ both_member_options t x ⟹ ¬ both_member_options (vebt_delete t x) x "
by (simp add: dele_bmo_cont_corr)
corollary "invar_vebt t n ⟹ both_member_options (vebt_delete t y) x ⟹ both_member_options t x ∧ x ≠ y"
using dele_bmo_cont_corr by blast
end
end