--- a/doc-src/IsarImplementation/Thy/ML.thy Wed Mar 28 11:17:32 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Mar 28 11:40:12 2012 +0200
@@ -120,7 +120,7 @@
For historical reasons, many capitalized names omit underscores,
e.g.\ old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}.
- Genuine mixed-case names are \emph{not} used, bacause clear division
+ Genuine mixed-case names are \emph{not} used, because clear division
of words is essential for readability.\footnote{Camel-case was
invented to workaround the lack of underscore in some early
non-ASCII character sets. Later it became habitual in some language
@@ -1774,4 +1774,4 @@
to implement a mailbox as synchronized variable over a purely
functional queue. *}
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/DAList.thy Wed Mar 28 11:17:32 2012 +0200
+++ b/src/HOL/Library/DAList.thy Wed Mar 28 11:40:12 2012 +0200
@@ -68,17 +68,6 @@
where "map_default" is "AList.map_default :: 'key => 'value => ('value => 'value) => ('key * 'value) list => ('key * 'value) list"
by (simp add: distinct_map_default)
-(* FIXME: theorems are still used in Multiset; make code certificates available to the user *)
-lemma impl_of_empty: "impl_of empty = []"
-by (simp add: empty_def Alist_inverse)
-
-lemma impl_of_update: "impl_of (update k v xs) = AList.update k v (impl_of xs)"
-by (simp add: update_def Alist_inverse distinct_update)
-
-lemma impl_of_filter:
- "impl_of (filter P xs) = List.filter P (impl_of xs)"
-unfolding filter_def by (simp add: Alist_inverse distinct_map_fst_filter)
-
subsection {* Abstract operation properties *}
(* FIXME: to be completed *)
--- a/src/HOL/Library/Multiset.thy Wed Mar 28 11:17:32 2012 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Mar 28 11:40:12 2012 +0200
@@ -1109,23 +1109,17 @@
using assms
unfolding subtract_entries_raw_def by (induct ys) (auto simp add: distinct_map_entry)
-text {* Operations on alists *}
-
-definition join
-where
- "join f xs ys = DAList.Alist (join_raw f (DAList.impl_of xs) (DAList.impl_of ys))"
+text {* Operations on alists with distinct keys *}
-lemma [code abstract]:
- "DAList.impl_of (join f xs ys) = join_raw f (DAList.impl_of xs) (DAList.impl_of ys)"
-unfolding join_def by (simp add: Alist_inverse distinct_join_raw)
-
-definition subtract_entries
+quotient_definition join :: "('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
where
- "subtract_entries xs ys = DAList.Alist (subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys))"
+ "join" is "join_raw :: ('a \<Rightarrow> 'b \<times> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"
+by (simp add: distinct_join_raw)
-lemma [code abstract]:
- "DAList.impl_of (subtract_entries xs ys) = subtract_entries_raw (DAList.impl_of xs) (DAList.impl_of ys)"
-unfolding subtract_entries_def by (simp add: Alist_inverse distinct_subtract_entries_raw)
+quotient_definition subtract_entries :: "('a, ('b :: minus)) alist \<Rightarrow> ('a, 'b) alist \<Rightarrow> ('a, 'b) alist"
+where
+ "subtract_entries" is "subtract_entries_raw :: ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('a \<times> 'b) list"
+by (simp add: distinct_subtract_entries_raw)
text {* Implementing multisets by means of association lists *}
@@ -1192,7 +1186,7 @@
lemma single_Bag [code]:
"{#x#} = Bag (DAList.update x 1 DAList.empty)"
- by (simp add: multiset_eq_iff alist.Alist_inverse impl_of_update impl_of_empty)
+ by (simp add: multiset_eq_iff alist.Alist_inverse update_code_eqn empty_code_eqn)
lemma union_Bag [code]:
"Bag xs + Bag ys = Bag (join (\<lambda>x (n1, n2). n1 + n2) xs ys)"
@@ -1205,7 +1199,7 @@
lemma filter_Bag [code]:
"Multiset.filter P (Bag xs) = Bag (DAList.filter (P \<circ> fst) xs)"
-by (rule multiset_eqI) (simp add: count_of_filter impl_of_filter)
+by (rule multiset_eqI) (simp add: count_of_filter filter_code_eqn)
lemma mset_less_eq_Bag [code]:
"Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
--- a/src/HOL/Tools/Quotient/quotient_def.ML Wed Mar 28 11:17:32 2012 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Wed Mar 28 11:40:12 2012 +0200
@@ -218,7 +218,7 @@
fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
fun erase_quants ctm' =
case (Thm.term_of ctm') of
- Const ("HOL.eq", _) $ _ $ _ => Conv.all_conv ctm'
+ Const (@{const_name HOL.eq}, _) $ _ $ _ => Conv.all_conv ctm'
| _ => (Conv.binder_conv (K erase_quants) lthy then_conv
Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
in
@@ -234,8 +234,8 @@
fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
in
case (Thm.term_of ctm) of
- Const (@{const_name "fun_rel"}, _) $ _ $ _ =>
- (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
+ Const (@{const_name fun_rel}, _) $ _ $ _ =>
+ (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
| _ => Conv.all_conv ctm
end
@@ -248,7 +248,7 @@
val eq_thm =
(simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
in
- Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
+ Object_Logic.rulify (eq_thm RS Drule.equal_elim_rule2)
end
@@ -283,7 +283,7 @@
|> try HOLogic.dest_Trueprop
in
case lhs_eq of
- SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm)
+ SOME (Const (@{const_name HOL.eq}, _) $ _ $ _) => SOME (@{thm refl} RS thm)
| SOME _ => (case body_type (fastype_of lhs) of
Type (typ_name, _) => ( SOME
(#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))