text_formalization/jordan/float_example.hl

   1
   2 reneeds "jordan/float.hl";;
   3
   4 Float.REAL_INEQUALITY_CALCULATOR []  `#3.1415 < #4.0 * atn  (&1) /\ #4.0 * atn (&1) < #3.142`;;
   5
   6 Float.REAL_INEQUALITY_CALCULATOR []  `#1.26 < acs(#0.3) /\ acs (#0.3) < #1.27`;;
   7
   8 acos (0.3);;
   9
  10 Float.REAL_INEQUALITY_CALCULATOR []  `#3.14159 < pi`;;
  11
  12 Float.INTERVAL_OF_TERM [] [] 5 `&7 + (\i. &i pow 2) 1`;;
  13
  14 Float.FLOAT_CONV `float (int_of_num 3) (int_of_num 20)  <= float (int_of_num 3) (int_of_num 7) +. (float (int_of_num 4) (-- int_of_num 13))`;;
  15
  16 Float.FLOAT_LESS_CONV `&0 <   float (int_of_num 3) (int_of_num 7) -. (float (int_of_num 4) (-- int_of_num 13))`;;
  17
  18 Float.REAL_INEQUALITY_CALCULATOR []
  19   `-- (sum (0..1) (\i. (&i) pow 2)) < &1000`;;
  20
  21 Float.REAL_INEQUALITY_CALCULATOR []
  22    `cos (&3) < pi`;;
  23
  24 let rjrj = new_definition `rjrj = sqrt(&3)`;;
  25
  26 Float.REAL_INEQUALITY_CALCULATOR [("rjrj",PURE_ONCE_REWRITE_CONV[rjrj])]
  27    `rjrj < #1.73206`;;
  28
  29 let jrjr = new_definition `jrjr x = sqrt(x)`;;
  30
  31 Float.REAL_INEQUALITY_CALCULATOR [("rjrj",PURE_ONCE_REWRITE_CONV[rjrj]);
  32    ("jrjr",PURE_ONCE_REWRITE_CONV[jrjr])]
  33    `#1.31607 < jrjr rjrj /\ jrjr rjrj < #1.31608`;;
  34
  35 Pervasives.sqrt(Pervasives.sqrt(3.0));;
  36
  37 let rkkk = new_definition `rkkk x y z = (x * y) pow 2 + z`;;
  38
  39 Float.REAL_INEQUALITY_CALCULATOR [("rkkk",PURE_ONCE_REWRITE_CONV[rkkk])]
  40    `rkkk (&2) (&3) (&4) < #40.1`;;
  41
  42 Float.REAL_INEQUALITY_CALCULATOR []
  43   `#0.019 < abs (&3 - #3.02)`;;
  44
  45 Float.REAL_INEQUALITY_CALCULATOR []
  46   `pi + #0.019 < abs (&3 - #3.02)`;;
  47
  48
  49 Float.REAL_INEQUALITY_CALCULATOR []
  50   `sum (5..7) (\i. (&i) pow 2) < &1000`;;
  51
  52 Float.REAL_INEQUALITY_CALCULATOR [] `#12.91553 < #1.29155 pow 10 /\ #1.29155 pow 10 < #12.91554`;;
  53
  54 Float.REAL_INEQUALITY_CALCULATOR [] `#0.05 < &3 / (sqrt(&2) - #1.41)`;;
  55 Float.REAL_INEQUALITY_CALCULATOR [] `#0.05 * #0.04 - #0.3 < &3 / (sqrt(&2) - #1.41)`;;
  56
  57 Float.INTERVAL_DIV;;
  58
  59 3.0 /. (Pervasives.sqrt(2.0) -. 1.0);;
  60
  61 Float.REAL_INEQUALITY_CALCULATOR [] `((\t. t + &1) #12.0) < #15.0 `;;
  62
  63 BETA_CONV `((\t. t + &1) #12.0)`;;
  64
  65 Float.REAL_INEQUALITY_CALCULATOR [] `-- ((\t. &t + &1) 3) < -- #3.0`;;
  66
  67 Float.REAL_INEQUALITY_CALCULATOR [] `#1.4142135 < sqrt(&2) /\ (sqrt(&2) < #1.4142136)`;;
  68
  69 Float.REAL_INEQUALITY_CALCULATOR []
  70 `#4.059107977120 < sqrt(&7 / #3.2) + sqrt(&4 * sqrt(&2) + &1) /\
  71   sqrt(&7 / #3.2) + sqrt(&4 * sqrt(&2) + &1)< #4.059107977121`;;
  72
  73 Float.INTERVAL_DIV;;
  74
  75 Float.REAL_INEQUALITY_CALCULATOR [] `sqrt( #0.001 ) < #0.00001`;;
  76
  77 Float.REAL_INEQUALITY_CALCULATOR [] `&1/ &0  < #0.00001`;;
  78 Float.REAL_INEQUALITY_CALCULATOR []
  79   `(\i. (&i) pow 2 + (&i)) 33 <  &1000000`;;