val prod = mk_prod e_term facs; 

 val prod = mk_prod e_term facs; 

 term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";

 term2str prod = "(z + -1 * (1 / 2)) * (z + -1 * (-1 / 4))";

 val prod = mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"]; 

 val prod = mk_prod e_term [str2term "x + 1", str2term "x + 2", str2term "x + 3"]; 

 term2str prod = "(x + 1) * (x + 2) * (x + 3)";

 term2str prod = "(x + 1) * (x + 2) * (x + 3)";

 *)

 *)

 fun factors_from_solution sol = 

 fun factors_from_solution sol = 

   let val ts = HOLogic.dest_list sol

   let val ts = HOLogic.dest_list sol

   in mk_prod e_term (map fac_from_sol ts) end;

   in mk_prod e_term (map fac_from_sol ts) end;

 subsubsection {*Build a rule-set for ansatz*}

 subsubsection {*Build a rule-set for ansatz*}

 text {* the "ansatz" rules violate the principle that each variable on 

 text {* the "ansatz" rules violate the principle that each variable on 

   the right-hand-side must also occur on the left-hand-side of the rule:

   the right-hand-side must also occur on the left-hand-side of the rule:

   A, B, etc don't.

   A, B, etc don't.

   Thus the rewriter marks these variables with question marks: ?A, ?B, etc.

   Thus the rewriter marks these variables with question marks: ?A, ?B, etc.

   *}

   *}

 ML {*

 ML {*

 val ansatz_rls = prep_rls(

 val ansatz_rls = prep_rls(

   Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 

   Rls {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",dummy_ord), 

 	  erls = e_rls, srls = Erls, calc = [],

 	  erls = e_rls, srls = Erls, calc = [],

 	    Thm ("multiply_eq2",num_str @{thm multiply_eq2})

 	    Thm ("multiply_eq2",num_str @{thm multiply_eq2})

 	   ], 

 	   ], 

 	 scr = EmptyScr});

 	 scr = EmptyScr});

 *}

 *}

 ML {*

 ML {*

 val SOME (ttttt,_) = rewrite_set_ @{theory Isac} false ansatz_rls expr';

 val SOME (ttttt,_) = rewrite_set_ @{theory Isac} false ansatz_rls expr';

 *}

 *}

 ML {*

 ML {*

 term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";

 term2str expr' = "3 / ((z - 1 / 2) * (z - -1 / 4))";

 term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";

 term2str ttttt = "?A / (z - 1 / 2) + ?B / (z - -1 / 4)";

 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";

 if f2str fb = "[B = -4]" then () else error "part.fract. eq4_1";

 *}

 *}

 subsubsection {*substitute expression with solutions*}

 subsubsection {*substitute expression with solutions*}

 ML {*

 ML {*

 *}

 *}

 ML {*thy*}

 ML {*thy*}

 section {*Implement the Specification and the Method \label{spec-meth}*}

 section {*Implement the Specification and the Method \label{spec-meth}*}

 text{*==============================================*}

 text{*==============================================*}

 without "?" BUT THEN WRONG "*** upd_env_opt: (NONE,24 = ?A * ..."*)

 without "?" BUT THEN WRONG "*** upd_env_opt: (NONE,24 = ?A * ..."*)

 trace_script := true;

 trace_script := true;

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

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

 (*([6], Res), 24 = ?A * (1 / 2 + -1 * (-1 / 4)) + ?B * (1 / 2 + -1 * (1 / 2))*)

 (*([6], Res), 24 = ?A * (1 / 2 + -1 * (-1 / 4)) + ?B * (1 / 2 + -1 * (1 / 2))*)

 *}

 *}

 ML {*

 ML {*

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

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

 (*([7], Res), 24 = ?A * 3 / 4*)

 (*([7], Res), 24 = ?A * 3 / 4*)

 show_pt pt;

 show_pt pt;

 *}

 *}

 ML {*

 ML {*

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

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

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

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

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

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

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

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