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

@@ -1301,6 +1301,37 @@ 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({})
+  BY SumFunctionOnSetEmpty, FS_EmptySet
+<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
+  <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>. QED  BY <1>2, <2>3, <2>4, <2>5, <2>6
+<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.             *)
 (*************************************************************************)
@@ -1392,6 +1423,11 @@ 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)
+BY SumFunctionOnSetConst DEF SumFunction
+
 THEOREM SumFunctionMonotonic ==
   ASSUME NEW f, IsFiniteSet(DOMAIN f), NEW g, DOMAIN g = DOMAIN f,
          \A x \in DOMAIN f : f[x] \in Int,