(* Title:  "Knowledge/partial_fractions.sml"

     partial fraction decomposition

   Author: Jan Rocnik

   (c) due to copyright terms

*)

"--------------------------------------------------------";

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

"--------------------------------------------------------";

"----------- why helpless here ? ------------------------";

"----------- why not nxt = Model_Problem here ? ---------";

"----------- fun factors_from_solution ------------------";

"----------- Logic.unvarify_global ----------------------";

"----------- eval_drop_questionmarks --------------------";

"----------- = me for met_partial_fraction --------------";

"----------- autoCalculate for met_partial_fraction -----";

"----------- progr.vers.2: check erls for multiply_ansatz";

"----------- progr.vers.2: improve program --------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"----------- why helpless here ? ------------------------";

"----------- why helpless here ? ------------------------";

"----------- why helpless here ? ------------------------";

val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", 

  "stepResponse (x[n::real]::bool)"];

val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"], 

  ["SignalProcessing","Z_Transform","Inverse"]);

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

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

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

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

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

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

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

val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";

val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";

"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);

val ("ok", (_, _, ptp)) = locatetac tac (pt,p)

val (pt, p) = ptp;

"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = 

                           (p, ((pt, e_pos'),[]));

val pIopt = get_pblID (pt,ip);

ip = ([],Res); "false";

tacis; " = []";

pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";

(*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"

   THIS MEANS: replace no_meth by [no_meth] in Script.*)

(*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)

(*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)

"----------- why not nxt = Model_Problem here ? ---------";

"----------- why not nxt = Model_Problem here ? ---------";

"----------- why not nxt = Model_Problem here ? ---------";

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

"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);

val ("ok", (_, _, ptp)) = locatetac tac (pt,p);

val (pt, p) = ptp;

"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =

                           (p, ((pt, e_pos'),[]));

val pIopt = get_pblID (pt,ip);

ip = ([],Res); " = false";

tacis; " = []";                                         

pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);

member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";

(*                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into

nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).

This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.

See TODO.txt

*)

"----------- fun factors_from_solution ------------------";

"----------- fun factors_from_solution ------------------";

"----------- fun factors_from_solution ------------------";

val ctxt = Proof_Context.init_global @{theory Isac};

val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";

val SOME (_, t') = eval_factors_from_solution "" 0 t thy;

if term2str t' =

 "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"

then () else error "factors_from_solution broken";

"----------- Logic.unvarify_global ----------------------";

"----------- Logic.unvarify_global ----------------------";

"----------- Logic.unvarify_global ----------------------";

val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global

val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global

val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;

val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;

val test = HOLogic.mk_binop "Groups.plus_class.plus"

  (HOLogic.mk_binop "Rings.divide_class.divide" (A_var, denom1),

   HOLogic.mk_binop "Rings.divide_class.divide" (B_var, denom2));

if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()

  else error "HOLogic.mk_binop broken ?";

(* Logic.unvarify_global test

---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"

thus we need another fun var2free in termC.sml*)

"----------- = me for met_partial_fraction --------------";

"----------- = me for met_partial_fraction --------------";

"----------- = me for met_partial_fraction --------------";

val fmz =

  ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",

    "solveFor z", "decomposedFunction p_p"];

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

  ("Partial_Fractions", 

    ["partial_fraction", "rational", "simplification"],

    ["simplification","of_rationals","to_partial_fraction"]);

(*[ ], Pbl*)val (p,_,f,nxt,_,pt) =

              CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)

(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))")*)

(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)

(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "decomposedFunction p_p")*)

(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Partial_Fractions")*)

           (*05*)

(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["partial_fraction", "rational", "simplification"])*)

(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["simplification", "of_rationals", "to_partial_fraction"])*)

(*[ ], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["simplification", "of_rationals", "to_partial_fraction"])*)

(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_Rational")*)

(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("PolyEq", ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]))*)

            (*10*)

(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem)*)

(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)

(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)

(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions z_i")*)

(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "PolyEq")*)

(*[2], Pbl*)(*15*)

(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)

(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)

(*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)

(*[2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', z)"], "d2_polyeq_abcFormula_simplify"))*)

(*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify")*)

            (*20*)

(*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Or_to_List)*)

(*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions")*)

(*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)

(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - -1 / 4))")*)

(*[3], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ansatz_rls")*)

            (*25*)

(*[3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)")*)

(*[4], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "equival_trans")*)

(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)"*)

(*[5], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["z = 1 / 2"])*)

(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*nxt = Rewrite_Set "norm_Rational"*)

(*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac", ["normalise", "polynomial", "univariate", "equation"]*)

            (*30+1*)

(*[7], Pbl*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' [] pt'''; (*nxt = Model_Problem*)

(*[7], Pbl*)val (p'v,_,f,nxt'v,_,pt'v) = me nxt'''' p'''' [] pt''''; (*nxt = Add_Given "equality (3 = 3 * AA / 4)")*)

(*[7], Pbl*)val (p'v',_,f,nxt'v',_,pt'v') = me nxt'v p'v [] pt'v; (*nxt = Add_Given "solveFor AA")*)

(*[7], Pbl*)val (p'v'',_,f,nxt'v'',_,pt'v'') = me nxt'v' p'v' [] pt'v'; (*nxt = Add_Find "solutions AA_i")*)

(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac"*)

            (*35*)

(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*)

(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "normalise_poly"])*)

(*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)

(*[7, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"))*)

(*[7, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in")*)

               (*40*)

(*[7, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify"*)

(*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac", ["degree_1", "polynomial", "univariate", "equation"])*)

(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)

(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (3 + -3 / 4 * AA = 0)"*)

(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor AA"*)

    (*45*)

(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

    (*50*)

(*[7, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

    (*55*)

(*[7, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[7, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

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

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

    (*60*)

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

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

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

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

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

    (*65*)

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

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

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

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

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

    (*70*)

(*[10, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

    (*75*)

(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

    (*80*)

(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

    (*85*)

(*[10, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)

(*[10, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)

(*[10, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"*)

(*[10, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)

(*[10], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)"*)

    (*90*)

(*[11], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["AA = 4", "BB = -4"]*)

(*[11], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["partial_fraction", "rational", "simplification"]*)

(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*) 

case nxt of

  (_, End_Proof') => if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then () 

                     else error "= me .. met_partial_fraction f changed"

| _ => error "= me .. met_partial_fraction nxt changed";

show_pt_tac pt; (*[

([], Frm), Problem

 (''Partial_Fractions'',

  ??.\<^const>String.char.Char ''partial_fraction'' ''rational''

   ''simplification'')

. . . . . . . . . . Apply_Method ["simplification","of_rationals","to_partial_fraction"],

([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))

. . . . . . . . . . Rewrite_Set "norm_Rational",

([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)

. . . . . . . . . . Subproblem (Isac, ["abcFormula","degree_2","polynomial","univariate","equation"]),

([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)

. . . . . . . . . . Apply_Method ["PolyEq","solve_d2_polyeq_abc_equation"],

([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0

. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', z)], "d2_polyeq_abcFormula_simplify"),

([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or>

z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)

. . . . . . . . . . Rewrite_Set "polyeq_simplify",

([2,2], Res), z = 1 / 2 \<or> z = -1 / 4

. . . . . . . . . . Or_to_List ,

([2,3], Res), [z = 1 / 2, z = -1 / 4]

. . . . . . . . . . Check_elementwise "Assumptions",

([2,4], Res), [z = 1 / 2, z = -1 / 4]

. . . . . . . . . . Check_Postcond ["abcFormula","degree_2","polynomial","univariate","equation"],

([2], Res), [z = 1 / 2, z = -1 / 4]

. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4))",

([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))

. . . . . . . . . . Rewrite_Set "ansatz_rls",

([3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4)

. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)",

([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)

. . . . . . . . . . Rewrite_Set "equival_trans",

([4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)

. . . . . . . . . . Substitute ["z = 1 / 2"],

([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)

. . . . . . . . . . Rewrite_Set "norm_Rational",

([6], Res), 3 = 3 * AA / 4

. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),

([7], Pbl), solve (3 = 3 * AA / 4, AA)

. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],

([7,1], Frm), 3 = 3 * AA / 4

. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),

([7,1], Res), 3 - 3 * AA / 4 = 0

. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "make_ratpoly_in"),

([7,2], Res), 3 / 1 + -3 / 4 * AA = 0

. . . . . . . . . . Rewrite_Set "polyeq_simplify",

([7,3], Res), 3 + -3 / 4 * AA = 0

. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),

([7,4], Pbl), solve (3 + -3 / 4 * AA = 0, AA)

. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],

([7,4,1], Frm), 3 + -3 / 4 * AA = 0

. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "d1_polyeq_simplify"),

([7,4,1], Res), AA = -1 * 3 / (-3 / 4)

. . . . . . . . . . Rewrite_Set "polyeq_simplify",

([7,4,2], Res), AA = -3 / (-3 / 4)

. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",

([7,4,3], Res), AA = 4

. . . . . . . . . . Or_to_List ,

([7,4,4], Res), [AA = 4]

. . . . . . . . . . Check_elementwise "Assumptions",

([7,4,5], Res), [AA = 4]

. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],

([7,4], Res), [AA = 4]

. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],

([7], Res), [AA = 4]

. . . . . . . . . . Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)",

([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)

. . . . . . . . . . Substitute ["z = -1 / 4"],

([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)

. . . . . . . . . . Rewrite_Set "norm_Rational",

([9], Res), 3 = -3 * BB / 4

. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),

([10], Pbl), solve (3 = -3 * BB / 4, BB)

. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],

([10,1], Frm), 3 = -3 * BB / 4

. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),

([10,1], Res), 3 - -3 * BB / 4 = 0

. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "make_ratpoly_in"),

([10,2], Res), 3 / 1 + 3 / 4 * BB = 0

. . . . . . . . . . Rewrite_Set "polyeq_simplify",

([10,3], Res), 3 + 3 / 4 * BB = 0

. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),

([10,4], Pbl), solve (3 + 3 / 4 * BB = 0, BB)

. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],

([10,4,1], Frm), 3 + 3 / 4 * BB = 0

. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "d1_polyeq_simplify"),

([10,4,1], Res), BB = -1 * 3 / (3 / 4)

. . . . . . . . . . Rewrite_Set "polyeq_simplify",

([10,4,2], Res), BB = -3 / (3 / 4)

. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",

([10,4,3], Res), BB = -4

. . . . . . . . . . Or_to_List ,

([10,4,4], Res), [BB = -4]

. . . . . . . . . . Check_elementwise "Assumptions",

([10,4,5], Res), [BB = -4]

. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],

([10,4], Res), [BB = -4]

. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],

([10], Res), [BB = -4]

. . . . . . . . . . Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)",

([11], Frm), AA / (z - 1 / 2) + BB / (z - -1 / 4)

. . . . . . . . . . Substitute ["AA = 4","BB = -4"],

([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)

. . . . . . . . . . Check_Postcond ["partial_fraction","rational","simplification"],

([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)] 

val it = (): unit

*)

"----------- autoCalculate for met_partial_fraction -----";

"----------- autoCalculate for met_partial_fraction -----";

"----------- autoCalculate for met_partial_fraction -----";

reset_states ();

  val fmz =                                             

    ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", 

      "solveFor z", "decomposedFunction p_p"];

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

    ("Partial_Fractions", 

      ["partial_fraction", "rational", "simplification"],

      ["simplification","of_rationals","to_partial_fraction"]);

CalcTree [(fmz, (dI' ,pI' ,mI'))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc; 

val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1;

if p = ip andalso ip = ([], Res) then ()

  else error "autoCalculate for met_partial_fraction changed: final pos'";

val (Form f, tac, asms) = pt_extract (pt, p);

if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso

  terms2str' asms =

    "[BB = -4,BB is_polyexp,AA is_polyexp,AA = 4," ^

    "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^

    "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"

then case tac of NONE => ()

  | _ => error "me for met_partial_fraction changed: final result 1"

else error "me for met_partial_fraction changed: final result 2"

show_pt pt;

(*[

(([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])),

(([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),

(([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),

(([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),

(([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),

(([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |

z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),

(([2,2], Res), z = 1 / 2 | z = -1 / 4),

(([2,3], Res), [z = 1 / 2, z = -1 / 4]),

(([2,4], Res), [z = 1 / 2, z = -1 / 4]),

(([2], Res), [z = 1 / 2, z = -1 / 4]),

(([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),

(([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),

(([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),

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

(([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),

(([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),

(([6], Res), 3 = 3 * A / 4),

(([7], Pbl), solve (3 = 3 * A / 4, A)),

(([7,1], Frm), 3 = 3 * A / 4),

(([7,1], Res), 3 - 3 * A / 4 = 0),

(([7,2], Res), 3 / 1 + -3 / 4 * A = 0),

(([7,3], Res), 3 + -3 / 4 * A = 0),

(([7,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),

(([7,4,1], Frm), 3 + -3 / 4 * A = 0),

(([7,4,1], Res), A = -1 * 3 / (-3 / 4)),

(([7,4,2], Res), A = -3 / (-3 / 4)),

(([7,4,3], Res), A = 4),

(([7,4,4], Res), [A = 4]),

(([7,4,5], Res), [A = 4]),

(([7,4], Res), [A = 4]),

(([7], Res), [A = 4]),

(([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),

(([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),

(([9], Res), 3 = -3 * B / 4),

(([10], Pbl), solve (3 = -3 * B / 4, B)),

(([10,1], Frm), 3 = -3 * B / 4),

(([10,1], Res), 3 - -3 * B / 4 = 0),

(([10,2], Res), 3 / 1 + 3 / 4 * B = 0),

(([10,3], Res), 3 + 3 / 4 * B = 0),

(([10,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),

(([10,4,1], Frm), 3 + 3 / 4 * B = 0),

(([10,4,1], Res), B = -1 * 3 / (3 / 4)),

(([10,4,2], Res), B = -3 / (3 / 4)),

(([10,4,3], Res), B = -4),

(([10,4,4], Res), [B = -4]),

(([10,4,5], Res), [B = -4]),

(([10,4], Res), [B = -4]),

(([10], Res), [B = -4]),

(([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),

(([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),

(([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4))] *)

"----------- progr.vers.2: check erls for multiply_ansatz";

"----------- progr.vers.2: check erls for multiply_ansatz";

"----------- progr.vers.2: check erls for multiply_ansatz";

(*test for outcommented 3 lines in script: is norm_Rational strong enough?*)

val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";

val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;

term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";

val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)

term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^

  "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)

val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t''; 

if term2str t''' = "3 = (AA + -2 * BB + 4 * z * AA + 4 * z * BB) / 4" then () 

else error "ansatz_rls - multiply_ansatz - norm_Rational broken"; 

(*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)

val xxx = append_rls "multiply_ansatz_erls" norm_Rational 

  [Calc ("HOL.eq",eval_equal "#equal_")];

val multiply_ansatz = prep_rls @{theory} (

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

	  erls = xxx,

	  srls = Erls, calc = [], errpatts = [],

	  rules = 

	   [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})

	   ], 

	 scr = EmptyScr}:rls);

rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)

rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?*)

"----------- progr.vers.2: improve program --------------";

"----------- progr.vers.2: improve program --------------";

"----------- progr.vers.2: improve program --------------";

(*WN120318 stopped due to much effort with the test above*)

     "Script PartFracScript (f_f::real) (zzz::real) =                    " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)

     " (let f_f = Take f_f;                                       " ^

     "   (num_orig::real) = get_numerator f_f;                    " ^(*num_orig: 3*)

     "   f_f = (Rewrite_Set norm_Rational False) f_f;             " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)

     "   (numer::real) = get_numerator f_f;                       " ^(*numer: 24*)

     "   (denom::real) = get_denominator f_f;                     " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)

     "   (equ::bool) = (denom = (0::real));                       " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)

     "   (L_L::bool list) = (SubProblem (PolyEqX,                 " ^

     "     [abcFormula, degree_2, polynomial, univariate, equation], " ^

     "     [no_met]) [BOOL equ, REAL zzz]);                       " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)

     "   (facs::real) = factors_from_solution L_L;                " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)

     "   (eql::real) = Take (num_orig / facs);                    " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *) 

     "   (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql;  " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)

     "   (eq::bool) = Take (eql = eqr);                           " ^(*eq:  3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)

(*this has been tested below by rewrite_set_

     "   (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)

     "   (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)

     "   eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee;         " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*) 

NEXT try to outcomment the very next line..*)

     "   eq = (Try (Rewrite_Set equival_trans False)) eeeee;         " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*) 

     "   eq = drop_questionmarks eq;                              " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)

     "   (z1::real) = (rhs (NTH 1 L_L));                          " ^(*z1: 1 / 2*)

     "   (z2::real) = (rhs (NTH 2 L_L));                          " ^(*z2: -1 / 4*)

     "   (eq_a::bool) = Take eq;                                  " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)

     "   eq_a = (Substitute [zzz = z1]) eq;                       " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)

     "   eq_a = (Rewrite_Set norm_Rational False) eq_a;           " ^(*eq_a: 3 = 3 * A / 4*)

     "   (sol_a::bool list) =                                     " ^

     "     (SubProblem (IsacX, [univariate,equation], [no_met])   " ^

     "     [BOOL eq_a, REAL (A::real)]);                          " ^(*sol_a: [A = 4]*)

     "   (a::real) = (rhs (NTH 1 sol_a));                         " ^(*a: 4*)

     "   (eq_b::bool) = Take eq;                                  " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)

     "   eq_b = (Substitute [zzz = z2]) eq_b;                     " ^(*eq_b: *)

     "   eq_b = (Rewrite_Set norm_Rational False) eq_b;           " ^(*eq_b: *)

     "   (sol_b::bool list) =                                     " ^

     "     (SubProblem (IsacX, [univariate,equation], [no_met])   " ^

     "     [BOOL eq_b, REAL (B::real)]);                          " ^(*sol_b: [B = -4]*)

     "   (b::real) = (rhs (NTH 1 sol_b));                         " ^(*b: -4*)

     "   eqr = drop_questionmarks eqr;                            " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)

     "   (pbz::real) = Take eqr;                                  " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)

     "   pbz = ((Substitute [A = a, B = b]) pbz)                  " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)

     " in pbz)"