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