(* Title:  todo's for isac core

    Author: Walther Neuper 111013

    (c) copyright due to lincense terms.

 *)

 theory TODO

 imports "~~/src/Doc/Prog_Prove/LaTeXsugar"

 begin

 text \<open>

 Legend: here + code since 200120

   \<open>(*DOC\<close> identifies stuff dedicated for isac/Doc/Lucas_Interpreter

   \<open>(*?!?\<close> identifies a design question

 Distillation of "rounds of reforms":

   \<open>TODOs from current changesets\<close> \<rightarrow> \<open>Postponed from current changeset\<close> \<rightarrow>

   (*to be removed..*) \<rightarrow> \<open>Separated tasks\<close> (*.. to be removed*)

   \<rightarrow> subsection of \<open>Major reforms\<close>

 \<close>

 section \<open>TODOs from current changesets\<close>

 text\<open>

   Shift more complicated issues from  \<open>Current changeset\<close> to \<open>Postponed from current changeset\<close>

 \<close>

 subsection \<open>Current changeset\<close>

 text \<open>

   \begin{itemize}

   \item xxx

   \item xxx

   \item LI.do_next (*TODO RM..*)

   \item xxx

   \item  RENAME ARGS ContextC.subpbl_to_caller sub_ctxt prog_res ctxt_parent

   \item xxx

   \item RM asm FROM Check_Postcond' (pI, (prog_res, asm)) ... asms are handled by ctxt !

   \item xxx

   \item generate.sml: RM datatype edit = EdUndef | Write | Protect

   \item xxx

   \item ad ERROR @unknown fact all_left in Test_Isac: search "Undefined"

     Undef -> Real_Undef

   \item xxx

   \item TermC.list2isalist: typ -> term list -> term  .. should NOT requires typ

   \item xxx

   \item restore clarity of  "trace_rewrite": "=====" seems to be lost:

     #####  try calc: HOL.eq'    <<<------------------------------- here the error comes from

     =====  calc. to: ~ False    <<<------------------------------- \<not> x = 0 is NOT False

     #####  try calc: HOL.eq' 

     #####  try thm: not_true 

     #####  try thm: not_false 

     =====  rewrites to: True    <<<------------------------------- so x \<noteq> 0 is NOT True

   \item xxx

   \item get_ctxt_LI should replace get_ctxt

   \item xxx

   \item change separate test ----------------------vvv

     | by_tactic (tac as Tactic.Check_Postcond' _) ptp =

     LI.by_tactic tac (Istate.e_istate, ContextC.e_ctxt) ptp

     -----------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

   \item xxx

   \item mv Ctree.get_assumptions_ -> Ctree.ctxt_assumptions

   \item xxx

   \item Error_Pattern.check_error_pattern -> Error_Pattern.check

   \item xxx

   \item DEL double code: lev_on +??? in ctree-basic.sml + position

   \item xxx

   \item DEL double code: nxt_specify_init_calc IN specify.sml + step-specify.sml

   \item xxx

   \item ALL CODE: rename spec(ification) --> know(ledge), in Specification: Relation -> Knowledge

   \item xxx

   \item replace ContextC.insert_assumptions by Tactic.insert_assumptions

         NOTE: DONE in associate, ??missing in LI.do_step ??

   \item xxx

   \item associate: drop ctxt from arg.+ return

   \item xxx

   \item in check_leaf SEPARATE tracing

         collect all trace_script --> Trace_LI

         trace_script: replace ' by " in writeln

   \item xxx

   \item renamings

     \begin{itemize}

     \item NotAss -> Not_Associated | Ass -> Associated

     \item ContextC.subpbl_to_caller -> subpbl_to_caller

     \item Tactic.is_empty_tac -> Tactic.is_empty

     \item Istate.istate2str -> Istate.string_of

     \item xxx

     \item rename   Base_Tool.thy  <---         Base_Tools

     \item adopt naming conventions in Knowledge: EqSystem --> Equation_System, etc

     \item xxx

     \item rename field scr in meth

     \item xxx

     \item xxx

     \end{itemize}

   \item xxx

   \item relocations + renamings

     \begin{itemize}

     \item Rule.terms2str -> TermC.s_to_string

         Tactic_Def.tac2str -> Tactic_Def.input_to_string

     \item xxx

     \item xxx

     \item xxx

     \item xxx

     \end{itemize}

   \item xxx

   \item cleanup test-files

     \begin{itemize}

     \item test/..  tools.sml, atools.sml,  ...

     \item xxx

     \item xxx

     \item xxx

     \item xxx

     \end{itemize}

   \item xxx

   \item see in Test_Some/300-   (*TODO: DOUBLE subst, DROP ONE*)

   \item ? improve sig. eval_leaf E a v t -> (E, (a, v)) t

   \item xxx

   \item xxx

   \item clarify Tactic.Subproblem (domID, pblID) as term in Pstate {act_arg, ...}

         there it is Free ("Subproblem", "char list \<times> ..

         instead of  Const (|???.Subproblem", "char list \<times> ..

         AND THE STRING REPRESENTATION IS STRANGE: 

           Subproblem (''Test'',

            ??.\ <^const> String.char.Char ''LINEAR'' ''univariate'' ''equation''

             ''test'')

      ML \<open>

      \<close> ML \<open>

      term2str; (*defined by..*)

      fun term_to_string''' thy t =

        let

          val ctxt' = Config.put show_markup false (Proof_Context.init_global thy)

        in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

      \<close> ML \<open>

      val t = @{term "aaa + bbb"}

      val t = @{term "Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation''])"};

      \<close> ML \<open>

      val sss = Print_Mode.setmp [] (Syntax.string_of_term @{context}) t

      \<close> ML \<open>

      writeln sss (*.. here perfect: Subproblem (''Test'', [''LINEAR'', ''univariate'', ''equation'']) *)

      \<close> ML \<open>

      \<close>

   \item xxx

   \item xxx

   \item LI.locate_input_term cleanup, case ONLY

   \item xxx

   \item revert 9ef6e9e88178 (separate Tactic / Tactic_Def),

           because tactic.sml after ctree.sml doesn't gain much !

         ?Tactic.input -> Calc.tactic ?

   \item xxx

   \item xxx

   \item collect from_pblobj_or_detail*,

     -> Rule.rls(*..\<in> ist \<rightarrow> REMOVE*) * (Istate.T * Proof.context) * Program.T 

   \item init_istate ?-> Detail_Rls?

   \item xxx

   \item rename Ctree.pos' --> Pos.pos', type decl duplicate? delete, separate!

   \item xxx

   \item Istate_Def.e_istate -> Istate.empty

   \item xxx

   \item xxx

   \item xxx

   \item distribute test/../scrtools.sml: WAIT FOR FINAL CLEANUP OF src/../Interpret

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Postponed from current changeset\<close>

 text \<open>

   \begin{itemize}

   \item xxx

   \item xxx

   \item cleanup fun me:

     fun me (*(_, Empty_Tac) p _ _ = raise ERROR ("me:  Empty_Tac at " ^ pos'2str p)

       | me*) (_, tac) p _(*NEW remove*) pt =

     + -------------------------^^^^^^

     # see test-code.sml fun me_trace

       use this also for me, not only for me_ist_ctxt; del. me

       this requires much updating in all test/*

   \item xxx

   \item xxx

   \item generate, generate1: NO thy as arg.

         Generate.generate1 thy is redundant: is the same during pbl, thus lookup spec

         redesign return value (originally for output by fun me?)

   \item xxx

   \item shift tests into NEW model.sml (upd, upds_envv, ..)

   \item xxx

   \item xxx

   \item clarify handling of contexts ctxt ContextC

     \begin{itemize}

     \item xxx

     \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt

     \item xxx

     \item Check_Elementwise "Assumptions": prerequisite for ^^goal

       rm tactic Check_elementwise "Assumptions" in a way, which keeps it for Minisubpbl

       rm Assumptions  :: bool  (* TODO: remove with making ^^^ idle *)

     \item xxx

     \item xxx

     \end{itemize}

   \item xxx

   \item xxx

   \item complete mstools.sml (* survey on handling contexts:

   \item xxx

   \item xxx

   \item xxx

   \item xxx

   \item librarys.ml --> libraryC.sml + text from termC.sml

   \item xxx

   \item xxx

   \item xxx

   \item xxx

   \item xxx

   \item xxx

   \item concentrate "insert_assumptions" for locate_input_tactic in "associate", ?OR? Tactic.insert_assumptions

                                    DONE  for find_next_step by Tactic.insert_assumptions m' ctxt 

     \begin{itemize}

     \item rm from "generate1" ("Detail_Set_Inst'", Tactic.Detail_Set' ?)

     \item shift from "applicable_in..Apply_Method" to ? ? ? (is ONLY use-case in appl.sml))

     \item ?"insert_assumptions" necessary in "init_pstate" ?+++? in "applicable_in" ?+++? "associate"

     \item xxx

     \item xxx

     \item DO DELETIONS AFTER analogous concentrations in find_next_step

     \end{itemize}

   \item xxx

   \item ? what is the difference headline <--> cascmd in

     Subproblem' (spec, oris, headline, fmz_, context, cascmd)

   \item xxx

   \item inform: TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr --> parseNEW context istr

   \item xxx

   \item unify/clarify stac2tac_ | 

     \begin{itemize}

     \item xxx

     \item extract common code from associate.. stac2tac_xxx

     \item rename LItool.tac_from_prog -> Tactic.from_prog_tac ? Solve_Tac.from_prog_tac,

     \item xxx

     \item xxx

     \end{itemize}

   \item xxx

   \item unify in signature LANGUAGE_TOOLS =\\

     val pblterm: Rule.domID -> Celem.pblID -> term     vvv        vvv\\

     val subpbl: string -> string list -> term          unify with ^^^

   \item xxx

   \item Telem.safe is questionable: has it been replaced by Safe_Step, Not_Derivable, Helpless, etc?

     Note: replacement of Istate.safe by Istate.appy_ didn't care much about Telem.safe.

     If Telem.safe is kept, consider merge with CTbasic.ostate

   \item xxx

   \item remove find_next_step from solve Apply_Method';

     this enforces Pos.at_first_tactic, which should be dropped, too.

   \item xxx

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Postponed -?-> separated task ?\<close>

 text \<open>

   \begin{itemize}

   \item xxx          

   \item xxx

   \item replace all Ctree.update_* with Ctree.cupdate_problem

   \item xxx

   \item rename (ist as {eval, ...}) -> (ist as {eval_rls, ...})

   \item xxx

   \item exception PROG analogous to TERM

   \item xxx

   \item sig/struc ..elems --> ..elem

   \item xxx          

   \item distille CAS-command, CAScmd, etc into a struct

   \item xxx          

   \item check location of files:

         test/Tools/isac/Interpret/ptyps.thy

         test/Tools/isac/Specify.ptyps.sml

   \item xxx

   \item check occurences of Atools in src/ test/

   \item Const ("Atools.pow", _) ---> Const ("Base_Tool.pow", _) 

   \item xxx          

   \item rm Float

   \item xxx

   \item Diff.thy: differentiateX --> differentiate after removal of script-constant

   \item Test.thy: met_test_sqrt2: deleted?!

   \item xxx          

   \item Rule.rew_ord' := overwritel (! Rule.rew_ord', (*<<<---- use KEStore.xxx, too*)

   \item xxx

     \item automatically extrac rls from program-code 

       ? take ["SignalProcessing", "Z_Transform", "Inverse_sub"] as an example ?

   \item xxx          

   \item finish output of trace_script with Check_Postcond (useful for SubProblem)

   \item xxx

   \item xxx          

   \item xxx

   \item xxx          

   \item xxx

   \item xxx          

   \item xxx

   \item xxx          

   \end{itemize}

 \<close>

 section \<open>Separated tasks\<close>

 text \<open>

   This section shall be removed, because

   the distinction \<open>Simple\<close> | \<open>Simple but laborous\<close> | \<open>Questionable\<close>

   is too distracting when working on \<open>TODOs from current changesets\<close>.

 \<close>

 section \<open>Major reforms\<close>

 text \<open>

 \<close>

 subsection \<open>Exception Size raised\<close>

 text \<open>

   During update Isabelle2018 --> Isabelle2019 we noticed, that

   "isabelle build" uses resources more efficiently than "isabelle jedit".

   The former works, but the latter causes 

   \begin{itemize}

   \item "Exception- Size raised"

     in Build_Thydata.thy

   \item "exception Size raised (line 169 of "./basis/LibrarySupport.sml")"

     in test/../biegelinie-*.xml.

   \end{itemize}

   This has been detected after changeset (30cd47104ad7) "lucin: reorganise theories in ProgLang".

   Find tools to investigate the Exception, and find ways around it eventually.

 \<close>

 subsection \<open>Cleanup & review signatures wrt. implementation.pdf canonical argument order\<close>

 text \<open>

   \begin{itemize}

   \item there are comments in several signatures

   \item ML_file "~~/src/Tools/isac/Interpret/specification-elems.sml" can be (almost) deleted

   \item src/../Frontend/: signatures missing

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>overall structure of code\<close>

 text \<open>

   \begin{itemize}

   \item try to separate Isac_Knowledge from MathEngine

     common base: Knowledge_Author / ..??

   \item xxx

   \item  ML_file "~~/src/Tools/isac/Interpret/ctree.sml" (*shift to base in common with Interpret*)

   \item xxx

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Separate MathEngineBasic/ Specify/ Interpret/ MathEngine/\<close>

 text \<open>

   \begin{itemize}

   \item xxx

   \item xxx

   \item re-organise code for Interpret

     \begin{itemize}

     \item Step*: Step_Specify | Step_Solve | Step

       \begin{itemize}

       \item *.check | *.add ARE TOO LATE IN BUILD with Step_Specify | Step_Solve

         Specify_Step.check | Specify_Step.add <-- Applicable.applicable_in

         Solve_Step.check   | Solve_Step.add   <-- Generate.generate1

       \item xxx

       \end{itemize}

     \item xxx

     \item Prog_Tac: fun get_first takes both Prog_Tac + Program --- wait for separate Tactical

       then shift into common descendant

     \item xxx

     \end{itemize}

   \item xxx

   \item xxx

   \item ??????????? WHY CAN LI.by_tactic NOT BE REPLACED BY Step_Solve.by_tactic ???????????

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Review modelling- + specification-phase\<close>

 text \<open>

   \begin{itemize}

   \item xxx

   \item xxx

   \item xxx

   \item check match between args of partial_function and model-pattern of meth;

      provide error message.

   \item xxx

   \item "--- hack for funpack: generalise handling of meths which extend problem items ---"

     \begin{itemize}

     \item see several locations of hack in code

     \item these locations are NOT sufficient, see

       test/../biegelinie-3.sml --- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto ---

     \item "fun associate" "match_ags ..dI" instead "..pI" breaks many tests, however,

       this would be according to survey Notes (3) in src/../calchead.sml.

     \end{itemize}

   \item see "failed trial to generalise handling of meths"98298342fb6d

   \item abstract specify + nxt_specif to common aux-funs;

     see e.g. "--- hack for funpack: generalise handling of meths which extend problem items ---"

   \item xxx

   \item type model = itm list ?

   \item review survey Notes in src/../calchead.sml: they are questionable

   \item review copy-named, probably two issues commingled 

     \begin{itemize}

     \item special handling of "#Find#, because it is not a formal argument of partial_function

     \item special naming for solutions of equation solving: x_1, x_2, ...

     \end{itemize}

   \item xxx

   \item structure Tactic Specify -?-> Proglang (would require Model., Selem.)

   \item xxx

   \item this has been written in one go:

     \begin{itemize}

     \item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]

     \item reconsider add_field': where is it used for what? Shift into mk_oris

     \item reconsider match_itms_oris: where is it used for what? max_vt ONLY???

     \item in Specify_Method search root-oris for items (e.g. "errorBound"), #1# in survey

     \item Specify_Problem, Specify_Method: check respective identifiers after re-Specify_

       (relevant for pre-condition)

     \item unify match_ags to mk_oris1..N with different args (fmz | pat list, pbl | meth

     \item 

     \end{itemize}

   \end{itemize}

 \<close>

 subsection \<open>taci list, type step\<close>

 text \<open>

 taci was, most likely, invented to make "fun me" more efficient by avoiding duplicate rewrite,

 and probably, because the Kernel interface separated setNextTactic and applyTactic.

 Both are no good reasons to make code more complicated.

 !!! taci list is used in do_next !!!

   \begin{itemize}

   \item xxx

   \item can lev_on_total replace lev_on ? ..Test_Isac_Short + rename lev_on_total -> lev_on

   \item xxx

   \item Step* functions should return Calc.T instead of Chead.calcstate'

   \item xxx

   \item states.sml: check, when "length tacis > 1"

   \item in Test_Isac.thy there is only 1 error in Interpret/inform.sml

   \item (*WN190713 REMOVE: "creating a new node" was never implemented for more than one node?!?

   \item xxx

   \item brute force setting all empty ([], [], ptp) works!?! but ptp causes errors -- investigate!

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Ctree\<close>

 text \<open>

 analysis

 # mixture pos' .. pos in cappend_*, append_* is confusing

 # existpt p pt andalso Tactic.is_empty_tac DIFFERENT IN append_*, cappend_* is confusing

   "exception PTREE "get_obj: pos =" ^^^^^: ^^^^ due to cut !!!

   NOTE: exn IN if..andalso.. IS NOT!!! DETECTED, THIS                       is confusing

   see test/../--- Minisubpbl/800-append-on-Frm.sml ---

 # ?!? "cut branches below cannot be decided here" in append_atomic

 # sign. of functions too different ?!?canonical arg.order ?!?

   \begin{itemize}

   \item xxx

   \item remove update_branch, update_*? -- make branch, etc args of append_*

   \item xxx

   \item close sig Ctree, contains cappend_* ?only? --- ?make parallel to ?Pide_Store?

   \item xxx

   \item unify args to Ctree.state (pt, p)

   \item  fun update_env       .. repl_env                   \<rightarrow>update_istate

   \item xxx

   \item xxx

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>replace theory/thy by context/ctxt\<close>

 text \<open>

   \begin{itemize}

   \item xxx

   \item Specify/ works with thy | Interpret/ works with ctxt | MathEngine.step works with ?!?ctxt

     special case: Tactic.Refine_Problem

   \item xxx

   \item theory can be retrieved from ctxt by Proof_Context.theory_of

   \item xxx

   \item cleaup the many conversions string -- theory

   \item make dest_spec --> (theory, pblID, metID) ?+ common_subthy ?

   \item 1. Rewrite.eval_true_, then

     LItool.check_leaf, Rewrite.eval_prog_expr, Generate.generate1, LItool.tac_from_prog.

   \item fun associate

     let val thy = Celem.assoc_thy "Isac_Knowledge";(*TODO*)

   \item xxx

   \item xxx

   \item in locate_input_tactic .. ?scan_dn1?; Program.is_eval_expr   .use  Term.exists_Const

   \item locate_input_tactic: get_simplifier cstate (*TODO: shift to init_istate*)

   \item push srls into pstate

   \item lucas-intrpreter.locate_input_tactic: scan_to_tactic1 srls tac cstate (progr, Rule.e_rls)

                                                                                       ^^^^^^^^^^

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Rfuns, Begin_/End_Detail', Rrls, Istate\<close>

 text \<open>

 remove Rfuns -> Rule.Prog, Rule.EmptyScr

 consider separating spec.funs. to ?Inter_Steps?

   \begin{itemize}

   \item ^^^+ see from_pblobj_or_detail_thm, from_pblobj_or_detail_calc, ...

   \item xxx

   \item probably only "normal_form" seems to be needed

   \item deleted Rfuns in NEW "locate_input_tactic": no active test for "locate_rule"

     but that seems desirable

   \item ?how is the relation to reverse-rewriting ???

   \item "Rfuns" markers in test/../rational

   \item xxx

   \item datatype istate (Istate.T): remove RrlsState, pstate: use Rrls only for creating results beyond

     rewriting and/or respective intermediate steps (e.g. cancellation of fractions).

     Thus we get a 1-step-action which does NOT require a state beyond istate/pstate.

     Thus we drastically reduce complexity, also get rid of "fun from_pblobj_or_detail_calc" , etc.

   \item debug ^^^ related: is there an occurence of Steps with more than 1 element?

   \item xxx

   \item and do_next (* WN1907: ?only for Begin_/End_Detail' DEL!!!*)

   \item xxx

   \item shouldn't go Rfuns from Rewrite --> Rewrite_Set; they behave similar to "fun interSteps" ?

   \end{itemize}

 \<close>

 subsection \<open>Inverse_Z_Transform.thy\<close>

 text \<open>

   \begin{itemize}

   \item\label{new-var-rhs} rule1..6, ruleZY introduce new variables on the rhs of the rewrite-rule.

   ? replace rewriting with substitution ?!?

   The problem is related to the decision of typing for "d_d" and making bound variables free (while

   shifting specific handling in equation solving etc. to the meta-logic). 

   \item Find "stepResponse (x[n::real]::bool)" is superfluous, because immediately used by

     rewrite-rules; see \ref{new-var-rhs}.

   \item Reconsider whole problem:

     input only the polynomial as argument of partial_function, in ([1], Frm) compile lhs "X z" ?

   \end{itemize}

 \<close>

 subsection \<open>Adopt Isabelle's numerals for Isac\<close>

 text \<open>

   \begin{itemize}

   \item replace numerals of type "real" by "nat" in some specific functions from ListC.thy

     and have both representations in parallel for "nat".

   \item xxx

   \item xxx

   \end{itemize}

 \<close>

 subsection \<open>Redesign equation solver\<close>

 text \<open>

   Existing solver is structured along the WRONG assumption,

   that Poly.thy must be the LAST thy among all thys involved -- while the opposite is the case.

   Preliminary solution: all inappropriately located thms are collected in Base_Tools.thy

 \<close>

 subsection \<open>Finetunig required for xmldata in kbase\<close>

 text \<open>

   See xmldata https://intra.ist.tugraz.at/hg/isac/rev/5b222a649390

   and in kbase html-representation generated from these xmldata.

   Notes in ~~/xmldata/TODO.txt.

 \<close>

 section \<open>Hints for further development\<close>

 text \<open>

 \<close>

 subsection \<open>Coding standards & some explanations for math-authors\<close>

 text \<open>copy from doc/math-eng.tex WN.28.3.03

 WN071228 extended\<close>

 subsubsection \<open>Identifiers\<close>

 text \<open>Naming is particularily crucial, because Isabelles name space is global, and isac does

   not yet use the novel locale features introduces by Isar. For instance, {\tt probe} sounds

   reasonable as (1) a description in the model of a problem-pattern, (2) as an element of the

   problem hierarchies key, (3) as a socalled CAS-command, (4) as the name of a related script etc.

   However, all the cases (1)..(4) require different typing for one and the same

   identifier {\tt probe} which is impossible, and actually leads to strange errors

   (for instance (1) is used as string, except in a script addressing a Subproblem).

   These are the preliminary rules for naming identifiers>

   \begin{description}

   \item [elements of a key] into the hierarchy of problems or methods must not contain

     capital letters and may contain underscrores, e.g. {\tt probe, for_polynomials}.

   \item [descriptions in problem-patterns] must contain at least 1 capital letter and

     must not contain underscores, e.g. {\tt Probe, forPolynomials}.

   \item [CAS-commands] follow the same rules as descriptions in problem-patterns above, thus

     beware of conflicts~!

   \item [script identifiers] always end with {\tt Program}, e.g. {\tt ProbeScript}.

   \item [???] ???

   \item [???] ???

   \end{description}

 %WN071228 extended\<close>

 subsubsection \<open>Rule sets\<close>

 text \<open>The actual version of the coding standards for rulesets is in {\tt /IsacKnowledge/Atools.ML

   where it can be viewed using the knowledge browsers.

   There are rulesets visible to the student, and there are rulesets visible (in general) only for

   math authors. There are also rulesets which {\em must} exist for {\em each} theory;

   these contain the identifier of the respective theory (including all capital letters) 

   as indicated by {\it Thy} below.

   \begin{description}

   \item [norm\_{\it Thy}] exists for each theory, and {\em efficiently} calculates a

     normalform for all terms which can be expressed by the definitions of the respective theory

     (and the respective parents).

   \item [simplify\_{\it Thy}] exists for each theory, and calculates a normalform for all terms

     which can be expressed by the definitions of the respective theory (and the respective parents)

     such, that the rewrites can be presented to the student.

   \item [calculate\_{\it Thy}] exists for each theory, and evaluates terms with 

     numerical constants only (i.e. all terms which can be expressed by the definitions of

     the respective theory and the respective parent theories). In particular, this ruleset includes

     evaluating in/equalities with numerical constants only.

     WN.3.7.03: may be dropped due to more generality: numericals and non-numericals

     are logically equivalent, where the latter often add to the assumptions

     (e.g. in Check_elementwise).

   \end{description}

   The above rulesets are all visible to the user, and also may be input; 

   thus they must be contained in {\tt Theory_Data} (KEStore_Elems.add_rlss,

   KEStore_Elems.get_rlss). All these rulesets must undergo a preparation

   using the function {\tt prep_rls'}, which generates a script for stepwise rewriting etc.

   The following rulesets are used for internal purposes and usually invisible to the (naive) user:

   \begin{description}

   \item [*\_erls] TODO

   \item [*\_prls] 

   \item [*\_srls] 

   \end{description}

 {\tt Rule.append_rls, Rule.merge_rls, remove_rls} TODO

 \<close>

 subsection \<open>get proof-state\<close>

 text \<open>

   Re: [isabelle] Programatically get "this"

   ----------------------------------------------------

   So here is my (Makarius') version of your initial example, following these principles:

   begin{verbatim}

     notepad

     begin

       assume a: A

       ML_val \<open>

         val ctxt = @{context};

         val this_name =

           Name_Space.full_name (Proof_Context.naming_of ctxt) (Binding.name Auto_Bind.thisN);

         val this = #thms (the (Proof_Context.lookup_fact ctxt this_name));

       \<close>

     end

   end{verbatim}

 \<close>

 subsection \<open>write Specification to jEdit\<close>

 text \<open>

   Re: [isabelle] Printing terms with type annotations

   ----------------------------------------------------

   On 06/02/2019 17:52, Moa Johansson wrote:

   >

   > I’m writing some code that should create a snippet of Isar script.

   This is how Sledgehammer approximates this:

   http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2018/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML#l299

   (The module name already shows that the proper terminology is "Isar

   proof" (or "Isar proof text").  Proof scripts are a thing from the past,

   before Isar. You can emulate old-style proof scripts via a sequence of

   'apply' commands, but this is improper Isar.)

   Note that there is no standard function in Isabelle/Pure, because the

   problem to print just the right amount of type information is very

   complex and not fully solved. One day, after 1 or 2 rounds of

   refinements over the above approach, it might become generally available.

 \<close>

 subsection \<open>follow Isabelle conventions (*Does not yet work in Isabelle2018\<close>

 text \<open>

   isabelle update -u path_cartouches

   isabelle update -u inner_syntax_cartouches

 \<close>

 section \<open>Questions to Isabelle experts\<close>

 text \<open>

 \begin{itemize}

 \item xxx

 \item xxx

 \item ?OK Test_Isac_Short with

     LI.by_tactic tac (get_istate_LI pt p, get_ctxt_LI pt p) ptp

   instead

     LI.by_tactic tac (Istate.e_istate, ContextC.e_ctxt) ptp

   in step-solve ?

 \item xxx

 \item test from last CS with outcommented re-def of code -> 

   -> \<open>further tests additional to src/.. files\<close>

       ADDTESTS/redefined-code.sml

 \item xxx

 \item efb749b79361 Test_Some_Short.thy has 2 errors, which disappear in thy ?!?:

   ML_file "Interpret/error-pattern.sml" Undefined fact: "all_left"

   ML_file "Knowledge/inssort.sml" Undefined fact: "xfoldr_Nil"

 \item xxx

 \item what is the actual replacement of "hg log --follow" ?

 \item xxx

 \item how HANDLE these exceptions, e.g.:

     Syntax.read_term ctxt "Randbedingungen y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]"

   GIVES

     "Inner syntax error

      Failed to parse term"

 \item xxx

 \item how cope with "exception Size raised (line 171 of "./basis/LibrarySupport.sml")"

   e.g. in test/Interpret/lucas-interpreter.sml

 \item xxx

 \item xxx

 \end{itemize}

 \<close>

 section \<open>For copy & paste\<close>

 text \<open>

 \begin{itemize}

 \item xxx

   \begin{itemize}

   \item xxx

     \begin{itemize}

     \item xxx

       \begin{itemize}

       \item xxx

         \begin{itemize}

         \item xxx

         \end{itemize}

       \end{itemize}

     \end{itemize}

   \end{itemize}

 \end{itemize}

 \<close>

 subsection \<open>xxx\<close>

 subsubsection \<open>xxx\<close>

 end