7 AA_Set |
7 AA_Set |
8 Lookup2 |
8 Lookup2 |
9 begin |
9 begin |
10 |
10 |
11 fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where |
11 fun update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where |
12 "update x y Leaf = Node 1 Leaf (x,y) Leaf" | |
12 "update x y Leaf = Node Leaf (x,y) 1 Leaf" | |
13 "update x y (Node lv t1 (a,b) t2) = |
13 "update x y (Node t1 (a,b) lv t2) = |
14 (case cmp x a of |
14 (case cmp x a of |
15 LT \<Rightarrow> split (skew (Node lv (update x y t1) (a,b) t2)) | |
15 LT \<Rightarrow> split (skew (Node (update x y t1) (a,b) lv t2)) | |
16 GT \<Rightarrow> split (skew (Node lv t1 (a,b) (update x y t2))) | |
16 GT \<Rightarrow> split (skew (Node t1 (a,b) lv (update x y t2))) | |
17 EQ \<Rightarrow> Node lv t1 (x,y) t2)" |
17 EQ \<Rightarrow> Node t1 (x,y) lv t2)" |
18 |
18 |
19 fun delete :: "'a::linorder \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where |
19 fun delete :: "'a::linorder \<Rightarrow> ('a*'b) aa_tree \<Rightarrow> ('a*'b) aa_tree" where |
20 "delete _ Leaf = Leaf" | |
20 "delete _ Leaf = Leaf" | |
21 "delete x (Node lv l (a,b) r) = |
21 "delete x (Node l (a,b) lv r) = |
22 (case cmp x a of |
22 (case cmp x a of |
23 LT \<Rightarrow> adjust (Node lv (delete x l) (a,b) r) | |
23 LT \<Rightarrow> adjust (Node (delete x l) (a,b) lv r) | |
24 GT \<Rightarrow> adjust (Node lv l (a,b) (delete x r)) | |
24 GT \<Rightarrow> adjust (Node l (a,b) lv (delete x r)) | |
25 EQ \<Rightarrow> (if l = Leaf then r |
25 EQ \<Rightarrow> (if l = Leaf then r |
26 else let (l',ab') = split_max l in adjust (Node lv l' ab' r)))" |
26 else let (l',ab') = split_max l in adjust (Node l' ab' lv r)))" |
27 |
27 |
28 |
28 |
29 subsection "Invariance" |
29 subsection "Invariance" |
30 |
30 |
31 subsubsection "Proofs for insert" |
31 subsubsection "Proofs for insert" |
44 |
44 |
45 declare invar.simps(2)[simp] |
45 declare invar.simps(2)[simp] |
46 |
46 |
47 lemma lvl_update_sngl: "invar t \<Longrightarrow> sngl t \<Longrightarrow> lvl(update x y t) = lvl t" |
47 lemma lvl_update_sngl: "invar t \<Longrightarrow> sngl t \<Longrightarrow> lvl(update x y t) = lvl t" |
48 proof (induction t rule: update.induct) |
48 proof (induction t rule: update.induct) |
49 case (2 x y lv t1 a b t2) |
49 case (2 x y t1 a b lv t2) |
50 consider (LT) "x < a" | (GT) "x > a" | (EQ) "x = a" |
50 consider (LT) "x < a" | (GT) "x > a" | (EQ) "x = a" |
51 using less_linear by blast |
51 using less_linear by blast |
52 thus ?case proof cases |
52 thus ?case proof cases |
53 case LT |
53 case LT |
54 thus ?thesis using 2 by (auto simp add: skew_case split_case split: tree.splits) |
54 thus ?thesis using 2 by (auto simp add: skew_case split_case split: tree.splits) |
62 qed (auto simp add: lvl_0_iff) |
62 qed (auto simp add: lvl_0_iff) |
63 qed simp |
63 qed simp |
64 qed simp |
64 qed simp |
65 |
65 |
66 lemma lvl_update_incr_iff: "(lvl(update a b t) = lvl t + 1) \<longleftrightarrow> |
66 lemma lvl_update_incr_iff: "(lvl(update a b t) = lvl t + 1) \<longleftrightarrow> |
67 (\<exists>l x r. update a b t = Node (lvl t + 1) l x r \<and> lvl l = lvl r)" |
67 (\<exists>l x r. update a b t = Node l x (lvl t + 1) r \<and> lvl l = lvl r)" |
68 apply(cases t) |
68 apply(cases t) |
69 apply(auto simp add: skew_case split_case split: if_splits) |
69 apply(auto simp add: skew_case split_case split: if_splits) |
70 apply(auto split: tree.splits if_splits) |
70 apply(auto split: tree.splits if_splits) |
71 done |
71 done |
72 |
72 |
73 lemma invar_update: "invar t \<Longrightarrow> invar(update a b t)" |
73 lemma invar_update: "invar t \<Longrightarrow> invar(update a b t)" |
74 proof(induction t) |
74 proof(induction t) |
75 case N: (Node n l xy r) |
75 case N: (Node l xy n r) |
76 hence il: "invar l" and ir: "invar r" by auto |
76 hence il: "invar l" and ir: "invar r" by auto |
77 note iil = N.IH(1)[OF il] |
77 note iil = N.IH(1)[OF il] |
78 note iir = N.IH(2)[OF ir] |
78 note iir = N.IH(2)[OF ir] |
79 obtain x y where [simp]: "xy = (x,y)" by fastforce |
79 obtain x y where [simp]: "xy = (x,y)" by fastforce |
80 let ?t = "Node n l xy r" |
80 let ?t = "Node l xy n r" |
81 have "a < x \<or> a = x \<or> x < a" by auto |
81 have "a < x \<or> a = x \<or> x < a" by auto |
82 moreover |
82 moreover |
83 have ?case if "a < x" |
83 have ?case if "a < x" |
84 proof (cases rule: lvl_update[of a b l]) |
84 proof (cases rule: lvl_update[of a b l]) |
85 case (Same) thus ?thesis |
85 case (Same) thus ?thesis |
86 using \<open>a<x\<close> invar_NodeL[OF N.prems iil Same] |
86 using \<open>a<x\<close> invar_NodeL[OF N.prems iil Same] |
87 by (simp add: skew_invar split_invar del: invar.simps) |
87 by (simp add: skew_invar split_invar del: invar.simps) |
88 next |
88 next |
89 case (Incr) |
89 case (Incr) |
90 then obtain t1 w t2 where ial[simp]: "update a b l = Node n t1 w t2" |
90 then obtain t1 w t2 where ial[simp]: "update a b l = Node t1 w n t2" |
91 using N.prems by (auto simp: lvl_Suc_iff) |
91 using N.prems by (auto simp: lvl_Suc_iff) |
92 have l12: "lvl t1 = lvl t2" |
92 have l12: "lvl t1 = lvl t2" |
93 by (metis Incr(1) ial lvl_update_incr_iff tree.inject) |
93 by (metis Incr(1) ial lvl_update_incr_iff tree.inject) |
94 have "update a b ?t = split(skew(Node n (update a b l) xy r))" |
94 have "update a b ?t = split(skew(Node (update a b l) xy n r))" |
95 by(simp add: \<open>a<x\<close>) |
95 by(simp add: \<open>a<x\<close>) |
96 also have "skew(Node n (update a b l) xy r) = Node n t1 w (Node n t2 xy r)" |
96 also have "skew(Node (update a b l) xy n r) = Node t1 w n (Node t2 xy n r)" |
97 by(simp) |
97 by(simp) |
98 also have "invar(split \<dots>)" |
98 also have "invar(split \<dots>)" |
99 proof (cases r) |
99 proof (cases r) |
100 case Leaf |
100 case Leaf |
101 hence "l = Leaf" using N.prems by(auto simp: lvl_0_iff) |
101 hence "l = Leaf" using N.prems by(auto simp: lvl_0_iff) |
102 thus ?thesis using Leaf ial by simp |
102 thus ?thesis using Leaf ial by simp |
103 next |
103 next |
104 case [simp]: (Node m t3 y t4) |
104 case [simp]: (Node t3 y m t4) |
105 show ?thesis (*using N(3) iil l12 by(auto)*) |
105 show ?thesis (*using N(3) iil l12 by(auto)*) |
106 proof cases |
106 proof cases |
107 assume "m = n" thus ?thesis using N(3) iil by(auto) |
107 assume "m = n" thus ?thesis using N(3) iil by(auto) |
108 next |
108 next |
109 assume "m \<noteq> n" thus ?thesis using N(3) iil l12 by(auto) |
109 assume "m \<noteq> n" thus ?thesis using N(3) iil l12 by(auto) |
116 proof - |
116 proof - |
117 from \<open>invar ?t\<close> have "n = lvl r \<or> n = lvl r + 1" by auto |
117 from \<open>invar ?t\<close> have "n = lvl r \<or> n = lvl r + 1" by auto |
118 thus ?case |
118 thus ?case |
119 proof |
119 proof |
120 assume 0: "n = lvl r" |
120 assume 0: "n = lvl r" |
121 have "update a b ?t = split(skew(Node n l xy (update a b r)))" |
121 have "update a b ?t = split(skew(Node l xy n (update a b r)))" |
122 using \<open>a>x\<close> by(auto) |
122 using \<open>a>x\<close> by(auto) |
123 also have "skew(Node n l xy (update a b r)) = Node n l xy (update a b r)" |
123 also have "skew(Node l xy n (update a b r)) = Node l xy n (update a b r)" |
124 using N.prems by(simp add: skew_case split: tree.split) |
124 using N.prems by(simp add: skew_case split: tree.split) |
125 also have "invar(split \<dots>)" |
125 also have "invar(split \<dots>)" |
126 proof - |
126 proof - |
127 from lvl_update_sngl[OF ir sngl_if_invar[OF \<open>invar ?t\<close> 0], of a b] |
127 from lvl_update_sngl[OF ir sngl_if_invar[OF \<open>invar ?t\<close> 0], of a b] |
128 obtain t1 p t2 where iar: "update a b r = Node n t1 p t2" |
128 obtain t1 p t2 where iar: "update a b r = Node t1 p n t2" |
129 using N.prems 0 by (auto simp: lvl_Suc_iff) |
129 using N.prems 0 by (auto simp: lvl_Suc_iff) |
130 from N.prems iar 0 iir |
130 from N.prems iar 0 iir |
131 show ?thesis by (auto simp: split_case split: tree.splits) |
131 show ?thesis by (auto simp: split_case split: tree.splits) |
132 qed |
132 qed |
133 finally show ?thesis . |
133 finally show ?thesis . |
155 |
155 |
156 declare invar.simps(2)[simp del] |
156 declare invar.simps(2)[simp del] |
157 |
157 |
158 theorem post_delete: "invar t \<Longrightarrow> post_del t (delete x t)" |
158 theorem post_delete: "invar t \<Longrightarrow> post_del t (delete x t)" |
159 proof (induction t) |
159 proof (induction t) |
160 case (Node lv l ab r) |
160 case (Node l ab lv r) |
161 |
161 |
162 obtain a b where [simp]: "ab = (a,b)" by fastforce |
162 obtain a b where [simp]: "ab = (a,b)" by fastforce |
163 |
163 |
164 let ?l' = "delete x l" and ?r' = "delete x r" |
164 let ?l' = "delete x l" and ?r' = "delete x r" |
165 let ?t = "Node lv l ab r" let ?t' = "delete x ?t" |
165 let ?t = "Node l ab lv r" let ?t' = "delete x ?t" |
166 |
166 |
167 from Node.prems have inv_l: "invar l" and inv_r: "invar r" by (auto) |
167 from Node.prems have inv_l: "invar l" and inv_r: "invar r" by (auto) |
168 |
168 |
169 note post_l' = Node.IH(1)[OF inv_l] |
169 note post_l' = Node.IH(1)[OF inv_l] |
170 note preL = pre_adj_if_postL[OF Node.prems post_l'] |
170 note preL = pre_adj_if_postL[OF Node.prems post_l'] |