|
1 (* Author: Lukas Bulwahn, TU Muenchen *) |
|
2 |
|
3 header {* Lifting operations of RBT trees *} |
|
4 |
|
5 theory Lift_RBT |
|
6 imports Main "~~/src/HOL/Library/RBT_Impl" |
|
7 begin |
|
8 |
|
9 subsection {* Type definition *} |
|
10 |
|
11 typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}" |
|
12 morphisms impl_of RBT |
|
13 proof - |
|
14 have "RBT_Impl.Empty \<in> ?rbt" by simp |
|
15 then show ?thesis .. |
|
16 qed |
|
17 |
|
18 local_setup {* fn lthy => |
|
19 let |
|
20 val quotients = {qtyp = @{typ "('a, 'b) rbt"}, rtyp = @{typ "('a, 'b) RBT_Impl.rbt"}, |
|
21 equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}} |
|
22 val qty_full_name = @{type_name "rbt"} |
|
23 |
|
24 fun qinfo phi = Quotient_Info.transform_quotients phi quotients |
|
25 in lthy |
|
26 |> Local_Theory.declaration {syntax = false, pervasive = true} |
|
27 (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi) |
|
28 #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi |
|
29 {abs = @{term "RBT"}, rep = @{term "impl_of"}})) |
|
30 end |
|
31 *} |
|
32 |
|
33 lemma rbt_eq_iff: |
|
34 "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2" |
|
35 by (simp add: impl_of_inject) |
|
36 |
|
37 lemma rbt_eqI: |
|
38 "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2" |
|
39 by (simp add: rbt_eq_iff) |
|
40 |
|
41 lemma is_rbt_impl_of [simp, intro]: |
|
42 "is_rbt (impl_of t)" |
|
43 using impl_of [of t] by simp |
|
44 |
|
45 lemma RBT_impl_of [simp, code abstype]: |
|
46 "RBT (impl_of t) = t" |
|
47 by (simp add: impl_of_inverse) |
|
48 |
|
49 |
|
50 subsection {* Primitive operations *} |
|
51 |
|
52 quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup" |
|
53 |
|
54 declare lookup_def[unfolded map_fun_def comp_def id_def, code] |
|
55 |
|
56 (* FIXME: some bug in quotient?*) |
|
57 (* |
|
58 quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt" |
|
59 is "RBT_Impl.Empty" |
|
60 *) |
|
61 |
|
62 definition empty :: "('a\<Colon>linorder, 'b) rbt" where |
|
63 "empty = RBT RBT_Impl.Empty" |
|
64 |
|
65 lemma impl_of_empty [code abstract]: |
|
66 "impl_of empty = RBT_Impl.Empty" |
|
67 by (simp add: empty_def RBT_inverse) |
|
68 |
|
69 quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
70 is "RBT_Impl.insert" |
|
71 |
|
72 lemma impl_of_insert [code abstract]: |
|
73 "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)" |
|
74 by (simp add: insert_def RBT_inverse) |
|
75 |
|
76 quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
77 is "RBT_Impl.delete" |
|
78 |
|
79 lemma impl_of_delete [code abstract]: |
|
80 "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)" |
|
81 by (simp add: delete_def RBT_inverse) |
|
82 |
|
83 (* FIXME: bug in quotient? *) |
|
84 (* |
|
85 quotient_definition entries where "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" |
|
86 is "RBT_Impl.entries" |
|
87 *) |
|
88 definition entries :: "('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list" where |
|
89 [code]: "entries t = RBT_Impl.entries (impl_of t)" |
|
90 |
|
91 (* FIXME: bug in quotient? *) |
|
92 (* |
|
93 quotient_definition keys where "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list" |
|
94 is "RBT_Impl.keys" |
|
95 *) |
|
96 |
|
97 quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt" |
|
98 is "RBT_Impl.bulkload" |
|
99 |
|
100 lemma impl_of_bulkload [code abstract]: |
|
101 "impl_of (bulkload xs) = RBT_Impl.bulkload xs" |
|
102 by (simp add: bulkload_def RBT_inverse) |
|
103 |
|
104 quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
105 is "RBT_Impl.map_entry" |
|
106 |
|
107 lemma impl_of_map_entry [code abstract]: |
|
108 "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)" |
|
109 by (simp add: map_entry_def RBT_inverse) |
|
110 |
|
111 (* Another bug: map is supposed to be a new definition, not using the old one. |
|
112 quotient_definition "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
113 is "RBT_Impl.map" |
|
114 *) |
|
115 (* But this works, and then shows the other bug... *) |
|
116 (* |
|
117 quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" |
|
118 is "RBT_Impl.map" |
|
119 *) |
|
120 definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt" where |
|
121 "map f t = RBT (RBT_Impl.map f (impl_of t))" |
|
122 |
|
123 lemma impl_of_map [code abstract]: |
|
124 "impl_of (map f t) = RBT_Impl.map f (impl_of t)" |
|
125 by (simp add: map_def RBT_inverse) |
|
126 (* FIXME: bug? |
|
127 quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is "RBT_Impl.fold" |
|
128 *) |
|
129 (*FIXME: definition of fold should have the code attribute. *) |
|
130 |
|
131 definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where |
|
132 [code]: "fold f t = RBT_Impl.fold f (impl_of t)" |
|
133 |
|
134 |
|
135 end |