1.1 --- a/src/Tools/isac/Knowledge/Equation.thy	Sat Mar 17 13:43:24 2012 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Equation.thy	Mon Mar 19 09:48:03 2012 +0100
     1.3 @@ -5,6 +5,16 @@
     1.4  
     1.5  theory Equation imports Atools begin
     1.6  
     1.7 +text {* univariate equations over terms :
     1.8 +  In 2003 Richard Lang prototyped ISAC's equation solver while also alpha-testing
     1.9 +  the Lucas-Interpreter's Subproblem mechanism.
    1.10 +  This prototype suffers from the drop-out of Matthias Goldgruber for a year,
    1.11 +  who had started to work on simplification in parallel. So this implementation
    1.12 +  replaced simplifiers by many specific theorems for specific terms in specific
    1.13 +  phases of equation solving; these specific solutions wait for generalisation
    1.14 +  in future improvements of ISAC's equation solver.
    1.15 +*}
    1.16 +
    1.17  consts
    1.18  
    1.19    (*descriptions in the related problems TODOshift here from Descriptions.thy*)

     2.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Sat Mar 17 13:43:24 2012 +0100
     2.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Mon Mar 19 09:48:03 2012 +0100
     2.3 @@ -1438,7 +1438,17 @@
     2.4        (*asm_thm = [],*)
     2.5        rules = [Rls_ order_add_
     2.6  	       ], scr = EmptyScr}:rls;
     2.7 +*}
     2.8  
     2.9 +text {* rule-set make_polynomial also named norm_Poly:
    2.10 +  Rewrite order has not been implemented properly; the order is better in 
    2.11 +  make_polynomial_in (coded in SML).
    2.12 +  Notes on state of development:
    2.13 +  \# surprise 2006: test --- norm_Poly NOT COMPLETE ---
    2.14 +  \# migration Isabelle2002 --> 2011 weakened the rule set, see test
    2.15 +  --- Matthias Goldgruber 2003 rewrite orders ---, error "ord_make_polynomial_in #16b"
    2.16 +*}
    2.17 +ML {*
    2.18  (*. see MG-DA.p.52ff .*)
    2.19  val make_polynomial(*MG.03, overwrites version from above, 
    2.20      previously 'make_polynomial_'*) =

     3.1 --- a/src/Tools/isac/Knowledge/RatEq.thy	Sat Mar 17 13:43:24 2012 +0100
     3.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy	Mon Mar 19 09:48:03 2012 +0100
     3.3 @@ -9,6 +9,18 @@
     3.4  
     3.5  theory RatEq imports Rational begin
     3.6  
     3.7 +text {* univariate equations over multivariate rational terms:
     3.8 +  In 2003 this type has been integrated into ISAC's equation solver
     3.9 +  by Richard Lang; the root for the solver is Equation.thy.
    3.10 +  The migration Isabelle2002 --> 2011 found that application of theorems like 
    3.11 +  rat_mult_denominator_right: "[|Not(d=0)|] ==> ((a::real) = c / d) = (a*d = c)"
    3.12 +  in rule-sets does not transfer "d ~= 0" to the assumptions; see
    3.13 +  test --- repair NO asms from rls RatEq_eliminate ---.
    3.14 +  Thus the migration dropped update of Check_elementwise, which would require
    3.15 +  these assumptions; see 
    3.16 +  test --- pbl: rational, univariate, equation ---, --- x / (x ^ 2 - 6 * x + 9) - 1 /...
    3.17 +*}
    3.18 +
    3.19  consts
    3.20  
    3.21    is'_ratequation'_in :: "[bool, real] => bool" ("_ is'_ratequation'_in _")

     4.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Sat Mar 17 13:43:24 2012 +0100
     4.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Mon Mar 19 09:48:03 2012 +0100
     4.3 @@ -9,6 +9,16 @@
     4.4  
     4.5  theory RootEq imports Root begin
     4.6  
     4.7 +text {* univariate equations containing real square roots:
     4.8 +  This type of equations has been used to bootstrap Lucas-Interpretation.
     4.9 +  In 2003 this type has been extended and integrated into ISAC's equation solver
    4.10 +  by Richard Lang in 2003.
    4.11 +  The assumptions (all containing "<") didn't pass the xml-parsers at the 
    4.12 +  interface between math-engine and front-end.
    4.13 +  The migration Isabelle2002 --> 2011 dropped this type of equation, see
    4.14 +  test/../rooteq.sml, rootrateq.sml.
    4.15 +*}
    4.16 +
    4.17  consts
    4.18  
    4.19    is'_rootTerm'_in     :: "[real, real] => bool" ("_ is'_rootTerm'_in _")

     5.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Sat Mar 17 13:43:24 2012 +0100
     5.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Mon Mar 19 09:48:03 2012 +0100
     5.3 @@ -9,6 +9,12 @@
     5.4  
     5.5  theory RootRatEq imports LinEq RootEq RatEq RootRat begin 
     5.6  
     5.7 +text {* univariate equations over rational terms containing real square roots:
     5.8 +  In 2003 this type has been developed as part of ISAC's equation solver
     5.9 +  by Richard Lang in 2003.
    5.10 +  The migration Isabelle2002 --> 2011 dropped this type of equation, see RootEq.thy.
    5.11 +*}
    5.12 +
    5.13  consts
    5.14  
    5.15    is'_rootRatAddTerm'_in :: "[real, real] => bool" 

     6.1 --- a/src/Tools/isac/TODO.txt	Sat Mar 17 13:43:24 2012 +0100
     6.2 +++ b/src/Tools/isac/TODO.txt	Mon Mar 19 09:48:03 2012 +0100
     6.3 @@ -160,7 +160,7 @@
     6.4    investigation Check_elementwise stopped due to too much effort finding out,
     6.5    why Check_elementwise worked in 2002 in spite of the error.
     6.6  --------------------------------------------------------------------------------
     6.7 -WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeind 
     6.8 +WN120317.TODO postponed test/../ratinal,ratinal2.sml to joint work with dmeindl 
     6.9  --------------------------------------------------------------------------------
    6.10  WN120317.TODO found by test --- interSteps for Schalk 299a --- that 
    6.11    NO test with 'interSteps' is checked properly (with exn on changed behaviour)

     7.1 --- a/test/Tools/isac/Knowledge/atools.sml	Sat Mar 17 13:43:24 2012 +0100
     7.2 +++ b/test/Tools/isac/Knowledge/atools.sml	Mon Mar 19 09:48:03 2012 +0100
     7.3 @@ -192,12 +192,12 @@
     7.4    val ttt = (term_of o the o (parse thy)) ttt';
     7.5  val SOME (uuu,_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
     7.6  if term2str uuu = "(5 + 3 * x) / 18" then ()
     7.7 -else error "termorder.sml diff.behav ord_make_polynomial_in #16";
     7.8 +else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
     7.9  
    7.10  (*============ inhibit exn WN120316 ==============================================
    7.11 -val SOME (uuu,_) =rewrite_set_ thy false make_polynomial ttt;
    7.12 +val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
    7.13  if term2str uuu = "(5 + 3 * x) / 18" then ()
    7.14 -else error "termorder.sml diff.behav ord_make_polynomial_in #16";
    7.15 +else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
    7.16  ============ inhibit exn WN120316 ==============================================*)
    7.17  
    7.18  

     8.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml	Sat Mar 17 13:43:24 2012 +0100
     8.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml	Mon Mar 19 09:48:03 2012 +0100
     8.3 @@ -65,7 +65,14 @@
     8.4  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
     8.5  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
     8.6  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
     8.7 -val (p,_,f,nxt,_,pt) = me nxt p c pt; 
     8.8 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
     8.9 +(*============ inhibit exn WN120319 ==============================================
    8.10 +(*From final Test_Isac.thy we suddenly have
    8.11 +
    8.12 +          nxt = ("Model_Problem", Model_Problem)
    8.13 +
    8.14 +which we did not investigate further due to the decision to drop the whole type of equation.
    8.15 +*)
    8.16  if f2str f = "1 = (0 - -2) * (1 + -1 * sqrt x)" then ()
    8.17  else error "rootrateq.sml: diff.behav. in rootrat_equation_left_1 a";
    8.18  (*-> Subproblem ("RootRatEq", ["sq", "root'", "univariate", "equation"])*)
    8.19 @@ -156,6 +163,7 @@
    8.20  case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 4]")) => ()
    8.21  	 | _ => error "rootrateq.sml: diff.behav. in  -2 + 1/(1 - sqrt(x))= 0 -> [x = 1/4]";
    8.22  ============ inhibit exn WN120314 ==============================================*)
    8.23 +============ inhibit exn WN120319 ==============================================*)
    8.24  
    8.25  "------------ test thm rootrat_equation_left_2 -------------------";
    8.26  "------------ test thm rootrat_equation_left_2 -------------------";

     9.1 --- a/test/Tools/isac/Test_Some.thy	Sat Mar 17 13:43:24 2012 +0100
     9.2 +++ b/test/Tools/isac/Test_Some.thy	Mon Mar 19 09:48:03 2012 +0100
     9.3 @@ -1,16 +1,16 @@
     9.4   
     9.5  theory Test_Some imports Isac begin
     9.6  
     9.7 -use"../../../test/Tools/isac/Knowledge/atools.sml"
     9.8 +use"../../../test/Tools/isac/Knowledge/rootrateq.sml"
     9.9  
    9.10  ML {*
    9.11 -val thy = @{theory "Atools"};
    9.12 +val thy = @{theory "RootRatEq"};
    9.13  val ctxt = ProofContext.init_global thy;
    9.14 -print_depth 999;
    9.15 +print_depth 555;
    9.16  *}
    9.17  ML {*
    9.18 -
    9.19 -
    9.20 +*}
    9.21 +ML {* (*==================*)
    9.22  *}
    9.23  ML {*
    9.24  *}
    9.25 @@ -29,6 +29,11 @@
    9.26  ML {*
    9.27  "~~~~~ fun , args:"; val () = ();
    9.28  "~~~~~ to  return val:"; val () = ();
    9.29 +
    9.30 +*}
    9.31 +text {**}
    9.32 +ML {*
    9.33 +
    9.34  *}
    9.35  end
    9.36  
    9.37 @@ -40,3 +45,4 @@
    9.38  
    9.39  (*=========================^^^ correct until here ^^^===========================*)
    9.40  
    9.41 +