namespace http://cds.omdoc.org/examples❚
// a simple language for set theory
This primarily exemplifies advanced notations for parsing and presentation. ❚
theory Sets : http://cds.omdoc.org/urtheories?LF =
set : type❙
prop : type❙
in : set ⟶ set ⟶ prop❘ # 1 ∈ 2 prec 75 ❘ role Type❙
equal : set ⟶ set ⟶ prop❘
// No printable characters are reserved. Here = is used as a delimiter. ❘ # 1 = 2 prec 50❙
ded : prop ⟶ type ❘ # ded 1 prec 0❙
// Elem A yields a for elements of the set A.
Its notation is chosen such that variable attributions can be parsed and presented as x ∈ A instead of x : Elem A.❙
Elem : set ⟶ type ❘# Elem 1 prec 70❙
// The following declaration lifts equal to the types Elem A.
For parsing (#) it needs a different notation (==); for presentation (##) we can reuse =.❙
elemequal : {A} Elem A ⟶ Elem A ⟶ prop ❘ # 2 == 3 prec 50 ❘
// This notation for presentation is 2-dimensional: _ yields a subscript and %I marks an implicit (hidable) argument. ❘
## 2 = _ %I1 3 prec 50❙
// A universal quantifier over all elements of a given set.
Using Elem A, the relativization can be expressed in the type system.❙
forall : {A} (Elem A ⟶ prop) ⟶ prop ❘
// The notation uses V2T for an attributed variable (x ∈ A) and -3 for the scope.
Thus, forall is a binder as far as the MMT notation system is concerned.
The type system considers it as a higher-order constant of LF. The LF plugin for MMT configures the conversion between the two. ❘
# ∀ V2T . -3 prec -1❙
empty : set ❘ # ∅ ❙
// Several set operators use {}-based notations and are binders.
MMT can handle that.
However, we have to use ; instead of : for replacement because the delimiter scheme { : } is already used for the Pi symbol of LF.
Because the notations are left- and right-closed, we can give them very low precedences, which has the effect that they act like brackets.❙
compr : {A} (Elem A ⟶ prop) ⟶ set ❘ # { V2T | -3 } prec -100004❙
repl : {A}{B} (Elem A ⟶ Elem B) ⟶ set ❘ # { -4 ; V3T } prec -100006❙
union : set ⟶ set ⟶ set ❘# 1 ∪ 2 prec 120❙
inter : set ⟶ set ⟶ set ❘# 1 ∩ 2 prec 120❙
// The big operators for union and intersection are binders with 2-dimensional notations.
In the __ produces underscripts.❙
bigunion : {A} (Elem A ⟶ set) ⟶ set ❘# ⋃ V2T . -3 prec 60 ❘ ## ⋃ __ V2T -3 prec 5❙
biginter : {A} (Elem A ⟶ set) ⟶ set ❘# ⋂ V2T . -3 prec 60 ❘ ## ⋂ __ V2T -3 prec 5❙
fun : set ⟶ set ⟶ set❘ # 1 ⇒ 2 prec 120❘ // ^ produces superscripts. ❘ ## 2 ^ 1 ❙
lam : {A}{B} (Elem A ⟶ Elem B) ⟶ Elem (fun A B) ❘ # λ 3❙
app : {A}{B} Elem (fun A B) ⟶ Elem A ⟶ Elem B ❘ # 3 @ 4 prec 120❙
prod : set ⟶ set ⟶ set❘ # 1 × 2 prec 120❙
pair : {A}{B} Elem A ⟶ Elem B ⟶ Elem (A × B)❘
// We can use () in notations as well. But the precedence has to below the precedence of the built-in notation for bracketed expressions. ❘
# ( 3 , 4 ) prec -1000000001❘❙
// The two projection use, e.g., ._1 for parsing and subscripts for presentation. %D1 yields 1 as a delimiter (instead of an argument marker). ❙
pi1 : {A}{B} Elem (A × B) ⟶ Elem A❘ # 3 ._1 prec 200 ❘ ## 3 _ %D1 prec 200❙
pi2 : {A}{B} Elem (A × B) ⟶ Elem B❘ # 3 ._2 prec 201 ❘ ## 3 _ %D2 prec 200❙
cardinality : set ⟶ set ❘ # | 1 | prec -100000❙
// Some example expressions that use the notations. ❙
distributive : {A}{F: Elem A ⟶ set} ded A ∩ ⋃ x ∈ A. (F x) = ⋃ x. A ∩ (F x)❙
pairs : {A} ded {x ∈ A × A | x._1 == x._2} = {(x,x) ; x ∈ A} ❙
sizes : {A} (ded |{f∈A⇒A|∀x∈A.f@x==x}|=|∅⇒∅|)❙
❚