Theorems for sum of constant function

Add SumFunctionOnSetConst and SumFunctionConst stating that summing a
constant function over a finite set equals the constant times the
cardinality of the set, together with corresponding proofs and an
example in the doc comments.

[Feature]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

modules/FunctionTheorems.tla

@@ -767,6 +767,15 @@ THEOREM SumFunctionOnSetZero ==
          NEW fun, \A x \in S : fun[x] \in Nat
   PROVE  SumFunctionOnSet(fun, S) = 0 <=> \A x \in S : fun[x] = 0
 
+(*************************************************************************)
+(* Summing a constant function over a finite set yields the constant     *)
+(* multiplied by the cardinality of the set. For example,                *)
+(*   SumFunctionOnSet([s \in {"a","b","c"} |-> 5], {"a","b","c"}) = 15.  *)
+(*************************************************************************)
+THEOREM SumFunctionOnSetConst ==
+  ASSUME NEW S, IsFiniteSet(S), NEW c \in Int
+  PROVE  SumFunctionOnSet([s \in S |-> c], S) = c * Cardinality(S)
+
 (*************************************************************************)
 (* Summing a function is monotonic in the function argument.             *)
 (*************************************************************************)
@@ -825,6 +834,15 @@ THEOREM SumFunctionZero ==
          \A x \in DOMAIN fun : fun[x] \in Nat
   PROVE  SumFunction(fun) = 0 <=> \A x \in DOMAIN fun : fun[x] = 0
 
+(*************************************************************************)
+(* Summing a constant function yields the constant multiplied by the     *)
+(* cardinality of its domain. For example,                               *)
+(*   SumFunction([s \in {"a","b","c"} |-> 5]) = 15.                      *)
+(*************************************************************************)
+THEOREM SumFunctionConst ==
+  ASSUME NEW S, IsFiniteSet(S), NEW c \in Int
+  PROVE  SumFunction([s \in S |-> c]) = c * Cardinality(S)
+
 THEOREM SumFunctionMonotonic ==
   ASSUME NEW f, IsFiniteSet(DOMAIN f), NEW g, DOMAIN g = DOMAIN f,
          \A x \in DOMAIN f : f[x] \in Int,

modules/FunctionTheorems_proofs.tla

@@ -1310,6 +1310,49 @@ THEOREM SumFunctionOnSetZero ==
   <2>. P(S)  BY <1>1, <1>2, FS_Induction, IsaM("iprover")
   <2>. QED   BY DEF P
 
+(*************************************************************************)
+(* Summing a constant function over a finite set yields the constant     *)
+(* multiplied by the cardinality of the set.                             *)
+(*************************************************************************)
+THEOREM SumFunctionOnSetConst ==
+  ASSUME NEW S, IsFiniteSet(S), NEW c \in Int
+  PROVE  SumFunctionOnSet([s \in S |-> c], S) = c * Cardinality(S)
+<1>. DEFINE fun == [s \in S |-> c]
+<1>. DEFINE P(T) == SumFunctionOnSet(fun, T) = c * Cardinality(T)
+<1>1. P({})
+  <2>1. SumFunctionOnSet(fun, {}) = 0
+    BY SumFunctionOnSetEmpty
+  <2>2. Cardinality({}) = 0
+    BY FS_EmptySet
+  <2>3. c * Cardinality({}) = 0
+    BY <2>2
+  <2>. QED  BY <2>1, <2>3
+<1>2. ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW x \in S \ T
+      PROVE  P(T \union {x})
+  <2>1. \A j \in T \union {x} : fun[j] = c
+    BY <1>2
+  <2>2. \A j \in T \union {x} : fun[j] \in Int
+    BY <2>1, c \in Int
+  <2>3. SumFunctionOnSet(fun, T \union {x}) = fun[x] + SumFunctionOnSet(fun, T)
+    BY <1>2, <2>2, SumFunctionOnSetAddIndex
+  <2>4. fun[x] = c
+    BY <1>2
+  <2>5. Cardinality(T \union {x}) = Cardinality(T) + 1
+    BY <1>2, FS_AddElement
+  <2>6. Cardinality(T) \in Nat
+    BY <1>2, FS_CardinalityType
+  <2>7. SumFunctionOnSet(fun, T \union {x}) = c + c * Cardinality(T)
+    BY <1>2, <2>3, <2>4
+  <2>8. c + c * Cardinality(T) = c * (Cardinality(T) + 1)
+    BY <2>6
+  <2>9. c * (Cardinality(T) + 1) = c * Cardinality(T \union {x})
+    BY <2>5
+  <2>. QED  BY <2>7, <2>8, <2>9
+<1>. QED
+  <2>. HIDE DEF P
+  <2>. P(S)  BY <1>1, <1>2, FS_Induction, IsaM("iprover")
+  <2>. QED   BY DEF P
+
 (*************************************************************************)
 (* Summing a function is monotonic in the function argument.             *)
 (*************************************************************************)
@@ -1401,6 +1444,18 @@ THEOREM SumFunctionZero ==
   PROVE  SumFunction(fun) = 0 <=> \A x \in DOMAIN fun : fun[x] = 0
 BY SumFunctionOnSetZero DEF SumFunction 
 
+THEOREM SumFunctionConst ==
+  ASSUME NEW S, IsFiniteSet(S), NEW c \in Int
+  PROVE  SumFunction([s \in S |-> c]) = c * Cardinality(S)
+<1>. DEFINE fun == [s \in S |-> c]
+<1>1. DOMAIN fun = S
+  OBVIOUS
+<1>2. SumFunction(fun) = SumFunctionOnSet(fun, S)
+  BY <1>1 DEF SumFunction
+<1>3. SumFunctionOnSet(fun, S) = c * Cardinality(S)
+  BY SumFunctionOnSetConst
+<1>. QED  BY <1>2, <1>3
+
 THEOREM SumFunctionMonotonic ==
   ASSUME NEW f, IsFiniteSet(DOMAIN f), NEW g, DOMAIN g = DOMAIN f,
          \A x \in DOMAIN f : f[x] \in Int,