src/HOL/Data_Structures/AVL_Map.thy
author nipkow
Thu Jul 07 18:08:02 2016 +0200 (2016-07-07)
changeset 63411 e051eea34990
parent 61790 0494964bb226
child 67406 23307fd33906
permissions -rw-r--r--
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow@61232
     1
(* Author: Tobias Nipkow *)
nipkow@61232
     2
nipkow@61232
     3
section "AVL Tree Implementation of Maps"
nipkow@61232
     4
nipkow@61232
     5
theory AVL_Map
nipkow@61232
     6
imports
nipkow@61232
     7
  AVL_Set
nipkow@61232
     8
  Lookup2
nipkow@61232
     9
begin
nipkow@61232
    10
nipkow@63411
    11
fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
nipkow@61232
    12
"update x y Leaf = Node 1 Leaf (x,y) Leaf" |
nipkow@61581
    13
"update x y (Node h l (a,b) r) = (case cmp x a of
nipkow@61581
    14
   EQ \<Rightarrow> Node h l (x,y) r |
nipkow@61581
    15
   LT \<Rightarrow> balL (update x y l) (a,b) r |
nipkow@61581
    16
   GT \<Rightarrow> balR l (a,b) (update x y r))"
nipkow@61232
    17
nipkow@63411
    18
fun delete :: "'a::linorder \<Rightarrow> ('a*'b) avl_tree \<Rightarrow> ('a*'b) avl_tree" where
nipkow@61232
    19
"delete _ Leaf = Leaf" |
nipkow@61581
    20
"delete x (Node h l (a,b) r) = (case cmp x a of
nipkow@61648
    21
   EQ \<Rightarrow> del_root (Node h l (a,b) r) |
nipkow@61581
    22
   LT \<Rightarrow> balR (delete x l) (a,b) r |
nipkow@61581
    23
   GT \<Rightarrow> balL l (a,b) (delete x r))"
nipkow@61232
    24
nipkow@61232
    25
nipkow@61232
    26
subsection {* Functional Correctness Proofs *}
nipkow@61232
    27
nipkow@61232
    28
theorem inorder_update:
nipkow@61232
    29
  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
nipkow@61581
    30
by (induct t) (auto simp: upd_list_simps inorder_balL inorder_balR)
nipkow@61232
    31
nipkow@61232
    32
nipkow@61232
    33
theorem inorder_delete:
nipkow@61232
    34
  "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
nipkow@61232
    35
by(induction t)
nipkow@61581
    36
  (auto simp: del_list_simps inorder_balL inorder_balR
nipkow@61648
    37
     inorder_del_root inorder_del_maxD split: prod.splits)
nipkow@61232
    38
nipkow@61232
    39
interpretation Map_by_Ordered
nipkow@61232
    40
where empty = Leaf and lookup = lookup and update = update and delete = delete
nipkow@61686
    41
and inorder = inorder and inv = "\<lambda>_. True"
nipkow@61232
    42
proof (standard, goal_cases)
nipkow@61232
    43
  case 1 show ?case by simp
nipkow@61232
    44
next
nipkow@61790
    45
  case 2 thus ?case by(simp add: lookup_map_of)
nipkow@61232
    46
next
nipkow@61232
    47
  case 3 thus ?case by(simp add: inorder_update)
nipkow@61232
    48
next
nipkow@61232
    49
  case 4 thus ?case by(simp add: inorder_delete)
nipkow@61686
    50
qed auto
nipkow@61232
    51
nipkow@61232
    52
end