1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* External Rational Number Operations *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
13 | Hol_light of bool*term;; (* true if changed *)
18 | Big_int of Big_int.big_int
19 | Ratio of Ratio.ratio ///;;
21 let internalize_bool = function
27 let amp = `real_of_num` in
28 fun x -> mk_comb (amp,x);;
31 let real_div = `real_div` in
32 let quot n d = mk_binop real_div (realize n) (realize d) in
34 let n = mk_numeral(Big_int (Ratio.numerator_ratio x)) in
35 let d = mk_numeral(Big_int (Ratio.denominator_ratio x)) in
42 | Big_int _ -> realize(mk_numeral a)
43 | Int x -> realize (mk_small_numeral x)
44 | Ratio x -> real_of_rat x)
47 | Big_int _ ->(mk_numeral a)
48 | Int x -> (mk_small_numeral x)
49 | Ratio _ -> failwith "unnatural quotient")
50 | Hol_light (changed,t) -> t;;
52 let dest_binop_from oplist t =
53 let (h,y)= dest_comb t in
54 let (op,x) = dest_comb h in
55 if (mem op oplist) then (op,x,y) else failwith "op not found";;
61 let num_trunc_minus x y = if ( y >/ x) then zero else x -/ y;;
63 let rat_div x y = if (y =/ zero) then zero else (x // y);;
65 let rat_inv x = if (x =/ zero) then zero else (one // x);;
67 let mk_cty ty = map (fun (a,b)-> (mk_mconst(a,ty),b));;
70 let real_rels = mk_cty `:real->real->bool`
71 ["real_lt";"real_le";"=";"real_ge";"real_gt"];;
73 let num_rels = mk_cty `:num->num->bool`
74 ["<=";"<";"=";">=";">="];;
77 let real_binop = mk_cty `:real->real->real`
78 [("real_add",( +/ ));("real_sub", ( -/ ));("real_mul", ( */ ));("real_div",rat_div)];;
80 let num_binop = mk_cty `:num->num->num`
81 [("+",( +/ ));("-",num_trunc_minus);("*", ( */ ))];;
83 let dec_op = mk_cty `:num->num->real`
84 [("DECIMAL",( // ))];;
86 let numeral_op = mk_cty `:num->real` ["real_of_num",I];;
88 let real_unary = mk_cty `:real->real` [("real_neg",minus_num);("real_inv",rat_inv)];;
91 let lift (a,b) x = function;;
94 let rec mixed_of_term arith = function
95 | Var _ as u -> Hol_light (false,u)
96 | Const _ as u -> Hol_light (false,u)
97 | Abs(x,t) as u -> let t' = mixed_of_term false t in
99 | Hol_light (false,_) -> Hol_light (false,u)
100 | _ -> Hol_light (true,mk_abs(x, term_of_mixed t')))
102 | Const (h,y) as u -> Hol_lightu;;
109 let mixedalize t = t;;
116 let v = Int 3 // Int 4;;
117 let rec sqx n v = if (n = 0) then Int 1 else if (n=1) then v else (sqx (n-1) v)*/ (sqx (n-1) v);;