Add theorem about Head, Tail, and Range with IsInjective(seq).

Author: muenchnerkindl

modules/SequencesExtTheorems.tla

@@ -16,6 +16,11 @@ LEMMA TailTransitivityIsInjective
                IsInjective(seq)
         PROVE IsInjective(Tail(seq))
 
+LEMMA HeadTailRange ==
+  ASSUME NEW S, NEW seq \in Seq(S), seq # << >>, IsInjective(seq)
+  PROVE  /\ Head(seq) \in Range(seq)
+         /\ Range(Tail(seq)) = Range(seq) \ {Head(seq)}
+
 =============================================================================
 \* Modification History
 \* Last modified Thu Feb 27 11:38:41 PST 2020 by markus

modules/SequencesExtTheorems_proofs.tla

@@ -43,6 +43,28 @@ LEMMA TailTransitivityIsInjective \* With TLAPS 1.4.3
     <2>9. QED BY <2>1, <2>2, <2>3, <2>5, <2>6, <2>7, <2>8 DEF IsInjective
   <1>2. QED BY <1>1
 
+LEMMA HeadTailRange == \* With TLAPS 1.4.5 (but not 1.4.3)
+  ASSUME NEW S, NEW seq \in Seq(S), seq # << >>, IsInjective(seq)
+  PROVE  /\ Head(seq) \in Range(seq)
+         /\ Range(Tail(seq)) = Range(seq) \ {Head(seq)}
+<1>1. Head(seq) \in Range(seq)
+  BY SMT DEF Range
+<1>2. Range(Tail(seq)) \subseteq Range(seq)
+  BY SMT DEF Range
+<1>3. Head(seq) \notin Range(Tail(seq))
+  BY SMT DEF Range, IsInjective
+<1>4. ASSUME NEW x \in Range(seq), x # Head(seq)
+      PROVE  x \in Range(Tail(seq))
+  <2>1. PICK i \in DOMAIN seq : x = seq[i]
+    BY Isa DEF Range
+  <2>2. i # 1
+    BY SMT, <2>1, <1>4
+  <2>3. /\ i-1 \in DOMAIN Tail(seq)
+        /\ x = Tail(seq)[i-1]
+    BY SMT, <2>1, <2>2
+  <2>. QED  BY Isa, <2>3 DEF Range
+<1>. QED  BY Isa, <1>1, <1>2, <1>3, <1>4
+
 =============================================================================
 \* Modification History
 \* Last modified Thu Feb 27 11:44:49 PST 2020 by markus