8797

1 
(* Title: HOL/ex/AVL.ML


2 
ID: $Id$


3 
Author: Cornelia Pusch and Tobias Nipkow


4 
Copyright 1998 TUM


5 
*)


6 


7 
(****************************** isbal **********************************)


8 


9 
Addsimps[Let_def];


10 


11 
(* rotations preserve isbal property *)


12 


13 
Goalw [bal_def]


14 
"height l = Suc(Suc(height r)) > bal l = Right > isbal l > isbal r \


15 
\ > isbal (lr_rot (n, l, r))";


16 
by (case_tac "l" 1);


17 
by (Asm_simp_tac 1);


18 
by (case_tac "tree2" 1);


19 
by (Asm_simp_tac 1);


20 
by (asm_simp_tac (simpset() addsimps [max_def]) 1);


21 
by (arith_tac 1);


22 
qed_spec_mp "isbal_lr_rot";


23 


24 


25 
Goalw [bal_def]


26 
"height l = Suc(Suc(height r)) > bal l ~= Right > isbal l > isbal r \


27 
\ > isbal (r_rot (n, l, r))";


28 
by (case_tac "l" 1);


29 
by (Asm_simp_tac 1);


30 
by (asm_simp_tac (simpset() addsimps [max_def]) 1);


31 
qed_spec_mp "isbal_r_rot";


32 


33 


34 
Goalw [bal_def]


35 
"height r = Suc(Suc(height l)) > bal r = Left > isbal l > isbal r \


36 
\ > isbal (rl_rot (n, l, r))";


37 
by (case_tac "r" 1);


38 
by (Asm_simp_tac 1);


39 
by (case_tac "tree1" 1);


40 
by (asm_simp_tac (simpset() addsimps [max_def]) 1);


41 
by (asm_simp_tac (simpset() addsimps [max_def]) 1);


42 
by (arith_tac 1);


43 
qed_spec_mp "isbal_rl_rot";


44 


45 


46 
Goalw [bal_def]


47 
"height r = Suc(Suc(height l)) > bal r ~= Left > isbal l > isbal r \


48 
\ > isbal (l_rot (n, l, r))";


49 
by (case_tac "r" 1);


50 
by (Asm_simp_tac 1);


51 
by (asm_simp_tac (simpset() addsimps [max_def]) 1);


52 
qed_spec_mp "isbal_l_rot";


53 


54 


55 
(* lemmas about height after rotation *)


56 


57 
Goalw [bal_def]


58 
"bal l = Right > height l = Suc(Suc(height r)) \


59 
\ > Suc(height (lr_rot (n, l, r))) = height (MKT n l r) ";


60 
by (case_tac "l" 1);


61 
by (Asm_simp_tac 1);


62 
by (case_tac "tree2" 1);


63 
by (Asm_simp_tac 1);


64 
by (asm_simp_tac (simpset() addsimps [max_def]) 1);


65 
qed_spec_mp "height_lr_rot";


66 


67 


68 
Goalw [bal_def]


69 
"height l = Suc(Suc(height r)) > bal l ~= Right \


70 
\ > Suc(height (r_rot (n, l, r))) = height (MKT n l r)  \


71 
\ height (r_rot (n, l, r)) = height (MKT n l r)";


72 
by (case_tac "l" 1);


73 
by (Asm_simp_tac 1);


74 
by (asm_simp_tac (simpset() addsimps [max_def]) 1);


75 
qed_spec_mp "height_r_rot";


76 


77 


78 
Goalw [l_bal_def]


79 
"height l = Suc(Suc(height r)) \


80 
\ > Suc(height (l_bal n l r)) = height (MKT n l r)  \


81 
\ height (l_bal n l r) = height (MKT n l r)";


82 
by (case_tac "bal l = Right" 1);


83 
by (fast_tac (claset() addDs [height_lr_rot] addss simpset()) 1);


84 
by (fast_tac (claset() addDs [height_r_rot] addss simpset()) 1);


85 
qed_spec_mp "height_l_bal";


86 


87 


88 
Goalw [bal_def]


89 
"height r = Suc(Suc(height l)) > bal r = Left \


90 
\ > Suc(height (rl_rot (n, l, r))) = height (MKT n l r)";


91 
by (case_tac "r" 1);


92 
by (Asm_simp_tac 1);


93 
by (case_tac "tree1" 1);


94 
by (Asm_simp_tac 1);


95 
by (asm_simp_tac (simpset() addsimps [max_def]) 1);


96 
by (arith_tac 1);


97 
qed_spec_mp "height_rl_rot";


98 


99 


100 
Goalw [bal_def]


101 
"height r = Suc(Suc(height l)) > bal r ~= Left \


102 
\ > Suc(height (l_rot (n, l, r))) = height (MKT n l r)  \


103 
\ height (l_rot (n, l, r)) = height (MKT n l r)";


104 
by (case_tac "r" 1);


105 
by (Asm_simp_tac 1);


106 
by (asm_simp_tac (simpset() addsimps [max_def]) 1);


107 
qed_spec_mp "height_l_rot";


108 


109 


110 
Goalw [r_bal_def]


111 
"height r = Suc(Suc(height l)) \


112 
\ > Suc(height (r_bal n l r)) = height (MKT n l r)  \


113 
\ height (r_bal n l r) = height (MKT n l r)";


114 
by (case_tac "bal r = Left" 1);


115 
by (fast_tac (claset() addDs [height_rl_rot] addss simpset()) 1);


116 
by (fast_tac (claset() addDs [height_l_rot] addss simpset()) 1);


117 
qed_spec_mp "height_r_bal";


118 


119 


120 
(* lemma about height after insert *)


121 
Goal


122 
"isbal t \


123 
\ > height (insert x t) = height t  height (insert x t) = Suc(height t)";


124 
by (induct_tac "t" 1);


125 
by (Simp_tac 1);


126 
by (case_tac "x=nat" 1);


127 
by (Asm_simp_tac 1);


128 
by (case_tac "x<nat" 1);


129 
by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);


130 
by (forw_inst_tac [("n","nat")] height_l_bal 1);


131 
by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);


132 
by(fast_tac (claset() addss simpset()) 1);


133 
by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);


134 
by(fast_tac (claset() addss simpset()) 1);


135 
by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);


136 
by (forw_inst_tac [("n","nat")] height_r_bal 1);


137 
by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);


138 
by(fast_tac (claset() addss simpset()) 1);


139 
by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);


140 
by(fast_tac (claset() addss simpset()) 1);


141 
qed_spec_mp "height_insert";


142 


143 


144 
Goal


145 
"!!x. [ height (insert x l) ~= Suc(Suc(height r)); isbal (insert x l); isbal (MKT n l r) ] \


146 
\ ==> isbal (MKT n (insert x l) r)";


147 
by (cut_inst_tac [("x","x"),("t","l")] height_insert 1);


148 
by (Asm_full_simp_tac 1);


149 
by (fast_tac (claset() addss simpset()) 1);


150 
qed "isbal_insert_left";


151 


152 


153 
Goal


154 
"!!x. [ height (insert x r) ~= Suc(Suc(height l)); isbal (insert x r); isbal (MKT n l r) ] \


155 
\ ==> isbal (MKT n l (insert x r))";


156 
by (cut_inst_tac [("x","x"),("t","r")] height_insert 1);


157 
by (Asm_full_simp_tac 1);


158 
by (fast_tac (claset() addss simpset()) 1);


159 
qed "isbal_insert_right";


160 


161 
(* insertoperation preserves isbal property *)


162 


163 
Goal


164 
"isbal t > isbal(insert x t)";


165 
by (induct_tac "t" 1);


166 
by (Simp_tac 1);


167 
by (case_tac "x=nat" 1);


168 
by (Asm_simp_tac 1);


169 
by (case_tac "x<nat" 1);


170 
by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);


171 
by (case_tac "bal (insert x tree1) = Right" 1);


172 
by (fast_tac (claset() addIs [isbal_lr_rot] addss (simpset()


173 
addsimps [l_bal_def])) 1);


174 
by (fast_tac (claset() addIs [isbal_r_rot] addss (simpset()


175 
addsimps [l_bal_def])) 1);


176 
by (Clarify_tac 1);


177 
by (forward_tac [isbal_insert_left] 1);


178 
by (Asm_full_simp_tac 1);


179 
ba 1;


180 
by (Asm_full_simp_tac 1);


181 
by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);


182 
by (case_tac "bal (insert x tree2) = Left" 1);


183 
by (fast_tac (claset() addIs [isbal_rl_rot] addss (simpset()


184 
addsimps [r_bal_def])) 1);


185 
by (fast_tac (claset() addIs [isbal_l_rot] addss (simpset()


186 
addsimps [r_bal_def])) 1);


187 
by (Clarify_tac 1);


188 
by (forward_tac [isbal_insert_right] 1);


189 
by (Asm_full_simp_tac 1);


190 
ba 1;


191 
by (Asm_full_simp_tac 1);


192 
qed_spec_mp "isbal_insert";


193 


194 


195 
(****************************** isin **********************************)


196 


197 


198 
(* rotations preserve isin property *)


199 


200 
Goalw [bal_def]


201 
"height l = Suc(Suc(height r)) > bal l = Right \


202 
\ > isin x (lr_rot (n, l, r)) = isin x (MKT n l r)";


203 
by (case_tac "l" 1);


204 
by (Asm_simp_tac 1);


205 
by (case_tac "tree2" 1);


206 
by (Asm_simp_tac 1);


207 
by (fast_tac (claset() addss simpset()) 1);


208 
qed_spec_mp "isin_lr_rot";


209 


210 


211 
Goalw [bal_def]


212 
"height l = Suc(Suc(height r)) > bal l ~= Right \


213 
\ > isin x (r_rot (n, l, r)) = isin x (MKT n l r)";


214 
by (case_tac "l" 1);


215 
by (Asm_simp_tac 1);


216 
by (fast_tac (claset() addss simpset()) 1);


217 
qed_spec_mp "isin_r_rot";


218 


219 


220 
Goalw [bal_def]


221 
"height r = Suc(Suc(height l)) > bal r = Left \


222 
\ > isin x (rl_rot (n, l, r)) = isin x (MKT n l r)";


223 
by (case_tac "r" 1);


224 
by (Asm_simp_tac 1);


225 
by (case_tac "tree1" 1);


226 
by (asm_simp_tac (simpset() addsimps [max_def,le_def]) 1);


227 
by (fast_tac (claset() addss simpset()) 1);


228 
qed_spec_mp "isin_rl_rot";


229 


230 


231 
Goalw [bal_def]


232 
"height r = Suc(Suc(height l)) > bal r ~= Left \


233 
\ > isin x (l_rot (n, l, r)) = isin x (MKT n l r)";


234 
by (case_tac "r" 1);


235 
by (Asm_simp_tac 1);


236 
by (fast_tac (claset() addss simpset()) 1);


237 
qed_spec_mp "isin_l_rot";


238 


239 


240 
(* isin insert *)


241 


242 
Goal


243 
"isin y (insert x t) = (y=x  isin y t)";


244 
by (induct_tac "t" 1);


245 
by (Asm_simp_tac 1);


246 
by(asm_simp_tac (simpset() addsimps [l_bal_def,isin_lr_rot,isin_r_rot,


247 
r_bal_def,isin_rl_rot,isin_l_rot]) 1);


248 
by(Blast_tac 1);


249 
qed "isin_insert";


250 


251 


252 
(****************************** isord **********************************)


253 


254 
(* rotations preserve isord property *)


255 


256 
Goalw [bal_def]


257 
"height l = Suc(Suc(height r)) > bal l = Right > isord (MKT n l r) \


258 
\ > isord (lr_rot (n, l, r))";


259 
by (case_tac "l" 1);


260 
by (Asm_simp_tac 1);


261 
by (case_tac "tree2" 1);


262 
by (Asm_simp_tac 1);


263 
by (Asm_simp_tac 1);


264 
by(blast_tac (claset() addIs [less_trans])1);


265 
qed_spec_mp "isord_lr_rot";


266 


267 


268 
Goalw [bal_def]


269 
"height l = Suc(Suc(height r)) > bal l ~= Right > isord (MKT n l r) \


270 
\ > isord (r_rot (n, l, r))";


271 
by (case_tac "l" 1);


272 
by (Asm_simp_tac 1);


273 
by (auto_tac (claset() addIs [less_trans],simpset()));


274 
qed_spec_mp "isord_r_rot";


275 


276 


277 
Goalw [bal_def]


278 
"height r = Suc(Suc(height l)) > bal r = Left > isord (MKT n l r) \


279 
\ > isord (rl_rot (n, l, r))";


280 
by (case_tac "r" 1);


281 
by (Asm_simp_tac 1);


282 
by (case_tac "tree1" 1);


283 
by (asm_simp_tac (simpset() addsimps [le_def]) 1);


284 
by (Asm_simp_tac 1);


285 
by(blast_tac (claset() addIs [less_trans])1);


286 
qed_spec_mp "isord_rl_rot";


287 


288 


289 
Goalw [bal_def]


290 
"height r = Suc(Suc(height l)) > bal r ~= Left > isord (MKT n l r) \


291 
\ > isord (l_rot (n, l, r))";


292 
by (case_tac "r" 1);


293 
by (Asm_simp_tac 1);


294 
by (Asm_simp_tac 1);


295 
by(blast_tac (claset() addIs [less_trans])1);


296 
qed_spec_mp "isord_l_rot";


297 


298 
(* insert operation presreves isord property *)


299 


300 
Goal


301 
"isord t > isord(insert x t)";


302 
by (induct_tac "t" 1);


303 
by (Simp_tac 1);


304 
by (cut_inst_tac [("m","x"),("n","nat")] less_linear 1);


305 
by (fast_tac (claset() addss (simpset() addsimps [l_bal_def,isord_lr_rot,


306 
isord_r_rot,r_bal_def,isord_l_rot,isord_rl_rot,isin_insert])) 1);


307 
qed_spec_mp "isord_insert";
