src/HOL/Library/AList_Mapping.thy
changeset 49929 70300f1b6835
parent 46238 9ace9e5b79be
child 51161 6ed12ae3b3e1
     1.1 --- a/src/HOL/Library/AList_Mapping.thy	Thu Oct 18 15:52:32 2012 +0200
     1.2 +++ b/src/HOL/Library/AList_Mapping.thy	Thu Oct 18 15:52:33 2012 +0200
     1.3 @@ -8,34 +8,33 @@
     1.4  imports AList Mapping
     1.5  begin
     1.6  
     1.7 -definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" where
     1.8 -  "Mapping xs = Mapping.Mapping (map_of xs)"
     1.9 +lift_definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" is map_of .
    1.10  
    1.11  code_datatype Mapping
    1.12  
    1.13  lemma lookup_Mapping [simp, code]:
    1.14    "Mapping.lookup (Mapping xs) = map_of xs"
    1.15 -  by (simp add: Mapping_def)
    1.16 +  by transfer rule
    1.17  
    1.18  lemma keys_Mapping [simp, code]:
    1.19 -  "Mapping.keys (Mapping xs) = set (map fst xs)"
    1.20 -  by (simp add: keys_def dom_map_of_conv_image_fst)
    1.21 +  "Mapping.keys (Mapping xs) = set (map fst xs)" 
    1.22 +  by transfer (simp add: dom_map_of_conv_image_fst)
    1.23  
    1.24  lemma empty_Mapping [code]:
    1.25    "Mapping.empty = Mapping []"
    1.26 -  by (rule mapping_eqI) simp
    1.27 +  by transfer simp
    1.28  
    1.29  lemma is_empty_Mapping [code]:
    1.30    "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
    1.31 -  by (cases xs) (simp_all add: is_empty_def null_def)
    1.32 +  by (case_tac xs) (simp_all add: is_empty_def null_def)
    1.33  
    1.34  lemma update_Mapping [code]:
    1.35    "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
    1.36 -  by (rule mapping_eqI) (simp add: update_conv')
    1.37 +  by transfer (simp add: update_conv')
    1.38  
    1.39  lemma delete_Mapping [code]:
    1.40    "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
    1.41 -  by (rule mapping_eqI) (simp add: delete_conv')
    1.42 +  by transfer (simp add: delete_conv')
    1.43  
    1.44  lemma ordered_keys_Mapping [code]:
    1.45    "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
    1.46 @@ -47,11 +46,11 @@
    1.47  
    1.48  lemma tabulate_Mapping [code]:
    1.49    "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
    1.50 -  by (rule mapping_eqI) (simp add: map_of_map_restrict)
    1.51 +  by transfer (simp add: map_of_map_restrict)
    1.52  
    1.53  lemma bulkload_Mapping [code]:
    1.54    "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
    1.55 -  by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
    1.56 +  by transfer (simp add: map_of_map_restrict fun_eq_iff)
    1.57  
    1.58  lemma equal_Mapping [code]:
    1.59    "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
    1.60 @@ -60,9 +59,8 @@
    1.61  proof -
    1.62    have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
    1.63      by (auto simp add: image_def intro!: bexI)
    1.64 -  show ?thesis
    1.65 -    by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
    1.66 -      (auto dest!: map_of_eq_dom intro: aux)
    1.67 +  show ?thesis apply transfer 
    1.68 +  by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
    1.69  qed
    1.70  
    1.71  lemma [code nbe]: