# HG changeset patch # User bulwahn # Date 1332927612 -7200 # Node ID d81ee6c5209a8118d3de3c4e568990fac1957cfd # Parent b351ad77eb7824ee8f3ccc3ff7375b4efac47836# Parent b9b2e183e94d058a94db24633adbf6577a33ea33 merged diff -r b9b2e183e94d -r d81ee6c5209a doc-src/IsarImplementation/Thy/ML.thy --- 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 diff -r b9b2e183e94d -r d81ee6c5209a src/HOL/Library/DAList.thy --- 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 *) diff -r b9b2e183e94d -r d81ee6c5209a src/HOL/Library/Multiset.thy --- 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 \ 'b \ 'b \ 'b) \ ('a, 'b) alist \ ('a, 'b) alist \ ('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 \ 'b \ 'b \ 'b) \ ('a \ 'b) list \ ('a \ 'b) list \ ('a \ '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 \ ('a, 'b) alist \ ('a, 'b) alist" +where + "subtract_entries" is "subtract_entries_raw :: ('a \ 'b) list \ ('a \ 'b) list \ ('a \ '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 (\x (n1, n2). n1 + n2) xs ys)" @@ -1205,7 +1199,7 @@ lemma filter_Bag [code]: "Multiset.filter P (Bag xs) = Bag (DAList.filter (P \ 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 \ A \ (\(x, n) \ set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \ count A x)" diff -r b9b2e183e94d -r d81ee6c5209a src/HOL/Tools/Quotient/quotient_def.ML --- 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))