author  wenzelm 
Sun, 03 Aug 2014 17:38:59 +0200  
changeset 57850  34382a1f37d6 
parent 51161  6ed12ae3b3e1 
child 58881  b9556a055632 
permissions  rwrr 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

1 
(* Title: HOL/Library/AList_Mapping.thy 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

2 
Author: Florian Haftmann, TU Muenchen 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

3 
*) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

4 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

5 
header {* Implementation of mappings with Association Lists *} 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

6 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

7 
theory AList_Mapping 
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46171
diff
changeset

8 
imports AList Mapping 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

9 
begin 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

10 

49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

11 
lift_definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" is map_of . 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

12 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

13 
code_datatype Mapping 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

14 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

15 
lemma lookup_Mapping [simp, code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

16 
"Mapping.lookup (Mapping xs) = map_of xs" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

17 
by transfer rule 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

18 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

19 
lemma keys_Mapping [simp, code]: 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

20 
"Mapping.keys (Mapping xs) = set (map fst xs)" 
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

21 
by transfer (simp add: dom_map_of_conv_image_fst) 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

22 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

23 
lemma empty_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

24 
"Mapping.empty = Mapping []" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

25 
by transfer simp 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

26 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

27 
lemma is_empty_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

28 
"Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

29 
by (case_tac xs) (simp_all add: is_empty_def null_def) 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

30 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

31 
lemma update_Mapping [code]: 
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46171
diff
changeset

32 
"Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

33 
by transfer (simp add: update_conv') 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

34 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

35 
lemma delete_Mapping [code]: 
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46171
diff
changeset

36 
"Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

37 
by transfer (simp add: delete_conv') 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

38 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

39 
lemma ordered_keys_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

40 
"Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

41 
by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

42 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

43 
lemma size_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

44 
"Mapping.size (Mapping xs) = length (remdups (map fst xs))" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

45 
by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

46 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

47 
lemma tabulate_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

48 
"Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

49 
by transfer (simp add: map_of_map_restrict) 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

50 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

51 
lemma bulkload_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

52 
"Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])" 
49929
70300f1b6835
update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer
kuncar
parents:
46238
diff
changeset

53 
by transfer (simp add: map_of_map_restrict fun_eq_iff) 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

54 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

55 
lemma equal_Mapping [code]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

56 
"HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow> 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

57 
(let ks = map fst xs; ls = map fst ys 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

58 
in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

59 
proof  
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

60 
have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

61 
by (auto simp add: image_def intro!: bexI) 
51161
6ed12ae3b3e1
attempt to reestablish conventions which theories are loaded into the grand unified library theory;
haftmann
parents:
49929
diff
changeset

62 
show ?thesis apply transfer 
57850  63 
by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux) 
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

64 
qed 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

65 

787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

66 
lemma [code nbe]: 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

67 
"HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

68 
by (fact equal_refl) 
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
diff
changeset

69 

44913  70 
end 