Added AVL
authornipkow
Fri May 05 12:51:33 2000 +0200 (2000-05-05)
changeset 8797b55e2354d71e
parent 8796 4a3612f30865
child 8798 d289a68e74ea
Added AVL
src/HOL/IsaMakefile
src/HOL/ex/AVL.ML
src/HOL/ex/AVL.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu May 04 18:40:57 2000 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri May 05 12:51:33 2000 +0200
     1.3 @@ -413,9 +413,9 @@
     1.4  
     1.5  HOL-ex: HOL $(LOG)/HOL-ex.gz
     1.6  
     1.7 -$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/BT.ML ex/BT.thy ex/Fib.ML ex/Fib.thy \
     1.8 +$(LOG)/HOL-ex.gz: $(OUT)/HOL  ex/AVL.ML ex/AVL.thy ex/BT.ML ex/BT.thy \
     1.9    ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \
    1.10 -  ex/NatSum.thy ex/Primes.ML ex/Primes.thy \
    1.11 +  ex/NatSum.thy ex/Fib.ML ex/Fib.thy ex/Primes.ML ex/Primes.thy \
    1.12    ex/Factorization.ML ex/Factorization.thy \
    1.13    ex/Primrec.ML ex/Primrec.thy \
    1.14    ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/AVL.ML	Fri May 05 12:51:33 2000 +0200
     2.3 @@ -0,0 +1,307 @@
     2.4 +(*  Title:      HOL/ex/AVL.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Cornelia Pusch and Tobias Nipkow
     2.7 +    Copyright   1998  TUM
     2.8 +*)
     2.9 +
    2.10 +(******************************    isbal    **********************************)
    2.11 +
    2.12 +Addsimps[Let_def];
    2.13 +
    2.14 +(* rotations preserve isbal property *)
    2.15 +
    2.16 +Goalw [bal_def]
    2.17 +"height l = Suc(Suc(height r)) --> bal l = Right --> isbal l --> isbal r \
    2.18 +\ --> isbal (lr_rot (n, l, r))";
    2.19 +by (case_tac "l" 1); 
    2.20 + by (Asm_simp_tac 1);
    2.21 +by (case_tac "tree2" 1);
    2.22 + by (Asm_simp_tac 1);
    2.23 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    2.24 +by (arith_tac 1);
    2.25 +qed_spec_mp "isbal_lr_rot";
    2.26 +
    2.27 +
    2.28 +Goalw [bal_def]
    2.29 +"height l = Suc(Suc(height r)) --> bal l ~= Right --> isbal l --> isbal r \
    2.30 +\ --> isbal (r_rot (n, l, r))";
    2.31 +by (case_tac "l" 1); 
    2.32 + by (Asm_simp_tac 1);
    2.33 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    2.34 +qed_spec_mp "isbal_r_rot";
    2.35 +
    2.36 +
    2.37 +Goalw [bal_def]
    2.38 +"height r = Suc(Suc(height l)) --> bal r = Left --> isbal l --> isbal r \
    2.39 +\ --> isbal (rl_rot (n, l, r))";
    2.40 +by (case_tac "r" 1); 
    2.41 + by (Asm_simp_tac 1);
    2.42 +by (case_tac "tree1" 1);
    2.43 + by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    2.44 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    2.45 +by (arith_tac 1);
    2.46 +qed_spec_mp "isbal_rl_rot";
    2.47 +
    2.48 +
    2.49 +Goalw [bal_def]
    2.50 +"height r = Suc(Suc(height l)) --> bal r ~= Left --> isbal l --> isbal r \
    2.51 +\ --> isbal (l_rot (n, l, r))";
    2.52 +by (case_tac "r" 1); 
    2.53 + by (Asm_simp_tac 1);
    2.54 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    2.55 +qed_spec_mp "isbal_l_rot";
    2.56 +
    2.57 +
    2.58 +(* lemmas about height after rotation *)
    2.59 +
    2.60 +Goalw [bal_def]
    2.61 +"bal l = Right --> height l = Suc(Suc(height r))   \
    2.62 +\ -->     Suc(height (lr_rot (n, l, r)))  = height (MKT n l r) ";
    2.63 +by (case_tac "l" 1); 
    2.64 + by (Asm_simp_tac 1);
    2.65 +by (case_tac "tree2" 1);
    2.66 + by (Asm_simp_tac 1);
    2.67 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    2.68 +qed_spec_mp "height_lr_rot";
    2.69 +
    2.70 +
    2.71 +Goalw [bal_def]
    2.72 +"height l = Suc(Suc(height r)) --> bal l ~= Right \
    2.73 +\ --> Suc(height (r_rot (n, l, r))) = height (MKT n l r) | \
    2.74 +\         height (r_rot (n, l, r))  = height (MKT n l r)";
    2.75 +by (case_tac "l" 1); 
    2.76 + by (Asm_simp_tac 1);
    2.77 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    2.78 +qed_spec_mp "height_r_rot";
    2.79 +
    2.80 +
    2.81 +Goalw [l_bal_def]
    2.82 +"height l = Suc(Suc(height r))  \
    2.83 +\ --> Suc(height (l_bal n l r)) = height (MKT n l r) | \
    2.84 +\         height (l_bal n l r)  = height (MKT n l r)";
    2.85 +by (case_tac "bal l = Right" 1);
    2.86 + by (fast_tac (claset() addDs [height_lr_rot] addss simpset()) 1);
    2.87 +by (fast_tac (claset() addDs [height_r_rot] addss simpset()) 1);
    2.88 +qed_spec_mp "height_l_bal";
    2.89 +
    2.90 +
    2.91 +Goalw [bal_def]
    2.92 +"height r = Suc(Suc(height l)) --> bal r = Left \
    2.93 +\ -->     Suc(height (rl_rot (n, l, r)))  = height (MKT n l r)";
    2.94 +by (case_tac "r" 1); 
    2.95 + by (Asm_simp_tac 1);
    2.96 +by (case_tac "tree1" 1);
    2.97 + by (Asm_simp_tac 1);
    2.98 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
    2.99 +by (arith_tac 1);
   2.100 +qed_spec_mp "height_rl_rot";
   2.101 +
   2.102 +
   2.103 +Goalw [bal_def]
   2.104 +"height r = Suc(Suc(height l)) --> bal r ~= Left \
   2.105 +\ --> Suc(height (l_rot (n, l, r))) = height (MKT n l r) | \
   2.106 +\         height (l_rot (n, l, r))  = height (MKT n l r)";
   2.107 +by (case_tac "r" 1); 
   2.108 + by (Asm_simp_tac 1);
   2.109 +by (asm_simp_tac (simpset() addsimps [max_def]) 1);
   2.110 +qed_spec_mp "height_l_rot";
   2.111 +
   2.112 +
   2.113 +Goalw [r_bal_def]
   2.114 +"height r = Suc(Suc(height l))  \
   2.115 +\ --> Suc(height (r_bal n l r)) = height (MKT n l r) | \
   2.116 +\         height (r_bal n l r)  = height (MKT n l r)";
   2.117 +by (case_tac "bal r = Left" 1);
   2.118 + by (fast_tac (claset() addDs [height_rl_rot] addss simpset()) 1);
   2.119 +by (fast_tac (claset() addDs [height_l_rot] addss simpset()) 1);
   2.120 +qed_spec_mp "height_r_bal";
   2.121 +
   2.122 +
   2.123 +(* lemma about height after insert *)
   2.124 +Goal
   2.125 +"isbal t  \
   2.126 +\ --> height (insert x t) = height t | height (insert x t) = Suc(height t)";
   2.127 +by (induct_tac "t" 1);
   2.128 + by (Simp_tac 1);
   2.129 +by (case_tac "x=nat" 1);
   2.130 + by (Asm_simp_tac 1);
   2.131 +by (case_tac "x<nat" 1);
   2.132 + by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);
   2.133 +  by (forw_inst_tac [("n","nat")]  height_l_bal 1);  
   2.134 +  by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
   2.135 +  by(fast_tac (claset() addss simpset()) 1);
   2.136 + by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
   2.137 + by(fast_tac (claset() addss simpset()) 1);
   2.138 +by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
   2.139 + by (forw_inst_tac [("n","nat")]  height_r_bal 1); 
   2.140 + by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
   2.141 + by(fast_tac (claset() addss simpset()) 1);
   2.142 +by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
   2.143 +by(fast_tac (claset() addss simpset()) 1);
   2.144 +qed_spec_mp "height_insert";
   2.145 +
   2.146 +
   2.147 +Goal
   2.148 +"!!x. [| height (insert x l) ~= Suc(Suc(height r)); isbal (insert x l); isbal (MKT n l r) |] \
   2.149 +\ ==> isbal (MKT n (insert x l) r)";
   2.150 +by (cut_inst_tac [("x","x"),("t","l")] height_insert 1);
   2.151 + by (Asm_full_simp_tac 1); 
   2.152 +by (fast_tac (claset() addss simpset()) 1);
   2.153 +qed "isbal_insert_left";
   2.154 +
   2.155 +
   2.156 +Goal
   2.157 +"!!x. [| height (insert x r) ~= Suc(Suc(height l)); isbal (insert x r); isbal (MKT n l r) |] \
   2.158 +\ ==> isbal (MKT n l (insert x r))";
   2.159 +by (cut_inst_tac [("x","x"),("t","r")] height_insert 1);
   2.160 + by (Asm_full_simp_tac 1); 
   2.161 +by (fast_tac (claset() addss simpset()) 1);
   2.162 +qed "isbal_insert_right";
   2.163 +
   2.164 +(* insert-operation preserves isbal property *)
   2.165 +
   2.166 +Goal
   2.167 +"isbal t --> isbal(insert x t)";
   2.168 +by (induct_tac "t" 1);
   2.169 + by (Simp_tac 1);
   2.170 +by (case_tac "x=nat" 1);
   2.171 + by (Asm_simp_tac 1); 
   2.172 +by (case_tac "x<nat" 1);
   2.173 + by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);
   2.174 +  by (case_tac "bal (insert x tree1) = Right" 1);
   2.175 +   by (fast_tac (claset() addIs [isbal_lr_rot] addss (simpset() 
   2.176 +	addsimps [l_bal_def])) 1);  
   2.177 +  by (fast_tac (claset() addIs [isbal_r_rot] addss (simpset() 
   2.178 +	addsimps [l_bal_def])) 1);  
   2.179 + by (Clarify_tac 1);
   2.180 + by (forward_tac [isbal_insert_left] 1);
   2.181 +   by (Asm_full_simp_tac 1); 
   2.182 +  ba 1;
   2.183 + by (Asm_full_simp_tac 1); 
   2.184 +by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
   2.185 + by (case_tac "bal (insert x tree2) = Left" 1);
   2.186 +  by (fast_tac (claset() addIs [isbal_rl_rot] addss (simpset() 
   2.187 +	addsimps [r_bal_def])) 1);  
   2.188 + by (fast_tac (claset() addIs [isbal_l_rot] addss (simpset() 
   2.189 +	addsimps [r_bal_def])) 1);  
   2.190 +by (Clarify_tac 1);
   2.191 +by (forward_tac [isbal_insert_right] 1);
   2.192 +   by (Asm_full_simp_tac 1); 
   2.193 +  ba 1;
   2.194 + by (Asm_full_simp_tac 1); 
   2.195 +qed_spec_mp "isbal_insert";
   2.196 +
   2.197 +
   2.198 +(******************************    isin    **********************************)
   2.199 +
   2.200 +
   2.201 +(* rotations preserve isin property *)
   2.202 +
   2.203 +Goalw [bal_def]
   2.204 +"height l = Suc(Suc(height r)) --> bal l = Right  \
   2.205 +\ --> isin x (lr_rot (n, l, r)) = isin x (MKT n l r)";
   2.206 +by (case_tac "l" 1); 
   2.207 + by (Asm_simp_tac 1);
   2.208 +by (case_tac "tree2" 1);
   2.209 + by (Asm_simp_tac 1);
   2.210 +by (fast_tac (claset() addss simpset()) 1);
   2.211 +qed_spec_mp "isin_lr_rot";
   2.212 +
   2.213 +
   2.214 +Goalw [bal_def]
   2.215 +"height l = Suc(Suc(height r)) --> bal l ~= Right  \
   2.216 +\ --> isin x (r_rot (n, l, r)) = isin x (MKT n l r)";
   2.217 +by (case_tac "l" 1); 
   2.218 + by (Asm_simp_tac 1);
   2.219 +by (fast_tac (claset() addss simpset()) 1);
   2.220 +qed_spec_mp "isin_r_rot";
   2.221 +
   2.222 +
   2.223 +Goalw [bal_def]
   2.224 +"height r = Suc(Suc(height l)) --> bal r = Left  \
   2.225 +\ --> isin x (rl_rot (n, l, r)) = isin x (MKT n l r)";
   2.226 +by (case_tac "r" 1); 
   2.227 + by (Asm_simp_tac 1);
   2.228 +by (case_tac "tree1" 1);
   2.229 + by (asm_simp_tac (simpset() addsimps [max_def,le_def]) 1);
   2.230 +by (fast_tac (claset() addss simpset()) 1);
   2.231 +qed_spec_mp "isin_rl_rot";
   2.232 +
   2.233 +
   2.234 +Goalw [bal_def]
   2.235 +"height r = Suc(Suc(height l)) --> bal r ~= Left  \
   2.236 +\ --> isin x (l_rot (n, l, r)) = isin x (MKT n l r)";
   2.237 +by (case_tac "r" 1); 
   2.238 + by (Asm_simp_tac 1);
   2.239 +by (fast_tac (claset() addss simpset()) 1);
   2.240 +qed_spec_mp "isin_l_rot";
   2.241 +
   2.242 +
   2.243 +(* isin insert *)
   2.244 +
   2.245 +Goal
   2.246 +"isin y (insert x t) = (y=x | isin y t)";
   2.247 +by (induct_tac "t" 1);
   2.248 + by (Asm_simp_tac 1);
   2.249 +by(asm_simp_tac (simpset() addsimps [l_bal_def,isin_lr_rot,isin_r_rot,
   2.250 +	r_bal_def,isin_rl_rot,isin_l_rot]) 1);
   2.251 +by(Blast_tac 1);
   2.252 +qed "isin_insert";
   2.253 +
   2.254 +
   2.255 +(******************************    isord    **********************************)
   2.256 +
   2.257 +(* rotations preserve isord property *)
   2.258 +
   2.259 +Goalw [bal_def]
   2.260 +"height l = Suc(Suc(height r)) --> bal l = Right --> isord (MKT n l r) \
   2.261 +\ --> isord (lr_rot (n, l, r))";
   2.262 +by (case_tac "l" 1); 
   2.263 + by (Asm_simp_tac 1);
   2.264 +by (case_tac "tree2" 1);
   2.265 + by (Asm_simp_tac 1);
   2.266 +by (Asm_simp_tac 1);
   2.267 +by(blast_tac (claset() addIs [less_trans])1);
   2.268 +qed_spec_mp "isord_lr_rot";
   2.269 +
   2.270 +
   2.271 +Goalw [bal_def]
   2.272 +"height l = Suc(Suc(height r)) --> bal l ~= Right --> isord (MKT n l r) \
   2.273 +\ --> isord (r_rot (n, l, r))";
   2.274 +by (case_tac "l" 1); 
   2.275 + by (Asm_simp_tac 1);
   2.276 +by (auto_tac (claset() addIs [less_trans],simpset()));
   2.277 +qed_spec_mp "isord_r_rot";
   2.278 +
   2.279 +
   2.280 +Goalw [bal_def]
   2.281 +"height r = Suc(Suc(height l)) --> bal r = Left --> isord (MKT n l r) \
   2.282 +\ --> isord (rl_rot (n, l, r))";
   2.283 +by (case_tac "r" 1); 
   2.284 + by (Asm_simp_tac 1);
   2.285 +by (case_tac "tree1" 1);
   2.286 + by (asm_simp_tac (simpset() addsimps [le_def]) 1);
   2.287 +by (Asm_simp_tac 1);
   2.288 +by(blast_tac (claset() addIs [less_trans])1);
   2.289 +qed_spec_mp "isord_rl_rot";
   2.290 +
   2.291 +
   2.292 +Goalw [bal_def]
   2.293 +"height r = Suc(Suc(height l)) --> bal r ~= Left --> isord (MKT n l r)  \
   2.294 +\ --> isord (l_rot (n, l, r))";
   2.295 +by (case_tac "r" 1); 
   2.296 + by (Asm_simp_tac 1);
   2.297 +by (Asm_simp_tac 1);
   2.298 +by(blast_tac (claset() addIs [less_trans])1);
   2.299 +qed_spec_mp "isord_l_rot";
   2.300 +
   2.301 +(* insert operation presreves isord property *)
   2.302 +
   2.303 +Goal
   2.304 +"isord t --> isord(insert x t)";
   2.305 +by (induct_tac "t" 1);
   2.306 + by (Simp_tac 1);
   2.307 +by (cut_inst_tac [("m","x"),("n","nat")] less_linear 1);
   2.308 + by (fast_tac (claset() addss (simpset() addsimps [l_bal_def,isord_lr_rot,
   2.309 +	isord_r_rot,r_bal_def,isord_l_rot,isord_rl_rot,isin_insert])) 1);  
   2.310 +qed_spec_mp "isord_insert";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/AVL.thy	Fri May 05 12:51:33 2000 +0200
     3.3 @@ -0,0 +1,97 @@
     3.4 +(*  Title:      HOL/ex/AVL.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Cornelia Pusch and Tobias Nipkow
     3.7 +    Copyright   1998  TUM
     3.8 +
     3.9 +AVL trees: at the moment only insertion.
    3.10 +This version works exclusively with nat.
    3.11 +Balance check could be simplified by working with int:
    3.12 +"isbal (MKT n l r) = (abs(int(height l) - int(height r)) <= #1 &
    3.13 +                      isbal l & isbal r)"
    3.14 +*)
    3.15 +
    3.16 +AVL = Main +
    3.17 +
    3.18 +datatype tree = ET | MKT nat tree tree
    3.19 +
    3.20 +consts
    3.21 + height :: "tree => nat"
    3.22 + isin   :: "nat => tree => bool"
    3.23 + isord  :: "tree => bool"
    3.24 + isbal  :: "tree => bool"
    3.25 +
    3.26 +primrec
    3.27 +"height ET = 0"
    3.28 +"height (MKT n l r) = Suc(max (height l) (height r))"
    3.29 +
    3.30 +primrec
    3.31 +"isin k ET = False"
    3.32 +"isin k (MKT n l r) = (k=n | isin k l | isin k r)"
    3.33 +
    3.34 +primrec
    3.35 +"isord ET = True"
    3.36 +"isord (MKT n l r) = ((! n'. isin n' l --> n' < n) &
    3.37 +                      (! n'. isin n' r --> n < n') &
    3.38 +                      isord l & isord r)"
    3.39 +
    3.40 +primrec
    3.41 +"isbal ET = True"
    3.42 +"isbal (MKT n l r) = ((height l = height r | 
    3.43 +                       height l = Suc(height r) | 
    3.44 +                       height r = Suc(height l)) & 
    3.45 +                      isbal l & isbal r)"
    3.46 +
    3.47 +
    3.48 +datatype bal = Just | Left | Right
    3.49 +
    3.50 +constdefs
    3.51 + bal :: "tree => bal"
    3.52 +"bal t == case t of ET => Just
    3.53 + | (MKT n l r) => if height l = height r then Just
    3.54 +                  else if height l < height r then Right else Left"
    3.55 +
    3.56 +consts
    3.57 + r_rot,l_rot,lr_rot,rl_rot :: "nat * tree * tree => tree"
    3.58 +
    3.59 +recdef r_rot "{}"
    3.60 +"r_rot (n, MKT ln ll lr, r) = MKT ln ll (MKT n lr r)"
    3.61 +
    3.62 +recdef l_rot "{}"
    3.63 +"l_rot(n, l, MKT rn rl rr) = MKT rn (MKT n l rl) rr"
    3.64 +
    3.65 +recdef lr_rot "{}"
    3.66 +"lr_rot(n, MKT ln ll (MKT lrn lrl lrr), r) = MKT lrn (MKT ln ll lrl) (MKT n lrr r)"
    3.67 +
    3.68 +recdef rl_rot "{}"
    3.69 +"rl_rot(n, l, MKT rn (MKT rln rll rlr) rr) = MKT rln (MKT n l rll) (MKT rn rlr rr)"
    3.70 +
    3.71 +
    3.72 +constdefs 
    3.73 + l_bal :: "nat => tree => tree => tree"
    3.74 +"l_bal n l r == if bal l = Right 
    3.75 +                then lr_rot (n, l, r)
    3.76 +                else r_rot (n, l, r)"
    3.77 +
    3.78 + r_bal :: "nat => tree => tree => tree"
    3.79 +"r_bal n l r == if bal r = Left
    3.80 +                then rl_rot (n, l, r)
    3.81 +                else l_rot (n, l, r)"
    3.82 +
    3.83 +consts
    3.84 + insert :: "nat => tree => tree"
    3.85 +primrec
    3.86 +"insert x ET = MKT x ET ET"
    3.87 +"insert x (MKT n l r) = 
    3.88 +   (if x=n
    3.89 +    then MKT n l r
    3.90 +    else if x<n
    3.91 +         then let l' = insert x l
    3.92 +              in if height l' = Suc(Suc(height r))
    3.93 +                 then l_bal n l' r
    3.94 +                 else MKT n l' r
    3.95 +         else let r' = insert x r
    3.96 +              in if height r' = Suc(Suc(height l))
    3.97 +                 then r_bal n l r'
    3.98 +                 else MKT n l r')"
    3.99 +
   3.100 +end
     4.1 --- a/src/HOL/ex/ROOT.ML	Thu May 04 18:40:57 2000 +0200
     4.2 +++ b/src/HOL/ex/ROOT.ML	Fri May 05 12:51:33 2000 +0200
     4.3 @@ -23,6 +23,7 @@
     4.4  time_use     "mesontest.ML";
     4.5  time_use     "mesontest2.ML";
     4.6  time_use_thy "BT";
     4.7 +time_use_thy "AVL";
     4.8  time_use_thy "InSort";
     4.9  time_use_thy "Qsort";
    4.10  time_use_thy "Puzzle";