(* Author: Tobias Nipkow, Daniel Stüwe *)
section ‹1-2 Brother Tree Implementation of Sets
›
theory Brother12_Set
imports
Cmp
Set_Specs
"HOL-Number_Theory.Fib"
begin
subsection ‹Data Type
and Operations
›
datatype 'a bro =
N0 |
N1
"'a bro" |
N2
"'a bro" 'a "'a bro
" |
(* auxiliary constructors: *)
L2
'a |
N3
"'a bro" 'a "'a bro
" 'a "'a bro"
definition empty ::
"'a bro" where
"empty = N0"
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::linorder \ 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::linorder \ '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::linorder \ '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 split_min ::
"'a bro \ ('a \ 'a bro) option" where
"split_min N0 = None" |
"split_min (N1 t) =
(
case split_min t of
None
==> None |
Some (a, t
') \ Some (a, N1 t'))
" |
"split_min (N2 t1 a t2) =
(
case split_min t1 of
None
==> Some (a, N1 t2) |
Some (b, t1
') \ Some (b, n2 t1' a t2))
"
fun del ::
"'a::linorder \ '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 split_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::linorder \ '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 isin_set:
"t \ T h \ sorted(inorder t) \ isin t x = (x \ set(inorder t))"
by(
induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+
subsubsection
"Proofs for insertion"
lemma inorder_n1:
"inorder(n1 t) = inorder t"
by(cases t rule: n1.cases) (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(cases
"(l,a,r)" rule: n2.cases) (auto)
lemma inorder_split_min:
"t \ T h \ (split_min t = None \ inorder t = []) \
(split_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)"
apply (
induction h arbitrary: t)
apply (auto simp: del_list_simps inorder_n2 split: option.splits)
apply (auto simp: del_list_simps inorder_n2
inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
done
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)"
proof (
induction h arbitrary: t)
case 0
then show ?
case by simp
next
case (Suc h)
then show ?
case by (fastforce simp: Bp_if_B n2_type dest: n1_type)
qed
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
have ?
case if "x < a"
proof -
have "n2 (ins x t1) a t2 \ Bp (Suc h)"
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
with ‹x < a
› show ?
case by simp
qed
moreover
have ?
case if "a < x"
proof -
have "n2 t1 a (ins x t2) \ Bp (Suc h)"
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
with ‹a < x
› show ?
case by simp
qed
moreover
have ?
case if "x = a"
proof -
from 1
have "t \ Bp (Suc h)" by(rule Bp_if_B)
thus "?case" using ‹x = a
› by simp
qed
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)
using Um.simps(1)
apply blast
apply force
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 split_minNoneN0:
"\t \ B h; split_min t = None\ \ t = N0"
by (cases t) (auto split: option.splits)
lemma split_minNoneN1 :
"\t \ U h; split_min t = None\ \ t = N1 N0"
by (cases h) (auto simp: split_minNoneN0 split: option.splits)
lemma split_min_type:
"t \ B h \ split_min t = Some (a, t') \ t' \ T h"
"t \ U h \ split_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
"split_min t1")
case None
show ?thesis
proof cases
assume "t1 \ B h"
with split_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
"split_min t1")
case None
with split_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
have ?
case if "x < a"
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
have ?
case if "x > a"
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
have ?
case if [simp]:
"x=a"
proof (cases
"split_min r")
case None
show ?thesis
proof cases
assume "r \ B h"
with split_minNoneN0[OF this None] lr
show ?thesis
by(simp)
next
assume "r \ B h"
hence "r \ U h" using lr
by auto
with split_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 split_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 split_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 = empty
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 simp: empty_def)
subsection ‹Height-Size Relation
›
text ‹By Daniel Stüwe
›
fun fib_tree ::
"nat \ unit bro" where
"fib_tree 0 = N0"
|
"fib_tree (Suc 0) = N2 N0 () N0"
|
"fib_tree (Suc(Suc h)) = N2 (fib_tree (h+1)) () (N1 (fib_tree h))"
fun fib
' :: "nat \ nat" where
"fib' 0 = 0"
|
"fib' (Suc 0) = 1"
|
"fib' (Suc(Suc h)) = 1 + fib' (Suc h) + fib' h"
fun size ::
"'a bro \ nat" where
"size N0 = 0"
|
"size (N1 t) = size t"
|
"size (N2 t1 _ t2) = 1 + size t1 + size t2"
lemma fib_tree_B:
"fib_tree h \ B h"
by (
induction h rule: fib_tree.induct) auto
declare [[names_short]]
lemma size_fib
': "size (fib_tree h) = fib' h
"
by (
induction h rule: fib_tree.induct) auto
lemma fibfib:
"fib' h + 1 = fib (Suc(Suc h))"
by (
induction h rule: fib_tree.induct) auto
lemma B_N2_cases[consumes 1]:
assumes "N2 t1 a t2 \ B (Suc n)"
obtains
(BB)
"t1 \ B n" and "t2 \ B n" |
(UB)
"t1 \ U n" and "t2 \ B n" |
(BU)
"t1 \ B n" and "t2 \ U n"
using assms
by auto
lemma size_bounded:
"t \ B h \ size t \ size (fib_tree h)"
unfolding size_fib
' proof (induction h arbitrary: t rule: fib'.induct)
case (3 h t
')
note main = 3
then obtain t1 a t2
where t
': "t' = N2 t1 a t2
" by auto
with main
have "N2 t1 a t2 \ B (Suc (Suc h))" by auto
thus ?
case proof (cases rule: B_N2_cases)
case BB
then obtain x y z
where t2:
"t2 = N2 x y z \ t2 = N2 z y x" "x \ B h" by auto
show ?thesis
unfolding t
' using main(1)[OF BB(1)] main(2)[OF t2(2)] t2(1) by auto
next
case UB
then obtain t11
where t1:
"t1 = N1 t11" "t11 \ B h" by auto
show ?thesis
unfolding t
' t1(1) using main(2)[OF t1(2)] main(1)[OF UB(2)] by simp
next
case BU
then obtain t22
where t2:
"t2 = N1 t22" "t22 \ B h" by auto
show ?thesis
unfolding t
' t2(1) using main(2)[OF t2(2)] main(1)[OF BU(1)] by simp
qed
qed auto
theorem "t \ B h \ fib (h + 2) \ size t + 1"
using size_bounded
by (simp add: size_fib
' fibfib[symmetric] del: fib.simps)
end
