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

     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 "------ polyeq-2.sml ---------------------------------------------";

    13 "------ polyeq-1.sml ---------------------------------------------";

    14 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";

    15 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

    16 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

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

    18 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";

    19 "----------- rls make_polynomial_in ------------------------------";

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

    21 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";

    22 "-----------------------------------------------------------------";

    23 "-----------------------------------------------------------------";

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

    27 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";

    28 "----------- (a*b - (a+b)*x + x \<up> 2 = 0), (*Schalk 2,S.68Nr.44.a*)";

    29  val fmz = ["equality (a*b - (a+b)*x + x \<up> 2 = 0)",

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

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

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

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

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

    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;

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

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

    53 (*WN.2.5.03 TODO FIXME Matthias ?

    54  case f of

    55      Form'

    56 	 (Test_Out.FormKF

    57 	      (~1,EdUndef,0,Nundef,

    58 	       "[x = (a + b) / 2 + - 1 * sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) \<up> 2 / 2 \<up> 2 - a * b)]"))

    59 	 => ()

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

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

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

    65 "----------- (-64 + x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";

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

    67  val fmz = ["equality (-64 + x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)

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

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

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

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

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

    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;

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

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

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

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

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

    89 *)

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

    92 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

    93 "----------- (- 147 + 3*x \<up> 2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";

    94 val fmz = ["equality (- 147 + 3*x \<up> 2 = 0)",(*Schalk 2, S.66 Nr.1.b*)

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

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

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

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

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

   100 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; val (p,_,f,nxt,_,pt) = me nxt p [] pt;

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

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

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

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

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

   111 *)

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

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

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

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

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

   119 (*EP- 17 Schalk_I_p86_n5*)

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

   121 (* Refine.refine fmz ["univariate", "equation"];

   122 *)

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

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

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

   126 (* val nxt =

   127   ("Model_Problem",

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

   129   : string * tac*)

   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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

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

   135 (* val nxt =

   136   ("Subproblem",

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

   138   : string * tac *)

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

   140 (*val nxt =

   141   ("Model_Problem",

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

   143   : string * tac *)

   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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

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

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

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

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

   156 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";

   157 "----------- ((x+1)*(x+2) - (3*x - 2) \<up> 2=.. Schalk II s.68 Bsp 37";

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

   159 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2) \<up> 2=(2*x - 1) \<up> 2+(3*x - 1)*(x+1))",

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

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

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

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

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

   165 (* val nxt =

   166   ("Model_Problem",

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

   168   : string * tac *)

   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;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

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

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

   175 (* val nxt =

   176   ("Subproblem",

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

   178   : string * tac*)

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

   180 (*val nxt =

   181   ("Model_Problem",

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

   183   : string * tac*)

   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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

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

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

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

   195 "    -4 + x \<up> 2 =0     ";

   196 "    -4 + x \<up> 2 =0     ";

   197 "    -4 + x \<up> 2 =0     ";

   198 val fmz = ["equality ( -4 + x \<up> 2 =0)", "solveFor x", "solutions L"];

   199 (* val fmz = ["equality (1 + x \<up> 2 =0)", "solveFor x", "solutions L"];*)

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

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

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

   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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

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

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

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

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

   215 "----------- rls make_polynomial_in ------------------------------";

   216 "----------- rls make_polynomial_in ------------------------------";

   217 val thy = @{theory};

   218 val ctxt = @{context};

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

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

   221 (*3(b)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "R1");

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

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

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

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

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

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

   229 (*3(c)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "p");

   230 val t = TermC.str2term "y \<up> 2 + - 2 * (x * p) = 0";

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

   232 if UnparseC.term t' = "y \<up> 2 + - 2 * x * p = 0" then ()

   233 else error "make_polynomial_in (y \<up> 2 + - 2 * (x * p) = 0)";

   235 (*3(d)*)val (bdv,v) = (TermC.str2term "''bdv''", TermC.str2term "x2");

   236 val t = TermC.str2term

   237 "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";

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

   239 if UnparseC.term t' =

   240 "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"

   241 then ()

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

   243 "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";

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

   246 if UnparseC.term t' =

   247 "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"

   248 then ()

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

   250 "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";

   252 (*3(e)*)val (bdv,v) = (TermC.str2term "bdv", TermC.str2term "a");

   253 val t = TermC.str2term

   254 "A \<up> 2 + c \<up> 2 * (c / d) \<up> 2 + (-4 * (c / d) \<up> 2) * a \<up> 2 = 0";

   255 val NONE = rewrite_set_inst_ ctxt false [(bdv,v)] make_polynomial_in t;

   256 (* the invisible parentheses are as expected *)

   258 val t = TermC.str2term "(x + 1) * (x + 2) - (3 * x - 2) \<up> 2 - ((2 * x - 1) \<up> 2 + (3 * x - 1) * (x + 1)) = 0";

   259 rewrite_set_ ctxt false expand_binoms t;

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

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

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

   265 reset_states ();

   266 CalcTree

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

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

   269 Iterator 1;

   270 moveActiveRoot 1;

   272 autoCalculate 1 CompleteCalc;

   273 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;

   274 interSteps 1 ([1],Res)

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

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

   279 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";

   280 "----------- rls d2_polyeq_bdv_only_simplify ---------------------";

   281 val t = TermC.str2term "-6 * x + 5 * x \<up> 2 = (0::real)";

   282 val subst = [(TermC.str2term "(bdv::real)", TermC.str2term "(x::real)")];

   283 val SOME (t''''', _) = rewrite_set_inst_ ctxt true subst d2_polyeq_bdv_only_simplify t;

   284 (* steps in rls d2_polyeq_bdv_only_simplify:*)

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

   287 t |> UnparseC.term; t |> TermC.atomty;

   288 val thm = @{thm d2_prescind1};

   289 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;

   290 val SOME (t', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t; UnparseC.term t';

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

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

   294 t' |> UnparseC.term; t' |> TermC.atomty;

   295 val thm = @{thm d2_reduce_equation1};

   296 thm |> Thm.prop_of |> UnparseC.term; thm |> Thm.prop_of |> TermC.atomty;

   297 val SOME (t'', _) = rewrite_inst_ ctxt Rewrite_Ord.function_empty Rule_Set.empty true subst thm t'; UnparseC.term t'';

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

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

   300 *)

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

   302 else error "rls d2_polyeq_bdv_only_simplify broken";

author	wneuper <Walther.Neuper@jku.at>
	Thu, 04 Aug 2022 12:48:37 +0200
changeset 60509	2e0b7ca391dc
parent 60500	59a3af532717
child 60549	c0a775618258
permissions	-rw-r--r--