added Brother12_Map
authornipkow
Sat Dec 05 16:13:28 2015 +0100 (2015-12-05)
changeset 617899ce1a397410a
parent 61788 1e4caf2beb5d
child 61790 0494964bb226
added Brother12_Map
src/HOL/Data_Structures/Brother12_Map.thy
src/HOL/Data_Structures/Brother12_Set.thy
src/HOL/Data_Structures/Tree23_Map.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Data_Structures/Brother12_Map.thy	Sat Dec 05 16:13:28 2015 +0100
     1.3 @@ -0,0 +1,210 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +section \<open>A 1-2 Brother Tree Implementation of Maps\<close>
     1.7 +
     1.8 +theory Brother12_Map
     1.9 +imports
    1.10 +  Brother12_Set
    1.11 +  Map_by_Ordered
    1.12 +begin
    1.13 +
    1.14 +fun lookup :: "('a \<times> 'b) bro \<Rightarrow> 'a::cmp \<Rightarrow> 'b option" where
    1.15 +"lookup N0 x = None" |
    1.16 +"lookup (N1 t) x = lookup t x" |
    1.17 +"lookup (N2 l (a,b) r) x =
    1.18 +  (case cmp x a of
    1.19 +     LT \<Rightarrow> lookup l x |
    1.20 +     EQ \<Rightarrow> Some b |
    1.21 +     GT \<Rightarrow> lookup r x)"
    1.22 +
    1.23 +locale update = insert
    1.24 +begin
    1.25 +
    1.26 +fun upd :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    1.27 +"upd x y N0 = L2 (x,y)" |
    1.28 +"upd x y (N1 t) = n1 (upd x y t)" |
    1.29 +"upd x y (N2 l (a,b) r) =
    1.30 +  (case cmp x a of
    1.31 +     LT \<Rightarrow> n2 (upd x y l) (a,b) r |
    1.32 +     EQ \<Rightarrow> N2 l (a,y) r |
    1.33 +     GT \<Rightarrow> n2 l (a,b) (upd x y r))"
    1.34 +
    1.35 +definition update :: "'a::cmp \<Rightarrow> 'b \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    1.36 +"update x y t = tree(upd x y t)"
    1.37 +
    1.38 +end
    1.39 +
    1.40 +context delete
    1.41 +begin
    1.42 +
    1.43 +fun del :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    1.44 +"del _ N0         = N0" |
    1.45 +"del x (N1 t)     = N1 (del x t)" |
    1.46 +"del x (N2 l (a,b) r) =
    1.47 +  (case cmp x a of
    1.48 +     LT \<Rightarrow> n2 (del x l) (a,b) r |
    1.49 +     GT \<Rightarrow> n2 l (a,b) (del x r) |
    1.50 +     EQ \<Rightarrow> (case del_min r of
    1.51 +              None \<Rightarrow> N1 l |
    1.52 +              Some (ab, r') \<Rightarrow> n2 l ab r'))"
    1.53 +
    1.54 +definition delete :: "'a::cmp \<Rightarrow> ('a\<times>'b) bro \<Rightarrow> ('a\<times>'b) bro" where
    1.55 +"delete a t = tree (del a t)"
    1.56 +
    1.57 +end
    1.58 +
    1.59 +subsection "Functional Correctness Proofs"
    1.60 +
    1.61 +subsubsection "Proofs for lookup"
    1.62 +
    1.63 +lemma lookup_map_of: "t \<in> T h \<Longrightarrow>
    1.64 +  sorted1(inorder t) \<Longrightarrow> lookup t x = map_of (inorder t) x"
    1.65 +by(induction h arbitrary: t) (auto simp: map_of_simps split: option.splits)
    1.66 +
    1.67 +subsubsection "Proofs for update"
    1.68 +
    1.69 +context update
    1.70 +begin
    1.71 +
    1.72 +lemma inorder_upd: "t \<in> T h \<Longrightarrow>
    1.73 +  sorted1(inorder t) \<Longrightarrow> inorder(upd x y t) = upd_list x y (inorder t)"
    1.74 +by(induction h arbitrary: t) (auto simp: upd_list_simps inorder_n1 inorder_n2)
    1.75 +
    1.76 +lemma inorder_update: "t \<in> T h \<Longrightarrow>
    1.77 +  sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    1.78 +by(simp add: update_def inorder_upd inorder_tree)
    1.79 +
    1.80 +end
    1.81 +
    1.82 +subsubsection \<open>Proofs for deletion\<close>
    1.83 +
    1.84 +context delete
    1.85 +begin
    1.86 +
    1.87 +lemma inorder_del:
    1.88 +  "t \<in> B h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
    1.89 +  "t \<in> U h \<Longrightarrow> sorted1(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
    1.90 +by(induction h arbitrary: t)
    1.91 +  (auto simp: del_list_simps inorder_n2 inorder_del_min split: option.splits)
    1.92 +
    1.93 +end
    1.94 +
    1.95 +
    1.96 +subsection \<open>Invariant Proofs\<close>
    1.97 +
    1.98 +subsubsection \<open>Proofs for update\<close>
    1.99 +
   1.100 +context update
   1.101 +begin
   1.102 +
   1.103 +lemma upd_type:
   1.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)"
   1.105 +apply(induction h arbitrary: t)
   1.106 + apply (simp)
   1.107 +apply (fastforce simp: Bp_if_B n2_type dest: n1_type)
   1.108 +done
   1.109 +
   1.110 +lemma update_type:
   1.111 +  "t \<in> T h \<Longrightarrow> update x y t \<in> T h \<union> T (Suc h)"
   1.112 +unfolding update_def by (metis Un_iff upd_type tree_type1 tree_type2)
   1.113 +
   1.114 +end
   1.115 +
   1.116 +subsubsection "Proofs for deletion"
   1.117 +
   1.118 +context delete
   1.119 +begin
   1.120 +
   1.121 +lemma del_type:
   1.122 +  "t \<in> B h \<Longrightarrow> del x t \<in> T h"
   1.123 +  "t \<in> U h \<Longrightarrow> del x t \<in> Um h"
   1.124 +proof (induction h arbitrary: x t)
   1.125 +  case (Suc h)
   1.126 +  { case 1
   1.127 +    then obtain l a b r where [simp]: "t = N2 l (a,b) r" and
   1.128 +      lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto
   1.129 +    { assume "x < a"
   1.130 +      have ?case
   1.131 +      proof cases
   1.132 +        assume "l \<in> B h"
   1.133 +        from n2_type3[OF Suc.IH(1)[OF this] lr(2)]
   1.134 +        show ?thesis using `x<a` by(simp)
   1.135 +      next
   1.136 +        assume "l \<notin> B h"
   1.137 +        hence "l \<in> U h" "r \<in> B h" using lr by auto
   1.138 +        from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)]
   1.139 +        show ?thesis using `x<a` by(simp)
   1.140 +      qed
   1.141 +    } moreover
   1.142 +    { assume "x > a"
   1.143 +      have ?case
   1.144 +      proof cases
   1.145 +        assume "r \<in> B h"
   1.146 +        from n2_type3[OF lr(1) Suc.IH(1)[OF this]]
   1.147 +        show ?thesis using `x>a` by(simp)
   1.148 +      next
   1.149 +        assume "r \<notin> B h"
   1.150 +        hence "l \<in> B h" "r \<in> U h" using lr by auto
   1.151 +        from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]]
   1.152 +        show ?thesis using `x>a` by(simp)
   1.153 +      qed
   1.154 +    } moreover
   1.155 +    { assume [simp]: "x=a"
   1.156 +      have ?case
   1.157 +      proof (cases "del_min r")
   1.158 +        case None
   1.159 +        show ?thesis
   1.160 +        proof cases
   1.161 +          assume "r \<in> B h"
   1.162 +          with del_minNoneN0[OF this None] lr show ?thesis by(simp)
   1.163 +        next
   1.164 +          assume "r \<notin> B h"
   1.165 +          hence "r \<in> U h" using lr by auto
   1.166 +          with del_minNoneN1[OF this None] lr(3) show ?thesis by (simp)
   1.167 +        qed
   1.168 +      next
   1.169 +        case [simp]: (Some br')
   1.170 +        obtain b r' where [simp]: "br' = (b,r')" by fastforce
   1.171 +        show ?thesis
   1.172 +        proof cases
   1.173 +          assume "r \<in> B h"
   1.174 +          from del_min_type(1)[OF this] n2_type3[OF lr(1)]
   1.175 +          show ?thesis by simp
   1.176 +        next
   1.177 +          assume "r \<notin> B h"
   1.178 +          hence "l \<in> B h" and "r \<in> U h" using lr by auto
   1.179 +          from del_min_type(2)[OF this(2)] n2_type2[OF this(1)]
   1.180 +          show ?thesis by simp
   1.181 +        qed
   1.182 +      qed
   1.183 +    } ultimately show ?case by auto
   1.184 +  }
   1.185 +  { case 2 with Suc.IH(1) show ?case by auto }
   1.186 +qed auto
   1.187 +
   1.188 +lemma delete_type:
   1.189 +  "t \<in> T h \<Longrightarrow> delete x t \<in> T h \<union> T(h-1)"
   1.190 +unfolding delete_def
   1.191 +by (cases h) (simp, metis del_type tree_type Un_iff Suc_eq_plus1 diff_Suc_1)
   1.192 +
   1.193 +end
   1.194 +
   1.195 +subsection "Overall correctness"
   1.196 +
   1.197 +interpretation Map_by_Ordered
   1.198 +where empty = N0 and lookup = lookup and update = update.update
   1.199 +and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> T h"
   1.200 +proof (standard, goal_cases)
   1.201 +  case 2 thus ?case by(auto intro!: lookup_map_of)
   1.202 +next
   1.203 +  case 3 thus ?case by(auto intro!: update.inorder_update)
   1.204 +next
   1.205 +  case 4 thus ?case
   1.206 +    by(auto simp: delete.delete_def delete.inorder_tree delete.inorder_del)
   1.207 +next
   1.208 +  case 6 thus ?case using update.update_type by (metis Un_iff)
   1.209 +next
   1.210 +  case 7 thus ?case using delete.delete_type by blast
   1.211 +qed auto
   1.212 +
   1.213 +end
     2.1 --- a/src/HOL/Data_Structures/Brother12_Set.thy	Fri Dec 04 22:19:04 2015 +0100
     2.2 +++ b/src/HOL/Data_Structures/Brother12_Set.thy	Sat Dec 05 16:13:28 2015 +0100
     2.3 @@ -54,13 +54,13 @@
     2.4  "n2 t1 a t2 = N2 t1 a t2"
     2.5  
     2.6  fun ins :: "'a::cmp \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where
     2.7 -"ins a N0 = L2 a" |
     2.8 -"ins a (N1 t) = n1 (ins a t)" |
     2.9 -"ins a (N2 l b r) =
    2.10 -  (case cmp a b of
    2.11 -     LT \<Rightarrow> n2 (ins a l) b r |
    2.12 -     EQ \<Rightarrow> N2 l b r |
    2.13 -     GT \<Rightarrow> n2 l b (ins a r))"
    2.14 +"ins x N0 = L2 x" |
    2.15 +"ins x (N1 t) = n1 (ins x t)" |
    2.16 +"ins x (N2 l a r) =
    2.17 +  (case cmp x a of
    2.18 +     LT \<Rightarrow> n2 (ins x l) a r |
    2.19 +     EQ \<Rightarrow> N2 l a r |
    2.20 +     GT \<Rightarrow> n2 l a (ins x r))"
    2.21  
    2.22  fun tree :: "'a bro \<Rightarrow> 'a bro" where
    2.23  "tree (L2 a) = N2 N0 a N0" |
    2.24 @@ -210,7 +210,7 @@
    2.25  
    2.26  subsection \<open>Invariant Proofs\<close>
    2.27  
    2.28 -subsection \<open>Proofs for insertion\<close>
    2.29 +subsubsection \<open>Proofs for insertion\<close>
    2.30  
    2.31  lemma n1_type: "t \<in> Bp h \<Longrightarrow> n1 t \<in> T (Suc h)"
    2.32  by(cases h rule: Bp.cases) auto
    2.33 @@ -301,7 +301,7 @@
    2.34  
    2.35  end
    2.36  
    2.37 -subsection "Proofs for deletion"
    2.38 +subsubsection "Proofs for deletion"
    2.39  
    2.40  lemma B_simps[simp]: 
    2.41    "N1 t \<in> B h = False"
    2.42 @@ -470,11 +470,12 @@
    2.43  
    2.44  end
    2.45  
    2.46 +
    2.47  subsection "Overall correctness"
    2.48  
    2.49  interpretation Set_by_Ordered
    2.50 -where empty = N0 and isin = isin and insert = insert.insert and delete = delete.delete
    2.51 -and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> T h"
    2.52 +where empty = N0 and isin = isin and insert = insert.insert
    2.53 +and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> T h"
    2.54  proof (standard, goal_cases)
    2.55    case 2 thus ?case by(auto intro!: isin_set)
    2.56  next
     3.1 --- a/src/HOL/Data_Structures/Tree23_Map.thy	Fri Dec 04 22:19:04 2015 +0100
     3.2 +++ b/src/HOL/Data_Structures/Tree23_Map.thy	Sat Dec 05 16:13:28 2015 +0100
     3.3 @@ -77,11 +77,11 @@
     3.4  
     3.5  
     3.6  lemma inorder_upd:
     3.7 -  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd a b t)) = upd_list a b (inorder t)"
     3.8 +  "sorted1(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(upd x y t)) = upd_list x y (inorder t)"
     3.9  by(induction t) (auto simp: upd_list_simps split: up\<^sub>i.splits)
    3.10  
    3.11  corollary inorder_update:
    3.12 -  "sorted1(inorder t) \<Longrightarrow> inorder(update a b t) = upd_list a b (inorder t)"
    3.13 +  "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    3.14  by(simp add: update_def inorder_upd)
    3.15  
    3.16  
    3.17 @@ -97,10 +97,10 @@
    3.18  
    3.19  subsection \<open>Balancedness\<close>
    3.20  
    3.21 -lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd a b t)) \<and> height(upd a b t) = height t"
    3.22 +lemma bal_upd: "bal t \<Longrightarrow> bal (tree\<^sub>i(upd x y t)) \<and> height(upd x y t) = height t"
    3.23  by (induct t) (auto split: up\<^sub>i.split)(* 16 secs in 2015 *)
    3.24  
    3.25 -corollary bal_update: "bal t \<Longrightarrow> bal (update a b t)"
    3.26 +corollary bal_update: "bal t \<Longrightarrow> bal (update x y t)"
    3.27  by (simp add: update_def bal_upd)
    3.28  
    3.29  
     4.1 --- a/src/HOL/ROOT	Fri Dec 04 22:19:04 2015 +0100
     4.2 +++ b/src/HOL/ROOT	Sat Dec 05 16:13:28 2015 +0100
     4.3 @@ -178,7 +178,7 @@
     4.4      RBT_Map
     4.5      Tree23_Map
     4.6      Tree234_Map
     4.7 -    Brother12_Set
     4.8 +    Brother12_Map
     4.9      Splay_Map
    4.10    document_files "root.tex" "root.bib"
    4.11