1.1 --- a/src/Tools/isac/IsacKnowledge/Atools.thy Mon Aug 23 11:22:25 2010 +0200
1.2 +++ b/src/Tools/isac/IsacKnowledge/Atools.thy Mon Aug 23 17:10:57 2010 +0200
1.3 @@ -10,7 +10,7 @@
1.4 *)
1.5
1.6
1.7 -Atools = ComplexI + Descript +
1.8 +Atools = Descript + Typefix +
1.9
1.10 (*-------------------- consts------------------------------------------------*)
1.11 consts
2.1 --- a/src/Tools/isac/IsacKnowledge/Complex.ML Mon Aug 23 11:22:25 2010 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,22 +0,0 @@
2.4 -(*Komplexe Zahlen, anders als von Isabelle vorgeschlagen,
2.5 - und naeher an der traditionellen Schreibweise (sh.auch Mathematica)*)
2.6 -
2.7 -
2.8 -(*---- solche Tests gehoeren nach kbtest/complex.sml ---
2.9 - val t = (term_of o the o (parse thy)) "I__";
2.10 - atomt t;
2.11 - val t = (term_of o the o (parse thy)) "1 + 2 * I__";
2.12 - atomt t;
2.13 - val t = (term_of o the o (parse thy))
2.14 - "1 + 2 * I__ + 3 + 4 * I__ * (5 + 6 * I__) / (7 + 8 * I__)";
2.15 - atomt t;
2.16 -(*andere konkrete Syntax ???*)
2.17 -
2.18 - val t = (term_of o the o (parse thy)) "Float ((1,2),(0,0)) * I__";
2.19 - atomt t;
2.20 - (*term2str t;*)
2.21 - val t = (term_of o the o (parse thy))
2.22 - "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
2.23 - atomt t;
2.24 - (*term2str t;*)
2.25 ----------------------------------------------------------*)
2.26 \ No newline at end of file
3.1 --- a/src/Tools/isac/IsacKnowledge/Complex.thy Mon Aug 23 11:22:25 2010 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,27 +0,0 @@
3.4 -(* imaginary unit, close to traditional notation in algebra systems;
3.5 - types questionable, see Isabelle/HOL/Real/Complex_Numbers.thy
3.6 -
3.7 - use_thy_only"IsacKnowledge/Complex";
3.8 - use_thy_only"Complex";
3.9 -
3.10 - use_thy"knowledge/Complex";
3.11 - use_thy"Complex";
3.12 - *)
3.13 -
3.14 -
3.15 -Complex = Float +
3.16 -
3.17 -consts
3.18 -(* waere auch eine Moeglichkeit
3.19 - "I'_'_" :: "real => real" ("_ I'_'_" [999] 998)
3.20 -*)
3.21 - "I'_'_" :: "real" ("I'_'_")
3.22 -
3.23 -rules
3.24 -(* waere auch eine Moeglichkeit
3.25 - add_I "a I__ + b I__ = (a + b) I__"
3.26 - mult_I "a I__ * b I__ = -1 * a * b"
3.27 -*)
3.28 - square_I "I__ * I__ = -1"
3.29 -
3.30 -end
3.31 \ No newline at end of file
4.1 --- a/src/Tools/isac/IsacKnowledge/ComplexI.ML Mon Aug 23 11:22:25 2010 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,22 +0,0 @@
4.4 -(*Komplexe Zahlen, anders als von Isabelle vorgeschlagen,
4.5 - und naeher an der traditionellen Schreibweise (sh.auch Mathematica)*)
4.6 -
4.7 -
4.8 -(*---- solche Tests gehoeren nach kbtest/complex.sml ---
4.9 - val t = (term_of o the o (parse thy)) "I__";
4.10 - atomt t;
4.11 - val t = (term_of o the o (parse thy)) "1 + 2 * I__";
4.12 - atomt t;
4.13 - val t = (term_of o the o (parse thy))
4.14 - "1 + 2 * I__ + 3 + 4 * I__ * (5 + 6 * I__) / (7 + 8 * I__)";
4.15 - atomt t;
4.16 -(*andere konkrete Syntax ???*)
4.17 -
4.18 - val t = (term_of o the o (parse thy)) "Float ((1,2),(0,0)) * I__";
4.19 - atomt t;
4.20 - (*term2str t;*)
4.21 - val t = (term_of o the o (parse thy))
4.22 - "Float ((1,2),(0,0)) + Float ((3,4),(0,0)) * I__";
4.23 - atomt t;
4.24 - (*term2str t;*)
4.25 ----------------------------------------------------------*)
4.26 \ No newline at end of file
5.1 --- a/src/Tools/isac/IsacKnowledge/ComplexI.thy Mon Aug 23 11:22:25 2010 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,27 +0,0 @@
5.4 -(* imaginary unit, close to traditional notation in algebra systems;
5.5 - types questionable, see Isabelle/HOL/Real/Complex_Numbers.thy
5.6 -
5.7 - use_thy_only"IsacKnowledge/ComplexI";
5.8 - use_thy_only"ComplexI";
5.9 -
5.10 - use_thy"knowledge/ComplexI";
5.11 - use_thy"ComplexI";
5.12 - *)
5.13 -
5.14 -
5.15 -ComplexI = Float +
5.16 -
5.17 -consts
5.18 -(* waere auch eine Moeglichkeit
5.19 - "I'_'_" :: "real => real" ("_ I'_'_" [999] 998)
5.20 -*)
5.21 - "I'_'_" :: "real" ("I'_'_")
5.22 -
5.23 -rules
5.24 -(* waere auch eine Moeglichkeit
5.25 - add_I "a I__ + b I__ = (a + b) I__"
5.26 - mult_I "a I__ * b I__ = -1 * a * b"
5.27 -*)
5.28 - square_I "I__ * I__ = -1"
5.29 -
5.30 -end
5.31 \ No newline at end of file
6.1 --- a/src/Tools/isac/IsacKnowledge/Float.ML Mon Aug 23 11:22:25 2010 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,95 +0,0 @@
6.4 -(* use"Float.ML";
6.5 - *)
6.6 -
6.7 -theory' := overwritel (!theory', [("Float.thy",Float.thy)]);
6.8 -
6.9 -(*.used for calculating built in binary operations in Isabelle2002.
6.10 - integer numerals n are ((n,0),(0,0)) i.e. precision is (0,0)*)
6.11 -fun calc "op +" ((a, b), _:int * int) ((c, d), _:int * int) =
6.12 - if b < d
6.13 - then ((a + c * power 10 (d - b), b), (0, 0))(*FIXXXME precision*)
6.14 - else ((a * power 10 (b - d) + c, d), (0, 0))(*FIXXXME precision*)
6.15 - | calc "op -" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
6.16 - ((a - c,0),(0,0))
6.17 - | calc "op *" ((a, b), _) ((c, d), _) = (*FIXXXME precision*)
6.18 - ((a * c, b + d), (0, 0))
6.19 - | calc "HOL.divide" ((a, 0), _) ((c, 0), _) = (*FIXXXME float + prec.*)
6.20 - ((a div c, 0), (0, 0))
6.21 - | calc "Atools.pow" ((a, b), _) ((c, d), _) = (*FIXXXME float + prec.*)
6.22 - ((power a c, 0), (0, 0))
6.23 - | calc op_ ((a, b), (p11, p12)) ((c, d), (p21, p22)) =
6.24 - raise error ("calc: not impl. for Float (("^
6.25 - (string_of_int a )^","^(string_of_int b )^"), ("^
6.26 - (string_of_int p11)^","^(string_of_int p12)^")) "^op_^" (("^
6.27 - (string_of_int c )^","^(string_of_int d )^"), ("^
6.28 - (string_of_int p21)^","^(string_of_int p22)^"))");
6.29 -(*> calc "op +" ((~1,0),(0,0)) ((2,0),(0,0));
6.30 -val it = ((1,0),(0,0))*)
6.31 -
6.32 -(*.toggle the sign of an integer numeral.*)
6.33 -fun minus ((a, b:int), _:int * int) = ((~1 * a, b), (0, 0));
6.34 -
6.35 -(*.convert internal floatingpoint prepresentation to int and float.*)
6.36 -fun term_of_float T ((val1, 0), ( 0, 0)) =
6.37 - term_of_num T val1
6.38 - | term_of_float T ((val1, val2), (precision1, precision2)) =
6.39 - let val pT = pairT T T
6.40 - in Const ("Float.Float", (pairT pT pT) --> T)
6.41 - $ (pairt (pairt (Free (str_of_int val1, T))
6.42 - (Free (str_of_int val2, T)))
6.43 - (pairt (Free (str_of_int precision1, T))
6.44 - (Free (str_of_int precision2, T))))
6.45 - end;
6.46 -(*> val t = str2term "Float ((1,2),(0,0))";
6.47 -> val Const ("Float.Float", fT) $ _ = t;
6.48 -> atomtyp fT;
6.49 -> val ffT = (pairT (pairT HOLogic.realT HOLogic.realT)
6.50 -> (pairT HOLogic.realT HOLogic.realT)) --> HOLogic.realT;
6.51 -> atomtyp ffT;
6.52 -> fT = ffT;
6.53 -val it = true : bool
6.54 -
6.55 -t = float_term_of_num HOLogic.realT ((1,2),(0,0));
6.56 -val it = true : bool*)
6.57 -
6.58 -(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
6.59 -fun var_op_float v op_ optype ntyp ((v1, 0), (0, 0)) =
6.60 - var_op_num v op_ optype ntyp v1
6.61 - | var_op_float v op_ optype T ((v1, v2), (p1, p2)) =
6.62 - let val pT = pairT T T
6.63 - in Const (op_, optype) $ v $
6.64 - (Const ("Float.Float", (pairT pT pT) --> T)
6.65 - $ (pairt (pairt (Free (str_of_int v1, T))
6.66 - (Free (str_of_int v2, T)))
6.67 - (pairt (Free (str_of_int p1, T))
6.68 - (Free (str_of_int p2, T)))))
6.69 - end;
6.70 -(*> val t = str2term "a + b";
6.71 -> val Const ("op +", optype) $ _ $ _ = t;
6.72 -> val t = str2term "v + Float ((11,-1),(0,0))";val v = str2term "v";
6.73 -> t = var_op_float v "op +" optype HOLogic.realT ((11,~1),(0,0));
6.74 -val it = true : bool*)
6.75 -
6.76 -(*.assoc. convert internal floatingpoint prepresentation to int and float.*)
6.77 -fun float_op_var v op_ optype ntyp ((v1, 0), (0, 0)) =
6.78 - num_op_var v op_ optype ntyp v1
6.79 - | float_op_var v op_ optype T ((v1, v2), (p1, p2)) =
6.80 - let val pT = pairT T T
6.81 - in Const (op_,optype) $
6.82 - (Const ("Float.Float", (pairT pT pT) --> T)
6.83 - $ (pairt (pairt (Free (str_of_int v1, T))
6.84 - (Free (str_of_int v2, T)))
6.85 - (pairt (Free (str_of_int p1, T))
6.86 - (Free (str_of_int p2, T))))) $ v
6.87 - end;
6.88 -(*> val t = str2term "a + b";
6.89 -> val Const ("op +", optype) $ _ $ _ = t;
6.90 -> val t = str2term "Float ((11,-1),(0,0)) + v";val v = str2term "v";
6.91 -> t = float_op_var v "op +" optype HOLogic.realT ((11,~1),(0,0));
6.92 -val it = true : bool*)
6.93 -
6.94 -
6.95 -
6.96 -
6.97 -
6.98 -
7.1 --- a/src/Tools/isac/IsacKnowledge/Float.thy Mon Aug 23 11:22:25 2010 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,12 +0,0 @@
7.4 -(* use_thy_only"IsacKonwledge/Float";
7.5 - use_thy_only"Float";
7.6 - use_thy"Float";
7.7 - *)
7.8 -
7.9 -Float = Typefix +
7.10 -
7.11 -consts
7.12 -
7.13 - Float :: "((real * real) * (real * real)) => real"
7.14 -
7.15 -end
7.16 \ No newline at end of file
8.1 --- a/src/Tools/isac/IsacKnowledge/Typefix.thy Mon Aug 23 11:22:25 2010 +0200
8.2 +++ b/src/Tools/isac/IsacKnowledge/Typefix.thy Mon Aug 23 17:10:57 2010 +0200
8.3 @@ -2,7 +2,9 @@
8.4 WN.11.99, from Markus Wenzel
8.5 *)
8.6
8.7 -Typefix = Script +
8.8 +theory Typefix
8.9 +imports "../Scripts/Script"
8.10 +begin
8.11
8.12 syntax
8.13
8.14 @@ -18,13 +20,12 @@
8.15 "uminus"=> "_umin :: [real] => real" (*"- _" [80] 80*)
8.16 "op *" => "_times :: [real, real] => real" (*infixl 70 *)
8.17
8.18 -end
8.19 -
8.20 -
8.21 -ML
8.22 -
8.23 +ML {*
8.24 val parse_translation =
8.25 [("_plus", curry Term.list_comb (Syntax.const "op +")),
8.26 ("_minus", curry Term.list_comb (Syntax.const "op -")),
8.27 ("_umin", curry Term.list_comb (Syntax.const "uminus")),
8.28 ("_times", curry Term.list_comb (Syntax.const "op *"))];
8.29 +*}
8.30 +
8.31 +end
8.32 \ No newline at end of file
9.1 --- a/src/Tools/isac/Isac_Mathengine.thy Mon Aug 23 11:22:25 2010 +0200
9.2 +++ b/src/Tools/isac/Isac_Mathengine.thy Mon Aug 23 17:10:57 2010 +0200
9.3 @@ -21,6 +21,10 @@
9.4 imports Complex_Main "Scripts/Script" (*ListG, Tools, Script*)
9.5 begin
9.6
9.7 +ML {*
9.8 +writeln "**** build the isac kernel = math-engine + IsacKnowledge ";
9.9 +writeln "**** build the math-engine ******************************" *}
9.10 +
9.11 ML {* Toplevel.debug := true; *}
9.12 use "library.sml"
9.13 use "calcelems.sml"
9.14 @@ -57,7 +61,47 @@
9.15 use "print_exn_G.sml"
9.16 text "**** build math-engine complete *************************"
9.17
9.18 +ML {* writeln "**** build the IsacKnowledge ****************************" *}
9.19 +use_thy"IsacKnowledge/Typefix"
9.20
9.21 +ML {*
9.22
9.23 +111;
9.24 +*}
9.25 +
9.26 +use_thy"IsacKnowledge/Descript"
9.27 +
9.28 +
9.29 +ML {*
9.30 +val str = "1234567890";
9.31 +*}
9.32 +
9.33 +(*
9.34 +use_thy"IsacKnowledge/Atools"
9.35 +use_thy"IsacKnowledge/Simplify"
9.36 +use_thy"IsacKnowledge/Poly"
9.37 +use_thy"IsacKnowledge/Rational"
9.38 +use_thy"IsacKnowledge/PolyMinus"
9.39 +use_thy"IsacKnowledge/Equation"
9.40 +use_thy"IsacKnowledge/LinEq"
9.41 +use_thy"IsacKnowledge/Root"
9.42 +use_thy"IsacKnowledge/RootEq"
9.43 +use_thy"IsacKnowledge/RatEq"
9.44 +use_thy"IsacKnowledge/RootRat"
9.45 +use_thy"IsacKnowledge/RootRatEq"
9.46 +use_thy"IsacKnowledge/PolyEq"
9.47 +use_thy"IsacKnowledge/Vect"
9.48 +use_thy"IsacKnowledge/Calculus"
9.49 +use_thy"IsacKnowledge/Trig"
9.50 +use_thy"IsacKnowledge/LogExp"
9.51 +use_thy"IsacKnowledge/Diff"
9.52 +use_thy"IsacKnowledge/DiffApp"
9.53 +use_thy"IsacKnowledge/Integrate"
9.54 +use_thy"IsacKnowledge/EqSystem"
9.55 +use_thy"IsacKnowledge/Biegelinie"
9.56 +use_thy"IsacKnowledge/AlgEin"
9.57 +use_thy"IsacKnowledge/Test"
9.58 +use_thy"IsacKnowledge/Isac"
9.59 +*)
9.60 end
9.61