namespace http://cds.omdoc.org/examples/tutorial❚

import rules scala://tutorial.examples.mmt.kwarc.info❚

theory Nat : ?NatDed =
	/T We start with a sort for the natural numbers and an abbreviation ℕ for the terms
		of that sort - i.e. the type of actual numbers, which we will populate with literals: ❙
	Nat : sort ❙
	ℕ = tm Nat ❙
	
	/T The literals are provided by a RealizedType rule written in Scala in 
		scala_realizations/info/kwarc/mmt/examples/tutorial/Literals.scala
	  These rules are special constants declared by the "rule" keyword followed by the classname: ❙
	rule rules?NatLiterals ❙
	/T The MMT build system includes a target for building these Scala files - the command is "build MMT/examples scala-bin" ❙

	/T The rule NatLiterals introduces MMT literals for all natural numbers as well as a lexing rule for them.
	   To see whether it works, let's define the constant "zero" as the literal 0: ❙
	zero = 0 ❙
	
	/T In addition to RealizedType rules, there are also RealizedOperator rules, which allow us
		to associate a function on literals declared in MMT with a corresponding implementation 
		in Scala. We can use this to implement the successor function: ❙
	S : ℕ ⟶ ℕ ❙
	rule rules?Succ ❙

	/T Succ is implemented in such a way that it can be inverted, which MMT will use for unification, when working with terms that contain both literals and variables: ❙

	/T MMT will now simplify every instance of S being applied to literals to the actual
		computation result. We can test this, by proving that the successor
		of 17 is 18 by reflexivity of equality alone: ❙
	succ_test : ⊢ S 17 = 18 ❘ = refl 18 ❙
	
	/T Now for the same thing with addition: ❙
	plus : ℕ ⟶ ℕ ⟶ ℕ ❘ # 1 + 2 prec 40 ❙
	rule rules?Plus ❙
	/T We can again test, whether this works by proving an equality with refl: ❙
	plus_test : ⊢ 5 + 5 = 10 ❘ = refl 10 ❙
	
	/T We use Scala to implement computations on literals.
	   Additionally, we need symbolic rewrite rules for working with other expressions.
	   The LF plugin includes a ChangeListener that automatically generates rewrite rules from certain constants.
	   To do so, we add the role Simplify to the constants.
	   We must have previously added roles Judgment and Eq to ⊢ and =, respectively.❙
	plus_def1 : {x} ⊢ x + zero = x ❘ # plus_def1 1 ❘ role Simplify ❙
	plus_def1b : {x} ⊢ zero + x = x ❘ role Simplify ❙
	plus_def2 : {x,y} ⊢ S x + y = S (x + y) ❘ role Simplify ❙
	plus_def2b : {x,y} ⊢ x + S y = S (x + y) ❘ role Simplify ❙
	/T The generate rules will make MMT rewrite the left to the right side of the equality during type-checking. ❙
	
	/T We also add associativity (omitting the proof), which we need in the view below.❙
  plus_assoc : {x,y,z} ⊢ (x + y) + z = x + (y + z) ❘ # plus_assoc 1 2 3 ❙
❚
	
view NatAsMonoid : ?Monoid → ?Nat =
	u = Nat ❙
	comp = plus ❙
	unit = zero ❙
	assoc = allI ([x] allI ([y] allI (plus_assoc x y))) ❙
	unit_axiom = allI ([x] plus_def1 x) ❙
❚