wneuper@59549: (* Title: "Knowledge/partial_fractions.sml" wneuper@59549: partial fraction decomposition neuper@42289: Author: Jan Rocnik neuper@42289: (c) due to copyright terms neuper@42289: *) neuper@42289: neuper@42289: "--------------------------------------------------------"; neuper@42289: "table of contents --------------------------------------"; neuper@42289: "--------------------------------------------------------"; neuper@42305: "----------- why helpless here ? ------------------------"; neuper@42310: "----------- why not nxt = Model_Problem here ? ---------"; neuper@42359: "----------- fun factors_from_solution ------------------"; neuper@42359: "----------- Logic.unvarify_global ----------------------"; neuper@42359: "----------- eval_drop_questionmarks --------------------"; neuper@42376: "----------- = me for met_partial_fraction --------------"; wneuper@59248: "----------- autoCalculate for met_partial_fraction -----"; neuper@42386: "----------- progr.vers.2: check erls for multiply_ansatz"; neuper@42386: "----------- progr.vers.2: improve program --------------"; wneuper@59550: "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------"; wneuper@59550: "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------"; neuper@42289: "--------------------------------------------------------"; neuper@42289: "--------------------------------------------------------"; neuper@42289: "--------------------------------------------------------"; neuper@42289: neuper@42289: neuper@42305: "----------- why helpless here ? ------------------------"; neuper@42305: "----------- why helpless here ? ------------------------"; neuper@42305: "----------- why helpless here ? ------------------------"; walther@60329: val fmz = ["filterExpression (X z = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))", wneuper@59550: "functionName X_z", "stepResponse (x[n::real]::bool)"]; wneuper@59592: val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"], walther@59997: ["SignalProcessing", "Z_Transform", "Inverse"]); neuper@42305: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; neuper@42305: val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given"; neuper@42305: val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find"; neuper@42305: val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory"; neuper@42305: val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem"; neuper@42305: val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method"; neuper@42305: val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method"; walther@60329: 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))"; walther@60329: 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)))"; walther@59749: "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt); walther@59804: val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p) neuper@42305: val (pt, p) = ptp; walther@59765: "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = neuper@42305: (p, ((pt, e_pos'),[])); neuper@42305: val pIopt = get_pblID (pt,ip); neuper@42305: ip = ([],Res); "false"; neuper@42305: tacis; " = []"; neuper@42405: pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*) walther@60017: member op = [Pbl,Met] p_ ; "false"; walther@59760: (*Step_Solve.do_next (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'" wneuper@59585: THIS MEANS: replace no_meth by [no_meth] in Program.*) walther@59765: (*WAS val ("helpless",_) = Step.do_next p ((pt, e_pos'),[]) *) neuper@42305: (*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*) neuper@42289: neuper@42310: "----------- why not nxt = Model_Problem here ? ---------"; neuper@42310: "----------- why not nxt = Model_Problem here ? ---------"; neuper@42310: "----------- why not nxt = Model_Problem here ? ---------"; neuper@42313: val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; walther@59749: "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); walther@59804: val ("ok", (_, _, ptp)) = Step.by_tactic tac (pt,p); neuper@42313: val (pt, p) = ptp; walther@59765: "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = neuper@42313: (p, ((pt, e_pos'),[])); neuper@42313: val pIopt = get_pblID (pt,ip); neuper@42313: ip = ([],Res); " = false"; neuper@42313: tacis; " = []"; neuper@42405: pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*); walther@60017: member op = [Pbl,Met] p_; " = false"; walther@60242: (* \ \ \ \ \ \ \ \ \ \ \ ^ leads into walther@59760: Step_Solve.do_next, which is definitely WRONG (should be nxt_specify_ for FIND_ADD). walther@59845: This ERROR seems to be introduced together with ctxt, concerns Apply_Method without implicit_take. neuper@42313: See TODO.txt neuper@42313: *) neuper@42310: neuper@42359: "----------- fun factors_from_solution ------------------"; neuper@42359: "----------- fun factors_from_solution ------------------"; neuper@42359: "----------- fun factors_from_solution ------------------"; wneuper@59592: val ctxt = Proof_Context.init_global @{theory Isac_Knowledge}; walther@60329: val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = - 1 / 4]"; jan@42352: val SOME (_, t') = eval_factors_from_solution "" 0 t thy; walther@59868: if UnparseC.term t' = walther@60329: "factors_from_solution [z = 1 / 2, z = - 1 / 4] = (z - 1 / 2) * (z - - 1 / 4)" jan@42352: then () else error "factors_from_solution broken"; jan@42352: neuper@42359: "----------- Logic.unvarify_global ----------------------"; neuper@42359: "----------- Logic.unvarify_global ----------------------"; neuper@42359: "----------- Logic.unvarify_global ----------------------"; neuper@42359: val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global neuper@42359: val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global jan@42352: walther@60329: val denom1 = parseNEW ctxt "(z + - 1 * (1 / 2))::real" |> the; walther@60329: val denom2 = parseNEW ctxt "(z + - 1 * (- 1 / 4))::real" |> the; neuper@42359: wenzelm@60309: val test = HOLogic.mk_binop \<^const_name>\plus\ wenzelm@60309: (HOLogic.mk_binop \<^const_name>\divide\ (A_var, denom1), wenzelm@60309: HOLogic.mk_binop \<^const_name>\divide\ (B_var, denom2)); neuper@42359: walther@60329: if UnparseC.term test = "?A / (z + - 1 * (1 / 2)) + ?B / (z + - 1 * (- 1 / 4))" then () neuper@42359: else error "HOLogic.mk_binop broken ?"; neuper@42359: neuper@42359: (* Logic.unvarify_global test neuper@42359: ---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z" neuper@42359: thus we need another fun var2free in termC.sml*) neuper@42359: neuper@42376: "----------- = me for met_partial_fraction --------------"; neuper@42376: "----------- = me for met_partial_fraction --------------"; neuper@42376: "----------- = me for met_partial_fraction --------------"; wneuper@59534: val fmz = walther@60329: ["functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))", wneuper@59534: "solveFor z", "decomposedFunction p_p"]; wneuper@59534: val (dI',pI',mI') = wneuper@59534: ("Partial_Fractions", wneuper@59534: ["partial_fraction", "rational", "simplification"], walther@59997: ["simplification", "of_rationals", "to_partial_fraction"]); wneuper@59534: (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = wneuper@59534: CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*) walther@60329: (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))")*) wneuper@59534: (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*) wneuper@59534: (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "decomposedFunction p_p")*) wneuper@59534: (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Partial_Fractions")*) wneuper@59534: (*05*) wneuper@59534: (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["partial_fraction", "rational", "simplification"])*) wneuper@59534: (*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["simplification", "of_rationals", "to_partial_fraction"])*) wneuper@59534: (*[ ], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["simplification", "of_rationals", "to_partial_fraction"])*) wneuper@59534: (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_Rational")*) wneuper@59534: (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("PolyEq", ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]))*) wneuper@59534: (*10*) wneuper@59534: (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem)*) walther@60329: (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (- 1 + - 2 * z + 8 * z \ 2 = 0)")*) wneuper@59534: (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*) wneuper@59534: (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions z_i")*) wneuper@59534: (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "PolyEq")*) wneuper@59534: (*[2], Pbl*)(*15*) wneuper@59534: (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*) wneuper@59534: (*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*) wneuper@59534: (*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*) wneuper@59534: (*[2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', z)"], "d2_polyeq_abcFormula_simplify"))*) wneuper@59534: (*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify")*) wneuper@59534: (*20*) wneuper@59534: (*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Or_to_List)*) wneuper@59534: (*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions")*) wneuper@59534: (*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*) walther@60329: (*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - - 1 / 4))")*) wneuper@59534: (*[3], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ansatz_rls")*) wneuper@59534: (*25*) walther@60329: (*[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)")*) wneuper@59534: (*[4], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "equival_trans")*) walther@60329: (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 = AA * (z - - 1 / 4) + BB * (z - 1 / 2)"*) wneuper@59534: (*[5], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["z = 1 / 2"])*) wneuper@59534: (*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*nxt = Rewrite_Set "norm_Rational"*) wneuper@59592: (*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac_Knowledge", ["normalise", "polynomial", "univariate", "equation"]*) wneuper@59534: (*30+1*) wneuper@59534: (*[7], Pbl*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' [] pt'''; (*nxt = Model_Problem*) wneuper@59534: (*[7], Pbl*)val (p'v,_,f,nxt'v,_,pt'v) = me nxt'''' p'''' [] pt''''; (*nxt = Add_Given "equality (3 = 3 * AA / 4)")*) wneuper@59534: (*[7], Pbl*)val (p'v',_,f,nxt'v',_,pt'v') = me nxt'v p'v [] pt'v; (*nxt = Add_Given "solveFor AA")*) wneuper@59534: (*[7], Pbl*)val (p'v'',_,f,nxt'v'',_,pt'v'') = me nxt'v' p'v' [] pt'v'; (*nxt = Add_Find "solutions AA_i")*) wneuper@59592: (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac_Knowledge"*) wneuper@59534: (*35*) wneuper@59534: (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*) wneuper@59534: (*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "normalise_poly"])*) wneuper@59534: (*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*) wneuper@59534: (*[7, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite ("all_left", "\ ?b =!= 0 \ (?a = ?b) = (?a - ?b = 0)"))*) wneuper@59534: (*[7, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in")*) wneuper@59534: (*40*) wneuper@59534: (*[7, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify"*) wneuper@59592: (*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac_Knowledge", ["degree_1", "polynomial", "univariate", "equation"])*) wneuper@59534: (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*) wneuper@59534: (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (3 + -3 / 4 * AA = 0)"*) wneuper@59534: (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor AA"*) wneuper@59534: (*45*) wneuper@59534: (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*50*) wneuper@59534: (*[7, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*55*) wneuper@59534: (*[7, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[7], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[8], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*60*) wneuper@59534: (*[8], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[9], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*65*) wneuper@59534: (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*70*) wneuper@59534: (*[10, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*75*) wneuper@59534: (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*80*) wneuper@59534: (*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*85*) wneuper@59534: (*[10, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *) wneuper@59534: (*[10, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*) wneuper@59534: (*[10, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"*) wneuper@59534: (*[10, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*) neuper@42376: walther@60329: (*[10], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "AA / (z - 1 / 2) + BB / (z - - 1 / 4)"*) wneuper@59534: (*90*) wneuper@59534: (*[11], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["AA = 4", "BB = -4"]*) wneuper@59534: (*[11], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["partial_fraction", "rational", "simplification"]*) wneuper@59534: (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*) wneuper@59534: wneuper@59534: case nxt of walther@60329: (_, End_Proof') => if f2str f = "4 / (z - 1 / 2) + -4 / (z - - 1 / 4)" then () wneuper@59534: else error "= me .. met_partial_fraction f changed" wneuper@59534: | _ => error "= me .. met_partial_fraction nxt changed"; wneuper@59534: walther@59983: Test_Tool.show_pt_tac pt; (**) neuper@42376: wneuper@59248: "----------- autoCalculate for met_partial_fraction -----"; wneuper@59248: "----------- autoCalculate for met_partial_fraction -----"; wneuper@59248: "----------- autoCalculate for met_partial_fraction -----"; Walther@60549: States.reset (); neuper@42413: val fmz = walther@60329: ["functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))", neuper@42413: "solveFor z", "decomposedFunction p_p"]; neuper@42413: val (dI', pI', mI') = neuper@42413: ("Partial_Fractions", neuper@42413: ["partial_fraction", "rational", "simplification"], walther@59997: ["simplification", "of_rationals", "to_partial_fraction"]); neuper@42413: CalcTree [(fmz, (dI' ,pI' ,mI'))]; neuper@42413: Iterator 1; neuper@42413: moveActiveRoot 1; wneuper@59248: autoCalculate 1 CompleteCalc; neuper@42413: Walther@60549: val ((pt,p),_) = States.get_calc 1; val ip = States.get_pos 1 1; neuper@42413: if p = ip andalso ip = ([], Res) then () wneuper@59248: else error "autoCalculate for met_partial_fraction changed: final pos'"; neuper@42413: walther@59983: val (Form f, tac, asms) = ME_Misc.pt_extract (pt, p); walther@60329: if UnparseC.term f = "4 / (z - 1 / 2) + -4 / (z - - 1 / 4)" andalso walther@59868: UnparseC.terms_short asms = wneuper@59534: "[BB = -4,BB is_polyexp,AA is_polyexp,AA = 4," ^ walther@60329: "lhs (- 1 + - 2 * z + 8 * z \ 2 = 0) has_degree_in z = 2," ^ walther@60329: "lhs (- 1 + - 2 * z + 8 * z \ 2 = 0) is_poly_in z,z = 1 / 2,z = - 1 / 4,z is_polyexp]" wneuper@59253: then case tac of NONE => () wneuper@59534: | _ => error "me for met_partial_fraction changed: final result 1" wneuper@59534: else error "me for met_partial_fraction changed: final result 2" neuper@42413: walther@59983: Test_Tool.show_pt pt; (**) neuper@42413: neuper@42386: "----------- progr.vers.2: check erls for multiply_ansatz"; neuper@42386: "----------- progr.vers.2: check erls for multiply_ansatz"; neuper@42386: "----------- progr.vers.2: check erls for multiply_ansatz"; neuper@42386: (*test for outcommented 3 lines in script: is norm_Rational strong enough?*) Walther@60565: val t = TermC.parse_test @{context} "(3 / ((- 1 + - 2 * z + 8 * z \ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - - 1 / 4)))"; wneuper@59592: val SOME (t', _) = rewrite_set_ @{theory Isac_Knowledge} true ansatz_rls t; walther@60329: UnparseC.term t' = "3 / ((- 1 + - 2 * z + 8 * z \ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - - 1 / 4)"; neuper@42386: wneuper@59592: val SOME (t'', _) = rewrite_set_ @{theory Isac_Knowledge} true multiply_ansatz t'; (*true*) walther@60329: UnparseC.term t'' = "(z - 1 / 2) * (z - - 1 / 4) * 3 / ((- 1 + - 2 * z + 8 * z \ 2) * 3 / 24) =\n" ^ walther@60329: "?A * (z - - 1 / 4) + ?B * (z - 1 / 2)"; (*true*) neuper@42386: wneuper@59592: val SOME (t''', _) = rewrite_set_ @{theory Isac_Knowledge} true norm_Rational t''; walther@60329: if UnparseC.term t''' = "3 = (AA + - 2 * BB + 4 * z * AA + 4 * z * BB) / 4" then () neuper@52103: else error "ansatz_rls - multiply_ansatz - norm_Rational broken"; neuper@42386: neuper@42386: (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*) walther@59852: val xxx = Rule_Set.append_rules "multiply_ansatz_erls" norm_Rational wenzelm@60309: [Eval (\<^const_name>\HOL.eq\,eval_equal "#equal_")]; neuper@42386: s1210629013@55444: val multiply_ansatz = prep_rls @{theory} ( walther@59851: Rule_Set.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord), neuper@42386: erls = xxx, walther@59851: srls = Rule_Set.Empty, calc = [], errpatts = [], neuper@42386: rules = walther@59871: [Thm ("multiply_2nd_order",ThmC.numerals_to_Free @{thm multiply_2nd_order}) neuper@42386: ], walther@59878: scr = Empty_Prog}:rls); neuper@42386: neuper@42386: rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*) wneuper@59514: rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?*) neuper@42386: neuper@42386: "----------- progr.vers.2: improve program --------------"; neuper@42386: "----------- progr.vers.2: improve program --------------"; neuper@42386: "----------- progr.vers.2: improve program --------------"; neuper@42386: (*WN120318 stopped due to much effort with the test above*) walther@60329: "Program PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z)), zzz: z*) neuper@42386: " (let f_f = Take f_f; " ^ neuper@42386: " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*) walther@60329: " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (- 1 + - 2 * z + 8 * z \ 2)*) neuper@42386: " (numer::real) = get_numerator f_f; " ^(*numer: 24*) walther@60329: " (denom::real) = get_denominator f_f; " ^(*denom: - 1 + - 2 * z + 8 * z \ 2*) walther@60329: " (equ::bool) = (denom = (0::real)); " ^(*equ: - 1 + - 2 * z + 8 * z \ 2 = 0*) wneuper@59476: " (L_L::bool list) = (SubProblem (PolyEqX, " ^ neuper@42386: " [abcFormula, degree_2, polynomial, univariate, equation], " ^ walther@60329: " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = - 1 / 4]*) walther@60329: " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - - 1 / 4)*) walther@60329: " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - - 1 / 4)) *) walther@60329: " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - - 1 / 4)*) walther@60329: " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - - 1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - - 1 / 4)*) neuper@42386: (*this has been tested below by rewrite_set_ neuper@42386: " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**) neuper@42386: " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**) walther@60329: " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - - 1 / 4) + ?B * (z - 1 / 2)*) neuper@42386: NEXT try to outcomment the very next line..*) walther@60329: " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - - 1 / 4) + ?B * (z - 1 / 2)*) walther@60329: " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - - 1 / 4) + B * (z - 1 / 2)*) neuper@42386: " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*) walther@60329: " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: - 1 / 4*) walther@60329: " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - - 1 / 4) + B * (z - 1 / 2)*) walther@60329: " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - - 1 / 4) + B * (1 / 2 - 1 / 2)*) neuper@42386: " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*) neuper@42386: " (sol_a::bool list) = " ^ wneuper@59476: " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^ neuper@42386: " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*) neuper@42386: " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*) walther@60329: " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - - 1 / 4) + B * (z - 1 / 2)*) neuper@42386: " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *) neuper@42386: " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *) neuper@42386: " (sol_b::bool list) = " ^ wneuper@59476: " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^ neuper@42386: " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*) neuper@42386: " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*) walther@60329: " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - - 1 / 4)*) walther@60329: " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - - 1 / 4)*) walther@60329: " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - - 1 / 4)*) wneuper@59550: " in pbz)"; neuper@42386: wneuper@59550: "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------"; wneuper@59550: "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------"; wneuper@59550: "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------"; wneuper@59550: val fmz_from_Subproblem_of_Inverse_sub = (*see --- test [SignalProcessing,Z_Transform,Inverse_s.."*) walther@60329: (["functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))", "solveFor z", wneuper@59550: "decomposedFunction p_p'''"], wneuper@59592: ("Isac_Knowledge", ["partial_fraction", "rational", "simplification"], wneuper@59550: ["simplification", "of_rationals", "to_partial_fraction"])) wneuper@59550: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz_from_Subproblem_of_Inverse_sub)]; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt; wneuper@59550: walther@60329: if fst nxt = "End_Proof'" andalso f2str f = "4 / (z - 1 / 2) + -4 / (z - - 1 / 4)" then () wneuper@59550: else error "--- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---"; wneuper@59550: wneuper@59550: wneuper@59550: "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------"; wneuper@59550: "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------"; wneuper@59550: "----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------"; Walther@60549: States.reset (); wneuper@59550: (*val PblObj {fmz_from_Subproblem_of_Inverse_sub, ...} = get_obj I pt (fst p) wneuper@59550: see --- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";*) wneuper@59550: wneuper@59550: val fmz_from_Subproblem_of_Inverse_sub = (*see --- test [SignalProcessing,Z_Transform,Inverse_s.."*) walther@60329: (["functionTerm (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))", "solveFor z", wneuper@59550: "decomposedFunction p_p'''"], wneuper@59592: ("Isac_Knowledge", ["partial_fraction", "rational", "simplification"], wneuper@59550: ["simplification", "of_rationals", "to_partial_fraction"])); wneuper@59550: CalcTree [fmz_from_Subproblem_of_Inverse_sub]; wneuper@59550: Iterator 1; wneuper@59550: moveActiveRoot 1; wneuper@59550: (* wneuper@59550: autoCalculate 1 CompleteCalc; wneuper@59550: exception Empty raised (line 429 of "library.ML") TODO during lucin: *) wneuper@59550: wneuper@59550: (* walther@59901: LItool.trace_on := true; wneuper@59550: walther@59997: @@@ program ["simplification", "of_rationals", "to_partial_fraction"] wneuper@59550: @@@ istate [" walther@60329: (f_f, 3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))", " wneuper@59550: (zzz, z)"] walther@60329: @@@ next leaf 'Take f_f' ---> Program.Tac 'Take (3 / (z * (z - 1 / 4 + - 1 / 8 * (1 / z))))' wneuper@59550: *) wneuper@59550: