Natural Numbers: Basic theorems

 

   fun nat_diagonal f _ a b = f a b if a and b stem from the same constructor
      |nat_diagonal _ g a b = g a b

   fun nat_diagonal_const f _ a b = f if a and b stem from the same constructor
      |nat_diagonal_const g _ _ _ = g

   val nat_filter = nat_diagonal_const unit empty

   fun nat_Thm 0       0       = unit
      |nat_Thm 0       (suc n) = {n:nat}(Eq 0 (suc n))->empty
      |nat_Thm (suc m) 0       = {m:nat}(Eq (suc m) 0)->empty
      |nat_Thm (suc m) (suc n) = injective suc

 ** Module lib_ML_nat Imports lib_empty lib_unit lib_nat
  nat_diagonal = ... : {C|Type}(nat->nat->C)->(nat->nat->C)->nat->nat->C
  nat_diagonal_const = ... : {C|Type}C->C->nat->nat->C
  nat_filter = ... : nat->nat->Type
  f = ... : nat->Type
  g = ... : nat->Type
  nat_Thm = ... : nat->nat->Type
  get_filter = ... : {m,n|nat}(Eq m n)->Type
  nat_thm = ... : {u,v:nat}nat_Thm u v