# HG changeset patch
# User nipkow
# Date 1449328408 -3600
# Node ID 9ce1a397410a056099fd7613e8395f909aa65d66
# Parent  1e4caf2beb5d8668c38d13947704c3f2f1fe5e0b
added Brother12_Map

diff -r 1e4caf2beb5d -r 9ce1a397410a src/HOL/Data_Structures/Brother12_Map.thy
--- /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
diff -r 1e4caf2beb5d -r 9ce1a397410a src/HOL/Data_Structures/Brother12_Set.thy
--- 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
diff -r 1e4caf2beb5d -r 9ce1a397410a src/HOL/Data_Structures/Tree23_Map.thy
--- 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)
 
 
diff -r 1e4caf2beb5d -r 9ce1a397410a src/HOL/ROOT
--- 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"