Copy Functions.tla and useful operators from SequenceTheorems.tla

from TLAPS modules.

Adresses GitHub issue #2
#2

modules/Functions.tla

@@ -0,0 +1,63 @@
+------------------------------ MODULE Functions -----------------------------
+(***************************************************************************)
+(* `^{\large\bf \vspace{12pt}                                              *)
+(*  Notions about functions including injection, surjection, and bijection.*)
+(*  Originally contributed by Tom Rodeheffer, MSR.                         *)
+(*  \vspace{12pt}}^'                                                       *)
+(***************************************************************************)
+
+
+(***************************************************************************)
+(* Restriction of a function to a set (should be a subset of the domain).  *)
+(***************************************************************************)
+Restrict(f,S) == [ x \in S |-> f[x] ]
+
+(***************************************************************************)
+(* Range of a function.                                                    *)
+(* Note: The image of a set under function f can be defined as             *)
+(*       Range(Restrict(f,S)).                                             *)
+(***************************************************************************)
+Range(f) == { f[x] : x \in DOMAIN f }
+
+
+(***************************************************************************)
+(* The inverse of a function.                                              *)
+(***************************************************************************)
+Inverse(f,S,T) == [t \in T |-> CHOOSE s \in S : t \in Range(f) => f[s] = t]
+
+
+(***************************************************************************)
+(* A map is an injection iff each element in the domain maps to a distinct *)
+(* element in the range.                                                   *)
+(***************************************************************************)
+Injection(S,T) == { M \in [S -> T] : \A a,b \in S : M[a] = M[b] => a = b }
+
+
+(***************************************************************************)
+(* A map is a surjection iff for each element in the range there is some   *)
+(* element in the domain that maps to it.                                  *)
+(***************************************************************************)
+Surjection(S,T) == { M \in [S -> T] : \A t \in T : \E s \in S : M[s] = t }
+
+
+(***************************************************************************)
+(* A map is a bijection iff it is both an injection and a surjection.      *)
+(***************************************************************************)
+Bijection(S,T) == Injection(S,T) \cap Surjection(S,T)
+
+
+(***************************************************************************)
+(* An injection, surjection, or bijection exists if the corresponding set  *)
+(* is nonempty.                                                            *)
+(***************************************************************************)
+ExistsInjection(S,T)  == Injection(S,T) # {}
+ExistsSurjection(S,T) == Surjection(S,T) # {}
+ExistsBijection(S,T)  == Bijection(S,T) # {}
+
+
+=============================================================================
+\* Modification History
+\* Last modified Wed Jul 10 20:32:37 CEST 2013 by merz
+\* Last modified Wed Jun 05 12:14:19 CEST 2013 by bhargav
+\* Last modified Fri May 03 12:55:35 PDT 2013 by tomr
+\* Created Thu Apr 11 10:30:48 PDT 2013 by tomr

modules/SequencesExt.tla

@@ -3,6 +3,7 @@
 LOCAL INSTANCE Sequences
 LOCAL INSTANCE Naturals
 LOCAL INSTANCE FiniteSets
+LOCAL INSTANCE Functions
   (*************************************************************************)
   (* Imports the definitions from the modules, but doesn't export them.    *)
   (*************************************************************************)
@@ -24,6 +25,8 @@ IsInjective(s) ==
   (*                                                                       *)
   (* This definition is overridden by TLC in the Java class SequencesExt.  *)
   (* The operator is overridden by the Java method with the same name.     *)
+  (*                                                                       *)
+  (* Also see Functions!Injective operator.                                *)
   (*************************************************************************)
   \A i, j \in DOMAIN s: (s[i] = s[j]) => (i = j)
 
@@ -34,4 +37,86 @@ SetToSeq(S) ==
   (**************************************************************************)
   CHOOSE f \in [1..Cardinality(S) -> S] : IsInjective(f)
 
+-----------------------------------------------------------------------------
+
+Reverse(s) ==
+  (**************************************************************************)
+  (* Reverse the given sequence s:  Let l be Len(s) (length of s).          *)
+  (* Equals a sequence s.t. << S[l], S[l-1], ..., S[1]>>                    *)
+  (**************************************************************************)
+  [ i \in 1..Len(s) |-> s[(Len(s) - i) + 1] ]
+
+-----------------------------------------------------------------------------
+
+\* The operators below have been extracted from the TLAPS module 
+\* SequencesTheorems.tla as of 10/14/2019.  The original comments have been
+\* partially rewritten.
+
+InsertAt(s, i, e) ==
+  (**************************************************************************)
+  (* Inserts element e at the position i moving the original element to i+1 *)
+  (* and so on.  In other words, a sequence t s.t.:                         *)
+  (*   /\ Len(t) = Len(s) + 1                                               *)
+  (*   /\ t[i] = e                                                          *)
+  (*   /\ \A j \in 1..(i - 1): t[j] = s[j]                                  *)
+  (*   /\ \A k \in (i + 1)..Len(s): t[k + 1] = s[k]                         *)
+  (**************************************************************************)
+  SubSeq(s, 1, i-1) \o <<e>> \o SubSeq(s, i, Len(s))
+
+ReplaceAt(s, i, e) ==
+  (**************************************************************************)
+  (* Replaces the element at position i with the element e.                 *)
+  (**************************************************************************)
+  [s EXCEPT ![i] = e]
+
+RemoveAt(s, i) == 
+  (**************************************************************************)
+  (* Replaces the element at position i shortening the length of s by one.  *)
+  (**************************************************************************)
+  SubSeq(s, 1, i-1) \o SubSeq(s, i+1, Len(s))
+
+-----------------------------------------------------------------------------
+
+Front(s) == 
+  (**************************************************************************)
+  (* The sequence formed by removing its last element.                      *)
+  (**************************************************************************)
+  SubSeq(s, 1, Len(s)-1)
+
+Last(s) ==
+  (**************************************************************************)
+  (* The last element of the sequence.                                      *)
+  (**************************************************************************)
+  s[Len(s)]
+
+-----------------------------------------------------------------------------
+
+IsPrefix(s, t) ==
+  (**************************************************************************)
+  (* TRUE iff the sequence s is a prefix of the sequence t, s.t.            *)
+  (* \E u \in Seq(Range(t)) : t = s \o u. In other words, there exists      *)
+  (* a suffix u that with s prepended equals t.                             *)
+  (**************************************************************************)
+  DOMAIN s \subseteq DOMAIN t /\ \A i \in DOMAIN s: s[i] = t[i]
+
+IsStrictPrefix(s,t) ==
+  (**************************************************************************)
+  (* TRUE iff the sequence s is a prefix of the sequence t and s # t        *)
+  (**************************************************************************)
+  IsPrefix(s, t) /\ s # t
+
+IsSuffix(s, t) ==
+  (**************************************************************************)
+  (* TRUE iff the sequence s is a suffix of the sequence t, s.t.            *)
+  (* \E u \in Seq(Range(t)) : t = u \o s. In other words, there exists a    *)
+  (* prefix that with s appended equals t.                                  *)
+  (**************************************************************************)
+  IsPrefix(Reverse(s), Reverse(t))
+
+IsStrictSuffix(s, t) ==
+  (**************************************************************************)
+  (* TRUE iff the sequence s is a suffix of the sequence t and s # t        *)
+  (**************************************************************************)
+  IsSuffix(s,t) /\ s # t
+
 =============================================================================

tests/SequencesExtTests.tla

@@ -26,4 +26,43 @@ ASSUME(SetToSeq({1}) = <<1>>)
 ASSUME(LET s == {"t","l","a","p","l","u","s"}
            seq == SetToSeq(s)
        IN Len(seq) = Cardinality(s) /\ ToSet(seq) = s)
+
+ASSUME(Reverse(<<>>) = <<>>)
+ASSUME(Reverse(<<1,2,3>>) = <<3,2,1>>)
+ASSUME(Reverse(<<1,1,2>>) = <<2,1,1>>)
+ASSUME(Reverse(<<"a","a","b">>) = <<"b","a","a">>)
+
+-----------------------------------------------------------------------------
+
+ASSUME(ReplaceAt(<<1>>, 1, 2) = <<2>>) 
+ASSUME(ReplaceAt(<<1,1,1>>, 1, 2) = <<2,1,1>>) 
+
+-----------------------------------------------------------------------------
+
+ASSUME(IsPrefix(<<>>, <<>>))
+ASSUME(IsPrefix(<<>>, <<1>>))
+ASSUME(IsPrefix(<<1>>, <<1,2>>))
+ASSUME(IsPrefix(<<1,2>>, <<1,2>>))
+ASSUME(IsPrefix(<<1,2>>, <<1,2,3>>))
+
+ASSUME(~IsPrefix(<<1,2,3>>, <<1,2>>))
+ASSUME(~IsPrefix(<<1,2,2>>, <<1,2,3>>))
+ASSUME(~IsPrefix(<<1,2,3>>, <<1,2,2>>))
+ASSUME(~IsPrefix(<<1>>, <<2>>))
+ASSUME(~IsPrefix(<<2>>, <<1>>))
+ASSUME(~IsPrefix(<<2,1>>, <<1,2>>))
+ASSUME(~IsPrefix(<<1,2>>, <<2,1>>))
+
+ASSUME(~IsStrictPrefix(<<>>, <<>>))
+ASSUME(IsStrictPrefix(<<>>, <<1>>))
+ASSUME(IsStrictPrefix(<<1>>, <<1,2>>))
+ASSUME(~IsStrictPrefix(<<1,2>>, <<1,2>>))
+ASSUME(IsStrictPrefix(<<1,2>>, <<1,2,3>>))
+
+ASSUME(IsSuffix(<<3>>, <<1,2,3>>))
+ASSUME(IsSuffix(<<2,3>>, <<1,2,3>>))
+ASSUME(~IsSuffix(<<3,2>>, <<1,2,3>>))
+ASSUME(IsSuffix(<<1,2,3>>, <<1,2,3>>))
+
+ASSUME(~IsStrictSuffix(<<1,2,3>>, <<1,2,3>>))
 =============================================================================