Theory VEBT_Pred
theory VEBT_Pred imports VEBT_MinMax VEBT_Insert
begin
section ‹The Predecessor Operation›
definition is_pred_in_set :: "nat set ⇒ nat ⇒ nat ⇒ bool" where
"is_pred_in_set xs x y = (y ∈ xs ∧ y < x ∧ (∀ z ∈ xs. (z < x ⟶ z ≤ y)))"
context VEBT_internal begin
subsection ‹Lemmas on Sets and Predecessorship›
corollary pred_member: "is_pred_in_set (set_vebt' t) x y = (vebt_member t y ∧ y < x ∧ (∀ z. vebt_member t z ∧ z < x ⟶ z ≤ y))"
using is_pred_in_set_def set_vebt'_def by auto
lemma "finite (A:: nat set) ⟹ A ≠ {}⟹ Max A ∈ A"
proof(induction A rule: finite.induct)
case emptyI
then show ?case by blast
next
case (insertI A a)
then show ?case
by (meson Max_in finite_insert)
qed
lemma obtain_set_pred: assumes "(x::nat) > z " and "min_in_set A z" and "finite A" shows "∃ y. is_pred_in_set A x y"
proof-
have "{y ∈ A. y < x} ≠ {}"
using assms(1) assms(2) min_in_set_def by auto
hence "Max {y ∈ A. y < x} ∈ {y ∈ A. y < x}"
by (metis (full_types) Max_eq_iff finite_M_bounded_by_nat)
moreover have "i ∈ A⟹ i < x ⟹ i ≤ Max {y ∈ A. y < x} " for i by simp
ultimately have "is_pred_in_set A x (Max {y ∈ A. y < x})"
using is_pred_in_set_def by auto
then show?thesis by auto
qed
lemma pred_none_empty: assumes "(∄ x. is_pred_in_set (xs) a x)" and "finite xs"shows "¬ (∃ x ∈ xs. ord_class.less x a)"
proof-
have "∃ x ∈ xs. ord_class.less x a ⟹ False"
proof-
assume "∃ x ∈ xs. ord_class.less x a"
hence "{x ∈ xs. ord_class.less x a} ≠ {}" by auto
hence "Max {y ∈ xs. y < a} ∈ {y ∈ xs. y < a}"
by (metis (full_types) Max_eq_iff finite_M_bounded_by_nat)
moreover hence "i ∈ xs ⟹ ord_class.less i a⟹
ord_class.less_eq i (Max {y ∈ xs. ord_class.less y a}) " for i
by (simp add: assms(2))
ultimately have "is_pred_in_set xs a (Max {y ∈ xs. y < a})"
using is_pred_in_set_def by auto
then show False
using assms(1) by blast
qed
then show ?thesis by blast
qed
end
subsection ‹The actual Function for Predecessor Search›
context begin
interpretation VEBT_internal .
fun vebt_pred :: "VEBT ⇒ nat ⇒ nat option" where
"vebt_pred (Leaf _ _) 0 = None"|
"vebt_pred (Leaf a _) (Suc 0) = (if a then Some 0 else None)"|
"vebt_pred (Leaf a b) _ = (if b then Some 1 else if a then Some 0 else None)"|
"vebt_pred (Node None _ _ _) _ = None"|
"vebt_pred (Node _ 0 _ _) _ = None"|
"vebt_pred (Node _ (Suc 0) _ _) _ = None"|
"vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = (
if x > ma then Some ma
else (let l = low x (deg div 2); h = high x (deg div 2) in
if h < length treeList then
let minlow = vebt_mint (treeList ! h) in (
if minlow ≠ None ∧ (Some l >⇩o minlow) then
Some (2^(deg div 2)) *⇩o Some h +⇩o vebt_pred (treeList ! h) l
else let pr = vebt_pred summary h in
if pr = None then (
if x > mi then Some mi
else None)
else Some (2^(deg div 2)) *⇩o pr +⇩o vebt_maxt (treeList ! the pr) )
else None))"
end
context VEBT_internal begin
subsection ‹Auxiliary Lemmas›
lemma pred_max:
assumes "deg ≥ 2" and "(x::nat) > ma"
shows "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some ma"
by (metis VEBT_Pred.vebt_pred.simps(7) add_2_eq_Suc assms(1) assms(2) le_add_diff_inverse)
lemma pred_lesseq_max:
assumes "deg ≥ 2" and "(x::nat) ≤ ma"
shows "vebt_pred (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 minlow = vebt_mint (treeList ! h) in
(if minlow ≠ None ∧ (Some l >⇩o minlow) then
Some (2^(deg div 2)) *⇩o Some h +⇩o vebt_pred (treeList ! h) l
else let pr = vebt_pred summary h in
if pr = None then (if x > mi then Some mi else None)
else Some (2^(deg div 2)) *⇩o pr +⇩o vebt_maxt (treeList ! the pr) )
else None)"
by (smt VEBT_Pred.vebt_pred.simps(7) add_numeral_left assms(1) assms(2) leD le_add_diff_inverse numerals(1) plus_1_eq_Suc semiring_norm(2))
lemma pred_list_to_short:
assumes "deg ≥ 2" and "ord_class.less_eq x ma" and " high x (deg div 2) ≥ length treeList"
shows "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = None"
by (simp add: assms(1) assms(2) assms(3) leD pred_lesseq_max)
lemma pred_less_length_list:
assumes "deg ≥ 2" and "ord_class.less_eq x ma" and " high x (deg div 2) < length treeList"
shows
"vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = (let l = low x (deg div 2); h = high x (deg div 2); minlow = vebt_mint (treeList ! h) in
(if minlow ≠ None ∧ (Some l >⇩o minlow) then
Some (2^(deg div 2)) *⇩o Some h +⇩o vebt_pred (treeList ! h) l
else let pr = vebt_pred summary h in
if pr = None then (if x > mi then Some mi else None)
else Some (2^(deg div 2)) *⇩o pr +⇩o vebt_maxt (treeList ! the pr) ))"
by (simp add: assms(1) assms(2) assms(3) pred_lesseq_max)
subsection ‹Correctness Proof›
theorem pred_corr: "invar_vebt t n ⟹ vebt_pred t x = Some px == is_pred_in_set (set_vebt' t) x px"
proof(induction t n arbitrary: x px rule: invar_vebt.induct)
case (1 a b)
then show ?case
proof(cases x)
case 0
then show ?thesis
by (simp add: is_pred_in_set_def)
next
case (Suc sucX)
hence "x ≥ 0 ∧ x = Suc sucX" by auto
then show ?thesis
proof(cases sucX)
case 0
then show ?thesis
by (simp add: Suc pred_member)
next
case (Suc nat)
hence "x≥ 2"
by (simp add: ‹0 ≤ x ∧ x = Suc sucX›)
then show ?thesis
proof(cases b)
case True
hence "vebt_pred (Leaf a b) x = Some 1"
by (simp add: Suc ‹0 ≤ x ∧ x = Suc sucX›)
moreover have "is_pred_in_set (set_vebt' (Leaf a b)) x 1"
by (simp add: Suc True ‹0 ≤ x ∧ x = Suc sucX› pred_member)
ultimately show ?thesis
using pred_member by auto
next
case False
hence "b = False" by simp
then show ?thesis
proof(cases a)
case True
hence "vebt_pred (Leaf a b) x = Some 0"
by (simp add: False Suc ‹0 ≤ x ∧ x = Suc sucX›)
moreover have "is_pred_in_set (set_vebt' (Leaf a b)) x 0"
by (simp add: False True ‹0 ≤ x ∧ x = Suc sucX› pred_member)
ultimately show ?thesis
by (metis False VEBT_Member.vebt_member.simps(1) option.sel pred_member)
next
case False
then show ?thesis
by (simp add: Suc ‹0 ≤ x ∧ x = Suc sucX› pred_member)
qed
qed
qed
qed
next
case (2 treeList n summary m deg)
then show ?case
by (simp add: pred_member)
next
case (3 treeList n summary m deg)
then show ?case
by (simp add: pred_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))
moreover hence thisvalid:"invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg"
using 4 invar_vebt.intros(4)[of treeList n summary m] by blast
ultimately have "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 > ma")
case True
hence 0: "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some ma"
by (simp add: ‹2 ≤ deg› pred_max)
have 1:"ma = the (vebt_maxt (Node (Some (mi, ma)) deg treeList summary))" by simp
hence "ma ∈ 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 < ma ⟹ y ≤ x)" for y by blast
hence 4: "∀ y ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary). y < ma ⟶ y ≤ x" by blast
hence "is_pred_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x ma"
by (metis "4.hyps"(9) True ‹ma ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary)› less_or_eq_imp_le mem_Collect_eq member_inv pred_member set_vebt'_def)
then show ?thesis
by (metis "0" option.sel leD le_less_Suc_eq not_less_eq pred_member)
next
case False
hence "x ≤ ma"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 ?minlow = "vebt_mint (treeList ! ?h)"
let ?pr = "vebt_pred summary ?h"
have 1:"vebt_pred (Node (Some (mi, ma)) deg treeList summary) x =
(if ?minlow ≠ None ∧ (Some ?l >⇩o ?minlow) then
Some (2^(deg div 2)) *⇩o Some ?h +⇩o vebt_pred (treeList ! ?h) ?l
else let pr = vebt_pred summary ?h in
if pr = None then (if x > mi then Some mi else None)
else Some (2^(deg div 2)) *⇩o pr +⇩o vebt_maxt (treeList ! the pr) )"
by (smt True ‹2 ≤ deg› ‹x ≤ ma› pred_less_length_list)
then show ?thesis
proof(cases "?minlow ≠ None ∧ (Some ?l >⇩o ?minlow)")
case True
then obtain minl where 00:"(Some minl = ?minlow) ∧ ?l > minl" by auto
have 01:"invar_vebt ((treeList ! ?h)) n ∧ (treeList ! ?h) ∈ set treeList "
by (simp add: "4.hyps"(1) "4.hyps"(4) "4.hyps"(5) ‹deg div 2 = n› ‹high x n < 2 ^ n ∧ low x n < 2 ^ n›)
have 02:"vebt_member ((treeList ! ?h)) minl"
using "00" "01" mint_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 predy where 04:"is_pred_in_set (set_vebt' (treeList ! ?h)) ?l predy"
using "00" "01" mint_corr obtain_set_pred by fastforce
hence 05:"Some predy = vebt_pred (treeList ! ?h) ?l" using 4(1) 01 by force
hence "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some (2^(deg div 2)* ?h + predy) "
using "1" True add_def mul_def option_shift.simps(3) by metis
hence 06: "predy ∈ set_vebt' (treeList ! ?h)"
using "04" is_pred_in_set_def by blast
hence 07: "predy < 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 pred_member by auto
let ?y = "2^(deg div 2)* ?h + predy"
have 08: "vebt_member (treeList ! ?h) predy"
using "06" set_vebt'_def by auto
hence 09: "both_member_options (treeList ! ?h) predy"
using "01" both_member_options_equiv_member by blast
have 10: "high ?y (deg div 2) = ?h ∧ low ?y (deg div 2) = predy"
by (simp add: "07" high_inv low_inv mult.commute)
hence 14:"both_member_options (Node (Some (mi, ma)) deg treeList summary) ?y"
by (metis "07" "09" "4.hyps"(4) "4.hyps"(5) Suc_1 ‹2 ≤ deg› ‹deg div 2 = n› add_leD1 both_member_options_from_chilf_to_complete_tree plus_1_eq_Suc)
have 15: "vebt_member (Node (Some (mi, ma)) deg treeList summary) ?y"
using "14" thisvalid valid_member_both_member_options by blast
have 16: "Some ?y = vebt_pred (Node (Some (mi, ma)) deg treeList summary) x"
by (simp add: ‹vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some (2 ^ (deg div 2) * high x (deg div 2) + predy)›)
have 17: "x = ?h * 2^(deg div 2) + ?l"
using bit_concat_def bit_split_inv by auto
have 18: "x - ?y = ?h * 2^(deg div 2) + ?l -?h * 2^(deg div 2) - predy "
by (metis "17" diff_diff_add mult.commute)
hence 19: "?y < x"
using "04" "17" mult.commute nat_add_left_cancel_less pred_member by fastforce
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 0000: "high z (deg div 2) = high x (deg div 2)" by simp
then show ?thesis
proof(cases "z = mi")
case True
then show ?thesis
using "15" vebt_mint.simps(3) mint_corr_help thisvalid by blast
next
case False
hence ad:"vebt_member (treeList ! ?h) (low z (deg div 2))"
using vebt_member.simps(5)[of mi ma "deg-2" treeList summary z]
by (metis True ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z› ‹x ≤ ma› ‹z < x› leD member_inv)
have "is_pred_in_set (set_vebt' (treeList ! ?h)) ?l predy"
using "04" by blast
have "low z (deg div 2) < ?l"
by (metis (full_types) True ‹z < x› bit_concat_def bit_split_inv nat_add_left_cancel_less)
hence "predy ≥ low z (deg div 2)" using 04 ad unfolding is_pred_in_set_def
by (simp add: set_vebt'_def)
hence "?y ≥ z"
by (smt True bit_concat_def bit_split_inv diff_add_inverse diff_diff_add diff_is_0_eq mult.commute)
then show ?thesis by blast
qed
next
case False
hence "high z (deg div 2) < high ?y (deg div 2)"
using "10" ‹high z (deg div 2) ≤ high x (deg div 2)› by linarith
then show ?thesis
by (metis div_le_mono high_def nat_le_linear not_le)
qed
qed
hence "is_pred_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x ?y"
by (simp add: "15" "19" pred_member)
then show ?thesis using 16
by (metis eq_iff option.inject pred_member)
next
case False
hence i1:"?minlow = None ∨ ¬ (Some ?l >⇩o ?minlow)" by simp
hence 2: "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = (
if ?pr = None then (if x > mi
then Some mi
else None)
else Some (2^(deg div 2)) *⇩o ?pr +⇩o vebt_maxt (treeList ! the ?pr))"
using "1" by auto
have " invar_vebt (treeList ! ?h) n"
by (metis "4"(1) True inthall member_def)
hence 33:"∄ u. vebt_member (treeList ! ?h) u ∧ u < ?l"
proof(cases "?minlow = None")
case True
then show ?thesis using mint_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 minilow where "?minlow =Some minilow"
using False by blast
hence "minilow ≥ ?l"
using "i1" by auto
then show ?thesis
by (meson ‹vebt_mint (treeList ! high x (deg div 2)) = Some minilow› ‹invar_vebt (treeList ! high x (deg div 2)) n› leD less_le_trans mint_corr_help)
qed
then show ?thesis
proof(cases "?pr= None")
case True
hence "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = (if x > mi then Some mi else None)"
by (simp add: "2")
hence "∄ i. is_pred_in_set (set_vebt' summary) ?h i"
using "4.hyps"(3) True by force
hence "∄ i. i < ?h ∧ vebt_member summary i " using pred_none_empty[of "set_vebt' summary" ?h]
proof -
{ fix nn :: nat
have "∀n. ((is_pred_in_set (Collect (vebt_member summary)) (high x (deg div 2)) esk1_0 ∨ infinite (Collect (vebt_member summary))) ∨ n ∉ Collect (vebt_member summary)) ∨ ¬ n < high x (deg div 2)"
using ‹∄i. is_pred_in_set (set_vebt' summary) (high x (deg div 2)) i› pred_none_empty set_vebt'_def by auto
then have "¬ nn < high x (deg div 2) ∨ ¬ vebt_member summary nn"
by (metis (no_types) "4.hyps"(2) ‹∄i. is_pred_in_set (set_vebt' summary) (high x (deg div 2)) i› mem_Collect_eq set_vebt'_def set_vebt_finite) }
then show ?thesis
by blast
qed
then show ?thesis
proof(cases "x > mi")
case True
hence "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some mi"
by (simp add: ‹vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = (if mi < x then Some mi else None)›)
have "(vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ z > mi) ⟹ False" for z
proof-
assume "vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ z > mi"
hence "vebt_member ( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using ‹x ≤ ma› member_inv not_le by blast
moreover hence "high z (deg div 2) < 2^m"
using "4.hyps"(4) ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ mi < z› ‹x ≤ ma› member_inv by fastforce
moreover hence "invar_vebt (treeList ! (high z (deg div 2))) n" using 4(1)
by (simp add: "4.hyps"(4))
ultimately have "vebt_member summary (high z (deg div 2))" using 4(7)
using "4.hyps"(2) both_member_options_equiv_member by blast
have "(high z (deg div 2)) ≤ ?h"
by (simp add: ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ mi < z› div_le_mono high_def less_or_eq_imp_le)
then show False
by (metis "33" ‹¬ (∃i<high x (deg div 2). vebt_member summary i)› ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ mi < z› ‹vebt_member (treeList ! high z (deg div 2)) (low z (deg div 2))› ‹vebt_member summary (high z (deg div 2))› bit_concat_def bit_split_inv le_neq_implies_less nat_add_left_cancel_less)
qed
hence "is_pred_in_set (set_vebt' ((Node (Some (mi, ma)) deg treeList summary))) x mi"
by (metis VEBT_Member.vebt_member.simps(5) True ‹2 ≤ deg› add_2_eq_Suc le_add_diff_inverse le_less_linear pred_member)
then show ?thesis
by (metis ‹vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some mi› ‹x ≤ ma› option.sel leD member_inv pred_member)
next
case False
hence "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = None"
by (simp add: "2" True)
then show ?thesis
by (metis (full_types) False less_trans member_inv option.distinct(1) pred_max pred_member)
qed
next
case False
hence fst:"vebt_pred (Node (Some (mi, ma)) deg treeList summary) x =
Some (2^(deg div 2)) *⇩o ?pr +⇩o vebt_maxt (treeList ! the ?pr)"
using "2" by presburger
obtain pr where "?pr = Some pr"
using False by blast
hence "is_pred_in_set (set_vebt' summary) ?h pr"
using "4.hyps"(3) by blast
hence "vebt_member summary pr"
using pred_member by blast
hence "both_member_options summary pr"
using "4.hyps"(2) both_member_options_equiv_member by auto
hence "pr < 2^m"
using "4.hyps"(2) ‹vebt_member summary pr› member_bound by blast
hence "∃ maxy. both_member_options (treeList ! pr) maxy"
using "4.hyps"(7) ‹both_member_options summary pr› by blast
hence fgh:"set_vebt' (treeList ! pr) ≠ {}"
by (metis "4.hyps"(1) "4.hyps"(2) "4.hyps"(4) ‹vebt_member summary pr› empty_Collect_eq member_bound nth_mem set_vebt'_def valid_member_both_member_options)
hence "invar_vebt (treeList ! the ?pr) n"
by (simp add: "4.hyps"(1) "4.hyps"(4) ‹pr < 2 ^ m› ‹vebt_pred summary (high x (deg div 2)) = Some pr›)
then obtain maxy where "Some maxy = vebt_maxt (treeList ! pr)"
by (metis ‹vebt_pred summary (high x (deg div 2)) = Some pr› fgh option.sel vebt_maxt.elims maxt_corr_help_empty)
hence "Some maxy = vebt_maxt (treeList ! the ?pr)"
by (simp add: ‹vebt_pred summary (high x (deg div 2)) = Some pr›)
hence "max_in_set (set_vebt' (treeList ! the ?pr)) maxy"
using ‹invar_vebt (treeList ! the (vebt_pred summary (high x (deg div 2)))) n› maxt_corr by auto
hence scmem:"vebt_member (treeList ! the ?pr) maxy"
using ‹Some maxy = vebt_maxt (treeList ! the (vebt_pred summary (high x (deg div 2))))› ‹invar_vebt (treeList ! the (vebt_pred summary (high x (deg div 2)))) n› maxt_member by force
let ?res = "Some (2^(deg div 2)) *⇩o ?pr +⇩o vebt_maxt (treeList ! the ?pr)"
obtain res where snd: "res = the ?res" by blast
hence "res = 2^(deg div 2) * pr + maxy"
by (metis ‹Some maxy = vebt_maxt (treeList ! pr)› ‹vebt_pred summary (high x (deg div 2)) = Some pr› add_def option.sel mul_def option_shift.simps(3))
have "high res (deg div 2) = pr"
by (metis ‹deg div 2 = n› ‹res = 2 ^ (deg div 2) * pr + maxy› ‹invar_vebt (treeList ! the ?pr) n› high_inv member_bound mult.commute scmem)
hence "res < x"
by (metis ‹is_pred_in_set (set_vebt' summary) (high x (deg div 2)) pr› div_le_mono high_def pred_member verit_comp_simplify1(3))
have "both_member_options (treeList ! (high res (deg div 2))) (low res (deg div 2))"
by (metis ‹deg div 2 = n› ‹high res (deg div 2) = pr› ‹vebt_pred summary (high x (deg div 2)) = Some pr› ‹res = 2 ^ (deg div 2) * pr + maxy› ‹invar_vebt (treeList ! the (vebt_pred summary (high x (deg div 2)))) n› both_member_options_equiv_member option.sel low_inv member_bound mult.commute scmem)
have "both_member_options (Node (Some (mi, ma)) deg treeList summary) res"
by (metis "4.hyps"(2) "4.hyps"(4) "4.hyps"(6) ‹1 ≤ n› ‹both_member_options (treeList ! high res (deg div 2)) (low res (deg div 2))› ‹high res (deg div 2) = pr› ‹vebt_member summary pr› both_member_options_from_chilf_to_complete_tree member_bound trans_le_add1)
hence "vebt_member (Node (Some (mi, ma)) deg treeList summary) res"
using thisvalid valid_member_both_member_options by auto
hence "res > mi"
by (metis "4.hyps"(11) ‹both_member_options (treeList ! high res (deg div 2)) (low res (deg div 2))› ‹deg div 2 = n› ‹high res (deg div 2) = pr› ‹pr < 2 ^ m› ‹res < x› ‹x ≤ ma› less_le_trans member_inv)
hence "res < ma"
using ‹res < x› ‹x ≤ ma› less_le_trans by blast
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 ≠ ma"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x› ‹x ≤ ma› leD by blast
hence "mi ≠ ma"
by (metis ‹mi < res› ‹res < x› ‹x ≤ ma› leD less_trans)
hence "z < 2^deg"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x› member_bound thisvalid by blast
hence abc:"invar_vebt (treeList ! (high z (deg div 2))) n"
by (metis "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) in_set_member inthall)
then show "z ≤ res"
proof(cases "z = mi")
case True
then show ?thesis
using ‹mi < res› by auto
next
case False
hence abe:"vebt_member( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using "20" ‹z ≠ ma› by blast
hence abh:"vebt_member summary (high z (deg div 2))"
by (metis "20" "4.hyps"(2) "4.hyps"(4) "4.hyps"(7) False ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x› ‹x ≤ ma› abc both_member_options_equiv_member not_le)
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) > pr ⟹ False"
proof-
assume "high z(deg div 2) > pr"
hence "vebt_member summary (high z(deg div 2))"
using abh by blast
have aaaa:"?h ≤ high z(deg div 2)"
by (meson ‹is_pred_in_set (set_vebt' summary) (high x (deg div 2)) pr› ‹pr < high z (deg div 2)› abh leD not_le_imp_less pred_member)
have bbbb:"?h ≥ high z(deg div 2)"
by (simp add: ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x› div_le_mono dual_order.strict_implies_order high_def)
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
hence "(low z (deg div 2)) < ?l"
by (metis ‹high x (deg div 2) = high z (deg div 2)› ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x› add_le_cancel_left div_mult_mod_eq high_def less_le low_def)
then show False
using "33" ‹vebt_member (treeList ! high x (deg div 2)) (low z (deg div 2))› by blast
qed
hence "high z(deg div 2) ≤ pr"
using not_less by blast
then show " z ≤ res"
proof(cases "high z(deg div 2) = pr")
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) ≤ maxy"
using True ‹Some maxy = vebt_maxt (treeList ! pr)› abc abe maxt_corr_help by auto
hence "z ≤ res"
by (metis True ‹res = 2 ^ (deg div 2) * pr + maxy› add_le_cancel_left div_mult_mod_eq high_def low_def mult.commute)
then show ?thesis by simp
next
case False
hence "high z(deg div 2) < pr"
by (simp add: ‹high z (deg div 2) ≤ pr› less_le)
then show ?thesis
by (metis ‹high res (deg div 2) = pr› div_le_mono high_def leD linear)
qed
qed
qed
hence "is_pred_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x res"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) res› ‹res < x› pred_member by presburger
then show ?thesis using fst snd
by (metis ‹Some maxy = vebt_maxt (treeList ! the (vebt_pred summary (high x (deg div 2))))› ‹vebt_pred summary (high x (deg div 2)) = Some pr› ‹res = 2 ^ (deg div 2) * pr + maxy› add_shift dual_order.eq_iff mul_shift pred_member)
qed
qed
next
case False
then show ?thesis
by (metis "4.hyps"(10) "4.hyps"(5) "4.hyps"(6) ‹1 ≤ n› ‹deg div 2 = n› ‹length treeList = 2 ^ n› ‹x ≤ ma› exp_split_high_low(1) le_less_trans le_neq_implies_less not_less not_less_zero zero_neq_one)
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))
moreover hence thisvalid:"invar_vebt (Node (Some (mi, ma)) deg treeList summary) deg"
using 5 invar_vebt.intros(5)[of treeList n summary m] by blast
ultimately have "deg div 2 =n" by simp
then show ?case
proof(cases "x > ma")
case True
hence 0: "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some ma"
by (simp add: ‹2 ≤ deg› pred_max)
have 1:"ma = the (vebt_maxt (Node (Some (mi, ma)) deg treeList summary))" by simp
hence "ma ∈ 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 < ma ⟹ y ≤ x)" for y by blast
hence 4: "∀ y ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary). y < ma ⟶ y ≤ x" by blast
hence "is_pred_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x ma"
by (metis "5.hyps"(9) True ‹ma ∈ set_vebt' (Node (Some (mi, ma)) deg treeList summary)› less_or_eq_imp_le mem_Collect_eq member_inv pred_member set_vebt'_def)
then show ?thesis
by (metis "0" option.sel leD le_less_Suc_eq not_less_eq pred_member)
next
case False
hence "x ≤ ma"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: ‹deg div 2 = n› ‹length treeList = 2 ^ m› low_def)
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
let ?minlow = "vebt_mint (treeList ! ?h)"
let ?pr = "vebt_pred summary ?h"
have 1:"vebt_pred (Node (Some (mi, ma)) deg treeList summary) x =
(if ?minlow ≠ None ∧ (Some ?l >⇩o ?minlow) then
Some (2^(deg div 2)) *⇩o Some ?h +⇩o vebt_pred (treeList ! ?h) ?l
else let pr = vebt_pred summary ?h in
if pr = None then (if x > mi then Some mi else None)
else Some (2^(deg div 2)) *⇩o pr +⇩o vebt_maxt (treeList ! the pr) )"
by (smt True ‹2 ≤ deg› ‹x ≤ ma› pred_less_length_list)
then show ?thesis
proof(cases "?minlow ≠ None ∧ (Some ?l >⇩o ?minlow)")
case True
then obtain minl where 00:"(Some minl = ?minlow) ∧ ?l > minl" by auto
have 01:"invar_vebt ((treeList ! ?h)) n ∧ (treeList ! ?h) ∈ set treeList "
by (metis "5.hyps"(1) ‹deg div 2 = n› ‹high x n < 2 ^ m ∧ low x n < 2 ^ n› ‹length treeList = 2 ^ m ∧ invar_vebt summary m› inthall member_def)
have 02:"vebt_member ((treeList ! ?h)) minl"
using "00" "01" mint_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 predy where 04:"is_pred_in_set (set_vebt' (treeList ! ?h)) ?l predy"
using "00" "01" mint_corr obtain_set_pred by fastforce
hence 05:"Some predy = vebt_pred (treeList ! ?h) ?l" using 5(1) 01 by force
hence "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some (2^(deg div 2)* ?h + predy) "
by (metis "1" True add_def mul_def option_shift.simps(3))
hence 06: "predy ∈ set_vebt' (treeList ! ?h)"
using "04" is_pred_in_set_def by blast
hence 07: "predy < 2^(deg div 2) ∧ ?h < 2^(deg div 2 +1) ∧ deg div 2 + deg div 2 +1 = deg"
using "04" "5.hyps"(5) "5.hyps"(6) ‹high x n < 2 ^ m ∧ low x n < 2 ^ n› pred_member by force
let ?y = "2^(deg div 2)* ?h + predy"
have 08: "vebt_member (treeList ! ?h) predy"
using "06" set_vebt'_def by auto
hence 09: "both_member_options (treeList ! ?h) predy"
using "01" both_member_options_equiv_member by blast
have 10: "high ?y (deg div 2) = ?h ∧ low ?y (deg div 2) = predy"
by (simp add: "07" high_inv low_inv mult.commute)
hence 14:"both_member_options (Node (Some (mi, ma)) deg treeList summary) ?y"
using "07" "09" "5.hyps"(4) ‹deg div 2 = n› ‹high x n < 2 ^ m ∧ low x n < 2 ^ n› both_member_options_from_chilf_to_complete_tree by auto
have 15: "vebt_member (Node (Some (mi, ma)) deg treeList summary) ?y"
using "14" thisvalid valid_member_both_member_options by blast
have 16: "Some ?y = vebt_pred (Node (Some (mi, ma)) deg treeList summary) x"
by (simp add: ‹vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some (2 ^ (deg div 2) * high x (deg div 2) + predy)›)
have 17: "x = ?h * 2^(deg div 2) + ?l"
using bit_concat_def bit_split_inv by auto
have 18: "x - ?y = ?h * 2^(deg div 2) + ?l -?h * 2^(deg div 2) - predy "
by (metis "17" diff_diff_add mult.commute)
hence 19: "?y < x"
using "04" "17" mult.commute nat_add_left_cancel_less pred_member by fastforce
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 0000: "high z (deg div 2) = high x (deg div 2)" by simp
then show ?thesis
proof(cases "z = mi")
case True
then show ?thesis
by (metis "15" "5.hyps"(9) add.left_neutral le_add2 less_imp_le_nat member_inv)
next
case False
hence ad:"vebt_member (treeList ! ?h) (low z (deg div 2))"
using vebt_member.simps(5)[of mi ma "deg-2" treeList summary z]
by (metis True ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z› ‹x ≤ ma› ‹z < x› leD member_inv)
have "is_pred_in_set (set_vebt' (treeList ! ?h)) ?l predy"
using "04" by blast
have "low z (deg div 2) < ?l"
by (metis (full_types) True ‹z < x› bit_concat_def bit_split_inv nat_add_left_cancel_less)
hence "predy ≥ low z (deg div 2)" using 04 ad unfolding is_pred_in_set_def
by (simp add: set_vebt'_def)
hence "?y ≥ z"
by (smt True bit_concat_def bit_split_inv diff_add_inverse diff_diff_add diff_is_0_eq mult.commute)
then show ?thesis by blast
qed
next
case False
hence "high z (deg div 2) < high ?y (deg div 2)"
using "10" ‹high z (deg div 2) ≤ high x (deg div 2)› by linarith
then show ?thesis
by (metis div_le_mono high_def nat_le_linear not_le)
qed
qed
hence "is_pred_in_set (set_vebt'(Node (Some (mi, ma)) deg treeList summary)) x ?y"
by (simp add: "15" "19" pred_member)
then show ?thesis using 16
by (metis eq_iff option.inject pred_member)
next
case False
hence i1:"?minlow = None ∨ ¬ (Some ?l >⇩o ?minlow)" by simp
hence 2: "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = (
if ?pr = None then (if x > mi
then Some mi
else None)
else Some (2^(deg div 2)) *⇩o ?pr +⇩o vebt_maxt (treeList ! the ?pr))"
using "1" by auto
have " invar_vebt (treeList ! ?h) n"
by (metis "5"(1) True inthall member_def)
hence 33:"∄ u. vebt_member (treeList ! ?h) u ∧ u < ?l"
proof(cases "?minlow = None")
case True
then show ?thesis using mint_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 minilow where "?minlow =Some minilow"
using False by blast
hence "minilow ≥ ?l"
using "i1" by auto
then show ?thesis
by (meson ‹vebt_mint (treeList ! high x (deg div 2)) = Some minilow› ‹invar_vebt (treeList ! high x (deg div 2)) n› leD less_le_trans mint_corr_help)
qed
then show ?thesis
proof(cases "?pr= None")
case True
hence "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = (if x > mi then Some mi else None)"
by (simp add: "2")
hence "∄ i. is_pred_in_set (set_vebt' summary) ?h i"
using "5.hyps"(3) True by force
hence "∄ i. i < ?h ∧ vebt_member summary i " using pred_none_empty[of "set_vebt' summary" ?h]
proof -
{ fix nn :: nat
have "∀n. ((is_pred_in_set (Collect (vebt_member summary)) (high x (deg div 2)) esk1_0 ∨ infinite (Collect (vebt_member summary))) ∨ n ∉ Collect (vebt_member summary)) ∨ ¬ n < high x (deg div 2)"
using ‹∄i. is_pred_in_set (set_vebt' summary) (high x (deg div 2)) i› pred_none_empty set_vebt'_def by auto
then have "¬ nn < high x (deg div 2) ∨ ¬ vebt_member summary nn"
by (metis (no_types) "5.hyps"(2) ‹∄i. is_pred_in_set (set_vebt' summary) (high x (deg div 2)) i› mem_Collect_eq set_vebt'_def set_vebt_finite) }
then show ?thesis
by blast
qed
then show ?thesis
proof(cases "x > mi")
case True
hence "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some mi"
by (simp add: ‹vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = (if mi < x then Some mi else None)›)
have "(vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ z > mi) ⟹ False" for z
proof-
assume "vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ z > mi"
hence "vebt_member ( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using ‹x ≤ ma› member_inv not_le by blast
moreover hence "high z (deg div 2) < 2^m"
using "5.hyps"(4) ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ mi < z› ‹x ≤ ma› member_inv by fastforce
moreover hence "invar_vebt (treeList ! (high z (deg div 2))) n" using 5(1)
by (simp add: "5.hyps"(4))
ultimately have "vebt_member summary (high z (deg div 2))" using 5(7)
using "5.hyps"(2) both_member_options_equiv_member by blast
have "(high z (deg div 2)) ≤ ?h"
by (simp add: ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ mi < z› div_le_mono high_def less_or_eq_imp_le)
then show False
by (metis "33" ‹¬ (∃i<high x (deg div 2). vebt_member summary i)› ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x ∧ mi < z› ‹vebt_member (treeList ! high z (deg div 2)) (low z (deg div 2))› ‹vebt_member summary (high z (deg div 2))› bit_concat_def bit_split_inv le_neq_implies_less nat_add_left_cancel_less)
qed
hence "is_pred_in_set (set_vebt' ((Node (Some (mi, ma)) deg treeList summary))) x mi"
by (metis VEBT_Member.vebt_member.simps(5) True ‹2 ≤ deg› add_2_eq_Suc le_add_diff_inverse le_less_linear pred_member)
then show ?thesis
by (metis ‹vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = Some mi› ‹x ≤ ma› option.sel leD member_inv pred_member)
next
case False
hence "vebt_pred (Node (Some (mi, ma)) deg treeList summary) x = None"
by (simp add: "2" True)
then show ?thesis
by (metis (full_types) False less_trans member_inv option.distinct(1) pred_max pred_member)
qed
next
case False
hence fst:"vebt_pred (Node (Some (mi, ma)) deg treeList summary) x =
Some (2^(deg div 2)) *⇩o ?pr +⇩o vebt_maxt (treeList ! the ?pr)"
using "2" by presburger
obtain pr where "?pr = Some pr"
using False by blast
hence "is_pred_in_set (set_vebt' summary) ?h pr"
using "5.hyps"(3) by blast
hence "vebt_member summary pr"
using pred_member by blast
hence "both_member_options summary pr"
using "5.hyps"(2) both_member_options_equiv_member by auto
hence "pr < 2^m"
using "5.hyps"(2) ‹vebt_member summary pr› member_bound by blast
hence "∃ maxy. both_member_options (treeList ! pr) maxy"
using "5.hyps"(7) ‹both_member_options summary pr› by blast
hence fgh:"set_vebt' (treeList ! pr) ≠ {}"
by (metis "5.hyps"(1) "5.hyps"(4) Collect_empty_eq ‹pr < 2 ^ m› nth_mem set_vebt'_def valid_member_both_member_options)
hence "invar_vebt (treeList ! the ?pr) n"
by (simp add: "5.hyps"(1) "5.hyps"(4) ‹pr < 2 ^ m› ‹vebt_pred summary (high x (deg div 2)) = Some pr›)
then obtain maxy where "Some maxy = vebt_maxt (treeList ! pr)"
by (metis ‹vebt_pred summary (high x (deg div 2)) = Some pr› fgh option.sel vebt_maxt.elims maxt_corr_help_empty)
hence "Some maxy = vebt_maxt (treeList ! the ?pr)"
by (simp add: ‹vebt_pred summary (high x (deg div 2)) = Some pr›)
hence "max_in_set (set_vebt' (treeList ! the ?pr)) maxy"
using ‹invar_vebt (treeList ! the (vebt_pred summary (high x (deg div 2)))) n› maxt_corr by auto
hence scmem:"vebt_member (treeList ! the ?pr) maxy"
using ‹Some maxy = vebt_maxt (treeList ! the (vebt_pred summary (high x (deg div 2))))› ‹invar_vebt (treeList ! the (vebt_pred summary (high x (deg div 2)))) n› maxt_member by force
let ?res = "Some (2^(deg div 2)) *⇩o ?pr +⇩o vebt_maxt (treeList ! the ?pr)"
obtain res where snd: "res = the ?res" by blast
hence "res = 2^(deg div 2) * pr + maxy"
by (metis ‹Some maxy = vebt_maxt (treeList ! pr)› ‹vebt_pred summary (high x (deg div 2)) = Some pr› add_def option.sel mul_def option_shift.simps(3))
have "high res (deg div 2) = pr"
by (metis ‹deg div 2 = n› ‹res = 2 ^ (deg div 2) * pr + maxy› ‹invar_vebt (treeList ! the ?pr) n› high_inv member_bound mult.commute scmem)
hence "res < x"
by (metis ‹is_pred_in_set (set_vebt' summary) (high x (deg div 2)) pr› div_le_mono high_def pred_member verit_comp_simplify1(3))
have "both_member_options (treeList ! (high res (deg div 2))) (low res (deg div 2))"
by (metis ‹deg div 2 = n› ‹high res (deg div 2) = pr› ‹vebt_pred summary (high x (deg div 2)) = Some pr› ‹res = 2 ^ (deg div 2) * pr + maxy› ‹invar_vebt (treeList ! the (vebt_pred summary (high x (deg div 2)))) n› both_member_options_equiv_member option.sel low_inv member_bound mult.commute scmem)
have "both_member_options (Node (Some (mi, ma)) deg treeList summary) res"
by (metis "5.hyps"(2) "5.hyps"(4) "5.hyps"(6) ‹1 ≤ n› ‹both_member_options (treeList ! high res (deg div 2)) (low res (deg div 2))› ‹high res (deg div 2) = pr› ‹vebt_member summary pr› both_member_options_from_chilf_to_complete_tree member_bound trans_le_add1)
hence "vebt_member (Node (Some (mi, ma)) deg treeList summary) res"
using thisvalid valid_member_both_member_options by auto
hence "res > mi"
by (metis "5.hyps"(11) ‹both_member_options (treeList ! high res (deg div 2)) (low res (deg div 2))› ‹deg div 2 = n› ‹high res (deg div 2) = pr› ‹pr < 2 ^ m› ‹res < x› ‹x ≤ ma› less_le_trans member_inv)
hence "res < ma"
using ‹res < x› ‹x ≤ ma› less_le_trans by blast
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 ≠ ma"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x› ‹x ≤ ma› leD by blast
hence "mi ≠ ma"
by (metis ‹mi < res› ‹res < x› ‹x ≤ ma› leD less_trans)
hence "z < 2^deg"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x› member_bound thisvalid by blast
hence "(high z (deg div 2)) <2^m"
by (metis "5.hyps"(5) "5.hyps"(6) ‹1 ≤ n› ‹deg div 2 = n› exp_split_high_low(1) less_le_trans numeral_One zero_less_Suc zero_less_numeral)
hence abc:"invar_vebt (treeList ! (high z (deg div 2))) n"
by (simp add: "5.hyps"(1) "5.hyps"(4))
then show "z ≤ res"
proof(cases "z = mi")
case True
then show ?thesis
using ‹mi < res› by auto
next
case False
hence abe:"vebt_member( treeList ! (high z (deg div 2))) (low z (deg div 2))"
using "20" ‹z ≠ ma› by blast
hence abh:"vebt_member summary (high z (deg div 2))"
using "5.hyps"(7) ‹high z (deg div 2) < 2 ^ m› ‹length treeList = 2 ^ m ∧ invar_vebt summary m› abc both_member_options_equiv_member 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) > pr ⟹ False"
proof-
assume "high z(deg div 2) > pr"
hence "vebt_member summary (high z(deg div 2))"
using abh by blast
have aaaa:"?h ≤ high z(deg div 2)"
by (meson ‹is_pred_in_set (set_vebt' summary) (high x (deg div 2)) pr› ‹pr < high z (deg div 2)› abh leD not_le_imp_less pred_member)
have bbbb:"?h ≥ high z(deg div 2)"
by (simp add: ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x› div_le_mono dual_order.strict_implies_order high_def)
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
hence "(low z (deg div 2)) < ?l"
by (metis ‹high x (deg div 2) = high z (deg div 2)› ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) z ∧ z < x› add_le_cancel_left div_mult_mod_eq high_def less_le low_def)
then show False
using "33" ‹vebt_member (treeList ! high x (deg div 2)) (low z (deg div 2))› by blast
qed
hence "high z(deg div 2) ≤ pr"
using not_less by blast
then show " z ≤ res"
proof(cases "high z(deg div 2) = pr")
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) ≤ maxy"
using True ‹Some maxy = vebt_maxt (treeList ! pr)› abc abe maxt_corr_help by auto
hence "z ≤ res"
by (metis True ‹res = 2 ^ (deg div 2) * pr + maxy› add_le_cancel_left div_mult_mod_eq high_def low_def mult.commute)
then show ?thesis by simp
next
case False
hence "high z(deg div 2) < pr"
by (simp add: ‹high z (deg div 2) ≤ pr› less_le)
then show ?thesis
by (metis ‹high res (deg div 2) = pr› div_le_mono high_def leD linear)
qed
qed
qed
hence "is_pred_in_set (set_vebt' (Node (Some (mi, ma)) deg treeList summary)) x res"
using ‹vebt_member (Node (Some (mi, ma)) deg treeList summary) res› ‹res < x› pred_member by presburger
then show ?thesis using fst snd
by (metis ‹Some maxy = vebt_maxt (treeList ! the (vebt_pred summary (high x (deg div 2))))› ‹vebt_pred summary (high x (deg div 2)) = Some pr› ‹res = 2 ^ (deg div 2) * pr + maxy› add_shift dual_order.eq_iff mul_shift pred_member)
qed
qed
next
case False
then show ?thesis
by (metis "5.hyps"(10) "5.hyps"(4) "5.hyps"(5) "5.hyps"(6) ‹1 ≤ n› ‹deg div 2 = n› ‹x ≤ ma› exp_split_high_low(1) le_0_eq le_less_trans verit_comp_simplify1(3) zero_less_Suc zero_neq_one)
qed
qed
qed
corollary pred_empty: assumes "invar_vebt t n "
shows " (vebt_pred t x = None) = ({y. vebt_member t y ∧ y < x} = {})"
proof
show " vebt_pred t x = None ⟹ {y. vebt_member t y ∧ x > y} = {}"
proof
show "vebt_pred t x = None ⟹ {y. vebt_member t y ∧ x > y} ⊆ {}"
proof-
assume "vebt_pred t x = None"
hence "∄ y. is_pred_in_set (set_vebt' t) x y"
using assms pred_corr by force
moreover hence "is_pred_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 pred_none_empty set_vebt'_def set_vebt_finite by auto
qed
show " vebt_pred t x = None ⟹ {} ⊆ {y. vebt_member t y ∧ x > y}" by simp
qed
show " {y. vebt_member t y ∧ x > y} = {} ⟹ vebt_pred t x = None"
proof-
assume "{y. vebt_member t y ∧ x > y} = {} "
hence "is_pred_in_set (set_vebt' t) x y ⟹ False" for y
using pred_member by auto
thus "vebt_pred t x = None"
by (meson assms option_shift.elims pred_corr)
qed
qed
theorem pred_correct: "invar_vebt t n ⟹ vebt_pred t x = Some sx ⟷is_pred_in_set (set_vebt t) x sx"
by (simp add: pred_corr set_vebt_set_vebt'_valid)
lemma helpypredd:"invar_vebt t n ⟹ vebt_pred t x = Some y ⟹ y < 2^n"
using member_bound pred_corr pred_member by blast
lemma "invar_vebt t n ⟹ vebt_pred t x = Some y ⟹ y < x"
by (simp add: pred_corr pred_member)
end
end