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