Add Functions!Pointwise

Adds Github issue #96
#96

[Feature]

modules/Functions.tla

@@ -52,6 +52,16 @@ RestrictValues(f, Test(_)) ==
 (***************************************************************************)
 Range(f) == { f[x] : x \in DOMAIN f }
 
+(***************************************************************************)
+(* Assuming DOMAIN f \subseteq DOMAIN g, apply the binary operation T to   *)
+(* the corresponding elements of the two functions f and g.                *)
+(*                                                                         *)
+(* Example:                                                                *)
+(*   LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2)                           *)
+(*       g == ("a" :> 1 @@ "b" :> 1 @@ "c" :> 3)                           *)
+(*   IN Pointwise(f,g,+) = ("a" :> 1 @@ "b" :> 2 @@ "c" :> 5 )             *)
+(***************************************************************************)
+Pointwise(f, g, T(_,_)) == [ e \in DOMAIN f |-> T(f[e], g[e]) ]
 
 (***************************************************************************)
 (* The inverse of a function.                                              *)

tests/FunctionsTests.tla

@@ -1,5 +1,5 @@
 ------------------------- MODULE FunctionsTests -------------------------
-EXTENDS Functions, Naturals, TLC, TLCExt, FiniteSets, Sequences
+EXTENDS Functions, Integers, TLC, TLCExt, FiniteSets, Sequences
 
 ASSUME LET T == INSTANCE TLC IN T!PrintT("FunctionsTests")
 
@@ -97,4 +97,14 @@ ASSUME
 	LET F == (0 :> "n1" @@ 2 :> "n2" @@ 1 :> "n3")
 	IN AntiFunction(AntiFunction(F)) = F
 
+ASSUME
+    LET f == ("a" :> 0 @@ "b" :> 1 @@ "c" :> 2)
+        g == ("a" :> 1 @@ "b" :> 1 @@ "c" :> 3)
+    IN Pointwise(f,g,+) = ("a" :> 1 @@ "b" :> 2 @@ "c" :> 5 )
+
+ASSUME
+    LET f == ("a" :> 1 @@ "b" :> 1 @@ "c" :> 2)
+        g == ("a" :> 1 @@ "b" :> 1 @@ "c" :> 3)
+    IN Pointwise(f,g,-) = ("a" :> 0 @@ "b" :> 0 @@ "c" :> (-1) )
+
 =============================================================================