17 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var: |
17 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var: |
18 Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *) |
18 Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *) |
19 |
19 |
20 (*.used for calculating built in binary operations in Isabelle2002. |
20 (*.used for calculating built in binary operations in Isabelle2002. |
21 integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*) |
21 integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*) |
22 fun calc "op +" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*) |
22 fun calc "Groups.plus_class.plus" ((a, b), _:int * int) ((c, d), _:int * int) = (*FIXME.WN1008 drop Float.calc, var_op_float, float_op_var, term_of_float*) |
23 if b < d |
23 if b < d |
24 then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*) |
24 then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*) |
25 else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*) |
25 else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*) |
26 | calc "op -" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*) |
26 | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*) |
27 ((a - c,0),(0,0)) |
27 ((a - c,0),(0,0)) |
28 | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*) |
28 | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*) |
29 ((a * c, b + d), (0, 0)) |
29 ((a * c, b + d), (0, 0)) |
30 | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*) |
30 | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*) |
31 ((a div c, 0), (0, 0)) |
31 ((a div c, 0), (0, 0)) |
32 | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*) |
32 | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*) |
33 ((power a c, 0), (0, 0)) |
33 ((power a c, 0), (0, 0)) |
34 | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) = |
34 | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) = |
35 raise error ("calc: not impl. for Float (("^ |
35 raise error ("calc: not impl. for Float (("^ |
36 (string_of_int a )^","^(string_of_int b )^"), ("^ |
36 (string_of_int a )^","^(string_of_int b )^"), ("^ |
37 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^ |
37 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^ |
38 (string_of_int c )^","^(string_of_int d )^"), ("^ |
38 (string_of_int c )^","^(string_of_int d )^"), ("^ |
39 (string_of_int p21)^","^(string_of_int p22)^"))"); |
39 (string_of_int p21)^","^(string_of_int p22)^"))"); |
40 (*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0)); |
40 (*> calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0)); |
41 val it = ((1,0),(0,0))*) |
41 val it = ((1,0),(0,0))*) |
42 |
42 |
43 (*.convert internal floatingpoint prepresentation to int and float.*) |
43 (*.convert internal floatingpoint prepresentation to int and float.*) |
44 fun term_of_float T ((val1, 0), ( 0, 0)) = |
44 fun term_of_float T ((val1, 0), ( 0, 0)) = |
45 term_of_num T val1 |
45 term_of_num T val1 |
74 (Free (str_of_int v2, T))) |
74 (Free (str_of_int v2, T))) |
75 (pairt (Free (str_of_int p1, T)) |
75 (pairt (Free (str_of_int p1, T)) |
76 (Free (str_of_int p2, T))))) |
76 (Free (str_of_int p2, T))))) |
77 end; |
77 end; |
78 (*> val t = str2term "a + b"; |
78 (*> val t = str2term "a + b"; |
79 > val Const ("op +", optype) $ _ $ _ = t; |
79 > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t; |
80 > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v"; |
80 > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v"; |
81 > t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0)); |
81 > t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0)); |
82 val it = true : bool*) |
82 val it = true : bool*) |
83 |
83 |
84 (*.assoc. convert internal floatingpoint prepresentation to int and float.*) |
84 (*.assoc. convert internal floatingpoint prepresentation to int and float.*) |
85 fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) = |
85 fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) = |
86 num_op_var v op_ optype ntyp v1 |
86 num_op_var v op_ optype ntyp v1 |
92 (Free (str_of_int v2, T))) |
92 (Free (str_of_int v2, T))) |
93 (pairt (Free (str_of_int p1, T)) |
93 (pairt (Free (str_of_int p1, T)) |
94 (Free (str_of_int p2, T))))) $ v |
94 (Free (str_of_int p2, T))))) $ v |
95 end; |
95 end; |
96 (*> val t = str2term "a + b"; |
96 (*> val t = str2term "a + b"; |
97 > val Const ("op +", optype) $ _ $ _ = t; |
97 > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t; |
98 > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v"; |
98 > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v"; |
99 > t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0)); |
99 > t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0)); |
100 val it = true : bool*) |
100 val it = true : bool*) |
101 *} |
101 *} |
102 |
102 |
103 end |
103 end |