1.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Sep 22 16:52:14 2019 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Thu Sep 26 17:47:10 2019 +0200
     1.3 @@ -60,8 +60,7 @@
     1.4  (*
     1.5    theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret"
     1.6      ML_file solve.sml
     1.7 -    ML_file mathengine.sml
     1.8 -    ML_file "~~/src/Tools/isac/Frontend/messages.sml"
     1.9 +    ML_file "mathengine-stateless.sml"
    1.10      ML_file messages.sml
    1.11      ML_file states.sml
    1.12  *)        "MathEngine/MathEngine"

     2.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Sun Sep 22 16:52:14 2019 +0200
     2.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Thu Sep 26 17:47:10 2019 +0200
     2.3 @@ -181,9 +181,9 @@
     2.4      equs = SubProblem (''Biegelinie'', [''setzeRandbedingungen'', ''Biegelinien''],
     2.5               [''Biegelinien'', ''setzeRandbedingungenEin'']) [BOOL_LIST funs, BOOL_LIST s];
     2.6      cons = SubProblem (''Biegelinie'', [''LINEAR'', ''system''], [''no_met''])
     2.7 -             [BOOL_LIST equs, REAL_LIST vs];     \<comment> \<open>PROG consts\<close>
     2.8 +             [BOOL_LIST equs, REAL_LIST vs];
     2.9      B = Take (lastI funs);
    2.10 -    B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B                         
    2.11 +    B = ((Substitute cons) @@ (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B
    2.12    in B)"
    2.13  setup \<open>KEStore_Elems.add_mets
    2.14      [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID

     3.1 --- a/src/Tools/isac/Knowledge/Diff.thy	Sun Sep 22 16:52:14 2019 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Diff.thy	Thu Sep 26 17:47:10 2019 +0200
     3.3 @@ -386,19 +386,20 @@
     3.4  
     3.5  partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
     3.6    where
     3.7 -"simplify_derivative f_f v_v =
     3.8 +"simplify_derivative term bound_variable =
     3.9   (let
    3.10 -   f_f' = Take (d_d v_v f_f)
    3.11 +   term' = Take (d_d bound_variable term)
    3.12   in ((Try (Rewrite_Set ''norm_Rational'' False)) @@
    3.13 -     (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@
    3.14 -     (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''norm_diff'' False)) @@
    3.15 -     (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)) @@
    3.16 -     (Try (Rewrite_Set ''norm_Rational'' False))) f_f')"
    3.17 +     (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_conv'' False)) @@
    3.18 +     (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''norm_diff'' False)) @@
    3.19 +     (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_sym_conv'' False)) @@
    3.20 +     (Try (Rewrite_Set ''norm_Rational'' False))) term')"
    3.21 +
    3.22  setup \<open>KEStore_Elems.add_mets
    3.23      [Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
    3.24        (["diff","after_simplification"],
    3.25 -        [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
    3.26 -          ("#Find"  ,["derivative f_f'"])],
    3.27 +        [("#Given" ,["functionTerm term","differentiateFor bound_variable"]),
    3.28 +          ("#Find"  ,["derivative term'"])],
    3.29          {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
    3.30            crls=Atools_erls, errpats = [], nrls = norm_Rational},
    3.31          @{thm simplify_derivative.simps})]

     4.1 --- a/src/Tools/isac/ProgLang/ProgLang.thy	Sun Sep 22 16:52:14 2019 +0200
     4.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy	Thu Sep 26 17:47:10 2019 +0200
     4.3 @@ -7,8 +7,8 @@
     4.4  begin
     4.5  
     4.6  text \<open>Abstract:
     4.7 -  Here the language is defined, which extends Isabelle's functions to Isac's programs
     4.8 -  for Lucas-Interpretation.
     4.9 +  The imported theories define the language, which extends Isabelle's functions to
    4.10 +  Isac's programs for Lucas-Interpretation.
    4.11    The language is interpreted by use of Isac's rewrite engine, defined in the ML-file below.
    4.12  \<close>
    4.13  

     5.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy	Sun Sep 22 16:52:14 2019 +0200
     5.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy	Thu Sep 26 17:47:10 2019 +0200
     5.3 @@ -34,7 +34,7 @@
     5.4    Note: the items below MUST ALL be recorded in xxx TODO
     5.5  \<close>
     5.6  consts
     5.7 -  SubProblem   :: "[char list * char list list * char list list, arg list] => 'a"
     5.8 +  Calculate    :: "[char list, 'a] => 'a"
     5.9    Rewrite      :: "[char list, bool, 'a] => 'a"
    5.10    Rewrite'_Inst:: "[(char list * real) list, char list, bool, 'a] => 'a"
    5.11  			               ("(Rewrite'_Inst (_ _ _))" 11) (*without last argument ^^ for @@*)
    5.12 @@ -42,14 +42,16 @@
    5.13    Rewrite'_Set'_Inst
    5.14                 :: "[((char list) * real) list, char list, bool, 'a] => 'a"
    5.15  		                 ("(Rewrite'_Set'_Inst (_ _ _))" 11) (*without last argument ^^ for @@*)
    5.16 -  Calculate    :: "[char list, 'a] => 'a"
    5.17 +  Or'_to'_List :: "bool => 'a list"  ("Or'_to'_List (_)" 11)
    5.18 +  SubProblem   :: "[char list * char list list * char list list, arg list] => 'a"
    5.19 +  Substitute   :: "[bool list, 'a] => 'a"
    5.20 +  Take         :: "'a => 'a"
    5.21 +
    5.22    Calculate1   :: "[char list, 'a] => 'a" (*FIXXXME: unknown to lucas-interpreter*)
    5.23 -  Substitute   :: "[bool list, 'a] => 'a"
    5.24    Check'_elementwise :: (* TODO: is idle, retained for test purposes in Minisubpbl *)
    5.25  		  "['a list, 'b set] => 'a list" ("Check'_elementwise (_ _)" 11)
    5.26    Assumptions  :: bool  (* TODO: remove with making ^^^ idle *)
    5.27 -  Take         :: "'a => 'a"
    5.28 -  Or'_to'_List :: "bool => 'a list"  ("Or'_to'_List (_)" 11)
    5.29 +
    5.30  
    5.31  subsection \<open>TODO\<close>
    5.32  ML \<open>

     6.1 --- a/src/Tools/isac/TODO.thy	Sun Sep 22 16:52:14 2019 +0200
     6.2 +++ b/src/Tools/isac/TODO.thy	Thu Sep 26 17:47:10 2019 +0200
     6.3 @@ -22,10 +22,8 @@
     6.4    \item separate code required in both, ProgLang & Interpret
     6.5    \item xxx
     6.6    \item /-------------------------------------------------------------------
     6.7 -  \item Atools.thy (*> tests*) -> /test/.. 
     6.8    \item check occurences of KEStore_Elems.add_rlss [("list_rls",
     6.9    \item rename list_rls accordingly
    6.10 -  \item + see subsection \<open>overall structure of code\<close>
    6.11    \item ------------------------------------------------------------------/
    6.12    \item xxx
    6.13      \item lucas-interpreter.sml         ----- vvvvvvvvv
    6.14 @@ -51,6 +49,16 @@
    6.15    \item open Istate in LucinNEW
    6.16    \end{itemize}
    6.17  \<close>
    6.18 +subsection \<open>Differences between code and paper\<close>
    6.19 +text \<open>
    6.20 +* Prog_Tac.consts
    6.21 +  Rewrite'_Inst:: "[(char list * real) list, char list, bool, 'a] => 'a"
    6.22 +->Rewrite'_Inst:: "[(char list *   'a) list, char list,       'a] => 'a"
    6.23 +* Tactical.consts
    6.24 +  Seq      :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10)
    6.25 +->Seq      :: "['a => 'a, 'a => 'a, 'a] => 'a" (infixr "@@" 10)
    6.26 ++ If       :: "[bool, 'a => 'a, 'a => 'a, 'a] => 'a"
    6.27 +\<close>
    6.28  subsection \<open>Postponed from current changeset\<close>
    6.29  text \<open>
    6.30    \begin{itemize}
    6.31 @@ -291,6 +299,8 @@
    6.32      \item special naming for solutions of equation solving: x_1, x_2, ...
    6.33      \end{itemize}
    6.34    \item xxx
    6.35 +  \item structure Tactic Specify -?-> Proglang (would require Model., Selem.)
    6.36 +  \item xxx
    6.37    \item this has been written in one go:
    6.38      \begin{itemize}
    6.39      \item reconsidering Model.max_vt, use problem with meth ["DiffApp","max_by_calculus"]