# HG changeset patch # User Walther Neuper # Date 1332146883 -3600 # Node ID 04d3f013382726286164443efacd8cd101ad1406 # Parent 4f1cc40522c452e3a0bc020d2786ab1c5a70e160 state of development Isabelle2002 --> 2011 wrt. test/../Knowledge ?!? test --- test thm rootrat_equation_left_1 --- changed behavior. diff -r 4f1cc40522c4 -r 04d3f0133827 src/Tools/isac/Knowledge/Equation.thy --- a/src/Tools/isac/Knowledge/Equation.thy Sat Mar 17 13:43:24 2012 +0100 +++ b/src/Tools/isac/Knowledge/Equation.thy Mon Mar 19 09:48:03 2012 +0100 @@ -5,6 +5,16 @@ theory Equation imports Atools begin +text {* univariate equations over terms : + In 2003 Richard Lang prototyped ISAC's equation solver while also alpha-testing + the Lucas-Interpreter's Subproblem mechanism. + This prototype suffers from the drop-out of Matthias Goldgruber for a year, + who had started to work on simplification in parallel. So this implementation + replaced simplifiers by many specific theorems for specific terms in specific + phases of equation solving; these specific solutions wait for generalisation + in future improvements of ISAC's equation solver. +*} + consts (*descriptions in the related problems TODOshift here from Descriptions.thy*) diff -r 4f1cc40522c4 -r 04d3f0133827 src/Tools/isac/Knowledge/Poly.thy --- a/src/Tools/isac/Knowledge/Poly.thy Sat Mar 17 13:43:24 2012 +0100 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Mar 19 09:48:03 2012 +0100 @@ -1438,7 +1438,17 @@ (*asm_thm = [],*) rules = [Rls_ order_add_ ], scr = EmptyScr}:rls; +*} +text {* rule-set make_polynomial also named norm_Poly: + Rewrite order has not been implemented properly; the order is better in + make_polynomial_in (coded in SML). + Notes on state of development: + \# surprise 2006: test --- norm_Poly NOT COMPLETE --- + \# migration Isabelle2002 --> 2011 weakened the rule set, see test + --- Matthias Goldgruber 2003 rewrite orders ---, error "ord_make_polynomial_in #16b" +*} +ML {* (*. see MG-DA.p.52ff .*) val make_polynomial(*MG.03, overwrites version from above, previously 'make_polynomial_'*) = diff -r 4f1cc40522c4 -r 04d3f0133827 src/Tools/isac/Knowledge/RatEq.thy --- a/src/Tools/isac/Knowledge/RatEq.thy Sat Mar 17 13:43:24 2012 +0100 +++ b/src/Tools/isac/Knowledge/RatEq.thy Mon Mar 19 09:48:03 2012 +0100 @@ -9,6 +9,18 @@ theory RatEq imports Rational begin +text {* univariate equations over multivariate rational terms: + In 2003 this type has been integrated into ISAC's equation solver + by Richard Lang; the root for the solver is Equation.thy. + The migration Isabelle2002 --> 2011 found that application of theorems like + rat_mult_denominator_right: "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)" + in rule-sets does not transfer "d ~= 0" to the assumptions; see + test --- repair NO asms from rls RatEq_eliminate ---. + Thus the migration dropped update of Check_elementwise, which would require + these assumptions; see + test --- pbl: rational, univariate, equation ---, --- x / (x ^ 2 - 6 * x + 9) - 1 /... +*} + consts is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _") diff -r 4f1cc40522c4 -r 04d3f0133827 src/Tools/isac/Knowledge/RootEq.thy --- a/src/Tools/isac/Knowledge/RootEq.thy Sat Mar 17 13:43:24 2012 +0100 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon Mar 19 09:48:03 2012 +0100 @@ -9,6 +9,16 @@ theory RootEq imports Root begin +text {* univariate equations containing real square roots: + This type of equations has been used to bootstrap Lucas-Interpretation. + In 2003 this type has been extended and integrated into ISAC's equation solver + by Richard Lang in 2003. + The assumptions (all containing "<") didn't pass the xml-parsers at the + interface between math-engine and front-end. + The migration Isabelle2002 --> 2011 dropped this type of equation, see + test/../rooteq.sml, rootrateq.sml. +*} + consts is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _") diff -r 4f1cc40522c4 -r 04d3f0133827 src/Tools/isac/Knowledge/RootRatEq.thy --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sat Mar 17 13:43:24 2012 +0100 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Mar 19 09:48:03 2012 +0100 @@ -9,6 +9,12 @@ theory RootRatEq imports LinEq RootEq RatEq RootRat begin +text {* univariate equations over rational terms containing real square roots: + In 2003 this type has been developed as part of ISAC's equation solver + by Richard Lang in 2003. + The migration Isabelle2002 --> 2011 dropped this type of equation, see RootEq.thy. +*} + consts is'_rootRatAddTerm'_in :: "[real, real] => bool" diff -r 4f1cc40522c4 -r 04d3f0133827 src/Tools/isac/TODO.txt --- a/src/Tools/isac/TODO.txt Sat Mar 17 13:43:24 2012 +0100 +++ b/src/Tools/isac/TODO.txt Mon Mar 19 09:48:03 2012 +0100 @@ -160,7 +160,7 @@ investigation Check_elementwise stopped due to too much effort finding out, why Check_elementwise worked in 2002 in spite of the error. -------------------------------------------------------------------------------- -WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeind +WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl -------------------------------------------------------------------------------- WN120317.TODO found by test --- interSteps for Schalk 299a --- that NO test with 'interSteps' is checked properly (with exn on changed behaviour) diff -r 4f1cc40522c4 -r 04d3f0133827 test/Tools/isac/Knowledge/atools.sml --- a/test/Tools/isac/Knowledge/atools.sml Sat Mar 17 13:43:24 2012 +0100 +++ b/test/Tools/isac/Knowledge/atools.sml Mon Mar 19 09:48:03 2012 +0100 @@ -192,12 +192,12 @@ val ttt = (term_of o the o (parse thy)) ttt'; val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt; if term2str uuu = "(5 + 3 * x) / 18" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #16"; +else error "termorder.sml diff.behav ord_make_polynomial_in #16a"; (*============ inhibit exn WN120316 ============================================== -val SOME (uuu,_) =rewrite_set_ thy false make_polynomial ttt; +val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt; if term2str uuu = "(5 + 3 * x) / 18" then () -else error "termorder.sml diff.behav ord_make_polynomial_in #16"; +else error "termorder.sml diff.behav ord_make_polynomial_in #16b"; ============ inhibit exn WN120316 ==============================================*) diff -r 4f1cc40522c4 -r 04d3f0133827 test/Tools/isac/Knowledge/rootrateq.sml --- a/test/Tools/isac/Knowledge/rootrateq.sml Sat Mar 17 13:43:24 2012 +0100 +++ b/test/Tools/isac/Knowledge/rootrateq.sml Mon Mar 19 09:48:03 2012 +0100 @@ -65,7 +65,14 @@ val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt; -val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*============ inhibit exn WN120319 ============================================== +(*From final Test_Isac.thy we suddenly have + + nxt = ("Model_Problem", Model_Problem) + +which we did not investigate further due to the decision to drop the whole type of equation. +*) if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then () else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a"; (*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"])*) @@ -156,6 +163,7 @@ case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => () | _ => error "rootrateq.sml: diff.behav. in -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]"; ============ inhibit exn WN120314 ==============================================*) +============ inhibit exn WN120319 ==============================================*) "------------ test thm rootrat_equation_left_2 -------------------"; "------------ test thm rootrat_equation_left_2 -------------------"; diff -r 4f1cc40522c4 -r 04d3f0133827 test/Tools/isac/Test_Some.thy --- a/test/Tools/isac/Test_Some.thy Sat Mar 17 13:43:24 2012 +0100 +++ b/test/Tools/isac/Test_Some.thy Mon Mar 19 09:48:03 2012 +0100 @@ -1,16 +1,16 @@ theory Test_Some imports Isac begin -use"../../../test/Tools/isac/Knowledge/atools.sml" +use"../../../test/Tools/isac/Knowledge/rootrateq.sml" ML {* -val thy = @{theory "Atools"}; +val thy = @{theory "RootRatEq"}; val ctxt = ProofContext.init_global thy; -print_depth 999; +print_depth 555; *} ML {* - - +*} +ML {* (*==================*) *} ML {* *} @@ -29,6 +29,11 @@ ML {* "~~~~~ fun , args:"; val () = (); "~~~~~ to return val:"; val () = (); + +*} +text {**} +ML {* + *} end @@ -40,3 +45,4 @@ (*=========================^^^ correct until here ^^^===========================*) +