added AA_Map; tuned titles
authornipkow
Mon Jan 11 20:51:13 2016 +0100 (2016-01-11)
changeset 6213090a3016a6c12
parent 62129 72d19e588e97
child 62132 09c2a77f91d3
added AA_Map; tuned titles
src/HOL/Data_Structures/AA_Map.thy
src/HOL/Data_Structures/AA_Set.thy
src/HOL/Data_Structures/Brother12_Map.thy
src/HOL/Data_Structures/Brother12_Set.thy
src/HOL/Data_Structures/Tree234_Map.thy
src/HOL/Data_Structures/Tree234_Set.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/Data_Structures/Tree23_Set.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/AA_Map.thy	Mon Jan 11 20:51:13 2016 +0100
     1.3 @@ -0,0 +1,54 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +section "AA Implementation of Maps"
     1.7 +
     1.8 +theory AA_Map
     1.9 +imports
    1.10 +  AA_Set
    1.11 +  Lookup2
    1.12 +begin
    1.13 +
    1.14 +fun update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
    1.15 +"update x y Leaf = Node 1 Leaf (x,y) Leaf" |
    1.16 +"update x y (Node lv t1 (a,b) t2) =
    1.17 +  (case cmp x a of
    1.18 +     LT \<Rightarrow> split (skew (Node lv (update x y t1) (a,b) t2)) |
    1.19 +     GT \<Rightarrow> split (skew (Node lv t1 (a,b) (update x y t2))) |
    1.20 +     EQ \<Rightarrow> Node lv t1 (x,y) t2)"
    1.21 +
    1.22 +fun delete :: "'a::cmp \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where
    1.23 +"delete _ Leaf = Leaf" |
    1.24 +"delete x (Node lv l (a,b) r) =
    1.25 +  (case cmp x a of
    1.26 +     LT \<Rightarrow> adjust (Node lv (delete x l) (a,b) r) |
    1.27 +     GT \<Rightarrow> adjust (Node lv l (a,b) (delete x r)) |
    1.28 +     EQ \<Rightarrow> (if l = Leaf then r
    1.29 +            else let (l',ab') = del_max l in adjust (Node lv l' ab' r)))"
    1.30 +
    1.31 +
    1.32 +subsection {* Functional Correctness Proofs *}
    1.33 +
    1.34 +theorem inorder_update:
    1.35 +  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    1.36 +by (induct t) (auto simp: upd_list_simps inorder_split inorder_skew)
    1.37 +
    1.38 +
    1.39 +theorem inorder_delete:
    1.40 +  "sorted1(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)"
    1.41 +by(induction t)
    1.42 +  (auto simp: del_list_simps inorder_adjust del_maxD split: prod.splits)
    1.43 +
    1.44 +interpretation Map_by_Ordered
    1.45 +where empty = Leaf and lookup = lookup and update = update and delete = delete
    1.46 +and inorder = inorder and inv = "\<lambda>_. True"
    1.47 +proof (standard, goal_cases)
    1.48 +  case 1 show ?case by simp
    1.49 +next
    1.50 +  case 2 thus ?case by(simp add: lookup_map_of)
    1.51 +next
    1.52 +  case 3 thus ?case by(simp add: inorder_update)
    1.53 +next
    1.54 +  case 4 thus ?case by(simp add: inorder_delete)
    1.55 +qed auto
    1.56 +
    1.57 +end
     2.1 --- a/src/HOL/Data_Structures/AA_Set.thy	Mon Jan 11 18:27:27 2016 +0100
     2.2 +++ b/src/HOL/Data_Structures/AA_Set.thy	Mon Jan 11 20:51:13 2016 +0100
     2.3 @@ -1,9 +1,10 @@
     2.4  (*
     2.5  Author: Tobias Nipkow
     2.6 -Invariants are under development
     2.7 +
     2.8 +Added trivial cases to function `adjust' to obviate invariants.
     2.9  *)
    2.10  
    2.11 -section \<open>An AA Tree Implementation of Sets\<close>
    2.12 +section \<open>AA Tree Implementation of Sets\<close>
    2.13  
    2.14  theory AA_Set
    2.15  imports
    2.16 @@ -16,13 +17,13 @@
    2.17  fun lvl :: "'a aa_tree \<Rightarrow> nat" where
    2.18  "lvl Leaf = 0" |
    2.19  "lvl (Node lv _ _ _) = lv"
    2.20 -
    2.21 +(*
    2.22  fun invar :: "'a aa_tree \<Rightarrow> bool" where
    2.23  "invar Leaf = True" |
    2.24  "invar (Node h l a r) =
    2.25   (invar l \<and> invar r \<and>
    2.26    h = lvl l + 1 \<and> (h = lvl r + 1 \<or> (\<exists>lr b rr. r = Node h lr b rr \<and> h = lvl rr + 1)))"
    2.27 -
    2.28 +*)
    2.29  fun skew :: "'a aa_tree \<Rightarrow> 'a aa_tree" where
    2.30  "skew (Node lva (Node lvb t1 b t2) a t3) =
    2.31    (if lva = lvb then Node lva t1 b (Node lva t2 a t3) else Node lva (Node lvb t1 b t2) a t3)" |
    2.32 @@ -105,8 +106,7 @@
    2.33  subsubsection "Proofs for delete"
    2.34  
    2.35  lemma del_maxD:
    2.36 -  "\<lbrakk> del_max t = (t',x); t \<noteq> Leaf; sorted(inorder t) \<rbrakk> \<Longrightarrow>
    2.37 -   inorder t' @ [x] = inorder t"
    2.38 +  "\<lbrakk> del_max t = (t',x); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> inorder t' @ [x] = inorder t"
    2.39  by(induction t arbitrary: t' rule: del_max.induct)
    2.40    (auto simp: sorted_lems split: prod.splits)
    2.41  
     3.1 --- a/src/HOL/Data_Structures/Brother12_Map.thy	Mon Jan 11 18:27:27 2016 +0100
     3.2 +++ b/src/HOL/Data_Structures/Brother12_Map.thy	Mon Jan 11 20:51:13 2016 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4  (* Author: Tobias Nipkow *)
     3.5  
     3.6 -section \<open>A 1-2 Brother Tree Implementation of Maps\<close>
     3.7 +section \<open>1-2 Brother Tree Implementation of Maps\<close>
     3.8  
     3.9  theory Brother12_Map
    3.10  imports
     4.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Mon Jan 11 18:27:27 2016 +0100
     4.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Mon Jan 11 20:51:13 2016 +0100
     4.3 @@ -1,6 +1,6 @@
     4.4  (* Author: Tobias Nipkow *)
     4.5  
     4.6 -section \<open>A 1-2 Brother Tree Implementation of Sets\<close>
     4.7 +section \<open>1-2 Brother Tree Implementation of Sets\<close>
     4.8  
     4.9  theory Brother12_Set
    4.10  imports
     5.1 --- a/src/HOL/Data_Structures/Tree234_Map.thy	Mon Jan 11 18:27:27 2016 +0100
     5.2 +++ b/src/HOL/Data_Structures/Tree234_Map.thy	Mon Jan 11 20:51:13 2016 +0100
     5.3 @@ -1,6 +1,6 @@
     5.4  (* Author: Tobias Nipkow *)
     5.5  
     5.6 -section \<open>A 2-3-4 Tree Implementation of Maps\<close>
     5.7 +section \<open>2-3-4 Tree Implementation of Maps\<close>
     5.8  
     5.9  theory Tree234_Map
    5.10  imports
     6.1 --- a/src/HOL/Data_Structures/Tree234_Set.thy	Mon Jan 11 18:27:27 2016 +0100
     6.2 +++ b/src/HOL/Data_Structures/Tree234_Set.thy	Mon Jan 11 20:51:13 2016 +0100
     6.3 @@ -1,6 +1,6 @@
     6.4  (* Author: Tobias Nipkow *)
     6.5  
     6.6 -section \<open>A 2-3-4 Tree Implementation of Sets\<close>
     6.7 +section \<open>2-3-4 Tree Implementation of Sets\<close>
     6.8  
     6.9  theory Tree234_Set
    6.10  imports
     7.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Mon Jan 11 18:27:27 2016 +0100
     7.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Mon Jan 11 20:51:13 2016 +0100
     7.3 @@ -1,6 +1,6 @@
     7.4  (* Author: Tobias Nipkow *)
     7.5  
     7.6 -section \<open>A 2-3 Tree Implementation of Maps\<close>
     7.7 +section \<open>2-3 Tree Implementation of Maps\<close>
     7.8  
     7.9  theory Tree23_Map
    7.10  imports
     8.1 --- a/src/HOL/Data_Structures/Tree23_Set.thy	Mon Jan 11 18:27:27 2016 +0100
     8.2 +++ b/src/HOL/Data_Structures/Tree23_Set.thy	Mon Jan 11 20:51:13 2016 +0100
     8.3 @@ -1,6 +1,6 @@
     8.4  (* Author: Tobias Nipkow *)
     8.5  
     8.6 -section \<open>A 2-3 Tree Implementation of Sets\<close>
     8.7 +section \<open>2-3 Tree Implementation of Sets\<close>
     8.8  
     8.9  theory Tree23_Set
    8.10  imports
     9.1 --- a/src/HOL/ROOT	Mon Jan 11 18:27:27 2016 +0100
     9.2 +++ b/src/HOL/ROOT	Mon Jan 11 20:51:13 2016 +0100
     9.3 @@ -180,7 +180,7 @@
     9.4      Tree23_Map
     9.5      Tree234_Map
     9.6      Brother12_Map
     9.7 -    AA_Set
     9.8 +    AA_Map
     9.9      Splay_Map
    9.10    document_files "root.tex" "root.bib"
    9.11