1 files changed, 82 insertions, 0 deletions
diff --git a/snapshots/isabelle/lib/lem/Lem_map_extra.thy b/snapshots/isabelle/lib/lem/Lem_map_extra.thy
new file mode 100644
index 00000000..4117fe81
--- /dev/null
+++ b/snapshots/isabelle/lib/lem/Lem_map_extra.thy
@@ -0,0 +1,82 @@
+chapter \<open>Generated by Lem from map_extra.lem.\<close>
+
+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 \<Rightarrow> 'v)\<Rightarrow> 'k set \<Rightarrow>('k,'v)Map.map "  where 
+     " fromSet f s = ( Finite_Set.fold (\<lambda> 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 \<Rightarrow> 'v \<Rightarrow> 'r \<Rightarrow> 'r)\<Rightarrow>('k,'v)Map.map \<Rightarrow> 'r \<Rightarrow> 'r "  where 
+     " fold f m v = ( Finite_Set.fold ( \<lambda>x .  
+  (case  x of (k, v) => \<lambda> 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 \<Rightarrow> 'b \<Rightarrow> 'c option)\<Rightarrow>('a,'b)Map.map \<Rightarrow>('a,'c)Map.map "  where 
+     " option_map f m = (
+  List.foldl
+    (\<lambda> m' .  \<lambda>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