equal
deleted
inserted
replaced
7 |
7 |
8 (*<*) |
8 (*<*) |
9 theory RBT |
9 theory RBT |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
|
13 lemma map_sorted_distinct_set_unique: (*FIXME move*) |
|
14 assumes "inj_on f (set xs \<union> set ys)" |
|
15 assumes "sorted (map f xs)" "distinct (map f xs)" |
|
16 "sorted (map f ys)" "distinct (map f ys)" |
|
17 assumes "set xs = set ys" |
|
18 shows "xs = ys" |
|
19 proof - |
|
20 from assms have "map f xs = map f ys" |
|
21 by (simp add: sorted_distinct_set_unique) |
|
22 moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys" |
|
23 by (blast intro: map_inj_on) |
|
24 qed |
|
25 |
12 |
26 subsection {* Datatype of RB trees *} |
13 subsection {* Datatype of RB trees *} |
27 |
14 |
28 datatype color = R | B |
15 datatype color = R | B |
29 datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt" |
16 datatype ('a, 'b) rbt = Empty | Branch color "('a, 'b) rbt" 'a 'b "('a, 'b) rbt" |