src/HOL/ex/AVL.ML
changeset 8797 b55e2354d71e
child 12486 0ed8bdd883e0
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/AVL.ML	Fri May 05 12:51:33 2000 +0200
     1.3 @@ -0,0 +1,307 @@
     1.4 +(*  Title:      HOL/ex/AVL.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Cornelia Pusch and Tobias Nipkow
     1.7 +    Copyright   1998  TUM
     1.8 +*)
     1.9 +
    1.10 +(******************************    isbal    **********************************)
    1.11 +
    1.12 +Addsimps[Let_def];
    1.13 +
    1.14 +(* rotations preserve isbal property *)
    1.15 +
    1.16 +Goalw [bal_def]
    1.17 +"height l = Suc(Suc(height r)) --> bal l = Right --> isbal l --> isbal r \
    1.18 +\ --> isbal (lr_rot (n, l, r))";
    1.19 +by (case_tac "l" 1); 
    1.20 + by (Asm_simp_tac 1);
    1.21 +by (case_tac "tree2" 1);
    1.22 + by (Asm_simp_tac 1);
    1.23 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    1.24 +by (arith_tac 1);
    1.25 +qed_spec_mp "isbal_lr_rot";
    1.26 +
    1.27 +
    1.28 +Goalw [bal_def]
    1.29 +"height l = Suc(Suc(height r)) --> bal l ~= Right --> isbal l --> isbal r \
    1.30 +\ --> isbal (r_rot (n, l, r))";
    1.31 +by (case_tac "l" 1); 
    1.32 + by (Asm_simp_tac 1);
    1.33 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    1.34 +qed_spec_mp "isbal_r_rot";
    1.35 +
    1.36 +
    1.37 +Goalw [bal_def]
    1.38 +"height r = Suc(Suc(height l)) --> bal r = Left --> isbal l --> isbal r \
    1.39 +\ --> isbal (rl_rot (n, l, r))";
    1.40 +by (case_tac "r" 1); 
    1.41 + by (Asm_simp_tac 1);
    1.42 +by (case_tac "tree1" 1);
    1.43 + by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    1.44 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    1.45 +by (arith_tac 1);
    1.46 +qed_spec_mp "isbal_rl_rot";
    1.47 +
    1.48 +
    1.49 +Goalw [bal_def]
    1.50 +"height r = Suc(Suc(height l)) --> bal r ~= Left --> isbal l --> isbal r \
    1.51 +\ --> isbal (l_rot (n, l, r))";
    1.52 +by (case_tac "r" 1); 
    1.53 + by (Asm_simp_tac 1);
    1.54 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    1.55 +qed_spec_mp "isbal_l_rot";
    1.56 +
    1.57 +
    1.58 +(* lemmas about height after rotation *)
    1.59 +
    1.60 +Goalw [bal_def]
    1.61 +"bal l = Right --> height l = Suc(Suc(height r))   \
    1.62 +\ -->     Suc(height (lr_rot (n, l, r)))  = height (MKT n l r) ";
    1.63 +by (case_tac "l" 1); 
    1.64 + by (Asm_simp_tac 1);
    1.65 +by (case_tac "tree2" 1);
    1.66 + by (Asm_simp_tac 1);
    1.67 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    1.68 +qed_spec_mp "height_lr_rot";
    1.69 +
    1.70 +
    1.71 +Goalw [bal_def]
    1.72 +"height l = Suc(Suc(height r)) --> bal l ~= Right \
    1.73 +\ --> Suc(height (r_rot (n, l, r))) = height (MKT n l r) | \
    1.74 +\         height (r_rot (n, l, r))  = height (MKT n l r)";
    1.75 +by (case_tac "l" 1); 
    1.76 + by (Asm_simp_tac 1);
    1.77 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    1.78 +qed_spec_mp "height_r_rot";
    1.79 +
    1.80 +
    1.81 +Goalw [l_bal_def]
    1.82 +"height l = Suc(Suc(height r))  \
    1.83 +\ --> Suc(height (l_bal n l r)) = height (MKT n l r) | \
    1.84 +\         height (l_bal n l r)  = height (MKT n l r)";
    1.85 +by (case_tac "bal l = Right" 1);
    1.86 + by (fast_tac (claset() addDs [height_lr_rot] addss simpset()) 1);
    1.87 +by (fast_tac (claset() addDs [height_r_rot] addss simpset()) 1);
    1.88 +qed_spec_mp "height_l_bal";
    1.89 +
    1.90 +
    1.91 +Goalw [bal_def]
    1.92 +"height r = Suc(Suc(height l)) --> bal r = Left \
    1.93 +\ -->     Suc(height (rl_rot (n, l, r)))  = height (MKT n l r)";
    1.94 +by (case_tac "r" 1); 
    1.95 + by (Asm_simp_tac 1);
    1.96 +by (case_tac "tree1" 1);
    1.97 + by (Asm_simp_tac 1);
    1.98 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    1.99 +by (arith_tac 1);
   1.100 +qed_spec_mp "height_rl_rot";
   1.101 +
   1.102 +
   1.103 +Goalw [bal_def]
   1.104 +"height r = Suc(Suc(height l)) --> bal r ~= Left \
   1.105 +\ --> Suc(height (l_rot (n, l, r))) = height (MKT n l r) | \
   1.106 +\         height (l_rot (n, l, r))  = height (MKT n l r)";
   1.107 +by (case_tac "r" 1); 
   1.108 + by (Asm_simp_tac 1);
   1.109 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
   1.110 +qed_spec_mp "height_l_rot";
   1.111 +
   1.112 +
   1.113 +Goalw [r_bal_def]
   1.114 +"height r = Suc(Suc(height l))  \
   1.115 +\ --> Suc(height (r_bal n l r)) = height (MKT n l r) | \
   1.116 +\         height (r_bal n l r)  = height (MKT n l r)";
   1.117 +by (case_tac "bal r = Left" 1);
   1.118 + by (fast_tac (claset() addDs [height_rl_rot] addss simpset()) 1);
   1.119 +by (fast_tac (claset() addDs [height_l_rot] addss simpset()) 1);
   1.120 +qed_spec_mp "height_r_bal";
   1.121 +
   1.122 +
   1.123 +(* lemma about height after insert *)
   1.124 +Goal
   1.125 +"isbal t  \
   1.126 +\ --> height (insert x t) = height t | height (insert x t) = Suc(height t)";
   1.127 +by (induct_tac "t" 1);
   1.128 + by (Simp_tac 1);
   1.129 +by (case_tac "x=nat" 1);
   1.130 + by (Asm_simp_tac 1);
   1.131 +by (case_tac "x<nat" 1);
   1.132 + by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);
   1.133 +  by (forw_inst_tac [("n","nat")]  height_l_bal 1);  
   1.134 +  by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
   1.135 +  by(fast_tac (claset() addss simpset()) 1);
   1.136 + by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
   1.137 + by(fast_tac (claset() addss simpset()) 1);
   1.138 +by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
   1.139 + by (forw_inst_tac [("n","nat")]  height_r_bal 1); 
   1.140 + by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
   1.141 + by(fast_tac (claset() addss simpset()) 1);
   1.142 +by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
   1.143 +by(fast_tac (claset() addss simpset()) 1);
   1.144 +qed_spec_mp "height_insert";
   1.145 +
   1.146 +
   1.147 +Goal
   1.148 +"!!x. [| height (insert x l) ~= Suc(Suc(height r)); isbal (insert x l); isbal (MKT n l r) |] \
   1.149 +\ ==> isbal (MKT n (insert x l) r)";
   1.150 +by (cut_inst_tac [("x","x"),("t","l")] height_insert 1);
   1.151 + by (Asm_full_simp_tac 1); 
   1.152 +by (fast_tac (claset() addss simpset()) 1);
   1.153 +qed "isbal_insert_left";
   1.154 +
   1.155 +
   1.156 +Goal
   1.157 +"!!x. [| height (insert x r) ~= Suc(Suc(height l)); isbal (insert x r); isbal (MKT n l r) |] \
   1.158 +\ ==> isbal (MKT n l (insert x r))";
   1.159 +by (cut_inst_tac [("x","x"),("t","r")] height_insert 1);
   1.160 + by (Asm_full_simp_tac 1); 
   1.161 +by (fast_tac (claset() addss simpset()) 1);
   1.162 +qed "isbal_insert_right";
   1.163 +
   1.164 +(* insert-operation preserves isbal property *)
   1.165 +
   1.166 +Goal
   1.167 +"isbal t --> isbal(insert x t)";
   1.168 +by (induct_tac "t" 1);
   1.169 + by (Simp_tac 1);
   1.170 +by (case_tac "x=nat" 1);
   1.171 + by (Asm_simp_tac 1); 
   1.172 +by (case_tac "x<nat" 1);
   1.173 + by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);
   1.174 +  by (case_tac "bal (insert x tree1) = Right" 1);
   1.175 +   by (fast_tac (claset() addIs [isbal_lr_rot] addss (simpset() 
   1.176 +	addsimps [l_bal_def])) 1);  
   1.177 +  by (fast_tac (claset() addIs [isbal_r_rot] addss (simpset() 
   1.178 +	addsimps [l_bal_def])) 1);  
   1.179 + by (Clarify_tac 1);
   1.180 + by (forward_tac [isbal_insert_left] 1);
   1.181 +   by (Asm_full_simp_tac 1); 
   1.182 +  ba 1;
   1.183 + by (Asm_full_simp_tac 1); 
   1.184 +by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
   1.185 + by (case_tac "bal (insert x tree2) = Left" 1);
   1.186 +  by (fast_tac (claset() addIs [isbal_rl_rot] addss (simpset() 
   1.187 +	addsimps [r_bal_def])) 1);  
   1.188 + by (fast_tac (claset() addIs [isbal_l_rot] addss (simpset() 
   1.189 +	addsimps [r_bal_def])) 1);  
   1.190 +by (Clarify_tac 1);
   1.191 +by (forward_tac [isbal_insert_right] 1);
   1.192 +   by (Asm_full_simp_tac 1); 
   1.193 +  ba 1;
   1.194 + by (Asm_full_simp_tac 1); 
   1.195 +qed_spec_mp "isbal_insert";
   1.196 +
   1.197 +
   1.198 +(******************************    isin    **********************************)
   1.199 +
   1.200 +
   1.201 +(* rotations preserve isin property *)
   1.202 +
   1.203 +Goalw [bal_def]
   1.204 +"height l = Suc(Suc(height r)) --> bal l = Right  \
   1.205 +\ --> isin x (lr_rot (n, l, r)) = isin x (MKT n l r)";
   1.206 +by (case_tac "l" 1); 
   1.207 + by (Asm_simp_tac 1);
   1.208 +by (case_tac "tree2" 1);
   1.209 + by (Asm_simp_tac 1);
   1.210 +by (fast_tac (claset() addss simpset()) 1);
   1.211 +qed_spec_mp "isin_lr_rot";
   1.212 +
   1.213 +
   1.214 +Goalw [bal_def]
   1.215 +"height l = Suc(Suc(height r)) --> bal l ~= Right  \
   1.216 +\ --> isin x (r_rot (n, l, r)) = isin x (MKT n l r)";
   1.217 +by (case_tac "l" 1); 
   1.218 + by (Asm_simp_tac 1);
   1.219 +by (fast_tac (claset() addss simpset()) 1);
   1.220 +qed_spec_mp "isin_r_rot";
   1.221 +
   1.222 +
   1.223 +Goalw [bal_def]
   1.224 +"height r = Suc(Suc(height l)) --> bal r = Left  \
   1.225 +\ --> isin x (rl_rot (n, l, r)) = isin x (MKT n l r)";
   1.226 +by (case_tac "r" 1); 
   1.227 + by (Asm_simp_tac 1);
   1.228 +by (case_tac "tree1" 1);
   1.229 + by (asm_simp_tac (simpset() addsimps [max_def,le_def]) 1);
   1.230 +by (fast_tac (claset() addss simpset()) 1);
   1.231 +qed_spec_mp "isin_rl_rot";
   1.232 +
   1.233 +
   1.234 +Goalw [bal_def]
   1.235 +"height r = Suc(Suc(height l)) --> bal r ~= Left  \
   1.236 +\ --> isin x (l_rot (n, l, r)) = isin x (MKT n l r)";
   1.237 +by (case_tac "r" 1); 
   1.238 + by (Asm_simp_tac 1);
   1.239 +by (fast_tac (claset() addss simpset()) 1);
   1.240 +qed_spec_mp "isin_l_rot";
   1.241 +
   1.242 +
   1.243 +(* isin insert *)
   1.244 +
   1.245 +Goal
   1.246 +"isin y (insert x t) = (y=x | isin y t)";
   1.247 +by (induct_tac "t" 1);
   1.248 + by (Asm_simp_tac 1);
   1.249 +by(asm_simp_tac (simpset() addsimps [l_bal_def,isin_lr_rot,isin_r_rot,
   1.250 +	r_bal_def,isin_rl_rot,isin_l_rot]) 1);
   1.251 +by(Blast_tac 1);
   1.252 +qed "isin_insert";
   1.253 +
   1.254 +
   1.255 +(******************************    isord    **********************************)
   1.256 +
   1.257 +(* rotations preserve isord property *)
   1.258 +
   1.259 +Goalw [bal_def]
   1.260 +"height l = Suc(Suc(height r)) --> bal l = Right --> isord (MKT n l r) \
   1.261 +\ --> isord (lr_rot (n, l, r))";
   1.262 +by (case_tac "l" 1); 
   1.263 + by (Asm_simp_tac 1);
   1.264 +by (case_tac "tree2" 1);
   1.265 + by (Asm_simp_tac 1);
   1.266 +by (Asm_simp_tac 1);
   1.267 +by(blast_tac (claset() addIs [less_trans])1);
   1.268 +qed_spec_mp "isord_lr_rot";
   1.269 +
   1.270 +
   1.271 +Goalw [bal_def]
   1.272 +"height l = Suc(Suc(height r)) --> bal l ~= Right --> isord (MKT n l r) \
   1.273 +\ --> isord (r_rot (n, l, r))";
   1.274 +by (case_tac "l" 1); 
   1.275 + by (Asm_simp_tac 1);
   1.276 +by (auto_tac (claset() addIs [less_trans],simpset()));
   1.277 +qed_spec_mp "isord_r_rot";
   1.278 +
   1.279 +
   1.280 +Goalw [bal_def]
   1.281 +"height r = Suc(Suc(height l)) --> bal r = Left --> isord (MKT n l r) \
   1.282 +\ --> isord (rl_rot (n, l, r))";
   1.283 +by (case_tac "r" 1); 
   1.284 + by (Asm_simp_tac 1);
   1.285 +by (case_tac "tree1" 1);
   1.286 + by (asm_simp_tac (simpset() addsimps [le_def]) 1);
   1.287 +by (Asm_simp_tac 1);
   1.288 +by(blast_tac (claset() addIs [less_trans])1);
   1.289 +qed_spec_mp "isord_rl_rot";
   1.290 +
   1.291 +
   1.292 +Goalw [bal_def]
   1.293 +"height r = Suc(Suc(height l)) --> bal r ~= Left --> isord (MKT n l r)  \
   1.294 +\ --> isord (l_rot (n, l, r))";
   1.295 +by (case_tac "r" 1); 
   1.296 + by (Asm_simp_tac 1);
   1.297 +by (Asm_simp_tac 1);
   1.298 +by(blast_tac (claset() addIs [less_trans])1);
   1.299 +qed_spec_mp "isord_l_rot";
   1.300 +
   1.301 +(* insert operation presreves isord property *)
   1.302 +
   1.303 +Goal
   1.304 +"isord t --> isord(insert x t)";
   1.305 +by (induct_tac "t" 1);
   1.306 + by (Simp_tac 1);
   1.307 +by (cut_inst_tac [("m","x"),("n","nat")] less_linear 1);
   1.308 + by (fast_tac (claset() addss (simpset() addsimps [l_bal_def,isord_lr_rot,
   1.309 +	isord_r_rot,r_bal_def,isord_l_rot,isord_rl_rot,isin_insert])) 1);  
   1.310 +qed_spec_mp "isord_insert";