--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Brother12_Map.thy Sat Dec 05 16:13:28 2015 +0100
@@ -0,0 +1,210 @@
+(* Author: Tobias Nipkow *)
+
+section \<open>A 1-2 Brother Tree Implementation of Maps\<close>
+
+theory Brother12_Map
+imports
+ Brother12_Set
+ Map_by_Ordered
+begin
+
+fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::cmp \<Rightarrow> 'b option" where
+"lookup N0 x = None" |
+"lookup (N1 t) x = lookup t x" |
+"lookup (N2 l (a,b) r) x =
+ (case cmp x a of
+ LT \<Rightarrow> lookup l x |
+ EQ \<Rightarrow> Some b |
+ GT \<Rightarrow> lookup r x)"
+
+locale update = insert
+begin
+
+fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
+"upd x y N0 = L2 (x,y)" |
+"upd x y (N1 t) = n1 (upd x y t)" |
+"upd x y (N2 l (a,b) r) =
+ (case cmp x a of
+ LT \<Rightarrow> n2 (upd x y l) (a,b) r |
+ EQ \<Rightarrow> N2 l (a,y) r |
+ GT \<Rightarrow> n2 l (a,b) (upd x y r))"
+
+definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
+"update x y t = tree(upd x y t)"
+
+end
+
+context delete
+begin
+
+fun del :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
+"del _ N0 = N0" |
+"del x (N1 t) = N1 (del x t)" |
+"del x (N2 l (a,b) r) =
+ (case cmp x a of
+ LT \<Rightarrow> n2 (del x l) (a,b) r |
+ GT \<Rightarrow> n2 l (a,b) (del x r) |
+ EQ \<Rightarrow> (case del_min r of
+ None \<Rightarrow> N1 l |
+ Some (ab, r') \<Rightarrow> n2 l ab r'))"
+
+definition delete :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
+"delete a t = tree (del a t)"
+
+end
+
+subsection "Functional Correctness Proofs"
+
+subsubsection "Proofs for lookup"
+
+lemma lookup_map_of: "t \<in> T h \<Longrightarrow>
+ sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
+by(induction h arbitrary: t) (auto simp: map_of_simps split: option.splits)
+
+subsubsection "Proofs for update"
+
+context update
+begin
+
+lemma inorder_upd: "t \<in> T h \<Longrightarrow>
+ sorted1(inorder t) \<Longrightarrow> inorder(upd x y t) = upd_list x y (inorder t)"
+by(induction h arbitrary: t) (auto simp: upd_list_simps inorder_n1 inorder_n2)
+
+lemma inorder_update: "t \<in> T h \<Longrightarrow>
+ sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
+by(simp add: update_def inorder_upd inorder_tree)
+
+end
+
+subsubsection \<open>Proofs for deletion\<close>
+
+context delete
+begin
+
+lemma inorder_del:
+ "t \<in> B h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
+ "t \<in> U h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
+by(induction h arbitrary: t)
+ (auto simp: del_list_simps inorder_n2 inorder_del_min split: option.splits)
+
+end
+
+
+subsection \<open>Invariant Proofs\<close>
+
+subsubsection \<open>Proofs for update\<close>
+
+context update
+begin
+
+lemma upd_type:
+ "(t \<in> B h \<longrightarrow> upd x y t \<in> Bp h) \<and> (t \<in> U h \<longrightarrow> upd x y t \<in> T h)"
+apply(induction h arbitrary: t)
+ apply (simp)
+apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
+done
+
+lemma update_type:
+ "t \<in> T h \<Longrightarrow> update x y t \<in> T h \<union> T (Suc h)"
+unfolding update_def by (metis Un_iff upd_type tree_type1 tree_type2)
+
+end
+
+subsubsection "Proofs for deletion"
+
+context delete
+begin
+
+lemma del_type:
+ "t \<in> B h \<Longrightarrow> del x t \<in> T h"
+ "t \<in> U h \<Longrightarrow> del x t \<in> Um h"
+proof (induction h arbitrary: x t)
+ case (Suc h)
+ { case 1
+ then obtain l a b r where [simp]: "t = N2 l (a,b) r" and
+ lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
+ { assume "x < a"
+ have ?case
+ proof cases
+ assume "l \<in> B h"
+ from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
+ show ?thesis using `x<a` by(simp)
+ next
+ assume "l \<notin> B h"
+ hence "l \<in> U h" "r \<in> 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 \<in> B h"
+ from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
+ show ?thesis using `x>a` by(simp)
+ next
+ assume "r \<notin> B h"
+ hence "l \<in> B h" "r \<in> 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 \<in> B h"
+ with del_minNoneN0[OF this None] lr show ?thesis by(simp)
+ next
+ assume "r \<notin> B h"
+ hence "r \<in> 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 \<in> B h"
+ from del_min_type(1)[OF this] n2_type3[OF lr(1)]
+ show ?thesis by simp
+ next
+ assume "r \<notin> B h"
+ hence "l \<in> B h" and "r \<in> 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 delete_type:
+ "t \<in> T h \<Longrightarrow> delete x t \<in> T h \<union> T(h-1)"
+unfolding delete_def
+by (cases h) (simp, metis del_type tree_type Un_iff Suc_eq_plus1 diff_Suc_1)
+
+end
+
+subsection "Overall correctness"
+
+interpretation Map_by_Ordered
+where empty = N0 and lookup = lookup and update = update.update
+and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> T h"
+proof (standard, goal_cases)
+ case 2 thus ?case by(auto intro!: lookup_map_of)
+next
+ case 3 thus ?case by(auto intro!: update.inorder_update)
+next
+ case 4 thus ?case
+ by(auto simp: delete.delete_def delete.inorder_tree delete.inorder_del)
+next
+ case 6 thus ?case using update.update_type by (metis Un_iff)
+next
+ case 7 thus ?case using delete.delete_type by blast
+qed auto
+
+end
--- a/src/HOL/Data_Structures/Brother12_Set.thy Fri Dec 04 22:19:04 2015 +0100
+++ b/src/HOL/Data_Structures/Brother12_Set.thy Sat Dec 05 16:13:28 2015 +0100
@@ -54,13 +54,13 @@
"n2 t1 a t2 = N2 t1 a t2"
fun ins :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
-"ins a N0 = L2 a" |
-"ins a (N1 t) = n1 (ins a t)" |
-"ins a (N2 l b r) =
- (case cmp a b of
- LT \<Rightarrow> n2 (ins a l) b r |
- EQ \<Rightarrow> N2 l b r |
- GT \<Rightarrow> n2 l b (ins a r))"
+"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 \<Rightarrow> n2 (ins x l) a r |
+ EQ \<Rightarrow> N2 l a r |
+ GT \<Rightarrow> n2 l a (ins x r))"
fun tree :: "'a bro \<Rightarrow> 'a bro" where
"tree (L2 a) = N2 N0 a N0" |
@@ -210,7 +210,7 @@
subsection \<open>Invariant Proofs\<close>
-subsection \<open>Proofs for insertion\<close>
+subsubsection \<open>Proofs for insertion\<close>
lemma n1_type: "t \<in> Bp h \<Longrightarrow> n1 t \<in> T (Suc h)"
by(cases h rule: Bp.cases) auto
@@ -301,7 +301,7 @@
end
-subsection "Proofs for deletion"
+subsubsection "Proofs for deletion"
lemma B_simps[simp]:
"N1 t \<in> B h = False"
@@ -470,11 +470,12 @@
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 = "\<lambda>t. \<exists>h. t \<in> T h"
+where empty = N0 and isin = isin and insert = insert.insert
+and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> T h"
proof (standard, goal_cases)
case 2 thus ?case by(auto intro!: isin_set)
next
--- a/src/HOL/Data_Structures/Tree23_Map.thy Fri Dec 04 22:19:04 2015 +0100
+++ b/src/HOL/Data_Structures/Tree23_Map.thy Sat Dec 05 16:13:28 2015 +0100
@@ -77,11 +77,11 @@
lemma inorder_upd:
- "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
+ "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)"
by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
corollary inorder_update:
- "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
+ "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
by(simp add: update_def inorder_upd)
@@ -97,10 +97,10 @@
subsection \<open>Balancedness\<close>
-lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd a b t)) \<and> height(upd a b t) = height t"
+lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
by (induct t) (auto split: up\<^sub>i.split)(* 16 secs in 2015 *)
-corollary bal_update: "bal t \<Longrightarrow> bal (update a b t)"
+corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)"
by (simp add: update_def bal_upd)
--- a/src/HOL/ROOT Fri Dec 04 22:19:04 2015 +0100
+++ b/src/HOL/ROOT Sat Dec 05 16:13:28 2015 +0100
@@ -178,7 +178,7 @@
RBT_Map
Tree23_Map
Tree234_Map
- Brother12_Set
+ Brother12_Map
Splay_Map
document_files "root.tex" "root.bib"