62 show ?thesis apply transfer |
62 show ?thesis apply transfer |
63 by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux) |
63 by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux) |
64 qed |
64 qed |
65 |
65 |
66 lemma map_values_Mapping [code]: |
66 lemma map_values_Mapping [code]: |
67 fixes f :: "'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list" |
67 fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list" |
68 shows "Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f y)) xs)" |
68 shows "Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f x y)) xs)" |
69 proof (transfer, rule ext, goal_cases) |
69 proof (transfer, rule ext, goal_cases) |
70 case (1 f xs x) |
70 case (1 f xs x) |
71 thus ?case by (induction xs) auto |
71 thus ?case by (induction xs) auto |
|
72 qed |
|
73 |
|
74 lemma combine_with_key_code [code]: |
|
75 "Mapping.combine_with_key f (Mapping xs) (Mapping ys) = |
|
76 Mapping.tabulate (remdups (map fst xs @ map fst ys)) |
|
77 (\<lambda>x. the (combine_options (f x) (map_of xs x) (map_of ys x)))" |
|
78 proof (transfer, rule ext, rule sym, goal_cases) |
|
79 case (1 f xs ys x) |
|
80 show ?case |
|
81 by (cases "map_of xs x"; cases "map_of ys x"; simp) |
|
82 (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff |
|
83 dest: map_of_SomeD split: option.splits)+ |
72 qed |
84 qed |
73 |
85 |
74 lemma combine_code [code]: |
86 lemma combine_code [code]: |
75 "Mapping.combine f (Mapping xs) (Mapping ys) = |
87 "Mapping.combine f (Mapping xs) (Mapping ys) = |
76 Mapping.tabulate (remdups (map fst xs @ map fst ys)) |
88 Mapping.tabulate (remdups (map fst xs @ map fst ys)) |
77 (\<lambda>x. the (combine_options f (map_of xs x) (map_of ys x)))" |
89 (\<lambda>x. the (combine_options f (map_of xs x) (map_of ys x)))" |
78 proof (transfer, rule ext, rule sym, goal_cases) |
90 proof (transfer, rule ext, rule sym, goal_cases) |
79 case (1 f xs ys x) |
91 case (1 f xs ys x) |
80 show ?case |
92 show ?case |
81 by (cases "map_of xs x"; cases "map_of ys x"; simp) |
93 by (cases "map_of xs x"; cases "map_of ys x"; simp) |
82 (force simp: map_of_eq_None_iff combine_options_altdef option.the_def o_def image_iff |
94 (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff |
83 dest: map_of_SomeD split: option.splits)+ |
95 dest: map_of_SomeD split: option.splits)+ |
84 qed |
96 qed |
85 |
97 |
86 (* TODO: Move? *) |
98 (* TODO: Move? *) |
87 lemma map_of_filter_distinct: |
99 lemma map_of_filter_distinct: |