-
Notifications
You must be signed in to change notification settings - Fork 0
/
RBT_set_opt.thy
1265 lines (1084 loc) · 58.3 KB
/
RBT_set_opt.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
theory RBT_set_opt
imports "HOL-Library.RBT_Impl" "Containers.Set_Impl"
begin
definition is_empty :: "('a, 'b) rbt \<Rightarrow> bool" where
"is_empty t \<longleftrightarrow> (case t of RBT_Impl.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
lemma is_empty_prop[simp]: "is_empty t \<longleftrightarrow> t = RBT_Impl.Empty"
by (auto simp: is_empty_def split: RBT_Impl.rbt.splits)
definition small_rbt :: "('a, 'b) rbt \<Rightarrow> bool" where
"small_rbt t \<longleftrightarrow> bheight t < 6"
definition flip_rbt :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> bool" where
"flip_rbt t1 t2 \<longleftrightarrow> bheight t2 < bheight t1"
abbreviation MR where "MR l a b r \<equiv> Branch RBT_Impl.R l a b r"
abbreviation MB where "MB l a b r \<equiv> Branch RBT_Impl.B l a b r"
fun baliL :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"baliL (MR (MR t1 a b t2) a' b' t3) a'' b'' t4 = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)"
| "baliL (MR t1 a b (MR t2 a' b' t3)) a'' b'' t4 = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)"
| "baliL t1 a b t2 = MB t1 a b t2"
fun baliR :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"baliR t1 a b (MR t2 a' b' (MR t3 a'' b'' t4)) = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)"
| "baliR t1 a b (MR (MR t2 a' b' t3) a'' b'' t4) = MR (MB t1 a b t2) a' b' (MB t3 a'' b'' t4)"
| "baliR t1 a b t2 = MB t1 a b t2"
fun paint :: "color \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"paint c RBT_Impl.Empty = RBT_Impl.Empty"
| "paint c (RBT_Impl.Branch _ l a b r) = RBT_Impl.Branch c l a b r"
fun baldL :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"baldL (MR t1 a b t2) a' b' t3 = MR (MB t1 a b t2) a' b' t3"
| "baldL t1 a b (MB t2 a' b' t3) = baliR t1 a b (MR t2 a' b' t3)"
| "baldL t1 a b (MR (MB t2 a' b' t3) a'' b'' t4) =
MR (MB t1 a b t2) a' b' (baliR t3 a'' b'' (paint RBT_Impl.R t4))"
| "baldL t1 a b t2 = MR t1 a b t2"
fun baldR :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"baldR t1 a b (MR t2 a' b' t3) = MR t1 a b (MB t2 a' b' t3)"
| "baldR (MB t1 a b t2) a' b' t3 = baliL (MR t1 a b t2) a' b' t3"
| "baldR (MR t1 a b (MB t2 a' b' t3)) a'' b'' t4 =
MR (baliL (paint RBT_Impl.R t1) a b t2) a' b' (MB t3 a'' b'' t4)"
| "baldR t1 a b t2 = MR t1 a b t2"
fun app :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"app RBT_Impl.Empty t = t"
| "app t RBT_Impl.Empty = t"
| "app (MR t1 a b t2) (MR t3 a'' b'' t4) = (case app t2 t3 of
MR u2 a' b' u3 \<Rightarrow> (MR (MR t1 a b u2) a' b' (MR u3 a'' b'' t4))
| t23 \<Rightarrow> MR t1 a b (MR t23 a'' b'' t4))"
| "app (MB t1 a b t2) (MB t3 a'' b'' t4) = (case app t2 t3 of
MR u2 a' b' u3 \<Rightarrow> MR (MB t1 a b u2) a' b' (MB u3 a'' b'' t4)
| t23 \<Rightarrow> baldL t1 a b (MB t23 a'' b'' t4))"
| "app t1 (MR t2 a b t3) = MR (app t1 t2) a b t3"
| "app (MR t1 a b t2) t3 = MR t1 a b (app t2 t3)"
fun rbt_joinL :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"rbt_joinL l a b r = (if bheight l \<ge> bheight r then MR l a b r
else case r of MB l' a' b' r' \<Rightarrow> baliL (rbt_joinL l a b l') a' b' r'
| MR l' a' b' r' \<Rightarrow> MR (rbt_joinL l a b l') a' b' r')"
fun rbt_joinR :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"rbt_joinR l a b r = (if bheight l \<le> bheight r then MR l a b r
else case l of MB l' a' b' r' \<Rightarrow> baliR l' a' b' (rbt_joinR r' a b r)
| MR l' a' b' r' \<Rightarrow> MR l' a' b' (rbt_joinR r' a b r))"
definition rbt_join :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"rbt_join l a b r = (if bheight l > bheight r
then paint RBT_Impl.B (rbt_joinR l a b r)
else if bheight l < bheight r
then paint RBT_Impl.B (rbt_joinL l a b r)
else MB l a b r)"
declare rbt_joinL.simps[simp del]
declare rbt_joinR.simps[simp del]
lemma [simp]: "size (paint c t) = size t"
by (cases t) auto
lemma size_baliL[simp]: "size (baliL t1 a b t2) = Suc (size t1 + size t2)"
by (induction t1 a b t2 rule: baliL.induct) auto
lemma size_baliR[simp]: "size (baliR t1 a b t2) = Suc (size t1 + size t2)"
by (induction t1 a b t2 rule: baliR.induct) auto
lemma size_baldL[simp]: "size (baldL t1 a b t2) = Suc (size t1 + size t2)"
by (induction t1 a b t2 rule: baldL.induct) auto
lemma size_baldR[simp]: "size (baldR t1 a b t2) = Suc (size t1 + size t2)"
by (induction t1 a b t2 rule: baldR.induct) auto
lemma size_app[simp]: "size (app t1 t2) = size t1 + size t2"
by (induction t1 t2 rule: app.induct)
(auto split: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
lemma size_rbt_joinL[simp]: "size (rbt_joinL t1 a b t2) = Suc (size t1 + size t2)"
by (induction t1 a b t2 rule: rbt_joinL.induct)
(auto simp: rbt_joinL.simps split: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
lemma size_rbt_joinR[simp]: "size (rbt_joinR t1 a b t2) = Suc (size t1 + size t2)"
by (induction t1 a b t2 rule: rbt_joinR.induct)
(auto simp: rbt_joinR.simps split: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
lemma size_rbt_join[simp]: "size (rbt_join t1 a b t2) = Suc (size t1 + size t2)"
by (auto simp: rbt_join_def)
definition "rbt t \<longleftrightarrow> inv1 t \<and> inv2 t"
lemma rbt_Node: "\<lbrakk> rbt (RBT_Impl.Branch c l a b r) \<rbrakk> \<Longrightarrow> rbt l \<and> rbt r"
by (auto simp: rbt_def)
lemma color_of_paint_B: "color_of (paint RBT_Impl.B t) = RBT_Impl.B"
by (cases t) auto
lemma paint2: "paint c2 (paint c1 t) = paint c2 t"
by (cases t) auto
lemma inv1_paint_B: "inv1l t \<Longrightarrow> inv1 (paint RBT_Impl.B t)"
by (cases t) auto
lemma inv2_paint: "inv2 t \<Longrightarrow> inv2 (paint c t)"
by (cases t) auto
lemma inv1_baliL:
"\<lbrakk>inv1l l; inv1 r\<rbrakk> \<Longrightarrow> inv1 (baliL l a b r)"
by (induct l a b r rule: baliL.induct) auto
lemma inv1_baliR:
"\<lbrakk>inv1 l; inv1l r\<rbrakk> \<Longrightarrow> inv1 (baliR l a b r)"
by (induct l a b r rule: baliR.induct) auto
lemma bheight_baliL:
"bheight l = bheight r \<Longrightarrow> bheight (baliL l a b r) = Suc (bheight l)"
by (induct l a b r rule: baliL.induct) auto
lemma bheight_baliR:
"bheight l = bheight r \<Longrightarrow> bheight (baliR l a b r) = Suc (bheight l)"
by (induct l a b r rule: baliR.induct) auto
lemma inv2_baliL:
"\<lbrakk> inv2 l; inv2 r; bheight l = bheight r \<rbrakk> \<Longrightarrow> inv2 (baliL l a b r)"
by (induct l a b r rule: baliL.induct) auto
lemma inv2_baliR:
"\<lbrakk> inv2 l; inv2 r; bheight l = bheight r \<rbrakk> \<Longrightarrow> inv2 (baliR l a b r)"
by (induct l a b r rule: baliR.induct) auto
lemma inv_baliR: "\<lbrakk> inv2 l; inv2 r; inv1 l; inv1l r; bheight l = bheight r \<rbrakk>
\<Longrightarrow> inv1 (baliR l a b r) \<and> inv2 (baliR l a b r) \<and> bheight (baliR l a b r) = Suc (bheight l)"
by (induct l a b r rule: baliR.induct) auto
lemma inv_baliL: "\<lbrakk> inv2 l; inv2 r; inv1l l; inv1 r; bheight l = bheight r \<rbrakk>
\<Longrightarrow> inv1 (baliL l a b r) \<and> inv2 (baliL l a b r) \<and> bheight (baliL l a b r) = Suc (bheight l)"
by (induct l a b r rule: baliL.induct) auto
lemma bheight_paint_R:
"color_of t = RBT_Impl.B \<Longrightarrow> bheight (paint RBT_Impl.R t) = bheight t - 1"
by (cases t) auto
lemma inv2_baldL_inv1:
"\<lbrakk> inv2 l; inv2 r; bheight l + 1 = bheight r; inv1 r \<rbrakk>
\<Longrightarrow> inv2 (baldL l a b r) \<and> bheight (baldL l a b r) = bheight r"
by (induct l a b r rule: baldL.induct)
(auto simp: inv2_baliR inv2_paint bheight_baliR bheight_paint_R)
lemma inv2_baldL_B:
"\<lbrakk> inv2 l; inv2 r; bheight l + 1 = bheight r; color_of r = RBT_Impl.B \<rbrakk>
\<Longrightarrow> inv2 (baldL l a b r) \<and> bheight (baldL l a b r) = bheight r"
by (induct l a b r rule: baldL.induct) (auto simp add: inv2_baliR bheight_baliR)
lemma inv1_baldL: "\<lbrakk>inv1l l; inv1 r; color_of r = RBT_Impl.B\<rbrakk> \<Longrightarrow> inv1 (baldL l a b r)"
by (induct l a b r rule: baldL.induct) (simp_all add: inv1_baliR)
lemma inv1lI: "inv1 t \<Longrightarrow> inv1l t"
by (cases t) auto
lemma neq_Black[simp]: "(c \<noteq> RBT_Impl.B) = (c = RBT_Impl.R)"
by (cases c) auto
lemma [simp]: "inv1 t \<Longrightarrow> inv1l (paint c t)"
by (cases t) auto
lemma inv1l_baldL: "\<lbrakk> inv1l l; inv1 r \<rbrakk> \<Longrightarrow> inv1l (baldL l a b r)"
by (induct l a b r rule: baldL.induct) (auto simp: inv1_baliR paint2)
lemma inv2_baldR_inv1:
"\<lbrakk> inv2 l; inv2 r; bheight l = bheight r + 1; inv1 l \<rbrakk>
\<Longrightarrow> inv2 (baldR l a b r) \<and> bheight (baldR l a b r) = bheight l"
by (induct l a b r rule: baldR.induct)
(auto simp: inv2_baliL bheight_baliL inv2_paint bheight_paint_R)
lemma inv1_baldR: "\<lbrakk>inv1 l; inv1l r; color_of l = RBT_Impl.B\<rbrakk> \<Longrightarrow> inv1 (baldR l a b r)"
by (induct l a b r rule: baldR.induct) (simp_all add: inv1_baliL)
lemma inv1l_baldR: "\<lbrakk> inv1 l; inv1l r \<rbrakk> \<Longrightarrow>inv1l (baldR l a b r)"
by (induct l a b r rule: baldR.induct) (auto simp: inv1_baliL paint2)
lemma inv2_app:
"\<lbrakk> inv2 l; inv2 r; bheight l = bheight r \<rbrakk>
\<Longrightarrow> inv2 (app l r) \<and> bheight (app l r) = bheight l"
by (induct l r rule: app.induct)
(auto simp: inv2_baldL_B split: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
lemma inv1_app:
"\<lbrakk> inv1 l; inv1 r \<rbrakk> \<Longrightarrow>
(color_of l = RBT_Impl.B \<and> color_of r = RBT_Impl.B \<longrightarrow> inv1 (app l r)) \<and> inv1l (app l r)"
by (induct l r rule: app.induct)
(auto simp: inv1_baldL split: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
lemma inv_baldL:
"\<lbrakk> inv2 l; inv2 r; bheight l + 1 = bheight r; inv1l l; inv1 r \<rbrakk>
\<Longrightarrow> inv2 (baldL l a b r) \<and> bheight (baldL l a b r) = bheight r
\<and> inv1l (baldL l a b r) \<and> (color_of r = RBT_Impl.B \<longrightarrow> inv1 (baldL l a b r))"
by (induct l a b r rule: baldL.induct)
(auto simp: inv_baliR inv2_paint bheight_baliR bheight_paint_R paint2)
lemma inv_baldR:
"\<lbrakk> inv2 l; inv2 r; bheight l = bheight r + 1; inv1 l; inv1l r \<rbrakk>
\<Longrightarrow> inv2 (baldR l a b r) \<and> bheight (baldR l a b r) = bheight l
\<and> inv1l (baldR l a b r) \<and> (color_of l = RBT_Impl.B \<longrightarrow> inv1 (baldR l a b r))"
by (induct l a b r rule: baldR.induct)
(auto simp: inv_baliL inv2_paint bheight_baliL bheight_paint_R paint2)
lemma inv_app:
"\<lbrakk> inv2 l; inv2 r; bheight l = bheight r; inv1 l; inv1 r \<rbrakk>
\<Longrightarrow> inv2 (app l r) \<and> bheight (app l r) = bheight l
\<and> inv1l (app l r) \<and> (color_of l = RBT_Impl.B \<and> color_of r = RBT_Impl.B \<longrightarrow> inv1 (app l r))"
by (induct l r rule: app.induct)
(auto simp: inv2_baldL_B inv_baldL
split: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
lemma neq_LeafD: "t \<noteq> RBT_Impl.Empty \<Longrightarrow> \<exists>l x c r. t = RBT_Impl.Branch c l x () r"
by (cases t) auto
lemma inv1l_rbt_joinL:
"\<lbrakk> inv1 l; inv1 r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow>
inv1l (rbt_joinL l a b r)
\<and> (bheight l \<noteq> bheight r \<and> color_of r = RBT_Impl.B \<longrightarrow> inv1(rbt_joinL l a b r))"
proof (induct l a b r rule: rbt_joinL.induct)
case (1 l a b r) thus ?case
by (auto simp: inv1_baliL rbt_joinL.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma inv1l_rbt_joinR:
"\<lbrakk> inv1 l; inv2 l; inv1 r; inv2 r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow>
inv1l (rbt_joinR l a b r)
\<and> (bheight l \<noteq> bheight r \<and> color_of l = RBT_Impl.B \<longrightarrow> inv1(rbt_joinR l a b r))"
proof (induct l a b r rule: rbt_joinR.induct)
case (1 l a b r) thus ?case
by (fastforce simp: inv1_baliR rbt_joinR.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma bheight_rbt_joinL:
"\<lbrakk> inv2 l; inv2 r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> bheight (rbt_joinL l a b r) = bheight r"
proof (induct l a b r rule: rbt_joinL.induct)
case (1 l a b r) thus ?case
by (auto simp: bheight_baliL rbt_joinL.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma inv2_rbt_joinL:
"\<lbrakk> inv2 l; inv2 r; bheight l \<le> bheight r \<rbrakk> \<Longrightarrow> inv2 (rbt_joinL l a b r)"
proof (induct l a b r rule: rbt_joinL.induct)
case (1 l a b r) thus ?case
by (auto simp: inv2_baliL bheight_rbt_joinL rbt_joinL.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma bheight_rbt_joinR:
"\<lbrakk> inv2 l; inv2 r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (rbt_joinR l a b r) = bheight l"
proof (induct l a b r rule: rbt_joinR.induct)
case (1 l a b r) thus ?case
by (fastforce simp: bheight_baliR rbt_joinR.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma inv2_rbt_joinR:
"\<lbrakk> inv2 l; inv2 r; bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> inv2 (rbt_joinR l a b r)"
proof (induct l a b r rule: rbt_joinR.induct)
case (1 l a b r) thus ?case
by (fastforce simp: inv2_baliR bheight_rbt_joinR rbt_joinR.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma bheight_paint_Black: "bheight (paint RBT_Impl.B t) \<le> bheight t + 1"
by (cases t) auto
lemma keys_paint: "RBT_Impl.keys (paint c t) = RBT_Impl.keys t"
by (cases t) auto
lemma keys_baliL:
"RBT_Impl.keys (baliL l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r"
by (cases "(l,a,b,r)" rule: baliL.cases) auto
lemma keys_baliR:
"RBT_Impl.keys (baliR l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r"
by (cases "(l,a,b,r)" rule: baliR.cases) auto
lemma keys_baldL:
"RBT_Impl.keys (baldL l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r"
by (cases "(l,a,b,r)" rule: baldL.cases)
(auto simp: keys_baliL keys_baliR keys_paint)
lemma keys_baldR:
"RBT_Impl.keys (baldR l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r"
by (cases "(l,a,b,r)" rule: baldR.cases)
(auto simp: keys_baliL keys_baliR keys_paint)
lemma keys_app:
"RBT_Impl.keys (app l r) = RBT_Impl.keys l @ RBT_Impl.keys r"
by (induction l r rule: app.induct)
(auto simp: keys_baldL keys_baldR
split: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
lemma keys_rbt_joinL: "bheight l \<le> bheight r \<Longrightarrow>
RBT_Impl.keys (rbt_joinL l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r"
proof (induction l a b r rule: rbt_joinL.induct)
case (1 l a b r)
thus ?case
by (auto simp: keys_baliL rbt_joinL.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma keys_rbt_joinR:
"RBT_Impl.keys (rbt_joinR l a b r) = RBT_Impl.keys l @ a # RBT_Impl.keys r"
proof (induction l a b r rule: rbt_joinR.induct)
case (1 l a b r)
thus ?case
by (force simp: keys_baliR rbt_joinR.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma set_baliL:
"set (RBT_Impl.keys (baliL l a b r)) = set (RBT_Impl.keys l) \<union> {a} \<union> set (RBT_Impl.keys r)"
by (cases "(l,a,b,r)" rule: baliL.cases) auto
lemma set_rbt_joinL:
"bheight l \<le> bheight r \<Longrightarrow>
set (RBT_Impl.keys (rbt_joinL l a b r)) = set (RBT_Impl.keys l) \<union> {a} \<union> set (RBT_Impl.keys r)"
proof (induction l a b r rule: rbt_joinL.induct)
case (1 l a b r)
thus ?case
by (auto simp: set_baliL rbt_joinL.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma set_baliR:
"set (RBT_Impl.keys (baliR l a b r)) = set (RBT_Impl.keys l) \<union> {a} \<union> set (RBT_Impl.keys r)"
by (cases "(l,a,b,r)" rule: baliR.cases) auto
lemma set_rbt_joinR:
"set (RBT_Impl.keys (rbt_joinR l a b r)) = set (RBT_Impl.keys l) \<union> {a} \<union> set (RBT_Impl.keys r)"
proof (induction l a b r rule: rbt_joinR.induct)
case (1 l a b r)
thus ?case
by (force simp: set_baliR rbt_joinR.simps[of l a b r]
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma set_paint: "set (RBT_Impl.keys (paint c t)) = set (RBT_Impl.keys t)"
by (cases t) auto
lemma set_rbt_join: "set (RBT_Impl.keys (rbt_join l a b r)) =
set (RBT_Impl.keys l) \<union> {a} \<union> set (RBT_Impl.keys r)"
by (simp add: set_rbt_joinL set_rbt_joinR set_paint rbt_join_def)
lemma inv_rbt_join: "\<lbrakk> inv1 l; inv2 l; inv1 r; inv2 r \<rbrakk> \<Longrightarrow>
inv1 (rbt_join l a b r) \<and> inv2 (rbt_join l a b r)"
by (auto simp: rbt_join_def inv1l_rbt_joinL inv1l_rbt_joinR inv2_rbt_joinL inv2_rbt_joinR
inv2_paint inv1_paint_B)
lemma color_of_rbt_join: "color_of (rbt_join l a b r) = color.B"
by (auto simp: rbt_join_def color_of_paint_B)
lemma rbt_join: "rbt l \<Longrightarrow> rbt r \<Longrightarrow> rbt (rbt_join l a b r)"
using inv_rbt_join
by (fastforce simp: rbt_def color_of_rbt_join)
fun rbt_recolor :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"rbt_recolor (Branch RBT_Impl.R t1 k v t2) =
(if color_of t1 = RBT_Impl.B \<and> color_of t2 = RBT_Impl.B then Branch RBT_Impl.B t1 k v t2
else Branch RBT_Impl.R t1 k v t2)"
| "rbt_recolor t = t"
lemma rbt_recolor: "rbt t \<Longrightarrow> rbt (rbt_recolor t)"
by (induction t rule: rbt_recolor.induct) (auto simp: rbt_def)
fun split_min :: "('a, 'b) rbt \<Rightarrow> 'a \<times> 'b \<times> ('a, 'b) rbt" where
"split_min RBT_Impl.Empty = undefined"
| "split_min (RBT_Impl.Branch _ l a b r) =
(if is_empty l then (a,b,r) else let (a',b',l') = split_min l in (a',b',rbt_join l' a b r))"
lemma split_min_set:
"\<lbrakk> split_min t = (a,b,t'); t \<noteq> RBT_Impl.Empty \<rbrakk> \<Longrightarrow>
a \<in> set (RBT_Impl.keys t) \<and> set (RBT_Impl.keys t) = {a} \<union> set (RBT_Impl.keys t')"
by (induction t arbitrary: t') (auto simp: set_rbt_join split: prod.splits if_splits)
lemma split_min_inv:
"\<lbrakk> split_min t = (a,b,t'); rbt t; t \<noteq> RBT_Impl.Empty \<rbrakk> \<Longrightarrow> rbt t'"
by (induction t arbitrary: t') (auto simp: rbt_join split: if_splits prod.splits dest: rbt_Node)
definition rbt_join2 :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"rbt_join2 l r = (if is_empty r then l else let (a,b,r') = split_min r in rbt_join l a b r')"
lemma set_rbt_join2[simp]:
"set (RBT_Impl.keys (rbt_join2 l r)) = set (RBT_Impl.keys l) \<union> set (RBT_Impl.keys r)"
by (simp add: rbt_join2_def split_min_set set_rbt_join split: prod.split)
lemma inv_rbt_join2: "\<lbrakk> rbt l; rbt r \<rbrakk> \<Longrightarrow> rbt (rbt_join2 l r)"
by (simp add: rbt_join2_def rbt_join inv_rbt_join split_min_set split_min_inv split: prod.split)
context ord begin
fun split :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> ('a, 'b) rbt \<times> 'b option \<times> ('a, 'b) rbt" where
"split RBT_Impl.Empty k = (RBT_Impl.Empty, None, RBT_Impl.Empty)"
| "split (RBT_Impl.Branch _ l a b r) x =
(if x < a then (case split l x of (l1, \<beta>, l2) \<Rightarrow> (l1, \<beta>, rbt_join l2 a b r))
else if a < x then (case split r x of (r1, \<beta>, r2) \<Rightarrow> (rbt_join l a b r1, \<beta>, r2))
else (l, Some b, r))"
lemma split_rbt: "split t x = (l,\<beta>,r) \<Longrightarrow> rbt t \<Longrightarrow> rbt l \<and> rbt r"
by (induction t arbitrary: l r)
(auto simp: set_rbt_join rbt_join rbt_greater_prop rbt_less_prop
split: if_splits prod.splits dest!: rbt_Node)
lemma split_size: "split t2 a = (l2,\<beta>,r2) \<Longrightarrow> size l2 + size r2 \<le> size t2"
by (induction t2 a arbitrary: l2 r2 rule: split.induct) (auto split: if_splits prod.splits)
function union :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"union f t1 t2 = (let (f, t1, t2) =
if flip_rbt t1 t2 then (\<lambda>k v v'. f k v' v, t2, t1) else (f, t1, t2) in
if small_rbt t1 then RBT_Impl.fold (rbt_insert_with_key f) t1 t2
else (case t2 of RBT_Impl.Empty \<Rightarrow> t1
| RBT_Impl.Branch _ l2 a b r2 \<Rightarrow>
case split t1 a of (l1, \<beta>, r1) \<Rightarrow>
rbt_join (union f l1 l2) a (case \<beta> of None \<Rightarrow> b | Some b' \<Rightarrow> f a b b') (union f r1 r2)))"
by pat_completeness auto
termination
apply (relation "measure (\<lambda>(f,t1, t2). size t1 + size t2)")
apply (auto split: if_splits)
apply (metis add_leD1 le_imp_less_Suc ord.split_size trans_le_add2)
apply (metis add_leD1 le_imp_less_Suc ord.split_size trans_le_add1)
apply (metis add_leD2 le_imp_less_Suc ord.split_size trans_le_add2)
apply (metis add_leD2 le_imp_less_Suc ord.split_size trans_le_add1)
done
declare union.simps[simp del]
lemma rbt_fold_rbt_insert:
assumes "rbt t2"
shows "rbt (RBT_Impl.fold (rbt_insert_with_key f) t1 t2)"
proof -
define xs where "xs = RBT_Impl.entries t1"
from assms show ?thesis
unfolding RBT_Impl.fold_def xs_def[symmetric]
by (induct xs rule: rev_induct)
(auto simp: rbt_def rbt_insert_with_key_def ins_inv1_inv2)
qed
lemma rbt_union: "rbt t1 \<Longrightarrow> rbt t2 \<Longrightarrow> rbt (union f t1 t2)"
proof (induction f t1 t2 rule: union.induct)
case (1 t1 t2)
thus ?case
by (auto simp: union.simps[of t1 t2] rbt_join split_rbt rbt_fold_rbt_insert
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits prod.split if_splits
dest: rbt_Node)
qed
function inter :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"inter f t1 t2 = (let (f, t1, t2) =
if flip_rbt t1 t2 then (\<lambda>k v v'. f k v' v, t2, t1) else (f, t1, t2) in
if small_rbt t1 then
rbtreeify (List.map_filter (\<lambda>(k, v). case rbt_lookup t2 k of None \<Rightarrow> None
| Some v' \<Rightarrow> Some (k, f k v v')) (RBT_Impl.entries t1))
else case t2 of RBT_Impl.Empty \<Rightarrow> RBT_Impl.Empty
| RBT_Impl.Branch _ l2 a b r2 \<Rightarrow>
case split t1 a of (l1, \<beta>, r1) \<Rightarrow> let l' = inter f l1 l2; r' = inter f r1 r2 in
(case \<beta> of None \<Rightarrow> rbt_join2 l' r' | Some b' \<Rightarrow> rbt_join l' a (f a b b') r'))"
by pat_completeness auto
termination
apply (relation "measure (\<lambda>(f, t1, t2). size t1 + size t2)")
apply (auto split: if_splits)
apply (metis add_leD1 le_imp_less_Suc ord.split_size trans_le_add2)
apply (metis add_leD1 le_imp_less_Suc ord.split_size trans_le_add1)
apply (metis add_leD2 le_imp_less_Suc ord.split_size trans_le_add2)
apply (metis add_leD2 le_imp_less_Suc ord.split_size trans_le_add1)
done
declare inter.simps[simp del]
lemma rbt_rbtreeify[simp]: "rbt (rbtreeify kvs)"
by (simp add: rbt_def rbtreeify_def inv1_rbtreeify_g inv2_rbtreeify_g)
lemma rbt_inter: "rbt t1 \<Longrightarrow> rbt t2 \<Longrightarrow> rbt (inter f t1 t2)"
proof(induction f t1 t2 rule: inter.induct)
case (1 t1 t2)
thus ?case
by (auto simp: inter.simps[of t1 t2] inv_rbt_join inv_rbt_join2 split_rbt Let_def rbt_join
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits prod.split if_splits
option.splits dest!: rbt_Node)
qed
fun minus :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"minus t1 t2 = (if small_rbt t2 then RBT_Impl.fold (\<lambda>k _ t. rbt_delete k t) t2 t1
else if small_rbt t1 then
rbtreeify (filter (\<lambda>(k, _). rbt_lookup t2 k = None) (RBT_Impl.entries t1))
else case t2 of RBT_Impl.Empty \<Rightarrow> t1
| RBT_Impl.Branch _ l2 a b r2 \<Rightarrow>
case split t1 a of (l1, _, r1) \<Rightarrow> rbt_join2 (minus l1 l2) (minus r1 r2))"
declare minus.simps[simp del]
end
context linorder begin
lemma rbt_delete: "rbt t \<Longrightarrow> rbt (rbt_delete x t)"
using rbt_del_inv1_inv2[of t x]
by (auto simp: rbt_def rbt_delete_def rbt_del_inv1_inv2)
lemma rbt_fold_rbt_delete:
assumes "rbt t2"
shows "rbt (RBT_Impl.fold (\<lambda>k _ t. rbt_delete k t) t1 t2)"
proof -
define xs where "xs = RBT_Impl.entries t1"
from assms show ?thesis
unfolding RBT_Impl.fold_def xs_def[symmetric]
by (induct xs rule: rev_induct) (auto simp: rbt_delete)
qed
lemma rbt_minus: "rbt t1 \<Longrightarrow> rbt t2 \<Longrightarrow> rbt (minus t1 t2)"
proof(induction t1 t2 rule: minus.induct)
case (1 t1 t2)
thus ?case
by (auto simp: minus.simps[of t1 t2] inv_rbt_join inv_rbt_join2 split_rbt rbt_fold_rbt_delete
split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits prod.split if_splits
dest: rbt_Node)
qed
end
context
fixes comp :: "'a comparator"
begin
fun split_comp :: "('a, 'b) rbt \<Rightarrow> 'a \<Rightarrow> ('a, 'b) rbt \<times> 'b option \<times> ('a, 'b) rbt" where
"split_comp RBT_Impl.Empty k = (RBT_Impl.Empty, None, RBT_Impl.Empty)"
| "split_comp (RBT_Impl.Branch _ l a b r) x = (case comp x a of
Lt \<Rightarrow> (case split_comp l x of (l1, \<beta>, l2) \<Rightarrow> (l1, \<beta>, rbt_join l2 a b r))
| Gt \<Rightarrow> (case split_comp r x of (r1, \<beta>, r2) \<Rightarrow> (rbt_join l a b r1, \<beta>, r2))
| Eq \<Rightarrow> (l, Some b, r))"
lemma split_comp_size: "split_comp t2 a = (l2, b, r2) \<Longrightarrow> size l2 + size r2 \<le> size t2"
by (induction t2 a arbitrary: l2 b r2 rule: split_comp.induct)
(auto split: order.splits if_splits prod.splits)
function union_comp :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"union_comp f t1 t2 = (let (f, t1, t2) =
if flip_rbt t1 t2 then (\<lambda>k v v'. f k v' v, t2, t1) else (f, t1, t2) in
if small_rbt t1 then RBT_Impl.fold (rbt_comp_insert_with_key comp f) t1 t2
else (case t2 of RBT_Impl.Empty \<Rightarrow> t1
| RBT_Impl.Branch _ l2 a b r2 \<Rightarrow>
case split_comp t1 a of (l1, \<beta>, r1) \<Rightarrow>
rbt_join (union_comp f l1 l2) a (case \<beta> of None \<Rightarrow> b | Some b' \<Rightarrow> f a b b') (union_comp f r1 r2)))"
by pat_completeness auto
termination
apply (relation "measure (\<lambda>(f,t1, t2). size t1 + size t2)")
apply (auto split: if_splits)
apply (metis add_leD1 le_imp_less_Suc split_comp_size trans_le_add2)
apply (metis add_leD1 le_imp_less_Suc split_comp_size trans_le_add1)
apply (metis add_leD2 le_imp_less_Suc split_comp_size trans_le_add2)
apply (metis add_leD2 le_imp_less_Suc split_comp_size trans_le_add1)
done
declare union_comp.simps[simp del]
function inter_comp :: "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"inter_comp f t1 t2 = (let (f, t1, t2) =
if flip_rbt t1 t2 then (\<lambda>k v v'. f k v' v, t2, t1) else (f, t1, t2) in
if small_rbt t1 then
rbtreeify (List.map_filter (\<lambda>(k, v). case rbt_comp_lookup comp t2 k of None \<Rightarrow> None
| Some v' \<Rightarrow> Some (k, f k v v')) (RBT_Impl.entries t1))
else case t2 of RBT_Impl.Empty \<Rightarrow> RBT_Impl.Empty
| RBT_Impl.Branch _ l2 a b r2 \<Rightarrow>
case split_comp t1 a of (l1, \<beta>, r1) \<Rightarrow> let l' = inter_comp f l1 l2; r' = inter_comp f r1 r2 in
(case \<beta> of None \<Rightarrow> rbt_join2 l' r' | Some b' \<Rightarrow> rbt_join l' a (f a b b') r'))"
by pat_completeness auto
termination
apply (relation "measure (\<lambda>(f, t1, t2). size t1 + size t2)")
apply (auto split: if_splits)
apply (metis add_leD1 le_imp_less_Suc split_comp_size trans_le_add2)
apply (metis add_leD1 le_imp_less_Suc split_comp_size trans_le_add1)
apply (metis add_leD2 le_imp_less_Suc split_comp_size trans_le_add2)
apply (metis add_leD2 le_imp_less_Suc split_comp_size trans_le_add1)
done
declare inter_comp.simps[simp del]
fun minus_comp :: "('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where
"minus_comp t1 t2 = (if small_rbt t2 then RBT_Impl.fold (\<lambda>k _ t. rbt_comp_delete comp k t) t2 t1
else if small_rbt t1 then
rbtreeify (filter (\<lambda>(k, _). rbt_comp_lookup comp t2 k = None) (RBT_Impl.entries t1))
else case t2 of RBT_Impl.Empty \<Rightarrow> t1
| RBT_Impl.Branch _ l2 a b r2 \<Rightarrow>
case split_comp t1 a of (l1, _, r1) \<Rightarrow> rbt_join2 (minus_comp l1 l2) (minus_comp r1 r2))"
declare minus_comp.simps[simp del]
end
context fixes c :: "'a comparator"
assumes c: "comparator c"
begin
declare comparator.le_lt_convs[OF c, simp add]
lemma anti_sym: "lt_of_comp c a x \<Longrightarrow> lt_of_comp c x a \<Longrightarrow> False"
by (metis c comparator.Gt_lt_conv comparator.Lt_lt_conv order.distinct(5))
lemma split_comp: "split_comp c t x = ord.split (lt_of_comp c) t x"
by (induction t x rule: split_comp.induct[where comp=c])
(auto simp: ord.split.simps split: order.splits prod.splits dest: anti_sym)
lemma union_comp: "union_comp c f t1 t2 = ord.union (lt_of_comp c) f t1 t2"
proof (induction f t1 t2 rule: union_comp.induct[where comp=c])
case (1 f t1 t2)
obtain f' t1' t2' where flip:
"(f', t1', t2') = (if flip_rbt t1 t2 then (\<lambda>k v v'. f k v' v, t2, t1) else (f, t1, t2))"
by fastforce
show ?case
proof (cases t2')
case (Branch _ l2 a b r2)
have t1_not_Empty: "t2' \<noteq> RBT_Impl.Empty"
by (auto simp: Branch)
obtain l1 \<beta> r1 where split: "split_comp c t1' a = (l1, \<beta>, r1)"
by (cases "split_comp c t1' a") auto
show ?thesis
using 1[OF flip refl _ _ Branch]
unfolding union_comp.simps[of _ _ t1] ord.union.simps[of _ _ t1] flip[symmetric]
by (auto simp: Branch split split_comp[symmetric] rbt_comp_insert_with_key[OF c]
split: unit.splits prod.splits)
qed (auto simp: union_comp.simps[of _ _ t1] ord.union.simps[of _ _ t1] flip[symmetric]
rbt_comp_insert_with_key[OF c] split_comp[symmetric])
qed
lemma inter_comp: "inter_comp c f t1 t2 = ord.inter (lt_of_comp c) f t1 t2"
proof (induction f t1 t2 rule: inter_comp.induct[where comp=c])
case (1 f t1 t2)
obtain f' t1' t2' where flip:
"(f', t1', t2') = (if flip_rbt t1 t2 then (\<lambda>k v v'. f k v' v, t2, t1) else (f, t1, t2))"
by fastforce
show ?case
proof (cases t2')
case (Branch _ l2 a b r2)
have t1_not_Empty: "t2' \<noteq> RBT_Impl.Empty"
by (auto simp: Branch)
obtain l1 \<beta> r1 where split: "split_comp c t1' a = (l1, \<beta>, r1)"
by (cases "split_comp c t1' a") auto
show ?thesis
using 1[OF flip refl _ _ Branch]
unfolding inter_comp.simps[of _ _ t1] ord.inter.simps[of _ _ t1] flip[symmetric]
by (auto simp: Branch split split_comp[symmetric] rbt_comp_lookup[OF c]
split: unit.splits prod.splits)
qed (auto simp: inter_comp.simps[of _ _ t1] ord.inter.simps[of _ _ t1] flip[symmetric]
rbt_comp_lookup[OF c] split_comp[symmetric])
qed
lemma minus_comp: "minus_comp c t1 t2 = ord.minus (lt_of_comp c) t1 t2"
proof (induction t1 t2 rule: minus_comp.induct[where comp=c])
case (1 t1 t2)
show ?case
proof (cases t2)
case (Branch _ l2 a u r2)
have t2_not_Empty: "t2 \<noteq> RBT_Impl.Empty"
by (auto simp: Branch)
obtain l1 \<beta> r1 where split: "split_comp c t1 a = (l1, \<beta>, r1)"
by (cases "split_comp c t1 a") auto
show ?thesis
using 1[OF _ _ Branch]
unfolding minus_comp.simps[of _ t1 t2] ord.minus.simps[of _ t1 t2]
by (auto simp: Branch split split_comp[symmetric] rbt_comp_delete[OF c] rbt_comp_lookup[OF c]
split: unit.splits prod.splits)
qed (auto simp: minus_comp.simps[of _ t1] ord.minus.simps[of _ t1]
rbt_comp_delete[OF c] rbt_comp_lookup[OF c] split_comp[symmetric])
qed
end
context linorder begin
lemma rbt_sorted_baliL:
"\<lbrakk>rbt_sorted l; rbt_sorted r; l |\<guillemotleft> a; a \<guillemotleft>| r\<rbrakk> \<Longrightarrow> rbt_sorted (baliL l a b r)"
using rbt_greater_trans rbt_less_trans
apply (cases "(l,a,b,r)" rule: baliL.cases)
apply (auto simp: rbt_sorted_def)
apply blast+
done
lemma rbt_sorted_baliR:
"\<lbrakk>rbt_sorted l; rbt_sorted r; l |\<guillemotleft> a; a \<guillemotleft>| r\<rbrakk> \<Longrightarrow> rbt_sorted (baliR l a b r)"
using rbt_greater_trans rbt_less_trans
apply (cases "(l,a,b,r)" rule: baliR.cases)
apply (auto simp: rbt_sorted_def)
apply blast+
done
lemma rbt_sorted_rbt_joinL:
"\<lbrakk>rbt_sorted (RBT_Impl.Branch c l a b r); bheight l \<le> bheight r\<rbrakk>
\<Longrightarrow> rbt_sorted (rbt_joinL l a b r)"
proof (induction l a b r arbitrary: c rule: rbt_joinL.induct)
case (1 l a b r)
thus ?case
by (auto simp: set_baliL rbt_joinL.simps[of l a b r] set_rbt_joinL rbt_less_prop
intro!: rbt_sorted_baliL split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma rbt_sorted_rbt_joinR:
"\<lbrakk>rbt_sorted l; rbt_sorted r; l |\<guillemotleft> a; a \<guillemotleft>| r\<rbrakk>
\<Longrightarrow> rbt_sorted (rbt_joinR l a b r)"
proof (induction l a b r rule: rbt_joinR.induct)
case (1 l a b r)
thus ?case
by (auto simp: set_baliR rbt_joinR.simps[of l a b r] set_rbt_joinR rbt_greater_prop
intro!: rbt_sorted_baliR split!: RBT_Impl.rbt.splits RBT_Impl.color.splits unit.splits)
qed
lemma rbt_sorted_paint: "rbt_sorted (paint c t) = rbt_sorted t"
by (cases t) auto
lemma rbt_sorted_rbt_join: "rbt_sorted (RBT_Impl.Branch c l a b r) \<Longrightarrow>
rbt_sorted (rbt_join l a b r)"
by (auto simp: rbt_sorted_paint rbt_sorted_rbt_joinL rbt_sorted_rbt_joinR rbt_join_def)
lemma split_min_rbt_sorted:
"\<lbrakk> split_min t = (a,b,t'); rbt_sorted t; t \<noteq> RBT_Impl.Empty \<rbrakk> \<Longrightarrow>
rbt_sorted t' \<and> (\<forall>x \<in> set (RBT_Impl.keys t'). a < x)"
by (induction t arbitrary: t')
(fastforce simp: split_min_set rbt_sorted_rbt_join set_rbt_join rbt_less_prop rbt_greater_prop
split: if_splits prod.splits)+
lemma rbt_sorted_rbt_join2:
"\<lbrakk> rbt_sorted l; rbt_sorted r; \<forall>x \<in> set (RBT_Impl.keys l). \<forall>y \<in> set (RBT_Impl.keys r). x < y \<rbrakk>
\<Longrightarrow> rbt_sorted (rbt_join2 l r)"
by (simp add: rbt_join2_def rbt_sorted_rbt_join split_min_set split_min_rbt_sorted set_rbt_join
rbt_greater_prop rbt_less_prop split: prod.split)
lemma split: "split t x = (l,\<beta>,r) \<Longrightarrow> rbt_sorted t \<Longrightarrow>
set (RBT_Impl.keys l) = {a \<in> set (RBT_Impl.keys t). a < x} \<and>
set (RBT_Impl.keys r) = {a \<in> set (RBT_Impl.keys t). x < a} \<and>
rbt_sorted l \<and> rbt_sorted r"
by (induction t arbitrary: l r)
(force simp: Let_def set_rbt_join rbt_greater_prop rbt_less_prop
split: if_splits prod.splits intro!: rbt_sorted_rbt_join)+
lemma split_lookup: "split t x = (l,\<beta>,r) \<Longrightarrow> rbt_sorted t \<Longrightarrow> \<beta> = rbt_lookup t x"
by (induction t arbitrary: l r)
(force simp: Let_def set_rbt_join rbt_greater_prop rbt_less_prop
split: if_splits prod.splits intro!: rbt_sorted_rbt_join)+
lemma keys_paint'[simp]: "RBT_Impl.keys (RBT_Impl.paint c t) = RBT_Impl.keys t"
by (cases t) auto
lemma [simp]: "set (RBT_Impl.keys (rbt_insert_with_key f a b t2)) = {a} \<union> set (RBT_Impl.keys t2)"
by (auto simp: rbt_insert_with_key_def keys_ins)
lemma set_tree_fold_insert:
assumes "rbt_sorted t2"
shows "set (RBT_Impl.keys (RBT_Impl.fold (rbt_insert_with_key f) t1 t2)) =
set (RBT_Impl.keys t1) \<union> set (RBT_Impl.keys t2)"
proof -
define xs where "xs = RBT_Impl.entries t1"
have keys_t1: "set (RBT_Impl.keys t1) = fst ` set xs"
by (auto simp: xs_def RBT_Impl.keys_def)
from assms show ?thesis
unfolding RBT_Impl.fold_def xs_def[symmetric] keys_t1
by (induction xs rule: rev_induct) (auto simp: rev_image_eqI)
qed
lemma rbt_sorted_fold_insertwk:
"rbt_sorted t \<Longrightarrow> rbt_sorted (RBT_Impl.fold (rbt_insert_with_key f) t' t)"
by (induct t' arbitrary: t)
(simp_all add: rbt_insertwk_rbt_sorted)
lemma rbt_sorted_union: "rbt_sorted t1 \<Longrightarrow> rbt_sorted t2 \<Longrightarrow>
set (RBT_Impl.keys (union f t1 t2)) = set (RBT_Impl.keys t1) \<union> set (RBT_Impl.keys t2) \<and>
rbt_sorted (union f t1 t2)"
proof(induction f t1 t2 rule: union.induct)
case (1 f t1 t2)
obtain f' t1' t2' where flip:
"(f', t1', t2') = (if flip_rbt t1 t2 then (\<lambda>k v v'. f k v' v, t2, t1) else (f, t1, t2))"
by fastforce
have set_flip: "set (RBT_Impl.keys t1) \<union> set (RBT_Impl.keys t2) =
set (RBT_Impl.keys t1') \<union> set (RBT_Impl.keys t2')"
using flip
by (auto split: if_splits)
have rbt_sorted': "rbt_sorted t1'" "rbt_sorted t2'"
using 1(3,4) flip
by (auto split: if_splits)
then show ?case
proof (cases t2')
case (Branch _ l2 a b r2)
obtain l1 \<beta> r1 where split_t1': "split t1' a = (l1, \<beta>, r1)"
by (cases "split t1' a") auto
have rbt_sort: "rbt_sorted l2" "rbt_sorted r2"
using 1(3,4) flip
by (auto simp: Branch split: if_splits)
note split_t1'_prop = split[OF split_t1' rbt_sorted'(1)]
have union_l1_l2: "\<not>small_rbt t1' \<Longrightarrow>
set (RBT_Impl.keys (union f' l1 l2)) = set (RBT_Impl.keys l1) \<union> set (RBT_Impl.keys l2) \<and>
rbt_sorted (union f' l1 l2)"
using 1(1)[OF flip refl refl _ Branch split_t1'[symmetric]] rbt_sort split_t1'_prop
by auto
have union_r1_r2: "\<not>small_rbt t1' \<Longrightarrow>
set (RBT_Impl.keys (union f' r1 r2)) = set (RBT_Impl.keys r1) \<union> set (RBT_Impl.keys r2) \<and>
rbt_sorted (union f' r1 r2)"
using 1(2)[OF flip refl refl _ Branch split_t1'[symmetric]] rbt_sort split_t1'_prop
by auto
have "set (RBT_Impl.keys (union f t1 t2)) = set (RBT_Impl.keys t1) \<union> set (RBT_Impl.keys t2)"
using rbt_sorted' union_l1_l2 union_r1_r2 split_t1'_prop
unfolding set_flip union.simps[of _ t1] flip[symmetric]
by (auto simp: set_tree_fold_insert Branch split_t1' set_rbt_join
split!: unit.splits if_splits option.splits)
moreover have "rbt_sorted (union f t1 t2)"
using rbt_sorted' 1(3,4) union_l1_l2 union_r1_r2 split_t1'_prop
unfolding set_flip union.simps[of _ t1] flip[symmetric]
by (auto simp: rbt_sorted_fold_insertwk Branch split_t1' rbt_less_prop rbt_greater_prop
intro!: rbt_sorted_rbt_join
split!: unit.splits if_splits option.splits)
ultimately show ?thesis
by auto
qed (auto simp: set_flip union.simps[of _ t1] flip[symmetric] set_tree_fold_insert
intro!: rbt_sorted_fold_insertwk)
qed
lemma rbt_sorted_rbtreeify_map_filter:
assumes "rbt_sorted t"
shows "rbt_sorted (rbtreeify (List.map_filter
(\<lambda>(k, v). case rbt_lookup t2 k of None \<Rightarrow> None
| Some v' \<Rightarrow> Some (k, f k v v')) (RBT_Impl.entries t)))"
proof -
have unfold: "map fst (List.map_filter (\<lambda>(k, v). case P k of None \<Rightarrow> None
| Some v' \<Rightarrow> Some (k, f k v v')) xs) =
filter (\<lambda>k. case P k of None \<Rightarrow> False | _ \<Rightarrow> True) (map fst xs)"
for P xs
by (induction xs) (auto simp: List.map_filter_def split: option.splits)
show ?thesis
using rbt_sorted_entries[OF assms] distinct_entries[OF assms] sorted_filter[of id]
by (auto simp: unfold intro!: rbt_sorted_rbtreeify)
qed
lemma rbtreeify_keys_map_filter: "rbt_sorted t2 \<Longrightarrow>
set (RBT_Impl.keys (rbtreeify (List.map_filter (\<lambda>(k, v). case rbt_lookup t2 k of None \<Rightarrow> None
| Some v' \<Rightarrow> Some (k, f k v v')) (RBT_Impl.entries t1)))) =
set (RBT_Impl.keys t1) \<inter> set (RBT_Impl.keys t2)"
apply (auto simp: RBT_Impl.keys_def List.map_filter_def split: option.splits)
apply force
apply (metis local.map_of_entries map_of_eq_None_iff option.distinct(1))
apply (smt image_iff local.map_of_entries local.rbt_lookup_in_tree mem_Collect_eq
option.case(2) option.collapse option.distinct(1) option.simps(1) prod.sel(1) prod.simps(2))
done
lemma rbt_lookup_iff_keys:
"rbt_sorted t \<Longrightarrow> rbt_lookup t k = None \<longleftrightarrow> k \<notin> set (RBT_Impl.keys t)"
"rbt_sorted t \<Longrightarrow> (\<exists>v. rbt_lookup t k = Some v) \<longleftrightarrow> k \<in> set (RBT_Impl.keys t)"
using entry_in_tree_keys rbt_lookup_keys[of t]
by (fastforce simp: RBT_Impl.keys_def dom_def)+
lemma rbt_sorted_inter: "rbt_sorted t1 \<Longrightarrow> rbt_sorted t2 \<Longrightarrow>
set (RBT_Impl.keys (inter f t1 t2)) = set (RBT_Impl.keys t1) \<inter> set (RBT_Impl.keys t2) \<and>
rbt_sorted (inter f t1 t2)"
proof(induction f t1 t2 rule: inter.induct)
case (1 f t1 t2)
obtain f' t1' t2' where flip:
"(f', t1', t2') = (if flip_rbt t1 t2 then (\<lambda>k v v'. f k v' v, t2, t1) else (f, t1, t2))"
by fastforce
have set_flip: "set (RBT_Impl.keys t1) \<inter> set (RBT_Impl.keys t2) =
set (RBT_Impl.keys t1') \<inter> set (RBT_Impl.keys t2')"
using flip
by (auto split: if_splits)
have rbt_sorted': "rbt_sorted t1'" "rbt_sorted t2'"
using 1(3,4) flip
by (auto split: if_splits)
show ?case
proof (cases t2')
case [simp]: (Branch _ l2 a u r2)
have set_flip: "set (RBT_Impl.keys t1) \<inter> set (RBT_Impl.keys t2) =
set (RBT_Impl.keys t1') \<inter> set (RBT_Impl.keys t2')"
using flip
by (auto split: if_splits)
obtain l1 \<beta> r1 where sp: "split t1' a = (l1, \<beta>, r1)"
by (cases "split t1' a") auto
have rbt_sort: "rbt_sorted l2" "rbt_sorted r2"
using 1(3,4) flip
by (auto split: if_splits)
note split_t1'_prop = split[OF sp rbt_sorted'(1)]
have inter_l1_l2: "\<not>small_rbt t1' \<Longrightarrow>
set (RBT_Impl.keys (inter f' l1 l2)) = set (RBT_Impl.keys l1) \<inter> set (RBT_Impl.keys l2) \<and>
rbt_sorted (inter f' l1 l2)"
using 1(1)[OF flip refl refl _ Branch sp[symmetric]] rbt_sort split_t1'_prop
by auto
have inter_r1_r2: "\<not>small_rbt t1' \<Longrightarrow>
set (RBT_Impl.keys (inter f' r1 r2)) = set (RBT_Impl.keys r1) \<inter> set (RBT_Impl.keys r2) \<and>
rbt_sorted (inter f' r1 r2)"
using 1(2)[OF flip refl refl _ Branch sp[symmetric]] rbt_sort split_t1'_prop
by auto
{
assume not_small: "\<not>small_rbt t1'"
let ?L2 = "set (RBT_Impl.keys l2)"
let ?R2 = "set (RBT_Impl.keys r2)"
have *: "a \<notin> ?L2 \<union> ?R2" using \<open>rbt_sorted t2'\<close>
by (auto simp: rbt_less_prop rbt_greater_prop)
let ?L1 = "set (RBT_Impl.keys l1)"
let ?R1 = "set (RBT_Impl.keys r1)"
let ?K = "case \<beta> of None \<Rightarrow> {} | _ \<Rightarrow> {a}"
have t2: "set (RBT_Impl.keys t1') = ?L1 \<union> ?R1 \<union> ?K" and
**: "?L1 \<inter> ?R1 = {}" "a \<notin> ?L1 \<union> ?R1" "?L2 \<inter> ?R1 = {}" "?L1 \<inter> ?R2 = {}"
using split[OF sp] split_lookup[OF sp] rbt_lookup_iff_keys[of t1'] less_linear rbt_sorted'
by (auto simp: rbt_less_prop rbt_greater_prop split: option.splits)
have "set (RBT_Impl.keys t1') \<inter> set (RBT_Impl.keys t2') =
(?L2 \<union> ?R2 \<union> {a}) \<inter> (?L1 \<union> ?R1 \<union> ?K)"
by (auto simp add: t2)
also have "\<dots> = (?L1 \<inter> ?L2) \<union> (?R1 \<inter> ?R2) \<union> ?K"
using * **
by (auto split: option.splits)
also have "\<dots> = set (RBT_Impl.keys (inter f t1 t2))"
using inter_l1_l2[OF not_small] inter_r1_r2[OF not_small]
by (auto simp: inter.simps[of _ t1] flip[symmetric] not_small sp set_rbt_join
split: unit.splits option.splits)
finally have "set (RBT_Impl.keys (inter f t1 t2)) =
set (RBT_Impl.keys t1) \<inter> set (RBT_Impl.keys t2)"
unfolding set_flip
by auto
}
moreover have "small_rbt t1' \<Longrightarrow> set (RBT_Impl.keys (inter f t1 t2)) =
set (RBT_Impl.keys (rbtreeify (List.map_filter (\<lambda>(k, v). case rbt_lookup t2' k of None \<Rightarrow> None
| Some v' \<Rightarrow> Some (k, f' k v v')) (RBT_Impl.entries t1'))))"
by (auto simp: inter.simps[of _ t1] flip[symmetric])
ultimately have "set (RBT_Impl.keys (ord_class.inter f t1 t2)) =
set (RBT_Impl.keys t1) \<inter> set (RBT_Impl.keys t2)"
using flip
unfolding rbtreeify_keys_map_filter[OF rbt_sorted'(2)] set_flip
by auto
moreover have "rbt_sorted (inter f t1 t2)"
using rbt_sorted'(1) rbt_sort 1(3,4) inter_l1_l2 inter_r1_r2 split_t1'_prop
by (auto simp: inter.simps[of _ t1] flip[symmetric] sp rbt_less_prop rbt_greater_prop Let_def
intro!: rbt_sorted_rbtreeify_map_filter rbt_sorted_rbt_join rbt_sorted_rbt_join2
split!: unit.splits if_splits option.splits)
ultimately show ?thesis
by auto
qed (auto simp: rbtreeify_def set_flip inter.simps[of _ t1] flip[symmetric] List.map_filter_def)
qed
lemma [simp]: "RBT_Impl.entries (RBT_Impl.paint c t) = RBT_Impl.entries t"
by (cases t) auto
lemma [simp]: "rbt t \<Longrightarrow> rbt_sorted t \<Longrightarrow>
set (RBT_Impl.keys (rbt_delete a t)) = set (RBT_Impl.keys t) - {a}"
using rbt_del_in_tree[of t]
by (auto simp: rbt_def RBT_Impl.keys_def rbt_delete_def)
lemma [simp]: "rbt_sorted t \<Longrightarrow> rbt_sorted (rbt_delete x t)"
by (auto simp: rbt_delete_def rbt_del_rbt_sorted)
lemma fold_rbt_delete:
assumes "rbt t2" "rbt_sorted t2"
shows "set (RBT_Impl.keys (RBT_Impl.fold (\<lambda>k _ t. rbt_delete k t) t1 t2)) =
set (RBT_Impl.keys t2) - set (RBT_Impl.keys t1)"
"rbt (RBT_Impl.fold (\<lambda>k _ t. rbt_delete k t) t1 t2)"
"rbt_sorted (RBT_Impl.fold (\<lambda>k _ t. rbt_delete k t) t1 t2)"
proof -
define xs where "xs = RBT_Impl.entries t1"
have keys_t1: "set (RBT_Impl.keys t1) = fst ` set xs"
by (auto simp: xs_def RBT_Impl.keys_def)
from assms show
"set (RBT_Impl.keys (RBT_Impl.fold (\<lambda>k _ t. rbt_delete k t) t1 t2)) =
set (RBT_Impl.keys t2) - set (RBT_Impl.keys t1)"
"rbt (RBT_Impl.fold (\<lambda>k _ t. rbt_delete k t) t1 t2)"
"rbt_sorted (RBT_Impl.fold (\<lambda>k _ t. rbt_delete k t) t1 t2)"
unfolding RBT_Impl.fold_def xs_def[symmetric] keys_t1
by (induct xs rule: rev_induct) (auto simp: rev_image_eqI rbt_delete rbt_del_rbt_sorted)
qed
lemma rbt_sorted_fold_delete: "rbt_sorted t \<Longrightarrow>
rbt_sorted (RBT_Impl.fold (\<lambda>k _ t. rbt_delete k t) t' t)"
by (induct t' arbitrary: t) auto
lemma rbtreeify_keys_None:
assumes "rbt_sorted t1"
shows "set (RBT_Impl.keys (rbtreeify (filter (\<lambda>(k, _). rbt_lookup t1 k = None)
(RBT_Impl.entries t2)))) = set (RBT_Impl.keys t2) - set (RBT_Impl.keys t1)"
apply (auto simp: RBT_Impl.keys_def map_of_entries[OF assms, symmetric] split: prod.splits)
using image_iff weak_map_of_SomeI
apply fastforce
apply (smt fst_conv image_iff map_of_eq_None_iff mem_Collect_eq)
done