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

/T   A Semigroup consists of ...❚
theory Semigroup : ?NatDed =
   /T ... a sort for the universe ...❙   
   u : sort❙
   /T ... a binary function on the universe, written as infix ∘ ...❙
   comp : tm u ⟶ tm u ⟶ tm u❘ # 1 ∘ 2 prec 40❙
   /T ...such that ∘ is associative.❙
   assoc : ⊢  ∀[x]∀[y]∀[z] (x ∘ y) ∘ z = x ∘ (y ∘ z)❙
   
   /T We prove a few abbreviations that come in handy when doing proofs:❙
   assocLeftToRight: {x,y,z} ⊢ (x ∘ y) ∘ z = x ∘ (y ∘ z)❘= [x,y,z] allE (allE (allE assoc x) y) z❘ # assocLR %I1 %I2 %I3❙
   assocRightToLeft: {x,y,z} ⊢ x ∘ (y ∘ z) = (x ∘ y) ∘ z❘= [x,y,z] sym assocLR❘ # assocRL %I1 %I2 %I3❙
❚
 
theory Monoid : ?NatDed =
	include ?Semigroup ❙
	
  // metadata can be attributed both to a theory ... ❙
  @_description s❙
	// ... and to constants ... ❙
	unit : tm u ❘ # e ❘ @_description  ❙
	// ... any symbol can be used as a metadata key, several @_XXX keys are predefined❙
	
	unit_axiom : ⊢ ∀[x] x ∘ e = x❘ @_description  ❙
❚
	                                   
theory PreOrder : ?NatDed =
	o : sort ❙
	order : tm o ⟶ tm o ⟶ prop ❘ # 1 ≤ 2 prec 50 ❙
	reflexivity : {x} ⊢ x ≤ x ❙
	transitivity : {x,y,z} ⊢ x ≤ y ⟶ ⊢ y ≤ z ⟶ ⊢ x ≤ z ❙
	
	// We prove the ternary case of transitivity by chaining transitivity twice.❙
	transitivity3: {w,x,y,z} ⊢ w ≤ x ⟶ ⊢ x ≤ y ⟶ ⊢ y ≤ z ⟶ ⊢ w ≤ z❘
	      = [w,x,y,z,p,q,r] transitivity (transitivity p q) r❙

❚
	
view MonoidAsPreorder : ?PreOrder → ?Monoid =
	/T Assignments in views are of the form NAME = EXPRESSION. First, the universes: ❙
	o = u ❙
	/T Now for the order itself, which is defined by a ≤ b ⇔ ∃x a∘x=b. Thus: ❙
	order = [x,y] (∃[z] x ∘ z = y) ❙
	/T The target statement for reflexivity translates as ${x} ⊢ ∃[z] x ∘ z = x$, which
		we now need to prove for monoids: ❙
	reflexivity = [x] exI e (allE unit_axiom x)❙
	/T The target statement for transitivity is ${x,y,z} ⊢ (∃[a] x ∘ a = y) ⟶ ⊢ (∃[b] y ∘ b = z) ⟶ ⊢ ∃[c] x ∘ c = z$ where the proof has to extract witness a with proof pa from p and b and qb from q and then supply the witness c as a∘b along with its proof:❙
	transitivity = [x,y,z,p,q] exE p [a,pa] exE q [b,qb] exI (a ∘ b) trans assocRL trans (congTerm ([k]k∘b) pa) qb❙
❚
	
theory Abelian : ?NatDed =
	include ?Semigroup ❙

	commutative : ⊢ ∀[x] ∀[y] x ∘ y = y ∘ x ❙
❚
	
theory Group : ?NatDed =
	include ?Monoid ❙
	
	inverse : tm u ⟶ tm u ❘ # 1 ⁻¹  ❙ 
	/T jsuperminus jsuper1	❙
	
	inverse_axiom : ⊢ ∀[x] x ∘ (x ⁻¹ ) = e ❙
❚

theory AbelianGroup : ?NatDed =
	include ?Group ❙
	include ?Abelian ❙
❚
	
theory Ring : ?NatDed =
	/T We will add two structures, one for addition and one for multiplication. ❙
	/T Addition forms an abelian group, hence we will use that theory for our structure. ❙
	/T In the structure, we first give the universe u a new ALIAS R. This way, we don't
		have to refer to the universe of our Ring with add/u all the time. ❙
	/T Afterwards, we provide new notations for the other symbols. Note, that none of the symbols
			we "modify" are declared directly in the theory we're including (i.e. AbelianGroup).
			Structures can modify along includes without problems. ❙
	structure add : ?AbelianGroup =
		u @ R ❙
		comp # 1 + 2 prec 40 ❙
		unit # O ❙
		inverse # - 1 ❙
	❚
	/T We can now add a DEFINITION to Multiplication/u, making it equal to R=Addition/u. 
		That way, both + and ⋅ are defined on the SAME
		universe (i.e. R), while being two separate operations nonetheless (as opposed to when
		using plain includes): ❙
	structure mult : ?Monoid =
		u = R ❙
		comp # 1 ⋅ 2 prec 45 ❙
		unit # I ❙
	❚
	/T Alternatively we could have defined mult/u directly as add/u
		
	/T Finally, we can use the symbols in our structures jointly in distributivity: ❙
		
	distributive : ⊢ ∀[a]∀[b]∀[c] a ⋅ (b + c) = a ⋅ b + a ⋅ c ❙
❚