4 |
4 |
5 theory Lift_RBT |
5 theory Lift_RBT |
6 imports Main "~~/src/HOL/Library/RBT_Impl" |
6 imports Main "~~/src/HOL/Library/RBT_Impl" |
7 begin |
7 begin |
8 |
8 |
|
9 definition inv :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
10 where [simp]: "inv R = (\<lambda>x y. R x \<and> x = y)" |
|
11 |
9 subsection {* Type definition *} |
12 subsection {* Type definition *} |
10 |
13 |
11 typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}" |
14 quotient_type ('a, 'b) rbt = "('a\<Colon>linorder, 'b) RBT_Impl.rbt" / "inv is_rbt" morphisms impl_of RBT |
12 morphisms impl_of RBT |
15 sorry |
13 proof - |
16 |
14 have "RBT_Impl.Empty \<in> ?rbt" by simp |
17 (* |
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 "op ="}, 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: |
18 lemma rbt_eq_iff: |
34 "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2" |
19 "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2" |
35 by (simp add: impl_of_inject) |
20 by (simp add: impl_of_inject) |
36 |
21 |
37 lemma rbt_eqI: |
22 lemma rbt_eqI: |
43 using impl_of [of t] by simp |
28 using impl_of [of t] by simp |
44 |
29 |
45 lemma RBT_impl_of [simp, code abstype]: |
30 lemma RBT_impl_of [simp, code abstype]: |
46 "RBT (impl_of t) = t" |
31 "RBT (impl_of t) = t" |
47 by (simp add: impl_of_inverse) |
32 by (simp add: impl_of_inverse) |
48 |
33 *) |
49 |
34 |
50 subsection {* Primitive operations *} |
35 subsection {* Primitive operations *} |
51 |
36 |
52 quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup" |
37 quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup" |
53 done |
38 by simp |
54 |
39 |
55 declare lookup_def[unfolded map_fun_def comp_def id_def, code] |
40 declare lookup_def[unfolded map_fun_def comp_def id_def, code] |
56 |
41 |
57 (* FIXME: quotient_definition at the moment requires that types variables match exactly, |
42 (* FIXME: quotient_definition at the moment requires that types variables match exactly, |
58 i.e., sort constraints must be annotated to the constant being lifted. |
43 i.e., sort constraints must be annotated to the constant being lifted. |