1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Fri Oct 14 11:43:00 2011 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Fri Oct 14 14:33:25 2011 +0200
1.3 @@ -395,15 +395,14 @@
1.4 [];
1.5
1.6 (*.for evaluation of conditions in rewrite rules.*)
1.7 -val Poly_erls =
1.8 - append_rls "Poly_erls" Atools_erls
1.9 - [ Calc ("HOL.eq",eval_equal "#equal_"),
1.10 - Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
1.11 - Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.12 - Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.13 - Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.14 - Calc ("Atools.pow" ,eval_binop "#power_")
1.15 - ];
1.16 +val Poly_erls = append_rls "Poly_erls" Atools_erls
1.17 + [ Calc ("HOL.eq",eval_equal "#equal_"),
1.18 + Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
1.19 + Calc ("Groups.plus_class.plus",eval_binop "#add_"),
1.20 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
1.21 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
1.22 + Calc ("Atools.pow" ,eval_binop "#power_")
1.23 + ];
1.24
1.25 val poly_crls =
1.26 append_rls "poly_crls" Atools_crls
2.1 --- a/src/Tools/isac/Knowledge/RootRat.thy Fri Oct 14 11:43:00 2011 +0200
2.2 +++ b/src/Tools/isac/Knowledge/RootRat.thy Fri Oct 14 14:33:25 2011 +0200
2.3 @@ -26,8 +26,8 @@
2.4 ];
2.5
2.6 ruleset' := overwritelthy thy (!ruleset',
2.7 - [("rootrat_erls", rootrat_erls), (*FIXXXME:del with rls.rls'*)
2.8 - ("calculate_RootRat", calculate_RootRat)
2.9 + [("rootrat_erls", prep_rls rootrat_erls), (*FIXXXME:del with rls.rls'*)
2.10 + ("calculate_RootRat", prep_rls calculate_RootRat)
2.11 ]);
2.12 *}
2.13
3.1 --- a/src/Tools/isac/TODO.txt Fri Oct 14 11:43:00 2011 +0200
3.2 +++ b/src/Tools/isac/TODO.txt Fri Oct 14 14:33:25 2011 +0200
3.3 @@ -17,9 +17,9 @@
3.4 before all tests are RUNNING
3.5
3.6 --------------------------------------------------------------------------------
3.7 -WN111013 TODO: lots of cleanup/removal in test/../Test.thy
3.8 +WN111013.TODO: lots of cleanup/removal in test/../Test.thy
3.9 --------------------------------------------------------------------------------
3.10 -WN111013 TODO: remove concept around "fun init_form", lots of troubles with
3.11 +WN111013.TODO: remove concept around "fun init_form", lots of troubles with
3.12 this special case (see) --- why not nxt = Model_Problem here ? ---
3.13
3.14 the following methods need init_form,
3.15 @@ -87,7 +87,7 @@
3.16 Trig //
3.17 Vect //
3.18 --------------------------------------------------------------------------------
3.19 -WN111013 TODO: these scripts start with Take or Sub_Problem, i.e. NO init_form
3.20 +WN111013.TODO: these scripts start with Take or Sub_Problem, i.e. NO init_form
3.21
3.22 AlgEin
3.23 ["Berechnung","erstNumerisch"]
3.24 @@ -139,3 +139,13 @@
3.25 Test //
3.26 Trig //
3.27 Vect //
3.28 +--------------------------------------------------------------------------------
3.29 +WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat, see test/
3.30 +... FIRST redesign
3.31 +# simplify_* , *_simp_*
3.32 +# norm_*
3.33 +# calc_* , calculate_* ... require iteration over all rls ...
3.34 +... see --- val rls = calculate_RootRat > calculate_Rational --- CONTINUE !
3.35 +--------------------------------------------------------------------------------
3.36 +WN111014.TODO fun prep_rls | !!!use this function in ruleset' := !!!
3.37 +--------------------------------------------------------------------------------
4.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Fri Oct 14 11:43:00 2011 +0200
4.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Fri Oct 14 14:33:25 2011 +0200
4.3 @@ -7,7 +7,8 @@
4.4
4.5 "-----------------------------------------------------------------";
4.6 "table of contents -----------------------------------------------";
4.7 -(*WN060608 some ----- are not in this table*)
4.8 +(*WN060608 some ----- are not in this table.
4.9 + WN111014.TODO missing checks*)
4.10 "-----------------------------------------------------------------";
4.11 "----------- tests on predicates in problems ---------------------";
4.12 "----------- test matching problems --------------------------0---";
4.13 @@ -726,6 +727,11 @@
4.14 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
4.15 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
4.16 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
4.17 +(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
4.18 +see --- val rls = calculate_RootRat > calculate_Rational ---
4.19 +calculate_RootRat was a TODO with 2002, requires re-design.
4.20 +see also --- (-8 - 2*x + x^^^2 = 0), by rewriting --- below
4.21 +*)
4.22 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
4.23 "solveFor x","solutions L"];
4.24 val (dI',pI',mI') =
4.25 @@ -757,7 +763,8 @@
4.26 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
4.27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.28 (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
4.29 - x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
4.30 + x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Rational
4.31 + NOT IMPLEMENTED SINCE 2002 ------------------------------^^^^^^^^^^^^^^^^^^*)
4.32 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.33 (*"x = -2 | x = 4" nxt = Or_to_List*)
4.34 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.35 @@ -773,6 +780,47 @@
4.36 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
4.37 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
4.38 "----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
4.39 +(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
4.40 +see --- val rls = calculate_RootRat > calculate_Rational ---*)
4.41 +val thy = @{theory PolyEq};
4.42 +val ctxt = ProofContext.init_global thy;
4.43 +val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
4.44 +val t = (the o (parseNEW ctxt)) "-8 - 2*x + x^^^2 = (0::real)";
4.45 +
4.46 +val rls = complete_square;
4.47 +val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
4.48 +term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
4.49 +
4.50 +val thm = num_str @{thm square_explicit1};
4.51 +val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
4.52 +term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
4.53 +
4.54 +val thm = num_str @{thm root_plus_minus};
4.55 +val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
4.56 +term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
4.57 + "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
4.58 +
4.59 +(*the thm bdv_explicit2* here required to be constrained to ::real*)
4.60 +val thm = num_str @{thm bdv_explicit2};
4.61 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
4.62 +term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
4.63 + "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
4.64 +
4.65 +val thm = num_str @{thm bdv_explicit3};
4.66 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
4.67 +term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
4.68 + "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
4.69 +
4.70 +val thm = num_str @{thm bdv_explicit2};
4.71 +val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
4.72 +term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
4.73 + "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
4.74 +
4.75 +val rls = calculate_RootRat;
4.76 +val SOME (t,asm) = rewrite_set_ thy true rls t;
4.77 +if term2str t = "-1 * x = -1 + sqrt (1 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))"
4.78 +then () else error "(-8 - 2*x + x^^^2 = 0), by rewriting -- ERROR INDICATES IMPROVEMENT";
4.79 +(*SHOULD BE: term2str = "x = -2 | x = 4;*)
4.80
4.81
4.82
4.83 @@ -781,7 +829,7 @@
4.84 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
4.85 "---- test the erls ----";
4.86 val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
4.87 - val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
4.88 + val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_erls t1;
4.89 val t' = term2str t;
4.90 (*if t'= "HOL.True" then ()
4.91 else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
4.92 @@ -929,15 +977,10 @@
4.93 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
4.94 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
4.95 (*EP-17 Schalk_I_p86_n5*)
4.96 -val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
4.97 +val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
4.98 (* refine fmz ["univariate","equation"];
4.99 *)
4.100 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
4.101 -(*val p = e_pos';
4.102 -val c = [];
4.103 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
4.104 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
4.105 -
4.106 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
4.107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
4.108 (* val nxt =
4.109 @@ -1078,12 +1121,12 @@
4.110 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";
4.111 states:=[];
4.112 CalcTree
4.113 -[(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
4.114 +[(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
4.115 ("PolyEq",["univariate","equation"],["no_met"]))];
4.116 Iterator 1;
4.117 moveActiveRoot 1;
4.118 autoCalculate 1 CompleteCalc;
4.119 val ((pt,p),_) = get_calc 1; show_pt pt;
4.120
4.121 -interSteps 1 ([1],Res) (*no Rewrite_Set...*);
4.122 +interSteps 1 ([1],Res) (*<ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);
4.123
5.1 --- a/test/Tools/isac/Knowledge/rootrat.sml Fri Oct 14 11:43:00 2011 +0200
5.2 +++ b/test/Tools/isac/Knowledge/rootrat.sml Fri Oct 14 14:33:25 2011 +0200
5.3 @@ -5,7 +5,59 @@
5.4 "-----------------------------------------------------------------";
5.5 "table of contents -----------------------------------------------";
5.6 "-----------------------------------------------------------------";
5.7 -"----------- tests on predicates in problems ---------------------";
5.8 +"----------- val rls = calculate_RootRat > calculate_Rational ----";
5.9 "-----------------------------------------------------------------";
5.10 "-----------------------------------------------------------------";
5.11 "-----------------------------------------------------------------";
5.12 +
5.13 +
5.14 +"----------- val rls = calculate_RootRat > calculate_Rational ----";
5.15 +"----------- val rls = calculate_RootRat > calculate_Rational ----";
5.16 +"----------- val rls = calculate_RootRat > calculate_Rational ----";
5.17 +(*stopped du to TODO.txt WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat*)
5.18 +
5.19 +(*val calculate_RootRat =
5.20 + append_rls "calculate_RootRat" calculate_Rational [...]
5.21 + val calculate_Rational = prep_rls (merge_rls "calculate_Rational" [...]
5.22 + calculate_Poly
5.23 + val calculate_Poly =
5.24 + append_rls "calculate_PolyFIXXXME.not.impl." e_rls [];
5.25 + WN111014.TODO calculate_Poly < calculate_Rational < calculate_RootRat
5.26 +*)
5.27 +
5.28 +val thy = @{theory RootRat};
5.29 +val ctxt = ProofContext.init_global thy;
5.30 +val ttt = (the o (parseNEW ctxt)) ("-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
5.31 + "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))");
5.32 +atomty t; (*!real ?by sqrt and ^^^?*)
5.33 +
5.34 +"--- val rls = calculate_Poly ---";
5.35 +(*val rls = assoc_rls "calculate_Poly"; WAS ME_Isa: 'calculate_Poly' not in system
5.36 +GOON with what just started ...*)
5.37 +val calculate_Poly = append_rls "calculate_Poly" e_rls
5.38 + [ Calc ("Groups.plus_class.plus",eval_binop "#add_"),
5.39 + Calc ("Groups.minus_class.minus",eval_binop "#sub_"),
5.40 + Calc ("Groups.times_class.times",eval_binop "#mult_"),
5.41 + Calc ("Atools.pow" ,eval_binop "#power_")
5.42 + ];
5.43 +val rls = calculate_Poly;
5.44 +
5.45 +(*val SOME (t,asm) = rewrite_set_ thy true rls ttt; WAS: NONE .. ok*)
5.46 +
5.47 +"--- val rls = calculate_Rational ---";
5.48 +val rls = assoc_rls "calculate_Rational";
5.49 +val rls = calculate_Rational;
5.50 +
5.51 +val SOME (t,asm) = rewrite_set_ thy true rls ttt;
5.52 +if term2str t = "-1 * x = -1 + sqrt (1 ^^^ 2 - -8) | x = -1 * (-1 + -1 * sqrt (1 ^^^ 2 - -8))"
5.53 +then () else error "val rls = calculate_Rational GOON";
5.54 +
5.55 +"--- val rls = calculate_RootRat ---";
5.56 +val rls = assoc_rls "calculate_RootRat";
5.57 +val rls = calculate_RootRat;
5.58 +
5.59 +val SOME (t,asm) = rewrite_set_ thy true rls ttt;
5.60 +
5.61 +(*~~~~~ val rls = calculate_RootRat: rewrite stepwise*)
5.62 +val thm = num_str @{thm complete_square2};
5.63 +
6.1 --- a/test/Tools/isac/Test_Isac.thy Fri Oct 14 11:43:00 2011 +0200
6.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Oct 14 14:33:25 2011 +0200
6.3 @@ -158,10 +158,10 @@
6.4 use "Knowledge/lineq.sml" (*new 2011*)
6.5 (*use "Knowledge/rooteq.sml" 2002*)
6.6 (*use "Knowledge/rateq.sml" 2002*)
6.7 -(*use "Knowledge/rootrat.sml" 2002*)
6.8 + use "Knowledge/rootrat.sml"
6.9 (*use "Knowledge/rootrateq.sml" 2002*)
6.10 use "Knowledge/partial_fractions.sml"
6.11 -(*use "Knowledge/polyeq.sml" part. WN110906: problems with comments*)
6.12 + use "Knowledge/polyeq.sml"
6.13 (*use "Knowledge/rlang.sml" 2002???*)
6.14 use "Knowledge/calculus.sml" (*new 2011*)
6.15 use "Knowledge/trig.sml"
7.1 --- a/test/Tools/isac/Test_Some.thy Fri Oct 14 11:43:00 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Fri Oct 14 14:33:25 2011 +0200
7.3 @@ -4,197 +4,10 @@
7.4 use"../../../test/Tools/isac/Knowledge/polyeq.sml"
7.5
7.6 ML {* (*=================*)
7.7 -print_depth 999;
7.8 -"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.9 -"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.10 -"----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
7.11 - val fmz = ["equality (-8 - 2*x + x^^^2 = (0::real))", (*Schalk 2, S.67 Nr.31.b*)
7.12 - "solveFor x","solutions L"];
7.13 - val (dI',pI',mI') =
7.14 - ("PolyEq",["degree_2","expanded","univariate","equation"],
7.15 - ["PolyEq","complete_square"]);
7.16 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
7.17 -val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.18 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.19 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.20 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
7.21 - (*Apply_Method ("PolyEq","complete_square")*)
7.22 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set_Inst (["(bdv, x)"], "complete_square"*)
7.23 -f2str f; "-8 - 2 * x + x ^^^ 2 = 0";
7.24 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("square_explicit1"*)
7.25 -f2str f; "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
7.26 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Rewrite ("root_plus_minus"*)
7.27 -f2str f; "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
7.28 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Rewrite_Set "calculate_RootRat"*)
7.29 -f2str f; "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
7.30 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Or_to_List*)
7.31 -f2str f; "1 - x = sqrt (1 ^^^ 2 - -8) | 1 - x = -1 * sqrt (1 ^^^ 2 - -8)";
7.32 -*}
7.33 -ML{*
7.34 -@{thm "bdv_explicit2"};
7.35 -@{thm "bdv_explicit3"};
7.36 *}
7.37 ML{*
7.38 *}
7.39 -ML{*
7.40 -*}
7.41 -ML{*
7.42 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
7.43 -*}
7.44 -ML{*
7.45 -f2str f;
7.46 - (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
7.47 - -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
7.48 -*}
7.49 -ML{*
7.50 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
7.51 -*}
7.52 -ML{*
7.53 -f2str f;
7.54 - (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
7.55 - x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
7.56 -*}
7.57 -ML{*
7.58 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
7.59 -*}
7.60 -ML{*
7.61 -f2str f;
7.62 - (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
7.63 - x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
7.64 -*}
7.65 -ML{*
7.66 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
7.67 -*}
7.68 -ML{*
7.69 -f2str f;
7.70 - (*"x = -2 | x = 4" nxt = Or_to_List*)
7.71 -*}
7.72 -ML{*
7.73 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
7.74 -*}
7.75 -ML{*
7.76 -f2str f;
7.77 - (*"[x = -2, x = 4]" nxt = Check_Postcond*)
7.78 -*}
7.79 -ML{*
7.80 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
7.81 -*}
7.82 -ML{*
7.83 -f2str f;
7.84 -(* FIXXXME
7.85 - case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
7.86 - | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
7.87 -*)
7.88 -*}
7.89 -ML{*
7.90 -f2str f
7.91 -*}
7.92 -ML{*
7.93 -if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
7.94 -else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
7.95 -*}
7.96 -ML{*
7.97 -"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
7.98 -"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
7.99 -"----------- (-8 - 2*x + x^^^2 = 0), by rewriting ---------------";
7.100 -print_depth 9;
7.101 -val thy = @{theory PolyEq};
7.102 -val ctxt = ProofContext.init_global thy;
7.103 -val inst = [((the o (parseNEW ctxt)) "bdv::real", (the o (parseNEW ctxt)) "x::real")];
7.104 -val t = (the o (parseNEW ctxt)) "-8 - 2*x + x^^^2 = (0::real)";
7.105 -
7.106 -val rls = complete_square;
7.107 -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
7.108 -term2str t = "-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2";
7.109 -
7.110 -val thm = num_str @{thm square_explicit1};
7.111 -val SOME (t,asm) = rewrite_ thy dummy_ord Erls true thm t;
7.112 -term2str t = "(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8";
7.113 -
7.114 -val thm = num_str @{thm root_plus_minus};
7.115 -val SOME (t,asm) = rewrite_ thy dummy_ord PolyEq_erls true thm t;
7.116 -term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
7.117 - "\n2 / 2 - x = -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
7.118 -
7.119 -(*the thm bdv_explicit2* here required to be constrained to ::real*)
7.120 -val thm = num_str @{thm bdv_explicit2};
7.121 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
7.122 -term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
7.123 - "\n-1 * x = - (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8)";
7.124 -
7.125 -val thm = num_str @{thm bdv_explicit3};
7.126 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
7.127 -term2str t = "2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |"^
7.128 - "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))";
7.129 -
7.130 -val thm = num_str @{thm bdv_explicit2};
7.131 -val SOME (t,asm) = rewrite_inst_ thy dummy_ord Erls true inst thm t;
7.132 -*}
7.133 -ML{*
7.134 -term2str t = "-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
7.135 - "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))"
7.136 -*}
7.137 -ML{*
7.138 -val rls = calculate_Rational;
7.139 -val rls = calculate_RootRat;
7.140 -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls t;
7.141 -
7.142 -*}
7.143 -ML{*
7.144 -term2str t;
7.145 -*}
7.146 -ML{*
7.147 -(* "-1 * x = -1 + sqrt (1 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))"*)
7.148 -*}
7.149 ML{* (*==================*)
7.150 -"----------- val rls = calculate_RootRat > calculate_Rational ----";
7.151 -"----------- val rls = calculate_RootRat > calculate_Rational ----";
7.152 -"----------- val rls = calculate_RootRat > calculate_Rational ----";
7.153 -(*val calculate_RootRat =
7.154 - append_rls "calculate_RootRat" calculate_Rational [...]*)
7.155 -val thy = @{theory RootRat};
7.156 -val ctxt = ProofContext.init_global thy;
7.157 -val ttt = (the o (parseNEW ctxt)) ("-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |"^
7.158 - "\nx = -1 * (- (2 / 2) + -1 * sqrt ((2 / 2) ^^^ 2 - -8))");
7.159 -atomty t; (*!real ?by sqrt and ^^^?*)
7.160 -
7.161 -"--- val rls = calculate_Rational ---";
7.162 -val rls = assoc_rls "calculate_Rational";
7.163 -val rls = calculate_Rational;
7.164 -*}
7.165 -ML{*
7.166 -*}
7.167 -ML{*
7.168 -*}
7.169 -ML{*
7.170 -*}
7.171 -ML{*
7.172 -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls ttt;
7.173 -if term2str t = "-1 * x = -1 + sqrt (1 ^^^ 2 - -8) | x = -1 * (-1 + -1 * sqrt (1 ^^^ 2 - -8))"
7.174 -then () else error "val rls = calculate_Rational";
7.175 -*}
7.176 -ML{*
7.177 -"--- val rls = calculate_RootRat ---";
7.178 -val rls = assoc_rls "calculate_RootRat";
7.179 -val rls = calculate_RootRat;
7.180 -
7.181 -trace_rewrite := false;
7.182 -*}
7.183 -ML{*
7.184 -val SOME (t,asm) = rewrite_set_inst_ thy true inst rls ttt;
7.185 -*}
7.186 -ML{*
7.187 -term2str t
7.188 -*}
7.189 -ML{*
7.190 -
7.191 -*}
7.192 -ML{*
7.193 -(*~~~~~ val rls = calculate_RootRat: rewrite stepwise*)
7.194 -val thm = num_str @{thm complete_square2};
7.195 -
7.196 -*}
7.197 -ML{*
7.198 *}
7.199 ML{*
7.200 *}