equal
deleted
inserted
replaced
260 apply (simp add: subcls1_def2 is_class_def) |
260 apply (simp add: subcls1_def2 is_class_def) |
261 apply auto |
261 apply auto |
262 done |
262 done |
263 |
263 |
264 |
264 |
265 syntax |
265 abbreviation (input) |
266 mtd_mb :: "cname \<times> ty \<times> 'c \<Rightarrow> 'c" |
266 "mtd_mb == snd o snd" |
267 translations |
|
268 "mtd_mb" => "Fun.comp snd snd" |
|
269 |
267 |
270 lemma map_of_map_fst: "\<lbrakk> inj f; |
268 lemma map_of_map_fst: "\<lbrakk> inj f; |
271 \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk> |
269 \<forall>x\<in>set xs. fst (f x) = fst x; \<forall>x\<in>set xs. fst (g x) = fst x \<rbrakk> |
272 \<Longrightarrow> map_of (map g xs) k |
270 \<Longrightarrow> map_of (map g xs) k |
273 = Option.map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)" |
271 = Option.map (\<lambda> e. (snd (g ((inv f) (k, e))))) (map_of (map f xs) k)" |