Theory Lem_map_extra

chapter ‹Generated by Lem from ‹map_extra.lem›.›

theory "Lem_map_extra" 

imports
  Main
  "Lem_bool"
  "Lem_basic_classes"
  "Lem_function"
  "Lem_assert_extra"
  "Lem_maybe"
  "Lem_list"
  "Lem_num"
  "Lem_set"
  "Lem_map"

begin 



― ‹‹open import Bool Basic_classes Function Assert_extra Maybe List Num Set Map››

― ‹‹ -------------------------------------------------------------------------- ››
― ‹‹ find                                                                       ››
― ‹‹ -------------------------------------------------------------------------- ››

― ‹‹val find : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> 'v››
― ‹‹let find k m=  match (lookup k m) with Just x -> x | Nothing -> failwith "Map_extra.find" end››



― ‹‹ -------------------------------------------------------------------------- ››
― ‹‹ from sets / domain / range                                                 ››
― ‹‹ -------------------------------------------------------------------------- ››


― ‹‹val fromSet : forall 'k 'v. MapKeyType 'k => ('k -> 'v) -> set 'k -> map 'k 'v››
definition fromSet  :: "('k ⇒ 'v)⇒ 'k set ⇒('k,'v)Map.map "  where 
     " fromSet f s = ( Finite_Set.fold (λ k m .  map_update k (f k) m) Map.empty s )"


― ‹‹
assert fromSet_0: (fromSet succ (Set.empty : set nat) = Map.empty)
assert fromSet_1: (fromSet succ {(2:nat); 3; 4}) = Map.fromList [(2,3); (3, 4); (4, 5)]
››

― ‹‹ -------------------------------------------------------------------------- ››
― ‹‹ fold                                                                       ››
― ‹‹ -------------------------------------------------------------------------- ››

― ‹‹val fold : forall 'k 'v 'r. MapKeyType 'k, SetType 'k, SetType 'v => ('k -> 'v -> 'r -> 'r) -> map 'k 'v -> 'r -> 'r››
definition fold  :: "('k ⇒ 'v ⇒ 'r ⇒ 'r)⇒('k,'v)Map.map ⇒ 'r ⇒ 'r "  where 
     " fold f m v = ( Finite_Set.fold ( λx .  
  (case  x of (k, v) => λ r .  f k v r )) v (map_to_set m))"


― ‹‹
assert fold_1: (fold (fun k v a -> (a+k)) (Map.fromList [((2:nat),(3:nat)); (3, 4); (4, 5)]) 0 = 9)
assert fold_2: (fold (fun k v a -> (a+v)) (Map.fromList [((2:nat),(3:nat)); (3, 4); (4, 5)]) 0 = 12)
››

― ‹‹val toList: forall 'k 'v. MapKeyType 'k => map 'k 'v -> list ('k * 'v)››
― ‹‹ declare compile_message toList = "Map_extra.toList is only defined for the ocaml, isabelle and coq backend" ››

― ‹‹ more 'map' functions ››

― ‹‹ TODO: this function is in map_extra rather than map just for implementation reasons ››
― ‹‹val mapMaybe : forall 'a 'b 'c. MapKeyType 'a => ('a -> 'b -> maybe 'c) -> map 'a 'b -> map 'a 'c››
― ‹‹ OLD: TODO: mapMaybe depends on toList that is not defined for hol and isabelle ››
definition option_map  :: "('a ⇒ 'b ⇒ 'c option)⇒('a,'b)Map.map ⇒('a,'c)Map.map "  where 
     " option_map f m = (
  List.foldl
    (λ m' .  λx .  
  (case  x of
      (k, v) =>
  (case  f k v of   None => m' | Some v' => map_update k v' m' )
  ))
    Map.empty
    (list_of_set (LemExtraDefs.map_to_set m)))"


end