1.1 --- a/test/Tools/isac/Test_Some.thy Thu May 30 12:39:13 2019 +0200
1.2 +++ b/test/Tools/isac/Test_Some.thy Sat Jun 01 11:09:19 2019 +0200
1.3 @@ -67,10 +67,998 @@
1.4 "~~~~~ fun xxx , args:"; val () = ();
1.5 \<close>
1.6
1.7 -section \<open>===================================================================================\<close>
1.8 +section \<open>================= "Knowledge/partial_fractions.sml" ============================\<close>
1.9 ML \<open>
1.10 "~~~~~ fun xxx , args:"; val () = ();
1.11 \<close> ML \<open>
1.12 +(* Title: partial fraction decomposition
1.13 + Author: Jan Rocnik
1.14 + (c) due to copyright terms
1.15 +*)
1.16 +
1.17 +"--------------------------------------------------------";
1.18 +"table of contents --------------------------------------";
1.19 +"--------------------------------------------------------";
1.20 +"----------- why helpless here ? ------------------------";
1.21 +"----------- why not nxt = Model_Problem here ? ---------";
1.22 +"----------- fun factors_from_solution ------------------";
1.23 +"----------- Logic.unvarify_global ----------------------";
1.24 +"----------- eval_drop_questionmarks --------------------";
1.25 +"----------- = me for met_partial_fraction --------------";
1.26 +"----------- autoCalculate for met_partial_fraction -----";
1.27 +"----------- progr.vers.2: check erls for multiply_ansatz";
1.28 +"----------- progr.vers.2: improve program --------------";
1.29 +"--------------------------------------------------------";
1.30 +"--------------------------------------------------------";
1.31 +"--------------------------------------------------------";
1.32 +
1.33 +
1.34 +"----------- why helpless here ? ------------------------";
1.35 +"----------- why helpless here ? ------------------------";
1.36 +"----------- why helpless here ? ------------------------";
1.37 +\<close> ML \<open>
1.38 +val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
1.39 + "stepResponse (x[n::real]::bool)"];
1.40 +val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
1.41 + ["SignalProcessing","Z_Transform","Inverse"]);
1.42 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
1.43 +\<close> ML \<open>
1.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
1.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
1.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
1.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
1.48 +\<close> ML \<open>
1.49 +(*CURRENT*)(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Specify_Method ["SignalProcessing", "Z_Transform", "Inverse"])*)
1.50 +\<close> ML \<open>
1.51 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
1.52 +(*CURRENT*)(*ERROR in creating the environment from formal args. of partial_function "HOL.eq"
1.53 +and the actual args., ie. items of the guard of "["SignalProcessing","Z_Transform","Inverse"]" by "assoc_by_type":
1.54 +formal arg "TYPE('a)" doesn't mach an actual arg.
1.55 +with:
1.56 +3 formal args: ["TYPE('a)","X_eq","z"]
1.57 +2 actual args: ["X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))","x [n]"]*)
1.58 +\<close> ML \<open>
1.59 +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))";
1.60 +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)))";
1.61 +\<close> ML \<open>
1.62 +"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
1.63 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
1.64 +val (pt, p) = ptp;
1.65 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
1.66 + (p, ((pt, e_pos'),[]));
1.67 +val pIopt = get_pblID (pt,ip);
1.68 +ip = ([],Res); "false";
1.69 +tacis; " = []";
1.70 +pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
1.71 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
1.72 +(*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
1.73 + THIS MEANS: replace no_meth by [no_meth] in Script.*)
1.74 +(*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
1.75 +(*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
1.76 +
1.77 +\<close> ML \<open>
1.78 +"----------- why not nxt = Model_Problem here ? ---------";
1.79 +"----------- why not nxt = Model_Problem here ? ---------";
1.80 +"----------- why not nxt = Model_Problem here ? ---------";
1.81 +val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
1.82 +"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
1.83 +val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
1.84 +val (pt, p) = ptp;
1.85 +"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
1.86 + (p, ((pt, e_pos'),[]));
1.87 +val pIopt = get_pblID (pt,ip);
1.88 +ip = ([],Res); " = false";
1.89 +tacis; " = []";
1.90 +pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
1.91 +member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
1.92 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
1.93 +nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
1.94 +This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.
1.95 +See TODO.txt
1.96 +*)
1.97 +
1.98 +\<close> ML \<open>
1.99 +"----------- fun factors_from_solution ------------------";
1.100 +"----------- fun factors_from_solution ------------------";
1.101 +"----------- fun factors_from_solution ------------------";
1.102 +val ctxt = Proof_Context.init_global @{theory Isac};
1.103 +val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
1.104 +val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
1.105 +if term2str t' =
1.106 + "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"
1.107 +then () else error "factors_from_solution broken";
1.108 +
1.109 +\<close> ML \<open>
1.110 +"----------- Logic.unvarify_global ----------------------";
1.111 +"----------- Logic.unvarify_global ----------------------";
1.112 +"----------- Logic.unvarify_global ----------------------";
1.113 +val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
1.114 +val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
1.115 +
1.116 +val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;
1.117 +val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
1.118 +
1.119 +val test = HOLogic.mk_binop "Groups.plus_class.plus"
1.120 + (HOLogic.mk_binop "Rings.divide_class.divide" (A_var, denom1),
1.121 + HOLogic.mk_binop "Rings.divide_class.divide" (B_var, denom2));
1.122 +
1.123 +if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
1.124 + else error "HOLogic.mk_binop broken ?";
1.125 +
1.126 +(* Logic.unvarify_global test
1.127 +---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
1.128 +thus we need another fun var2free in termC.sml*)
1.129 +
1.130 +\<close> ML \<open>
1.131 +"----------- = me for met_partial_fraction --------------";
1.132 +"----------- = me for met_partial_fraction --------------";
1.133 +"----------- = me for met_partial_fraction --------------";
1.134 +val fmz =
1.135 + ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
1.136 + "solveFor z", "decomposedFunction p_p"];
1.137 +val (dI',pI',mI') =
1.138 + ("Partial_Fractions",
1.139 + ["partial_fraction", "rational", "simplification"],
1.140 + ["simplification","of_rationals","to_partial_fraction"]);
1.141 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) =
1.142 + CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
1.143 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))")*)
1.144 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
1.145 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "decomposedFunction p_p")*)
1.146 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Partial_Fractions")*)
1.147 + (*05*)
1.148 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["partial_fraction", "rational", "simplification"])*)
1.149 +(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
1.150 +(*[ ], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
1.151 +(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_Rational")*)
1.152 +(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("PolyEq", ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]))*)
1.153 + (*10*)
1.154 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem)*)
1.155 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)
1.156 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
1.157 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions z_i")*)
1.158 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "PolyEq")*)
1.159 +(*[2], Pbl*)(*15*)
1.160 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
1.161 +(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
1.162 +(*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
1.163 +(*[2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', z)"], "d2_polyeq_abcFormula_simplify"))*)
1.164 +(*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify")*)
1.165 + (*20*)
1.166 +(*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Or_to_List)*)
1.167 +(*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions")*)
1.168 +(*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
1.169 +(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - -1 / 4))")*)
1.170 +(*[3], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ansatz_rls")*)
1.171 + (*25*)
1.172 +(*[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)")*)
1.173 +(*[4], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "equival_trans")*)
1.174 +(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)"*)
1.175 +(*[5], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["z = 1 / 2"])*)
1.176 +(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*nxt = Rewrite_Set "norm_Rational"*)
1.177 +(*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac", ["normalise", "polynomial", "univariate", "equation"]*)
1.178 + (*30+1*)
1.179 +(*[7], Pbl*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' [] pt'''; (*nxt = Model_Problem*)
1.180 +(*[7], Pbl*)val (p'v,_,f,nxt'v,_,pt'v) = me nxt'''' p'''' [] pt''''; (*nxt = Add_Given "equality (3 = 3 * AA / 4)")*)
1.181 +(*[7], Pbl*)val (p'v',_,f,nxt'v',_,pt'v') = me nxt'v p'v [] pt'v; (*nxt = Add_Given "solveFor AA")*)
1.182 +(*[7], Pbl*)val (p'v'',_,f,nxt'v'',_,pt'v'') = me nxt'v' p'v' [] pt'v'; (*nxt = Add_Find "solutions AA_i")*)
1.183 +(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac"*)
1.184 + (*35*)
1.185 +(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*)
1.186 +(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
1.187 +(*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
1.188 +(*[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)"))*)
1.189 +(*[7, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in")*)
1.190 + (*40*)
1.191 +(*[7, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify"*)
1.192 +(*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac", ["degree_1", "polynomial", "univariate", "equation"])*)
1.193 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
1.194 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (3 + -3 / 4 * AA = 0)"*)
1.195 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor AA"*)
1.196 + (*45*)
1.197 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.198 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.199 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.200 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.201 +(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.202 + (*50*)
1.203 +(*[7, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.204 +(*[7, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.205 +(*[7, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.206 +(*[7, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.207 +(*[7, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.208 + (*55*)
1.209 +(*[7, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.210 +(*[7, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.211 +(*[7, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.212 +(*[7], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.213 +(*[8], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.214 + (*60*)
1.215 +(*[8], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.216 +(*[9], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.217 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.218 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.219 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.220 + (*65*)
1.221 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.222 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.223 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.224 +(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.225 +(*[10], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.226 + (*70*)
1.227 +(*[10, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.228 +(*[10, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.229 +(*[10, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.230 +(*[10, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.231 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.232 + (*75*)
1.233 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.234 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.235 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.236 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.237 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.238 + (*80*)
1.239 +(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.240 +(*[10, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.241 +(*[10, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.242 +(*[10, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.243 +(*[10, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.244 + (*85*)
1.245 +(*[10, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
1.246 +(*[10, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
1.247 +(*[10, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"*)
1.248 +(*[10, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
1.249 +
1.250 +(*[10], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)"*)
1.251 + (*90*)
1.252 +(*[11], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["AA = 4", "BB = -4"]*)
1.253 +(*[11], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["partial_fraction", "rational", "simplification"]*)
1.254 +(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
1.255 +
1.256 +case nxt of
1.257 + (_, End_Proof') => if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then ()
1.258 + else error "= me .. met_partial_fraction f changed"
1.259 +| _ => error "= me .. met_partial_fraction nxt changed";
1.260 +
1.261 +show_pt_tac pt; (*[
1.262 +([], Frm), Problem
1.263 + (''Partial_Fractions'',
1.264 + ??.\<^const>String.char.Char ''partial_fraction'' ''rational''
1.265 + ''simplification'')
1.266 +. . . . . . . . . . Apply_Method ["simplification","of_rationals","to_partial_fraction"],
1.267 +([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))
1.268 +. . . . . . . . . . Rewrite_Set "norm_Rational",
1.269 +([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)
1.270 +. . . . . . . . . . Subproblem (Isac, ["abcFormula","degree_2","polynomial","univariate","equation"]),
1.271 +([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)
1.272 +. . . . . . . . . . Apply_Method ["PolyEq","solve_d2_polyeq_abc_equation"],
1.273 +([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0
1.274 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', z)], "d2_polyeq_abcFormula_simplify"),
1.275 +([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or>
1.276 +z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)
1.277 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
1.278 +([2,2], Res), z = 1 / 2 \<or> z = -1 / 4
1.279 +. . . . . . . . . . Or_to_List ,
1.280 +([2,3], Res), [z = 1 / 2, z = -1 / 4]
1.281 +. . . . . . . . . . Check_elementwise "Assumptions",
1.282 +([2,4], Res), [z = 1 / 2, z = -1 / 4]
1.283 +. . . . . . . . . . Check_Postcond ["abcFormula","degree_2","polynomial","univariate","equation"],
1.284 +([2], Res), [z = 1 / 2, z = -1 / 4]
1.285 +. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4))",
1.286 +([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))
1.287 +. . . . . . . . . . Rewrite_Set "ansatz_rls",
1.288 +([3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4)
1.289 +. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)",
1.290 +([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)
1.291 +. . . . . . . . . . Rewrite_Set "equival_trans",
1.292 +([4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
1.293 +. . . . . . . . . . Substitute ["z = 1 / 2"],
1.294 +([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)
1.295 +. . . . . . . . . . Rewrite_Set "norm_Rational",
1.296 +([6], Res), 3 = 3 * AA / 4
1.297 +. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
1.298 +([7], Pbl), solve (3 = 3 * AA / 4, AA)
1.299 +. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
1.300 +([7,1], Frm), 3 = 3 * AA / 4
1.301 +. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
1.302 +([7,1], Res), 3 - 3 * AA / 4 = 0
1.303 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "make_ratpoly_in"),
1.304 +([7,2], Res), 3 / 1 + -3 / 4 * AA = 0
1.305 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
1.306 +([7,3], Res), 3 + -3 / 4 * AA = 0
1.307 +. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
1.308 +([7,4], Pbl), solve (3 + -3 / 4 * AA = 0, AA)
1.309 +. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
1.310 +([7,4,1], Frm), 3 + -3 / 4 * AA = 0
1.311 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "d1_polyeq_simplify"),
1.312 +([7,4,1], Res), AA = -1 * 3 / (-3 / 4)
1.313 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
1.314 +([7,4,2], Res), AA = -3 / (-3 / 4)
1.315 +. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
1.316 +([7,4,3], Res), AA = 4
1.317 +. . . . . . . . . . Or_to_List ,
1.318 +([7,4,4], Res), [AA = 4]
1.319 +. . . . . . . . . . Check_elementwise "Assumptions",
1.320 +([7,4,5], Res), [AA = 4]
1.321 +. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
1.322 +([7,4], Res), [AA = 4]
1.323 +. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
1.324 +([7], Res), [AA = 4]
1.325 +. . . . . . . . . . Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)",
1.326 +([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
1.327 +. . . . . . . . . . Substitute ["z = -1 / 4"],
1.328 +([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)
1.329 +. . . . . . . . . . Rewrite_Set "norm_Rational",
1.330 +([9], Res), 3 = -3 * BB / 4
1.331 +. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
1.332 +([10], Pbl), solve (3 = -3 * BB / 4, BB)
1.333 +. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
1.334 +([10,1], Frm), 3 = -3 * BB / 4
1.335 +. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
1.336 +([10,1], Res), 3 - -3 * BB / 4 = 0
1.337 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "make_ratpoly_in"),
1.338 +([10,2], Res), 3 / 1 + 3 / 4 * BB = 0
1.339 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
1.340 +([10,3], Res), 3 + 3 / 4 * BB = 0
1.341 +. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
1.342 +([10,4], Pbl), solve (3 + 3 / 4 * BB = 0, BB)
1.343 +. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
1.344 +([10,4,1], Frm), 3 + 3 / 4 * BB = 0
1.345 +. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "d1_polyeq_simplify"),
1.346 +([10,4,1], Res), BB = -1 * 3 / (3 / 4)
1.347 +. . . . . . . . . . Rewrite_Set "polyeq_simplify",
1.348 +([10,4,2], Res), BB = -3 / (3 / 4)
1.349 +. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
1.350 +([10,4,3], Res), BB = -4
1.351 +. . . . . . . . . . Or_to_List ,
1.352 +([10,4,4], Res), [BB = -4]
1.353 +. . . . . . . . . . Check_elementwise "Assumptions",
1.354 +([10,4,5], Res), [BB = -4]
1.355 +. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
1.356 +([10,4], Res), [BB = -4]
1.357 +. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
1.358 +([10], Res), [BB = -4]
1.359 +. . . . . . . . . . Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)",
1.360 +([11], Frm), AA / (z - 1 / 2) + BB / (z - -1 / 4)
1.361 +. . . . . . . . . . Substitute ["AA = 4","BB = -4"],
1.362 +([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)
1.363 +. . . . . . . . . . Check_Postcond ["partial_fraction","rational","simplification"],
1.364 +([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)]
1.365 +val it = (): unit
1.366 +*)
1.367 +
1.368 +"----------- autoCalculate for met_partial_fraction -----";
1.369 +"----------- autoCalculate for met_partial_fraction -----";
1.370 +"----------- autoCalculate for met_partial_fraction -----";
1.371 +reset_states ();
1.372 + val fmz =
1.373 + ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
1.374 + "solveFor z", "decomposedFunction p_p"];
1.375 + val (dI', pI', mI') =
1.376 + ("Partial_Fractions",
1.377 + ["partial_fraction", "rational", "simplification"],
1.378 + ["simplification","of_rationals","to_partial_fraction"]);
1.379 +CalcTree [(fmz, (dI' ,pI' ,mI'))];
1.380 +Iterator 1;
1.381 +moveActiveRoot 1;
1.382 +autoCalculate 1 CompleteCalc;
1.383 +
1.384 +val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1;
1.385 +if p = ip andalso ip = ([], Res) then ()
1.386 + else error "autoCalculate for met_partial_fraction changed: final pos'";
1.387 +
1.388 +val (Form f, tac, asms) = pt_extract (pt, p);
1.389 +if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
1.390 + terms2str' asms =
1.391 + "[BB = -4,BB is_polyexp,AA is_polyexp,AA = 4," ^
1.392 + "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
1.393 + "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"
1.394 +then case tac of NONE => ()
1.395 + | _ => error "me for met_partial_fraction changed: final result 1"
1.396 +else error "me for met_partial_fraction changed: final result 2"
1.397 +
1.398 +show_pt pt;
1.399 +(*[
1.400 +(([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])),
1.401 +(([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
1.402 +(([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
1.403 +(([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
1.404 +(([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
1.405 +(([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
1.406 +z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
1.407 +(([2,2], Res), z = 1 / 2 | z = -1 / 4),
1.408 +(([2,3], Res), [z = 1 / 2, z = -1 / 4]),
1.409 +(([2,4], Res), [z = 1 / 2, z = -1 / 4]),
1.410 +(([2], Res), [z = 1 / 2, z = -1 / 4]),
1.411 +(([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
1.412 +(([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
1.413 +(([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
1.414 +(([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)),
1.415 +(([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
1.416 +(([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),
1.417 +(([6], Res), 3 = 3 * A / 4),
1.418 +(([7], Pbl), solve (3 = 3 * A / 4, A)),
1.419 +(([7,1], Frm), 3 = 3 * A / 4),
1.420 +(([7,1], Res), 3 - 3 * A / 4 = 0),
1.421 +(([7,2], Res), 3 / 1 + -3 / 4 * A = 0),
1.422 +(([7,3], Res), 3 + -3 / 4 * A = 0),
1.423 +(([7,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),
1.424 +(([7,4,1], Frm), 3 + -3 / 4 * A = 0),
1.425 +(([7,4,1], Res), A = -1 * 3 / (-3 / 4)),
1.426 +(([7,4,2], Res), A = -3 / (-3 / 4)),
1.427 +(([7,4,3], Res), A = 4),
1.428 +(([7,4,4], Res), [A = 4]),
1.429 +(([7,4,5], Res), [A = 4]),
1.430 +(([7,4], Res), [A = 4]),
1.431 +(([7], Res), [A = 4]),
1.432 +(([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
1.433 +(([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),
1.434 +(([9], Res), 3 = -3 * B / 4),
1.435 +(([10], Pbl), solve (3 = -3 * B / 4, B)),
1.436 +(([10,1], Frm), 3 = -3 * B / 4),
1.437 +(([10,1], Res), 3 - -3 * B / 4 = 0),
1.438 +(([10,2], Res), 3 / 1 + 3 / 4 * B = 0),
1.439 +(([10,3], Res), 3 + 3 / 4 * B = 0),
1.440 +(([10,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),
1.441 +(([10,4,1], Frm), 3 + 3 / 4 * B = 0),
1.442 +(([10,4,1], Res), B = -1 * 3 / (3 / 4)),
1.443 +(([10,4,2], Res), B = -3 / (3 / 4)),
1.444 +(([10,4,3], Res), B = -4),
1.445 +(([10,4,4], Res), [B = -4]),
1.446 +(([10,4,5], Res), [B = -4]),
1.447 +(([10,4], Res), [B = -4]),
1.448 +(([10], Res), [B = -4]),
1.449 +(([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),
1.450 +(([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
1.451 +(([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4))] *)
1.452 +
1.453 +\<close> ML \<open>
1.454 +"----------- progr.vers.2: check erls for multiply_ansatz";
1.455 +"----------- progr.vers.2: check erls for multiply_ansatz";
1.456 +"----------- progr.vers.2: check erls for multiply_ansatz";
1.457 +(*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
1.458 +val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";
1.459 +val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;
1.460 +term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
1.461 +
1.462 +val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)
1.463 +term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
1.464 + "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
1.465 +
1.466 +val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
1.467 +if term2str t''' = "3 = (AA + -2 * BB + 4 * z * AA + 4 * z * BB) / 4" then ()
1.468 +else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
1.469 +
1.470 +(*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
1.471 +val xxx = append_rls "multiply_ansatz_erls" norm_Rational
1.472 + [Calc ("HOL.eq",eval_equal "#equal_")];
1.473 +
1.474 +val multiply_ansatz = prep_rls @{theory} (
1.475 + Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
1.476 + erls = xxx,
1.477 + srls = Erls, calc = [], errpatts = [],
1.478 + rules =
1.479 + [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
1.480 + ],
1.481 + scr = EmptyScr}:rls);
1.482 +
1.483 +rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)
1.484 +rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?*)
1.485 +
1.486 +"----------- progr.vers.2: improve program --------------";
1.487 +"----------- progr.vers.2: improve program --------------";
1.488 +"----------- progr.vers.2: improve program --------------";
1.489 +(*WN120318 stopped due to much effort with the test above*)
1.490 + "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
1.491 + " (let f_f = Take f_f; " ^
1.492 + " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
1.493 + " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
1.494 + " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
1.495 + " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
1.496 + " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
1.497 + " (L_L::bool list) = (SubProblem (PolyEqX, " ^
1.498 + " [abcFormula, degree_2, polynomial, univariate, equation], " ^
1.499 + " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
1.500 + " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
1.501 + " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *)
1.502 + " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
1.503 + " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
1.504 +(*this has been tested below by rewrite_set_
1.505 + " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)
1.506 + " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)
1.507 + " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
1.508 +NEXT try to outcomment the very next line..*)
1.509 + " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
1.510 + " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
1.511 + " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
1.512 + " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*)
1.513 + " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
1.514 + " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
1.515 + " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
1.516 + " (sol_a::bool list) = " ^
1.517 + " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
1.518 + " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
1.519 + " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
1.520 + " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
1.521 + " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
1.522 + " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
1.523 + " (sol_b::bool list) = " ^
1.524 + " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
1.525 + " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
1.526 + " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
1.527 + " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
1.528 + " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
1.529 + " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
1.530 + " in pbz)"
1.531 +
1.532 +\<close> ML \<open>
1.533 +\<close> ML \<open>
1.534 +"~~~~~ fun xxx , args:"; val () = ();
1.535 +\<close>
1.536 +
1.537 +section \<open>=============== "Knowledge/biegelinie-3.sml" ===============================\<close>
1.538 +ML \<open>
1.539 +"~~~~~ fun xxx , args:"; val () = ();
1.540 +\<close> ML \<open>
1.541 +(* "Knowledge/biegelinie-3.sml"
1.542 + author: Walther Neuper 190515
1.543 + (c) due to copyright terms
1.544 +*)
1.545 +"table of contents -----------------------------------------------";
1.546 +"-----------------------------------------------------------------";
1.547 +"----------- see biegelinie-1.sml---------------------------------";
1.548 +(* problems with generalised handling of meths which extend the model of a probl
1.549 + since 98298342fb6d: wait for review of whole model-specify phase *)
1.550 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
1.551 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
1.552 +"-----------------------------------------------------------------";
1.553 +"-----------------------------------------------------------------";
1.554 +"-----------------------------------------------------------------";
1.555 +
1.556 +\<close> ML \<open>
1.557 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
1.558 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
1.559 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
1.560 +"----- Bsp 7.70 with me";
1.561 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.562 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
1.563 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
1.564 + "AbleitungBiegelinie dy"];
1.565 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
1.566 + ["IntegrierenUndKonstanteBestimmen2"]);
1.567 +val p = e_pos'; val c = [];
1.568 +(*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*)
1.569 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
1.570 +
1.571 +(*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);
1.572 +(*+*)writeln (oris2str oris); (*[
1.573 +(1, ["1"], #Given,Traegerlaenge, ["L"]),
1.574 +(2, ["1"], #Given,Streckenlast, ["q_0"]),
1.575 +(3, ["1"], #Find,Biegelinie, ["y"]),
1.576 +(4, ["1"], #Relate,Randbedingungen, ["[y 0 = 0]","[y L = 0]","[M_b 0 = 0]","[M_b L = 0]"]),
1.577 +(5, ["1"], #undef,FunktionsVariable, ["x"]),
1.578 +(6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]),
1.579 +(7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*)
1.580 +(*+*)itms2str_ @{context} probl = "[]";
1.581 +(*+*)itms2str_ @{context} meth = "[]";
1.582 +(*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)
1.583 +
1.584 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
1.585 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
1.586 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
1.587 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
1.588 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
1.589 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
1.590 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
1.591 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
1.592 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
1.593 +(*----------- 10 -----------*)
1.594 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
1.595 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy*)
1.596 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
1.597 +
1.598 +(*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)
1.599 +(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*)
1.600 +(*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script"
1.601 +and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type":
1.602 +formal arg. "b" type-matches with several...actual args. "["dy","y"]"
1.603 +selected "dy"
1.604 +with
1.605 +formals: ["l","q","v","b","s","vs","id_abl"]
1.606 +actuals: ["L","q_0","x","[c, c_2, c_3, c_4]","dy","y","[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]"]*)
1.607 +
1.608 +"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.609 + val (pt''', p''') =
1.610 + (*locatetac is here for testing by me; step would suffice in me*)
1.611 + case locatetac tac (pt,p) of
1.612 + ("ok", (_, _, ptp)) => ptp
1.613 +;
1.614 +(*+*)p = ([], Met);
1.615 +(*+*)p''' = ([1], Pbl);
1.616 +(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');
1.617 +(*+*)(*MISSING after locatetac:*)
1.618 +(*+*)writeln (oris2str oris); (*[
1.619 +(1, ["1"], #Given,Streckenlast, ["q_0"]),
1.620 +(2, ["1"], #Given,FunktionsVariable, ["x"]),
1.621 +(3, ["1"], #Find,Funktionen, ["funs'''"])]
1.622 +MISSING:
1.623 + Biegelinie
1.624 + AbleitungBiegelinie
1.625 +*)
1.626 +"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
1.627 + val (mI, m) = Solve.mk_tac'_ tac;
1.628 +val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
1.629 +(*if*) member op = Solve.specsteps mI = false; (*else*)
1.630 +
1.631 +loc_solve_ (mI,m) ptp;
1.632 +"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
1.633 +
1.634 +Solve.solve m (pt, pos);
1.635 +"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tac.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _)))) =
1.636 + (m, (pt, pos));
1.637 +val {srls, ...} = Specify.get_met mI;
1.638 + val itms = case get_obj I pt p of
1.639 + PblObj {meth=itms, ...} => itms
1.640 + | _ => error "solve Apply_Method: uncovered case get_obj"
1.641 + val thy' = get_obj g_domID pt p;
1.642 + val thy = Celem.assoc_thy thy';
1.643 + val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of
1.644 + (is as Selem.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
1.645 + | _ => error "solve Apply_Method: uncovered case init_scrstate"
1.646 + val ini = Lucin.init_form thy sc env;
1.647 + val p = lev_dn p;
1.648 +val NONE = (*case*) ini (*of*);
1.649 + val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
1.650 + val d = Rule.e_rls (*FIXME: get simplifier from domID*);
1.651 +val Steps (_, ss as (_, _, pt', p', c') :: _) =
1.652 +(*case*) Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*);
1.653 +
1.654 +(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
1.655 +(*+*)(*MISSING after locate_gen:*)
1.656 +(*+*)writeln (oris2str oris); (*[
1.657 +(1, ["1"], #Given,Streckenlast, ["q_0"]),
1.658 +(2, ["1"], #Given,FunktionsVariable, ["x"]),
1.659 +(3, ["1"], #Find,Funktionen, ["funs'''"])]
1.660 +MISSING:
1.661 + Biegelinie
1.662 + AbleitungBiegelinie
1.663 +*)
1.664 +"~~~~~ fun locate_gen , args:"; val ((thy', srls), m, (pt, p),
1.665 + (scr as Rule.Prog sc, d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) =
1.666 + ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
1.667 +val thy = Celem.assoc_thy thy';
1.668 +(*if*) l = [] orelse (
1.669 + (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) = true;(*then*)
1.670 +(assy (thy',ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) (body_of sc));
1.671 +
1.672 +"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
1.673 + ((thy',ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (body_of sc));
1.674 +(*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);
1.675 +
1.676 +"~~~~~ fun assy , args:"; val ((thy',ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss), t) =
1.677 + (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
1.678 +val (a', LTool.STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*);
1.679 +(*+*)writeln (term2str stac); (*SubProblem
1.680 + (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
1.681 + [''Biegelinien'', ''ausBelastung''])
1.682 + [REAL q_0, REAL x, REAL_REAL y, REAL_REAL dy] *)
1.683 + val p' =
1.684 + case p_ of Frm => p
1.685 + | Res => lev_on p
1.686 + | _ => error ("assy: call by " ^ pos'2str (p,p_));
1.687 + val Ass (m,v') = (*case*) assod pt d m stac (*of*);
1.688 +
1.689 +"~~~~~ fun assod , args:"; val (pt, _, (Tac.Subproblem' ((domID, pblID, _), _, _, _, _, _)),
1.690 + (stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
1.691 + dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) =
1.692 + (pt, d, m, stac);
1.693 + val dI = HOLogic.dest_string dI';
1.694 + val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
1.695 + val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;
1.696 + val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;
1.697 + val ags = TermC.isalist2list ags';
1.698 +(*if*) mI = ["no_met"] = false; (*else*)
1.699 +(* val (pI, pors, mI) = *)
1.700 + (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
1.701 + handle ERROR "actual args do not match formal args"
1.702 + => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
1.703 +"~~~~~ fun match_ags , args:"; val (thy, pbt, ags) = (thy, ((#ppc o Specify.get_pbt) pI), ags);
1.704 +(*+*)pbt;
1.705 + fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
1.706 + val pbt' = filter_out is_copy_named pbt
1.707 + val cy = filter is_copy_named pbt
1.708 + val oris' = matc thy pbt' ags []
1.709 + val cy' = map (cpy_nam pbt' oris') cy
1.710 + val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
1.711 +
1.712 +(*+*)val c = [];
1.713 +(*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
1.714 +
1.715 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)
1.716 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
1.717 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Funktionen funs'''"*)
1.718 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
1.719 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
1.720 +(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)
1.721 +(*----------- 20 -----------*)
1.722 +(*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
1.723 +(*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)
1.724 +ERROR itms2args: 'Biegelinie' not in itms*)
1.725 +
1.726 +(*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)
1.727 + [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]
1.728 + ^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*)
1.729 +(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');
1.730 +(*+*)if oris2str oris =
1.731 +(*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"
1.732 +(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";
1.733 +writeln (oris2str oris); (*[
1.734 +(1, ["1"], #Given,Streckenlast, ["q_0"]),
1.735 +(2, ["1"], #Given,FunktionsVariable, ["x"]),
1.736 +(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
1.737 +(*+*)if itms2str_ @{context} probl = "[\n(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),\n(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),\n(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]"
1.738 +(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";
1.739 +writeln (itms2str_ @{context} probl); (*[
1.740 +(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
1.741 +(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
1.742 +(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)
1.743 +(*+*)if itms2str_ @{context} meth = "[]"
1.744 +(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";
1.745 +writeln (itms2str_ @{context} meth); (*[]*)
1.746 +
1.747 +"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
1.748 +(* val (pt, p) = *)
1.749 + (*locatetac is here for testing by me; step would suffice in me*)
1.750 + case locatetac tac (pt,p) of
1.751 + ("ok", (_, _, ptp)) => ptp
1.752 +;
1.753 +"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
1.754 + val (mI, m) = Solve.mk_tac'_ tac;
1.755 +val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
1.756 +(*if*) member op = Solve.specsteps mI = true; (*then*)
1.757 +
1.758 +(*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
1.759 +"~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);
1.760 +(* val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt;
1.761 +
1.762 +"~~~~~ fun specify , args:"; val ((Tac.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);
1.763 + val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
1.764 + PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
1.765 + (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
1.766 + val {ppc, pre, prls,...} = Specify.get_met mID
1.767 + val thy = Celem.assoc_thy dI
1.768 + val dI'' = if dI = Rule.e_domID then dI' else dI
1.769 + val pI'' = if pI = Celem.e_pblID then pI' else pI
1.770 +;
1.771 +(*+*)writeln (oris2str oris); (*[
1.772 +(1, ["1"], #Given,Streckenlast, ["q_0"]),
1.773 +(2, ["1"], #Given,FunktionsVariable, ["x"]),
1.774 +(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
1.775 +(*+*)writeln (pats2str' ppc);
1.776 +(*["(#Given, (Streckenlast, q__q))
1.777 +","(#Given, (FunktionsVariable, v_v))
1.778 +","(#Given, (Biegelinie, id_fun))
1.779 +","(#Given, (AbleitungBiegelinie, id_abl))
1.780 +","(#Find, (Funktionen, fun_s))"]*)
1.781 +(*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI));
1.782 +(*["(#Given, (Streckenlast, q_q))
1.783 +","(#Given, (FunktionsVariable, v_v))
1.784 +","(#Find, (Funktionen, funs'''))"]*)
1.785 + val oris = Specify.add_field' thy ppc oris
1.786 + val met = if met = [] then pbl else met
1.787 + val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
1.788 +;
1.789 +(*+*)writeln (itms2str_ @{context} itms); (*[
1.790 +(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
1.791 +(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
1.792 +(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)
1.793 +
1.794 +(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
1.795 +val itms =
1.796 + if mI' = ["Biegelinien", "ausBelastung"]
1.797 + then itms @
1.798 + [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
1.799 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1.800 + (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1.801 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
1.802 + (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
1.803 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1.804 + (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1.805 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
1.806 + else itms
1.807 +(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
1.808 +
1.809 +val itms' = itms @
1.810 + [(4, [1], true, "#Given", Cor ((@{term "Biegelinie"},
1.811 + [@{term "y::real \<Rightarrow> real"}]),
1.812 + (@{term "id_fun::real \<Rightarrow> real"},
1.813 + [@{term "y::real \<Rightarrow> real"}] ))),
1.814 + (5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"},
1.815 + [@{term "dy::real \<Rightarrow> real"}]),
1.816 + (@{term "id_abl::real \<Rightarrow> real"},
1.817 + [@{term "dy::real \<Rightarrow> real"}] )))]
1.818 +val itms'' = itms @
1.819 + [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
1.820 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1.821 + (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1.822 + [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
1.823 + (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
1.824 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
1.825 + (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
1.826 + [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
1.827 +;
1.828 +if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";
1.829 +(*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
1.830 +
1.831 +val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
1.832 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.833 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.834 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.835 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.836 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.837 +(*----------- 30 -----------*)
1.838 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.839 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.840 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.841 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.842 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.843 +(*----------- 40 -----------*)
1.844 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.845 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.846 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.847 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.848 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.849 +(*----------- 50 -----------*)
1.850 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.851 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.852 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.853 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.854 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.855 +(*----------- 60 -----------*)
1.856 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.857 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.858 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.859 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.860 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.861 +(*----------- 70 -----------*)
1.862 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.863 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.864 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.865 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.866 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.867 +(*----------- 80 -----------*)
1.868 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.869 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.870 +\<close> ML \<open>
1.871 +(**)val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.872 +\<close> ML \<open>
1.873 +(*CURRENT*)if p = ([2, 1], Pbl) andalso
1.874 +(*CURRENT*) f = PpcKF (Problem [], {Find = [Incompl "equality"], Given = [Incompl "functionEq", Incompl "substitution"], Relate = [], Where = [], With = []})
1.875 +(*CURRENT*)then
1.876 +(*CURRENT*) case nxt of
1.877 +(*CURRENT*) ("Add_Given", Add_Given "functionEq (hd [])") => ((*here is an error in partial_function*))
1.878 +(*CURRENT*) | _ => error "me biegelinie changed 1"
1.879 +(*CURRENT*)else error "me biegelinie changed 2";
1.880 +\<close> ML \<open>
1.881 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.882 +(*CURRENT*)nxt;(* = ("Tac ", Tac "[error] appl_add: is_known: seek_oridts: input ('substitution (NTH (1 + -4) [])') not found in oris (typed)")*)
1.883 +\<close> ML \<open>
1.884 +(*----- due to "switch from Script to partial_function" 4035ec339062 ?
1.885 + OR ?due to "failed trial to generalise handling of meths which extend the model of a probl " 98298342fb6d
1.886 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.887 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.888 +(*----------- 90 -----------*)
1.889 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.890 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.891 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.892 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.893 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.894 +(*---------- 100 -----------*)
1.895 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.896 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.897 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.898 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.899 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.900 +(*---------- 110 -----------*)
1.901 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.902 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.903 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.904 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.905 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.906 +(*---------- 120 -----------*)
1.907 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.908 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.909 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.910 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.911 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.912 +(*---------- 130 -----------*)
1.913 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.914 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.915 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.916 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.917 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.918 +
1.919 +if p = ([3], Pbl)
1.920 +then
1.921 + case nxt of
1.922 + ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") =>
1.923 + (case f of
1.924 + PpcKF
1.925 + (Problem [],
1.926 + {Find = [Incompl "solution []"], Given =
1.927 + [Correct
1.928 + "equalities\n [0 = -1 * c_4 / -1,\n 0 =\n (-24 * c_4 * EI + -24 * L * c_3 * EI + 12 * L ^^^ 2 * c_2 +\n 4 * L ^^^ 3 * c +\n -1 * L ^^^ 4 * q_0) /\n (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
1.929 + Incompl "solveForVars [c]"],
1.930 + Relate = [], Where = [], With = []}) => ()
1.931 + | _ => error "Bsp.7.70 me changed 1")
1.932 + | _ => error "Bsp.7.70 me changed 2"
1.933 +else error "Bsp.7.70 me changed 3";
1.934 +-----*)
1.935 +(* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
1.936 +
1.937 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
1.938 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
1.939 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
1.940 +(* the error in this test might be independent from introduction of y, dy
1.941 + as arguments in IntegrierenUndKonstanteBestimmen2,
1.942 + rather due to so far untested use of "auto" *)
1.943 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.944 + "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
1.945 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
1.946 + "AbleitungBiegelinie dy"];
1.947 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
1.948 + ["IntegrierenUndKonstanteBestimmen2"]);
1.949 +
1.950 +reset_states ();
1.951 +CalcTree [(fmz, (dI',pI',mI'))];
1.952 +Iterator 1;
1.953 +moveActiveRoot 1;
1.954 +
1.955 +(*[], Met*)autoCalculate 1 CompleteCalcHead;
1.956 +(*[1], Pbl*)autoCalculate 1 (Step 1); (* into SubProblem *)
1.957 +(*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)
1.958 +(*[2], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
1.959 +(*[2], Res*)autoCalculate 1 CompleteSubpbl;
1.960 +(*[3], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
1.961 +(*[3], Met*)autoCalculate 1 CompleteCalcHead;
1.962 +(*[3, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.963 +(*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: generate1: not impl.for Empty_Tac_*)
1.964 +(*[3, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.965 +(*[3, 2], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.966 +(*[3, 3], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.967 +(*[3, 4], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.968 +(*[3, 5], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.969 +(*[3, 6], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.970 +(*[3, 7], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.971 +(*[3, 8], Pbl*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.972 +(*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;
1.973 +(*[3, 8, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.974 +(*[3, 8, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
1.975 +(*(**)autoCalculate 1 (Step 1);
1.976 +*** generate1: not impl.for Empty_Tac_
1.977 +val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)
1.978 +
1.979 +val ((pt,_),_) = get_calc 1;
1.980 +val ip = get_pos 1 1;
1.981 +val (Form f, tac, asms) = pt_extract (pt, ip);
1.982 +
1.983 +if ip = ([2, 1, 1], Frm) andalso
1.984 +term2str f = "hd []"
1.985 +then
1.986 + case tac of
1.987 + SOME Empty_Tac => ()
1.988 + | _ => error "ERROR biegel.7.70 changed 1"
1.989 +else error "ERROR biegel.7.70 changed 2";
1.990 +
1.991 +(*----- this state has been reached shortly after 98298342fb6d:
1.992 +if ip = ([3, 8, 1], Res) andalso
1.993 +term2str f = "[-1 * c_4 / -1 = 0,\n (6 * c_4 * EI + 6 * L * c_3 * EI + -3 * L ^^^ 2 * c_2 + -1 * L ^^^ 3 * c) /\n (6 * EI) =\n L ^^^ 4 * q_0 / (-24 * EI),\n c_2 = 0, c_2 + L * c = L ^^^ 2 * q_0 / 2]"
1.994 +then
1.995 + case tac of
1.996 + SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
1.997 + | _ => error "ERROR biegel.7.70 changed 1"
1.998 +else error "ERROR biegel.7.70 changed 2";
1.999 +*)
1.1000 \<close> ML \<open>
1.1001 \<close> ML \<open>
1.1002 "~~~~~ fun xxx , args:"; val () = ();