diff --git a/modules/Functions.tla b/modules/Functions.tla index 78c83ab..eab6edc 100644 --- a/modules/Functions.tla +++ b/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. *) diff --git a/tests/FunctionsTests.tla b/tests/FunctionsTests.tla index a61c714..79fa23f 100644 --- a/tests/FunctionsTests.tla +++ b/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) ) + =============================================================================