src/HOL/Data_Structures/Brother12_Map.thy
 author nipkow Sat Apr 21 08:41:42 2018 +0200 (14 months ago) changeset 68020 6aade817bee5 parent 67965 aaa31cd0caef child 68431 b294e095f64c permissions -rw-r--r--
del_min -> split_min
```     1 (* Author: Tobias Nipkow *)
```
```     2
```
```     3 section \<open>1-2 Brother Tree Implementation of Maps\<close>
```
```     4
```
```     5 theory Brother12_Map
```
```     6 imports
```
```     7   Brother12_Set
```
```     8   Map_Specs
```
```     9 begin
```
```    10
```
```    11 fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::linorder \<Rightarrow> 'b option" where
```
```    12 "lookup N0 x = None" |
```
```    13 "lookup (N1 t) x = lookup t x" |
```
```    14 "lookup (N2 l (a,b) r) x =
```
```    15   (case cmp x a of
```
```    16      LT \<Rightarrow> lookup l x |
```
```    17      EQ \<Rightarrow> Some b |
```
```    18      GT \<Rightarrow> lookup r x)"
```
```    19
```
```    20 locale update = insert
```
```    21 begin
```
```    22
```
```    23 fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
```
```    24 "upd x y N0 = L2 (x,y)" |
```
```    25 "upd x y (N1 t) = n1 (upd x y t)" |
```
```    26 "upd x y (N2 l (a,b) r) =
```
```    27   (case cmp x a of
```
```    28      LT \<Rightarrow> n2 (upd x y l) (a,b) r |
```
```    29      EQ \<Rightarrow> N2 l (a,y) r |
```
```    30      GT \<Rightarrow> n2 l (a,b) (upd x y r))"
```
```    31
```
```    32 definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
```
```    33 "update x y t = tree(upd x y t)"
```
```    34
```
```    35 end
```
```    36
```
```    37 context delete
```
```    38 begin
```
```    39
```
```    40 fun del :: "'a::linorder \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
```
```    41 "del _ N0         = N0" |
```
```    42 "del x (N1 t)     = N1 (del x t)" |
```
```    43 "del x (N2 l (a,b) r) =
```
```    44   (case cmp x a of
```
```    45      LT \<Rightarrow> n2 (del x l) (a,b) r |
```
```    46      GT \<Rightarrow> n2 l (a,b) (del x r) |
```
```    47      EQ \<Rightarrow> (case split_min r of
```
```    48               None \<Rightarrow> N1 l |
```
```    49               Some (ab, r') \<Rightarrow> n2 l ab r'))"
```
```    50
```
```    51 definition delete :: "'a::linorder \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
```
```    52 "delete a t = tree (del a t)"
```
```    53
```
```    54 end
```
```    55
```
```    56 subsection "Functional Correctness Proofs"
```
```    57
```
```    58 subsubsection "Proofs for lookup"
```
```    59
```
```    60 lemma lookup_map_of: "t \<in> T h \<Longrightarrow>
```
```    61   sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
```
```    62 by(induction h arbitrary: t) (auto simp: map_of_simps split: option.splits)
```
```    63
```
```    64 subsubsection "Proofs for update"
```
```    65
```
```    66 context update
```
```    67 begin
```
```    68
```
```    69 lemma inorder_upd: "t \<in> T h \<Longrightarrow>
```
```    70   sorted1(inorder t) \<Longrightarrow> inorder(upd x y t) = upd_list x y (inorder t)"
```
```    71 by(induction h arbitrary: t) (auto simp: upd_list_simps inorder_n1 inorder_n2)
```
```    72
```
```    73 lemma inorder_update: "t \<in> T h \<Longrightarrow>
```
```    74   sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
```
```    75 by(simp add: update_def inorder_upd inorder_tree)
```
```    76
```
```    77 end
```
```    78
```
```    79 subsubsection \<open>Proofs for deletion\<close>
```
```    80
```
```    81 context delete
```
```    82 begin
```
```    83
```
```    84 lemma inorder_del:
```
```    85   "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
```
```    86 by(induction h arbitrary: t) (auto simp: del_list_simps inorder_n2
```
```    87      inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits)
```
```    88
```
```    89 lemma inorder_delete:
```
```    90   "t \<in> T h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
```
```    91 by(simp add: delete_def inorder_del inorder_tree)
```
```    92
```
```    93 end
```
```    94
```
```    95
```
```    96 subsection \<open>Invariant Proofs\<close>
```
```    97
```
```    98 subsubsection \<open>Proofs for update\<close>
```
```    99
```
```   100 context update
```
```   101 begin
```
```   102
```
```   103 lemma upd_type:
```
```   104   "(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)"
```
```   105 apply(induction h arbitrary: t)
```
```   106  apply (simp)
```
```   107 apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
```
```   108 done
```
```   109
```
```   110 lemma update_type:
```
```   111   "t \<in> B h \<Longrightarrow> update x y t \<in> B h \<union> B (Suc h)"
```
```   112 unfolding update_def by (metis upd_type tree_type)
```
```   113
```
```   114 end
```
```   115
```
```   116 subsubsection "Proofs for deletion"
```
```   117
```
```   118 context delete
```
```   119 begin
```
```   120
```
```   121 lemma del_type:
```
```   122   "t \<in> B h \<Longrightarrow> del x t \<in> T h"
```
```   123   "t \<in> U h \<Longrightarrow> del x t \<in> Um h"
```
```   124 proof (induction h arbitrary: x t)
```
```   125   case (Suc h)
```
```   126   { case 1
```
```   127     then obtain l a b r where [simp]: "t = N2 l (a,b) r" and
```
```   128       lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
```
```   129     have ?case if "x < a"
```
```   130     proof cases
```
```   131       assume "l \<in> B h"
```
```   132       from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
```
```   133       show ?thesis using \<open>x<a\<close> by(simp)
```
```   134     next
```
```   135       assume "l \<notin> B h"
```
```   136       hence "l \<in> U h" "r \<in> B h" using lr by auto
```
```   137       from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
```
```   138       show ?thesis using \<open>x<a\<close> by(simp)
```
```   139     qed
```
```   140     moreover
```
```   141     have ?case if "x > a"
```
```   142     proof cases
```
```   143       assume "r \<in> B h"
```
```   144       from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
```
```   145       show ?thesis using \<open>x>a\<close> by(simp)
```
```   146     next
```
```   147       assume "r \<notin> B h"
```
```   148       hence "l \<in> B h" "r \<in> U h" using lr by auto
```
```   149       from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
```
```   150       show ?thesis using \<open>x>a\<close> by(simp)
```
```   151     qed
```
```   152     moreover
```
```   153     have ?case if [simp]: "x=a"
```
```   154     proof (cases "split_min r")
```
```   155       case None
```
```   156       show ?thesis
```
```   157       proof cases
```
```   158         assume "r \<in> B h"
```
```   159         with split_minNoneN0[OF this None] lr show ?thesis by(simp)
```
```   160       next
```
```   161         assume "r \<notin> B h"
```
```   162         hence "r \<in> U h" using lr by auto
```
```   163         with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
```
```   164       qed
```
```   165     next
```
```   166       case [simp]: (Some br')
```
```   167       obtain b r' where [simp]: "br' = (b,r')" by fastforce
```
```   168       show ?thesis
```
```   169       proof cases
```
```   170         assume "r \<in> B h"
```
```   171         from split_min_type(1)[OF this] n2_type3[OF lr(1)]
```
```   172         show ?thesis by simp
```
```   173       next
```
```   174         assume "r \<notin> B h"
```
```   175         hence "l \<in> B h" and "r \<in> U h" using lr by auto
```
```   176         from split_min_type(2)[OF this(2)] n2_type2[OF this(1)]
```
```   177         show ?thesis by simp
```
```   178       qed
```
```   179     qed
```
```   180     ultimately show ?case by auto
```
```   181   }
```
```   182   { case 2 with Suc.IH(1) show ?case by auto }
```
```   183 qed auto
```
```   184
```
```   185 lemma delete_type:
```
```   186   "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)"
```
```   187 unfolding delete_def
```
```   188 by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1)
```
```   189
```
```   190 end
```
```   191
```
```   192 subsection "Overall correctness"
```
```   193
```
```   194 interpretation Map_by_Ordered
```
```   195 where empty = N0 and lookup = lookup and update = update.update
```
```   196 and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h"
```
```   197 proof (standard, goal_cases)
```
```   198   case 2 thus ?case by(auto intro!: lookup_map_of)
```
```   199 next
```
```   200   case 3 thus ?case by(auto intro!: update.inorder_update)
```
```   201 next
```
```   202   case 4 thus ?case by(auto intro!: delete.inorder_delete)
```
```   203 next
```
```   204   case 6 thus ?case using update.update_type by (metis Un_iff)
```
```   205 next
```
```   206   case 7 thus ?case using delete.delete_type by blast
```
```   207 qed auto
```
```   208
```
```   209 end
```