src/HOL/Library/RBT_Mapping.thy
changeset 51438 a614e456870b
parent 51379 6dd83e007f56
child 56019 682bba24e474
equal deleted inserted replaced
51437:8739f8abbecb 51438:a614e456870b
    37   "Mapping.delete k (Mapping t) = Mapping (delete k t)"
    37   "Mapping.delete k (Mapping t) = Mapping (delete k t)"
    38   by (transfer fixing: t) simp
    38   by (transfer fixing: t) simp
    39 
    39 
    40 lemma map_entry_Mapping [code]:
    40 lemma map_entry_Mapping [code]:
    41   "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
    41   "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)"
    42 by (transfer fixing: t, case_tac "lookup t k") auto
    42   apply (transfer fixing: t) by (case_tac "lookup t k") auto
    43 
    43 
    44 lemma keys_Mapping [code]:
    44 lemma keys_Mapping [code]:
    45   "Mapping.keys (Mapping t) = set (keys t)"
    45   "Mapping.keys (Mapping t) = set (keys t)"
    46 by (transfer fixing: t) (simp add: lookup_keys)
    46 by (transfer fixing: t) (simp add: lookup_keys)
    47 
    47