(* Title:  quick and dirty for quick update Isabelle2002 --> Isabelle2009-2

   Author: Walther Neuper 000301

   (c) due to copyright terms

*)

theory Delete imports "../ProgLang/Language" begin

axioms (* theorems which are available only with long names,

          which can not yet be handled in isac's scripts *)

  real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)"

 (*Semiring_Normalization.comm_semiring_1_class.normalizing_semiring_rules(19)*)

  real_mult_minus1:       "-1 * z = - (z::real)"

  real_mult_2:            "2 * z = z + (z::real)"

ML {* 

(* TODO rebuild fun calc, fun term_of_float,fun var_op_float, fun float_op_var:

   Float ((a, b), _:int * int, (c, d), _:int * int) has been deleted already *)

(*.used for calculating built in binary operations in Isabelle2002.

   integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)

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*)

    if b < d 

    then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)

    else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)

  | calc "Groups.minus_class.minus" ((a, 0), _) ((c, 0), _) =       (*FIXXXME float + prec.*)

    ((a - c,0),(0,0))

  | calc "op *" ((a, b), _) ((c, d), _) =       (*FIXXXME precision*)

    ((a * c, b + d), (0, 0))

  | calc "Rings.inverse_class.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)

    ((a div c, 0), (0, 0))

  | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)

    ((power a c, 0), (0, 0))

  | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) = 

    error ("calc: not impl. for Float (("^

		 (string_of_int a  )^","^(string_of_int b  )^"), ("^

		 (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^

		 (string_of_int c  )^","^(string_of_int d  )^"), ("^

		 (string_of_int p21)^","^(string_of_int p22)^"))");

(*> calc "Groups.plus_class.plus" ((~1,0),(0,0)) ((2,0),(0,0)); 

val it = ((1,0),(0,0))*)

(*.convert internal floatingpoint prepresentation to int and float.*)

fun term_of_float T ((val1,    0), (         0,          0)) =

    term_of_num T val1

  | term_of_float T ((val1, val2), (precision1, precision2)) =

    let val pT = pairT T T

    in Const ("Float.Float", (pairT pT pT) --> T)

	     $ (pairt (pairt (Free (str_of_int val1, T))

			     (Free (str_of_int val2, T)))

		      (pairt (Free (str_of_int precision1, T))

			     (Free (str_of_int precision2, T))))

    end;

(*> val t = str2term "Float ((1,2),(0,0))";

> val Const ("Float.Float", fT) $ _ = t;

> atomtyp fT;

> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT) 

> 	     (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;

> atomtyp ffT;

> fT = ffT;

val it = true : bool

t = float_term_of_num HOLogic.realT ((1,2),(0,0));

val it = true : bool*)

(*.assoc. convert internal floatingpoint prepresentation to int and float.*)

fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =

    var_op_num v op_ optype ntyp v1

  | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =

    let val pT = pairT T T

    in Const (op_, optype) $ v $ 

	     (Const ("Float.Float", (pairT pT pT) --> T)

		    $ (pairt (pairt (Free (str_of_int v1, T))

				    (Free (str_of_int v2, T)))

			     (pairt (Free (str_of_int p1, T))

				    (Free (str_of_int p2, T)))))

    end;

(*> val t = str2term "a + b";

> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;

> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";

> t = var_op_float v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));

val it = true : bool*)

(*.assoc. convert internal floatingpoint prepresentation to int and float.*)

fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =

    num_op_var v op_ optype ntyp v1

  | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =

    let val pT = pairT T T

    in Const (op_,optype) $ 

	     (Const ("Float.Float", (pairT pT pT) --> T)

		    $ (pairt (pairt (Free (str_of_int v1, T))

				    (Free (str_of_int v2, T)))

			     (pairt (Free (str_of_int p1, T))

				    (Free (str_of_int p2, T))))) $ v

    end;

(*> val t = str2term "a + b";

> val Const ("Groups.plus_class.plus", optype) $ _ $ _ = t;

> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";

> t = float_op_var v "Groups.plus_class.plus" optype HOLogic.realT ((11,~1),(0,0));

val it = true : bool*)

*}

end