src/HOL/ex/AVL.ML
author nipkow
Fri May 05 12:51:33 2000 +0200 (2000-05-05)
changeset 8797 b55e2354d71e
child 12486 0ed8bdd883e0
permissions -rw-r--r--
Added AVL
     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 (* insert-operation 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";