1 files changed, 72 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_map_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_map_extraScript.sml
new file mode 100644
index 00000000..57a258f8
--- /dev/null
+++ b/snapshots/hol4/lem/hol-lib/lem_map_extraScript.sml
@@ -0,0 +1,72 @@
+(*Generated by Lem from map_extra.lem.*)
+open HolKernel Parse boolLib bossLib;
+open lem_boolTheory lem_basic_classesTheory lem_functionTheory lem_assert_extraTheory lem_maybeTheory lem_listTheory lem_numTheory lem_setTheory lem_mapTheory;
+
+val _ = numLib.prefer_num();
+
+
+
+val _ = new_theory "lem_map_extra"
+
+
+
+(*open import Bool Basic_classes Function Assert_extra Maybe List Num Set Map*)
+
+(* -------------------------------------------------------------------------- *)
+(* find                                                                       *)
+(* -------------------------------------------------------------------------- *)
+
+(*val find : forall 'k 'v. MapKeyType 'k => 'k -> Map.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.map 'k 'v*)
+(*let fromSet f s=  Set_helpers.fold (fun k m -> Map.insert k (f k) m) s Map.empty*)
+
+(*
+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.map 'k 'v -> 'r -> 'r*)
+val _ = Define `
+ ((fold:('k -> 'v -> 'r -> 'r) ->('k,'v)fmap -> 'r -> 'r) f m v=  (ITSET (\ (k, v) r .  f k v r) (FMAP_TO_SET m) v))`;
+
+
+(*
+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.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.maybe 'c) -> Map.map 'a 'b -> Map.map 'a 'c*)
+(* OLD: TODO: mapMaybe depends on toList that is not defined for hol and isabelle *)
+val _ = Define `
+ ((option_map:('a -> 'b -> 'c option) ->('a,'b)fmap ->('a,'c)fmap) f m=  
+ (FOLDL
+    (\ m' (k, v) . 
+      (case f k v of
+          NONE => m'
+        | SOME v' =>m' |+ (k, v')
+      ))
+    FEMPTY
+    (MAP_TO_LIST m)))`;
+
+
+val _ = export_theory()
+