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

theory Bool : http://cds.omdoc.org/urtheories?LF =
  bool  : type
  true  : bool
  false  : bool


theory Logic : http://cds.omdoc.org/urtheories?LF =
  include ?Bool
  ded   : bool ⟶ type #  1 prec -5  role Judgment
  trueI : ⊦ true

  
theory Nat : http://cds.omdoc.org/urtheories?LF =
  nat   : type
  zero  : nat              # O 
  succ  : nat ⟶ nat       # 1 ' prec 20
  one   : nat             
        = zero'            # I 
  plus  : nat ⟶ nat ⟶ nat  # 1 + 2 prec 10 
  times : nat ⟶ nat ⟶ nat  # 1 * 2 prec 15 
  
  include ?Bool
  equal : nat ⟶ nat ⟶ bool  # 1 = 2 prec 5role Eq
  leq   : nat ⟶ nat ⟶ bool  # 1  2 prec 5


theory NatRules : http://cds.omdoc.org/urtheories?LF =
  include ?Logic
  include ?Nat 

  refl  : {X} ⊦ X = X  
  sym   : {X,Y} ⊦ X = Y ⟶ ⊦ Y = X 
  trans : {X,Y,Z} ⊦ X = Y ⟶ ⊦ Y = Z ⟶ ⊦ X = Z 
  
  eq_leq : {X,Y,Z} ⊦ X = Y ⟶ ⊦ Y ≤ Z ⟶ ⊦ X ≤ Z  
  leq_eq : {X,Y,Z} ⊦ X ≤ Y ⟶ ⊦ Y = Z ⟶ ⊦ X ≤ Z  
  
  plus_comm  : {X,Y} ⊦ X + Y = Y + X  
  plus_assoc : {X,Y,Z} ⊦ (X + Y) + Z = X + (Y + Z) 
  plus_neut_Ex : {X} ⊦ X + O = X  # %%prefix 0 1
  plus_neut_L  : {X} ⊦ O + X = X = [X] trans plus_comm (plus_neut_Ex X) role Simplify 
  plus_neut    : {X} ⊦ X + O = X  = [X] plus_neut_Ex X role Simplify 
  
  plus_succ_R : {X,Y} ⊦ X + Y' = (X+Y)'role Simplify 
  plus_succ_L : {X,Y} ⊦ X' + Y = (X+Y)'role Simplify 
  
  times_comm  : {X,Y} ⊦ X * Y = Y * X  
  times_assoc : {X,Y,Z} ⊦ (X * Y) * Z = X * (Y * Z)  
  times_neut  : {X} ⊦ X * I = Xrole Simplify  
  
  times_zero  : {X} ⊦ X * O = Orole Simplify  
  times_succ_R : {X,Y} ⊦ X * Y' = (X*Y) + Xrole Simplify 
  times_succ_L : {X,Y} ⊦ X' * Y = (X*Y) + Xrole Simplify 

  distrib     : {X,Y,Z} ⊦ X * (Y + Z) = X * Y + X * Zrole Simplify
  
  leq_refl    : {X} ⊦ X≤X  
  leq_trans   : {X,Y,Z} ⊦ X≤Y ⟶ ⊦ Y≤Z ⟶ ⊦ X≤Z    
  leq_antisym : {X,Y} ⊦ X≤Y ⟶ ⊦ Y≤X ⟶ ⊦ X=Y      
  
  plus_mono     : {X,Y,Z} ⊦ X≤Y ⟶ ⊦ X+Z ≤ Y+Z  
  plus_mono_L   : {X,Y,Z} ⊦ X≤Y ⟶ ⊦ Z+X ≤ Z+Y   
                = [X,Y,Z,p] leq_eq (eq_leq plus_comm (plus_mono p)) plus_comm
  plus_invmono  : {X,Y,Z} ⊦ X+Z≤Y+Z ⟶ ⊦ X≤Y  

  theory NatOnly : http://cds.omdoc.org/urtheories?LF =
    least         : {X} ⊦ O ≤ X 
    plus_larger_L : {X,Y} ⊦ X≤X+Y  
                  = [X][Y] eq_leq (sym plus_neut) (plus_mono_L least)  
    plus_larger_R : {X,Y} ⊦ Y≤X+Y  
                  = [X][Y] leq_eq plus_larger_L plus_comm
    times_mono    : {X,Y,Z} ⊦ X ≤ Y ⟶ ⊦ X * Z ≤ Y * Z  
    times_invmono : {X,Y,Z} ⊦ X * Z ≤ Y * Z ⟶ ⊦ X ≤ Y  
  

  
theory NatMinus : http://cds.omdoc.org/urtheories?LF =
  include ?NatRules 
  include ?NatRules/NatOnly
 
  // A partial subtraction operation that takes a proof of definedness as a 3rd argument. ❙
  minus    : {X,Y} ⊦ Y≤X ⟶ nat   # 1 - 2 ! 3 prec 15   ## 1 - 2 %I3
  minus_pi : {X,Y,P,Q} ⊦ X-Y!P = X-Y!Q                  

  minus_intro_L : {X,Y,Z} {p: ⊦ X+Y=Z} ⊦ Z-Y!(leq_eq plus_larger_R p) = X  
  minus_intro_R : {X,Y,Z} {p: ⊦ X+Y=Z} ⊦ Z-X!(leq_eq plus_larger_L p) = Y   
                = [X,Y,Z] [p] trans minus_pi (minus_intro_L (trans plus_comm p))
  minus_elim    : {X,Y,Z,P} ⊦ Z-Y!P = X  ⟶  ⊦ X+Y = Z                      

  
  // minus_inverse : {X} ⊦ X-X!leq_refl = O  ❘
                = [X] trans minus_pi (minus_intro_R (plus_neut_Ex X)) ❙
  // minus_neut    : {X} ⊦ X-O!least = X ❘
                = [X] trans minus_pi (minus_intro_L (plus_neut_Ex X))  ❙
  // also provable: associativity +- (maybe X-(Y+Z)=(X-Y)-Z must be axiom) and distributivity *- ❙