1.1 --- a/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Mar 23 14:25:31 2012 +0100
1.2 +++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Mar 23 14:26:09 2012 +0100
1.3 @@ -6,15 +6,15 @@
1.4 imports Main "~~/src/HOL/Library/RBT_Impl"
1.5 begin
1.6
1.7 -definition inv :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
1.8 - where [simp]: "inv R = (\<lambda>x y. R x \<and> x = y)"
1.9 -
1.10 subsection {* Type definition *}
1.11
1.12 -quotient_type ('a, 'b) rbt = "('a\<Colon>linorder, 'b) RBT_Impl.rbt" / "inv is_rbt" morphisms impl_of RBT
1.13 -sorry
1.14 +typedef (open) ('a, 'b) rbt = "{t :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt. is_rbt t}"
1.15 + morphisms impl_of RBT
1.16 +proof -
1.17 + have "RBT_Impl.Empty \<in> ?rbt" by simp
1.18 + then show ?thesis ..
1.19 +qed
1.20
1.21 -(*
1.22 lemma rbt_eq_iff:
1.23 "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
1.24 by (simp add: impl_of_inject)
1.25 @@ -30,15 +30,14 @@
1.26 lemma RBT_impl_of [simp, code abstype]:
1.27 "RBT (impl_of t) = t"
1.28 by (simp add: impl_of_inverse)
1.29 -*)
1.30
1.31 subsection {* Primitive operations *}
1.32
1.33 +setup_lifting type_definition_rbt
1.34 +
1.35 quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
1.36 by simp
1.37
1.38 -declare lookup_def[unfolded map_fun_def comp_def id_def, code]
1.39 -
1.40 (* FIXME: quotient_definition at the moment requires that types variables match exactly,
1.41 i.e., sort constraints must be annotated to the constant being lifted.
1.42 But, it should be possible to infer the necessary sort constraints, making the explicit
1.43 @@ -53,67 +52,38 @@
1.44 *)
1.45
1.46 quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
1.47 -is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" done
1.48 -
1.49 -lemma impl_of_empty [code abstract]:
1.50 - "impl_of empty = RBT_Impl.Empty"
1.51 - by (simp add: empty_def RBT_inverse)
1.52 +is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" by (simp add: empty_def)
1.53
1.54 quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
1.55 -is "RBT_Impl.insert" done
1.56 -
1.57 -lemma impl_of_insert [code abstract]:
1.58 - "impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
1.59 - by (simp add: insert_def RBT_inverse)
1.60 +is "RBT_Impl.insert" by simp
1.61
1.62 quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
1.63 -is "RBT_Impl.delete" done
1.64 -
1.65 -lemma impl_of_delete [code abstract]:
1.66 - "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
1.67 - by (simp add: delete_def RBT_inverse)
1.68 +is "RBT_Impl.delete" by simp
1.69
1.70 (* FIXME: unnecessary type annotations *)
1.71 quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
1.72 -is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" done
1.73 -
1.74 -lemma [code]: "entries t = RBT_Impl.entries (impl_of t)"
1.75 -unfolding entries_def map_fun_def comp_def id_def ..
1.76 +is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" by simp
1.77
1.78 (* FIXME: unnecessary type annotations *)
1.79 quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
1.80 -is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" done
1.81 +is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" by simp
1.82
1.83 quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
1.84 -is "RBT_Impl.bulkload" done
1.85 -
1.86 -lemma impl_of_bulkload [code abstract]:
1.87 - "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
1.88 - by (simp add: bulkload_def RBT_inverse)
1.89 +is "RBT_Impl.bulkload" by simp
1.90
1.91 quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
1.92 -is "RBT_Impl.map_entry" done
1.93 -
1.94 -lemma impl_of_map_entry [code abstract]:
1.95 - "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
1.96 - by (simp add: map_entry_def RBT_inverse)
1.97 +is "RBT_Impl.map_entry" by simp
1.98
1.99 (* FIXME: unnecesary type annotations *)
1.100 quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
1.101 is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt"
1.102 -done
1.103 -
1.104 -lemma impl_of_map [code abstract]:
1.105 - "impl_of (map f t) = RBT_Impl.map f (impl_of t)"
1.106 - by (simp add: map_def RBT_inverse)
1.107 +by simp
1.108
1.109 (* FIXME: unnecessary type annotations *)
1.110 quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
1.111 -is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" done
1.112 +is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" by simp
1.113
1.114 -lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
1.115 -unfolding fold_def map_fun_def comp_def id_def ..
1.116 -
1.117 +export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
1.118
1.119 subsection {* Derived operations *}
1.120
1.121 @@ -177,6 +147,10 @@
1.122 "fold f t = List.fold (prod_case f) (entries t)"
1.123 by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
1.124
1.125 +lemma impl_of_empty:
1.126 + "impl_of empty = RBT_Impl.Empty"
1.127 + by (simp add: empty_def RBT_inverse)
1.128 +
1.129 lemma is_empty_empty [simp]:
1.130 "is_empty t \<longleftrightarrow> t = empty"
1.131 by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
1.132 @@ -198,5 +172,4 @@
1.133 by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
1.134
1.135
1.136 -
1.137 end
1.138 \ No newline at end of file