updated "op +", "op -", "op *". "HOL.divide" in src & test
find . -type f -exec sed -i s/"\"op +\""/"\"Groups.plus_class.plus\""/g {} \;
find . -type f -exec sed -i s/"\"op -\""/"\"Groups.minus_class.minus\""/g {} \;
find . -type f -exec sed -i s/"\"op *\""/"\"Groups.times_class.times\""/g {} \;
find . -type f -exec sed -i s/"\"HOL.divide\""/"\"Rings.inverse_class.divide\""/g {} \;
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)"
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 *)
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)*)
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*)
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*)
26 | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
28 | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
29 ((a * c, b + d), (0, 0))
30 | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
31 ((a div c, 0), (0, 0))
32 | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
33 ((power a c, 0), (0, 0))
34 | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
35 raise error ("calc: not impl. for Float (("^
36 (string_of_int a )^","^(string_of_int b )^"), ("^
37 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
38 (string_of_int c )^","^(string_of_int d )^"), ("^
39 (string_of_int p21)^","^(string_of_int p22)^"))");
40 (*> calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0));
41 val it = ((1,0),(0,0))*)
43 (*.convert internal floatingpoint prepresentation to int and float.*)
44 fun term_of_float T ((val1, 0), ( 0, 0)) =
46 | term_of_float T ((val1, val2), (precision1, precision2)) =
47 let val pT = pairT T T
48 in Const ("Float.Float", (pairT pT pT) --> T)
49 $ (pairt (pairt (Free (str_of_int val1, T))
50 (Free (str_of_int val2, T)))
51 (pairt (Free (str_of_int precision1, T))
52 (Free (str_of_int precision2, T))))
54 (*> val t = str2term "Float ((1,2),(0,0))";
55 > val Const ("Float.Float", fT) $ _ = t;
57 > val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
58 > (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
63 t = float_term_of_num HOLogic.realT ((1,2),(0,0));
64 val it = true : bool*)
66 (*.assoc. convert internal floatingpoint prepresentation to int and float.*)
67 fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
68 var_op_num v op_ optype ntyp v1
69 | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
70 let val pT = pairT T T
71 in Const (op_, optype) $ v $
72 (Const ("Float.Float", (pairT pT pT) --> T)
73 $ (pairt (pairt (Free (str_of_int v1, T))
74 (Free (str_of_int v2, T)))
75 (pairt (Free (str_of_int p1, T))
76 (Free (str_of_int p2, T)))))
78 (*> val t = str2term "a + b";
79 > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
80 > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
81 > t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
82 val it = true : bool*)
84 (*.assoc. convert internal floatingpoint prepresentation to int and float.*)
85 fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
86 num_op_var v op_ optype ntyp v1
87 | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
88 let val pT = pairT T T
89 in Const (op_,optype) $
90 (Const ("Float.Float", (pairT pT pT) --> T)
91 $ (pairt (pairt (Free (str_of_int v1, T))
92 (Free (str_of_int v2, T)))
93 (pairt (Free (str_of_int p1, T))
94 (Free (str_of_int p2, T))))) $ v
96 (*> val t = str2term "a + b";
97 > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
98 > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
99 > t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
100 val it = true : bool*)