1.1 --- a/src/HOL/Library/Mapping.thy	Fri Jul 02 16:50:52 2010 +0200
     1.2 +++ b/src/HOL/Library/Mapping.thy	Fri Jul 02 16:50:53 2010 +0200
     1.3 @@ -8,19 +8,36 @@
     1.4  
     1.5  subsection {* Type definition and primitive operations *}
     1.6  
     1.7 -datatype ('a, 'b) mapping = Mapping "'a \<rightharpoonup> 'b"
     1.8 +typedef (open) ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
     1.9 +  morphisms lookup Mapping ..
    1.10 +
    1.11 +lemma lookup_Mapping [simp]:
    1.12 +  "lookup (Mapping f) = f"
    1.13 +  by (rule Mapping_inverse) rule
    1.14 +
    1.15 +lemma Mapping_lookup [simp]:
    1.16 +  "Mapping (lookup m) = m"
    1.17 +  by (fact lookup_inverse)
    1.18 +
    1.19 +declare lookup_inject [simp]
    1.20 +
    1.21 +lemma Mapping_inject [simp]:
    1.22 +  "Mapping f = Mapping g \<longleftrightarrow> f = g"
    1.23 +  by (simp add: Mapping_inject)
    1.24 +
    1.25 +lemma mapping_eqI:
    1.26 +  assumes "lookup m = lookup n"
    1.27 +  shows "m = n"
    1.28 +  using assms by simp
    1.29  
    1.30  definition empty :: "('a, 'b) mapping" where
    1.31    "empty = Mapping (\<lambda>_. None)"
    1.32  
    1.33 -primrec lookup :: "('a, 'b) mapping \<Rightarrow> 'a \<rightharpoonup> 'b" where
    1.34 -  "lookup (Mapping f) = f"
    1.35 +definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
    1.36 +  "update k v m = Mapping ((lookup m)(k \<mapsto> v))"
    1.37  
    1.38 -primrec update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
    1.39 -  "update k v (Mapping f) = Mapping (f (k \<mapsto> v))"
    1.40 -
    1.41 -primrec delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
    1.42 -  "delete k (Mapping f) = Mapping (f (k := None))"
    1.43 +definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
    1.44 +  "delete k m = Mapping ((lookup m)(k := None))"
    1.45  
    1.46  
    1.47  subsection {* Derived operations *}
    1.48 @@ -59,15 +76,6 @@
    1.49  
    1.50  subsection {* Properties *}
    1.51  
    1.52 -lemma lookup_inject [simp]:
    1.53 -  "lookup m = lookup n \<longleftrightarrow> m = n"
    1.54 -  by (cases m, cases n) simp
    1.55 -
    1.56 -lemma mapping_eqI:
    1.57 -  assumes "lookup m = lookup n"
    1.58 -  shows "m = n"
    1.59 -  using assms by simp
    1.60 -
    1.61  lemma keys_is_none_lookup [code_inline]:
    1.62    "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
    1.63    by (auto simp add: keys_def is_none_def)
    1.64 @@ -78,11 +86,11 @@
    1.65  
    1.66  lemma lookup_update [simp]:
    1.67    "lookup (update k v m) = (lookup m) (k \<mapsto> v)"
    1.68 -  by (cases m) simp
    1.69 +  by (simp add: update_def)
    1.70  
    1.71  lemma lookup_delete [simp]:
    1.72    "lookup (delete k m) = (lookup m) (k := None)"
    1.73 -  by (cases m) simp
    1.74 +  by (simp add: delete_def)
    1.75  
    1.76  lemma lookup_map_entry [simp]:
    1.77    "lookup (map_entry k f m) = (lookup m) (k := Option.map f (lookup m k))"
    1.78 @@ -150,11 +158,11 @@
    1.79  
    1.80  lemma is_empty_update [simp]:
    1.81    "\<not> is_empty (update k v m)"
    1.82 -  by (cases m) (simp add: is_empty_empty)
    1.83 +  by (simp add: is_empty_empty update_def)
    1.84  
    1.85  lemma is_empty_delete:
    1.86    "is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}"
    1.87 -  by (cases m) (auto simp add: is_empty_empty keys_def dom_eq_empty_conv [symmetric] simp del: dom_eq_empty_conv)
    1.88 +  by (auto simp add: delete_def is_empty_def keys_def simp del: dom_eq_empty_conv)
    1.89  
    1.90  lemma is_empty_replace [simp]:
    1.91    "is_empty (replace k v m) \<longleftrightarrow> is_empty m"
    1.92 @@ -268,23 +276,18 @@
    1.93    by (simp add: ordered_keys_def)
    1.94  
    1.95  
    1.96 -subsection {* Some technical code lemmas *}
    1.97 +subsection {* Code generator setup *}
    1.98  
    1.99 -lemma [code]:
   1.100 -  "mapping_case f m = f (Mapping.lookup m)"
   1.101 -  by (cases m) simp
   1.102 +instantiation mapping :: (type, type) eq
   1.103 +begin
   1.104  
   1.105 -lemma [code]:
   1.106 -  "mapping_rec f m = f (Mapping.lookup m)"
   1.107 -  by (cases m) simp
   1.108 +definition [code del]:
   1.109 +  "HOL.eq m n \<longleftrightarrow> lookup m = lookup n"
   1.110  
   1.111 -lemma [code]:
   1.112 -  "Nat.size (m :: (_, _) mapping) = 0"
   1.113 -  by (cases m) simp
   1.114 +instance proof
   1.115 +qed (simp add: eq_mapping_def)
   1.116  
   1.117 -lemma [code]:
   1.118 -  "mapping_size f g m = 0"
   1.119 -  by (cases m) simp
   1.120 +end
   1.121  
   1.122  
   1.123  hide_const (open) empty is_empty lookup update delete ordered_keys keys size