1 (* Title: todo's for isac core
2 Author: Walther Neuper 111013
3 (c) copyright due to lincense terms.
6 imports "~~/src/Doc/Prog_Prove/LaTeXsugar"
10 Legend: here + code since 200120
11 \<open>(*DOC\<close> identifies stuff dedicated for isac/Doc/Lucas_Interpreter
12 \<open>(*?!?\<close> identifies a design question
14 Distillation of "rounds of reforms":
15 \<open>TODOs from current changesets\<close> \<rightarrow> \<open>Postponed from current changeset\<close> \<rightarrow>
16 (*to be removed..*) \<rightarrow> \<open>Separated tasks\<close> (*.. to be removed*)
17 \<rightarrow> subsection of \<open>Major reforms\<close>
20 section \<open>TODOs from current changesets\<close>
22 Shift more complicated issues from \<open>Current changeset\<close> to \<open>Postponed from current changeset\<close>
24 subsection \<open>Current changeset\<close>
26 (*/------- to from -------\*)
27 (*\------- to from -------/*)
31 \item Input_Descript.descriptor -> Input_Descript.T
33 \item Step_Specify.initialisePIDE: remove hdl in return-value
34 rename Step_Specify.nxt_specify_init_calc
36 \item relate Prog_Epxr.lhs to Thm.lhs_of
38 \item as soon as src/../parseC.sml is stable,
39 remove defs from Test_Parse_Isac.thy
40 + and shift tests from Test_Parse_Isac -> test/../parseC.sml
42 \item Specify.find_next_step: References.select
43 cpI = ["vonBelastungZu", "Biegelinien"]: References_Def.id
46 \item Calc.state_empty_post \<rightarrow> Calc.state_post_empty
48 \item distribute code from test/../calchead.sml
50 \item rename Tactic.Calculate -> Tactic.Evaluate
52 \item replace src/ Erls by Rule_Set.Empty
54 \item rename ptyps.sml -> specify-etc.sml
55 rename Specify -> Specify_Etc
56 rename Specify -> Specify
58 \item specific_from_prog in..end: replace o by |> (Test_Isac or Test_Some!)
60 \item cleanup ThmC in MathEngBasic
71 subsection \<open>Postponed from current changeset\<close>
75 \item make steps around SubProblem more consistent:
76 SubProblem (thy, [pbl]) is bypassed by Model_Problem, if it is 1st Tactic in a Program.
78 * the Tactic SubProblem (thy, [pbl]) creates the formula SubProblem (thy, [pbl])
80 * the Tactic Model_Problem starts Specification
82 see test/../sub-problem.sml
84 \item Specify_Step.add has dummy argument Istate_Def.Uistate -- remove down to Ctree
86 \item Step_Specify.by_tactic (Tactic.Model_Problem' (id, _, met))
87 by_tactic (Tactic.Specify_Theory' domID)
88 had very old, strange code at 11b5b8b81876
89 ?redes Model_Problem', Specify_Theory' <--> Specify_Method: Step_Specify.complet_for ?
90 INTERMED. NO REPAIR: NOT PROMPTED IN TESTS
92 \item unify code Specify.find_next_step <--> Step_Specify.by_tactic (Tactic.Specify_Method'
94 \item Isa20.implementation: 0.2.4 Printing ML values ?INSTEAD? *.TO_STRING ???
95 ??? writeln ( make_string {x = x, y = y}); ???
97 \item revise O_Model and I_Model with an example with more than 1 variant.
99 \item ctxt is superfluous in specify-phase due to type constraints from Input_Descript.thy
101 \item Derive.do_one: TODO find code in common with complete_solve
102 Derive.embed: TODO rewrite according to CAO (+ no intermediate access to Ctree)
104 \item Solve_Check: postponed parsing input to _ option
106 \item ? "fetch-tactics.sml" from Mathengine -> BridgeLibisabelle ?
108 \item ? unify struct.Step and struct.Solve in MathEngine ?
110 \item use "Eval_Def" for renaming identifiers
112 \item why does Test_Build_Thydata.thy depend on ProgLang and not on CalcElements ?
116 \item LI.do_next (*TODO RM..*) ???
117 \item generate.sml: RM datatype edit TOGETHER WITH datatype inout
118 \item TermC.list2isalist: typ -> term list -> term .. should NOT requires typ
119 \item get_ctxt_LI should replace get_ctxt
120 \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
121 \item rename Base_Tool.thy <--- Base_Tools
122 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
123 \item rename field scr in meth
131 \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}
132 there it is Free ("Subproblem", "char list \<times> ..
133 instead of Const (|???.Subproblem", "char list \<times> ..
134 AND THE STRING REPRESENTATION IS STRANGE:
135 Subproblem (''Test'',
136 ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation''
140 term2str; (*defined by..*)
141 fun term_to_string''' thy t =
143 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
144 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
146 val t = @{term "aaa + bbb"}
147 val t = @{term "Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation''])"};
149 val sss = Print_Mode.setmp [] (Syntax.string_of_term @{context}) t
151 writeln sss (*.. here perfect: Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation'']) *)
156 \item cleanup fun me:
157 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
158 | me*) (_, tac) p _(*NEW remove*) pt =
159 + -------------------------^^^^^^
160 # see test-code.sml fun me_trace
161 use this also for me, not only for me_ist_ctxt; del. me
162 this requires much updating in all test/*
164 \item shift tests into NEW model.sml (upd, upds_envv, ..)
166 \item clarify handling of contexts ctxt ContextC
169 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
171 \item Check_Elementwise "Assumptions": prerequisite for ^^goal
172 rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
173 rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
179 \item complete mstools.sml (* survey on handling contexts:
184 \item librarys.ml --> libraryC.sml + text from termC.sml
191 \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
192 DONE for find_next_step by Tactic.insert_assumptions m' ctxt
194 \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
195 \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
198 \item DO DELETIONS AFTER analogous concentrations in find_next_step
201 \item ? what is the difference headline <--> cascmd in
202 Subproblem' (spec, oris, headline, fmz_, context, cascmd)
203 \item Substitute' what does "re-calculation mean in the datatype comment?
205 \item inform: TermC.parse (ThyC.get_theory "Isac_Knowledge") istr --> parseNEW context istr
207 \item unify/clarify stac2tac_ |
210 \item extract common code from associate.. stac2tac_xxx
211 \item rename LItool.tac_from_prog -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,
216 \item unify in signature LANGUAGE_TOOLS =\\
217 val pblterm: ThyC.id -> Problem.id -> term vvv vvv\\
218 val subpbl: string -> string list -> term unify with ^^^
220 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
221 Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
222 If Telem.safe is kept, consider merge with CTbasic.ostate
224 \item remove find_next_step from solve Apply_Method';
225 this enforces Pos.at_first_tactic, which should be dropped, too.
231 subsection \<open>Postponed --> Major reforms\<close>
236 \item make parser mutually recursive for Problem .. Solution
237 preps. in Test_Parse_Isac:
239 subsubsection "problem_mini" shows a principal issue with recursive parsing
240 probably due to !2! arguments of parser (as shown in Cookbook)
241 Test_Parsers_Cookbook:
242 (* recursive parser p.140 \<section>6.1 adapted to tokens: *) shows differences,
243 which might help understanding the principal issue
244 see also Test_Parsers subsection "recursive parsing"
248 \item revisit bootstrap Calcelements. rule->calcelems->termC
249 would be nice, but is hard: UnparseC.terms -> TermC.s_to_string
251 \item replace all Ctree.update_* with Ctree.cupdate_problem
253 \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
255 \item exception PROG analogous to TERM
257 \item sig/struc ..elems --> ..elem
259 \item distille CAS-command, CAScmd, etc into a struct
261 \item check location of files:
262 test/Tools/isac/Interpret/ptyps.thy
263 test/Tools/isac/Specify.ptyps.sml
265 \item check occurences of Atools in src/ test/
266 \item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _)
270 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
271 \item Test.thy: met_test_sqrt2: deleted?!
273 \item Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (*<<<---- use Know_Store.xxx, too*)
275 \item automatically extrac rls from program-code
276 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
278 \item finish output of LItool.trace with Check_Postcond (useful for SubProblem)
280 \item replace Rule_Set.empty by Rule_Set.Empty
281 latter is more clear, but replacing ***breaks rewriting over all examples***,
282 e.g. see ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x'
283 in Minisubplb/200-start-method-NEXT_STEP.sml:
284 (*+* )------- in f3cac3053e7b (Rule_Set.empty just renamed, NOT deleted) we had
286 (*+*) Rls {calc = [], erls = Erls, errpatts = [], id = "empty", preconds = [], rew_ord =
287 (*+*) ("dummy_ord", fn), rules = [], scr = Empty_Prog, srls = Erls}:
288 (*+*).. THIS IS Rule_Set.empty, BUT IT DID not CAUSE ANY ERROR !
289 (*+*)------- WITH Rule_Set.empty REMOVED (based on f3cac3053e7b) we had
290 (*+*)val Empty = prls (* <---ERROR: rewrite__set_ called with 'Erls' for 'precond_rootpbl x' *)
291 ( *+*)val ["sqroot-test", "univariate", "equation", "test"] = cpI
292 THAT INDICATES, that much rewriting/evaluating JUST WORKED BY CHANCE?!?
303 section \<open>Major reforms\<close>
306 subsection \<open>Exception Size raised\<close>
308 During update Isabelle2018 --> Isabelle2019 we noticed, that
309 "isabelle build" uses resources more efficiently than "isabelle jedit".
310 The former works, but the latter causes
312 \item "Exception- Size raised"
314 \item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
315 in test/../biegelinie-*.xml.
317 This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
319 Find tools to investigate the Exception, and find ways around it eventually.
321 subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
324 \item there are comments in several signatures
325 \item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted
326 \item src/../Frontend/: signatures missing
330 subsection \<open>overall structure of code\<close>
333 \item try to separate Isac_Knowledge from MathEngine
334 common base: Knowledge_Author / ..??
336 \item ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)
342 subsection \<open>Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/\<close>
347 \item re-organise code for Interpret
349 \item Step*: Step_Specify | Step_Solve | Step DONE
351 \item Prog_Tac: fun get_first_argument takes both Prog_Tac + Program --- wait for separate Tactical
352 then shift into common descendant
357 \item ??????????? WHY CAN LI.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
362 subsection \<open>Review modelling- + specification-phase\<close>
368 \item check match between args of partial_function and model-pattern of meth;
369 provide error message.
371 \item "--- hack for funpack: generalise handling of meths which extend problem items ---"
373 \item see several locations of hack in code
374 \item these locations are NOT sufficient, see
375 test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
376 \item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,
377 this would be according to survey Notes (3) in src/../calchead.sml.
379 \item see "failed trial to generalise handling of meths"98298342fb6d
380 \item abstract specify + nxt_specif to common aux-funs;
381 see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
383 \item type model = itm list ?
384 \item review survey Notes in src/../calchead.sml: they are questionable
385 \item review copy-named, probably two issues commingled
387 \item special handling of "#Find#, because it is not a formal argument of partial_function
388 \item special naming for solutions of equation solving: x_1, x_2, ...
392 \item this has been written in one go:
394 \item reconsidering I_Model.max_vt, use problem with meth ["DiffApp", "max_by_calculus"]
395 \item reconsider add_field': where is it used for what? Shift into mk_oris
396 \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
397 \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
398 \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
399 (relevant for pre-condition)
400 \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
405 subsection \<open>taci list, type step\<close>
407 taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
408 and probably, because the Kernel interface separated setNextTactic and applyTactic.
409 Both are no good reasons to make code more complicated.
411 !!! taci list is used in do_next !!!
415 \item can lev_on_total replace lev_on ? ..Test_Isac_Short + rename lev_on_total -> lev_on
417 \item Step* functions should return Calc.T instead of Calc.state_post
419 \item states.sml: check, when "length tacis > 1"
420 \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
421 \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
423 \item brute force setting all empty ([], [], ptp) works!?! but ptp causes errors -- investigate!
427 subsection \<open>Ctree\<close>
430 # mixture pos' .. pos in cappend_*, append_* is confusing
431 # existpt p pt andalso Tactic.is_empty DIFFERENT IN append_*, cappend_* is confusing
432 "exception PTREE "get_obj: pos =" ^^^^^: ^^^^ due to cut !!!
433 NOTE: exn IN if..andalso.. IS NOT!!! DETECTED, THIS is confusing
434 see test/../--- Minisubpbl/800-append-on-Frm.sml ---
435 # ?!? "cut branches below cannot be decided here" in append_atomic
436 # sign. of functions too different ?!?canonical arg.order ?!?
439 \item remove update_branch, update_*? -- make branch, etc args of append_*
441 \item close sig Ctree, contains cappend_* ?only? --- ?make parallel to ?Pide_Store?
443 \item unify args to Ctree.state (pt, p)
444 \item fun update_env .. repl_env \<rightarrow>updatempty
451 subsection \<open>replace theory/thy by context/ctxt\<close>
455 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
456 special case: Tactic.Refine_Problem
458 \item theory can be retrieved from ctxt by Proof_Context.theory_of
460 \item cleaup the many conversions string -- theory
461 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
462 \item 1. Rewrite.eval_true_, then
463 LItool.check_leaf, Rewrite.eval_prog_expr, Step.add, LItool.tac_from_prog.
465 let val thy = ThyC.get_theory "Isac_Knowledge";(*TODO*)
468 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
469 \item push srls into pstate
470 \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule_Set.Empty)
475 subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
477 remove refactor Rfuns, Rule.Prog, Rule.Empty_Prog, RrlsState: this is a concept never brought to work.
478 Clarify relation to reverse rewriting!
480 \item separate mut.recursion program with rule and rls by deleting fild scr in rls
481 (possible since CS 43160c1e775a
482 ` "replace Prog. in prep_rls by Auto_Prog.gen, which generates Prog. on the fly" )
484 \item probably only "normal_form" seems to be needed
485 \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
486 but that seems desirable
487 \item ?how is the relation to reverse-rewriting ???
488 \item "Rfuns" markers in test/../rational
490 \item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
491 rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
492 Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
493 Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
494 \item debug ^^^ related: is there an occurence of Steps with more than 1 element?
496 \item and do_next (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
498 \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
500 \item ?finally Prog could go from Calcelems to ProgLang?
503 subsection \<open>Inverse_Z_Transform.thy\<close>
506 \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
507 ? replace rewriting with substitution ?!?
508 The problem is related to the decision of typing for "d_d" and making bound variables free (while
509 shifting specific handling in equation solving etc. to the meta-logic).
510 \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
511 rewrite-rules; see \ref{new-var-rhs}.
512 \item Reconsider whole problem:
513 input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
516 subsection \<open>Adopt Isabelle's numerals for Isac\<close>
519 \item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
520 and have both representations in parallel for "nat".
525 subsection \<open>Redesign equation solver\<close>
527 Existing solver is structured along the WRONG assumption,
528 that Poly.thy must be the LAST thy among all thys involved -- while the opposite is the case.
530 Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
532 subsection \<open>Finetunig required for xmldata in kbase\<close>
534 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
535 and in kbase html-representation generated from these xmldata.
536 Notes in ~~/xmldata/TODO.txt.
539 section \<open>Hints for further development\<close>
542 subsection \<open>Coding standards & some explanations for math-authors\<close>
543 text \<open>copy from doc/math-eng.tex WN.28.3.03
544 WN071228 extended\<close>
546 subsubsection \<open>Identifiers\<close>
547 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
548 not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
549 reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
550 problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
551 However, all the cases (1)..(4) require different typing for one and the same
552 identifier {\tt probe} which is impossible, and actually leads to strange errors
553 (for instance (1) is used as string, except in a script addressing a Subproblem).
555 These are the preliminary rules for naming identifiers>
557 \item [elements of a key] into the hierarchy of problems or methods must not contain
558 capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
559 \item [descriptions in problem-patterns] must contain at least 1 capital letter and
560 must not contain underscores, e.g. {\tt Probe, forPolynomials}.
561 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
562 beware of conflicts~!
563 \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
567 %WN071228 extended\<close>
569 subsubsection \<open>Rule sets\<close>
570 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
571 where it can be viewed using the knowledge browsers.
573 There are rulesets visible to the student, and there are rulesets visible (in general) only for
574 math authors. There are also rulesets which {\em must} exist for {\em each} theory;
575 these contain the identifier of the respective theory (including all capital letters)
576 as indicated by {\it Thy} below.
579 \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
580 normalform for all terms which can be expressed by the definitions of the respective theory
581 (and the respective parents).
582 \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
583 which can be expressed by the definitions of the respective theory (and the respective parents)
584 such, that the rewrites can be presented to the student.
585 \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
586 numerical constants only (i.e. all terms which can be expressed by the definitions of
587 the respective theory and the respective parent theories). In particular, this ruleset includes
588 evaluating in/equalities with numerical constants only.
589 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
590 are logically equivalent, where the latter often add to the assumptions
591 (e.g. in Check_elementwise).
594 The above rulesets are all visible to the user, and also may be input;
595 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
596 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
597 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
598 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
605 {\tt Rule_Set.append_rules, Rule_Set.merge, remove_rls} TODO
608 subsection \<open>get proof-state\<close>
610 Re: [isabelle] Programatically get "this"
611 ----------------------------------------------------
612 So here is my (Makarius') version of your initial example, following these principles:
618 val ctxt = @{context};
621 Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN);
622 val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
627 subsection \<open>write Specification to jEdit\<close>
629 Re: [isabelle] Printing terms with type annotations
630 ----------------------------------------------------
631 On 06/02/2019 17:52, Moa Johansson wrote:
633 > I’m writing some code that should create a snippet of Isar script.
635 This is how Sledgehammer approximates this:
637 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
639 (The module name already shows that the proper terminology is "Isar
640 proof" (or "Isar proof text"). Proof scripts are a thing from the past,
641 before Isar. You can emulate old-style proof scripts via a sequence of
642 'apply' commands, but this is improper Isar.)
644 Note that there is no standard function in Isabelle/Pure, because the
645 problem to print just the right amount of type information is very
646 complex and not fully solved. One day, after 1 or 2 rounds of
647 refinements over the above approach, it might become generally available.
649 subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
651 isabelle update -u path_cartouches
652 isabelle update -u inner_syntax_cartouches
654 section \<open>Questions to Isabelle experts\<close>
657 \item ad ERROR Undefined fact "all_left" in Test_Isac: error-pattern.sml
658 Undefined fact: "xfoldr_Nil" inssort.sml
659 (* probably two different reasons:
661 (*WN0509 compare PolyEq.all_left "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)"*)
662 all_left: "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)" and
665 (*WN0509 compare LinEq.all_left "[|Not(b=!=0)|] ==> (a=b) = (a+(-1)*b=0)"*)
666 all_left: "[|Not(b=!=0)|] ==> (a = b) = (a - b = 0)" and
668 test/../partial_fractions.sml
669 (*[7], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
670 (*[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)"))*)
672 test/../mathengine-stateless.sml
673 (*if ThmC.string_of_thm @ {thm rnorm_equation_add} = "\<not> ?b =!= 0 \<Longrightarrow> (?a = ?b) = (?a + - 1 * ?b = 0)"
674 then () else error "string_of_thm changed";*)
676 (*---------------------------------------------------------------------------------------------*)
678 primrec xfoldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a xlist \<Rightarrow> 'b \<Rightarrow> 'b" where
679 xfoldr_Nil: "xfoldr f {|| ||} = id" |
680 xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
683 srls = Rule_Set.empty, calc = [], rules = [
684 Rule.Thm ("xfoldr_Nil",(*num_str*) @{thm xfoldr_Nil} (* foldr ?f [] = id *)),
688 \item ?OK Test_Isac_Short with
689 LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp
691 LI.by_tactic tac (Istate.empty, ContextC.empty) ptp
694 \item test from last CS with outcommented re-def of code ->
695 -> \<open>further tests additional to src/.. files\<close>
696 ADDTESTS/redefined-code.sml
698 \item efb749b79361 Test_Some_Short.thy has 2 errors, which disappear in thy ?!?:
699 ML_file "Interpret/error-pattern.sml" Undefined fact: "all_left"
700 ML_file "Knowledge/inssort.sml" Undefined fact: "xfoldr_Nil"
702 \item what is the actual replacement of "hg log --follow" ?
704 \item how HANDLE these exceptions, e.g.:
705 Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
708 Failed to parse term"
710 \item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"
711 e.g. in test/Interpret/lucas-interpreter.sml
717 section \<open>For copy & paste\<close>
735 subsection \<open>xxx\<close>
736 subsubsection \<open>xxx\<close>