1.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Mar 27 11:20:43 2019 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Mar 27 19:14:47 2019 +0100
1.3 @@ -179,7 +179,8 @@
1.4 val thy = @{theory};
1.5 val poly_consts =
1.6 ["Groups.plus_class.plus", "Groups.minus_class.minus",
1.7 - "Rings.divide_class.divide", "Groups.times_class.times"];
1.8 + "Rings.divide_class.divide", "Groups.times_class.times",
1.9 + "Atools.pow"];
1.10 \<close>
1.11 subsubsection \<open>for predicates in specifications (ML)\<close>
1.12 ML \<open>
2.1 --- a/src/Tools/isac/Knowledge/Rational.thy Wed Mar 27 11:20:43 2019 +0100
2.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Wed Mar 27 19:14:47 2019 +0100
2.3 @@ -121,7 +121,9 @@
2.4 subsection \<open>Conversion term <--> poly\<close>
2.5 subsubsection \<open>Convert a term to the internal representation of a multivariate polynomial\<close>
2.6 ML \<open>
2.7 -fun monom_of_term vs (c, es) (Free (id, _)) =
2.8 +fun monom_of_term vs (c, es) (Const (id, _)) =
2.9 + (c, list_update es (find_index (curry op = (strip_thy id)) vs) 1)
2.10 + | monom_of_term vs (c, es) (Free (id, _)) =
2.11 if TermC.is_num' id
2.12 then (id |> TermC.int_of_str_opt |> the |> curry op * c, es) (*several numerals in one monom*)
2.13 else (c, list_update es (find_index (curry op = id) vs) 1)
2.14 @@ -130,9 +132,11 @@
2.15 | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
2.16 let val (c', es') = monom_of_term vs (c, es) m1
2.17 in monom_of_term vs (c', es') m2 end
2.18 - | monom_of_term _ _ t = raise ERROR ("poly malformed with " ^ Rule.term2str t)
2.19 + | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ Rule.term2str t)
2.20
2.21 -fun monoms_of_term vs (t as Free _) =
2.22 +fun monoms_of_term vs (t as Const _) =
2.23 + [monom_of_term vs (1, replicate (length vs) 0) t]
2.24 + | monoms_of_term vs (t as Free _) =
2.25 [monom_of_term vs (1, replicate (length vs) 0) t]
2.26 | monoms_of_term vs (t as Const ("Atools.pow", _) $ _ $ _) =
2.27 [monom_of_term vs (1, replicate (length vs) 0) t]
2.28 @@ -140,7 +144,7 @@
2.29 [monom_of_term vs (1, replicate (length vs) 0) t]
2.30 | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =
2.31 (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
2.32 - | monoms_of_term _ t = raise ERROR ("poly malformed with " ^ Rule.term2str t)
2.33 + | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ Rule.term2str t)
2.34
2.35 (* convert a term to the internal representation of a multivariate polynomial;
2.36 the conversion is quite liberal, see test --- fun poly_of_term ---:
2.37 @@ -370,7 +374,7 @@
2.38 NONE => NONE
2.39 | SOME ((n1, d1), (n2, d2)) =>
2.40 let (* vvvvvvv vvvvvvvvvvv tolerate Free, Const, Var *)
2.41 - val vs = t |> ids2str |> subtract op = poly_consts |> sort string_ord
2.42 + val vs = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord
2.43 in
2.44 case (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) of
2.45 (SOME _, SOME a, SOME _, SOME b) =>
2.46 @@ -602,11 +606,6 @@
2.47
2.48 section \<open>Rulesets for general simplification\<close>
2.49 ML \<open>
2.50 -
2.51 -(*-------------------18.3.03 --> struct <-----------vvv--
2.52 -val add_fractions_p = common_nominator_p; (*FIXXXME:eilig f"ur norm_Rational*)
2.53 - -------------------18.3.03 --> struct <-----------vvv--*)
2.54 -
2.55 (*erls for calculate_Rational; make local with FIXX@ME result:term *term list*)
2.56 val powers_erls = prep_rls'(
2.57 Rule.Rls {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord),
3.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml Wed Mar 27 11:20:43 2019 +0100
3.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml Wed Mar 27 19:14:47 2019 +0100
3.3 @@ -179,19 +179,24 @@
3.4 \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 + \
3.5 \ -1 * q_0 / 24 * L ^^^ 4)]";
3.6 val SOME (t,_) = rewrite_set_ thy true norm_Rational t;
3.7 -if term2str t = "[0 = c_2 + 0 / EI, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (24 * EI)]"
3.8 +if term2str t = (*"[0 = c_2 + 0 / EI,
3.9 + 0 = c_2 + L * c + L ^^^ 4 * q_0 / (24 * EI)]"*)
3.10 + "[0 = c_2, 0 = (24 * EI * c_2 + 24 * EI * L * c + L ^^^ 4 * q_0) / (24 * EI)]"
3.11 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
3.12
3.13 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
3.14 -if term2str t = "[0 = 0 / EI + c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
3.15 +if term2str t = (*"[0 = 0 / EI + c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"*)
3.16 + "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
3.17 then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
3.18
3.19 val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
3.20 -if term2str t = "[c_2 = 0 + -1 * (0 / EI),\n L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
3.21 +if term2str t = (*"[c_2 = 0 + -1 * (0 / EI),\n L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"*)
3.22 + "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
3.23 then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
3.24
3.25 val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
3.26 -if term2str t = "[c_2 = 0 / EI, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
3.27 +if term2str t = (*"[c_2 = 0 / EI, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"*)
3.28 + "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
3.29 then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
3.30
3.31 val xxx = rewrite_set_ thy true order_system t;
3.32 @@ -594,7 +599,7 @@
3.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.34 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.35 if f2str f =
3.36 -"[c_2 = 0 / EI, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
3.37 +"[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
3.38 then () else error "eqsystem.sml me simpl. before SubProblem b";
3.39 case nxt of
3.40 (_, Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
3.41 @@ -630,7 +635,8 @@
3.42 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.43 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
3.44 if f2str f =
3.45 -"[c = (0 / EI + -1 * q_0 * L ^^^ 4 / (24 * EI)) / L, c_2 = 0 / EI]"
3.46 +(*"[c = (0 / EI + -1 * q_0 * L ^^^ 4 / (24 * EI)) / L, c_2 = 0 / EI]"*)
3.47 + "[c = -1 * q_0 * L ^^^ 3 / 24, c_2 = 0]"
3.48 then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
3.49 case nxt of
3.50 (_, End_Proof') => ()
4.1 --- a/test/Tools/isac/Knowledge/rational.sml Wed Mar 27 11:20:43 2019 +0100
4.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Mar 27 19:14:47 2019 +0100
4.3 @@ -18,6 +18,7 @@
4.4 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
4.5 "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
4.6 "-------- rls norm_Rational downto fun add_fraction_p_ -----------------------";
4.7 +"----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
4.8 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
4.9 "-------- rewrite_set_ add_fractions_p from: Mathematik 1 Schalk -------------";
4.10 "-------- integration lev.1 -- lev.5: cancel_p_ & add_fractions_p_ -----------";
4.11 @@ -423,6 +424,95 @@
4.12 val ((a', b'), c) = gcd_poly a b
4.13 *)
4.14
4.15 +"----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
4.16 +"----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
4.17 +"----------- fun check_frac_sum with Free A and Const AA ---------------------------------------";
4.18 +val thy = @{theory Isac(*Partial_Fractions*)}
4.19 +val ctxt = Proof_Context.init_global thy;
4.20 +
4.21 +(*---------- (1) with Free A, B ----------------------------------------------------------------*)
4.22 +val t = (the o (parseNEW ctxt)) "3 = A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";
4.23 + (* required for applying thms in rewriting ^^^^*)
4.24 +(* we get details from here..*)
4.25 +
4.26 +Celem.trace_rewrite := true;
4.27 +val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
4.28 +Celem.trace_rewrite := false;
4.29 +(* trace_rewrite:
4.30 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
4.31 + (* |||||||||||||||||||||||||||||||||||| *)
4.32 +
4.33 +val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 1 GUESS 1 GUESS 1 GUESS 1 *)
4.34 + "A / 2 + A / 4 + (B / 2 + -1 * B / (2::real))";
4.35 +"~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
4.36 +val NONE = (*case*) check_frac_sum t (*of*)
4.37 +
4.38 +(* trace_rewrite:
4.39 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
4.40 + (* |||||||||||||||||||||||||||| *)
4.41 +val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
4.42 + "A / 4 + (B / 2 + -1 * B / (2::real))";
4.43 +"~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
4.44 +val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
4.45 +(*+*)if (term2str n1, term2str d1) = ("A" , "4") andalso
4.46 +(*+*) (term2str n2, term2str d2) = ("B / 2 + -1 * B / 2", "1")
4.47 +(*+*)then () else error "check_frac_sum (A / 4 + (B / 2 + -1 * B / (2::real))) changed";
4.48 +
4.49 + val vs = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord;
4.50 +val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
4.51 + (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
4.52 +
4.53 +"~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);
4.54 +val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
4.55 +(*+*)if xxx = 1 then () else error "monom_of_term changed"
4.56 +
4.57 +"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Free (id, _))) =
4.58 + (vs, (1, replicate (length vs) 0), t);
4.59 +if vs = ["A", "B"] andalso c = 1 andalso id = "A"
4.60 +then () else error "monom_of_term Free changed";
4.61 +
4.62 +(*---------- (2) with Const AA, BB --------------------------------------------------------------*)
4.63 +val t = (the o (parseNEW ctxt)) "3 = AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";
4.64 + (*AA :: real*)
4.65 +(* we get details from here..*)
4.66 +
4.67 +Celem.trace_rewrite := true;
4.68 +val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
4.69 +Celem.trace_rewrite := false;
4.70 +(* trace_rewrite:
4.71 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
4.72 + (* |||||||||||||||||||||||||||||||||||| *)
4.73 +
4.74 +val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
4.75 + "AA / 2 + AA / 4 + (BB / 2 + -1 * BB / 2)";
4.76 +"~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
4.77 +val NONE = (*case*) check_frac_sum t (*of*)
4.78 +
4.79 +(* trace_rewrite:
4.80 +add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
4.81 + (* |||||||||||||||||||||||||||| *)
4.82 +val t = (the o (parseNEW ctxt))(* ||||||||||||||||||||||||| *)
4.83 + "AA / 4 + (BB / 2 + -1 * BB / 2)";
4.84 +"~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
4.85 +val SOME ((n1, d1), (n2, d2)) = (*case*) check_frac_sum t (*of*);
4.86 +(*+*)if (term2str n1, term2str d1) = ("AA" , "4") andalso
4.87 +(*+*) (term2str n2, term2str d2) = ("BB / 2 + -1 * BB / 2", "1")
4.88 +(*+*)then () else error "check_frac_sum (AA / 4 + (BB / 2 + -1 * BB / 2)) changed";
4.89 +
4.90 + val vs = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord;
4.91 +val (SOME [(1, [1, 0])], SOME [(4, [0, 0])], NONE, SOME [(1, [0, 0])]) =
4.92 + (*case*) (poly_of_term vs n1, poly_of_term vs d1, poly_of_term vs n2, poly_of_term vs d2) (*of*);
4.93 +
4.94 +"~~~~~ fun poly_of_term , args:"; val (vs, t) = (vs, n1);
4.95 +val SOME [(1, [xxx, 0])] = SOME [monom_of_term vs (1, replicate (length vs) 0) t];
4.96 +(*+*)if xxx = 1 then () else error "monom_of_term changed"
4.97 +
4.98 +"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (id, _))) =
4.99 + (vs, (1, replicate (length vs) 0), t);
4.100 +if vs = ["AA", "BB"] andalso c = 1 andalso id = "Partial_Fractions.AA"
4.101 +then () else error "monom_of_term Const changed";
4.102 +
4.103 +
4.104 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
4.105 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
4.106 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
5.1 --- a/test/Tools/isac/Test_Some.thy Wed Mar 27 11:20:43 2019 +0100
5.2 +++ b/test/Tools/isac/Test_Some.thy Wed Mar 27 19:14:47 2019 +0100
5.3 @@ -25,9 +25,10 @@
5.4 open TermC; atomt;
5.5 open Celem; e_pbt;
5.6 open Rule; string_of_thm;
5.7 + open Tools; eval_lhs;
5.8 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
5.9 \<close>
5.10 -ML_file "Knowledge/partial_fractions.sml"
5.11 +(*ML_file "Knowledge/partial_fractions.sml"*)
5.12
5.13 section \<open>code for copy & paste ===============================================================\<close>
5.14 ML \<open>
5.15 @@ -66,475 +67,44 @@
5.16 "~~~~~ fun xxx, args:"; val () = ();
5.17 \<close>
5.18
5.19 -section \<open>===================================================================================\<close>
5.20 +section {* ===--- fun check_frac_sum with Free A and Const AA ---=============*}
5.21 ML \<open>
5.22 "~~~~~ fun xxx, args:"; val () = ();
5.23 \<close> ML \<open>
5.24 \<close> ML \<open>
5.25 \<close> ML \<open>
5.26 -"~~~~~ fun xxx, args:"; val () = ();
5.27 -\<close>
5.28 -
5.29 -section \<open>=========================== fun maxthy ===========================================\<close>
5.30 -ML \<open>
5.31 -"~~~~~ fun maxthy , args:"; val () = ();
5.32 \<close> ML \<open>
5.33 \<close> ML \<open>
5.34 \<close> ML \<open>
5.35 -"~~~~~ fun xxx, args:"; val () = ();
5.36 -\<close>
5.37 -
5.38 -section \<open>====================== test with error due to AA =================================\<close>
5.39 -ML \<open>
5.40 -fun common_subthy (thy1, thy2) =
5.41 - if Context.subthy (thy1, thy2) then thy2
5.42 - else if Context.subthy (thy2, thy1) then thy1
5.43 - else @{theory Isac}
5.44 \<close> ML \<open>
5.45 -"----------- = me for met_partial_fraction --------------";
5.46 -"----------- = me for met_partial_fraction --------------";
5.47 -"----------- = me for met_partial_fraction --------------";
5.48 - val fmz =
5.49 - ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
5.50 - "solveFor z", "decomposedFunction p_p"];
5.51 - val (dI',pI',mI') =
5.52 - ("Partial_Fractions",
5.53 - ["partial_fraction", "rational", "simplification"],
5.54 - ["simplification","of_rationals","to_partial_fraction"]);
5.55 - val (p,_,f,nxt,_,pt) =
5.56 - CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem", Model_Problem)*)
5.57 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Add_Given", Add_Given "functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))")*)
5.58 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Add_Given", Add_Given "solveFor z")*)
5.59 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Add_Find", Add_Find "decomposedFunction p_p")*)
5.60 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Theory", Specify_Theory "Partial_Fractions")*)
5.61 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Problem", Specify_Problem ["partial_fraction", "rational", "simplification"])*)
5.62 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Method", Specify_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
5.63 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method", Apply_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
5.64 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_Rational")*)
5.65 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Subproblem", Subproblem ("PolyEq", ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]))*)
5.66 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Model_Problem", Model_Problem)*)
5.67 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Add_Given", Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)
5.68 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Add_Given", Add_Given "solveFor z")*)
5.69 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Add_Find", Add_Find "solutions z_i")*)
5.70 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Theory", Specify_Theory "PolyEq")*)
5.71 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Problem", Specify_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
5.72 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Method", Specify_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
5.73 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
5.74 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set_Inst", Rewrite_Set_Inst (["(''bdv'', z)"], "d2_polyeq_abcFormula_simplify"))*)
5.75 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "polyeq_simplify")*)
5.76 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Or_to_List ", Or_to_List)*)
5.77 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Check_elementwise", Check_elementwise "Assumptions")*)
5.78 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Check_Postcond", Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
5.79 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Take", Take "3 / ((z - 1 / 2) * (z - -1 / 4))")*)
5.80 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "ansatz_rls")*)
5.81 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Take", Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)")*)
5.82 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "equival_trans")*)
5.83 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Take", Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)"*)
5.84 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Substitute", Substitute ["z = 1 / 2"])*)
5.85 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_Rational")*)
5.86 \<close> ML \<open>
5.87 - val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; (*nxt = ("Subproblem", Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]))
5.88 - from refine in step: ^^^^^^^^ *)
5.89 -show_pt pt;(*[ notexists [7], but PolyEq comes with (next) step
5.90 -:
5.91 -(([6], Res), 3 = AA * 3 / 4)]
5.92 -val it = (): unit*)
5.93 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, [], pt);
5.94 - val (pt, p) =
5.95 - case locatetac tac (pt,p) of
5.96 - ("ok", (_, _, ptp)) => ptp
5.97 \<close> ML \<open>
5.98 -(*case*) step p ((pt, Ctree.e_pos'),[]) (*of*);
5.99 -"~~~~~ fun step , args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Ctree.e_pos'),[]));
5.100 \<close> ML \<open>
5.101 -val pIopt = get_pblID (pt,ip);
5.102 \<close> ML \<open>
5.103 -(*if*) ip = ([], Ctree.Res) = false
5.104 \<close> ML \<open>
5.105 -val [] = (*case*) tacis (*of*);
5.106 \<close> ML \<open>
5.107 -val SOME _ = (*case*) pIopt (*of*);
5.108 \<close> ML \<open>
5.109 -(*if*) (member op = [Ctree.Pbl, Ctree.Met] p_
5.110 - andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p))) = false
5.111 \<close> ML \<open>
5.112 -(*val ((tac, _, _)::_, _, _) =*) Solve.nxt_solve_ (pt, ip)
5.113 -(*tac = Subproblem ("PolyEq", ["normalise", "polynomial", "univariate", "equation"]) STEP INTO*)
5.114 \<close> ML \<open>
5.115 -"~~~~~ and nxt_solve_ , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
5.116 \<close> ML \<open>
5.117 -(*if*) Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) = false;
5.118 \<close> ML \<open>
5.119 - val thy' = get_obj g_domID pt (par_pblobj pt p); (* = "Partial_Fractions"*)
5.120 -\<close> ML \<open>
5.121 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
5.122 -\<close> ML \<open>
5.123 - val (srls, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
5.124 -\<close> ML \<open>
5.125 -(* val (tac_, is, (t, _)) =*) Lucin.next_tac (thy', srls) (pt, pos) sc is;
5.126 -(*tac_ = Subproblem' (("PolyEq", ["normalise", ..*);
5.127 -\<close> ML \<open>
5.128 -"~~~~~ fun next_tac , args:"; val (thy, (ptp as (pt, (p, _))), (sc as Rule.Prog prog),
5.129 - (Selem.ScrState (E,l,a,v,s,_), ctxt)) = ((thy', srls), (pt, pos), sc, is);
5.130 -(*thy = ("Partial_Fractions", Rls .. OK*)
5.131 -\<close> ML \<open>
5.132 -(*if*) l = [] = false
5.133 -\<close> ML \<open>
5.134 -(*val Appy (m', scrst as (_,_,_,v,_,_)) =*) (*else*) nstep_up thy ptp sc E l Skip_ a v
5.135 -(*m'= Subproblem' (("PolyEq", ["normalise",...*)
5.136 -\<close> ML \<open>
5.137 -"~~~~~ and nstep_up , args:"; val (thy, ptp, (Rule.Prog sc), E, l, ay, a, v) =
5.138 - (thy, ptp, sc, E, l, Skip_, a, v);
5.139 -\<close> ML \<open>
5.140 -1 < length l = true
5.141 -\<close> ML \<open>
5.142 -val up = drop_last l;
5.143 -\<close> ML \<open>
5.144 -(*Appy (Subproblem' (("PolyEq", ["nor.. =*) (nxt_up thy ptp (Rule.Prog sc) E up ay (go up sc) a v );
5.145 -\<close> ML \<open>
5.146 -"~~~~~ fun nxt_up , args:"; val (thy, ptp, (scr as (Rule.Prog sc)), E, l, ay, (Const ("HOL.Let"(*1*), _) $ _), a, v) =
5.147 - (thy, ptp, (Rule.Prog sc), E, up, ay, (go up sc), a, v);
5.148 -\<close> ML \<open>
5.149 -(*if*) ay = Napp_ = false
5.150 -\<close> ML \<open>
5.151 - (*else*) val up = drop_last l
5.152 -\<close> ML \<open>
5.153 -val Const ("HOL.Let",_) $ _ $ (Abs aa) = (*case*) go up sc (*of*);
5.154 -\<close> ML \<open>
5.155 - val (i, T, body) = aa
5.156 -\<close> ML \<open>
5.157 - val i = TermC.mk_Free (i, T)
5.158 -\<close> ML \<open>
5.159 - val E = LTool.upd_env E (i, v)
5.160 -\<close> ML \<open>
5.161 -(*val Appy lre =*) (*case*) appy thy ptp E (up @ [Celem.R, Celem.D]) body a v (*of*);
5.162 -\<close> ML \<open>
5.163 -"~~~~~ fun appy , args:"; val (thy, ptp, E, l, (Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) =
5.164 - (thy, ptp, E, (up @ [Celem.R, Celem.D]), body, a, v);
5.165 -\<close> ML \<open>
5.166 -(*val ay =*) (*case*) appy thy ptp E (l @ [Celem.L, Celem.R]) e a v (*of*);
5.167 -\<close> ML \<open>
5.168 -"~~~~~ fun appy , args:"; val (((th,sr)), (pt, p), E, l, t, a, v) = (* a leaf has been found *)
5.169 - (thy, ptp, E, (l @ [Celem.L, Celem.R]), e, a, v);
5.170 -\<close> ML \<open>
5.171 -val (a', LTool.STac stac) = (*case*) handle_leaf "next " th sr E a v t (*of*);
5.172 -\<close> ML \<open>
5.173 -(*val (m,m') =*) stac2tac_ pt (Celem.assoc_thy th) stac
5.174 -\<close> ML \<open>
5.175 -"~~~~~ fun stac2tac_ , args:"; val (pt, _, (stac as Const ("Script.SubProblem", _) $
5.176 - (Const ("Product_Type.Pair", _) $ dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) =
5.177 - (pt, (Celem.assoc_thy th), stac);
5.178 -\<close> ML \<open>
5.179 - val dI = HOLogic.dest_string dI'; (* = "Isac"*)
5.180 -\<close> ML \<open>
5.181 - val thy = Celem.maxthy (Celem.assoc_thy dI) (rootthy pt); (* = "Isac",
5.182 - ^^^= "Isac" ^^^ Isac.Partial_Fractions*)
5.183 -\<close> ML \<open>
5.184 - val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;
5.185 - val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;
5.186 - val ags = TermC.isalist2list ags';
5.187 -\<close> ML \<open>
5.188 -(*if*) mI = ["no_met"] = true
5.189 -\<close> ML \<open>
5.190 - val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
5.191 -\<close> ML \<open>
5.192 - val pI' = Specify.refine_ori' pors pI; (* NOT CONCERNED WITH thy *)
5.193 -\<close> ML \<open>
5.194 -pI' = ["normalise", "polynomial", "univariate", "equation"];
5.195 -\<close> ML \<open>
5.196 - val (pI, pors, mI) = (pI', pors (* refinement over models with diff.prec only *),
5.197 - (hd o #met o Specify.get_pbt) pI')
5.198 -\<close> ML \<open>
5.199 - val (fmz_, vals) = Chead.oris2fmz_vals pors;
5.200 - val {cas,ppc,thy,...} = Specify.get_pbt pI
5.201 - val dI = Rule.theory2theory' thy (*.take dI from _refined_ pbl.*)
5.202 - val dI = Rule.theory2theory' (common_subthy (Celem.assoc_thy dI, rootthy pt));
5.203 -(* ^^^^ the theory inserted into Subproblem*)
5.204 -\<close> ML \<open>
5.205 -dI = "PolyEq";
5.206 -(*rootthy pt = Isac.Partial_Fractions*)
5.207 -\<close> ML \<open>
5.208 -if Context.theory_name (common_subthy (Celem.assoc_thy dI, rootthy pt)) = "Isac"
5.209 -then () else error "stac2tac_ finds a wrong theory"
5.210 -\<close> ML \<open>
5.211 -\<close> ML \<open>
5.212 -"~~~~~ fun common_subthy , args:"; val () = (); (*see --- fun common_subthy --*)
5.213 -\<close> ML \<open>
5.214 -\<close> ML \<open>
5.215 -case Tac.Subproblem (dI, pI) of
5.216 - Subproblem ("Isac", ["normalise", "polynomial", "univariate", "equation"]) => ()
5.217 -| _ => error "pbl refinement derives wrong thy from PolyEq .. Partial_Fractions"
5.218 -\<close> ML \<open>
5.219 -\<close> ML \<open> (*^^^^^^ new test code*)
5.220 -\<close> ML \<open>
5.221 -\<close> ML \<open>
5.222 -
5.223 - val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; (*nxt = ("Model_Problem", Model_Problem*)
5.224 -\<close> ML \<open>
5.225 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Add_Given", Add_Given "equality (3 = AA * 3 / 4)")*)
5.226 -\<close> ML \<open>
5.227 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Add_Given", Add_Given "solveFor AA")*)
5.228 -\<close> ML \<open>
5.229 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Add_Find", Add_Find "solutions AA_i")*)
5.230 -\<close> ML \<open>
5.231 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Theory", Specify_Theory "Isac")*)
5.232 -\<close> ML \<open>
5.233 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Problem", Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*)
5.234 -\<close> ML \<open>
5.235 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Method", Specify_Method ["PolyEq", "normalise_poly"])*)
5.236 -\<close> ML \<open>
5.237 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Apply_Method", Apply_Method ["PolyEq", "normalise_poly"])*)
5.238 -\<close> ML \<open>
5.239 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite", Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"))*)
5.240 -\<close> ML \<open>
5.241 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set_Inst", Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in"))*)
5.242 -\<close> ML \<open>
5.243 -f2str f = "3 - 3 * A / 4 = 0"; (*in 333*)
5.244 -f2str f = "3 - AA * 3 / 4 = 0"; (*in REP*)
5.245 -\<close> ML \<open>
5.246 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333: = ("Rewrite_Set", Rewrite_Set "polyeq_simplify")
5.247 -REP: ("Subproblem", Subproblem ("Isac", ["degree_0", "polynomial", "univariate", "equation"]))*)
5.248 -\<close> ML \<open>
5.249 -f2str f = "3 / 1 + -3 / 4 * A = 0"; (*in 333*)
5.250 -f2str f = "3 + -1 * AA * 3 / 4 = 0";(*in REP*)
5.251 -\<close> ML \<open>
5.252 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333 = ("Subproblem", Subproblem ("PolyEq", ["degree_1", "p
5.253 -REP ("Model_Problem", Model_Problem)*)
5.254 -\<close> ML \<open>
5.255 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333
5.256 -REP ("Add_Given", Add_Given "equality (3 + -1 * AA * 3 / 4 = 0)")*)
5.257 -\<close> ML \<open>
5.258 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333
5.259 -REP ("Add_Given", Add_Given "solveFor AA")*)
5.260 -\<close> ML \<open>
5.261 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333
5.262 -REP ("Add_Given", Add_Given "solveFor AA")*)
5.263 -\<close> ML \<open>
5.264 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333
5.265 -REP ("Specify_Theory", Specify_Theory "Isac")*)
5.266 -\<close> ML \<open>
5.267 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333 ("Specify_Theory", Specify_Theory "PolyEq")
5.268 -REP: ("Specify_Problem", Specify_Problem ["degree_0", "polynomial", "univariate", "equation"])*)
5.269 -\<close> ML \<open>
5.270 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333 ("Specify_Problem", Specify_Problem ["degree_1", "polynomial", "univariate", "equation"])
5.271 -REP: ("Specify_Method", Specify_Method ["PolyEq", "solve_d0_polyeq_equation"])*)
5.272 -\<close> ML \<open>
5.273 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333 ("Specify_Method", Specify_Method ["PolyEq", "solve_d1_polyeq_equation"])
5.274 -REP: ("Apply_Method", Apply_Method ["PolyEq", "solve_d0_polyeq_equation"])*)
5.275 -\<close> ML \<open>
5.276 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333 Apply_Method ["PolyEq", "solve_d1_polyeq_equation"])
5.277 -REP: ("Rewrite_Set_Inst", Rewrite_Set_Inst (["(''bdv'', AA)"], "d0_polyeq_simplify"))*)
5.278 -\<close> ML \<open>
5.279 -f2str f; (*in REP = "3 + -1 * AA * 3 / 4 = 0"*)
5.280 -f2str f; (*vvv*)
5.281 -\<close> ML \<open>
5.282 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333 = ("Rewrite_Set_Inst", Rewrite_Set_Inst (["(bdv, A)"], "d1_polyeq_simplify"))
5.283 -REP: = ("Or_to_List ", Or_to_List)*)
5.284 -\<close> ML \<open>
5.285 -f2str f; (*in REP = "False"*)
5.286 -f2str f; (*in 333 = FormKF "3 + -3 / 4 * A = 0"*)
5.287 -\<close> ML \<open>
5.288 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = 333: ("Rewrite_Set", Rewrite_Set "polyeq_simplify")*)
5.289 -\<close> ML \<open>
5.290 -f2str f; (*in REP*)
5.291 -f2str f; (*in 333 = "A = -1 * 3 / (-3 / 4)"*)
5.292 -\<close> ML \<open>
5.293 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.294 -\<close> ML \<open>
5.295 -f2str f; (*in REP*)
5.296 -f2str f; (*in 333 = "A = -3 / (-3 / 4)"*)
5.297 -\<close> ML \<open>
5.298 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.299 -\<close> ML \<open>
5.300 -f2str f; (*in REP*)
5.301 -f2str f; (*in 333 = "A = 4"*)
5.302 -\<close> ML \<open>
5.303 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.304 -\<close> ML \<open>
5.305 -f2str f; (*in REP*)
5.306 -f2str f; (*in 333 = "[A = 4]"*)
5.307 -\<close> ML \<open>
5.308 -show_pt_tac pt(*[
5.309 -([], Frm), Problem
5.310 - (''Partial_Fractions'', [''partial_fraction'', ''rational'',''simplification'')
5.311 -. . . . . . . . . . Apply_Method ["simplification","of_rationals","to_partial_fraction"],
5.312 -([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))
5.313 -. . . . . . . . . . Rewrite_Set "norm_Rational",
5.314 -([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)
5.315 -. . . . . . . . . . Subproblem (Isac, ["abcFormula","degree_2","polynomial","univariate","equation"]),
5.316 -([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)
5.317 -. . . . . . . . . . Apply_Method ["PolyEq","solve_d2_polyeq_abc_equation"],
5.318 -([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0
5.319 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', z)], "d2_polyeq_abcFormula_simplify"),
5.320 -([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or>
5.321 -z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)
5.322 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
5.323 -([2,2], Res), z = 1 / 2 \<or> z = -1 / 4
5.324 -. . . . . . . . . . Or_to_List ,
5.325 -([2,3], Res), [z = 1 / 2, z = -1 / 4]
5.326 -. . . . . . . . . . Check_elementwise "Assumptions",
5.327 -([2,4], Res), [z = 1 / 2, z = -1 / 4]
5.328 -. . . . . . . . . . Check_Postcond ["abcFormula","degree_2","polynomial","univariate","equation"],
5.329 -([2], Res), [z = 1 / 2, z = -1 / 4]
5.330 -. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4))",
5.331 -([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))
5.332 -. . . . . . . . . . Rewrite_Set "ansatz_rls",
5.333 -([3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4)
5.334 -. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)",
5.335 -([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)
5.336 -. . . . . . . . . . Rewrite_Set "equival_trans",
5.337 -([4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
5.338 -. . . . . . . . . . Substitute ["z = 1 / 2"],
5.339 -([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)
5.340 -. . . . . . . . . . Rewrite_Set "norm_Rational",
5.341 -([6], Res), 3 = AA * 3 / 4
5.342 -. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
5.343 -([7], Pbl), solve (3 = AA * 3 / 4, AA)
5.344 -. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
5.345 -([7,1], Frm), 3 = AA * 3 / 4
5.346 -. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
5.347 -([7,1], Res), 3 - AA * 3 / 4 = 0
5.348 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "make_ratpoly_in"),
5.349 -([7,2], Res), 3 + -1 * AA * 3 / 4 = 0
5.350 -. . . . . . . . . . Subproblem (Isac, ["degree_0","polynomial","univariate","equation"]),
5.351 -([7,3], Pbl), solve (3 + -1 * AA * 3 / 4 = 0, AA)
5.352 -. . . . . . . . . . Apply_Method ["PolyEq","solve_d0_polyeq_equation"],
5.353 -([7,3,1], Frm), 3 + -1 * AA * 3 / 4 = 0
5.354 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "d0_polyeq_simplify"),
5.355 -([7,3,1], Res), False
5.356 -. . . . . . . . . . Or_to_List ,
5.357 -([7,3,2], Res), []
5.358 -. . . . . . . . . . Check_Postcond ["degree_0","polynomial","univariate","equation"],
5.359 -([7,3], Res), []
5.360 -. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
5.361 -([7], Res), []
5.362 -. . . . . . . . . . Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)",
5.363 -([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
5.364 -. . . . . . . . . . Empty_Tac]
5.365 -val it = (): unit*)
5.366 -\<close> ML \<open>
5.367 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.368 -\<close> ML \<open>
5.369 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.370 -\<close> ML \<open>
5.371 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.372 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.373 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.374 -\<close> ML \<open>
5.375 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.376 -\<close> ML \<open>
5.377 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Theory", Specify_Theory "Isac")*)
5.378 -\<close> ML \<open>
5.379 -show_pt pt(*[
5.380 -(([], Frm), Problem
5.381 - (''Partial_Fractions'',
5.382 - ??.\<^const>String.char.Char ''partial_fraction'' ''rational''
5.383 - ''simplification'')),
5.384 -(([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
5.385 -(([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
5.386 -(([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
5.387 -(([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
5.388 -(([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or>
5.389 -z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
5.390 -(([2,2], Res), z = 1 / 2 \<or> z = -1 / 4),
5.391 -(([2,3], Res), [z = 1 / 2, z = -1 / 4]),
5.392 -(([2,4], Res), [z = 1 / 2, z = -1 / 4]),
5.393 -(([2], Res), [z = 1 / 2, z = -1 / 4]),
5.394 -(([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
5.395 -(([3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4)),
5.396 -(([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)),
5.397 -(([4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)),
5.398 -(([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)),
5.399 -(([6], Res), 3 = AA * 3 / 4),
5.400 -(([7], Pbl), solve (3 = AA * 3 / 4, AA)),
5.401 -(([7,1], Frm), 3 = AA * 3 / 4),
5.402 -(([7,1], Res), 3 - AA * 3 / 4 = 0),
5.403 -(([7,2], Res), 3 + -1 * AA * 3 / 4 = 0),
5.404 -(([7,3], Pbl), solve (3 + -1 * AA * 3 / 4 = 0, AA)),
5.405 -(([7,3,1], Frm), 3 + -1 * AA * 3 / 4 = 0),
5.406 -(([7,3,1], Res), False),
5.407 -(([7,3,2], Res), []),
5.408 -(([7,3], Res), []),
5.409 -(([7], Res), []),
5.410 -(([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)),
5.411 -(([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)),
5.412 -(([9], Res), 3 = BB * -3 / 4),
5.413 -(([10], Pbl), solve (3 = BB * -3 / 4, BB))]
5.414 -val it = (): unit*)
5.415 -\<close> ML \<open>
5.416 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.417 -
5.418 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.419 -
5.420 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.421 -
5.422 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.423 -
5.424 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.425 -
5.426 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.427 -
5.428 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.429 -
5.430 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.431 -
5.432 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.433 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.434 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.435 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.436 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.437 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.438 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.439 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.440 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.441 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.442 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.443 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.444 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.445 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.446 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.447 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.448 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.449 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.450 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.451 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.452 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.453 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.454 - val (p,_,f,nxt,_,pt) = me nxt p [] pt; (**)
5.455 -
5.456 -show_pt pt;
5.457 -\<close> ML \<open>
5.458 -f2str f
5.459 -\<close> ML \<open>
5.460 -if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then()
5.461 -else error "= me .. met_partial_fraction broken";\<close> ML \<open>
5.462 -\<close> ML \<open>
5.463 -"~~~~~ fun xxx, args:"; val () = ();
5.464 +"~~~~~ fun xxx , args:"; val () = ();
5.465 \<close>
5.466
5.467 section \<open>===================================================================================\<close>
5.468 ML \<open>
5.469 -"~~~~~ fun xxx, args:"; val () = ();
5.470 +"~~~~~ fun xxx , args:"; val () = ();
5.471 \<close> ML \<open>
5.472 \<close> ML \<open>
5.473 \<close> ML \<open>
5.474 -"~~~~~ fun xxx, args:"; val () = ();
5.475 +"~~~~~ fun xxx , args:"; val () = ();
5.476 \<close>
5.477
5.478 -section \<open>===================================================================================\<close>
5.479 -ML \<open>
5.480 -"~~~~~ fun xxx, args:"; val () = ();
5.481 -\<close> ML \<open>
5.482 -\<close> ML \<open>
5.483 -\<close> ML \<open>
5.484 -"~~~~~ fun xxx, args:"; val () = ();
5.485 -\<close>
5.486 +section {* code for copy & paste ===============================================================*}
5.487 +ML {*
5.488 +"~~~~~ fun xxx , args:"; val () = ();
5.489 +"~~~~~ and xxx , args:"; val () = ();
5.490
5.491 -section \<open>code for copy & paste ===============================================================\<close>
5.492 -ML \<open>
5.493 -"~~~~~ fun xxx, args:"; val () = ();
5.494 -"~~~~~ and xxx, args:"; val () = ();
5.495 -
5.496 -"~~~~~ to xxx return val:"; val () = ();
5.497 -\<close>
5.498 +"~~~~~ to return val:"; val () = ();
5.499 +*}
5.500 end