# HG changeset patch
# User haftmann
# Date 1270997465 -7200
# Node ID 1028cf8c0d1bcde2917ffd59ce5b76f022c9f1a1
# Parent  bae883012af3a4b25b7a5fbddcce476c70c77aee
constructor Mapping replaces AList

diff -r bae883012af3 -r 1028cf8c0d1b src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Fri Apr 09 13:35:54 2010 +0200
+++ b/src/HOL/Library/AssocList.thy	Sun Apr 11 16:51:05 2010 +0200
@@ -659,49 +659,49 @@
 
 subsection {* Implementation of mappings *}
 
-definition AList :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
-  "AList xs = Mapping (map_of xs)"
+definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
+  "Mapping xs = Mapping.Mapping (map_of xs)"
 
-code_datatype AList
+code_datatype Mapping
 
-lemma lookup_AList [simp, code]:
-  "Mapping.lookup (AList xs) = map_of xs"
-  by (simp add: AList_def)
+lemma lookup_Mapping [simp, code]:
+  "Mapping.lookup (Mapping xs) = map_of xs"
+  by (simp add: Mapping_def)
 
-lemma empty_AList [code]:
-  "Mapping.empty = AList []"
+lemma empty_Mapping [code]:
+  "Mapping.empty = Mapping []"
   by (rule mapping_eqI) simp
 
-lemma is_empty_AList [code]:
-  "Mapping.is_empty (AList xs) \<longleftrightarrow> null xs"
+lemma is_empty_Mapping [code]:
+  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> null xs"
   by (cases xs) (simp_all add: is_empty_def)
 
-lemma update_AList [code]:
-  "Mapping.update k v (AList xs) = AList (update k v xs)"
+lemma update_Mapping [code]:
+  "Mapping.update k v (Mapping xs) = Mapping (update k v xs)"
   by (rule mapping_eqI) (simp add: update_conv')
 
-lemma delete_AList [code]:
-  "Mapping.delete k (AList xs) = AList (delete k xs)"
+lemma delete_Mapping [code]:
+  "Mapping.delete k (Mapping xs) = Mapping (delete k xs)"
   by (rule mapping_eqI) (simp add: delete_conv')
 
-lemma keys_AList [code]:
-  "Mapping.keys (AList xs) = set (map fst xs)"
+lemma keys_Mapping [code]:
+  "Mapping.keys (Mapping xs) = set (map fst xs)"
   by (simp add: keys_def dom_map_of_conv_image_fst)
 
-lemma ordered_keys_AList [code]:
-  "Mapping.ordered_keys (AList xs) = sort (remdups (map fst xs))"
-  by (simp only: ordered_keys_def keys_AList sorted_list_of_set_sort_remdups)
+lemma ordered_keys_Mapping [code]:
+  "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
+  by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups)
 
-lemma size_AList [code]:
-  "Mapping.size (AList xs) = length (remdups (map fst xs))"
+lemma size_Mapping [code]:
+  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
   by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
 
-lemma tabulate_AList [code]:
-  "Mapping.tabulate ks f = AList (map (\<lambda>k. (k, f k)) ks)"
+lemma tabulate_Mapping [code]:
+  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
   by (rule mapping_eqI) (simp add: map_of_map_restrict)
 
-lemma bulkload_AList [code]:
-  "Mapping.bulkload vs = AList (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
+lemma bulkload_Mapping [code]:
+  "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
   by (rule mapping_eqI) (simp add: map_of_map_restrict expand_fun_eq)
 
 end
diff -r bae883012af3 -r 1028cf8c0d1b src/HOL/ex/Execute_Choice.thy
--- a/src/HOL/ex/Execute_Choice.thy	Fri Apr 09 13:35:54 2010 +0200
+++ b/src/HOL/ex/Execute_Choice.thy	Sun Apr 11 16:51:05 2010 +0200
@@ -58,15 +58,15 @@
 
 text {*
   Given @{text valuesum_rec} as initial description, we stepwise refine it to something executable;
-  first, we formally insert the constructor @{term AList} and split the one equation into two,
+  first, we formally insert the constructor @{term Mapping} and split the one equation into two,
   where the second one provides the necessary context:
 *}
 
-lemma valuesum_rec_AList:
-  shows [code]: "valuesum (AList []) = 0"
-  and "valuesum (AList (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (AList (x # xs))) in
-    the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
-  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_AList)
+lemma valuesum_rec_Mapping:
+  shows [code]: "valuesum (Mapping []) = 0"
+  and "valuesum (Mapping (x # xs)) = (let l = (SOME l. l \<in> Mapping.keys (Mapping (x # xs))) in
+    the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
+  by (simp_all add: valuesum_rec finite_dom_map_of is_empty_Mapping)
 
 text {*
   As a side effect the precondition disappears (but note this has nothing to do with choice!).
@@ -76,27 +76,27 @@
 *}
 
 lemma valuesum_rec_exec [code]:
-  "valuesum (AList (x # xs)) = (let l = fst (hd (x # xs)) in
-    the (Mapping.lookup (AList (x # xs)) l) + valuesum (Mapping.delete l (AList (x # xs))))"
+  "valuesum (Mapping (x # xs)) = (let l = fst (hd (x # xs)) in
+    the (Mapping.lookup (Mapping (x # xs)) l) + valuesum (Mapping.delete l (Mapping (x # xs))))"
 proof -
-  let ?M = "AList (x # xs)"
+  let ?M = "Mapping (x # xs)"
   let ?l1 = "(SOME l. l \<in> Mapping.keys ?M)"
   let ?l2 = "fst (hd (x # xs))"
-  have "finite (Mapping.keys ?M)" by (simp add: keys_AList)
+  have "finite (Mapping.keys ?M)" by (simp add: keys_Mapping)
   moreover have "?l1 \<in> Mapping.keys ?M"
-    by (rule someI) (auto simp add: keys_AList)
+    by (rule someI) (auto simp add: keys_Mapping)
   moreover have "?l2 \<in> Mapping.keys ?M"
-    by (simp add: keys_AList)
+    by (simp add: keys_Mapping)
   ultimately have "the (Mapping.lookup ?M ?l1) + valuesum (Mapping.delete ?l1 ?M) =
     the (Mapping.lookup ?M ?l2) + valuesum (Mapping.delete ?l2 ?M)"
     by (rule valuesum_choice)
-  then show ?thesis by (simp add: valuesum_rec_AList)
+  then show ?thesis by (simp add: valuesum_rec_Mapping)
 qed
   
 text {*
   See how it works:
 *}
 
-value "valuesum (AList [(''abc'', (42::int)), (''def'', 1705)])"
+value "valuesum (Mapping [(''abc'', (42::int)), (''def'', 1705)])"
 
 end