section ‹1-2 Brother Tree Implementation of Sets›
theory Brother12_Set
imports
Cmp
Set_by_Ordered
begin
subsection ‹Data Type and Operations›
datatype 'a bro =
N0 |
N1 "'a bro" |
N2 "'a bro" 'a "'a bro" |
L2 'a |
N3 "'a bro" 'a "'a bro" 'a "'a bro"
fun inorder :: "'a bro ⇒ 'a list" where
"inorder N0 = []" |
"inorder (N1 t) = inorder t" |
"inorder (N2 l a r) = inorder l @ a # inorder r" |
"inorder (L2 a) = [a]" |
"inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3"
fun isin :: "'a bro ⇒ 'a::cmp ⇒ bool" where
"isin N0 x = False" |
"isin (N1 t) x = isin t x" |
"isin (N2 l a r) x =
(case cmp x a of
LT ⇒ isin l x |
EQ ⇒ True |
GT ⇒ isin r x)"
fun n1 :: "'a bro ⇒ 'a bro" where
"n1 (L2 a) = N2 N0 a N0" |
"n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
"n1 t = N1 t"
hide_const (open) insert
locale insert
begin
fun n2 :: "'a bro ⇒ 'a ⇒ 'a bro ⇒ 'a bro" where
"n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" |
"n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
"n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" |
"n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" |
"n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" |
"n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" |
"n2 t1 a t2 = N2 t1 a t2"
fun ins :: "'a::cmp ⇒ 'a bro ⇒ 'a bro" where
"ins x N0 = L2 x" |
"ins x (N1 t) = n1 (ins x t)" |
"ins x (N2 l a r) =
(case cmp x a of
LT ⇒ n2 (ins x l) a r |
EQ ⇒ N2 l a r |
GT ⇒ n2 l a (ins x r))"
fun tree :: "'a bro ⇒ 'a bro" where
"tree (L2 a) = N2 N0 a N0" |
"tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" |
"tree t = t"
definition insert :: "'a::cmp ⇒ 'a bro ⇒ 'a bro" where
"insert x t = tree(ins x t)"
end
locale delete
begin
fun n2 :: "'a bro ⇒ 'a ⇒ 'a bro ⇒ 'a bro" where
"n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" |
"n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) =
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) =
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) =
N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" |
"n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) =
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
"n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) =
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" |
"n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) =
N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" |
"n2 t1 a1 t2 = N2 t1 a1 t2"
fun del_min :: "'a bro ⇒ ('a × 'a bro) option" where
"del_min N0 = None" |
"del_min (N1 t) =
(case del_min t of
None ⇒ None |
Some (a, t') ⇒ Some (a, N1 t'))" |
"del_min (N2 t1 a t2) =
(case del_min t1 of
None ⇒ Some (a, N1 t2) |
Some (b, t1') ⇒ Some (b, n2 t1' a t2))"
fun del :: "'a::cmp ⇒ 'a bro ⇒ 'a bro" where
"del _ N0 = N0" |
"del x (N1 t) = N1 (del x t)" |
"del x (N2 l a r) =
(case cmp x a of
LT ⇒ n2 (del x l) a r |
GT ⇒ n2 l a (del x r) |
EQ ⇒ (case del_min r of
None ⇒ N1 l |
Some (b, r') ⇒ n2 l b r'))"
fun tree :: "'a bro ⇒ 'a bro" where
"tree (N1 t) = t" |
"tree t = t"
definition delete :: "'a::cmp ⇒ 'a bro ⇒ 'a bro" where
"delete a t = tree (del a t)"
end
subsection ‹Invariants›
fun B :: "nat ⇒ 'a bro set"
and U :: "nat ⇒ 'a bro set" where
"B 0 = {N0}" |
"B (Suc h) = { N2 t1 a t2 | t1 a t2.
t1 ∈ B h ∪ U h ∧ t2 ∈ B h ∨ t1 ∈ B h ∧ t2 ∈ B h ∪ U h}" |
"U 0 = {}" |
"U (Suc h) = N1 ` B h"
abbreviation "T h ≡ B h ∪ U h"
fun Bp :: "nat ⇒ 'a bro set" where
"Bp 0 = B 0 ∪ L2 ` UNIV" |
"Bp (Suc 0) = B (Suc 0) ∪ {N3 N0 a N0 b N0|a b. True}" |
"Bp (Suc(Suc h)) = B (Suc(Suc h)) ∪
{N3 t1 a t2 b t3 | t1 a t2 b t3. t1 ∈ B (Suc h) ∧ t2 ∈ U (Suc h) ∧ t3 ∈ B (Suc h)}"
fun Um :: "nat ⇒ 'a bro set" where
"Um 0 = {}" |
"Um (Suc h) = N1 ` T h"
subsection "Functional Correctness Proofs"
subsubsection "Proofs for isin"
lemma
"t ∈ T h ⟹ sorted(inorder t) ⟹ isin t x = (x ∈ elems(inorder t))"
by(induction h arbitrary: t) (fastforce simp: elems_simps1 split: if_splits)+
lemma isin_set: "t ∈ T h ⟹
sorted(inorder t) ⟹ isin t x = (x ∈ elems(inorder t))"
by(induction h arbitrary: t) (auto simp: elems_simps2 split: if_splits)
subsubsection "Proofs for insertion"
lemma inorder_n1: "inorder(n1 t) = inorder t"
by(induction t rule: n1.induct) (auto simp: sorted_lems)
context insert
begin
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems)
lemma inorder_tree: "inorder(tree t) = inorder t"
by(cases t) auto
lemma inorder_ins: "t ∈ T h ⟹
sorted(inorder t) ⟹ inorder(ins a t) = ins_list a (inorder t)"
by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2)
lemma inorder_insert: "t ∈ T h ⟹
sorted(inorder t) ⟹ inorder(insert a t) = ins_list a (inorder t)"
by(simp add: insert_def inorder_ins inorder_tree)
end
subsubsection ‹Proofs for deletion›
context delete
begin
lemma inorder_tree: "inorder(tree t) = inorder t"
by(cases t) auto
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r"
by(induction l a r rule: n2.induct) (auto)
lemma inorder_del_min:
"t ∈ T h ⟹ (del_min t = None ⟷ inorder t = []) ∧
(del_min t = Some(a,t') ⟶ inorder t = a # inorder t')"
by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits)
lemma inorder_del:
"t ∈ T h ⟹ sorted(inorder t) ⟹ inorder(del x t) = del_list x (inorder t)"
by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
inorder_del_min[OF UnI1] inorder_del_min[OF UnI2] split: option.splits)
lemma inorder_delete:
"t ∈ T h ⟹ sorted(inorder t) ⟹ inorder(delete x t) = del_list x (inorder t)"
by(simp add: delete_def inorder_del inorder_tree)
end
subsection ‹Invariant Proofs›
subsubsection ‹Proofs for insertion›
lemma n1_type: "t ∈ Bp h ⟹ n1 t ∈ T (Suc h)"
by(cases h rule: Bp.cases) auto
context insert
begin
lemma tree_type: "t ∈ Bp h ⟹ tree t ∈ B h ∪ B (Suc h)"
by(cases h rule: Bp.cases) auto
lemma n2_type:
"(t1 ∈ Bp h ∧ t2 ∈ T h ⟶ n2 t1 a t2 ∈ Bp (Suc h)) ∧
(t1 ∈ T h ∧ t2 ∈ Bp h ⟶ n2 t1 a t2 ∈ Bp (Suc h))"
apply(cases h rule: Bp.cases)
apply (auto)[2]
apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+
done
lemma Bp_if_B: "t ∈ B h ⟹ t ∈ Bp h"
by (cases h rule: Bp.cases) simp_all
text{* An automatic proof: *}
lemma
"(t ∈ B h ⟶ ins x t ∈ Bp h) ∧ (t ∈ U h ⟶ ins x t ∈ T h)"
apply(induction h arbitrary: t)
apply (simp)
apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
done
text{* A detailed proof: *}
lemma ins_type:
shows "t ∈ B h ⟹ ins x t ∈ Bp h" and "t ∈ U h ⟹ ins x t ∈ T h"
proof(induction h arbitrary: t)
case 0
{ case 1 thus ?case by simp
next
case 2 thus ?case by simp }
next
case (Suc h)
{ case 1
then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
t1: "t1 ∈ T h" and t2: "t2 ∈ T h" and t12: "t1 ∈ B h ∨ t2 ∈ B h"
by auto
{ assume "x < a"
hence "?case ⟷ n2 (ins x t1) a t2 ∈ Bp (Suc h)" by simp
also have "…"
proof cases
assume "t1 ∈ B h"
with t2 show ?thesis by (simp add: Suc.IH(1) n2_type)
next
assume "t1 ∉ B h"
hence 1: "t1 ∈ U h" and 2: "t2 ∈ B h" using t1 t12 by auto
show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type)
qed
finally have ?case .
}
moreover
{ assume "a < x"
hence "?case ⟷ n2 t1 a (ins x t2) ∈ Bp (Suc h)" by simp
also have "…"
proof cases
assume "t2 ∈ B h"
with t1 show ?thesis by (simp add: Suc.IH(1) n2_type)
next
assume "t2 ∉ B h"
hence 1: "t1 ∈ B h" and 2: "t2 ∈ U h" using t2 t12 by auto
show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type)
qed
}
moreover
{ assume "x = a"
from 1 have "t ∈ Bp (Suc h)" by(rule Bp_if_B)
hence "?case" using `x = a` by simp
}
ultimately show ?case by auto
next
case 2 thus ?case using Suc(1) n1_type by fastforce }
qed
lemma insert_type:
"t ∈ B h ⟹ insert x t ∈ B h ∪ B (Suc h)"
unfolding insert_def by (metis ins_type(1) tree_type)
end
subsubsection "Proofs for deletion"
lemma B_simps[simp]:
"N1 t ∈ B h = False"
"L2 y ∈ B h = False"
"(N3 t1 a1 t2 a2 t3) ∈ B h = False"
"N0 ∈ B h ⟷ h = 0"
by (cases h, auto)+
context delete
begin
lemma n2_type1:
"⟦t1 ∈ Um h; t2 ∈ B h⟧ ⟹ n2 t1 a t2 ∈ T (Suc h)"
apply(cases h rule: Bp.cases)
apply auto[2]
apply(erule exE bexE conjE imageE | simp | erule disjE)+
done
lemma n2_type2:
"⟦t1 ∈ B h ; t2 ∈ Um h ⟧ ⟹ n2 t1 a t2 ∈ T (Suc h)"
apply(cases h rule: Bp.cases)
apply auto[2]
apply(erule exE bexE conjE imageE | simp | erule disjE)+
done
lemma n2_type3:
"⟦t1 ∈ T h ; t2 ∈ T h ⟧ ⟹ n2 t1 a t2 ∈ T (Suc h)"
apply(cases h rule: Bp.cases)
apply auto[2]
apply(erule exE bexE conjE imageE | simp | erule disjE)+
done
lemma del_minNoneN0: "⟦t ∈ B h; del_min t = None⟧ ⟹ t = N0"
by (cases t) (auto split: option.splits)
lemma del_minNoneN1 : "⟦t ∈ U h; del_min t = None⟧ ⟹ t = N1 N0"
by (cases h) (auto simp: del_minNoneN0 split: option.splits)
lemma del_min_type:
"t ∈ B h ⟹ del_min t = Some (a, t') ⟹ t' ∈ T h"
"t ∈ U h ⟹ del_min t = Some (a, t') ⟹ t' ∈ Um h"
proof (induction h arbitrary: t a t')
case (Suc h)
{ case 1
then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and
t12: "t1 ∈ T h" "t2 ∈ T h" "t1 ∈ B h ∨ t2 ∈ B h"
by auto
show ?case
proof (cases "del_min t1")
case None
show ?thesis
proof cases
assume "t1 ∈ B h"
with del_minNoneN0[OF this None] 1 show ?thesis by(auto)
next
assume "t1 ∉ B h"
thus ?thesis using 1 None by (auto)
qed
next
case [simp]: (Some bt')
obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
show ?thesis
proof cases
assume "t1 ∈ B h"
from Suc.IH(1)[OF this] 1 have "t1' ∈ T h" by simp
from n2_type3[OF this t12(2)] 1 show ?thesis by auto
next
assume "t1 ∉ B h"
hence t1: "t1 ∈ U h" and t2: "t2 ∈ B h" using t12 by auto
from Suc.IH(2)[OF t1] have "t1' ∈ Um h" by simp
from n2_type1[OF this t2] 1 show ?thesis by auto
qed
qed
}
{ case 2
then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 ∈ B h" by auto
show ?case
proof (cases "del_min t1")
case None
with del_minNoneN0[OF t1 None] 2 show ?thesis by(auto)
next
case [simp]: (Some bt')
obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce
from Suc.IH(1)[OF t1] have "t1' ∈ T h" by simp
thus ?thesis using 2 by auto
qed
}
qed auto
lemma del_type:
"t ∈ B h ⟹ del x t ∈ T h"
"t ∈ U h ⟹ del x t ∈ Um h"
proof (induction h arbitrary: x t)
case (Suc h)
{ case 1
then obtain l a r where [simp]: "t = N2 l a r" and
lr: "l ∈ T h" "r ∈ T h" "l ∈ B h ∨ r ∈ B h" by auto
{ assume "x < a"
have ?case
proof cases
assume "l ∈ B h"
from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
show ?thesis using `x<a` by(simp)
next
assume "l ∉ B h"
hence "l ∈ U h" "r ∈ B h" using lr by auto
from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
show ?thesis using `x<a` by(simp)
qed
} moreover
{ assume "x > a"
have ?case
proof cases
assume "r ∈ B h"
from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
show ?thesis using `x>a` by(simp)
next
assume "r ∉ B h"
hence "l ∈ B h" "r ∈ U h" using lr by auto
from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
show ?thesis using `x>a` by(simp)
qed
} moreover
{ assume [simp]: "x=a"
have ?case
proof (cases "del_min r")
case None
show ?thesis
proof cases
assume "r ∈ B h"
with del_minNoneN0[OF this None] lr show ?thesis by(simp)
next
assume "r ∉ B h"
hence "r ∈ U h" using lr by auto
with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
qed
next
case [simp]: (Some br')
obtain b r' where [simp]: "br' = (b,r')" by fastforce
show ?thesis
proof cases
assume "r ∈ B h"
from del_min_type(1)[OF this] n2_type3[OF lr(1)]
show ?thesis by simp
next
assume "r ∉ B h"
hence "l ∈ B h" and "r ∈ U h" using lr by auto
from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
show ?thesis by simp
qed
qed
} ultimately show ?case by auto
}
{ case 2 with Suc.IH(1) show ?case by auto }
qed auto
lemma tree_type: "t ∈ T (h+1) ⟹ tree t : B (h+1) ∪ B h"
by(auto)
lemma delete_type: "t ∈ B h ⟹ delete x t ∈ B h ∪ B(h-1)"
unfolding delete_def
by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
end
subsection "Overall correctness"
interpretation Set_by_Ordered
where empty = N0 and isin = isin and insert = insert.insert
and delete = delete.delete and inorder = inorder and inv = "λt. ∃h. t ∈ B h"
proof (standard, goal_cases)
case 2 thus ?case by(auto intro!: isin_set)
next
case 3 thus ?case by(auto intro!: insert.inorder_insert)
next
case 4 thus ?case by(auto intro!: delete.inorder_delete)
next
case 6 thus ?case using insert.insert_type by blast
next
case 7 thus ?case using delete.delete_type by blast
qed auto
end