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