merged
authorbulwahn
Wed, 28 Mar 2012 11:40:12 +0200
changeset 47182 d81ee6c5209a
parent 47181 b351ad77eb78 (diff)
parent 47174 b9b2e183e94d (current diff)
child 47183 f760e15343bc
merged
--- 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))