src/HOL/ex/AVL.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8797 b55e2354d71e
child 12486 0ed8bdd883e0
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8797
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/ex/AVL.ML
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
     2
    ID:         $Id$
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
     3
    Author:     Cornelia Pusch and Tobias Nipkow
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
     4
    Copyright   1998  TUM
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
     5
*)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
     6
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
     7
(******************************    isbal    **********************************)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
     8
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
     9
Addsimps[Let_def];
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    10
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    11
(* rotations preserve isbal property *)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    12
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    13
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    14
"height l = Suc(Suc(height r)) --> bal l = Right --> isbal l --> isbal r \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    15
\ --> isbal (lr_rot (n, l, r))";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    16
by (case_tac "l" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    17
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    18
by (case_tac "tree2" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    19
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    20
by (asm_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    21
by (arith_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    22
qed_spec_mp "isbal_lr_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    23
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    24
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    25
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    26
"height l = Suc(Suc(height r)) --> bal l ~= Right --> isbal l --> isbal r \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    27
\ --> isbal (r_rot (n, l, r))";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    28
by (case_tac "l" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    29
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    30
by (asm_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    31
qed_spec_mp "isbal_r_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    32
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    33
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    34
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    35
"height r = Suc(Suc(height l)) --> bal r = Left --> isbal l --> isbal r \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    36
\ --> isbal (rl_rot (n, l, r))";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    37
by (case_tac "r" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    38
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    39
by (case_tac "tree1" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    40
 by (asm_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    41
by (asm_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    42
by (arith_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    43
qed_spec_mp "isbal_rl_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    44
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    45
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    46
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    47
"height r = Suc(Suc(height l)) --> bal r ~= Left --> isbal l --> isbal r \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    48
\ --> isbal (l_rot (n, l, r))";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    49
by (case_tac "r" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    50
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    51
by (asm_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    52
qed_spec_mp "isbal_l_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    53
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    54
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    55
(* lemmas about height after rotation *)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    56
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    57
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    58
"bal l = Right --> height l = Suc(Suc(height r))   \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    59
\ -->     Suc(height (lr_rot (n, l, r)))  = height (MKT n l r) ";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    60
by (case_tac "l" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    61
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    62
by (case_tac "tree2" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    63
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    64
by (asm_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    65
qed_spec_mp "height_lr_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    66
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    67
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    68
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    69
"height l = Suc(Suc(height r)) --> bal l ~= Right \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    70
\ --> Suc(height (r_rot (n, l, r))) = height (MKT n l r) | \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    71
\         height (r_rot (n, l, r))  = height (MKT n l r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    72
by (case_tac "l" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    73
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    74
by (asm_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    75
qed_spec_mp "height_r_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    76
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    77
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    78
Goalw [l_bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    79
"height l = Suc(Suc(height r))  \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    80
\ --> Suc(height (l_bal n l r)) = height (MKT n l r) | \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    81
\         height (l_bal n l r)  = height (MKT n l r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    82
by (case_tac "bal l = Right" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    83
 by (fast_tac (claset() addDs [height_lr_rot] addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    84
by (fast_tac (claset() addDs [height_r_rot] addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    85
qed_spec_mp "height_l_bal";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    86
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    87
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    88
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    89
"height r = Suc(Suc(height l)) --> bal r = Left \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    90
\ -->     Suc(height (rl_rot (n, l, r)))  = height (MKT n l r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    91
by (case_tac "r" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    92
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    93
by (case_tac "tree1" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    94
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    95
by (asm_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    96
by (arith_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    97
qed_spec_mp "height_rl_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    98
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
    99
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   100
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   101
"height r = Suc(Suc(height l)) --> bal r ~= Left \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   102
\ --> Suc(height (l_rot (n, l, r))) = height (MKT n l r) | \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   103
\         height (l_rot (n, l, r))  = height (MKT n l r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   104
by (case_tac "r" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   105
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   106
by (asm_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   107
qed_spec_mp "height_l_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   108
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   109
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   110
Goalw [r_bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   111
"height r = Suc(Suc(height l))  \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   112
\ --> Suc(height (r_bal n l r)) = height (MKT n l r) | \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   113
\         height (r_bal n l r)  = height (MKT n l r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   114
by (case_tac "bal r = Left" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   115
 by (fast_tac (claset() addDs [height_rl_rot] addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   116
by (fast_tac (claset() addDs [height_l_rot] addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   117
qed_spec_mp "height_r_bal";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   118
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   119
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   120
(* lemma about height after insert *)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   121
Goal
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   122
"isbal t  \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   123
\ --> height (insert x t) = height t | height (insert x t) = Suc(height t)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   124
by (induct_tac "t" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   125
 by (Simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   126
by (case_tac "x=nat" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   127
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   128
by (case_tac "x<nat" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   129
 by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   130
  by (forw_inst_tac [("n","nat")]  height_l_bal 1);  
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   131
  by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   132
  by(fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   133
 by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   134
 by(fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   135
by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   136
 by (forw_inst_tac [("n","nat")]  height_r_bal 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   137
 by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   138
 by(fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   139
by (asm_full_simp_tac (simpset() addsimps [max_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   140
by(fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   141
qed_spec_mp "height_insert";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   142
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   143
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   144
Goal
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   145
"!!x. [| height (insert x l) ~= Suc(Suc(height r)); isbal (insert x l); isbal (MKT n l r) |] \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   146
\ ==> isbal (MKT n (insert x l) r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   147
by (cut_inst_tac [("x","x"),("t","l")] height_insert 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   148
 by (Asm_full_simp_tac 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   149
by (fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   150
qed "isbal_insert_left";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   151
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   152
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   153
Goal
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   154
"!!x. [| height (insert x r) ~= Suc(Suc(height l)); isbal (insert x r); isbal (MKT n l r) |] \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   155
\ ==> isbal (MKT n l (insert x r))";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   156
by (cut_inst_tac [("x","x"),("t","r")] height_insert 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   157
 by (Asm_full_simp_tac 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   158
by (fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   159
qed "isbal_insert_right";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   160
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   161
(* insert-operation preserves isbal property *)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   162
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   163
Goal
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   164
"isbal t --> isbal(insert x t)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   165
by (induct_tac "t" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   166
 by (Simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   167
by (case_tac "x=nat" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   168
 by (Asm_simp_tac 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   169
by (case_tac "x<nat" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   170
 by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   171
  by (case_tac "bal (insert x tree1) = Right" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   172
   by (fast_tac (claset() addIs [isbal_lr_rot] addss (simpset() 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   173
	addsimps [l_bal_def])) 1);  
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   174
  by (fast_tac (claset() addIs [isbal_r_rot] addss (simpset() 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   175
	addsimps [l_bal_def])) 1);  
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   176
 by (Clarify_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   177
 by (forward_tac [isbal_insert_left] 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   178
   by (Asm_full_simp_tac 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   179
  ba 1;
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   180
 by (Asm_full_simp_tac 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   181
by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   182
 by (case_tac "bal (insert x tree2) = Left" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   183
  by (fast_tac (claset() addIs [isbal_rl_rot] addss (simpset() 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   184
	addsimps [r_bal_def])) 1);  
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   185
 by (fast_tac (claset() addIs [isbal_l_rot] addss (simpset() 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   186
	addsimps [r_bal_def])) 1);  
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   187
by (Clarify_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   188
by (forward_tac [isbal_insert_right] 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   189
   by (Asm_full_simp_tac 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   190
  ba 1;
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   191
 by (Asm_full_simp_tac 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   192
qed_spec_mp "isbal_insert";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   193
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   194
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   195
(******************************    isin    **********************************)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   196
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   197
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   198
(* rotations preserve isin property *)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   199
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   200
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   201
"height l = Suc(Suc(height r)) --> bal l = Right  \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   202
\ --> isin x (lr_rot (n, l, r)) = isin x (MKT n l r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   203
by (case_tac "l" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   204
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   205
by (case_tac "tree2" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   206
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   207
by (fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   208
qed_spec_mp "isin_lr_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   209
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   210
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   211
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   212
"height l = Suc(Suc(height r)) --> bal l ~= Right  \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   213
\ --> isin x (r_rot (n, l, r)) = isin x (MKT n l r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   214
by (case_tac "l" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   215
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   216
by (fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   217
qed_spec_mp "isin_r_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   218
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   219
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   220
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   221
"height r = Suc(Suc(height l)) --> bal r = Left  \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   222
\ --> isin x (rl_rot (n, l, r)) = isin x (MKT n l r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   223
by (case_tac "r" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   224
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   225
by (case_tac "tree1" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   226
 by (asm_simp_tac (simpset() addsimps [max_def,le_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   227
by (fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   228
qed_spec_mp "isin_rl_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   229
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   230
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   231
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   232
"height r = Suc(Suc(height l)) --> bal r ~= Left  \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   233
\ --> isin x (l_rot (n, l, r)) = isin x (MKT n l r)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   234
by (case_tac "r" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   235
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   236
by (fast_tac (claset() addss simpset()) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   237
qed_spec_mp "isin_l_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   238
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   239
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   240
(* isin insert *)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   241
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   242
Goal
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   243
"isin y (insert x t) = (y=x | isin y t)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   244
by (induct_tac "t" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   245
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   246
by(asm_simp_tac (simpset() addsimps [l_bal_def,isin_lr_rot,isin_r_rot,
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   247
	r_bal_def,isin_rl_rot,isin_l_rot]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   248
by(Blast_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   249
qed "isin_insert";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   250
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   251
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   252
(******************************    isord    **********************************)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   253
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   254
(* rotations preserve isord property *)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   255
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   256
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   257
"height l = Suc(Suc(height r)) --> bal l = Right --> isord (MKT n l r) \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   258
\ --> isord (lr_rot (n, l, r))";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   259
by (case_tac "l" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   260
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   261
by (case_tac "tree2" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   262
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   263
by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   264
by(blast_tac (claset() addIs [less_trans])1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   265
qed_spec_mp "isord_lr_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   266
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   267
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   268
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   269
"height l = Suc(Suc(height r)) --> bal l ~= Right --> isord (MKT n l r) \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   270
\ --> isord (r_rot (n, l, r))";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   271
by (case_tac "l" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   272
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   273
by (auto_tac (claset() addIs [less_trans],simpset()));
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   274
qed_spec_mp "isord_r_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   275
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   276
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   277
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   278
"height r = Suc(Suc(height l)) --> bal r = Left --> isord (MKT n l r) \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   279
\ --> isord (rl_rot (n, l, r))";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   280
by (case_tac "r" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   281
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   282
by (case_tac "tree1" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   283
 by (asm_simp_tac (simpset() addsimps [le_def]) 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   284
by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   285
by(blast_tac (claset() addIs [less_trans])1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   286
qed_spec_mp "isord_rl_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   287
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   288
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   289
Goalw [bal_def]
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   290
"height r = Suc(Suc(height l)) --> bal r ~= Left --> isord (MKT n l r)  \
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   291
\ --> isord (l_rot (n, l, r))";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   292
by (case_tac "r" 1); 
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   293
 by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   294
by (Asm_simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   295
by(blast_tac (claset() addIs [less_trans])1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   296
qed_spec_mp "isord_l_rot";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   297
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   298
(* insert operation presreves isord property *)
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   299
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   300
Goal
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   301
"isord t --> isord(insert x t)";
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   302
by (induct_tac "t" 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   303
 by (Simp_tac 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   304
by (cut_inst_tac [("m","x"),("n","nat")] less_linear 1);
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   305
 by (fast_tac (claset() addss (simpset() addsimps [l_bal_def,isord_lr_rot,
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   306
	isord_r_rot,r_bal_def,isord_l_rot,isord_rl_rot,isin_insert])) 1);  
b55e2354d71e Added AVL
nipkow
parents:
diff changeset
   307
qed_spec_mp "isord_insert";