Commit c59c3ccb authored by Dennis Müller's avatar Dennis Müller

notations in sequences

parent 88723973
namespace http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final
theory Types : ur:?LF =
tp : type
tm : tp → type # tm 1 prec -1

theory Logic : ur:?LF =
prop: type
ded : prop → type# ⊦ 1 prec -1role Judgment

theory Equality : ur:?LF =
include ?Types
include ?Logic
equal : {A} tm A → tm A → prop# 2 = 3
refl : {A,X:tm A} ⊦ X = X
sym : {A,X,Y:tm A} ⊦ X = Y → ⊦ Y = X
trans : {A,X,Y,Z:tm A} ⊦ X = Y → ⊦ Y = Z → ⊦ X = Z
cong : {A,B,X,Y,F:tm A → tm B} ⊦ X = Y → ⊦ (F X) = (F Y)

theory STT : ur:?LF =
include ?Equality
fun : tp → tp → tp# 1 ⇒ 2
abstract : {A,B} (tm A → tm B) → tm (A ⇒ B)# λ 3
apply : {A,B} tm (A ⇒ B) → tm A → tm B# 3 @ 4 prec 5
beta : {A,B,F: tm A → tm B,X} ⊦ (λ F) @ X = (F X)

theory Eta : ur:?LF =
include ?STT
eta : {A,B,F: tm (A ⇒ B)} ⊦ (λ [x: tm A] (F @ x)) = F

theory Extensionality : ur:?LF =
include ?STT
ext : {A,B,F,G: tm (A ⇒ B)} ({x: tm A} ⊦ F @ x = G @ x) → ⊦ F = G# ext 5

// view EtaExt : ?Eta -> ?Extensionality =
// include mmtid ?STT
eta = [A,B,F] ext [x] beta

theory List : ?STT =
list : tp → tp# < 1 >
nilOf : {A: tp} tm <A># nil %I1
cons : {A: tp} tm A → tm <A> → tm <A># 2 + 3 prec 10
fold : {A,B} tm B → (tm A → tm B → tm B) → tm <A> → tm B
fold_nil : {A,B,N,C} ⊦ fold A B N C nil = N
fold_cons : {A,B,N,C,X,L} ⊦ fold A B N C (X+L) = C X (fold A B N C L)
map : {A,B} tm (A ⇒ B) → tm <A> → tm <B>= [A,B,f] fold A <B> nil ([a,bs] (f@a)+bs)# map 3 4
append : {A} tm <A> → tm <A> ⇒ <A>= [A] fold A (<A> ⇒ <A>) (λ[x]x) ([a,f] λ[l]a+(f@l))
flatten: {A} tm < <A> > → tm <A>= [A] fold <A> <A> nil ([l,r] (append A l) @ r)

theory Monad : ?STT =
operator: tp → tp# M 1 prec 20
unit : {A} tm A → tm M A# return 2
bind : {A,B} tm M A → tm (A ⇒ M B) → tm M B# 3 > 4 prec 5
neutral_left : {A,B,F: tm (A ⇒ M B)}{X: tm A} ⊦ (return X) > F = F @ X
neutral_right : {A,m: tm M A} ⊦ m > (λ [x] return x) = m
assoc: {A,B,C, F: tm (A ⇒ M B), G: tm (B ⇒ M C),m: tm M A} ⊦ (m > F) > G = m > (λ[x]F @ x > G)

view ListMonad : ?Monad -> ?List =
operator = list
unit = [A] [x] x+nil
bind = [A,B][l,f] (flatten B) (map f l)
// neutral_left = ...
// neutral_right = ...
// assoc = ...

theory MonadPlus : ?STT =
include ?Monad
// more stuff here

......@@ -4,16 +4,16 @@ theory FlexaryConnectives : ur:?LFS =
include ?PL❙
flexand : {n} prop^n ⟶ prop❘# ⋀ 2❙
flexandI : {n} {a: prop^n} ⟨' ⊦ a.i | i:n '⟩ ⟶ ⊦ ⋀ a❙
flexandE : {n} {a: prop^n} ⊦ ⋀ a ⟶ {i} DED (succ i) LEQ n ⟶ ⊦ a.i❙
flexandI : {n} {a: prop^n} ⟨' ⊦ a..i | i:n '⟩ ⟶ ⊦ ⋀ a❙
flexandE : {n} {a: prop^n} ⊦ ⋀ a ⟶ {i} DED (succ i) LEQ n ⟶ ⊦ a..i❙
flexor : {n} prop^n ⟶ prop❘# ⋁ 2❙
flexorI : {n} {a: prop^n} {i} DED (succ i) LEQ n ⟶ ⊦ a.i ⟶ ⊦ ⋁ a❙
flexorE : {n} {a: prop^n} {C} ⊦ ⋁ a ⟶ ⟨' ⊦ a.i ⟶ ⊦ C |i:n '⟩ ⟶ ⊦ C❙
flexorI : {n} {a: prop^n} {i} DED (succ i) LEQ n ⟶ ⊦ a..i ⟶ ⊦ ⋁ a❙
flexorE : {n} {a: prop^n} {C} ⊦ ⋁ a ⟶ ⟨' ⊦ a..i ⟶ ⊦ C |i:n '⟩ ⟶ ⊦ C❙
fleximp : {n} prop^n ⟶ prop ⟶ prop❘# 2 ⇒* 3 prec 10❙
fleximpI : {n} {a: prop^n, b} (⟨' ⊦ a.i|i:n '⟩ ⟶ ⊦ b) ⟶ ⊦ a ⇒* b❙
fleximpE : {n} {a: prop^n, b} ⊦ a ⇒* b ⟶ ⟨' ⊦ a.i|i:n '⟩ ⟶ ⊦ b❙
fleximpI : {n} {a: prop^n, b} (⟨' ⊦ a..i|i:n '⟩ ⟶ ⊦ b) ⟶ ⊦ a ⇒* b❙
fleximpE : {n} {a: prop^n, b} ⊦ a ⇒* b ⟶ ⟨' ⊦ a..i|i:n '⟩ ⟶ ⊦ b❙
......
namespace http://cds.omdoc.org/examples
theory FlexaryConnectives : ur:?LFS =
include ?PL
flexand : {n} prop^n → prop# ⋀ 2
flexandI : {n} {a: prop^n} ⟨' ded a.i | i:n '⟩ → ded ⋀ a
flexandE : {n} {a: prop^n} ded ⋀ a → {i} DED (succ i) LEQ n → ded a.i
flexor : {n} prop^n → prop# ⋁ 2
flexorI : {n} {a: prop^n} {i} DED (succ i) LEQ n → ded a.i → ded ⋁ a
flexorE : {n} {a: prop^n} {C} ded ⋁ a → ⟨' ded a.i → ded C |i:n '⟩ → ded C
fleximp : {n} prop^n → prop → prop# 2 ⇒* 3 prec 10
fleximpI : {n} {a: prop^n, b} (⟨' ded a.i|i:n '⟩ → ded b) → ded a ⇒* b
fleximpE : {n} {a: prop^n, b} ded a ⇒* b → ⟨' ded a.i|i:n '⟩ → ded b

theory FlexaryQuantifiers : ur:?LFS =
include ?FOL
flexforall : {n} (term^n → prop) → prop# ∀* 2
flexforallI: {n, F: term^n → prop} ({x:term^n} ded F x) → ded ∀* [x] F x
flexforallE: {n, F: term^n → prop} {x:term^n} ded (∀* [x] F x) → ded F x
flexexists : {n} (term^n → prop) → prop# ∃* 2
flexexistsI: {n, F: term^n → prop} {x:term^n} ded F x → ded ∃* [x] F x
flexexistsE: {n, F: term^n → prop,C} ({x:term^n} ded (∃* [x] F x) → ded C) → ded C

Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment