Structure reduceTheory

signature reduceTheory =
sig
  type thm = Thm.thm
  
  (*  Theorems  *)
    val div_thm : thm
    val mod_thm : thm
    val num_case_compute_lazy : thm
(*
   [arithmetic] Parent theory of "reduce"
   
   [div_thm]  Theorem
      
      ⊢ ∀x y q r. x DIV y = if x = q * y + r ∧ r < y then q else x DIV y
   
   [mod_thm]  Theorem
      
      ⊢ ∀x y q r. x MOD y = if x = q * y + r ∧ r < y then r else x MOD y
   
   [num_case_compute_lazy]  Theorem
      
      ⊢ num_CASE = (λn f g. if n = 0 then f else g (PRE n))
   
   
*)
end

HOL 4, Trindemossen-2