equal
deleted
inserted
replaced
220 table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None" |
220 table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None" |
221 apply (induct t) |
221 apply (induct t) |
222 apply auto |
222 apply auto |
223 done |
223 done |
224 |
224 |
225 lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard] |
225 lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI] |
226 |
226 |
227 lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow> |
227 lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow> |
228 table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)" |
228 table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)" |
229 apply (induct_tac "t") |
229 apply (induct_tac "t") |
230 apply auto |
230 apply auto |