text_formalization/leg/abc_of_quadratic_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: abc_of_quadratic                                               *)
   5 (* Chapter: LEG                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-02-07                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 (*
  14 f = \x. a x^2 + b x + c, extract a b c
  15 *)
  16
  17
  18 (* moved to sphere.hl.  This file is deprecated  *)
  19
  20 module type Abc_of_quadratic_def_type = sig
  21   val abc_of_quadratic : thm
  22 end;;
  23
  24
  25
  26 module Abc_of_quadratic : Abc_of_quadratic_def_type = struct
  27
  28  let abc_of_quadratic =
  29 new_definition `abc_of_quadratic f =
  30   let c = f (&0) in
  31   let  p = f (&1) in
  32   let n = f (-- &1) in
  33   ((p + n)/(&2) - c, (p -n)/(&2), c)` ;;
  34
  35 end;;
  36