libtlafmt 0.4.1

A formatter library for TLA+ specs, core of tlafmt
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/Functions.tla
---
------------------------------- 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) \intersect 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