(*Generated by Lem from map.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_basic_classesTheory lem_functionTheory lem_maybeTheory lem_listTheory lem_tupleTheory lem_setTheory lem_numTheory finite_mapTheory finite_mapLib;

val _ = numLib.prefer_num();



val _ = new_theory "lem_map"



(*open import Bool Basic_classes Function Maybe List Tuple Set Num*)
(*open import {hol} `finite_mapTheory` `finite_mapLib`*)

(*type map 'k 'v*)



(* -------------------------------------------------------------------------- *)
(* Map equality.                                                              *)
(* -------------------------------------------------------------------------- *)

(*val mapEqual : forall 'k 'v. Eq 'k, Eq 'v => map 'k 'v -> map 'k 'v -> bool*)
(*val mapEqualBy : forall 'k 'v. ('k -> 'k -> bool) -> ('v -> 'v -> bool) -> map 'k 'v -> map 'k 'v -> bool*)


(* -------------------------------------------------------------------------- *)
(* Map type class                                                             *)
(* -------------------------------------------------------------------------- *)

(*class ( MapKeyType 'a )
  val {ocaml;coq} mapKeyCompare : 'a -> 'a -> ordering
end*)

(* -------------------------------------------------------------------------- *)
(* Empty maps                                                                 *)
(* -------------------------------------------------------------------------- *)

(*val empty : forall 'k 'v. MapKeyType 'k => map 'k 'v*)
(*val emptyBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v*)


(* -------------------------------------------------------------------------- *)
(* Insertion                                                                  *)
(* -------------------------------------------------------------------------- *)

(*val insert    : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v -> map 'k 'v*)


(* -------------------------------------------------------------------------- *)
(* Singleton                                                                  *)
(* -------------------------------------------------------------------------- *)

(*val singleton : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v*)



(* -------------------------------------------------------------------------- *)
(* Emptyness check                                                            *)
(* -------------------------------------------------------------------------- *)

(*val null  : forall 'k 'v. MapKeyType 'k, Eq 'k, Eq 'v => map 'k 'v -> bool*)


(* -------------------------------------------------------------------------- *)
(* lookup                                                                     *)
(* -------------------------------------------------------------------------- *)

(*val lookupBy : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> maybe 'v*)

(*val lookup          : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> maybe 'v*)

(* -------------------------------------------------------------------------- *)
(* findWithDefault                                                            *)
(* -------------------------------------------------------------------------- *)

(*val findWithDefault : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v -> 'v*)

(* -------------------------------------------------------------------------- *)
(* from lists                                                                 *)
(* -------------------------------------------------------------------------- *)

(*val fromList  : forall 'k 'v. MapKeyType 'k => list ('k * 'v) -> map 'k 'v*)
(*let fromList l=  foldl (fun m (k,v) -> insert k v m) empty l*)


(* -------------------------------------------------------------------------- *)
(* to sets / domain / range                                                   *)
(* -------------------------------------------------------------------------- *)

(*val toSet : forall 'k 'v. MapKeyType 'k, SetType 'k, SetType 'v => map 'k 'v -> set ('k * 'v)*) 
(*val toSetBy : forall 'k 'v. (('k * 'v) -> ('k * 'v) -> ordering) -> map 'k 'v -> set ('k * 'v)*)


(*val domainBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v -> set 'k*)
(*val domain : forall 'k 'v. MapKeyType 'k, SetType 'k => map 'k 'v -> set 'k*)


(*val range : forall 'k 'v. MapKeyType 'k, SetType 'v => map 'k 'v -> set 'v*)
(*val rangeBy : forall 'k 'v. ('v -> 'v -> ordering) -> map 'k 'v -> set 'v*)


(* -------------------------------------------------------------------------- *)
(* member                                                                     *)
(* -------------------------------------------------------------------------- *)

(*val member          : forall 'k 'v. MapKeyType 'k, SetType 'k, Eq 'k => 'k -> map 'k 'v -> bool*)

(*val notMember       : forall 'k 'v. MapKeyType 'k, SetType 'k, Eq 'k => 'k -> map 'k 'v -> bool*)

(* -------------------------------------------------------------------------- *)
(* Quantification                                                             *)
(* -------------------------------------------------------------------------- *)

(*val any : forall 'k 'v. MapKeyType 'k, Eq 'v => ('k -> 'v -> bool) -> map 'k 'v -> bool*) 
(*val all : forall 'k 'v. MapKeyType 'k, Eq 'v => ('k -> 'v -> bool) -> map 'k 'v -> bool*) 

(*let all P m=  (forall k v. (P k v && ((Instance_Basic_classes_Eq_Maybe_maybe.=) (lookup k m) (Just v))))*)


(* -------------------------------------------------------------------------- *)
(* Set-like operations.                                                       *)
(* -------------------------------------------------------------------------- *)
(*val deleteBy         : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> map 'k 'v*)
(*val delete           : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> map 'k 'v*)
(*val deleteSwap      : forall 'k 'v. MapKeyType 'k => map 'k 'v -> 'k -> map 'k 'v*)

(*val union          : forall 'k 'v. MapKeyType 'k => map 'k 'v -> map 'k 'v -> map 'k 'v*)

(*val unions           : forall 'k 'v. MapKeyType 'k => list (map 'k 'v) -> map 'k 'v*)


(* -------------------------------------------------------------------------- *)
(* Maps (in the functor sense).                                               *)
(* -------------------------------------------------------------------------- *)

(*val map             : forall 'k 'v 'w. MapKeyType 'k => ('v -> 'w) -> map 'k 'v -> map 'k 'w*)

(*val mapi : forall 'k 'v 'w. MapKeyType 'k => ('k -> 'v -> 'w) -> map 'k 'v -> map 'k 'w*)

(* -------------------------------------------------------------------------- *)
(* Cardinality                                                                *)
(* -------------------------------------------------------------------------- *)
(*val size  : forall 'k 'v. MapKeyType 'k, SetType 'k => map 'k 'v -> nat*)

(* instance of SetType *)
val _ = Define `
 ((map_setElemCompare:(('d#'c)set ->('b#'a)set -> 'e) ->('d,'c)fmap ->('b,'a)fmap -> 'e) cmp x y=
   (cmp (FMAP_TO_SET x) (FMAP_TO_SET y)))`;

val _ = export_theory()