funpack: repair remaining test/../partial_fractions.sml, inverse_z_transform.sml
1.1 --- a/src/Tools/isac/Interpret/calchead.sml Sat Jun 01 11:09:19 2019 +0200
1.2 +++ b/src/Tools/isac/Interpret/calchead.sml Sat Jun 22 13:15:52 2019 +0200
1.3 @@ -54,6 +54,9 @@
1.4 (3) ori list is determined by fmz_ (in root-pbl) or by args of SubProblem;
1.5 it is as complete as possible (this has been different up to now).
1.6 (4) itm list is initialised by pbl-ppc | met-pps and completed (Cor) by stepwise user input.
1.7 +(5) model-pattern of pbl can omit technical items, e.g. boundVariable or functionName,
1.8 + add them to the model-pattern of met and let this input be done automatically;
1.9 + respective items must be in fmz.
1.10 #1# fmz contains items, which are stored in oris of the root(!)-problem.
1.11 This allows to specify methods, which require more input as anticipated
1.12 in writing partial_functions: such an item can be fetched from the root-problem's oris.
1.13 @@ -120,6 +123,7 @@
1.14 val appl_add: Proof.context -> string -> Model.ori list ->
1.15 Model.itm list -> (string * (term * term)) list -> Rule.cterm' -> additm
1.16 val nxt_add: theory -> (int * int list * string * term * term list) list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
1.17 + val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
1.18 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
1.19
1.20 (*----- kept as hints to initial design ideas; NOT in src/, NOT in test ------------------------*)
1.21 @@ -460,7 +464,6 @@
1.22 return _all_ terms already input to this item (e.g. valuesFor a,b) *)
1.23 fun is_known ctxt sel ori t =
1.24 let
1.25 - val _ = tracing ("RM is_known: t=" ^ Rule.term2str t)
1.26 val ots = (distinct o flat o (map #5)) ori
1.27 val oids = ((map (fst o dest_Free)) o distinct o flat o (map TermC.vars)) ots
1.28 val (d, ts) = Model.split_dts t
2.1 --- a/src/Tools/isac/Interpret/ctree-basic.sml Sat Jun 01 11:09:19 2019 +0200
2.2 +++ b/src/Tools/isac/Interpret/ctree-basic.sml Sat Jun 22 13:15:52 2019 +0200
2.3 @@ -262,7 +262,7 @@
2.4 | PblObj of
2.5 {cell : Celem.lrd option, (* unused: meaningful only for some _Prf_Obj *)
2.6 fmz : Selem.fmz, (* from init:FIXME never use this spec;-drop *)
2.7 - origin: (Model.ori list) * (* representation from fmz+pbt
2.8 + origin: (Model.ori list) *(* representation from fmz+pbt+met
2.9 for efficiently adding items in probl, meth *)
2.10 Celem.spec * (* updated by Refine_Tacitly *)
2.11 term, (* headline of calc-head, as calculated initially(!) *)
3.1 --- a/src/Tools/isac/Interpret/script.sml Sat Jun 01 11:09:19 2019 +0200
3.2 +++ b/src/Tools/isac/Interpret/script.sml Sat Jun 22 13:15:52 2019 +0200
3.3 @@ -243,7 +243,7 @@
3.4 (Tac.Check_elementwise (Rule.term_to_string''' thy pred), Tac.Empty_Tac_)
3.5 | stac2tac_ _ _ (Const("Script.Or'_to'_List", _) $ _ ) = (Tac.Or_to_List, Tac.Empty_Tac_)
3.6
3.7 - (*compare "| assod _ (Subproblem'"*)
3.8 + (*compare "| assod _ (Subproblem'" ..TODO: extract common code *)
3.9 | stac2tac_ pt _ (stac as Const ("Script.SubProblem", _) $
3.10 (Const ("Product_Type.Pair", _) $ dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags') =
3.11 let
3.12 @@ -257,6 +257,8 @@
3.13 then
3.14 let
3.15 val pors = (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
3.16 + (* Chead.match_ags : theory -> pat list -> term list -> ori list
3.17 + ^^^ variables ^^^ values *)
3.18 handle ERROR "actual args do not match formal args"
3.19 => (Chead.match_ags_msg pI stac ags(*raise exn*); [])
3.20 val pI' = Specify.refine_ori' pors pI;
3.21 @@ -402,7 +404,7 @@
3.22 SOME (t', _) => Ass (Tac.Substitute' (ro, erls, subte, t, t'), t')
3.23 | NONE => error "assod: Substitute' not applicable to val of Expr")
3.24
3.25 - (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)"*)
3.26 + (*compare "| stac2tac_ thy (Const ("Script.SubProblem",_)" ..TODO: extract common code *)
3.27 | assod pt _ (Tac.Subproblem' ((domID, pblID, _), _, _, _, _, _))
3.28 (stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
3.29 dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags') =
3.30 @@ -1084,14 +1086,22 @@
3.31 local
3.32 val errmsg = "ERROR: found no actual arguments for prog. of "
3.33 fun msg_miss sc metID caller f formals actuals =
3.34 - "ERROR in creating the environment from formal args. of partial_function \"" ^ LTool.id_of_scr sc ^ "\"\n" ^
3.35 + "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (LTool.get_fun_id sc) ^ "\"\n" ^
3.36 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
3.37 "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
3.38 "with:\n" ^
3.39 (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
3.40 (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
3.41 +fun msg_miss_type sc metID f formals actuals =
3.42 + "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (LTool.get_fun_id sc) ^ "\"\n" ^
3.43 + "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
3.44 + "formal arg \"" ^ Rule.term2str f ^ "\" of type \"" ^ Rule.type2str (type_of f) ^
3.45 + "\" doesn't mach an actual arg.\nwith:\n" ^
3.46 + (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
3.47 + (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals ^ "\n" ^
3.48 + " with types: " ^ (strs2str o (map (Rule.type2str o type_of))) actuals
3.49 fun msg_ambiguous sc metID f aas formals actuals =
3.50 - "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ LTool.id_of_scr sc ^ "\"\n" ^
3.51 + "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (LTool.get_fun_id sc) ^ "\"\n" ^
3.52 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
3.53 "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
3.54 "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
3.55 @@ -1099,6 +1109,14 @@
3.56 "with\n" ^
3.57 "formals: " ^ Rule.terms2str formals ^ "\n" ^
3.58 "actuals: " ^ Rule.terms2str actuals
3.59 +fun trace_init metID =
3.60 + if (!trace_script)
3.61 + then tracing("@@@ program " ^ strs2str metID)
3.62 + else ();
3.63 +fun trace_istate env =
3.64 + if (!trace_script)
3.65 + then tracing("@@@ istate " ^ Celem.env2str env)
3.66 + else ();
3.67 in
3.68 fun init_scrstate thy itms metID =
3.69 let
3.70 @@ -1119,11 +1137,12 @@
3.71 val actuals = itms2args thy metID itms
3.72 val _ = if actuals <> [] then () else raise ERROR (errmsg ^ strs2str' metID)
3.73 val (scr, sc) = (case (#scr o Specify.get_met) metID of
3.74 - scr as Rule.Prog sc => (scr, sc) | _ => raise ERROR ("init_scrstate with " ^ Celem.metID2str metID))
3.75 + scr as Rule.Prog sc => (trace_init metID; (scr, sc))
3.76 + | _ => raise ERROR ("init_scrstate with " ^ Celem.metID2str metID))
3.77 val formals = LTool.formal_args sc
3.78 fun assoc_by_type f aa =
3.79 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
3.80 - [] => error (msg_miss sc metID "assoc_by_type" f formals actuals)
3.81 + [] => error (msg_miss_type sc metID f formals actuals)
3.82 | [a] => (f, a)
3.83 | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
3.84 fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
3.85 @@ -1135,6 +1154,7 @@
3.86 let val (f, a) = assoc_by_type f aas
3.87 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
3.88 val env = relate_args [] formals actuals;
3.89 + val _ = trace_istate env;
3.90 val ctxt = Proof_Context.init_global thy |> Stool.declare_constraints' actuals
3.91 val {pre, prls, ...} = Specify.get_met metID;
3.92 val pres = Stool.check_preconds thy prls pre itms |> map snd;
4.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 01 11:09:19 2019 +0200
4.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy Sat Jun 22 13:15:52 2019 +0200
4.3 @@ -1,11 +1,11 @@
4.4 -(* Title: Test_Z_Transform
4.5 +(* Title: Inverse_Z_Transform
4.6 Author: Jan Rocnik
4.7 (c) copyright due to lincense terms.
4.8 *)
4.9
4.10 theory Inverse_Z_Transform imports PolyEq DiffApp Partial_Fractions begin
4.11
4.12 -axiomatization where
4.13 +axiomatization where \<comment> \<open>TODO: new variables on the rhs enforce replacement by substitution\<close>
4.14 rule1: "1 = \<delta>[n]" and
4.15 rule2: "|| z || > 1 ==> z / (z - 1) = u [n]" and
4.16 rule3: "|| z || < 1 ==> z / (z - 1) = -u [-n - 1]" and
4.17 @@ -23,7 +23,7 @@
4.18 subsection\<open>Define the Field Descriptions for the specification\<close>
4.19 consts
4.20 filterExpression :: "bool => una"
4.21 - stepResponse :: "bool => una"
4.22 + stepResponse :: "bool => una" \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6 above\<close>
4.23
4.24 ML \<open>
4.25 val inverse_z = prep_rls'(
4.26 @@ -51,16 +51,10 @@
4.27 (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])),
4.28 (Specify.prep_pbt thy "pbl_SP_Ztrans_inv" [] Celem.e_pblID
4.29 (["Inverse", "Z_Transform", "SignalProcessing"],
4.30 - [("#Given" ,["filterExpression X_eq"]),
4.31 - ("#Find" ,["stepResponse n_eq"])],
4.32 + [("#Given" , ["filterExpression X_eq"]),
4.33 + ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
4.34 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
4.35 - [["SignalProcessing","Z_Transform","Inverse"]])),
4.36 - (Specify.prep_pbt thy "pbl_SP_Ztrans_inv_sub" [] Celem.e_pblID
4.37 - (["Inverse_sub", "Z_Transform", "SignalProcessing"],
4.38 - [("#Given" ,["filterExpression X_eq"]),
4.39 - ("#Find" ,["stepResponse n_eq"])],
4.40 - Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE,
4.41 - [["SignalProcessing","Z_Transform","Inverse_sub"]]))]\<close>
4.42 + [["SignalProcessing","Z_Transform","Inverse"]]))]\<close>
4.43
4.44 subsection \<open>Define Name and Signature for the Method\<close>
4.45 consts
4.46 @@ -82,26 +76,27 @@
4.47 errpats = [], nrls = Rule.e_rls}, @{thm refl})]
4.48 \<close>
4.49
4.50 -(*WARNING: Additional type variable(s) in specification of "inverse_ztransform": 'a *)
4.51 partial_function (tailrec) inverse_ztransform :: "bool \<Rightarrow> real \<Rightarrow> bool"
4.52 where
4.53 -"inverse_ztransform X_eq z = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
4.54 - (let X = Take X_eq;
4.55 - X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
4.56 - X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
4.57 - funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
4.58 - denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close>
4.59 - equ = (denom = (0::real));
4.60 - fun_arg = Take (lhs X');
4.61 - arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close>
4.62 - L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
4.63 - [''Test'',''solve_linear'']) [BOOL equ, REAL z] \<comment> \<open>PROG string\<close>
4.64 +"inverse_ztransform X_eq X_z = \<comment> \<open>(1/z) instead of z ^^^ -1\<close>
4.65 + (let X = Take X_eq;
4.66 + X' = Rewrite ''ruleZY'' False X; \<comment> \<open>z * denominator\<close>
4.67 + X' = (Rewrite_Set ''norm_Rational'' False) X'; \<comment> \<open>simplify\<close>
4.68 + funterm = Take (rhs X'); \<comment> \<open>drop X' z = for equation solving\<close>
4.69 + denom = (Rewrite_Set ''partial_fraction'' False) funterm; \<comment> \<open>get_denominator\<close>
4.70 + equ = (denom = (0::real));
4.71 + fun_arg = Take (lhs X');
4.72 + arg = (Rewrite_Set ''partial_fraction'' False) X'; \<comment> \<open>get_argument TODO\<close>
4.73 + (L_L::bool list) = \<comment> \<open>'bool list' inhibits (?!?):
4.74 + WARNING: Additional type variable(s) in specification of inverse_ztransform: 'a\<close>
4.75 + SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],
4.76 + [''Test'',''solve_linear'']) [BOOL equ, REAL X_z]
4.77 in X) "
4.78 setup \<open>KEStore_Elems.add_mets
4.79 [Specify.prep_met thy "met_SP_Ztrans_inv" [] Celem.e_metID
4.80 (["SignalProcessing", "Z_Transform", "Inverse"],
4.81 - [("#Given" ,["filterExpression (X_eq::bool)"]),
4.82 - ("#Find" ,["stepResponse (n_eq::bool)"])],
4.83 + [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
4.84 + ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
4.85 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
4.86 errpats = [], nrls = Rule.e_rls},
4.87 @{thm inverse_ztransform.simps}
4.88 @@ -142,8 +137,8 @@
4.89 setup \<open>KEStore_Elems.add_mets
4.90 [Specify.prep_met thy "met_SP_Ztrans_inv_sub" [] Celem.e_metID
4.91 (["SignalProcessing", "Z_Transform", "Inverse_sub"],
4.92 - [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
4.93 - ("#Find" ,["stepResponse n_eq"])],
4.94 + [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
4.95 + ("#Find" ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
4.96 {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [],
4.97 srls = Rule.Rls {id="srls_partial_fraction",
4.98 preconds = [], rew_ord = ("termlessI",termlessI),
4.99 @@ -165,7 +160,7 @@
4.100 eval_factors_from_solution "#factors_from_solution")
4.101 ], scr = Rule.EmptyScr},
4.102 prls = Rule.e_rls, crls = Rule.e_rls, errpats = [], nrls = norm_Rational},
4.103 - @{thm simplify.simps}
4.104 + @{thm inverse_ztransform2.simps}
4.105 (*" Script InverseZTransform2 (X_eq::bool) (X_z::real) = "^ (*([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])*)
4.106 " (let X = Take X_eq; "^ (*([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))*)
4.107 " X' = Rewrite ''ruleZY'' False X; "^ (*([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
4.108 @@ -182,6 +177,9 @@
4.109 " n_eq = (Rewrite_Set ''inverse_z'' False) X_zeq "^ (*([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]*)
4.110 " in n_eq) "*))](* X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
4.111 \<close>
4.112 +ML \<open>
4.113 +\<close> ML \<open>
4.114 +\<close>
4.115
4.116 end
4.117
5.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Jun 01 11:09:19 2019 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Sat Jun 22 13:15:52 2019 +0200
5.3 @@ -101,7 +101,7 @@
5.4 ... (1==>2) ansatz
5.5 (2==>3) multiply_*
5.6 (3==>4) norm_Rational
5.7 -TODOs for this version ar in partial_fractions.sml "--- progr.vers.2: "
5.8 +TODOs for this version are in partial_fractions.sml "--- progr.vers.2: "
5.9 \<close>
5.10
5.11 ML \<open>
6.1 --- a/src/Tools/isac/ProgLang/Descript.thy Sat Jun 01 11:09:19 2019 +0200
6.2 +++ b/src/Tools/isac/ProgLang/Descript.thy Sat Jun 22 13:15:52 2019 +0200
6.3 @@ -24,6 +24,7 @@
6.4 functionOf :: "real => una"
6.5 (*functionTerm :: 'a => toreal 28.11.00*)
6.6 functionTerm :: "real => una" (*6.5.03: functionTerm -> functionEq*)
6.7 + functionName :: "real => una"
6.8 interval :: "real set => una"
6.9 maxArgument :: "bool => toreal"
6.10 maximum :: "real => toreal"
7.1 --- a/src/Tools/isac/ProgLang/scrtools.sml Sat Jun 01 11:09:19 2019 +0200
7.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml Sat Jun 22 13:15:52 2019 +0200
7.3 @@ -26,7 +26,6 @@
7.4 val get_calcs: theory -> term -> (Rule.prog_calcID * (Rule.calID * Rule.eval_fn)) list
7.5 val prep_rls: theory -> Rule.rls -> Rule.rls
7.6 val prep_program : thm -> term
7.7 - val id_of_scr : term -> string
7.8 val formal_args : term -> term list
7.9 val body_of : term -> term
7.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
7.11 @@ -53,7 +52,8 @@
7.12 |> Thm.prop_of
7.13 |> HOLogic.dest_Trueprop
7.14 |> Logic.unvarify_global
7.15 - |> TermC.inst_abs)
7.16 + |> TermC.inst_abs
7.17 + |> TermC.numbers_to_string (*for numbers in the program*))
7.18 handle TERM _ => raise TERM ("prep_program", [Thm.prop_of thm])
7.19
7.20 (* distinguish input to Model (deep embedding of terms as Isac's object language) *)
7.21 @@ -101,7 +101,7 @@
7.22 | get_fun_id t = raise TERM ("get_fun_id", [t])
7.23
7.24 (* get the arguments of the script out of the scripts parsetree *)
7.25 -fun formal_args tm = (tm (*TODO move to scrtools.sml*)
7.26 +fun formal_args tm = (tm
7.27 |> HOLogic.dest_eq
7.28 |> fst
7.29 |> strip_comb
7.30 @@ -114,9 +114,6 @@
7.31 |> snd)
7.32 handle TERM _ => raise TERM ("body_of", [tm])
7.33
7.34 -(* get the identifier of the script out of the scripts parsetree *)
7.35 -fun id_of_scr sc = (id_of o fst o strip_comb) sc;
7.36 -
7.37
7.38 (** generate a "type calc" from a script **)
7.39
8.1 --- a/src/Tools/isac/ProgLang/termC.sml Sat Jun 01 11:09:19 2019 +0200
8.2 +++ b/src/Tools/isac/ProgLang/termC.sml Sat Jun 22 13:15:52 2019 +0200
8.3 @@ -66,6 +66,7 @@
8.4 val strip_trueprop: term -> term
8.5
8.6 val num_str: thm -> thm
8.7 + val numbers_to_string: term -> term
8.8 val uminus_to_string: term -> term
8.9 val var2free: term -> term
8.10 val vars: term -> term list
8.11 @@ -82,7 +83,6 @@
8.12 val contains_one_of: thm * (string * typ) list -> bool
8.13 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
8.14 val atomt: term -> unit
8.15 - val numbers_to_string: term -> term
8.16 val typ_a2real: term -> term
8.17 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
8.18 end
9.1 --- a/src/Tools/isac/TODO.thy Sat Jun 01 11:09:19 2019 +0200
9.2 +++ b/src/Tools/isac/TODO.thy Sat Jun 22 13:15:52 2019 +0200
9.3 @@ -20,16 +20,25 @@
9.4 OR ?due to "failed trial to generalise handling of meths
9.5 which extend the model of a probl " 98298342fb6d
9.6 \item
9.7 +\item lucin: test/../partial_fractions: repair different behaviour of
9.8 + --- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ----
9.9 + --- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ----
9.10 +\item lucin: finish output of trace_script with Check_Postcond (useful for SubProblem)
9.11 +\item lucin: extract common code from assod .. stac2tac_
9.12 +\item prep_met: check match between args of partial_function and model-pattern of meth;
9.13 + provide error message.
9.14 \item Diff.thy
9.15 \begin{itemize}
9.16 \item differentiateX --> differentiate after removal of script-constant
9.17 \end{itemize}
9.18 \item Inverse_Z_Transform.thy:
9.19 \begin{itemize}
9.20 - \item thm ruleZY introduces a new variable on the rhs of the rewrite-rule.
9.21 + \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
9.22 + ? replace rewriting with substitution ?!?
9.23 The problem is related to the decision of typing for "d_d" and making bound variables free (while
9.24 - shifting specific handling in equation solving etc. to the metalogic).
9.25 - \item Find "stepResponse (x[n::real]::bool)" not reflected in met ?!
9.26 + shifting specific handling in equation solving etc. to the meta-logic).
9.27 + \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
9.28 + rewrite-rules; see \ref{new-var-rhs}.
9.29 \item Reconsider whole problem:
9.30 input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
9.31 \end{itemize}
10.1 --- a/src/Tools/isac/calcelems.sml Sat Jun 01 11:09:19 2019 +0200
10.2 +++ b/src/Tools/isac/calcelems.sml Sat Jun 22 13:15:52 2019 +0200
10.3 @@ -614,7 +614,7 @@
10.4 copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
10.5 see ME/calchead.sml 'fun is_copy_named'. *)
10.6 pre : term list, (* preconditions in where *)
10.7 - scr : Rule.scr (* prep_met gets progam or string "empty_script" *)
10.8 + scr : Rule.scr (* progam, empty as @{thm refl} or Rfuns *)
10.9 };
10.10 val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'",
10.11 erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls,
11.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Jun 01 11:09:19 2019 +0200
11.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Sat Jun 22 13:15:52 2019 +0200
11.3 @@ -894,7 +894,7 @@
11.4 setup \<open>KEStore_Elems.add_pbts
11.5 [prep_pbt thy "pbl_SP_Ztrans_inv" [] e_pblID
11.6 (["Inverse", "Z_Transform", "SignalProcessing"],
11.7 - [("#Given", ["filterExpression X_eq"]),
11.8 + [("#Given" ,["filterExpression X_eq"]),
11.9 ("#Find", ["stepResponse n_eq"])],
11.10 append_rls "e_rls" e_rls [(*for preds in where_*)],
11.11 NONE,
11.12 @@ -940,7 +940,8 @@
11.13 setup \<open>KEStore_Elems.add_mets
11.14 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
11.15 (["SignalProcessing", "Z_Transform", "Inverse"],
11.16 - [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
11.17 + [("#Given" ,["filterExpression X_eq", "boundVariable X_z"]),
11.18 + ("#Find", ["stepResponse n_eq"])],
11.19 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
11.20 errpats = [], nrls = e_rls},
11.21 "empty_script")]
11.22 @@ -953,10 +954,11 @@
11.23 setup \<open>KEStore_Elems.add_mets
11.24 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
11.25 (["SignalProcessing", "Z_Transform", "Inverse"],
11.26 - [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
11.27 + [("#Given" , ["filterExpression X_eq", "boundVariable X_z"]),
11.28 + ("#Find", ["stepResponse n_eq"])],
11.29 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = e_rls, prls = e_rls, crls = e_rls,
11.30 errpats = [], nrls = e_rls},
11.31 - "Script InverseZTransform (Xeq::bool) =" ^
11.32 + "Script InverseZTransform (Xeq::bool) =" ^ (*TODO boundVariable X_z*)
11.33 " (let X = Take Xeq;" ^
11.34 " X = Rewrite ruleZY False X" ^
11.35 " in X)")]
11.36 @@ -1127,7 +1129,8 @@
11.37 setup \<open>KEStore_Elems.add_mets
11.38 [prep_met thy "met_SP_Ztrans_inv" [] e_metID
11.39 (["SignalProcessing", "Z_Transform", "Inverse"],
11.40 - [("#Given" ,["filterExpression X_eq"]), ("#Find" ,["stepResponse n_eq"])],
11.41 + [("#Given" , ["filterExpression X_eq"]), (*TODO boundVariable X_z*)
11.42 + ("#Find", ["stepResponse n_eq"])],
11.43 {rew_ord'="tless_true", rls'= e_rls, calc = [], srls = srls, prls = e_rls, crls = e_rls,
11.44 errpats = [], nrls = e_rls},
11.45 "Script InverseZTransform (X_eq::bool) = "^
12.1 --- a/test/Tools/isac/Interpret/mathengine.sml Sat Jun 01 11:09:19 2019 +0200
12.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Sat Jun 22 13:15:52 2019 +0200
12.3 @@ -527,7 +527,7 @@
12.4 val SOME t = parseNEW ctxt "filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))";
12.5 val SOME t = parseNEW ctxt "stepResponse (x[n::real]::bool)";
12.6
12.7 -val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
12.8 +val fmz = ["filterExpression (X = 3 / (z - 1/4 + -1/8 * (1/(z::real))))", "boundVariable z",
12.9 "stepResponse (x[n::real]::bool)"];
12.10 val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
12.11 ["SignalProcessing","Z_Transform","Inverse"]);
13.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Sat Jun 01 11:09:19 2019 +0200
13.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Sat Jun 22 13:15:52 2019 +0200
13.3 @@ -8,9 +8,7 @@
13.4 "-----------------------------------------------------------------";
13.5 "----------- met/pbl [SignalProcessing,Z_Transform,inverse] known ";
13.6 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
13.7 -"----------- test [SignalProcessing,Z_Transform,Inverse_sub] autoc";
13.8 -"----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
13.9 -"----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
13.10 +"----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
13.11 "-----------------------------------------------------------------";
13.12 "-----------------------------------------------------------------";
13.13
13.14 @@ -23,11 +21,10 @@
13.15 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
13.16 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
13.17 "----------- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";
13.18 - val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
13.19 - "boundVariable X_z" (*special case: formal arg. = actual arg.*),
13.20 - "stepResponse (x[n::real]::bool)"];
13.21 -(*[], Frm*)val (dI, pI, mI) = ("Isac", ["Inverse_sub", "Z_Transform", "SignalProcessing"],
13.22 - ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
13.23 +val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
13.24 + "functionName X_z", "stepResponse (x[n::real]::bool)"];
13.25 +val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
13.26 + ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
13.27 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))]; (*Model_Problem*)
13.28 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Given "filterExpression (X z = ...*)
13.29 (*[], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Add_Find "stepResponse (x [n])")*)
13.30 @@ -51,7 +48,7 @@
13.31 if p = ([2, 1], Frm) andalso f2str fb = "3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))"
13.32 then () else error "Z_Transform,inverse_sub] me 1"; (*Rewrite_Set "norm_Rational"*)
13.33
13.34 -(*[2, 1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["abcFormula", "degree_2", "po...a*)
13.35 +(*[2,1], Res*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (*Subproblem ("Isac", ["abcFormula", "degree_2", "po...a*)
13.36 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
13.37 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
13.38 (*[2,2], Pbl*)val (p,_,fb,nxt,_,pt) = me nxt p [] pt; (**)
13.39 @@ -176,143 +173,15 @@
13.40 if p = ([], Res) andalso
13.41 f2str fb = "X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]"
13.42 then () else error "[SignalProcessing,Z_Transform,Inverse_sub] changed 1"
13.43 -| _ => error "[SignalProcessing,Z_Transform,Inverse_sub] changed 2"
13.44 +| _ => error "[SignalProcessing,Z_Transform,Inverse_sub] changed 2";
13.45
13.46 -(* show_pt_tac pt; [
13.47 -([], Frm), Problem
13.48 - (''Isac'',
13.49 - String.char.Char ''Inverse'' ''Z_Transform''
13.50 - ''SignalProcessing'')
13.51 -. . . . . . . . . . Apply_Method ["SignalProcessing","Z_Transform","Inverse_sub"],
13.52 -([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))
13.53 -. . . . . . . . . . Rewrite ("ruleZY", "(?X ?z = ?a / ?b) = (?X' ?z = ?a / (?z * ?b))"),
13.54 -([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))
13.55 -. . . . . . . . . . Subproblem (Isac, ["partial_fraction","rational","simplification"]),
13.56 -([2], Pbl), Problem
13.57 - (''Isac'',
13.58 - String.char.Char ''partial_fraction'' ''rational''
13.59 - ''simplification'')
13.60 -. . . . . . . . . . Apply_Method ["simplification","of_rationals","to_partial_fraction"],
13.61 -([2,1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))
13.62 -. . . . . . . . . . Rewrite_Set "norm_Rational",
13.63 -([2,1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)
13.64 -. . . . . . . . . . Subproblem (Isac, ["abcFormula","degree_2","polynomial","univariate","equation"]),
13.65 -([2,2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)
13.66 -. . . . . . . . . . Apply_Method ["PolyEq","solve_d2_polyeq_abc_equation"],
13.67 -([2,2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0
13.68 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', z)], "d2_polyeq_abcFormula_simplify"),
13.69 -([2,2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or>
13.70 -z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)
13.71 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
13.72 -([2,2,2], Res), z = 1 / 2 \<or> z = -1 / 4
13.73 -. . . . . . . . . . Or_to_List ,
13.74 -([2,2,3], Res), [z = 1 / 2, z = -1 / 4]
13.75 -. . . . . . . . . . Check_elementwise "Assumptions",
13.76 -([2,2,4], Res), [z = 1 / 2, z = -1 / 4]
13.77 -. . . . . . . . . . Check_Postcond ["abcFormula","degree_2","polynomial","univariate","equation"],
13.78 -([2,2], Res), [z = 1 / 2, z = -1 / 4]
13.79 -. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4))",
13.80 -([2,3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))
13.81 -. . . . . . . . . . Rewrite_Set "ansatz_rls",
13.82 -([2,3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4)
13.83 -. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)",
13.84 -([2,4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)
13.85 -. . . . . . . . . . Rewrite_Set "equival_trans",
13.86 -([2,4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
13.87 -. . . . . . . . . . Substitute ["z = 1 / 2"],
13.88
13.89 -(*([2,5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2) ..from dropped drop_questionmarks*)
13.90 -
13.91 -([2,5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)
13.92 -. . . . . . . . . . Rewrite_Set "norm_Rational",
13.93 -([2,6], Res), 3 = 3 * AA / 4
13.94 -. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
13.95 -([2,7], Pbl), solve (3 = 3 * AA / 4, AA)
13.96 -. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
13.97 -([2,7,1], Frm), 3 = 3 * AA / 4
13.98 -. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
13.99 -([2,7,1], Res), 3 - 3 * AA / 4 = 0
13.100 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "make_ratpoly_in"),
13.101 -([2,7,2], Res), 3 / 1 + -3 / 4 * AA = 0
13.102 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
13.103 -([2,7,3], Res), 3 + -3 / 4 * AA = 0
13.104 -. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
13.105 -([2,7,4], Pbl), solve (3 + -3 / 4 * AA = 0, AA)
13.106 -. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
13.107 -([2,7,4,1], Frm), 3 + -3 / 4 * AA = 0
13.108 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "d1_polyeq_simplify"),
13.109 -([2,7,4,1], Res), AA = -1 * 3 / (-3 / 4)
13.110 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
13.111 -([2,7,4,2], Res), AA = -3 / (-3 / 4)
13.112 -. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
13.113 -([2,7,4,3], Res), AA = 4
13.114 -. . . . . . . . . . Or_to_List ,
13.115 -([2,7,4,4], Res), [AA = 4]
13.116 -. . . . . . . . . . Check_elementwise "Assumptions",
13.117 -([2,7,4,5], Res), [AA = 4]
13.118 -. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
13.119 -([2,7,4], Res), [AA = 4]
13.120 -. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
13.121 -([2,7], Res), [AA = 4]
13.122 -. . . . . . . . . . Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)",
13.123 -([2,8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
13.124 -. . . . . . . . . . Substitute ["z = -1 / 4"],
13.125 -([2,8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)
13.126 -. . . . . . . . . . Rewrite_Set "norm_Rational",
13.127 -([2,9], Res), 3 = -3 * BB / 4
13.128 -. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
13.129 -([2,10], Pbl), solve (3 = -3 * BB / 4, BB)
13.130 -. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
13.131 -([2,10,1], Frm), 3 = -3 * BB / 4
13.132 -. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
13.133 -([2,10,1], Res), 3 - -3 * BB / 4 = 0
13.134 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "make_ratpoly_in"),
13.135 -([2,10,2], Res), 3 / 1 + 3 / 4 * BB = 0
13.136 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
13.137 -([2,10,3], Res), 3 + 3 / 4 * BB = 0
13.138 -. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
13.139 -([2,10,4], Pbl), solve (3 + 3 / 4 * BB = 0, BB)
13.140 -. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
13.141 -([2,10,4,1], Frm), 3 + 3 / 4 * BB = 0
13.142 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "d1_polyeq_simplify"),
13.143 -([2,10,4,1], Res), BB = -1 * 3 / (3 / 4)
13.144 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
13.145 -([2,10,4,2], Res), BB = -3 / (3 / 4)
13.146 -. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
13.147 -([2,10,4,3], Res), BB = -4
13.148 -. . . . . . . . . . Or_to_List ,
13.149 -([2,10,4,4], Res), [BB = -4]
13.150 -. . . . . . . . . . Check_elementwise "Assumptions",
13.151 -([2,10,4,5], Res), [BB = -4]
13.152 -. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
13.153 -([2,10,4], Res), [BB = -4]
13.154 -. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
13.155 -([2,10], Res), [BB = -4]
13.156 -. . . . . . . . . . Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)",
13.157 -([2,11], Frm), AA / (z - 1 / 2) + BB / (z - -1 / 4)
13.158 -. . . . . . . . . . Substitute ["AA = 4","BB = -4"],
13.159 -([2,11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)
13.160 -. . . . . . . . . . Check_Postcond ["partial_fraction","rational","simplification"],
13.161 -([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)
13.162 -. . . . . . . . . . Take "?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)",
13.163 -([3], Frm), ?X' z = 4 / (z - 1 / 2) + -4 / (z - -1 / 4)
13.164 -. . . . . . . . . . Rewrite ("ruleYZ", "?a / ?b + ?c / ?d = ?a * (?z / ?b) + ?c * (?z / ?d)"),
13.165 -([3], Res), ?X' z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))
13.166 -. . . . . . . . . . Take "X_z = 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))",
13.167 -([4], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))
13.168 -. . . . . . . . . . Rewrite_Set "inverse_z",
13.169 -([4], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n],
13.170 -. . . . . . . . . . Check_Postcond ["Inverse", "Z_Transform", "SignalProcessing"],
13.171 -([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n])]
13.172 -val it = (): unit*)
13.173 -
13.174 -"----------- test [SignalProcessing,Z_Transform,Inverse_sub] autoc";
13.175 -"----------- test [SignalProcessing,Z_Transform,Inverse_sub] autoc";
13.176 -"----------- test [SignalProcessing,Z_Transform,Inverse_sub] autoc";
13.177 +"----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
13.178 +"----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
13.179 +"----------- test [SignalProcessing,Z_Transform,Inverse_sub] auto-";
13.180 reset_states ();
13.181 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
13.182 - "boundVariable X_z" (*special case: formal arg. = actual arg.*),
13.183 - "stepResponse (x[n::real]::bool)"];
13.184 + "functionName X_z", "stepResponse (x[n::real]::bool)"];
13.185 val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
13.186 ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
13.187 CalcTree [(fmz, (dI,pI,mI))];
13.188 @@ -325,142 +194,3 @@
13.189 if term2str f = "X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]"
13.190 andalso p = ([], Res) then ()
13.191 else error "inv Z, exp 1 autoCalculate changed";
13.192 -
13.193 -"----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
13.194 -"----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
13.195 -"----------- test [SignalProcessing,Z_Transform,inverse] autocalc-";
13.196 -reset_states ();
13.197 -val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
13.198 - "boundVariable X_z" (*special case: formal arg. = actual arg.*),
13.199 - "stepResponse (x[n::real]::bool)"];
13.200 -val (dI, pI, mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
13.201 - ["SignalProcessing", "Z_Transform", "Inverse_sub"]);
13.202 -CalcTree [(fmz, (dI,pI,mI))];
13.203 -Iterator 1;
13.204 -moveActiveRoot 1;
13.205 -autoCalculate 1 CompleteCalc;
13.206 -
13.207 -val ((pt,_),_) = get_calc 1; val p = get_pos 1 1;
13.208 -val (Form f, tac, asms) = pt_extract (pt, p);
13.209 -if term2str f = "X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]"
13.210 - andalso p = ([], Res) then ()
13.211 - else error "inv Z, exp 1 autoCalculate changed";
13.212 -
13.213 -(*show_pt pt;[
13.214 -(([], Frm), Problem (Isac, [Inverse, Z_Transform, SignalProcessing])),
13.215 -(([1], Frm), X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))),
13.216 -(([1], Res), ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
13.217 -(([2], Res), ?X' z = 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
13.218 -(([3], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
13.219 -(([3,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
13.220 -(([3,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
13.221 -z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
13.222 -(([3,2], Res), z = 1 / 2 | z = -1 / 4),
13.223 -(([3,3], Res), [z = 1 / 2, z = -1 / 4]),
13.224 -(([3,4], Res), [z = 1 / 2, z = -1 / 4]),
13.225 -(([3], Res), [z = 1 / 2, z = -1 / 4]),
13.226 -(([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
13.227 -(([4], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
13.228 -(([5], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
13.229 -(([5], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)),
13.230 -(([6], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
13.231 -(([6], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),
13.232 -(([7], Res), 3 = 3 * A / 4),
13.233 -(([8], Pbl), solve (3 = 3 * A / 4, A)),
13.234 -(([8,1], Frm), 3 = 3 * A / 4),
13.235 -(([8,1], Res), 3 - 3 * A / 4 = 0),
13.236 -(([8,2], Res), 3 / 1 + -3 / 4 * A = 0),
13.237 -(([8,3], Res), 3 + -3 / 4 * A = 0),
13.238 -(([8,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),
13.239 -(([8,4,1], Frm), 3 + -3 / 4 * A = 0),
13.240 -(([8,4,1], Res), A = -1 * 3 / (-3 / 4)),
13.241 -(([8,4,2], Res), A = -3 / (-3 / 4)),
13.242 -(([8,4,3], Res), A = 4),
13.243 -(([8,4,4], Res), [A = 4]),
13.244 -(([8,4,5], Res), [A = 4]),
13.245 -(([8,4], Res), [A = 4]),
13.246 -(([8], Res), [A = 4]),
13.247 -(([9], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
13.248 -(([9], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),
13.249 -(([10], Res), 3 = -3 * B / 4),
13.250 -(([11], Pbl), solve (3 = -3 * B / 4, B)),
13.251 -(([11,1], Frm), 3 = -3 * B / 4),
13.252 -(([11,1], Res), 3 - -3 * B / 4 = 0),
13.253 -(([11,2], Res), 3 / 1 + 3 / 4 * B = 0),
13.254 -(([11,3], Res), 3 + 3 / 4 * B = 0),
13.255 -(([11,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),
13.256 -(([11,4,1], Frm), 3 + 3 / 4 * B = 0),
13.257 -(([11,4,1], Res), B = -1 * 3 / (3 / 4)),
13.258 -(([11,4,2], Res), B = -3 / (3 / 4)),
13.259 -(([11,4,3], Res), B = -4),
13.260 -(([11,4,4], Res), [B = -4]),
13.261 -(([11,4,5], Res), [B = -4]),
13.262 -(([11,4], Res), [B = -4]),
13.263 -(([11], Res), [B = -4]),
13.264 -(([12], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),
13.265 -(([12], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
13.266 -(([13], Res), 4 * (?z / (z - 1 / 2)) + -4 * (?z / (z - -1 / 4))),
13.267 -(([14], Frm), X_z = 4 * (z / (z - 1 / 2)) + -4 * (z / (z - -1 / 4))),
13.268 -(([14], Res), X_z = 4 * (1 / 2) ^^^ ?n * ?u [?n] + -4 * (-1 / 4) ^^^ ?n * ?u [?n]),
13.269 -(([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n])] *)
13.270 -
13.271 -"----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
13.272 -"----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
13.273 -"----------- [Signal..,inverse] (Step 1): <ISA> rhs (?X' z = ... -";
13.274 -(*====================================================================
13.275 -(* Below are _all_ steps from BridgeLog; _superfluous_ ones and output are text.
13.276 - REASON FOR THE ERROR: Inverse_Z_Transform.thy did not contain final version of method.
13.277 -
13.278 -[[to sml: theory TTY_Communication imports Isac.Isac begin
13.279 -ML {* reset_states (); *}
13.280 -*)
13.281 -ML {* CalcTree [(["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
13.282 - "stepResponse (x[n::real]::bool)"],("Isac",["Inverse","Z_Transform","SignalProcessing"],
13.283 - ["SignalProcessing","Z_Transform","Inverse"]))]; *}
13.284 -ML {* Iterator 1; *}
13.285 -ML {* moveActiveRoot 1; *}
13.286 -ML {* getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; *}
13.287 -text {* getFormulaeFromTo 1 ([],Pbl) ([],Pbl) 0 false; *}
13.288 -ML {* "##### 1.<NEXT> ############################################" *}
13.289 -ML {* (*completeCalcHead*)autoCalculate 1 CompleteCalcHead; *}
13.290 -text {* (*completeCalcHead*)getActiveFormula 1 ; *}
13.291 -text {* (*completeCalcHead*)refFormula 1 ([],Met); *}
13.292 -text {* refFormula 1 ([],Pbl); *}
13.293 -text {* fetchProposedTactic 1; *}
13.294 -ML {* autoCalculate 1 (Step 1); *}
13.295 -text {* getFormulaeFromTo 1 ([],Met) ([1],Frm) 0 false; *}
13.296 -text {* getFormulaeFromTo 1 ([],Met) ([1],Frm) 0 false; *}
13.297 -ML {* refFormula 1 ([1],Frm); *}
13.298 -text {*<ISA> ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) </ISA>*}
13.299 -text {* refFormula 1 ([1],Frm); *}
13.300 -ML {* "##### 2.<NEXT> ############################################" *}
13.301 -text {* refFormula 1 ([1],Frm); *}
13.302 -ML {* autoCalculate 1 (Step 1); *}
13.303 -text {* getFormulaeFromTo 1 ([1],Frm) ([1],Res) 0 false; *}
13.304 -text {* getFormulaeFromTo 1 ([1],Frm) ([1],Res) 0 false; *}
13.305 -ML {* refFormula 1 ([1],Res); *}
13.306 -text {*<ISA> ?X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))) </ISA>*}
13.307 -ML {* refFormula 1 ([1],Res); *}
13.308 -ML {* "##### 3.<NEXT> ############################################" *}
13.309 -text {* refFormula 1 ([1],Res); *}
13.310 -ML {* autoCalculate 1 (Step 1); *}
13.311 -text {* getFormulaeFromTo 1 ([1],Res) ([2],Res) 0 false; *}
13.312 -text {* getFormulaeFromTo 1 ([1],Res) ([2],Res) 0 false; *}
13.313 -ML {* refFormula 1 ([2],Res); *}
13.314 -text {*<ISA> rhs (?X' z = 24 / (-1 + -2 * z + 8 * z ^ 2)) </ISA>*}
13.315 -text {* refFormula 1 ([2],Res); *}
13.316 -ML {* "##### 4.<NEXT> ############################################" *}
13.317 -text {* refFormula 1 ([2],Res); *}
13.318 -ML {* autoCalculate 1 (Step 1); *}
13.319 -text {* getFormulaeFromTo 1 ([2],Res) ([3],Frm) 0 false; *}
13.320 -text {* getFormulaeFromTo 1 ([2],Res) ([3],Frm) 0 false; *}
13.321 -ML {* refFormula 1 ([3],Frm); *}
13.322 -text {*<ISA> rhs (?X' z = 24 / (-1 + -2 * z + 8 * z ^ 2)) </ISA>*}
13.323 -text {* refFormula 1 ([3],Frm); *}
13.324 -ML {* "##### 5.<NEXT> ############################################" *}
13.325 -text {* refFormula 1 ([3],Frm); *}
13.326 -ML {* autoCalculate 1 (Step 1); *}
13.327 -text {*<CALCMESSAGE> helpless </CALCMESSAGE>*}
13.328 -====================================================================*)
13.329 -
13.330 -
14.1 --- a/test/Tools/isac/Knowledge/biegelinie-3.sml Sat Jun 01 11:09:19 2019 +0200
14.2 +++ b/test/Tools/isac/Knowledge/biegelinie-3.sml Sat Jun 22 13:15:52 2019 +0200
14.3 @@ -326,18 +326,7 @@
14.4 (*----------- 80 -----------*)
14.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.7 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.8 -if p = ([2, 1], Pbl) andalso
14.9 - f = PpcKF (Problem [], {Find = [Incompl "equality"], Given = [Incompl "functionEq", Incompl "substitution"], Relate = [], Where = [], With = []})
14.10 -then
14.11 - case nxt of
14.12 - ("Add_Given", Add_Given "functionEq (hd [])") => ((*here is an error in partial_function*))
14.13 - | _ => error "me biegelinie changed 1"
14.14 -else error "me biegelinie changed 2";
14.15 -
14.16 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.17 -nxt;(* = ("Tac ", Tac "[error] appl_add: is_known: seek_oridts: input ('substitution (NTH (1 + -4) [])') not found in oris (typed)")*)
14.18 -(*----- due to problems with generalised handling of meths which extend the model of a probl
14.19 +val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.20 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.21 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
14.22 (*----------- 90 -----------*)
14.23 @@ -386,7 +375,6 @@
14.24 | _ => error "Bsp.7.70 me changed 1")
14.25 | _ => error "Bsp.7.70 me changed 2"
14.26 else error "Bsp.7.70 me changed 3";
14.27 ------*)
14.28 (* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
14.29
14.30 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
14.31 @@ -435,15 +423,6 @@
14.32 val ip = get_pos 1 1;
14.33 val (Form f, tac, asms) = pt_extract (pt, ip);
14.34
14.35 -if ip = ([2, 1, 1], Frm) andalso
14.36 -term2str f = "hd []"
14.37 -then
14.38 - case tac of
14.39 - SOME Empty_Tac => ()
14.40 - | _ => error "ERROR biegel.7.70 changed 1"
14.41 -else error "ERROR biegel.7.70 changed 2";
14.42 -
14.43 -(*----- this state has been reached shortly after 98298342fb6d:
14.44 if ip = ([3, 8, 1], Res) andalso
14.45 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]"
14.46 then
14.47 @@ -451,4 +430,4 @@
14.48 SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
14.49 | _ => error "ERROR biegel.7.70 changed 1"
14.50 else error "ERROR biegel.7.70 changed 2";
14.51 -*)
14.52 \ No newline at end of file
14.53 +(* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
15.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Sat Jun 01 11:09:19 2019 +0200
15.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Sat Jun 22 13:15:52 2019 +0200
15.3 @@ -16,6 +16,8 @@
15.4 "----------- autoCalculate for met_partial_fraction -----";
15.5 "----------- progr.vers.2: check erls for multiply_ansatz";
15.6 "----------- progr.vers.2: improve program --------------";
15.7 +"----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------";
15.8 +"----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
15.9 "--------------------------------------------------------";
15.10 "--------------------------------------------------------";
15.11 "--------------------------------------------------------";
15.12 @@ -25,7 +27,7 @@
15.13 "----------- why helpless here ? ------------------------";
15.14 "----------- why helpless here ? ------------------------";
15.15 val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
15.16 - "stepResponse (x[n::real]::bool)"];
15.17 + "functionName X_z", "stepResponse (x[n::real]::bool)"];
15.18 val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
15.19 ["SignalProcessing","Z_Transform","Inverse"]);
15.20 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
15.21 @@ -500,5 +502,94 @@
15.22 " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
15.23 " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
15.24 " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
15.25 - " in pbz)"
15.26 + " in pbz)";
15.27
15.28 +"----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------";
15.29 +"----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------";
15.30 +"----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---------";
15.31 +val fmz_from_Subproblem_of_Inverse_sub = (*see --- test [SignalProcessing,Z_Transform,Inverse_s.."*)
15.32 + (["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", "solveFor z",
15.33 + "decomposedFunction p_p'''"],
15.34 + ("Isac", ["partial_fraction", "rational", "simplification"],
15.35 + ["simplification", "of_rationals", "to_partial_fraction"]))
15.36 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz_from_Subproblem_of_Inverse_sub)];
15.37 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.38 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.39 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.40 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.41 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.42 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.43 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.44 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.45 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.46 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.47 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.48 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.49 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.50 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.51 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.52 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.53 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.54 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.55 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.56 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.57 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.58 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.59 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.60 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.61 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.62 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.63 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.64 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.65 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.66 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.67 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.68 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.69 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.70 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.71 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.72 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.73 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.74 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.75 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.76 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.77 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.78 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.79 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.80 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.81 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.82 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.83 +
15.84 +if fst nxt = "End_Proof'" andalso f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then ()
15.85 +else error "--- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ---";
15.86 +
15.87 +
15.88 +"----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
15.89 +"----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
15.90 +"----------- isolate SubProblem [simplification, of_rationals, to_partial_fraction] auto -------";
15.91 +reset_states ();
15.92 +(*val PblObj {fmz_from_Subproblem_of_Inverse_sub, ...} = get_obj I pt (fst p)
15.93 + see --- test [SignalProcessing,Z_Transform,Inverse_sub] me = ";*)
15.94 +
15.95 +val fmz_from_Subproblem_of_Inverse_sub = (*see --- test [SignalProcessing,Z_Transform,Inverse_s.."*)
15.96 + (["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))", "solveFor z",
15.97 + "decomposedFunction p_p'''"],
15.98 + ("Isac", ["partial_fraction", "rational", "simplification"],
15.99 + ["simplification", "of_rationals", "to_partial_fraction"]));
15.100 +CalcTree [fmz_from_Subproblem_of_Inverse_sub];
15.101 +Iterator 1;
15.102 +moveActiveRoot 1;
15.103 +(*
15.104 +autoCalculate 1 CompleteCalc;
15.105 +exception Empty raised (line 429 of "library.ML") TODO during lucin: *)
15.106 +
15.107 +(*
15.108 +trace_script := true;
15.109 +
15.110 +@@@ program ["simplification","of_rationals","to_partial_fraction"]
15.111 +@@@ istate ["
15.112 +(f_f, 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))","
15.113 +(zzz, z)"]
15.114 +@@@ next leaf 'Take f_f' ---> STac 'Take (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))'
15.115 +*)
15.116 +
16.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Sat Jun 01 11:09:19 2019 +0200
16.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Sat Jun 22 13:15:52 2019 +0200
16.3 @@ -64,32 +64,36 @@
16.4 val scr as Prog sc = (#scr o get_met) metID
16.5 val formals = formal_args sc
16.6 (*expects same sequence of (actual) args in itms and (formal) args in met*)
16.7 - fun relate_args env [] [] = env
16.8 - | relate_args _ _ [] =
16.9 - error ("ERROR in creating the environment for '" ^
16.10 - id_of_scr sc ^ "' from \nthe items of the guard of " ^
16.11 - metID2str metID ^ ",\n" ^
16.12 - "formal arg(s), from the script, miss actual arg(s), from the guards env:\n" ^
16.13 - (string_of_int o length) formals ^
16.14 - " formals: " ^ terms2str formals ^ "\n" ^
16.15 - (string_of_int o length) actuals ^
16.16 - " actuals: " ^ terms2str actuals)
16.17 - | relate_args env [] _ = env (*may drop Find!*)
16.18 - | relate_args env (a::aa) (f::ff) =
16.19 - if type_of a = type_of f
16.20 - then relate_args (env @ [(a, f)]) aa ff
16.21 - else
16.22 - error ("ERROR in creating the environment for '" ^
16.23 - id_of_scr sc ^ "' from \nthe items of the guard of " ^
16.24 - metID2str metID ^ ",\n" ^
16.25 - "different types of formal arg, from the script, " ^
16.26 - "and actual arg, from the guards env:'\n" ^
16.27 - "formal: '" ^ term2str a ^ "::" ^ (type2str o type_of) a ^ "'\n" ^
16.28 - "actual: '" ^ term2str f ^ "::" ^ (type2str o type_of) f ^ "'\n" ^
16.29 - "in\n" ^
16.30 - "formals: " ^ terms2str formals ^ "\n" ^
16.31 - "actuals: " ^ terms2str actuals)
16.32 - val env = relate_args [] formals actuals;
16.33 +fun msg_miss sc metID caller f formals actuals =
16.34 + "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (LTool.get_fun_id sc) ^ "\"\n" ^
16.35 + "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
16.36 + "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
16.37 + "with:\n" ^
16.38 + (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
16.39 + (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
16.40 +fun msg_ambiguous sc metID f aas formals actuals =
16.41 + "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (LTool.get_fun_id sc) ^ "\"\n" ^
16.42 + "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
16.43 + "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
16.44 + "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
16.45 + "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
16.46 + "with\n" ^
16.47 + "formals: " ^ Rule.terms2str formals ^ "\n" ^
16.48 + "actuals: " ^ Rule.terms2str actuals
16.49 + fun assoc_by_type f aa =
16.50 + case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
16.51 + [] => error (msg_miss sc metID "assoc_by_type" f formals actuals)
16.52 + | [a] => (f, a)
16.53 + | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
16.54 + fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
16.55 + | relate_args env [] _ = env (*may drop Find?*)
16.56 + | relate_args env (f::ff) (aas as (a::aa)) =
16.57 + if type_of f = type_of a
16.58 + then relate_args (env @ [(f, a)]) ff aa
16.59 + else
16.60 + let val (f, a) = assoc_by_type f aas
16.61 + in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
16.62 + val env = relate_args [] formals actuals;
16.63 val ctxt = Proof_Context.init_global thy |> declare_constraints' actuals
16.64 val {pre, prls, ...} = get_met metID;
16.65 val pres = check_preconds thy prls pre itms |> map snd;
17.1 --- a/test/Tools/isac/ProgLang/termC.sml Sat Jun 01 11:09:19 2019 +0200
17.2 +++ b/test/Tools/isac/ProgLang/termC.sml Sat Jun 22 13:15:52 2019 +0200
17.3 @@ -29,6 +29,7 @@
17.4 "----------- fun dest_binop_typ ----------------------------------------------------------------";
17.5 "----------- fun is_list -----------------------------------------------------------------------";
17.6 "----------- fun inst_abs ----------------------------------------------------------------------";
17.7 +"----------- fun numbers_to_string -------------------------------------------------------------";
17.8 "--------------------------------------------------------";
17.9 "--------------------------------------------------------";
17.10
17.11 @@ -740,3 +741,13 @@
17.12 val Const ("Equation.Function2Equality", _) $ Free ("fu_n", _) $ Free ("su_b", _) $ scr'_body = scr'
17.13 ;
17.14 if scr'_body = LTool.body_of original then () else error "inst_abs changed";
17.15 +
17.16 +"----------- fun numbers_to_string -------------------------------------------------------------";
17.17 +"----------- fun numbers_to_string -------------------------------------------------------------";
17.18 +"----------- fun numbers_to_string -------------------------------------------------------------";
17.19 +if numbers_to_string @{term "123::real"} = Free ("123", HOLogic.realT)
17.20 +then () else error "numbers_to_string '123' changed";
17.21 +if numbers_to_string @{term "1::real"} = Free ("1", HOLogic.realT)
17.22 +then () else error "numbers_to_string '1' changed";
17.23 +if numbers_to_string @{term "0::real"} = Free ("0", HOLogic.realT)
17.24 +then () else error "numbers_to_string '0' changed";
18.1 --- a/test/Tools/isac/Test_Some.thy Sat Jun 01 11:09:19 2019 +0200
18.2 +++ b/test/Tools/isac/Test_Some.thy Sat Jun 22 13:15:52 2019 +0200
18.3 @@ -67,998 +67,10 @@
18.4 "~~~~~ fun xxx , args:"; val () = ();
18.5 \<close>
18.6
18.7 -section \<open>================= "Knowledge/partial_fractions.sml" ============================\<close>
18.8 +section \<open>===================================================================================\<close>
18.9 ML \<open>
18.10 "~~~~~ fun xxx , args:"; val () = ();
18.11 \<close> ML \<open>
18.12 -(* Title: partial fraction decomposition
18.13 - Author: Jan Rocnik
18.14 - (c) due to copyright terms
18.15 -*)
18.16 -
18.17 -"--------------------------------------------------------";
18.18 -"table of contents --------------------------------------";
18.19 -"--------------------------------------------------------";
18.20 -"----------- why helpless here ? ------------------------";
18.21 -"----------- why not nxt = Model_Problem here ? ---------";
18.22 -"----------- fun factors_from_solution ------------------";
18.23 -"----------- Logic.unvarify_global ----------------------";
18.24 -"----------- eval_drop_questionmarks --------------------";
18.25 -"----------- = me for met_partial_fraction --------------";
18.26 -"----------- autoCalculate for met_partial_fraction -----";
18.27 -"----------- progr.vers.2: check erls for multiply_ansatz";
18.28 -"----------- progr.vers.2: improve program --------------";
18.29 -"--------------------------------------------------------";
18.30 -"--------------------------------------------------------";
18.31 -"--------------------------------------------------------";
18.32 -
18.33 -
18.34 -"----------- why helpless here ? ------------------------";
18.35 -"----------- why helpless here ? ------------------------";
18.36 -"----------- why helpless here ? ------------------------";
18.37 -\<close> ML \<open>
18.38 -val fmz = ["filterExpression (X z = 3 / (z - 1/4 + -1/8 * (1/(z::real))))",
18.39 - "stepResponse (x[n::real]::bool)"];
18.40 -val (dI,pI,mI) = ("Isac", ["Inverse", "Z_Transform", "SignalProcessing"],
18.41 - ["SignalProcessing","Z_Transform","Inverse"]);
18.42 -val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI,pI,mI))];
18.43 -\<close> ML \<open>
18.44 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Given";
18.45 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Add_Find";
18.46 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Theory";
18.47 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
18.48 -\<close> ML \<open>
18.49 -(*CURRENT*)(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*Specify_Method ["SignalProcessing", "Z_Transform", "Inverse"])*)
18.50 -\<close> ML \<open>
18.51 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
18.52 -(*CURRENT*)(*ERROR in creating the environment from formal args. of partial_function "HOL.eq"
18.53 -and the actual args., ie. items of the guard of "["SignalProcessing","Z_Transform","Inverse"]" by "assoc_by_type":
18.54 -formal arg "TYPE('a)" doesn't mach an actual arg.
18.55 -with:
18.56 -3 formal args: ["TYPE('a)","X_eq","z"]
18.57 -2 actual args: ["X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))","x [n]"]*)
18.58 -\<close> ML \<open>
18.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))";
18.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)))";
18.61 -\<close> ML \<open>
18.62 -"~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
18.63 -val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
18.64 -val (pt, p) = ptp;
18.65 -"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
18.66 - (p, ((pt, e_pos'),[]));
18.67 -val pIopt = get_pblID (pt,ip);
18.68 -ip = ([],Res); "false";
18.69 -tacis; " = []";
18.70 -pIopt; (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*)
18.71 -member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); "false";
18.72 -(*nxt_solve_ (pt,ip); "WAS isalist2list applied to NON-list 'no_meth'"
18.73 - THIS MEANS: replace no_meth by [no_meth] in Script.*)
18.74 -(*WAS val ("helpless",_) = step p ((pt, e_pos'),[]) *)
18.75 -(*WAS val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Empty_Tac instead SubProblem";*)
18.76 -
18.77 -\<close> ML \<open>
18.78 -"----------- why not nxt = Model_Problem here ? ---------";
18.79 -"----------- why not nxt = Model_Problem here ? ---------";
18.80 -"----------- why not nxt = Model_Problem here ? ---------";
18.81 -val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt''';
18.82 -"~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt);
18.83 -val ("ok", (_, _, ptp)) = locatetac tac (pt,p);
18.84 -val (pt, p) = ptp;
18.85 -"~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
18.86 - (p, ((pt, e_pos'),[]));
18.87 -val pIopt = get_pblID (pt,ip);
18.88 -ip = ([],Res); " = false";
18.89 -tacis; " = []";
18.90 -pIopt (* = SOME ["Inverse", "Z_Transform", "SignalProcessing"]*);
18.91 -member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); " = false";
18.92 -(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ leads into
18.93 -nxt_solve_, which is definitely WRONG (should be nxt_specify_ for FIND_ADD).
18.94 -This ERROR seems to be introduced together with ctxt, concerns Apply_Method without init_form.
18.95 -See TODO.txt
18.96 -*)
18.97 -
18.98 -\<close> ML \<open>
18.99 -"----------- fun factors_from_solution ------------------";
18.100 -"----------- fun factors_from_solution ------------------";
18.101 -"----------- fun factors_from_solution ------------------";
18.102 -val ctxt = Proof_Context.init_global @{theory Isac};
18.103 -val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
18.104 -val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
18.105 -if term2str t' =
18.106 - "factors_from_solution [z = 1 / 2, z = -1 / 4] = (z - 1 / 2) * (z - -1 / 4)"
18.107 -then () else error "factors_from_solution broken";
18.108 -
18.109 -\<close> ML \<open>
18.110 -"----------- Logic.unvarify_global ----------------------";
18.111 -"----------- Logic.unvarify_global ----------------------";
18.112 -"----------- Logic.unvarify_global ----------------------";
18.113 -val A_var = parseNEW ctxt "A::real" |> the |> Logic.varify_global
18.114 -val B_var = parseNEW ctxt "B::real" |> the |> Logic.varify_global
18.115 -
18.116 -val denom1 = parseNEW ctxt "(z + -1 * (1 / 2))::real" |> the;
18.117 -val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
18.118 -
18.119 -val test = HOLogic.mk_binop "Groups.plus_class.plus"
18.120 - (HOLogic.mk_binop "Rings.divide_class.divide" (A_var, denom1),
18.121 - HOLogic.mk_binop "Rings.divide_class.divide" (B_var, denom2));
18.122 -
18.123 -if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
18.124 - else error "HOLogic.mk_binop broken ?";
18.125 -
18.126 -(* Logic.unvarify_global test
18.127 ----> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
18.128 -thus we need another fun var2free in termC.sml*)
18.129 -
18.130 -\<close> ML \<open>
18.131 -"----------- = me for met_partial_fraction --------------";
18.132 -"----------- = me for met_partial_fraction --------------";
18.133 -"----------- = me for met_partial_fraction --------------";
18.134 -val fmz =
18.135 - ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
18.136 - "solveFor z", "decomposedFunction p_p"];
18.137 -val (dI',pI',mI') =
18.138 - ("Partial_Fractions",
18.139 - ["partial_fraction", "rational", "simplification"],
18.140 - ["simplification","of_rationals","to_partial_fraction"]);
18.141 -(*[ ], Pbl*)val (p,_,f,nxt,_,pt) =
18.142 - CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
18.143 -(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))")*)
18.144 -(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
18.145 -(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "decomposedFunction p_p")*)
18.146 -(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "Partial_Fractions")*)
18.147 - (*05*)
18.148 -(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["partial_fraction", "rational", "simplification"])*)
18.149 -(*[ ], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
18.150 -(*[ ], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["simplification", "of_rationals", "to_partial_fraction"])*)
18.151 -(*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "norm_Rational")*)
18.152 -(*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("PolyEq", ["abcFormula", "degree_2", "polynomial", "univariate", "equation"]))*)
18.153 - (*10*)
18.154 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem)*)
18.155 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (-1 + -2 * z + 8 * z ^^^ 2 = 0)")*)
18.156 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor z")*)
18.157 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Find "solutions z_i")*)
18.158 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Theory "PolyEq")*)
18.159 -(*[2], Pbl*)(*15*)
18.160 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
18.161 -(*[2], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
18.162 -(*[2], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "solve_d2_polyeq_abc_equation"])*)
18.163 -(*[2, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', z)"], "d2_polyeq_abcFormula_simplify"))*)
18.164 -(*[2, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify")*)
18.165 - (*20*)
18.166 -(*[2, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Or_to_List)*)
18.167 -(*[2, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions")*)
18.168 -(*[2, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["abcFormula", "degree_2", "polynomial", "univariate", "equation"])*)
18.169 -(*[2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 / ((z - 1 / 2) * (z - -1 / 4))")*)
18.170 -(*[3], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "ansatz_rls")*)
18.171 - (*25*)
18.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)")*)
18.173 -(*[4], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "equival_trans")*)
18.174 -(*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)"*)
18.175 -(*[5], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["z = 1 / 2"])*)
18.176 -(*[5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*nxt = Rewrite_Set "norm_Rational"*)
18.177 -(*[6], Res*)val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt;(*nxt = Subproblem ("Isac", ["normalise", "polynomial", "univariate", "equation"]*)
18.178 - (*30+1*)
18.179 -(*[7], Pbl*)val (p'''',_,f,nxt'''',_,pt'''') = me nxt''' p''' [] pt'''; (*nxt = Model_Problem*)
18.180 -(*[7], Pbl*)val (p'v,_,f,nxt'v,_,pt'v) = me nxt'''' p'''' [] pt''''; (*nxt = Add_Given "equality (3 = 3 * AA / 4)")*)
18.181 -(*[7], Pbl*)val (p'v',_,f,nxt'v',_,pt'v') = me nxt'v p'v [] pt'v; (*nxt = Add_Given "solveFor AA")*)
18.182 -(*[7], Pbl*)val (p'v'',_,f,nxt'v'',_,pt'v'') = me nxt'v' p'v' [] pt'v'; (*nxt = Add_Find "solutions AA_i")*)
18.183 -(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt'v'' p'v'' [] pt'v''; (*nxt = Specify_Theory "Isac"*)
18.184 - (*35*)
18.185 -(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Problem ["normalise", "polynomial", "univariate", "equation"])*)
18.186 -(*[7], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Specify_Method ["PolyEq", "normalise_poly"])*)
18.187 -(*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
18.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)"))*)
18.189 -(*[7, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst (["(''bdv'', AA)"], "make_ratpoly_in")*)
18.190 - (*40*)
18.191 -(*[7, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "polyeq_simplify"*)
18.192 -(*[7, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subproblem ("Isac", ["degree_1", "polynomial", "univariate", "equation"])*)
18.193 -(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Model_Problem*)
18.194 -(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "equality (3 + -3 / 4 * AA = 0)"*)
18.195 -(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "solveFor AA"*)
18.196 - (*45*)
18.197 -(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.198 -(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.199 -(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.200 -(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.201 -(*[7, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.202 - (*50*)
18.203 -(*[7, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.204 -(*[7, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.205 -(*[7, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.206 -(*[7, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.207 -(*[7, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.208 - (*55*)
18.209 -(*[7, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.210 -(*[7, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.211 -(*[7, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.212 -(*[7], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.213 -(*[8], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.214 - (*60*)
18.215 -(*[8], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.216 -(*[9], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.217 -(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.218 -(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.219 -(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.220 - (*65*)
18.221 -(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.222 -(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.223 -(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.224 -(*[10], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.225 -(*[10], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.226 - (*70*)
18.227 -(*[10, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.228 -(*[10, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.229 -(*[10, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.230 -(*[10, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.231 -(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.232 - (*75*)
18.233 -(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.234 -(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.235 -(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.236 -(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.237 -(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.238 - (*80*)
18.239 -(*[10, 4], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.240 -(*[10, 4], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.241 -(*[10, 4, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.242 -(*[10, 4, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.243 -(*[10, 4, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.244 - (*85*)
18.245 -(*[10, 4, 3], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = *)
18.246 -(*[10, 4, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_elementwise "Assumptions"*)
18.247 -(*[10, 4, 5], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["degree_1", "polynomial", "univariate", "equation"*)
18.248 -(*[10, 4], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["normalise", "polynomial", "univariate", "equation"]*)
18.249 -
18.250 -(*[10], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)"*)
18.251 - (*90*)
18.252 -(*[11], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Substitute ["AA = 4", "BB = -4"]*)
18.253 -(*[11], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["partial_fraction", "rational", "simplification"]*)
18.254 -(*[], Res*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = End_Proof'*)
18.255 -
18.256 -case nxt of
18.257 - (_, End_Proof') => if f2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" then ()
18.258 - else error "= me .. met_partial_fraction f changed"
18.259 -| _ => error "= me .. met_partial_fraction nxt changed";
18.260 -
18.261 -show_pt_tac pt; (*[
18.262 -([], Frm), Problem
18.263 - (''Partial_Fractions'',
18.264 - ??.\<^const>String.char.Char ''partial_fraction'' ''rational''
18.265 - ''simplification'')
18.266 -. . . . . . . . . . Apply_Method ["simplification","of_rationals","to_partial_fraction"],
18.267 -([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))
18.268 -. . . . . . . . . . Rewrite_Set "norm_Rational",
18.269 -([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)
18.270 -. . . . . . . . . . Subproblem (Isac, ["abcFormula","degree_2","polynomial","univariate","equation"]),
18.271 -([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)
18.272 -. . . . . . . . . . Apply_Method ["PolyEq","solve_d2_polyeq_abc_equation"],
18.273 -([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0
18.274 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', z)], "d2_polyeq_abcFormula_simplify"),
18.275 -([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) \<or>
18.276 -z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)
18.277 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
18.278 -([2,2], Res), z = 1 / 2 \<or> z = -1 / 4
18.279 -. . . . . . . . . . Or_to_List ,
18.280 -([2,3], Res), [z = 1 / 2, z = -1 / 4]
18.281 -. . . . . . . . . . Check_elementwise "Assumptions",
18.282 -([2,4], Res), [z = 1 / 2, z = -1 / 4]
18.283 -. . . . . . . . . . Check_Postcond ["abcFormula","degree_2","polynomial","univariate","equation"],
18.284 -([2], Res), [z = 1 / 2, z = -1 / 4]
18.285 -. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4))",
18.286 -([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))
18.287 -. . . . . . . . . . Rewrite_Set "ansatz_rls",
18.288 -([3], Res), AA / (z - 1 / 2) + BB / (z - -1 / 4)
18.289 -. . . . . . . . . . Take "3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)",
18.290 -([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = AA / (z - 1 / 2) + BB / (z - -1 / 4)
18.291 -. . . . . . . . . . Rewrite_Set "equival_trans",
18.292 -([4], Res), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
18.293 -. . . . . . . . . . Substitute ["z = 1 / 2"],
18.294 -([5], Res), 3 = AA * (1 / 2 - -1 / 4) + BB * (1 / 2 - 1 / 2)
18.295 -. . . . . . . . . . Rewrite_Set "norm_Rational",
18.296 -([6], Res), 3 = 3 * AA / 4
18.297 -. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
18.298 -([7], Pbl), solve (3 = 3 * AA / 4, AA)
18.299 -. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
18.300 -([7,1], Frm), 3 = 3 * AA / 4
18.301 -. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
18.302 -([7,1], Res), 3 - 3 * AA / 4 = 0
18.303 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "make_ratpoly_in"),
18.304 -([7,2], Res), 3 / 1 + -3 / 4 * AA = 0
18.305 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
18.306 -([7,3], Res), 3 + -3 / 4 * AA = 0
18.307 -. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
18.308 -([7,4], Pbl), solve (3 + -3 / 4 * AA = 0, AA)
18.309 -. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
18.310 -([7,4,1], Frm), 3 + -3 / 4 * AA = 0
18.311 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', AA)], "d1_polyeq_simplify"),
18.312 -([7,4,1], Res), AA = -1 * 3 / (-3 / 4)
18.313 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
18.314 -([7,4,2], Res), AA = -3 / (-3 / 4)
18.315 -. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
18.316 -([7,4,3], Res), AA = 4
18.317 -. . . . . . . . . . Or_to_List ,
18.318 -([7,4,4], Res), [AA = 4]
18.319 -. . . . . . . . . . Check_elementwise "Assumptions",
18.320 -([7,4,5], Res), [AA = 4]
18.321 -. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
18.322 -([7,4], Res), [AA = 4]
18.323 -. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
18.324 -([7], Res), [AA = 4]
18.325 -. . . . . . . . . . Take "3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)",
18.326 -([8], Frm), 3 = AA * (z - -1 / 4) + BB * (z - 1 / 2)
18.327 -. . . . . . . . . . Substitute ["z = -1 / 4"],
18.328 -([8], Res), 3 = AA * (-1 / 4 - -1 / 4) + BB * (-1 / 4 - 1 / 2)
18.329 -. . . . . . . . . . Rewrite_Set "norm_Rational",
18.330 -([9], Res), 3 = -3 * BB / 4
18.331 -. . . . . . . . . . Subproblem (Isac, ["normalise","polynomial","univariate","equation"]),
18.332 -([10], Pbl), solve (3 = -3 * BB / 4, BB)
18.333 -. . . . . . . . . . Apply_Method ["PolyEq","normalise_poly"],
18.334 -([10,1], Frm), 3 = -3 * BB / 4
18.335 -. . . . . . . . . . Rewrite ("all_left", "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a - ?b = 0)"),
18.336 -([10,1], Res), 3 - -3 * BB / 4 = 0
18.337 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "make_ratpoly_in"),
18.338 -([10,2], Res), 3 / 1 + 3 / 4 * BB = 0
18.339 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
18.340 -([10,3], Res), 3 + 3 / 4 * BB = 0
18.341 -. . . . . . . . . . Subproblem (Isac, ["degree_1","polynomial","univariate","equation"]),
18.342 -([10,4], Pbl), solve (3 + 3 / 4 * BB = 0, BB)
18.343 -. . . . . . . . . . Apply_Method ["PolyEq","solve_d1_polyeq_equation"],
18.344 -([10,4,1], Frm), 3 + 3 / 4 * BB = 0
18.345 -. . . . . . . . . . Rewrite_Set_Inst ([(''bdv'', BB)], "d1_polyeq_simplify"),
18.346 -([10,4,1], Res), BB = -1 * 3 / (3 / 4)
18.347 -. . . . . . . . . . Rewrite_Set "polyeq_simplify",
18.348 -([10,4,2], Res), BB = -3 / (3 / 4)
18.349 -. . . . . . . . . . Rewrite_Set "norm_Rational_parenthesized",
18.350 -([10,4,3], Res), BB = -4
18.351 -. . . . . . . . . . Or_to_List ,
18.352 -([10,4,4], Res), [BB = -4]
18.353 -. . . . . . . . . . Check_elementwise "Assumptions",
18.354 -([10,4,5], Res), [BB = -4]
18.355 -. . . . . . . . . . Check_Postcond ["degree_1","polynomial","univariate","equation"],
18.356 -([10,4], Res), [BB = -4]
18.357 -. . . . . . . . . . Check_Postcond ["normalise","polynomial","univariate","equation"],
18.358 -([10], Res), [BB = -4]
18.359 -. . . . . . . . . . Take "AA / (z - 1 / 2) + BB / (z - -1 / 4)",
18.360 -([11], Frm), AA / (z - 1 / 2) + BB / (z - -1 / 4)
18.361 -. . . . . . . . . . Substitute ["AA = 4","BB = -4"],
18.362 -([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)
18.363 -. . . . . . . . . . Check_Postcond ["partial_fraction","rational","simplification"],
18.364 -([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)]
18.365 -val it = (): unit
18.366 -*)
18.367 -
18.368 -"----------- autoCalculate for met_partial_fraction -----";
18.369 -"----------- autoCalculate for met_partial_fraction -----";
18.370 -"----------- autoCalculate for met_partial_fraction -----";
18.371 -reset_states ();
18.372 - val fmz =
18.373 - ["functionTerm (3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z))))",
18.374 - "solveFor z", "decomposedFunction p_p"];
18.375 - val (dI', pI', mI') =
18.376 - ("Partial_Fractions",
18.377 - ["partial_fraction", "rational", "simplification"],
18.378 - ["simplification","of_rationals","to_partial_fraction"]);
18.379 -CalcTree [(fmz, (dI' ,pI' ,mI'))];
18.380 -Iterator 1;
18.381 -moveActiveRoot 1;
18.382 -autoCalculate 1 CompleteCalc;
18.383 -
18.384 -val ((pt,p),_) = get_calc 1; val ip = get_pos 1 1;
18.385 -if p = ip andalso ip = ([], Res) then ()
18.386 - else error "autoCalculate for met_partial_fraction changed: final pos'";
18.387 -
18.388 -val (Form f, tac, asms) = pt_extract (pt, p);
18.389 -if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
18.390 - terms2str' asms =
18.391 - "[BB = -4,BB is_polyexp,AA is_polyexp,AA = 4," ^
18.392 - "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
18.393 - "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"
18.394 -then case tac of NONE => ()
18.395 - | _ => error "me for met_partial_fraction changed: final result 1"
18.396 -else error "me for met_partial_fraction changed: final result 2"
18.397 -
18.398 -show_pt pt;
18.399 -(*[
18.400 -(([], Frm), Problem (Partial_Fractions, [partial_fraction, rational, simplification])),
18.401 -(([1], Frm), 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))),
18.402 -(([1], Res), 24 / (-1 + -2 * z + 8 * z ^^^ 2)),
18.403 -(([2], Pbl), solve (-1 + -2 * z + 8 * z ^^^ 2 = 0, z)),
18.404 -(([2,1], Frm), -1 + -2 * z + 8 * z ^^^ 2 = 0),
18.405 -(([2,1], Res), z = (- -2 + sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8) |
18.406 -z = (- -2 - sqrt (-2 ^^^ 2 - 4 * 8 * -1)) / (2 * 8)),
18.407 -(([2,2], Res), z = 1 / 2 | z = -1 / 4),
18.408 -(([2,3], Res), [z = 1 / 2, z = -1 / 4]),
18.409 -(([2,4], Res), [z = 1 / 2, z = -1 / 4]),
18.410 -(([2], Res), [z = 1 / 2, z = -1 / 4]),
18.411 -(([3], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4))),
18.412 -(([3], Res), ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
18.413 -(([4], Frm), 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)),
18.414 -(([4], Res), 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)),
18.415 -(([5], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
18.416 -(([5], Res), 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)),
18.417 -(([6], Res), 3 = 3 * A / 4),
18.418 -(([7], Pbl), solve (3 = 3 * A / 4, A)),
18.419 -(([7,1], Frm), 3 = 3 * A / 4),
18.420 -(([7,1], Res), 3 - 3 * A / 4 = 0),
18.421 -(([7,2], Res), 3 / 1 + -3 / 4 * A = 0),
18.422 -(([7,3], Res), 3 + -3 / 4 * A = 0),
18.423 -(([7,4], Pbl), solve (3 + -3 / 4 * A = 0, A)),
18.424 -(([7,4,1], Frm), 3 + -3 / 4 * A = 0),
18.425 -(([7,4,1], Res), A = -1 * 3 / (-3 / 4)),
18.426 -(([7,4,2], Res), A = -3 / (-3 / 4)),
18.427 -(([7,4,3], Res), A = 4),
18.428 -(([7,4,4], Res), [A = 4]),
18.429 -(([7,4,5], Res), [A = 4]),
18.430 -(([7,4], Res), [A = 4]),
18.431 -(([7], Res), [A = 4]),
18.432 -(([8], Frm), 3 = A * (z - -1 / 4) + B * (z - 1 / 2)),
18.433 -(([8], Res), 3 = A * (-1 / 4 - -1 / 4) + B * (-1 / 4 - 1 / 2)),
18.434 -(([9], Res), 3 = -3 * B / 4),
18.435 -(([10], Pbl), solve (3 = -3 * B / 4, B)),
18.436 -(([10,1], Frm), 3 = -3 * B / 4),
18.437 -(([10,1], Res), 3 - -3 * B / 4 = 0),
18.438 -(([10,2], Res), 3 / 1 + 3 / 4 * B = 0),
18.439 -(([10,3], Res), 3 + 3 / 4 * B = 0),
18.440 -(([10,4], Pbl), solve (3 + 3 / 4 * B = 0, B)),
18.441 -(([10,4,1], Frm), 3 + 3 / 4 * B = 0),
18.442 -(([10,4,1], Res), B = -1 * 3 / (3 / 4)),
18.443 -(([10,4,2], Res), B = -3 / (3 / 4)),
18.444 -(([10,4,3], Res), B = -4),
18.445 -(([10,4,4], Res), [B = -4]),
18.446 -(([10,4,5], Res), [B = -4]),
18.447 -(([10,4], Res), [B = -4]),
18.448 -(([10], Res), [B = -4]),
18.449 -(([11], Frm), A / (z - 1 / 2) + B / (z - -1 / 4)),
18.450 -(([11], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)),
18.451 -(([], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4))] *)
18.452 -
18.453 -\<close> ML \<open>
18.454 -"----------- progr.vers.2: check erls for multiply_ansatz";
18.455 -"----------- progr.vers.2: check erls for multiply_ansatz";
18.456 -"----------- progr.vers.2: check erls for multiply_ansatz";
18.457 -(*test for outcommented 3 lines in script: is norm_Rational strong enough?*)
18.458 -val t = str2term "(3 / ((-1 + -2 * z + 8 * z ^^^ 2) *3/24)) = (3 / ((z - 1 / 2) * (z - -1 / 4)))";
18.459 -val SOME (t', _) = rewrite_set_ @{theory Isac} true ansatz_rls t;
18.460 -term2str t' = "3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - -1 / 4)";
18.461 -
18.462 -val SOME (t'', _) = rewrite_set_ @{theory Isac} true multiply_ansatz t'; (*true*)
18.463 -term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
18.464 - "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
18.465 -
18.466 -val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
18.467 -if term2str t''' = "3 = (AA + -2 * BB + 4 * z * AA + 4 * z * BB) / 4" then ()
18.468 -else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
18.469 -
18.470 -(*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
18.471 -val xxx = append_rls "multiply_ansatz_erls" norm_Rational
18.472 - [Calc ("HOL.eq",eval_equal "#equal_")];
18.473 -
18.474 -val multiply_ansatz = prep_rls @{theory} (
18.475 - Rls {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",dummy_ord),
18.476 - erls = xxx,
18.477 - srls = Erls, calc = [], errpatts = [],
18.478 - rules =
18.479 - [Thm ("multiply_2nd_order",num_str @{thm multiply_2nd_order})
18.480 - ],
18.481 - scr = EmptyScr}:rls);
18.482 -
18.483 -rewrite_set_ thy true xxx @{term "a+b = a+(b::real)"}; (*SOME ok*)
18.484 -rewrite_set_ thy true multiply_ansatz @{term "a+b = a+(b::real)"}; (*why NONE?*)
18.485 -
18.486 -"----------- progr.vers.2: improve program --------------";
18.487 -"----------- progr.vers.2: improve program --------------";
18.488 -"----------- progr.vers.2: improve program --------------";
18.489 -(*WN120318 stopped due to much effort with the test above*)
18.490 - "Script PartFracScript (f_f::real) (zzz::real) = " ^(*f_f: 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)), zzz: z*)
18.491 - " (let f_f = Take f_f; " ^
18.492 - " (num_orig::real) = get_numerator f_f; " ^(*num_orig: 3*)
18.493 - " f_f = (Rewrite_Set norm_Rational False) f_f; " ^(*f_f: 24 / (-1 + -2 * z + 8 * z ^^^ 2)*)
18.494 - " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
18.495 - " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
18.496 - " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
18.497 - " (L_L::bool list) = (SubProblem (PolyEqX, " ^
18.498 - " [abcFormula, degree_2, polynomial, univariate, equation], " ^
18.499 - " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
18.500 - " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
18.501 - " (eql::real) = Take (num_orig / facs); " ^(*eql: 3 / ((z - 1 / 2) * (z - -1 / 4)) *)
18.502 - " (eqr::real) = (Try (Rewrite_Set ansatz_rls False)) eql; " ^(*eqr: ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
18.503 - " (eq::bool) = Take (eql = eqr); " ^(*eq: 3 / ((z - 1 / 2) * (z - -1 / 4)) = ?A / (z - 1 / 2) + ?B / (z - -1 / 4)*)
18.504 -(*this has been tested below by rewrite_set_
18.505 - " (eeeee::bool) = Take ((num_orig / denom * denom / numer) = (num_orig / facs));" ^(**)
18.506 - " (eeeee::bool) = (Rewrite_Set ansatz_rls False) eeeee;" ^(**)
18.507 - " eq = (Try (Rewrite_Set multiply_ansatz False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
18.508 -NEXT try to outcomment the very next line..*)
18.509 - " eq = (Try (Rewrite_Set equival_trans False)) eeeee; " ^(*eq: 3 = ?A * (z - -1 / 4) + ?B * (z - 1 / 2)*)
18.510 - " eq = drop_questionmarks eq; " ^(*eq: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
18.511 - " (z1::real) = (rhs (NTH 1 L_L)); " ^(*z1: 1 / 2*)
18.512 - " (z2::real) = (rhs (NTH 2 L_L)); " ^(*z2: -1 / 4*)
18.513 - " (eq_a::bool) = Take eq; " ^(*eq_a: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
18.514 - " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
18.515 - " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
18.516 - " (sol_a::bool list) = " ^
18.517 - " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
18.518 - " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
18.519 - " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
18.520 - " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
18.521 - " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
18.522 - " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
18.523 - " (sol_b::bool list) = " ^
18.524 - " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
18.525 - " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
18.526 - " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
18.527 - " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
18.528 - " (pbz::real) = Take eqr; " ^(*pbz: A / (z - 1 / 2) + B / (z - -1 / 4)*)
18.529 - " pbz = ((Substitute [A = a, B = b]) pbz) " ^(*pbz: 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
18.530 - " in pbz)"
18.531 -
18.532 -\<close> ML \<open>
18.533 -\<close> ML \<open>
18.534 -"~~~~~ fun xxx , args:"; val () = ();
18.535 -\<close>
18.536 -
18.537 -section \<open>=============== "Knowledge/biegelinie-3.sml" ===============================\<close>
18.538 -ML \<open>
18.539 -"~~~~~ fun xxx , args:"; val () = ();
18.540 -\<close> ML \<open>
18.541 -(* "Knowledge/biegelinie-3.sml"
18.542 - author: Walther Neuper 190515
18.543 - (c) due to copyright terms
18.544 -*)
18.545 -"table of contents -----------------------------------------------";
18.546 -"-----------------------------------------------------------------";
18.547 -"----------- see biegelinie-1.sml---------------------------------";
18.548 -(* problems with generalised handling of meths which extend the model of a probl
18.549 - since 98298342fb6d: wait for review of whole model-specify phase *)
18.550 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
18.551 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
18.552 -"-----------------------------------------------------------------";
18.553 -"-----------------------------------------------------------------";
18.554 -"-----------------------------------------------------------------";
18.555 -
18.556 -\<close> ML \<open>
18.557 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
18.558 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
18.559 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
18.560 -"----- Bsp 7.70 with me";
18.561 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
18.562 - "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
18.563 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
18.564 - "AbleitungBiegelinie dy"];
18.565 -val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
18.566 - ["IntegrierenUndKonstanteBestimmen2"]);
18.567 -val p = e_pos'; val c = [];
18.568 -(*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*)
18.569 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
18.570 -
18.571 -(*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);
18.572 -(*+*)writeln (oris2str oris); (*[
18.573 -(1, ["1"], #Given,Traegerlaenge, ["L"]),
18.574 -(2, ["1"], #Given,Streckenlast, ["q_0"]),
18.575 -(3, ["1"], #Find,Biegelinie, ["y"]),
18.576 -(4, ["1"], #Relate,Randbedingungen, ["[y 0 = 0]","[y L = 0]","[M_b 0 = 0]","[M_b L = 0]"]),
18.577 -(5, ["1"], #undef,FunktionsVariable, ["x"]),
18.578 -(6, ["1"], #undef,GleichungsVariablen, ["[c]","[c_2]","[c_3]","[c_4]"]),
18.579 -(7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*)
18.580 -(*+*)itms2str_ @{context} probl = "[]";
18.581 -(*+*)itms2str_ @{context} meth = "[]";
18.582 -(*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)
18.583 -
18.584 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
18.585 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
18.586 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
18.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*)
18.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]"*)
18.589 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
18.590 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
18.591 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
18.592 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
18.593 -(*----------- 10 -----------*)
18.594 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
18.595 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy*)
18.596 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
18.597 -
18.598 -(*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)
18.599 -(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*)
18.600 -(*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script"
18.601 -and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type":
18.602 -formal arg. "b" type-matches with several...actual args. "["dy","y"]"
18.603 -selected "dy"
18.604 -with
18.605 -formals: ["l","q","v","b","s","vs","id_abl"]
18.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]"]*)
18.607 -
18.608 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt, p, c, pt);
18.609 - val (pt''', p''') =
18.610 - (*locatetac is here for testing by me; step would suffice in me*)
18.611 - case locatetac tac (pt,p) of
18.612 - ("ok", (_, _, ptp)) => ptp
18.613 -;
18.614 -(*+*)p = ([], Met);
18.615 -(*+*)p''' = ([1], Pbl);
18.616 -(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');
18.617 -(*+*)(*MISSING after locatetac:*)
18.618 -(*+*)writeln (oris2str oris); (*[
18.619 -(1, ["1"], #Given,Streckenlast, ["q_0"]),
18.620 -(2, ["1"], #Given,FunktionsVariable, ["x"]),
18.621 -(3, ["1"], #Find,Funktionen, ["funs'''"])]
18.622 -MISSING:
18.623 - Biegelinie
18.624 - AbleitungBiegelinie
18.625 -*)
18.626 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
18.627 - val (mI, m) = Solve.mk_tac'_ tac;
18.628 -val Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
18.629 -(*if*) member op = Solve.specsteps mI = false; (*else*)
18.630 -
18.631 -loc_solve_ (mI,m) ptp;
18.632 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = ((mI,m), ptp);
18.633 -
18.634 -Solve.solve m (pt, pos);
18.635 -"~~~~~ fun solve , args:"; val (("Apply_Method", m as Tac.Apply_Method' (mI, _, _, _)), (pt, (pos as (p, _)))) =
18.636 - (m, (pt, pos));
18.637 -val {srls, ...} = Specify.get_met mI;
18.638 - val itms = case get_obj I pt p of
18.639 - PblObj {meth=itms, ...} => itms
18.640 - | _ => error "solve Apply_Method: uncovered case get_obj"
18.641 - val thy' = get_obj g_domID pt p;
18.642 - val thy = Celem.assoc_thy thy';
18.643 - val (is, env, ctxt, sc) = case Lucin.init_scrstate thy itms mI of
18.644 - (is as Selem.ScrState (env,_,_,_,_,_), ctxt, sc) => (is, env, ctxt, sc)
18.645 - | _ => error "solve Apply_Method: uncovered case init_scrstate"
18.646 - val ini = Lucin.init_form thy sc env;
18.647 - val p = lev_dn p;
18.648 -val NONE = (*case*) ini (*of*);
18.649 - val (m', (is', ctxt'), _) = Lucin.next_tac (thy', srls) (pt, (p, Res)) sc (is, ctxt);
18.650 - val d = Rule.e_rls (*FIXME: get simplifier from domID*);
18.651 -val Steps (_, ss as (_, _, pt', p', c') :: _) =
18.652 -(*case*) Lucin.locate_gen (thy',srls) m' (pt,(p, Res)) (sc,d) (is', ctxt') (*of*);
18.653 -
18.654 -(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
18.655 -(*+*)(*MISSING after locate_gen:*)
18.656 -(*+*)writeln (oris2str oris); (*[
18.657 -(1, ["1"], #Given,Streckenlast, ["q_0"]),
18.658 -(2, ["1"], #Given,FunktionsVariable, ["x"]),
18.659 -(3, ["1"], #Find,Funktionen, ["funs'''"])]
18.660 -MISSING:
18.661 - Biegelinie
18.662 - AbleitungBiegelinie
18.663 -*)
18.664 -"~~~~~ fun locate_gen , args:"; val ((thy', srls), m, (pt, p),
18.665 - (scr as Rule.Prog sc, d), (Selem.ScrState (E,l,a,v,S,b), ctxt)) =
18.666 - ((thy',srls), m', (pt,(p, Res)), (sc,d), (is', ctxt'));
18.667 -val thy = Celem.assoc_thy thy';
18.668 -(*if*) l = [] orelse (
18.669 - (*init.in solve..Apply_Method...*)(last_elem o fst) p = 0 andalso snd p = Res) = true;(*then*)
18.670 -(assy (thy',ctxt,srls,d,Aundef) ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]) (body_of sc));
18.671 -
18.672 -"~~~~~ fun assy , args:"; val (ya, ((E,l,a,v,S,b),ss:step list), (Const ("HOL.Let",_) $ e $ (Abs (id,T,body)))) =
18.673 - ((thy',ctxt,srls,d,Aundef), ((E,[Celem.R],a,v,S,b), [(m,Generate.EmptyMout,pt,p,[])]), (body_of sc));
18.674 -(*case*) assy ya ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss) e (*of*);
18.675 -
18.676 -"~~~~~ fun assy , args:"; val ((thy',ctxt,sr,d,ap), ((E,l,a,v,S,_), (m,_,pt,(p,p_),c)::ss), t) =
18.677 - (ya, ((E , l @ [Celem.L, Celem.R], a,v,S,b), ss), e);
18.678 -val (a', LTool.STac stac) = (*case*) handle_leaf "locate" thy' sr E a v t (*of*);
18.679 -(*+*)writeln (term2str stac); (*SubProblem
18.680 - (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''],
18.681 - [''Biegelinien'', ''ausBelastung''])
18.682 - [REAL q_0, REAL x, REAL_REAL y, REAL_REAL dy] *)
18.683 - val p' =
18.684 - case p_ of Frm => p
18.685 - | Res => lev_on p
18.686 - | _ => error ("assy: call by " ^ pos'2str (p,p_));
18.687 - val Ass (m,v') = (*case*) assod pt d m stac (*of*);
18.688 -
18.689 -"~~~~~ fun assod , args:"; val (pt, _, (Tac.Subproblem' ((domID, pblID, _), _, _, _, _, _)),
18.690 - (stac as Const ("Script.SubProblem", _) $ (Const ("Product_Type.Pair", _) $
18.691 - dI' $ (Const ("Product_Type.Pair", _) $ pI' $ mI')) $ ags')) =
18.692 - (pt, d, m, stac);
18.693 - val dI = HOLogic.dest_string dI';
18.694 - val thy = Stool.common_subthy (Celem.assoc_thy dI, rootthy pt);
18.695 - val pI = pI' |> HOLogic.dest_list |> map HOLogic.dest_string;
18.696 - val mI = mI' |> HOLogic.dest_list |> map HOLogic.dest_string;
18.697 - val ags = TermC.isalist2list ags';
18.698 -(*if*) mI = ["no_met"] = false; (*else*)
18.699 -(* val (pI, pors, mI) = *)
18.700 - (pI, (Chead.match_ags thy ((#ppc o Specify.get_pbt) pI) ags)
18.701 - handle ERROR "actual args do not match formal args"
18.702 - => (Chead.match_ags_msg pI stac ags(*raise exn*); []), mI);
18.703 -"~~~~~ fun match_ags , args:"; val (thy, pbt, ags) = (thy, ((#ppc o Specify.get_pbt) pI), ags);
18.704 -(*+*)pbt;
18.705 - fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
18.706 - val pbt' = filter_out is_copy_named pbt
18.707 - val cy = filter is_copy_named pbt
18.708 - val oris' = matc thy pbt' ags []
18.709 - val cy' = map (cpy_nam pbt' oris') cy
18.710 - val ors = Specify.add_id (oris' @ cy') (*...appended in order to get into the model-items *)
18.711 -
18.712 -(*+*)val c = [];
18.713 -(*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
18.714 -
18.715 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)
18.716 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
18.717 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Funktionen funs'''"*)
18.718 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
18.719 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
18.720 -(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)
18.721 -(*----------- 20 -----------*)
18.722 -(*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
18.723 -(*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)
18.724 -ERROR itms2args: 'Biegelinie' not in itms*)
18.725 -
18.726 -(*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)
18.727 - [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]
18.728 - ^^^^^^^^^^^ ..ERROR itms2args: 'Biegelinie' not in itms*)
18.729 -(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');
18.730 -(*+*)if oris2str oris =
18.731 -(*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"
18.732 -(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";
18.733 -writeln (oris2str oris); (*[
18.734 -(1, ["1"], #Given,Streckenlast, ["q_0"]),
18.735 -(2, ["1"], #Given,FunktionsVariable, ["x"]),
18.736 -(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
18.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''']))]"
18.738 -(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";
18.739 -writeln (itms2str_ @{context} probl); (*[
18.740 -(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
18.741 -(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
18.742 -(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)
18.743 -(*+*)if itms2str_ @{context} meth = "[]"
18.744 -(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";
18.745 -writeln (itms2str_ @{context} meth); (*[]*)
18.746 -
18.747 -"~~~~~ fun me , args:"; val ((_, tac), p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
18.748 -(* val (pt, p) = *)
18.749 - (*locatetac is here for testing by me; step would suffice in me*)
18.750 - case locatetac tac (pt,p) of
18.751 - ("ok", (_, _, ptp)) => ptp
18.752 -;
18.753 -"~~~~~ fun locatetac , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
18.754 - val (mI, m) = Solve.mk_tac'_ tac;
18.755 -val Chead.Appl m = (*case*) Applicable.applicable_in p pt m (*of*);
18.756 -(*if*) member op = Solve.specsteps mI = true; (*then*)
18.757 -
18.758 -(*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
18.759 -"~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);
18.760 -(* val (p, _, f, _, _, pt) =*) Chead.specify m pos [] pt;
18.761 -
18.762 -"~~~~~ fun specify , args:"; val ((Tac.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);
18.763 - val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
18.764 - PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
18.765 - (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
18.766 - val {ppc, pre, prls,...} = Specify.get_met mID
18.767 - val thy = Celem.assoc_thy dI
18.768 - val dI'' = if dI = Rule.e_domID then dI' else dI
18.769 - val pI'' = if pI = Celem.e_pblID then pI' else pI
18.770 -;
18.771 -(*+*)writeln (oris2str oris); (*[
18.772 -(1, ["1"], #Given,Streckenlast, ["q_0"]),
18.773 -(2, ["1"], #Given,FunktionsVariable, ["x"]),
18.774 -(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
18.775 -(*+*)writeln (pats2str' ppc);
18.776 -(*["(#Given, (Streckenlast, q__q))
18.777 -","(#Given, (FunktionsVariable, v_v))
18.778 -","(#Given, (Biegelinie, id_fun))
18.779 -","(#Given, (AbleitungBiegelinie, id_abl))
18.780 -","(#Find, (Funktionen, fun_s))"]*)
18.781 -(*+*)writeln (pats2str' ((#ppc o Specify.get_pbt) pI));
18.782 -(*["(#Given, (Streckenlast, q_q))
18.783 -","(#Given, (FunktionsVariable, v_v))
18.784 -","(#Find, (Funktionen, funs'''))"]*)
18.785 - val oris = Specify.add_field' thy ppc oris
18.786 - val met = if met = [] then pbl else met
18.787 - val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
18.788 -;
18.789 -(*+*)writeln (itms2str_ @{context} itms); (*[
18.790 -(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
18.791 -(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
18.792 -(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)
18.793 -
18.794 -(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
18.795 -val itms =
18.796 - if mI' = ["Biegelinien", "ausBelastung"]
18.797 - then itms @
18.798 - [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
18.799 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
18.800 - (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
18.801 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
18.802 - (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
18.803 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
18.804 - (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
18.805 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
18.806 - else itms
18.807 -(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
18.808 -
18.809 -val itms' = itms @
18.810 - [(4, [1], true, "#Given", Cor ((@{term "Biegelinie"},
18.811 - [@{term "y::real \<Rightarrow> real"}]),
18.812 - (@{term "id_fun::real \<Rightarrow> real"},
18.813 - [@{term "y::real \<Rightarrow> real"}] ))),
18.814 - (5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"},
18.815 - [@{term "dy::real \<Rightarrow> real"}]),
18.816 - (@{term "id_abl::real \<Rightarrow> real"},
18.817 - [@{term "dy::real \<Rightarrow> real"}] )))]
18.818 -val itms'' = itms @
18.819 - [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
18.820 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
18.821 - (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
18.822 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
18.823 - (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Tools.una", [])])),
18.824 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
18.825 - (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
18.826 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
18.827 -;
18.828 -if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";
18.829 -(*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
18.830 -
18.831 -val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
18.832 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.833 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.834 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.835 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.836 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.837 -(*----------- 30 -----------*)
18.838 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.839 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.840 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.841 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.842 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.843 -(*----------- 40 -----------*)
18.844 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.845 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.846 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.847 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.848 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.849 -(*----------- 50 -----------*)
18.850 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.851 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.852 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.853 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.854 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.855 -(*----------- 60 -----------*)
18.856 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.857 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.858 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.859 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.860 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.861 -(*----------- 70 -----------*)
18.862 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.863 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.864 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.865 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.866 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.867 -(*----------- 80 -----------*)
18.868 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.869 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.870 -\<close> ML \<open>
18.871 -(**)val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.872 -\<close> ML \<open>
18.873 -(*CURRENT*)if p = ([2, 1], Pbl) andalso
18.874 -(*CURRENT*) f = PpcKF (Problem [], {Find = [Incompl "equality"], Given = [Incompl "functionEq", Incompl "substitution"], Relate = [], Where = [], With = []})
18.875 -(*CURRENT*)then
18.876 -(*CURRENT*) case nxt of
18.877 -(*CURRENT*) ("Add_Given", Add_Given "functionEq (hd [])") => ((*here is an error in partial_function*))
18.878 -(*CURRENT*) | _ => error "me biegelinie changed 1"
18.879 -(*CURRENT*)else error "me biegelinie changed 2";
18.880 -\<close> ML \<open>
18.881 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.882 -(*CURRENT*)nxt;(* = ("Tac ", Tac "[error] appl_add: is_known: seek_oridts: input ('substitution (NTH (1 + -4) [])') not found in oris (typed)")*)
18.883 -\<close> ML \<open>
18.884 -(*----- due to "switch from Script to partial_function" 4035ec339062 ?
18.885 - OR ?due to "failed trial to generalise handling of meths which extend the model of a probl " 98298342fb6d
18.886 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.887 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.888 -(*----------- 90 -----------*)
18.889 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.890 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.891 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.892 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.893 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.894 -(*---------- 100 -----------*)
18.895 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.896 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.897 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.898 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.899 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.900 -(*---------- 110 -----------*)
18.901 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.902 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.903 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.904 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.905 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.906 -(*---------- 120 -----------*)
18.907 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.908 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.909 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.910 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.911 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.912 -(*---------- 130 -----------*)
18.913 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.914 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.915 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.916 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.917 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.918 -
18.919 -if p = ([3], Pbl)
18.920 -then
18.921 - case nxt of
18.922 - ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") =>
18.923 - (case f of
18.924 - PpcKF
18.925 - (Problem [],
18.926 - {Find = [Incompl "solution []"], Given =
18.927 - [Correct
18.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]",
18.929 - Incompl "solveForVars [c]"],
18.930 - Relate = [], Where = [], With = []}) => ()
18.931 - | _ => error "Bsp.7.70 me changed 1")
18.932 - | _ => error "Bsp.7.70 me changed 2"
18.933 -else error "Bsp.7.70 me changed 3";
18.934 ------*)
18.935 -(* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
18.936 -
18.937 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
18.938 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
18.939 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---";
18.940 -(* the error in this test might be independent from introduction of y, dy
18.941 - as arguments in IntegrierenUndKonstanteBestimmen2,
18.942 - rather due to so far untested use of "auto" *)
18.943 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
18.944 - "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
18.945 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
18.946 - "AbleitungBiegelinie dy"];
18.947 -val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
18.948 - ["IntegrierenUndKonstanteBestimmen2"]);
18.949 -
18.950 -reset_states ();
18.951 -CalcTree [(fmz, (dI',pI',mI'))];
18.952 -Iterator 1;
18.953 -moveActiveRoot 1;
18.954 -
18.955 -(*[], Met*)autoCalculate 1 CompleteCalcHead;
18.956 -(*[1], Pbl*)autoCalculate 1 (Step 1); (* into SubProblem *)
18.957 -(*[1], Res*)autoCalculate 1 CompleteSubpbl; (**)
18.958 -(*[2], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
18.959 -(*[2], Res*)autoCalculate 1 CompleteSubpbl;
18.960 -(*[3], Pbl*)autoCalculate 1 (Step 1); (* out of SubProblem *)
18.961 -(*[3], Met*)autoCalculate 1 CompleteCalcHead;
18.962 -(*[3, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.963 -(*(**)autoCalculate 1 CompleteSubpbl; error in kernel 4: generate1: not impl.for Empty_Tac_*)
18.964 -(*[3, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.965 -(*[3, 2], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.966 -(*[3, 3], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.967 -(*[3, 4], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.968 -(*[3, 5], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.969 -(*[3, 6], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.970 -(*[3, 7], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.971 -(*[3, 8], Pbl*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.972 -(*[3, 8], Met*)autoCalculate 1 CompleteCalcHead;
18.973 -(*[3, 8, 1], Frm*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.974 -(*[3, 8, 1], Res*)autoCalculate 1 (Step 1); (* solve SubProblem *)
18.975 -(*(**)autoCalculate 1 (Step 1);
18.976 -*** generate1: not impl.for Empty_Tac_
18.977 -val it = <AUTOCALC><CALCID>1</CALCID><CALCMESSAGE>helpless</CALCMESSAGE></AUTOCALC>: XML.tree *)
18.978 -
18.979 -val ((pt,_),_) = get_calc 1;
18.980 -val ip = get_pos 1 1;
18.981 -val (Form f, tac, asms) = pt_extract (pt, ip);
18.982 -
18.983 -if ip = ([2, 1, 1], Frm) andalso
18.984 -term2str f = "hd []"
18.985 -then
18.986 - case tac of
18.987 - SOME Empty_Tac => ()
18.988 - | _ => error "ERROR biegel.7.70 changed 1"
18.989 -else error "ERROR biegel.7.70 changed 2";
18.990 -
18.991 -(*----- this state has been reached shortly after 98298342fb6d:
18.992 -if ip = ([3, 8, 1], Res) andalso
18.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]"
18.994 -then
18.995 - case tac of
18.996 - SOME (Check_Postcond ["normalise", "4x4", "LINEAR", "system"]) => ()
18.997 - | _ => error "ERROR biegel.7.70 changed 1"
18.998 -else error "ERROR biegel.7.70 changed 2";
18.999 -*)
18.1000 \<close> ML \<open>
18.1001 \<close> ML \<open>
18.1002 "~~~~~ fun xxx , args:"; val () = ();