wneuper/isa: test/Tools/isac/Knowledge/polyeq-2.sml@0763aec4c5b6

     1 (* Title:  Knowledge/polyeq-1.sml

     2            testexamples for PolyEq, poynomial equations and equational systems

     3    Author: Richard Lang 2003

     4    (c) due to copyright terms

     5 WN030609: some expls dont work due to unfinished handling of 'expanded terms';

     6           others marked with TODO have to be checked, too.

     7 *)

     9 "-----------------------------------------------------------------";

    10 "table of contents -----------------------------------------------";

    11 "-----------------------------------------------------------------";

    12 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";

    13 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

    14 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

    15 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";

    16 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";

    17 "----------- rls make_polynomial_in ------------------------------";

    18 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

    19 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";

    20 "-----------------------------------------------------------------";

    21 "-----------------------------------------------------------------";

    24 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";

    25 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";

    26 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";

    27  val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",

    28  	    "solveFor x","solutions L"];

    29  val (dI',pI',mI') =

    30      ("PolyEq",["degree_2","expanded","univariate","equation"],

    31       ["PolyEq","complete_square"]);

    32 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    33 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    34 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    35 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    36 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    37 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    38 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    39 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    40 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    41 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    42 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    43 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    44 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    45 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    46 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    47 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    48 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    49 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    50 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;

    51 (*WN.2.5.03 TODO FIXME Matthias ?

    52  case f of

    53      Form'

    54 	 (Test_Out.FormKF

    55 	      (~1,EdUndef,0,Nundef,

    56 	       "[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]"))

    57 	 => ()

    58    | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";

    59  this will be simplified [x = a, x = b] to by Factor.ML*)

    62 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

    63 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

    64 "----------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

    65  val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)

    66  	    "solveFor x","solutions L"];

    67  val (dI',pI',mI') =

    68      ("PolyEq",["degree_2","expanded","univariate","equation"],

    69       ["PolyEq","complete_square"]);

    70 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    71 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    72 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    73 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    74 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    75 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    76 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    77 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    78 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    79 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    80 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    81 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    82 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    83 val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;

    84 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"

    85  case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()

    86 	 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";

    87 *)

    89 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

    90 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

    91 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

    92 val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)

    93  	    "solveFor x","solutions L"];

    94 val (dI',pI',mI') =

    95      ("PolyEq",["degree_2","expanded","univariate","equation"],

    96       ["PolyEq","complete_square"]);

    97 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

    98 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

    99 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   100 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   101 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   102 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   103 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   104 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   105 val (p,_,f,nxt,_,pt) = me nxt p [] pt;

   106 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"

   107  case f of Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()

   108 	 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";

   109 *)

   110 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()

   111 else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";

   114 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";

   115 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";

   116 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";

   117 (*EP-17 Schalk_I_p86_n5*)

   118 val fmz = ["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];

   119 (* Specify.refine fmz ["univariate","equation"];

   120 *)

   121 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

   122 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   124 (* val nxt =

   125   ("Model_Problem",

   126    Model_Problem ["normalise","polynomial","univariate","equation"])

   127   : string * tac*)

   128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   133 (* val nxt =

   134   ("Subproblem",

   135    Subproblem ("PolyEq",["polynomial","univariate","equation"]))

   136   : string * tac *)

   137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   138 (*val nxt =

   139   ("Model_Problem",

   140    Model_Problem ["degree_1","polynomial","univariate","equation"])

   141   : string * tac *)

   142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   146 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   149 case f of Test_Out.FormKF "[x = 2]" => ()

   150 	 | _ => error "polyeq.sml: diff.behav. in [x = 2]";

   153 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";

   154 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";

   155 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";

   156 (*is in rlang.sml, too*)

   157 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",

   158 	   "solveFor x","solutions L"];

   159 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

   160 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   161 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)

   162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   163 (* val nxt =

   164   ("Model_Problem",

   165    Model_Problem ["normalise","polynomial","univariate","equation"])

   166   : string * tac *)

   167 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   168 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   169 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   170 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   171 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   172 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   173 (* val nxt =

   174   ("Subproblem",

   175    Subproblem ("PolyEq",["polynomial","univariate","equation"]))

   176   : string * tac*)

   177 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   178 (*val nxt =

   179   ("Model_Problem",

   180    Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])

   181   : string * tac*)

   182 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   183 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   185 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   186 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   187 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   188 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   189 case f of Test_Out.FormKF "[x = 2 / 15, x = 1]" => ()

   190 	 | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";

   193 "    -4 + x^^^2 =0     ";

   194 "    -4 + x^^^2 =0     ";

   195 "    -4 + x^^^2 =0     ";

   196 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];

   197 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)

   198 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)

   199 val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);

   200 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   202 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   203 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   205 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   207 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

   209 case f of Test_Out.FormKF "[x = 2, x = -2]" => ()

   210 	 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";

   212 "----------- rls make_polynomial_in ------------------------------";

   213 "----------- rls make_polynomial_in ------------------------------";

   214 "----------- rls make_polynomial_in ------------------------------";

   215 (*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)

   216 (*WN.19.3.03 ---v-*)

   217 (*3(b)*)val (bdv,v) = (str2term "''bdv''", str2term "R1");

   218 val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";

   219 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;

   220 if UnparseC.term t' = "-1 * R * R2 + R2 * R1 + -1 * R * R1 = 0" then ()

   221 else error "make_polynomial_in (-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0)";

   222 "-1 * R * R2 + (R2 + -1 * R) * R1 = 0";

   223 (*WN.19.3.03 ---^-*)

   225 (*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");

   226 val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";

   227 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;

   228 if UnparseC.term t' = "y ^^^ 2 + -2 * x * p = 0" then ()

   229 else error "make_polynomial_in (y ^^^ 2 + -2 * (x * p) = 0)";

   231 (*3(d)*)val (bdv,v) = (str2term "''bdv''", str2term "x2");

   232 val t = str2term

   233 "A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";

   234 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;

   235 if UnparseC.term t' =

   236 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) +\n-1 * x3 * y1 * (1 / 2) +\ny1 * (1 / 2) * x2 +\n-1 * y3 * (1 / 2) * x2 =\n0"

   237 then ()

   238 else error "make_polynomial_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";

   239 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";

   241 val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;

   242 if UnparseC.term t' =

   243 "A / 1 + x1 * y3 / 2 + x3 * y2 / 2 + -1 * x1 * y2 / 2 + -1 * x3 * y1 / 2 +\ny1 * x2 / 2 +\n-1 * y3 * x2 / 2 =\n0"

   244 then ()

   245 else error "make_ratpoly_in (A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1...";

   246 "A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) + -1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + -1 * y3 * (1 / 2)) * x2 = 0";

   248 (*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");

   249 val t = str2term

   250 "A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";

   251 val NONE = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;

   252 (* the invisible parentheses are as expected *)

   254 val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";

   255 Rewrite.trace_on:=(*true*)false;

   256 rewrite_set_ thy false expand_binoms t;

   257 Rewrite.trace_on:=false;

   260 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

   261 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

   262 "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

   263 reset_states ();

   264 CalcTree

   265 [(["equality ((3::real)*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],

   266   ("PolyEq",["univariate","equation"],["no_met"]))];

   267 Iterator 1;

   268 moveActiveRoot 1;

   270 autoCalculate 1 CompleteCalc;

   271 val ((pt,p),_) = get_calc 1; show_pt pt;

   272 interSteps 1 ([1],Res)

   273 (*BEFORE Isabelle2002 --> 2011: <ERROR> no Rewrite_Set... </ERROR> ?see fun prep_rls?*);

   276 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";

   277 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";

   278 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";

   279 val t = str2term "-6 * x + 5 * x ^^^ 2 = (0::real)";

   280 val subst = [(str2term "(bdv::real)", str2term "(x::real)")];

   281 val SOME (t''''', _) = rewrite_set_inst_ thy true subst d2_polyeq_bdv_only_simplify t;

   282 (* steps in rls d2_polyeq_bdv_only_simplify:*)

   284 (*-6 * x + 5 * x ^ 2 = 0 : Rewrite_Inst (["(''bdv'',x)"],("d2_prescind1","")) --> x * (-6 + 5 * x) = 0*)

   285 t |> UnparseC.term; t |> atomty;

   286 val thm = ThmC.numerals_to_Free @{thm d2_prescind1};

   287 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;

   288 val SOME (t', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t; UnparseC.term t';

   290 (*x * (-6 + 5 * x) = 0   : Rewrite_Inst (["(''bdv'',x)"],("d2_reduce_equation1",""))

   291                                                                         --> x = 0 | -6 + 5 * x = 0*)

   292 t' |> UnparseC.term; t' |> atomty;

   293 val thm = ThmC.numerals_to_Free @{thm d2_reduce_equation1};

   294 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> atomty;

   295 val SOME (t'', _) = rewrite_inst_ thy e_rew_ord Rule_Set.empty true subst thm t'; UnparseC.term t'';

   296 (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"

   297    instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"

   298 *)

   299 if UnparseC.term t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()

   300 else error "rls d2_polyeq_bdv_only_simplify broken";

author	Walther Neuper <walther.neuper@jku.at>
	Mon, 11 May 2020 20:49:27 +0200
changeset 59965	0763aec4c5b6
parent 59959	0f0718c61f68
child 59968	5dd1d96cb467
permissions	-rw-r--r--