src/HOL/Data_Structures/RBT_Set.thy
author nipkow
Sat Jan 28 15:12:19 2017 +0100 (2017-01-28)
changeset 64960 8be78855ee7a
parent 64953 f9cfb10761ff
child 66087 6e0c330f4051
permissions -rw-r--r--
split balance into two, clearer etc
nipkow@64951
     1
(* Author: Tobias Nipkow *)
nipkow@61224
     2
nipkow@61224
     3
section \<open>Red-Black Tree Implementation of Sets\<close>
nipkow@61224
     4
nipkow@61224
     5
theory RBT_Set
nipkow@61224
     6
imports
nipkow@64950
     7
  Complex_Main
nipkow@61224
     8
  RBT
nipkow@61581
     9
  Cmp
nipkow@61224
    10
  Isin2
nipkow@61224
    11
begin
nipkow@61224
    12
nipkow@63411
    13
fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@61749
    14
"ins x Leaf = R Leaf x Leaf" |
nipkow@61749
    15
"ins x (B l a r) =
nipkow@61678
    16
  (case cmp x a of
nipkow@64960
    17
     LT \<Rightarrow> baliL (ins x l) a r |
nipkow@64960
    18
     GT \<Rightarrow> baliR l a (ins x r) |
nipkow@61678
    19
     EQ \<Rightarrow> B l a r)" |
nipkow@61749
    20
"ins x (R l a r) =
nipkow@61678
    21
  (case cmp x a of
nipkow@61749
    22
    LT \<Rightarrow> R (ins x l) a r |
nipkow@61749
    23
    GT \<Rightarrow> R l a (ins x r) |
nipkow@61678
    24
    EQ \<Rightarrow> R l a r)"
nipkow@61224
    25
nipkow@63411
    26
definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@61749
    27
"insert x t = paint Black (ins x t)"
nipkow@61749
    28
nipkow@63411
    29
fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
nipkow@63411
    30
and delL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
nipkow@63411
    31
and delR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
nipkow@61224
    32
where
nipkow@61749
    33
"del x Leaf = Leaf" |
nipkow@61749
    34
"del x (Node _ l a r) =
nipkow@61678
    35
  (case cmp x a of
nipkow@61749
    36
     LT \<Rightarrow> delL x l a r |
nipkow@61749
    37
     GT \<Rightarrow> delR x l a r |
nipkow@61678
    38
     EQ \<Rightarrow> combine l r)" |
nipkow@64960
    39
"delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" |
nipkow@61749
    40
"delL x l a r = R (del x l) a r" |
nipkow@64960
    41
"delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" | 
nipkow@61749
    42
"delR x l a r = R l a (del x r)"
nipkow@61749
    43
nipkow@63411
    44
definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
nipkow@61749
    45
"delete x t = paint Black (del x t)"
nipkow@61224
    46
nipkow@61224
    47
nipkow@61224
    48
subsection "Functional Correctness Proofs"
nipkow@61224
    49
nipkow@61749
    50
lemma inorder_paint: "inorder(paint c t) = inorder t"
nipkow@62526
    51
by(cases t) (auto)
nipkow@61749
    52
nipkow@64960
    53
lemma inorder_baliL:
nipkow@64960
    54
  "inorder(baliL l a r) = inorder l @ a # inorder r"
nipkow@64960
    55
by(cases "(l,a,r)" rule: baliL.cases) (auto)
nipkow@64960
    56
nipkow@64960
    57
lemma inorder_baliR:
nipkow@64960
    58
  "inorder(baliR l a r) = inorder l @ a # inorder r"
nipkow@64960
    59
by(cases "(l,a,r)" rule: baliR.cases) (auto)
nipkow@61224
    60
nipkow@61749
    61
lemma inorder_ins:
nipkow@61749
    62
  "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
nipkow@64960
    63
by(induction x t rule: ins.induct)
nipkow@64960
    64
  (auto simp: ins_list_simps inorder_baliL inorder_baliR)
nipkow@61749
    65
nipkow@61224
    66
lemma inorder_insert:
nipkow@61749
    67
  "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
nipkow@61749
    68
by (simp add: insert_def inorder_ins inorder_paint)
nipkow@61224
    69
nipkow@64960
    70
lemma inorder_baldL:
nipkow@64960
    71
  "inorder(baldL l a r) = inorder l @ a # inorder r"
nipkow@64960
    72
by(cases "(l,a,r)" rule: baldL.cases)
nipkow@64960
    73
  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
nipkow@61224
    74
nipkow@64960
    75
lemma inorder_baldR:
nipkow@64960
    76
  "inorder(baldR l a r) = inorder l @ a # inorder r"
nipkow@64960
    77
by(cases "(l,a,r)" rule: baldR.cases)
nipkow@64960
    78
  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
nipkow@61224
    79
nipkow@61224
    80
lemma inorder_combine:
nipkow@61224
    81
  "inorder(combine l r) = inorder l @ inorder r"
nipkow@61224
    82
by(induction l r rule: combine.induct)
nipkow@64960
    83
  (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
nipkow@61224
    84
nipkow@61749
    85
lemma inorder_del:
nipkow@61749
    86
 "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
nipkow@61749
    87
 "sorted(inorder l) \<Longrightarrow>  inorder(delL x l a r) =
nipkow@61678
    88
    del_list x (inorder l) @ a # inorder r"
nipkow@61749
    89
 "sorted(inorder r) \<Longrightarrow>  inorder(delR x l a r) =
nipkow@61224
    90
    inorder l @ a # del_list x (inorder r)"
nipkow@61749
    91
by(induction x t and x l a r and x l a r rule: del_delL_delR.induct)
nipkow@64960
    92
  (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
nipkow@61224
    93
nipkow@61749
    94
lemma inorder_delete:
nipkow@61749
    95
  "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
nipkow@61749
    96
by (auto simp: delete_def inorder_del inorder_paint)
nipkow@61749
    97
nipkow@61581
    98
nipkow@63411
    99
subsection \<open>Structural invariants\<close>
nipkow@61224
   100
nipkow@64952
   101
text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
nipkow@61754
   102
nipkow@61754
   103
fun color :: "'a rbt \<Rightarrow> color" where
nipkow@61754
   104
"color Leaf = Black" |
nipkow@61754
   105
"color (Node c _ _ _) = c"
nipkow@61754
   106
nipkow@61754
   107
fun bheight :: "'a rbt \<Rightarrow> nat" where
nipkow@61754
   108
"bheight Leaf = 0" |
nipkow@64951
   109
"bheight (Node c l x r) = (if c = Black then bheight l + 1 else bheight l)"
nipkow@61754
   110
nipkow@63411
   111
fun invc :: "'a rbt \<Rightarrow> bool" where
nipkow@63411
   112
"invc Leaf = True" |
nipkow@63411
   113
"invc (Node c l a r) =
nipkow@64947
   114
  (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
nipkow@61754
   115
nipkow@64953
   116
fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
nipkow@64953
   117
"invc2 Leaf = True" |
nipkow@64953
   118
"invc2 (Node c l a r) = (invc l \<and> invc r)"
nipkow@61754
   119
nipkow@63411
   120
fun invh :: "'a rbt \<Rightarrow> bool" where
nipkow@63411
   121
"invh Leaf = True" |
nipkow@63411
   122
"invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
nipkow@61754
   123
nipkow@64953
   124
lemma invc2I: "invc t \<Longrightarrow> invc2 t"
nipkow@61754
   125
by (cases t) simp+
nipkow@61754
   126
nipkow@61754
   127
definition rbt :: "'a rbt \<Rightarrow> bool" where
nipkow@63411
   128
"rbt t = (invc t \<and> invh t \<and> color t = Black)"
nipkow@61754
   129
nipkow@61754
   130
lemma color_paint_Black: "color (paint Black t) = Black"
nipkow@61754
   131
by (cases t) auto
nipkow@61754
   132
nipkow@61754
   133
theorem rbt_Leaf: "rbt Leaf"
nipkow@61754
   134
by (simp add: rbt_def)
nipkow@61754
   135
nipkow@64953
   136
lemma paint_invc2: "invc2 t \<Longrightarrow> invc2 (paint c t)"
nipkow@61754
   137
by (cases t) auto
nipkow@61754
   138
nipkow@64953
   139
lemma invc_paint_Black: "invc2 t \<Longrightarrow> invc (paint Black t)"
nipkow@61754
   140
by (cases t) auto
nipkow@61754
   141
nipkow@63411
   142
lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
nipkow@61754
   143
by (cases t) auto
nipkow@61754
   144
nipkow@64960
   145
lemma invc_baliL:
nipkow@64960
   146
  "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" 
nipkow@64960
   147
by (induct l a r rule: baliL.induct) auto
nipkow@64960
   148
nipkow@64960
   149
lemma invc_baliR:
nipkow@64960
   150
  "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 
nipkow@64960
   151
by (induct l a r rule: baliR.induct) auto
nipkow@64960
   152
nipkow@64960
   153
lemma bheight_baliL:
nipkow@64960
   154
  "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)"
nipkow@64960
   155
by (induct l a r rule: baliL.induct) auto
nipkow@61754
   156
nipkow@64960
   157
lemma bheight_baliR:
nipkow@64960
   158
  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
nipkow@64960
   159
by (induct l a r rule: baliR.induct) auto
nipkow@61754
   160
nipkow@64960
   161
lemma invh_baliL: 
nipkow@64960
   162
  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)"
nipkow@64960
   163
by (induct l a r rule: baliL.induct) auto
nipkow@64960
   164
nipkow@64960
   165
lemma invh_baliR: 
nipkow@64960
   166
  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
nipkow@64960
   167
by (induct l a r rule: baliR.induct) auto
nipkow@61754
   168
nipkow@61754
   169
nipkow@61754
   170
subsubsection \<open>Insertion\<close>
nipkow@61754
   171
nipkow@63411
   172
lemma invc_ins: assumes "invc t"
nipkow@64953
   173
  shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
nipkow@61754
   174
using assms
nipkow@64960
   175
by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
nipkow@61754
   176
nipkow@63411
   177
lemma invh_ins: assumes "invh t"
nipkow@63411
   178
  shows "invh (ins x t)" "bheight (ins x t) = bheight t"
nipkow@61754
   179
using assms
nipkow@64960
   180
by(induct x t rule: ins.induct)
nipkow@64960
   181
  (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
nipkow@61754
   182
nipkow@63411
   183
theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
nipkow@63411
   184
by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
nipkow@61754
   185
  rbt_def insert_def)
nipkow@61754
   186
nipkow@63411
   187
nipkow@63411
   188
subsubsection \<open>Deletion\<close>
nipkow@63411
   189
nipkow@63411
   190
lemma bheight_paint_Red:
nipkow@63411
   191
  "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
nipkow@61754
   192
by (cases t) auto
nipkow@61754
   193
nipkow@64960
   194
lemma baldL_invh_with_invc:
nipkow@64960
   195
  assumes "invh l" "invh r" "bheight l + 1 = bheight r" "invc r"
nipkow@64960
   196
  shows "bheight (baldL l a r) = bheight l + 1"  "invh (baldL l a r)"
nipkow@61754
   197
using assms 
nipkow@64960
   198
by (induct l a r rule: baldL.induct)
nipkow@64960
   199
   (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
nipkow@61754
   200
nipkow@64960
   201
lemma baldL_invh_app: 
nipkow@64960
   202
  assumes "invh l" "invh r" "bheight l + 1 = bheight r" "color r = Black"
nipkow@64960
   203
  shows "invh (baldL l a r)" 
nipkow@64960
   204
        "bheight (baldL l a r) = bheight r"
nipkow@61754
   205
using assms 
nipkow@64960
   206
by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) 
nipkow@61754
   207
nipkow@64960
   208
lemma baldL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
nipkow@64960
   209
by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
nipkow@61754
   210
nipkow@64960
   211
lemma baldL_invc2: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
nipkow@64960
   212
by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I)
nipkow@61754
   213
nipkow@64960
   214
lemma baldR_invh_with_invc:
nipkow@64960
   215
  assumes "invh l" "invh r" "bheight l = bheight r + 1" "invc l"
nipkow@64960
   216
  shows "invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
nipkow@61754
   217
using assms
nipkow@64960
   218
by(induct l a r rule: baldR.induct)
nipkow@64960
   219
  (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
nipkow@61754
   220
nipkow@64960
   221
lemma invc_baldR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (baldR a x b)"
nipkow@64960
   222
by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL)
nipkow@61754
   223
nipkow@64960
   224
lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l x r)"
nipkow@64960
   225
by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
nipkow@61754
   226
nipkow@63411
   227
lemma invh_combine:
nipkow@64960
   228
  assumes "invh l" "invh r" "bheight l = bheight r"
nipkow@64960
   229
  shows "bheight (combine l r) = bheight l" "invh (combine l r)"
nipkow@61754
   230
using assms 
nipkow@64960
   231
by (induct l r rule: combine.induct) 
nipkow@64960
   232
   (auto simp: baldL_invh_app split: tree.splits color.splits)
nipkow@61754
   233
nipkow@63411
   234
lemma invc_combine: 
nipkow@64960
   235
  assumes "invc l" "invc r"
nipkow@64960
   236
  shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)"
nipkow@64960
   237
         "invc2 (combine l r)"
nipkow@61754
   238
using assms 
nipkow@64960
   239
by (induct l r rule: combine.induct)
nipkow@64960
   240
   (auto simp: baldL_invc invc2I split: tree.splits color.splits)
nipkow@61754
   241
nipkow@61754
   242
nipkow@64960
   243
lemma assumes "invh l" "invc l"
nipkow@64960
   244
  shows del_invc_invh:
nipkow@64960
   245
   "invh (del x l) \<and>
nipkow@64960
   246
   (color l = Red \<and> bheight (del x l) = bheight l \<and> invc (del x l) \<or>
nipkow@64960
   247
    color l = Black \<and> bheight (del x l) = bheight l - 1 \<and> invc2 (del x l))"
nipkow@64960
   248
and  "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
nipkow@64960
   249
   invh (delL x l k r) \<and> 
nipkow@64960
   250
   bheight (delL x l k r) = bheight l \<and> 
nipkow@64960
   251
   (color l = Black \<and> color r = Black \<and> invc (delL x l k r) \<or> 
nipkow@64960
   252
    (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delL x l k r))"
nipkow@64960
   253
  and "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
nipkow@64960
   254
  invh (delR x l k r) \<and> 
nipkow@64960
   255
  bheight (delR x l k r) = bheight l \<and> 
nipkow@64960
   256
  (color l = Black \<and> color r = Black \<and> invc (delR x l k r) \<or> 
nipkow@64960
   257
   (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delR x l k r))"
nipkow@61754
   258
using assms
nipkow@64960
   259
proof (induct x l and x l k r and x l k r rule: del_delL_delR.induct)
nipkow@61754
   260
case (2 y c _ y')
nipkow@61754
   261
  have "y = y' \<or> y < y' \<or> y > y'" by auto
nipkow@61754
   262
  thus ?case proof (elim disjE)
nipkow@61754
   263
    assume "y = y'"
nipkow@63411
   264
    with 2 show ?thesis
nipkow@63411
   265
    by (cases c) (simp_all add: invh_combine invc_combine)
nipkow@61754
   266
  next
nipkow@61754
   267
    assume "y < y'"
nipkow@64953
   268
    with 2 show ?thesis by (cases c) (auto simp: invc2I)
nipkow@61754
   269
  next
nipkow@61754
   270
    assume "y' < y"
nipkow@64953
   271
    with 2 show ?thesis by (cases c) (auto simp: invc2I)
nipkow@61754
   272
  qed
nipkow@61754
   273
next
nipkow@64960
   274
  case (3 y l z ra y' bb)
nipkow@64960
   275
  thus ?case by (cases "color (Node Black l z ra) = Black \<and> color bb = Black") (simp add: baldL_invh_with_invc baldL_invc baldL_invc2)+
nipkow@61754
   276
next
nipkow@64960
   277
  case (5 y a y' l z ra)
nipkow@64960
   278
  thus ?case by (cases "color a = Black \<and> color (Node Black l z ra) = Black") (simp add: baldR_invh_with_invc invc_baldR invc2_baldR)+
nipkow@61754
   279
next
nipkow@63411
   280
  case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
nipkow@61754
   281
qed auto
nipkow@61754
   282
nipkow@63411
   283
theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
nipkow@64953
   284
by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
nipkow@63411
   285
nipkow@63411
   286
text \<open>Overall correctness:\<close>
nipkow@63411
   287
nipkow@63411
   288
interpretation Set_by_Ordered
nipkow@63411
   289
where empty = Leaf and isin = isin and insert = insert and delete = delete
nipkow@63411
   290
and inorder = inorder and inv = rbt
nipkow@63411
   291
proof (standard, goal_cases)
nipkow@63411
   292
  case 1 show ?case by simp
nipkow@63411
   293
next
nipkow@63411
   294
  case 2 thus ?case by(simp add: isin_set)
nipkow@63411
   295
next
nipkow@63411
   296
  case 3 thus ?case by(simp add: inorder_insert)
nipkow@63411
   297
next
nipkow@63411
   298
  case 4 thus ?case by(simp add: inorder_delete)
nipkow@63411
   299
next
nipkow@63411
   300
  case 5 thus ?case by (simp add: rbt_Leaf) 
nipkow@63411
   301
next
nipkow@63411
   302
  case 6 thus ?case by (simp add: rbt_insert) 
nipkow@63411
   303
next
nipkow@63411
   304
  case 7 thus ?case by (simp add: rbt_delete) 
nipkow@63411
   305
qed
nipkow@63411
   306
nipkow@63411
   307
nipkow@63411
   308
subsection \<open>Height-Size Relation\<close>
nipkow@63411
   309
nipkow@64950
   310
lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
nipkow@64950
   311
by (cases c) auto
nipkow@64950
   312
nipkow@64950
   313
lemma rbt_height_bheight_if_nat: "invc t \<Longrightarrow> invh t \<Longrightarrow>
nipkow@64950
   314
  height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
nipkow@64950
   315
by(induction t) (auto split: if_split_asm)
nipkow@64950
   316
nipkow@64950
   317
lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
nipkow@64950
   318
  (if color t = Black then height t / 2 else (height t - 1) / 2) \<le> bheight t"
nipkow@64950
   319
by(induction t) (auto split: if_split_asm)
nipkow@64950
   320
nipkow@64950
   321
lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
nipkow@64950
   322
by(auto simp: rbt_def dest: rbt_height_bheight_if)
nipkow@64950
   323
nipkow@64950
   324
lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
nipkow@64950
   325
by (induction t) auto
nipkow@64950
   326
nipkow@64950
   327
lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
nipkow@64950
   328
proof -
nipkow@64950
   329
  have "2 powr (height t / 2) \<le> 2 powr bheight t"
nipkow@64950
   330
    using rbt_height_bheight[OF assms] by (simp)
nipkow@64950
   331
  also have "\<dots> \<le> size1 t" using assms
nipkow@64950
   332
    by (simp add: powr_realpow bheight_size_bound rbt_def)
nipkow@64950
   333
  finally have "2 powr (height t / 2) \<le> size1 t" .
nipkow@64950
   334
  hence "height t / 2 \<le> log 2 (size1 t)"
nipkow@64950
   335
    by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
nipkow@64950
   336
  thus ?thesis by simp
nipkow@64950
   337
qed
nipkow@64950
   338
nipkow@61224
   339
end