|
1 (* Title: quick and dirty for quick update Isabelle2002 --> Isabelle2009-2 |
|
2 Author: Walther Neuper 000301 |
|
3 (c) due to copyright terms |
|
4 *) |
|
5 |
|
6 theory Delete imports "../ProgLang/Language" begin |
|
7 |
|
8 axioms (* theorems which are available only with long names, |
|
9 which can not yet be handled in isac's scripts *) |
|
10 |
|
11 real_mult_left_commute "z1 * (z2 * z3) = z2 * (z1 * z3)" |
|
12 (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*) |
|
13 |
|
14 |
|
15 ML {* |
|
16 (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var: |
|
17 Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *) |
|
18 |
|
19 (*.used for calculating built in binary operations in Isabelle2002. |
|
20 integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*) |
|
21 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 if b < d |
|
23 then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*) |
|
24 else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*) |
|
25 | calc "op -" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*) |
|
26 ((a - c,0),(0,0)) |
|
27 | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*) |
|
28 ((a * c, b + d), (0, 0)) |
|
29 | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*) |
|
30 ((a div c, 0), (0, 0)) |
|
31 | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*) |
|
32 ((power a c, 0), (0, 0)) |
|
33 | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) = |
|
34 raise error ("calc: not impl. for Float (("^ |
|
35 (string_of_int a )^","^(string_of_int b )^"), ("^ |
|
36 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^ |
|
37 (string_of_int c )^","^(string_of_int d )^"), ("^ |
|
38 (string_of_int p21)^","^(string_of_int p22)^"))"); |
|
39 (*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0)); |
|
40 val it = ((1,0),(0,0))*) |
|
41 |
|
42 (*.convert internal floatingpoint prepresentation to int and float.*) |
|
43 fun term_of_float T ((val1, 0), ( 0, 0)) = |
|
44 term_of_num T val1 |
|
45 | term_of_float T ((val1, val2), (precision1, precision2)) = |
|
46 let val pT = pairT T T |
|
47 in Const ("Float.Float", (pairT pT pT) --> T) |
|
48 $ (pairt (pairt (Free (str_of_int val1, T)) |
|
49 (Free (str_of_int val2, T))) |
|
50 (pairt (Free (str_of_int precision1, T)) |
|
51 (Free (str_of_int precision2, T)))) |
|
52 end; |
|
53 (*> val t = str2term "Float ((1,2),(0,0))"; |
|
54 > val Const ("Float.Float", fT) $ _ = t; |
|
55 > atomtyp fT; |
|
56 > val ffT = (pairT (pairT HOLogic.realT HOLogic.realT) |
|
57 > (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT; |
|
58 > atomtyp ffT; |
|
59 > fT = ffT; |
|
60 val it = true : bool |
|
61 |
|
62 t = float_term_of_num HOLogic.realT ((1,2),(0,0)); |
|
63 val it = true : bool*) |
|
64 |
|
65 (*.assoc. convert internal floatingpoint prepresentation to int and float.*) |
|
66 fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) = |
|
67 var_op_num v op_ optype ntyp v1 |
|
68 | var_op_float v op_ optype T ((v1, v2), (p1, p2)) = |
|
69 let val pT = pairT T T |
|
70 in Const (op_, optype) $ v $ |
|
71 (Const ("Float.Float", (pairT pT pT) --> T) |
|
72 $ (pairt (pairt (Free (str_of_int v1, T)) |
|
73 (Free (str_of_int v2, T))) |
|
74 (pairt (Free (str_of_int p1, T)) |
|
75 (Free (str_of_int p2, T))))) |
|
76 end; |
|
77 (*> val t = str2term "a + b"; |
|
78 > val Const ("op +", optype) $ _ $ _ = t; |
|
79 > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v"; |
|
80 > t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0)); |
|
81 val it = true : bool*) |
|
82 |
|
83 (*.assoc. convert internal floatingpoint prepresentation to int and float.*) |
|
84 fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) = |
|
85 num_op_var v op_ optype ntyp v1 |
|
86 | float_op_var v op_ optype T ((v1, v2), (p1, p2)) = |
|
87 let val pT = pairT T T |
|
88 in Const (op_,optype) $ |
|
89 (Const ("Float.Float", (pairT pT pT) --> T) |
|
90 $ (pairt (pairt (Free (str_of_int v1, T)) |
|
91 (Free (str_of_int v2, T))) |
|
92 (pairt (Free (str_of_int p1, T)) |
|
93 (Free (str_of_int p2, T))))) $ v |
|
94 end; |
|
95 (*> val t = str2term "a + b"; |
|
96 > val Const ("op +", optype) $ _ $ _ = t; |
|
97 > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v"; |
|
98 > t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0)); |
|
99 val it = true : bool*) |
|
100 *} |
|
101 |
|
102 end |