equal
deleted
inserted
replaced
49 (let ks = map fst xs; ls = map fst ys |
49 (let ks = map fst xs; ls = map fst ys |
50 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))" |
50 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))" |
51 proof - |
51 proof - |
52 have *: "(a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" for a b xs |
52 have *: "(a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" for a b xs |
53 by (auto simp add: image_def intro!: bexI) |
53 by (auto simp add: image_def intro!: bexI) |
54 show ?thesis apply transfer |
54 show ?thesis |
55 by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: *) |
55 apply transfer |
|
56 apply (auto intro!: map_of_eqI) |
|
57 apply (auto dest!: map_of_eq_dom intro: *) |
|
58 done |
56 qed |
59 qed |
57 |
60 |
58 lemma map_values_Mapping [code]: |
61 lemma map_values_Mapping [code]: |
59 "Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f x y)) xs)" |
62 "Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f x y)) xs)" |
60 for f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list" |
63 for f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list" |
70 apply transfer |
73 apply transfer |
71 apply (rule ext) |
74 apply (rule ext) |
72 apply (rule sym) |
75 apply (rule sym) |
73 subgoal for f xs ys x |
76 subgoal for f xs ys x |
74 apply (cases "map_of xs x"; cases "map_of ys x"; simp) |
77 apply (cases "map_of xs x"; cases "map_of ys x"; simp) |
75 apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff |
78 apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff |
76 dest: map_of_SomeD split: option.splits)+ |
79 dest: map_of_SomeD split: option.splits)+ |
77 done |
80 done |
78 done |
81 done |
79 |
82 |
80 lemma combine_code [code]: |
83 lemma combine_code [code]: |
81 "Mapping.combine f (Mapping xs) (Mapping ys) = |
84 "Mapping.combine f (Mapping xs) (Mapping ys) = |
84 apply transfer |
87 apply transfer |
85 apply (rule ext) |
88 apply (rule ext) |
86 apply (rule sym) |
89 apply (rule sym) |
87 subgoal for f xs ys x |
90 subgoal for f xs ys x |
88 apply (cases "map_of xs x"; cases "map_of ys x"; simp) |
91 apply (cases "map_of xs x"; cases "map_of ys x"; simp) |
89 apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff |
92 apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff |
90 dest: map_of_SomeD split: option.splits)+ |
93 dest: map_of_SomeD split: option.splits)+ |
91 done |
94 done |
92 done |
95 done |
93 |
96 |
94 lemma map_of_filter_distinct: (* TODO: move? *) |
97 lemma map_of_filter_distinct: (* TODO: move? *) |
95 assumes "distinct (map fst xs)" |
98 assumes "distinct (map fst xs)" |
104 lemma filter_Mapping [code]: |
107 lemma filter_Mapping [code]: |
105 "Mapping.filter P (Mapping xs) = Mapping (filter (\<lambda>(k,v). P k v) (AList.clearjunk xs))" |
108 "Mapping.filter P (Mapping xs) = Mapping (filter (\<lambda>(k,v). P k v) (AList.clearjunk xs))" |
106 apply transfer |
109 apply transfer |
107 apply (rule ext) |
110 apply (rule ext) |
108 apply (subst map_of_filter_distinct) |
111 apply (subst map_of_filter_distinct) |
109 apply (simp_all add: map_of_clearjunk split: option.split) |
112 apply (simp_all add: map_of_clearjunk split: option.split) |
110 done |
113 done |
111 |
114 |
112 lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" |
115 lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" |
113 by (fact equal_refl) |
116 by (fact equal_refl) |
114 |
117 |