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>
28 \item Error_Pattern.check_error_pattern -> Error_Pattern.check
30 \item DEL double code: lev_on +??? in ctree-basic.sml + position
32 \item DEL double code: nxt_specify_init_calc IN specify.sml + step-specify.sml
34 \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge
36 \item replace ContextC.insert_assumptions by Tactic.insert_assumptions
37 NOTE: DONE in associate, ??missing in LI.do_step ??
39 \item associate: drop ctxt from arg.+ return
41 \item in check_leaf SEPARATE tracing
42 collect all trace_script --> Trace_LI
43 trace_script: replace ' by " in writeln
47 \item NotAss -> Not_Associated | Ass -> Associated
48 \item ContextC.from_subpbl_to_caller -> subpbl_to_caller
49 \item Tactic.is_empty_tac -> Tactic.is_empty
50 \item Istate.istate2str -> Istate.string_of
52 \item rename Base_Tool.thy <--- Base_Tools
53 \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc
55 \item rename field scr in meth
60 \item relocations + renamings
62 \item Rule.terms2str -> TermC.s_to_string
63 Tactic_Def.tac2str -> Tactic_Def.input_to_string
70 \item cleanup test-files
72 \item test/.. tools.sml, atools.sml, ...
79 \item see in Test_Some/300- (*TODO: DOUBLE subst, DROP ONE*)
80 \item ? improve sig. eval_leaf E a v t -> (E, (a, v)) t
83 \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}
84 there it is Free ("Subproblem", "char list \<times> ..
85 instead of Const (|???.Subproblem", "char list \<times> ..
86 AND THE STRING REPRESENTATION IS STRANGE:
88 ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation''
92 term2str; (*defined by..*)
93 fun term_to_string''' thy t =
95 val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)
96 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
98 val t = @{term "aaa + bbb"}
99 val t = @{term "Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation''])"};
101 val sss = Print_Mode.setmp [] (Syntax.string_of_term @{context}) t
103 writeln sss (*.. here perfect: Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation'']) *)
108 \item LI.locate_input_term cleanup, case ONLY
110 \item revert 9ef6e9e88178 (separate Tactic / Tactic_Def),
111 because tactic.sml after ctree.sml doesn't gain much !
112 ?Tactic.input -> Calc.tactic ?
115 \item collect from_pblobj_or_detail*,
116 -> Rule.rls(*..\<in> ist \<rightarrow> REMOVE*) * (Istate.T * Proof.context) * Program.T
117 \item init_istate ?-> Detail_Rls?
119 \item rename Ctree.pos' --> Pos.pos', type decl duplicate? delete, separate!
121 \item Istate_Def.e_istate -> Istate.empty
125 \item distribute test/../scrtools.sml: WAIT FOR FINAL CLEANUP OF src/../Interpret
130 subsection \<open>Postponed from current changeset\<close>
135 \item cleanup fun me:
136 fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
137 | me*) (_, tac) p _(*NEW remove*) pt =
138 + -------------------------^^^^^^
139 # see test-code.sml fun me_trace
140 use this also for me, not only for me_ist_ctxt; del. me
141 this requires much updating in all test/*
144 \item generate, generate1: NO thy as arg.
145 Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec
147 \item shift tests into NEW model.sml (upd, upds_envv, ..)
150 \item clarify handling of contexts ctxt ContextC
153 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
155 \item Check_Elementwise "Assumptions": prerequisite for ^^goal
156 rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl
157 rm Assumptions :: bool (* TODO: remove with making ^^^ idle *)
160 \item remove ctxt from Tactic.T; this makes use of ctxt more explicit (e.g. in LI)
162 \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt
163 \item rm ctxt from Subproblem' (is separated in associate!))
165 \item check Tactic.Subproblem': are 2 terms required?
167 \item Test_Some.--- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts --
168 --: wait for deleting Check_Elementwise Assumptions
170 \item lucas-intrpreter.scan_dn1: Generate.generate1 (Celem.assoc_thy "Isac_Knowledge")
174 \item complete mstools.sml (* survey on handling contexts:
179 \item librarys.ml --> libraryC.sml + text from termC.sml
186 \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions
187 DONE for find_next_step by Tactic.insert_assumptions m' ctxt
189 \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)
190 \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))
191 \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"
194 \item DO DELETIONS AFTER analogous concentrations in find_next_step
197 \item ? what is the difference headline <--> cascmd in
198 Subproblem' (spec, oris, headline, fmz_, context, cascmd)
200 \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr
202 \item unify/clarify stac2tac_ |
205 \item extract common code from associate.. stac2tac_xxx
206 \item rename LItool.tac_from_prog -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,
211 \item unify in signature LANGUAGE_TOOLS =\\
212 val pblterm: Rule.domID -> Celem.pblID -> term vvv vvv\\
213 val subpbl: string -> string list -> term unify with ^^^
215 \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?
216 Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.
217 If Telem.safe is kept, consider merge with CTbasic.ostate
219 \item remove find_next_step from solve Apply_Method';
220 this enforces Pos.at_first_tactic, which should be dropped, too.
226 subsection \<open>Postponed -?-> separated task ?\<close>
231 \item replace all Ctree.update_* with Ctree.cupdate_problem
233 \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})
235 \item exception PROG analogous to TERM
237 \item sig/struc ..elems --> ..elem
239 \item distille CAS-command, CAScmd, etc into a struct
241 \item check location of files:
242 test/Tools/isac/Interpret/ptyps.thy
243 test/Tools/isac/Specify.ptyps.sml
245 \item check occurences of Atools in src/ test/
246 \item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _)
250 \item Diff.thy: differentiateX --> differentiate after removal of script-constant
251 \item Test.thy: met_test_sqrt2: deleted?!
253 \item Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx, too*)
255 \item automatically extrac rls from program-code
256 ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?
258 \item finish output of trace_script with Check_Postcond (useful for SubProblem)
270 section \<open>Separated tasks\<close>
272 This section shall be removed, because
273 the distinction \<open>Simple\<close> | \<open>Simple but laborous\<close> | \<open>Questionable\<close>
274 is too distracting when working on \<open>TODOs from current changesets\<close>.
277 section \<open>Major reforms\<close>
280 subsection \<open>Exception Size raised\<close>
282 During update Isabelle2018 --> Isabelle2019 we noticed, that
283 "isabelle build" uses resources more efficiently than "isabelle jedit".
284 The former works, but the latter causes
286 \item "Exception- Size raised"
288 \item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"
289 in test/../biegelinie-*.xml.
291 This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".
293 Find tools to investigate the Exception, and find ways around it eventually.
295 subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>
298 \item there are comments in several signatures
299 \item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted
300 \item src/../Frontend/: signatures missing
304 subsection \<open>overall structure of code\<close>
307 \item try to separate Isac_Knowledge from MathEngine
308 common base: Knowledge_Author / ..??
310 \item ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)
316 subsection \<open>Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/\<close>
321 \item re-organise code for Interpret
323 \item Step*: Step_Specify | Step_Solve | Step
325 \item *.check | *.add ARE TOO LATE IN BUILD with Step_Specify | Step_Solve
326 Specify_Step.check | Specify_Step.add <-- Applicable.applicable_in
327 Solve_Step.check | Solve_Step.add <-- Generate.generate1
331 \item Prog_Tac: fun get_first takes both Prog_Tac + Program --- wait for separate Tactical
332 then shift into common descendant
337 \item ??????????? WHY CAN LI.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????
342 subsection \<open>Review modelling- + specification-phase\<close>
348 \item check match between args of partial_function and model-pattern of meth;
349 provide error message.
351 \item "--- hack for funpack: generalise handling of meths which extend problem items ---"
353 \item see several locations of hack in code
354 \item these locations are NOT sufficient, see
355 test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---
356 \item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,
357 this would be according to survey Notes (3) in src/../calchead.sml.
359 \item see "failed trial to generalise handling of meths"98298342fb6d
360 \item abstract specify + nxt_specif to common aux-funs;
361 see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"
363 \item type model = itm list ?
364 \item review survey Notes in src/../calchead.sml: they are questionable
365 \item review copy-named, probably two issues commingled
367 \item special handling of "#Find#, because it is not a formal argument of partial_function
368 \item special naming for solutions of equation solving: x_1, x_2, ...
371 \item structure Tactic Specify -?-> Proglang (would require Model., Selem.)
373 \item this has been written in one go:
375 \item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]
376 \item reconsider add_field': where is it used for what? Shift into mk_oris
377 \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???
378 \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey
379 \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_
380 (relevant for pre-condition)
381 \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth
386 subsection \<open>taci list, type step\<close>
388 taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,
389 and probably, because the Kernel interface separated setNextTactic and applyTactic.
390 Both are no good reasons to make code more complicated.
392 !!! taci list is used in do_next !!!
396 \item can lev_on_total replace lev_on ? ..Test_Isac_Short + rename lev_on_total -> lev_on
398 \item Step* functions should return Calc.T instead of Chead.calcstate'
400 \item states.sml: check, when "length tacis > 1"
401 \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml
402 \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?
404 \item brute force setting all empty ([], [], ptp) works!?! but ptp causes errors -- investigate!
408 subsection \<open>Ctree\<close>
411 # mixture pos' .. pos in cappend_*, append_* is confusing
412 # existpt p pt andalso Tactic.is_empty_tac DIFFERENT IN append_*, cappend_* is confusing
413 "exception PTREE "get_obj: pos =" ^^^^^: ^^^^ due to cut !!!
414 NOTE: exn IN if..andalso.. IS NOT!!! DETECTED, THIS is confusing
415 see test/../--- Minisubpbl/800-append-on-Frm.sml ---
416 # ?!? "cut branches below cannot be decided here" in append_atomic
417 # sign. of functions too different ?!?canonical arg.order ?!?
420 \item remove update_branch, update_*? -- make branch, etc args of append_*
422 \item close sig Ctree, contains cappend_* ?only? --- ?make parallel to ?Pide_Store?
424 \item unify args to Ctree.state (pt, p)
426 /----- ad design upd/get_ist/ctxt 1 ------------------------------------------------------------\
427 store ist+ctxt independent from Tactic.T according to LI, which handles ist+ctxt EXPLICITLY
428 # STATUS QUO WITH insert_pt NEW OBJECTS IN Ctree:
429 | generate1 _ (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, _) pt =
430 fun cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Complete
431 val pt = append_atomic p (Istate_Def.e_istate, ContextC.e_ctxt) f r f' s pt
432 val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
433 fun append_atomic p l f r f' s pt =
436 if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
437 then (*after Take*) ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
438 else ((NONE, SOME l), f)
440 insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = iss, branch = NoBranch,
441 result = f', ostate = s}) pt p
443 # Separation makes sense, because ist+ctxt is contained in each PrfObj+PblObj,
444 while Tactic.T is contained only in PrfObj.
445 Separating ist+ctxt relieves Tactic.T from fields, which must be set empty and filled later.
447 DONE@ /// (pt, (p, p_))
448 DONE | generate1 _ (Tactic.Rewrite' (_, _, _, _, thm', f, (f', asm))) (is, ctxt) (p, p_) pt =
449 DONE fun cappend_atomic pt p (is, ctxt) f (Tactic.Rewrite thm') (f', asm) Complete
451 val pt = append_atomic p (Istate_Def.e_istate, ContextC.e_ctxt) f r f' s pt
452 @////// val pt = update_loc' pt p (SOME ist_form, SOME ist_res)
453 fun append_atomic p l f r f' s pt =
456 if existpt p pt andalso Tactic.is_empty_tac (get_obj g_tac pt p)
457 then (*after Take*) ((fst (get_obj g_loc pt p), SOME l), get_obj g_form pt p)
458 else ((NONE, SOME l), f)
460 insert_pt (PrfObj {cell = NONE, form = f, tac = r, loc = ist_ctxt, branch = NoBranch,
461 result = f', ostate = s}) pt p
463 @ ANALOGOUS IN fun append_result, ..??
464 \----- ad design upd/get_ist/ctxt 1 ------------------------------------------------------------/
466 \item newest: upd_istate_LI, upd_ctxt_LI, get_istate_LI, get_ctxt
467 \item review get_ctxt, update_ctxt, get_istate_LI, upd_istate_LI, upd_ctxt_LI, update_loc', repl_loc
469 /----- ad design upd/get_ist/ctxt 2 ------------------------------------------------------------\
470 DESIGN NOTE ASSUMING SEPARATION OF ist+ctxt FROM tactic, SEE ABOVE:
471 upd/get_ist/ctxt can be decided by pos ONLY for Res,
472 so decision NOT by pos, but by DIFFERENT calls *_LI/specify:
473 *_LI : select for Res | (Frm, Pbl) by fst | snd from (SOME (ist, ctxt), (SOME (ist, ctxt))
474 *_specify: select ist | ctxt by fst | snd from SOME (ist, ctxt)
475 \----- ad design upd/get_ist/ctxt 2 ------------------------------------------------------------/
476 # retrieve ctxt: IS CONFUSED
477 1a.fun get_ctxt NEW or {ctxt, ...}
478 1b.fun get_ctxt_LI .. get_loc NEW analogous upd_ctxt_LI (if Res)
479 2a.fun get_istate_LI NEW or {istate, ...}
480 2b.fun get_istate_XX .. get_loc OK
482 # update ctxt: IS CORRECT, BUT REPEATED if
484 \fun upd_istate_ctxt_LI .. update_loc'..Res | else
485 \fun upd_ctxt_LI .. update_loc'..Res | else
486 \fun upd_istate_LI .. update_loc'..Res | else
487 fun update_ctxt .. repl_ctxt
488 fun update_env .. repl_env \<rightarrow>update_istate
496 subsection \<open>replace theory/thy by context/ctxt\<close>
500 \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt
501 special case: Tactic.Refine_Problem
503 \item theory can be retrieved from ctxt by Proof_Context.theory_of
505 \item cleaup the many conversions string -- theory
506 \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?
507 \item 1. Rewrite.eval_true_, then
508 LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.tac_from_prog.
510 let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)
513 \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr .use Term.exists_Const
514 \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)
515 \item push srls into pstate
516 \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls)
521 subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>
523 remove Rfuns -> Rule.Prog, Rule.EmptyScr
524 consider separating spec.funs. to ?Inter_Steps?
526 \item removing from_pblobj_or_detail' causes many strange errors
527 \item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ...
529 \item probably only "normal_form" seems to be needed
530 \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"
531 but that seems desirable
532 \item ?how is the relation to reverse-rewriting ???
533 \item "Rfuns" markers in test/../rational
535 \item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond
536 rewriting and/or respective intermediate steps (e.g. cancellation of fractions).
537 Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.
538 Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.
539 \item debug ^^^ related: is there an occurence of Steps with more than 1 element?
541 \item and do_next (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)
543 \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?
546 subsection \<open>Inverse_Z_Transform.thy\<close>
549 \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.
550 ? replace rewriting with substitution ?!?
551 The problem is related to the decision of typing for "d_d" and making bound variables free (while
552 shifting specific handling in equation solving etc. to the meta-logic).
553 \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by
554 rewrite-rules; see \ref{new-var-rhs}.
555 \item Reconsider whole problem:
556 input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?
559 subsection \<open>Adopt Isabelle's numerals for Isac\<close>
562 \item replace numerals of type "real" by "nat" in some specific functions from ListC.thy
563 and have both representations in parallel for "nat".
568 subsection \<open>Redesign equation solver\<close>
570 Existing solver is structured along the WRONG assumption,
571 that Poly.thy must be the LAST thy among all thys involved -- while the opposite is the case.
573 Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy
575 subsection \<open>Finetunig required for xmldata in kbase\<close>
577 See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390
578 and in kbase html-representation generated from these xmldata.
579 Notes in ~~/xmldata/TODO.txt.
582 section \<open>Hints for further development\<close>
585 subsection \<open>Coding standards & some explanations for math-authors\<close>
586 text \<open>copy from doc/math-eng.tex WN.28.3.03
587 WN071228 extended\<close>
589 subsubsection \<open>Identifiers\<close>
590 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does
591 not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds
592 reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the
593 problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.
594 However, all the cases (1)..(4) require different typing for one and the same
595 identifier {\tt probe} which is impossible, and actually leads to strange errors
596 (for instance (1) is used as string, except in a script addressing a Subproblem).
598 These are the preliminary rules for naming identifiers>
600 \item [elements of a key] into the hierarchy of problems or methods must not contain
601 capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.
602 \item [descriptions in problem-patterns] must contain at least 1 capital letter and
603 must not contain underscores, e.g. {\tt Probe, forPolynomials}.
604 \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus
605 beware of conflicts~!
606 \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.
610 %WN071228 extended\<close>
612 subsubsection \<open>Rule sets\<close>
613 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML
614 where it can be viewed using the knowledge browsers.
616 There are rulesets visible to the student, and there are rulesets visible (in general) only for
617 math authors. There are also rulesets which {\em must} exist for {\em each} theory;
618 these contain the identifier of the respective theory (including all capital letters)
619 as indicated by {\it Thy} below.
622 \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a
623 normalform for all terms which can be expressed by the definitions of the respective theory
624 (and the respective parents).
625 \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms
626 which can be expressed by the definitions of the respective theory (and the respective parents)
627 such, that the rewrites can be presented to the student.
628 \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with
629 numerical constants only (i.e. all terms which can be expressed by the definitions of
630 the respective theory and the respective parent theories). In particular, this ruleset includes
631 evaluating in/equalities with numerical constants only.
632 WN.3.7.03: may be dropped due to more generality: numericals and non-numericals
633 are logically equivalent, where the latter often add to the assumptions
634 (e.g. in Check_elementwise).
637 The above rulesets are all visible to the user, and also may be input;
638 thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,
639 KEStore_Elems.get_rlss). All these rulesets must undergo a preparation
640 using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.
641 The following rulesets are used for internal purposes and usually invisible to the (naive) user:
648 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO
651 subsection \<open>get proof-state\<close>
653 Re: [isabelle] Programatically get "this"
654 ----------------------------------------------------
655 So here is my (Makarius') version of your initial example, following these principles:
661 val ctxt = @{context};
664 Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN);
665 val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));
670 subsection \<open>write Specification to jEdit\<close>
672 Re: [isabelle] Printing terms with type annotations
673 ----------------------------------------------------
674 On 06/02/2019 17:52, Moa Johansson wrote:
676 > I’m writing some code that should create a snippet of Isar script.
678 This is how Sledgehammer approximates this:
680 http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299
682 (The module name already shows that the proper terminology is "Isar
683 proof" (or "Isar proof text"). Proof scripts are a thing from the past,
684 before Isar. You can emulate old-style proof scripts via a sequence of
685 'apply' commands, but this is improper Isar.)
687 Note that there is no standard function in Isabelle/Pure, because the
688 problem to print just the right amount of type information is very
689 complex and not fully solved. One day, after 1 or 2 rounds of
690 refinements over the above approach, it might become generally available.
692 subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>
694 isabelle update -u path_cartouches
695 isabelle update -u inner_syntax_cartouches
697 section \<open>Questions to Isabelle experts\<close>
700 \item what is the actual replacement of "hg log --follow" ?
702 \item how HANDLE these exceptions, e.g.:
703 Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"
706 Failed to parse term"
708 \item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"
709 e.g. in test/Interpret/lucas-interpreter.sml
715 section \<open>For copy & paste\<close>
733 subsection \<open>xxx\<close>
734 subsubsection \<open>xxx\<close>