namespace http://cds.omdoc.org/urtheories❚

theory NatSymbols =
	include ?TermsTypesKinds ❙
	NAT : type ❙
	zero : NAT ❙
❚

theory NatArith : ?LF =
  include ?NatSymbols ❙
  succ  : NAT ⟶ NAT      ❙
  one   : NAT             ❘
        = succ zero           ❙
  plus  : NAT ⟶ NAT ⟶ NAT ❙
  times : NAT ⟶ NAT ⟶ NAT ❙
❚

theory NatRels : ?Ded =
  include ?NatArith ❙
  LEQ   : NAT ⟶ NAT ⟶ BOOL ❘ # 1 LEQ 2 prec 5❙
  LESS  : NAT ⟶ NAT ⟶ BOOL ❘ # 1 LESS 2 prec 5❘
        = [m,n] (succ m) LEQ n❙
  REFL  : {n} DED n LEQ n❙
❚

theory NatRules : ?DHOL =
  include ?NatRels ❙

  eq_leq : {X,Y,Z} DED X EQ Y ⟶ DED Y LEQ Z ⟶ DED X LEQ Z  ❙
  leq_eq : {X,Y,Z} DED X LEQ Y ⟶ DED Y EQ Z ⟶ DED X LEQ Z  ❙
  
  plus_comm  : {X,Y} DED plus X Y EQ plus Y X  ❙
  plus_assoc : {X,Y,Z} DED plus (plus X Y) Z EQ plus X (plus Y Z) ❙
  plus_neut_Ex : {X} DED plus X zero EQ X ❘ # %%prefix 0 1❙
  plus_neut    : {X} DED plus X zero EQ X ❘ = [X] plus_neut_Ex X ❘role Simplify ❙
  
  plus_succ_R : {X,Y} DED plus X (succ Y) EQ succ (plus X Y)❘role Simplify ❙
  plus_succ_L : {X,Y} DED plus (succ X) Y EQ succ (plus X Y) ❘role Simplify ❙
  
  times_comm  : {X,Y} DED times X Y EQ times Y X  ❙
  times_assoc : {X,Y,Z} DED times (times X Y) Z EQ times X (times Y Z)  ❙
  times_neut  : {X} DED times X one EQ X❘role Simplify  ❙
  
  times_zero  : {X} DED times X zero EQ zero❘role Simplify  ❙
  times_succ_R : {X,Y} DED times X (succ Y) EQ plus (times X Y) X❘role Simplify ❙
  times_succ_L : {X,Y} DED times (succ X) Y EQ plus (times X Y) X❘role Simplify ❙

  distrib     : {X,Y,Z} DED times X (plus Y Z) EQ plus (times X Y) (times X Z) ❘role Simplify❙
  
  leq_refl    : {X} DED X LEQ X  ❙
  leq_trans   : {X,Y,Z} DED X LEQ Y ⟶ DED Y LEQ Z ⟶ DED X LEQ Z    ❙
  leq_antisym : {X,Y} DED X LEQ Y ⟶ DED Y LEQ X ⟶ DED X EQ Y      ❙
  
  plus_mono     : {X,Y,Z} DED X LEQ Y ⟶ DED (plus X Z) LEQ (plus Y Z)  ❙
  plus_mono_L   : {X,Y,Z} DED X LEQ Y ⟶ DED (plus Z X) LEQ (plus Z Y)  ❘ 
                = [X,Y,Z,p] leq_eq (eq_leq plus_comm (plus_mono p)) plus_comm❙
  plus_invmono  : {X,Y,Z} DED (plus X Z) LEQ (plus Y Z) ⟶ DED X LEQ Y  ❙

  theory NatOnly : ?DHOL =
    least         : {X} DED zero LEQ X ❙
    plus_larger_L : {X,Y} DED X LEQ (plus X Y)  ❘
                  = [X][Y] eq_leq (SYM plus_neut) (plus_mono_L least)  ❙
    plus_larger_R : {X,Y} DED Y LEQ (plus X Y)  ❘
                  = [X][Y] leq_eq plus_larger_L plus_comm❙
    times_mono    : {X,Y,Z} DED X LEQ Y ⟶ DED (times X Z) LEQ (times Y Z)  ❙
    times_invmono : {X,Y,Z} DED (times X Z) LEQ (times Y Z) ⟶ DED X LEQ Y  ❙
  ❚
❚

import rules scala://lf.mmt.kwarc.info❚
import uom scala://uom.api.mmt.kwarc.info❚

theory NatLiteralsOnly =
  include ?NatSymbols ❙
  rule rules?Realize NAT uom?StandardNat❙
  rule rules?Realize zero uom?Arithmetic/Zero❙
❚
    
theory NatLiterals : ?LF =
  include ?NatLiteralsOnly ❙
  include ?NatArith❙
  rule rules?Realize one uom?Arithmetic/One❙
  rule rules?Realize succ uom?Arithmetic/Succ❙
❚

theory Nat : ?DHOL =
  include ?NatSymbols❙
  include ?NatRules❙
  include ?NatRules/NatOnly❙
  include ?NatLiterals❙
❚