/T   This file contains the general structure of the MMT tutorial given at CICM 2016.❚


/T   A namespace declaration defines the root URI of the following content.❚
namespace http://cds.omdoc.org/examples/tutorial❚

document SFOL 

/T   A theory defines a language. It may optionally use a meta-theory, which is given by its URI.❚
ref ?FOL ❚

/T   We can already use our logic as the meta-theory of a theory.
     To refer to FOL, we use its URI, which is of the form NAMESPACE?THEORYNAME.
❚

/T   A Semigroup consists of ...❚
ref ?Semigroup ❚

  
/T   Now we define the proof theory of LF using natural ⊢uction proof rules.
     It is practical to do this in a separate theory that includes the syntax above.
❚        
     
ref ?NatDed ❚

/T   The rules declared so far only yield intuitionistic first-order logic. To get to classical logic,
we can use the modular approach and extend NatDed by the law of excluded middle: ❚
ref ?ClassicalSFOL ❚


document AlgebraicHierarchy 

/T   Exemplary, we can now built the usual hierarchy of algebraic theories in a modualar way, starting again with
	semigroups: ❚
ref ?Semigroup ❚

/T   Monoids just extend Semigroups: ❚
ref ?Monoid ❚

/T   A Monoid happens to be a preorder - a fact, that we can express using Views. A view is a morphism
		between two theories, that maps each declaration of the domain to a valid expression
		over the symbols in the codomain such, that typing judgments are preserved. ❚
		
/T   First, a theory of preorders: ❚
ref ?PreOrder ❚

/T   To show that monoids are preorders, we have to map each axiom of a preorder to a provable
			statement in the theory of monoids, i.e. we need a view preorder ⟶ monoid, like so: ❚
ref ?MonoidAsPreorder ❚

/T   Next, on to groups: ❚
ref ?Group ❚

/T   For Rings we will need abelian groups in particular, so let's create a theory for "abelian": ❚
ref ?Abelian ❚

/T   ...and one for abelian groups: ❚
ref ?AbelianGroup ❚

/T   Now for Rings. Obviously, if we want to implement a theory of rings modularly, we
			want to make use of the fact, that a ring is an additive abelian group with a multiplicative monoid.
			Both theories already exist, but we need them with respect to two different operations - includes
			will not get us there. Instead, we will use MMT structures. Structures behave like includes,
			except that they allow us to slightly modify the imported declarations; in particular we are allowed
			to provide new definitions and notations for the imported symbols: ❚
ref ?Ring ❚


document LiteralsAndRules 
/T   Next, we will look at different ways to implement RULES by writing a theory for 
			natural numbers ❚
ref ?Nat ❚

/T   And of course, natural numbers form a monoid, which we can express with a view: ❚
ref ?NatAsMonoid ❚