generalize SumFunctionOnSetConst

Signed-off-by: Stephan Merz <stephan.merz@loria.fr>

Author: muenchnerkindl

modules/FunctionTheorems.tla

@@ -767,14 +767,28 @@ THEOREM SumFunctionOnSetZero ==
          NEW fun, \A x \in S : fun[x] \in Nat
   PROVE  SumFunctionOnSet(fun, S) = 0 <=> \A x \in S : fun[x] = 0
 
+(*************************************************************************)
+(* Given any Int-valued function f and finite set S such that f[s] = c   *)
+(* for all s \in S, summing f over S yields c multiplied by the          *)
+(* cardinality of S. For example, for                                    *)
+(*   f == [s \in {"a", "b", "c"} |-> IF s = "c" THEN 42 ELSE 5],         *)
+(*   SumFunctionOnSet(f, {"a","b"}) = 10.                                *)
+(*************************************************************************)
+THEOREM SumFunctionOnSetConst ==
+  ASSUME NEW D, NEW S \in SUBSET D, IsFiniteSet(S),
+         NEW f \in [D -> Int], NEW c \in Int, \A x \in S : f[x] = c 
+  PROVE  SumFunctionOnSet(f, S) = c * Cardinality(S)
+
 (*************************************************************************)
 (* 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.             *)

modules/FunctionTheorems_proofs.tla

@@ -1310,10 +1310,38 @@ THEOREM SumFunctionOnSetZero ==
   <2>. P(S)  BY <1>1, <1>2, FS_Induction, IsaM("iprover")
   <2>. QED   BY DEF P
 
+(*************************************************************************)
+(* Given any Int-valued function f and finite set S such that f[s] = c   *)
+(* for all s \in S, summing f over S yields c multiplied by the          *)
+(* cardinality of S.                                                     *)
+(*************************************************************************)
+THEOREM SumFunctionOnSetConst ==
+  ASSUME NEW D, NEW S \in SUBSET D, IsFiniteSet(S),
+         NEW f \in [D -> Int], NEW c \in Int, \A x \in S : f[x] = c 
+  PROVE  SumFunctionOnSet(f, S) = c * Cardinality(S)
+<1>. DEFINE P(T) == SumFunctionOnSet(f, T) = c * Cardinality(T)
+<1>1. P({})
+  <2>1. SumFunctionOnSet(f, {}) = 0
+    BY SumFunctionOnSetEmpty
+  <2>2. Cardinality({}) = 0
+    BY FS_EmptySet
+  <2>. QED  BY <2>1, <2>2
+<1>2. ASSUME NEW T \in SUBSET S, IsFiniteSet(T), P(T), NEW x \in S \ T
+      PROVE  P(T \union {x})
+  <2>1. SumFunctionOnSet(f, T \union {x}) = c + SumFunctionOnSet(f, T)
+    BY <1>2, SumFunctionOnSetAddIndex
+  <2>2. Cardinality(T \union {x}) = Cardinality(T) + 1
+    BY <1>2, FS_AddElement
+  <2>3. Cardinality(T) \in Nat 
+    BY <1>2, FS_CardinalityType
+  <2>. QED  BY <1>2, <2>1, <2>2, <2>3
+<1>. QED  BY <1>1, <1>2, FS_Induction, IsaM("iprover")
+
 (*************************************************************************)
 (* 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)
@@ -1352,6 +1380,7 @@ THEOREM SumFunctionOnSetConst ==
   <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.             *)
@@ -1447,6 +1476,8 @@ 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
+(*
 <1>. DEFINE fun == [s \in S |-> c]
 <1>1. DOMAIN fun = S
   OBVIOUS
@@ -1455,6 +1486,7 @@ THEOREM SumFunctionConst ==
 <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,