Add FINTER to finite_mapTheory and develop cv_trans for finite maps

Manual/Description/theories.smd

@@ -4696,10 +4696,12 @@ alternate recursive presentation.
    ##thm FDIFF_FUPDATE
 ```
 
-There is one last, even more specialised, instance of `DRESTRICT` called `FMINUS`:
+There are two, even more specialised, instances of `DRESTRICT`
+called `FMINUS` and `FINTER`:
 
 ```repl
    ##thm FMINUS_def
+   ##thm FINTER_def
 ```
 
 **Union and sub-maps.**

src/finite_maps/finite_mapScript.sml

@@ -3569,6 +3569,37 @@ Definition FMINUS_def:
   FMINUS fm1 fm2 = FDIFF fm1 (FDOM fm2)
 End
 
+Theorem FLOOKUP_FMINUS:
+  FLOOKUP (FMINUS f1 f2) k =
+  case FLOOKUP f2 k of
+    NONE => FLOOKUP f1 k
+  | SOME v => NONE
+Proof
+  rw[FMINUS_def, FDIFF_def, FLOOKUP_DRESTRICT] >>
+  Cases_on ‘FLOOKUP f2 k’ >> gvs[FLOOKUP_DEF]
+QED
+
+(* ----------------------------------------------------------------------
+    FINTER : ('a |-> 'b) -> ('a |-> 'c) -> ('a |-> 'b)
+
+    Keeps the entries of the first map whose keys are in the domain of
+    the second map.
+  ----------------------------------------------------------------------- *)
+
+Definition FINTER_def:
+  FINTER f1 f2 = DRESTRICT f1 (FDOM f2)
+End
+
+Theorem FLOOKUP_FINTER:
+  FLOOKUP (FINTER f1 f2) k =
+  case FLOOKUP f2 k of
+    NONE => NONE
+  | SOME v => FLOOKUP f1 k
+Proof
+  rw[FINTER_def, FLOOKUP_DRESTRICT] >>
+  Cases_on ‘FLOOKUP f2 k’ >> gvs[FLOOKUP_DEF]
+QED
+
 
 Theorem FMERGE_WITH_KEY_FUNION_ALT:
   FMERGE_WITH_KEY f (FUNION m1 m2) m3 =
@@ -3920,7 +3951,7 @@ QED
 Theorem FLOOKUP_SIMP =
   [FLOOKUP_EMPTY, FLOOKUP_UPDATE, FDIFF_def, FLOOKUP_FMAP_MAP2,
    FLOOKUP_DRESTRICT, FLOOKUP_FDIFF, FLOOKUP_FUNION, FLOOKUP_FUN_FMAP,
-   FLOOKUP_FMAP_MAP2, FLOOKUP_FMERGE]
+   FLOOKUP_FMAP_MAP2, FLOOKUP_FMERGE, FLOOKUP_FMINUS, FLOOKUP_FINTER]
   |> map SPEC_ALL |> LIST_CONJ;
 
 (*---------------------------------------------------------------------------*)