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

subsection \<open>Shift programs for Lucas-Interpretation from strings to partial_function\<close>

text\<open>

String constants have already bee introduced to old string-programs.

Shifting this program code into partial_function reveals further issues:

\begin{itemize}

\item Biegelinie.thy was already broken after isabisac15, but never noticed.

  Switch from script to partial_function has it broken further,

  mostly due to generalisation of handling of meths which extend the model of a probl.

  !Check if (*CURRENT*) error is due to "switch from Script to partial_function" 4035ec339062 ? 

                             OR ?due to "failed trial to generalise handling of meths

                                 which extend the model of a probl " 98298342fb6d

\item

\item lucin: test/../partial_fractions: repair different behaviour of

  --- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ----

  --- isolate SubProblem [simplification, of_rationals, to_partial_fraction] me ----

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

\item lucin: extract common code from assod .. stac2tac_

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

  provide error message.

\item Diff.thy

  \begin{itemize}

  \item differentiateX --> differentiate after removal of script-constant

  \end{itemize}

\item Inverse_Z_Transform.thy:

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

\item Test.thy: met_test_sqrt2: deleted?!

\item learn to use unknown tools for investigating Test_Some in child of changeset 

  "funpack: failed trial to generalise handling of meths which extend the model of a probl"

\item re-consideration whole of modelling- + specification-phase

  \begin{itemize}

  \item introduction of y, dy as arguments in IntegrierenUndKonstanteBestimmen2

    caused major problems:

    \begin{itemize}

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

      in order to make Test_Isac run again.

      \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 assod" "match_ags ..dI" instead "..pI" breaks many tests, however,

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

      \end{itemize}

    \end{itemize}

  \item decide, whether to start with hack or with general notes

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

  \item other issues

    \begin{itemize}

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

    \end{itemize}

  \end{itemize}

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

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

\item

\item

\item

  \begin{itemize}

  \item 

    \begin{itemize}

    \item 

      \begin{itemize}

      \item 

      \end{itemize}

    \end{itemize}

  \end{itemize}

\end{itemize}

\<close>

subsubsection \<open>\<close>

section \<open>TODOs shifted here from above\<close>

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

text \<open>WN131021: 

intermediate states:

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

  and have both representations in parallel for "nat".

\<close>subsection \<open>finetunig required for xmldata\<close>

text \<open>WN140808: 

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

subsection \<open>\<close>

subsubsection \<open>\<close>

text\<open>

\begin{itemize}

\item 

\end{itemize}

\<close>

end