(* 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

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

text\<open>

  Shift more complicated issues from the next subsection to the next but one!

\<close>

subsection \<open>Current changeset\<close>

text \<open>

  \begin{itemize}

  \item xxx

  \item xxx

  \item xxx

  \item xxx

  \item xxx

  \item rm test/..--- check Scripts ---

  \item xxx

  \item reformat + rename "fun eval_leaf"+"fun get_stac"

        (*1*)(*2*)

        ?consistency with subst term?

  \item Tactic.Rewrite*': drop "bool"

  \item xxx

  \item exception PROG analogous to TERM

  \item xxx

  \item xxx

  \item xxx

  \item Prog_Tac: fun get_stac takes both Prog_Tac + Program --- wait for separate Taciical

    then shift into common descendant

    rename get_stac --> ?ptac?

  \item xxx

  \item xxx

  \item xxx

  \item separate code required in both, ProgLang & Interpret

  \item xxx

  \item /-------------------------------------------------------------------

  \item check occurences of KEStore_Elems.add_rlss [("list_rls",

  \item rename list_rls accordingly

  \item ------------------------------------------------------------------/

  \item xxx

    \item lucas-interpreter.sml         ----- vvvvvvvvv etc.

      val (p'',_,_,pt'') = Generate.generate1 @ {theory} tac' (Istate.Pstate is, ctxt) (po', p_) pt

  \item xxx

  \item rm Float

  \item xxx

    \item signature LIBRARY_C

    \item Program.thy  (*=========== record these ^^^ in 'tacs' in program.ML =========*)

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

    \item xxx

    \item xxx

    \end{itemize}

  \item xxx

  \item xxx

  \item distribute test/../scrtools.sml

  \item xxx

  \item xxx

  \item simplify calls of scan_dn1, scan_dn2 etc

  \item open Istate in LucinNEW

  \end{itemize}

\<close>

subsection \<open>Differences between code and paper\<close>

text \<open>

  \begin{itemize}

  \item xxx

  \item xxx

  \item xxx

  \item xxx

  \item xxx

  \end{itemize}

\<close>

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

text \<open>

  \begin{itemize}

  \item xxx

  \item re-organise code for Interpret

    \begin{itemize}

    \item Step*

      \begin{itemize}

      \item Step_Specify: Specify/step-specify.sml in analogy to Interpret/...

        \begin{itemize}

        \item Applicable.applicable_in --> Step_Specify.applicable

        \item Generate.generate1 --> Step_Specify.add

        \item xxx

        \end{itemize}

      \item Step_Solve: Interpret/step-solve ? is there recurs.-vvvvvvvvvvvvv?

        \begin{itemize}

        \item Step_Solve.do            <-- LucinNEW,do_solve_step

          ATTENTION: several uses of ---------------^^^^^^^^^^^^^ + recurs.! for Step_Solve.add

       \item Step_Solve.end_program   <--? LucinNEW,begin_end_prog  NOT separate ----------^^^^^^^

        \item Step_Solve.begin_program <-? LucinNEW,do_solve_step Apply_Method: ever used???

        \end{itemize}

      \item MathEngine/step.sml: Step.do calls Step_Solve.do | Step_Specify.do

        i.e. shift respective and other code from solve.sml to step.sml

    \item xxx

    \item MathEngBasic/calculation.sml

      \begin{itemize}

      \item rename Calc --> Calc_

      \item ? type Calc.T = CTree.state ?

      \item Calc.add_step <-- Step_Specify.add + Step_Solve.add <-- Generate.generate*

      \item xxx

      \end{itemize}

    \item xxx

    \end{itemize}

  \item xxx

  \item xxx

  \item decompose do_solve_step, begin_end_prog: mutual recursion only avoids multiple generate1

    ! ^^^ in determine_next_tactic --- ? ? ? in locate_input_tactic ?

  \item xxx

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

  \item xxx

  \item NEW structure Step.applicable     Step.add

                          ^applicable_in      ^generate1

  \item xxx

  \item revise Pstate {or, ...}; strange occurrence in program without Tactical.Or documented here

  \item xxx

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

  \item xxx

  \item NEW structures

    \begin{itemize}

    \item Step

      \begin{itemize}

      \item Applicable.applicable_in --> Step.applicable

      \item Generate.generate1       --> Step.add        ?-->? Calculation.add_step 

      \item xxx

      \end{itemize}

    \item Calculation ("Calc" is occupied ?!?)           ?^^^? Calculation

      \begin{itemize}

      \item Ctree.state ?-->? Calculation.T

      \item Chead.calcstate   --> Calculation.prestate

      \item Chead.calcstate'  --> Calculation.poststate

      \item e_calcstate, e_calcstate' -"-

      \item xxx

      \end{itemize}

    \end{itemize}

  \item xxx

  \item clarify handling of contexts

    \begin{itemize}

    \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 cleanup fun me:

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

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

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

    \item xxx

    \item Tactic.Apply_Method' (mI, _, _, _(*ctxt ?!?*))) .. remove ctxt

    \item rm ctxt from Subproblem' (is separated in associate!))

    \item check Tactic.Subproblem': are 2 terms required?

    \item xxx

    \item Test_Some.--- rat-equ: remove x = 0 from [x = 0, x = 6 / 5] due to contexts --

      --: wait for deleting Check_Elementwise Assumptions

    \item xxx

    \item lucas-intrpreter.scan_dn1: Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") 

    \end{itemize}

  \item xxx

  \item reconsider "fun eval_leaf"

     CAUTION: (1) currying with @@ requires 2 patterns for each tactic

              (2) the non-curried version must return NONE for a 

     	      (3) non-matching patterns become an Program.Expr by fall-through.

       (a, (*in these cases we hope, that a = SOME _*) --> exn ?PROGRAM?

     rename ?ptac?, prog_tac

  \item xxx

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

  \item xxx

  \item dest_spec (Const ("Product_Type.Pair", _) $ d $ (Const ("Product_Type.Pair", _) FORALL occur.

  \item introduce simple type names to LUCAS_INTERPRETER <-?-> readable paper

  \item xxx

  \item check in states: length ?? > 1 with tracing these cases

  \item xxx

  \item xxx

  \item Lucin.Ass_Weak etc \<longrightarrow> NEW structutre ? LItool ?

  \item xxx

  \item istate

    \begin{itemize}

    \item datatype L,R,D --> Istate

    \item xxx

    \item xxx

    \item xxx

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

    \item xxx

    \item change Lucin.interpret_leaf "locate" "Isac_Knowledge" sr E a v t

        to     Lucin.interpret_leaf "locate"  ctxt ( pstate )        !!srls in pstate!!^^

        and redesign interpret_leaf .. eval_leaf .. associate

        to Tactic.from_code : 

        + keep ! trace_script

        + scrstate2str --> pstate2str

    \item xxx

    \item after review of Rrls, detail ?-->? istate

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

    \item xxx

    \item push srls into pstate

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

                                                                                        ^^^^^^^^^^

    \item xxx

    \item xxx

    \end{itemize}

  \item xxx

  \item ctxt context

    \begin{itemize}

    \item xxx

    \item xxx

    \item xxx

    \end{itemize}

  \item trace_script: replace ' by " in writeln

  \item xxx

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

  \item xxx

  \item xxx

  \item xxx

  \item xxx

  \item xxx

  \item xxx

  \item pull update of Ctree.state out of 2 Lucin funs (locate_input_formula is different))

    \begin{itemize}

    \item 1. check if Ctree.state can be updated OUTSIDE determine_next_step

    \item 2. fun locate_input_tactic: pull generate1 out (because it stores ctxt also in cstate)

    \item 

    \item xxx

    \end{itemize}

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

                                   DONE  for determine_next_tactic 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 determine_next_tactic

    \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 extract common code from associate.. stac2tac_

  \end{itemize}

\<close>

section \<open>Separated tasks\<close>

text \<open>

\<close>

subsection \<open>Simple\<close>

text \<open>

  \item xxx

  \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 xxx

  \item drop  drop_questionmarks_

  \item xxx

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

  \item rename   Base_Tool.thy  <---         Base_Tool

  \item xxx

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

  \item xxx

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

  \item Test.thy: met_test_sqrt2: deleted?!

  \item xxx

  \item Applicable.applicable_in --> Applicable.tactic_at

  \item xxx

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

  \item xxx

  \item TermC.vars_of replace by vars (recognises numerals)

  \item xxx

  \item xxx

  \end{itemize}

\<close>

subsection \<open>Simple but laborous\<close>

text \<open>

  \begin{itemize}

  \item prep_met

    \begin{itemize}

    \item rename field scr in meth

    \item xxx

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

    \item xxx

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

       provide error message.

    \item xxx

    \item automatically extrac rls from program-code 

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

    \item xxx

    \item xxx

    \item xxx

    \end{itemize}

  \item xxx

  \item drop "init_form" and use "Take" in programs (start with latter!)

  \item xxx

  \item deprive Check_elementwise, but keep it for Minisubpl

    (which checks for Check_Postcond separated by another tactic)

    This seems a prerequisite for appropriate handling of contexts at Check_Postcond.

  \item xxx

  \end{itemize}

\<close>

subsection \<open>Questionable\<close>

text \<open>

  \begin{itemize}

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

  \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 determine_next_tactic from solve Apply_Method';

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

  \item xxx

  \item xxx

  \end{itemize}

\<close>

section \<open>Complex, related to --> other tasks\<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>solve, loc_solve_, begin_end_prog, do_solve_step, ...\<close>

text \<open>

  unify to calcstate, calcstate', ?Ctree.state?

  \begin{itemize}

  \item begin_end_prog Check_Postcond' needs NO 2.determine_next_tactic

                 solve Check_Postcond' needs, because NO prog_result in Tactic.input

     and applicable_in cannot get it.

  \item xxx

  \item adopt the same for specification phase

  \item xxx

  \end{itemize}

\<close>

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

text \<open>

  \begin{itemize}

  \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>

  \begin{itemize}

  \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

  \end{itemize}

\<close>

subsection \<open>Ctree\<close>

text \<open>

  \begin{itemize}

  \item review get_ctxt, update_ctxt, get_istate, upd_istate, upd_ctxt,

    <---> update_loc', repl_loc (remove the latter)

  \item delete field ctxt in PblObj in favour of loc

  \item xxx

  \item xxx

  \end{itemize}

\<close>

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

text \<open>

  \begin{itemize}

  \item xxx

  \item ??? can theory be retrieved from ctxt --- YES --- see Proof_Context.theory_of below

  \item xxx

  \item cleaup the many conversions string -- theory

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

  \item 1. Rewrite.eval_true_, then

    Lucin.interpret_leaf, Rewrite.eval_prog_expr, Generate.generate1, Lucin.stac2tac.

  \item fun associate

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

  \item xxx

  \item xxx

  \item xxx

  \item !!! Tactic.Refine_Problem uses Pattern.match, which takes a theory, NOT a ctxt

    but there is Proof_Context.theory_of !!!

  \end{itemize}

\<close>

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

text \<open>

  \begin{itemize}

  \item removing from_pblobj_or_detail' causes many strange errors

  \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_solve_step (* 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>Auto_Prog\<close>

text \<open>

two issues:

(1) fun prep_rls creates a Program with too general and wrong types.

(2) generated Programs (huge since strings are coded in ASCII) stored in rls drives

    Build_Thydata towards limits of resources.

  \begin{itemize}

  \item rename Auto_Prog.prep_rls --> Auto_Prog.generate

  \item Auto_Prog.generate : term -> rls -> (*Program*)term

     Ctree.current_formula---^^^^

  \item xxx

  \item xxx

  \item generate Program on demand in from_pblobj_or_detail'

  \item xxx

  \item xxx

  \end{itemize}

\<close>

subsection \<open>Redesign specify-phase\<close>

text \<open>

  \begin{itemize}

  \item xxx

  \item Separate Specify/ Interpret/ MathEngine/

    MathEngine.solve, ...,

    ? or identify "layers" like in Isabelle?

  \item xxx

  \item xxx

  \end{itemize}

\<close>

subsection \<open>Redesign thms for 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.

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

\<close>

subsection \<open>Finetunig required for xmldata\<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 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}

  \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