neuper@37965: (* Title:  quick and dirty for quick update Isabelle2002 --> Isabelle2009-2
neuper@37965:    Author: Walther Neuper 000301
neuper@37965:    (c) due to copyright terms
neuper@37965: *)
neuper@37965: 
neuper@37965: theory Delete imports "../ProgLang/Language" begin
neuper@37965: 
neuper@37965: axioms (* theorems which are available only with long names,
neuper@37965:           which can not yet be handled in isac's scripts *)
neuper@37965: 
neuper@37974:   real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)"
neuper@37965:  (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*)
neuper@37974:   real_mult_minus1:       "-1 * z = - (z::real)"
neuper@37974:   real_mult_2:            "2 * z = z + (z::real)"
neuper@37965: 
neuper@37965: ML {* 
neuper@37965: (* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var:
neuper@37965:    Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)
neuper@37965: 
neuper@37965: (*.used for calculating built in binary operations in Isabelle2002.
neuper@37965:    integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)
neuper@38014: 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*)
neuper@37965:     if b < d 
neuper@37965:     then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
neuper@37965:     else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
neuper@38014:   | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)
neuper@37965:     ((a - c,0),(0,0))
neuper@37965:   | calc "op *" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)
neuper@37965:     ((a * c, b + d), (0, 0))
neuper@38014:   | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
neuper@37965:     ((a div c, 0), (0, 0))
neuper@37965:   | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
neuper@37965:     ((power a c, 0), (0, 0))
neuper@37965:   | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) = 
neuper@38031:     error ("calc: not impl. for Float (("^
neuper@37965: 		 (string_of_int a  )^","^(string_of_int b  )^"), ("^
neuper@37965: 		 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
neuper@37965: 		 (string_of_int c  )^","^(string_of_int d  )^"), ("^
neuper@37965: 		 (string_of_int p21)^","^(string_of_int p22)^"))");
neuper@38014: (*> calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0)); 
neuper@37965: val it = ((1,0),(0,0))*)
neuper@37965: 
neuper@37965: (*.convert internal floatingpoint prepresentation to int and float.*)
neuper@37965: fun term_of_float T ((val1,    0), (         0,          0)) =
neuper@37965:     term_of_num T val1
neuper@37965:   | term_of_float T ((val1, val2), (precision1, precision2)) =
neuper@37965:     let val pT = pairT T T
neuper@37965:     in Const ("Float.Float", (pairT pT pT) --> T)
neuper@37965: 	     $ (pairt (pairt (Free (str_of_int val1, T))
neuper@37965: 			     (Free (str_of_int val2, T)))
neuper@37965: 		      (pairt (Free (str_of_int precision1, T))
neuper@37965: 			     (Free (str_of_int precision2, T))))
neuper@37965:     end;
neuper@37965: (*> val t = str2term "Float ((1,2),(0,0))";
neuper@37965: > val Const ("Float.Float", fT) $ _ = t;
neuper@37965: > atomtyp fT;
neuper@37965: > val ffT = (pairT (pairT HOLogic.realT HOLogic.realT) 
neuper@37965: > 	     (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
neuper@37965: > atomtyp ffT;
neuper@37965: > fT = ffT;
neuper@37965: val it = true : bool
neuper@37965: 
neuper@37965: t = float_term_of_num HOLogic.realT ((1,2),(0,0));
neuper@37965: val it = true : bool*)
neuper@37965: 
neuper@37965: (*.assoc. convert internal floatingpoint prepresentation to int and float.*)
neuper@37965: fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
neuper@37965:     var_op_num v op_ optype ntyp v1
neuper@37965:   | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
neuper@37965:     let val pT = pairT T T
neuper@37965:     in Const (op_, optype) $ v $ 
neuper@37965: 	     (Const ("Float.Float", (pairT pT pT) --> T)
neuper@37965: 		    $ (pairt (pairt (Free (str_of_int v1, T))
neuper@37965: 				    (Free (str_of_int v2, T)))
neuper@37965: 			     (pairt (Free (str_of_int p1, T))
neuper@37965: 				    (Free (str_of_int p2, T)))))
neuper@37965:     end;
neuper@37965: (*> val t = str2term "a + b";
neuper@38014: > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
neuper@37965: > val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
neuper@38014: > t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
neuper@37965: val it = true : bool*)
neuper@37965: 
neuper@37965: (*.assoc. convert internal floatingpoint prepresentation to int and float.*)
neuper@37965: fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
neuper@37965:     num_op_var v op_ optype ntyp v1
neuper@37965:   | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
neuper@37965:     let val pT = pairT T T
neuper@37965:     in Const (op_,optype) $ 
neuper@37965: 	     (Const ("Float.Float", (pairT pT pT) --> T)
neuper@37965: 		    $ (pairt (pairt (Free (str_of_int v1, T))
neuper@37965: 				    (Free (str_of_int v2, T)))
neuper@37965: 			     (pairt (Free (str_of_int p1, T))
neuper@37965: 				    (Free (str_of_int p2, T))))) $ v
neuper@37965:     end;
neuper@37965: (*> val t = str2term "a + b";
neuper@38014: > val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;
neuper@37965: > val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
neuper@38014: > t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));
neuper@37965: val it = true : bool*)
neuper@37965: *}
neuper@37965: 
neuper@37965: end