doc-isac/mat-eng-en.tex
author wneuper <Walther.Neuper@jku.at>
Sun, 31 Dec 2023 09:42:27 +0100
changeset 60787 26037efefd61
parent 60769 0df0759fed26
permissions -rw-r--r--
Doc/Specify_Phase 2: copy finished
     1 %WN051006 dropped in code, but interesting for case study 'order a list'
     2 %EqSystem.thy
     3 %---------------------------------------------------------------------------
     4 %
     5 % order'_system      :: "bool list => bool list " ("order'_system _")
     6 %
     7 %EqSystem.ML
     8 %---------------------------------------------------------------------------
     9 %(*("order_system", ("EqSystem.order'_system", 
    10 %                   eval_order_system "#eval_order_system_"))*)
    11 %fun eval_order_system _ "EqSystem.order'_system"
    12 %                         (p as (Const ("EqSystem.order'_system",_) $ ts)) _ =
    13 %    let val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") [])
    14 %                (isalist2list ts)
    15 %       val ts'' = list2isalist HOLogic.boolT ts'
    16 %    in if ts <> ts''
    17 %       then Some (term2str p ^ " = " ^ term2str ts'',
    18 %              Trueprop $ (mk_equality (p,ts'')))
    19 %       else None
    20 %    end
    21 %  | eval_order_system _ _ _ _ = None;
    22 %
    23 %
    24 %"Script Norm2SystemScript (es_::bool list) (vs_::real list) = \
    25 %\  (let es__ = Try (Rewrite_Set simplify_Integral_parenthesized False) es_; \
    26 %\       es__ = (Try (Calculate order_system_) (order_system es__))\
    27 %\in (SubProblem (Biegelinie_,[linear,system],[no_met])\
    28 %\                  [bool_list_ es__, real_list_ vs_]))"
    29 %              ));
    30 %
    31 %eqsystem.sml
    32 %---------------------------------------------------------------------------
    33 %"----------- eval_sort -------------------------------------------";
    34 %"----------- eval_sort -------------------------------------------";
    35 %"----------- eval_sort -------------------------------------------";
    36 %val ts = TermC.parse_test @{context} "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";
    37 %val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") [])
    38 %              (isalist2list ts);
    39 %terms2str ts';
    40 %val ts'' = list2isalist HOLogic.boolT ts';
    41 %if term2str ts'' = "[-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]"
    42 %then () else raise error "eqsystem.sml eval_sort 1";
    43 %
    44 %val t = TermC.parse_test @{context} "order_system [c_2 = 0,\
    45 %                \-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";
    46 %val Some (str,_) = eval_order_system "" "EqSystem.order'_system" t "";
    47 %if str = "order_system [c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0] = [-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]" then ()
    48 %else raise error "eqsystem.sml eval_sort 2";
    49 %
    50 %
    51 %
    52 %  calculate_ thy ("EqSystem.order'_system", 
    53 %                 eval_order_system "#eval_order_system_") t;
    54 %
    55 %---------------------------------------------------------------------------
    56 %---------------------------------------------------------------------------
    57 %---------------------------------------------------------------------------
    58 
    59 
    60 %In the following this text is not compatible with isac-code:
    61 %* move termorder to knowledge: FIXXXmat0201a
    62 %
    63 %
    64 
    65 \documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}
    66 \usepackage{latexsym}           % recommended by Ch.Schinagl 10.98
    67 \bibliographystyle{alpha}
    68 
    69 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
    70 
    71 \title{\isac --- Interface for\\
    72   Developers of Math Knowledge\\[1.0ex]
    73   and\\[1.0ex]
    74   Tools for Experiments in\\
    75   Symbolic Computation\\[1.0ex]}
    76 \author{The \isac-Team\\
    77   \tt isac-users@ist.tugraz.at\\[1.0ex]}
    78 \date{\today}
    79 
    80 \begin{document}
    81 \maketitle
    82 \newpage
    83 \tableofcontents
    84 \newpage
    85 \listoftables
    86 \newpage
    87 
    88 \chapter{Introduction}
    89 \section{The scope of this document}
    90 \paragraph{As a manual:} This document describes the interface to \isac's kernel (KE), the interface to the mathematics engine (ME) included in the KE, and to the various tools like rewriting, matching etc.
    91 
    92 \isac's KE is written in SML, the language developed in conjunction with predecessors of the theorem prover Isabelle. Thus, in this document we use the plain ASCII representation of SML code. The reader may note that the \isac-user is presented a completely different view on a graphical user interface.
    93 
    94 The document is selfcontained; basic knowledge about SML (as an introduction \cite{Paulson:91} is recommended), terms and rewriting is assumed.
    95 
    96 %The interfaces will be moderately exended during the first phase of development of the mathematics knowledge. The work on the subprojects defined should {\em not} create interfaces of any interest to a user or another author of knowledge except identifiers (of type string) for theorems, rulesets etc.
    97 
    98 Notation: SML code, directories, file names are {\tt written in 'tt'}; in particular {\tt ML>} is the KE prompt.
    99 
   100 \paragraph{Give it a try !} Another aim of this text is to give the reader hints for experiments with the tools introduced.
   101 
   102 \section{Related documents}\label{related-docs}
   103 Isabelle reference manual \cite{Isa-ref}, also contained in the Isabelle distribution under $\sim${\tt /doc/}.
   104 
   105 {\bf The actual locations of files is being recorded in \\{\tt /software/services/isac/README}
   106 \footnote{The KEs current version is {\tt isac.020120-math/} which is based on the version Isabelle99 at {\tt http://isabelle.in.tum.de}.\\
   107 The current locations at IST are\\
   108 {\tt [isabelle]\hspace{3em}      /software/sol26/Isabelle99/}\\
   109 {\tt [isac-src]\hspace{3em}      /software/services/isac/src/ke/}\\ 
   110 {\tt [isac-bin]\hspace{3em}      /software/services/isac/bin/ke/}
   111 } 
   112 and rigorously updated.} In this document we refer to the following directories
   113 \begin{tabbing}
   114 xxx\=Isabelle sources1234 \=\kill
   115 \>Isabelle sources \> {\tt [isabelle]/}\\
   116 \>KE sources       \> {\tt [isac-src]/\dots{version}\dots/}\\
   117 \>KE binary        \> {\tt [isac-bin]/\dots{version}\dots/}
   118 \end{tabbing}
   119 where {\tt\dots version\dots} stands for a directory-name containing information on the version.
   120 
   121 \section{Getting started}
   122 Change to the directory {\tt [isac-bin]} where \isac's binary is located and type to the unix-prompt '$>$' (ask your system administrator where the directory {\tt [isac-bin]} is on your system):
   123 \begin{verbatim}
   124    > [isac-bin]/sml @SMLload=isac.020120-math
   125    val it = false : bool
   126    ML>
   127 \end{verbatim}
   128 yielding the message {\tt val it = false : bool} followed by the prompt of the KE. Having been successful so far, just type in the input presented below -- all of it belongs to {\em one} session~!
   129 
   130 \part{Experimental approach}
   131 
   132 \chapter{Basics, terms and parsing}
   133 Isabelle implements terms of the {\it simply typed lambda calculus} \cite{typed-lambda} defined in $\sim${\tt/src/Pure.ML}. 
   134 \section{The definition of terms}
   135 There are two kinds of terms in Isabelle, 'raw terms' and 'certified terms'. \isac{} works on raw terms, which are efficient but hard to comprehend. 
   136 {\footnotesize\begin{verbatim}
   137    datatype term = 
   138        Const of string * typ
   139      | Free  of string * typ 
   140      | Var   of indexname * typ
   141      | Bound of int
   142      | Abs   of string * typ * term
   143      | op $  of term * term;
   144 
   145    datatype typ = Type  of string * typ list
   146                 | TFree of string * sort
   147                 | TVar  of indexname * sort;
   148 \end{verbatim}}%size % $
   149 where the definitions of sort and indexname is not relevant in this context. The {\tt typ}e is being inferred during parsing. Parsing creates the other kind of terms, {\tt cterm}. These {\tt cterm}s are encapsulated records, which cannot be composed without the respective Isabelle functions (checking for type correctness), but which then are conveniently displayed as strings (using SML compiler internals -- see below).
   150 
   151 \section{Theories and parsing}
   152 Parsing uses information contained in Isabelles theories $\sim${\tt /src/HOL}. The currently active theory is held in a global variable {\tt thy}; theories can be accessed individually;
   153 {\footnotesize\begin{verbatim}
   154    ML> thy;
   155    val it =
   156      {ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,
   157        Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat, Arith,
   158        Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype, Numeral, Bin,
   159        IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option, Map, Record,
   160        RelPow, Sexp, String, Calculation, SVC_Oracle, Main, Zorn, Filter, PNat,
   161        PRat, PReal, RealDef, RealOrd, RealInt, RealBin, HyperDef, Descript, ListG,
   162        Tools, Script, Typefix, Atools, RatArith, SqRoot, Differentiate, DiffAppl,
   163        InsSort, Isac} : theory                                                    ML>
   164    ML> HOL.thy;
   165    val it = {ProtoPure, CPure, HOL} : theory 
   166    ML>
   167    ML> parse;
   168    val it = fn : theory -> string -> cterm option
   169    ML> parse thy "a + b * #3";
   170    val it = Some "a + b * #3" : cterm option
   171    ML>
   172    ML> val t = (term_of o the) it;
   173    val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term
   174 \end{verbatim}}%size
   175 where {\tt term\_of} and {\tt the} are explained below. The syntax of the list of characters can be read out of Isabelles theories \cite{Isa-obj} {\tt [isabelle]/src/HOL/}\footnote{Or you may use your internetbrowser to look at the files in {\tt [isabelle]/browser\_info}.} 
   176 and from theories developed with in \isac{} at {\tt [isac-src]/knowledge/}. Note that the syntax of the terms is different from those displayed at \isac's frontend after conversion to MathML.
   177 
   178 
   179 \section{Displaying terms}
   180 The print depth on the SML top-level can be set in order to produce output in the amount of detail desired:
   181 {\footnotesize\begin{verbatim}
   182    ML> Compiler.Control.Print.printDepth;
   183    val it = ref 4 : int ref
   184    ML>
   185    ML> Compiler.Control.Print.printDepth:= 2;
   186    val it = () : unit
   187    ML> t;
   188    val it = # $ # $ (# $ #) : term
   189    ML>
   190    ML> Compiler.Control.Print.printDepth:= 6;
   191    val it = () : unit
   192    ML> t;
   193    val it =
   194      Const ("op +","[RealDef.real, RealDef.real] => RealDef.real") $
   195      Free ("a","RealDef.real") $
   196      (Const ("op *","[RealDef.real, RealDef.real] => RealDef.real") $
   197       Free ("b","RealDef.real") $ Free ("#3","RealDef.real")) : term
   198 \end{verbatim}}%size % $
   199 A closer look to the latter output shows that {\tt typ} is output as a string like {\tt cterm}. Other useful settings for the output are:
   200 {\footnotesize\begin{verbatim}
   201    ML> Compiler.Control.Print.printLength;
   202    val it = ref 8 : int ref
   203    ML> Compiler.Control.Print.stringDepth;
   204    val it = ref 250 : int ref
   205 \end{verbatim}}%size
   206 Anyway, the SML output of terms is not very readable; there are functions in the KE to display them:
   207 {\footnotesize\begin{verbatim}
   208    ML> atomt;
   209    val it = fn : term -> unit
   210    ML> atomt t; 
   211    *** -------------
   212    *** Const ( op +)
   213    *** . Free ( a, )
   214    *** . Const ( op *)
   215    *** . . Free ( b, )
   216    *** . . Free ( #3, )
   217    val it = () : unit
   218    ML>
   219    ML> TermC.atom_trace_detail \@\{context\};
   220    val it = fn : theory -> term -> unit
   221    ML> TermC.atom_trace_detail \@\{context\} t;
   222    *** -------------
   223    *** Const ( op +, [real, real] => real)
   224    *** . Free ( a, real)
   225    *** . Const ( op *, [real, real] => real)
   226    *** . . Free ( b, real)
   227    *** . . Free ( #3, real)
   228    val it = () : unit
   229 \end{verbatim}}%size
   230 where again the {\tt typ}s are rendered as strings, but more elegantly by use of the information contained in {\tt thy}..
   231 
   232 \paragraph{Give it a try !} {\bf The mathematics knowledge grows} as it is defined in Isabelle theory by theory. Have a look by your internet browser to the hierarchy of those theories at {\tt [isabelle]/src/HOL/HOL.thy} and its children available on your system. Or you may use your internetbrowser to look at the files in {\tt [isabelle]/browser\_info}.
   233 {\footnotesize\begin{verbatim}
   234    ML> (*-1-*) parse HOL.thy "#2^^^#3";
   235    *** Inner lexical error at: "^^^#3"
   236    val it = None : cterm option
   237    ML>
   238    ML> (*-2-*) parse HOL.thy "d_d x (a + x)";
   239    val it = None : cterm option
   240    ML>
   241    ML>
   242    ML> (*-3-*) parse RatArith.thy "#2^^^#3";
   243    val it = Some "#2 ^^^ #3" : cterm option
   244    ML>
   245    ML> (*-4-*) parse RatArith.thy "d_d x (a + x)";
   246    val it = Some "d_d x (a + x)" : cterm option
   247    ML>
   248    ML>
   249    ML> (*-5-*) parse Differentiate.thy "d_d x (a + x)";
   250    val it = Some "d_d x (a + x)" : cterm option
   251    ML>
   252    ML> (*-6-*) parse Differentiate.thy "#2^^^#3";
   253    val it = Some "#2 ^^^ #3" : cterm option
   254 \end{verbatim}}%size
   255 Don't trust the string representation: if we convert {\tt(*-4-*)} and {\tt(*-6-*)} to terms \dots
   256 {\footnotesize\begin{verbatim}
   257    ML> (*-4-*) val thy = RatArith.thy;
   258    ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
   259    *** -------------
   260    *** Free ( d_d, [real, real] => real)
   261    *** . Free ( x, real)
   262    *** . Const ( op +, [real, real] => real)
   263    *** . . Free ( a, real)
   264    *** . . Free ( x, real)
   265    val it = () : unit
   266    ML>
   267    ML> (*-6-*) val thy = Differentiate.thy;
   268    ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
   269    *** -------------
   270    *** Const ( Differentiate.d_d, [real, real] => real)
   271    *** . Free ( x, real)
   272    *** . Const ( op +, [real, real] => real)
   273    *** . . Free ( a, real)
   274    *** . . Free ( x, real)
   275    val it = () : unit
   276 \end{verbatim}}%size
   277 \dots we see: in {\tt(*-4-*)} we have an arbitrary function {\tt Free ( d\_d, \_)} and in {\tt(*-6-*)} we have the special function constant {\tt Const ( Differentiate.d\_d, \_)} for differentiation, which is defined in {\tt Differentiate.thy} and presumerably is meant.
   278 
   279 
   280 \section{Converting terms}
   281 The conversion from {\tt cterm} to {\tt term} has been shown above:
   282 {\footnotesize\begin{verbatim}
   283    ML> term_of;
   284    val it = fn : cterm -> term
   285    ML>
   286    ML> the;
   287    val it = fn : 'a option -> 'a
   288    ML>
   289    ML> val t = (term_of o the o (parse thy)) "a + b * #3";
   290    val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term
   291 \end{verbatim}}%size
   292 where {\tt the} unwraps the {\tt term option} --- an auxiliary function from Larry Paulsons basic library at {\tt [isabelle]/src/Pure/library.ML}, which is really worthwile to study for any SML programmer.
   293 
   294 The other conversions are the following, some of which use the {\it signature} {\tt sign} of a theory:
   295 {\footnotesize\begin{verbatim}
   296    ML> sign_of;
   297    val it = fn : theory -> Sign.sg
   298    ML>
   299    ML> cterm_of;
   300    val it = fn : Sign.sg -> term -> cterm
   301    ML> val ct = cterm_of (sign_of thy) t;
   302    val ct = "a + b * #3" : cterm
   303    ML>
   304    ML> Sign.string_of_term;
   305    val it = fn : Sign.sg -> term -> string
   306    ML> Sign.string_of_term (sign_of thy) t;
   307    val it = "a + b * #3" : ctem'
   308    ML>
   309    ML> string_of_cterm;
   310    val it = fn : cterm -> string
   311    ML> string_of_cterm ct;
   312    val it = "a + b * #3" : ctem'
   313 \end{verbatim}}%size
   314 
   315 \section{Theorems}
   316 Theorems are a type, {\tt thm}, even more protected than {\tt cterms}: they are defined as axioms or proven in Isabelle. These definitions and proofs are contained in theories in the directory {\tt[isac-src]/knowledge/}, e.g. the theorem {\tt diff\_sum} in the theory {\tt[isac-src]/knowledge/Differentiate.thy}. Additionally, each theorem has to be recorded for \isac{} in the respective {\tt *.ML}, e.g. {\tt diff\_sum} in {\tt[isac-src]/knowledge/Differentiate.ML} as follows:
   317 {\footnotesize\begin{verbatim}
   318    ML> theorem' := overwritel (!theorem',
   319    [("diff_const",num_str diff_const)
   320    ]);
   321 \end{verbatim}}%size
   322 The additional recording of theorems and other values will disappear in later versions of \isac.
   323 
   324 \chapter{Rewriting}
   325 \section{The arguments for rewriting}
   326 The type identifiers of the arguments and values of the rewrite-functions in \ref{rewrite} differ only in an apostroph: the apostrohped types are re-named strings in order to maintain readability.
   327 {\footnotesize\begin{verbatim}
   328    ML> HOL.thy;
   329    val it = {ProtoPure, CPure, HOL} : theory
   330    ML> "HOL.thy" : theory';
   331    val it = "HOL.thy" : theory'
   332    ML>
   333    ML> sqrt_right;
   334    val it = fn : rew_ord (* term * term -> bool *)
   335    ML> "sqrt_right" : rew_ord;
   336    val it = "sqrt_right" : rew_ord
   337    ML>
   338    ML> eval_rls;
   339    val it =
   340      Rls
   341        {preconds=[],rew_ord=("sqrt_right",fn),
   342         rules=[Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,
   343                Thm #,Thm #,Thm #,Thm #,Thm #,Calc #,Calc #,...],
   344         program=Script (Free #)} : rls
   345    ML> "eval_rls" : rls';
   346    val it = "eval_rls" : rls'
   347    ML>
   348    ML> diff_sum;
   349    val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : thm
   350    ML> ("diff_sum", "") : thm';
   351    val it = ("diff_sum","") : thm'
   352 \end{verbatim}}%size
   353 where a {\tt thm'} is a pair, eventually with the string-representation of the respective theorem.
   354  
   355 \section{The functions for rewriting}\label{rewrite}
   356 Rewriting comes along with two equivalent functions, where the first is being actually used within the KE, and the second one is useful for tests: 
   357 {\footnotesize\begin{verbatim}
   358    ML> rewrite_;
   359    val it = fn
   360      : theory
   361        -> rew_ord
   362           -> rls -> bool -> thm -> term -> (term * term list) option
   363    ML>
   364    ML> rewrite;
   365    val it = fn
   366      : theory'
   367        -> rew_ord
   368           -> rls' -> bool -> thm' -> cterm' -> (cterm' * cterm' list) option
   369 \end{verbatim}}%size
   370 The arguments are the following:\\
   371 \tabcolsep=4mm
   372 \def\arraystretch{1.5}
   373 \begin{tabular}{lp{11.0cm}}
   374   {\tt theory}  & the Isabelle theory containing the definitions necessary for parsing the {\tt term} \\
   375   {\tt rew\_ord}& the rewrite order \cite{nipk:rew-all-that} for ordered rewriting -- see the section \ref{term-order} below. For {\em no} ordered rewriting take {\tt tless\_true}, a dummy order yielding true for all arguments \\
   376   {\tt rls}     & the rule set for evaluating the condition within {\tt thm} in case {\tt thm} is a conditional rule \\
   377   {\tt bool}    & a flag which triggers the evaluation of the eventual condition in {\tt thm}: if {\tt false} then evaluate the condition and according to the result of the evaluation apply {\tt thm} or not (conditional rewriting \cite{nipk:rew-all-that}), if {\tt true} then don't evaluate the condition, but put it into the set of assumptions \\
   378   {\tt thm}     & the theorem used to try to rewrite {\tt term} \\
   379   {\tt term}    & the term eventually rewritten by {\tt thm} \\
   380 \end{tabular}\\
   381 
   382 \noindent The respective values of {\tt rewrite\_} and {\tt rewrite} are an {\tt option} of a pair, i.e. {\tt Some(\_,\_)} in case the {\tt term} can be rewritten by {\tt thm} w.r.t. {\tt rew\_ord} and/or {\tt rls}, or {\tt None} if no rewrite is found:\\
   383 \begin{tabular}{lp{10.4cm}}
   384   {\tt term}     & the term rewritten \\
   385   {\tt term list}& the assumptions eventually generated if the {\tt bool} flag is set to {\tt true} and {\tt thm} is applicable. \\
   386 \end{tabular}\\
   387 
   388 \paragraph{Give it a try !} {\bf\dots rewriting is fun~!} many examples can be found in {\tt [isac-src]/tests/\dots}. In {\tt [isac-src]/tests/differentiate.sml} the following can be found:
   389 {\footnotesize\begin{verbatim}
   390    ML> val thy' = "Differentiate.thy";
   391    val thy' = "Differentiate.thy" : string
   392    ML> val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";
   393    val ct = "d_d x (x ^^^ #2 + #3 * x + #4)" : cterm'
   394    ML>
   395    ML> val thm = ("diff_sum","");
   396    val thm = ("diff_sum","") : thm'
   397    ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
   398                      [("bdv","x::real")] thm ct;
   399    val ct = "d_d x (x ^^^ #2 + #3 * x) + d_d x #4" : cterm'
   400    ML>
   401    ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
   402                      [("bdv","x::real")] thm ct;
   403    val ct = "d_d x (x ^^^ #2) + d_d x (#3 * x) + d_d x #4" : cterm'
   404    ML>
   405    ML> val thm = ("diff_prod_const","");
   406    val thm = ("diff_prod_const","") : thm'
   407    ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true
   408                      [("bdv","x::real")] thm ct;
   409    val ct = "d_d x (x ^^^ #2) + #3 * d_d x x + d_d x #4" : cterm'
   410 \end{verbatim}}%size
   411 You can look up the theorems in {\tt [isac-src]/knowledge/Differentiate.thy} and try to apply them until you get the result you would expect if calculating by hand.
   412 \footnote{Hint: At the end you will need {\tt val (ct,\_) = the (rewrite\_set thy' "eval\_rls" false "SqRoot\_simplify" ct);}}
   413 
   414 \paragraph{Give it a try !}\label{cond-rew} {\bf Conditional rewriting} is a more powerful technique then ordinary rewriting, and is closer to the power of programming languages (see the subsequent 'try it out'~!). The following example expands a term to poynomial form:
   415 {\footnotesize\begin{verbatim}
   416    ML> val thy' = "Isac.thy";
   417    val thy' = "Isac.thy" : string
   418    ML> val ct' = "#3 * a + #2 * (a + #1)";
   419    val ct' = "#3 * a + #2 * (a + #1)" : cterm'
   420    ML>
   421    ML> val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");
   422    val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n")
   423      : thm'
   424    ML> (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
   425    val ct' = "#3 * a + (#2 * a + #2 * #1)" : cterm'
   426    ML>
   427    ML> val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");
   428    val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1")
   429      : thm'
   430    ML> (*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
   431    val ct' = "#3 * a + #2 * a + #2 * #1" : cterm'
   432    ML>
   433    ML> val thm' = ("rcollect_right",
   434      "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");
   435    val thm' =
   436      ("rcollect_right",
   437       "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n")
   438      : thm'
   439    ML> (*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
   440    val ct' = "(#3 + #2) * a + #2 * #1" : cterm'
   441    ML>
   442    ML> (*4*) val Some (ct',_) = calculate' thy' "plus" ct';
   443    val ct' = "#5 * a + #2 * #1" : cterm'
   444    ML>
   445    ML> (*5*) val Some (ct',_) = calculate' thy' "times" ct';
   446    val ct' = "#5 * a + #2" : cterm'
   447 \end{verbatim}}%size
   448 Note, that the two rules, {\tt radd\_mult\_distrib2} in {\tt(*1*)} and {\tt rcollect\_right} in {\tt(*3*)} would neutralize each other (i.e. a rule set would not terminate), if there would not be the condition {\tt is\_const}.
   449 
   450 \paragraph{Give it a try !} {\bf Functional programming} can, within a certain range, modeled by rewriting. In {\tt [isac-src]/\dots/tests/InsSort.thy} the following rules can be found, which are able to sort a list ('insertion sort'):
   451 {\footnotesize\begin{verbatim}
   452    sort_def   "sort ls = foldr ins ls []"
   453 
   454    ins_base   "ins [] a = [a]"
   455    ins_rec    "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))"  
   456 
   457    foldr_base "foldr f [] a = a"
   458    foldr_rec  "foldr f (x#xs) a = foldr f xs (f a x)"
   459 
   460    if_True    "(if True then ?x else ?y) = ?x"
   461    if_False   "(if False then ?x else ?y) = ?y"
   462 \end{verbatim}}%size
   463 where {\tt\#} is the list-constructor, {\tt foldr} is the well-known standard function of functional programming, and {\tt if\_True, if\_False} are auxiliary rules. Then the sort may be done by the following rewrites:
   464 {\footnotesize\begin{verbatim}
   465    ML>  val thy' = "InsSort.thy";
   466    val thy' = "InsSort.thy" : theory'
   467    ML>  val ct = "sort [#1,#3,#2]" : cterm';
   468    val ct = "sort [#1,#3,#2]" : cterm'
   469    ML>
   470    ML>  val thm = ("sort_def","");
   471    ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
   472    val ct = "foldr ins [#1, #3, #2] []" : cterm'
   473    ML>
   474    ML>  val thm = ("foldr_rec","");
   475    ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
   476    val ct = "foldr ins [#3, #2] (ins [] #1)" : cterm'
   477    ML>
   478    ML>  val thm = ("ins_base","");
   479    ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
   480    val ct = "foldr ins [#3, #2] [#1]" : cterm'
   481    ML>
   482    ML>  val thm = ("foldr_rec","");
   483    ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
   484    val ct = "foldr ins [#2] (ins [#1] #3)" : cterm'
   485    ML>
   486    ML>  val thm = ("ins_rec","");
   487    ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
   488    val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"
   489      : cterm'
   490    ML>
   491    ML>  val (ct,_) = the (calculate' thy' "le" ct);
   492    val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])" : cterm'
   493    ML>
   494    ML>  val thm = ("if_True","(if True then ?x else ?y) = ?x");
   495    ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);
   496    val ct = "foldr ins [#2] (#1 # ins [] #3)" : cterm'
   497    ML> 
   498    ...
   499    val ct = "sort [#1,#3,#2]" : cterm'
   500 \end{verbatim}}%size
   501 
   502 
   503 \section{Variants of rewriting}
   504 Some of the above examples already used variants of {\tt rewrite} all of which have the same value, and very similar arguments:
   505 {\footnotesize\begin{verbatim}
   506    ML> rewrite_inst_;
   507    val it = fn
   508      : theory
   509        -> rew_ord
   510           -> rls
   511              -> bool
   512              -> (cterm' * cterm') list
   513                    -> thm -> term -> (term * term list) option
   514    ML> rewrite_inst;
   515    val it = fn
   516      : theory'
   517        -> rew_ord
   518           -> rls'
   519              -> bool
   520                 -> (cterm' * cterm') list
   521                    -> thm' -> cterm' -> (cterm' * cterm' list) option
   522    ML>
   523    ML> rewrite_set_;
   524    val it = fn 
   525      : theory -> rls -> bool -> rls -> term -> (term * term list) option
   526    ML> rewrite_set;
   527    val it = fn
   528      : theory' -> rls' -> bool -> rls' -> cterm' -> (cterm' * cterm' list) option
   529    ML>
   530    ML> rewrite_set_inst_;
   531    val it = fn
   532      : theory
   533        -> rls
   534           -> bool
   535              -> (cterm' * cterm') list
   536                 -> rls -> term -> (term * term list) option
   537    ML> rewrite_set_inst;
   538    val it = fn
   539      : theory'
   540        -> rls'
   541           -> bool
   542              -> (cterm' * cterm') list
   543                 -> rls' -> cterm' -> (cterm' * cterm' list) option
   544 \end{verbatim}}%size
   545 
   546 \noindent The variant {\tt rewrite\_inst} substitutes {\tt (term * term) list} in {\tt thm} before rewriting,\\
   547 the variant {\tt rewrite\_set} rewrites with a whole rule set {\tt rls} (instead with a {\tt thm} only),\\
   548 the variant {\tt rewrite\_set\_inst} is a combination of the latter two variants. In order to watch how a term is rewritten theorem by theorem, there is a switch {\tt trace\_rewrite}:
   549 {\footnotesize\begin{verbatim}
   550    ML> toggle;
   551    val it = fn : bool ref -> bool
   552    ML>
   553    ML> toggle trace_rewrite;
   554    val it = true : bool
   555    ML> toggle trace_rewrite;
   556    val it = false : bool
   557 \end{verbatim}}%size
   558 
   559 \section{Rule sets}
   560 Some of the variants of {\tt rewrite} above do not only apply one theorem, but a whole set of theorems, called a 'rule set'. Such a rule set is applied as long one of its elements can be used for a rewrite (which can go forever, i.e. the rule set eventually does not 'terminate').
   561 
   562 A simple example of a rule set is {\tt rearrange\_assoc} which is defined in {\tt knowledge/RatArith.ML} as:
   563 {\footnotesize\begin{verbatim}
   564    val rearrange_assoc = 
   565      Rls{preconds = [], rew_ord = ("tless_true",tless_true), 
   566          rules = 
   567          [Thm ("radd_assoc_RS_sym",num_str (radd_assoc RS sym)),
   568           Thm ("rmult_assoc_RS_sym",num_str (rmult_assoc RS sym))],
   569          program = Script ((term_of o the o (parse thy)) 
   570          "empty_script")
   571          }:rls;
   572 \end{verbatim}}%size
   573 where 
   574 \begin{description}
   575 \item [\tt preconds] are conditions which must be true in order to make the rule set applicable (the empty list evaluates to {\tt true})
   576 \item [\tt rew\_ord] concerns term orders introduced below in \ref{term-order}
   577 \item [\tt rules] are the theorems to be applied -- in priciple applied in arbitrary order, because all these rule sets should be 'complete' \cite{nipk:rew-all-that} (and actually the theorems are applied in the sequence they appear in this list). The function {\tt num\_str} must be applied to theorems containing numeral constants (and thus is obsolete in this example). {\tt RS} is an infix function applying the theorem {\tt sym} to {\tt radd\_assoc} before storage (the effect see below)
   578 \item [\tt program] is the script applying the ruleset; it will disappear in later versions of \isac.
   579 \end{description}
   580 These variables evaluate to
   581 {\footnotesize\begin{verbatim}
   582    ML> sym;
   583    val it = "?s = ?t ==> ?t = ?s" : thm 
   584    ML> rearrange_assoc;
   585    val it =
   586      Rls
   587        {preconds=[],rew_ord=("tless_true",fn),
   588         rules=[Thm ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"),
   589                Thm ("rmult_assoc_RS_sym","?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")],
   590         program=Script (Free ("empty_script","RealDef.real"))} : rls 
   591 \end{verbatim}}%size
   592 
   593 \paragraph{Give it a try !} The above rule set makes an arbitrary number of parentheses disappear which are not necessary due to associativity of {\tt +} and 
   594 {\footnotesize\begin{verbatim}
   595    ML> val ct = (string_of_cterm o the o (parse RatArith.thy))
   596                 "a + (b * (c * d) + e)";
   597    val ct = "a + ((b * (c * d) + e) + f)" : cterm'
   598    ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
   599    val it = Some ("a + b * c * d + e + f",[]) : (string * string list) option
   600 \end{verbatim}}%size
   601 For acchieving this result the rule set has to be surprisingly busy:
   602 {\footnotesize\begin{verbatim}
   603    ML> toggle trace_rewrite;
   604    val it = true : bool
   605    ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;
   606    ### trying thm 'radd_assoc_RS_sym'
   607    ### rewrite_set_: a + b * (c * d) + e
   608    ### trying thm 'radd_assoc_RS_sym'
   609    ### trying thm 'rmult_assoc_RS_sym'
   610    ### rewrite_set_: a + b * c * d + e
   611    ### trying thm 'rmult_assoc_RS_sym'
   612    ### trying thm 'radd_assoc_RS_sym'
   613    ### trying thm 'rmult_assoc_RS_sym'
   614    val it = Some ("a + b * c * d + e",[]) : (string * string list) option
   615 \end{verbatim}}%size
   616  
   617 
   618 \section{Calculate numeric constants}
   619 As soon as numeric constants are in adjacent subterms (see the example on p.\pageref{cond-rew}), they can be calculated by the function
   620 {\footnotesize\begin{verbatim}
   621    ML> calculate;
   622    val it = fn : theory' -> string -> cterm' -> (cterm' * thm') option
   623    ML> calculate_;
   624    val it = fn : theory -> string -> term -> (term * (string * thm)) option
   625 \end{verbatim}}%size
   626 where the {\tt string} in the arguments defines the algebraic operation to be calculated. The function returns the result of the calculation, and as second element in the pair the theorem applied. The following algebraic operations are available:
   627 {\footnotesize\begin{verbatim}
   628    ML> calc_list;
   629    val it =
   630      ref
   631        [("plus",("op +",fn)),
   632         ("times",("op *",fn)),
   633         ("cancel_",("cancel",fn)),
   634         ("power",("pow",fn)),
   635         ("sqrt",("sqrt",fn)),
   636         ("Var",("Var",fn)),
   637         ("Length",("Length",fn)),
   638         ("Nth",("Nth",fn)),
   639         ("power",("pow",fn)),
   640         ("le",("op <",fn)),
   641         ("leq",("op <=",fn)),
   642         ("is_const",("is'_const",fn)),
   643         ("is_root_free",("is'_root'_free",fn)),
   644         ("contains_root",("contains'_root",fn)),
   645         ("ident",("ident",fn))]
   646      : (string * (string * (string -> term -> theory -> 
   647         (string * term) option))) list ref
   648 \end{verbatim}}%size
   649 These operations can be used in the following way.
   650 {\footnotesize\begin{verbatim}
   651    ML> calculate' "Isac.thy" "plus" "#1 + #2";
   652    val it = Some ("#3",("#add_#1_#2","\"#1 + #2 = #3\"")) : (string * thm') option
   653    ML>
   654    ML> calculate' "Isac.thy" "times" "#2 * #3";
   655    val it = Some ("#6",("#mult_#2_#3","\"#2 * #3 = #6\""))
   656      : (string * thm') option
   657    ML>
   658    ML> calculate' "Isac.thy" "power" "#2 ^^^ #3";
   659    val it = Some ("#8",("#power_#2_#3","\"#2 ^^^ #3 = #8\""))
   660      : (string * thm') option
   661    ML>
   662    ML> calculate' "Isac.thy" "cancel_" "#9 // #12";
   663    val it = Some ("#3 // #4",("#cancel_#9_#12","\"#9 // #12 = #3 // #4\""))
   664      : (string * thm') option
   665    ML>
   666    ML> ...
   667 \end{verbatim}}%size
   668           
   669 
   670 
   671 \chapter{Term orders}\label{term-order}
   672 Orders on terms are indispensable for the purpose of rewriting to normal forms in associative - commutative domains \cite{nipk:rew-all-that}, and for rewriting to normal forms necessary for matching models to problems, see sect.\ref{pbt}.
   673 \section{Examples for term orders}
   674 It is not trivial to construct a relation $<$ on terms such that it is really an order, i.e. a transitive and antisymmetric relation. These orders are 'recursive path orders' \cite{nipk:rew-all-that}. Some orders implemented in the knowledgebase at {\tt [isac-src]/knowledge/\dots}, %FIXXXmat0201a
   675 e.g.
   676 {\footnotesize\begin{verbatim}
   677    ML> sqrt_right;
   678    val it = fn : bool -> theory -> term * term -> bool
   679    ML> tless_true;
   680    val it = fn : 'a -> bool 
   681 \end{verbatim}}%size
   682 where the bool argument is a switch for tracing the checks on the respective subterms (and theory is necessary for displyinging the (sub-)terms as strings in the case of 'true'). The order {\tt tless\_true} is a dummy always yielding {\tt true}, and {\tt sqrt\_right} prefers a square root shifted to the right within a term:
   683 {\footnotesize\begin{verbatim}
   684    ML> val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";
   685    val t1 = Const # $ (# $ #) $ Free (#,#) : term
   686    ML>
   687    ML> val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";
   688    val t2 = Const # $ Free # $ (Const # $ Free #) : term
   689    ML>
   690    ML> sqrt_right false SqRoot.thy (t1, t2);
   691    val it = false : bool
   692    ML> sqrt_right false SqRoot.thy (t2, t1);
   693    val it = true : bool
   694 \end{verbatim}}%size
   695 The many checks performed recursively through all subterms can be traced throughout the algorithm in {\tt [isac-src]/knowledge/SqRoot.ML} by setting the flag to true:
   696 {\footnotesize\begin{verbatim}
   697    ML> val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";
   698    val t1 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term
   699    ML>
   700    ML> val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";
   701    val t2 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term
   702    ML>
   703    ML> sqrt_right true SqRoot.thy (t1, t2);
   704    t= f@ts= "op +" @ "[a + b * sqrt c,d]"
   705    u= g@us= "op +" @ "[a + sqrt b * c,d]"
   706    size_of_term(t,u)= (8, 8)
   707    hd_ord(f,g)      = EQUAL
   708    terms_ord(ts,us) = LESS
   709    -------
   710    t= f@ts= "op +" @ "[a,b * sqrt c]"
   711    u= g@us= "op +" @ "[a,sqrt b * c]"
   712    size_of_term(t,u)= (6, 6)
   713    hd_ord(f,g)      = EQUAL
   714    terms_ord(ts,us) = LESS
   715    -------
   716    t= f@ts= "a" @ "[]"
   717    u= g@us= "a" @ "[]"
   718    size_of_term(t,u)= (1, 1)
   719    hd_ord(f,g)      = EQUAL
   720    terms_ord(ts,us) = EQUAL
   721    -------
   722    t= f@ts= "op *" @ "[b,sqrt c]"
   723    u= g@us= "op *" @ "[sqrt b,c]"
   724    size_of_term(t,u)= (4, 4)
   725    hd_ord(f,g)      = EQUAL
   726    terms_ord(ts,us) = LESS
   727    -------
   728    t= f@ts= "b" @ "[]"
   729    u= g@us= "sqrt" @ "[b]"
   730    size_of_term(t,u)= (1, 2)
   731    hd_ord(f,g)      = LESS
   732    terms_ord(ts,us) = LESS
   733    -------
   734    val it = true : bool 
   735 \end{verbatim}}%size
   736 
   737 
   738 
   739 \section{Ordered rewriting}
   740 Rewriting faces problems in just the most elementary domains, which are all associative and commutative w.r.t. {\tt +} and {\tt *} --- the law of commutativity applied within a rule set causes this set not to terminate~! One method to cope with this difficulty is ordered rewriting, where a rewrite is only done if the resulting term is smaller w.r.t. a term order (with some additional properties called 'rewrite orders' \cite{nipk:rew-all-that}).
   741 
   742 Such a rule set {\tt ac\_plus\_times}, called an AC-rewrite system, can be found in {\tt[isac-src]/knowledge/RathArith.ML}:
   743 {\footnotesize\begin{verbatim}
   744    val ac_plus_times =
   745      Rls{preconds = [], rew_ord = ("term_order",term_order),
   746          rules =
   747          [Thm ("radd_commute",radd_commute),
   748           Thm ("radd_left_commute",radd_left_commute),
   749           Thm ("radd_assoc",radd_assoc),
   750           Thm ("rmult_commute",rmult_commute),
   751           Thm ("rmult_left_commute",rmult_left_commute),
   752           Thm ("rmult_assoc",rmult_assoc)],
   753          program = Script ((term_of o the o (parse thy))
   754          "empty_script")
   755          }:rls;
   756    val ac_plus_times =
   757      Rls
   758        {preconds=[],rew_ord=("term_order",fn),
   759         rules=[Thm ("radd_commute","?m + ?n = ?n + ?m"),
   760                Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"),
   761                Thm ("radd_assoc","?m + ?n + ?k = ?m + (?n + ?k)"),
   762                Thm ("rmult_commute","?m * ?n = ?n * ?m"),
   763                Thm ("rmult_left_commute","?x * (?y * ?z) = ?y * (?x * ?z)"),
   764                Thm ("rmult_assoc","?m * ?n * ?k = ?m * (?n * ?k)")],
   765         program=Script (Free ("empty_script","RealDef.real"))} : rls 
   766 \end{verbatim}}%size
   767 Note that the theorems {\tt radd\_left\_commute} and {\tt rmult\_left\_commute} are really necessary in order to make the rule set 'confluent'~!
   768 
   769 
   770 \paragraph{Give it a try !} Ordered rewriting is one technique to produce polynomial normal from from arbitrary integer terms:
   771 {\footnotesize\begin{verbatim}
   772    ML> val ct' = "#3 * a + b + #2 * a";
   773    val ct' = "#3 * a + b + #2 * a" : cterm'
   774    ML>
   775    ML> (*-1-*) radd_commute; val thm' = ("radd_commute","") : thm';
   776    val it = "?m + ?n = ?n + ?m" : thm
   777    val thm' = ("radd_commute","") : thm'
   778    ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
   779    val ct' = "#2 * a + (#3 * a + b)" : cterm'
   780    ML>
   781    ML> (*-2-*) rdistr_right_assoc_p; val thm' = ("rdistr_right_assoc_p","") : thm';
   782    val it = "?l * ?n + (?m * ?n + ?k) = (?l + ?m) * ?n + ?k" : thm
   783    val thm' = ("rdistr_right_assoc_p","") : thm'
   784    ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
   785    val ct' = "(#2 + #3) * a + b" : cterm'
   786    ML>
   787    ML> (*-3-*)
   788    ML> val Some (ct',_) = calculate thy' "plus" ct';
   789    val ct' = "#5 * a + b" : cterm'
   790 \end{verbatim}}%size %FIXXXmat0201b ... calculate !
   791 This looks nice, but if {\tt radd\_commute} is applied automatically in {\tt (*-1-*)} without checking the resulting term to be 'smaller' w.r.t. a term order, then rewritin goes on forever (i.e. it does not 'terminate') \dots
   792 {\footnotesize\begin{verbatim}
   793    ML> val ct' = "#3 * a + b + #2 * a" : cterm';
   794    val ct' = "#3 * a + b + #2 * a" : cterm'
   795    ML> val thm' = ("radd_commute","") : thm';
   796    val thm' = ("radd_commute","") : thm'
   797    ML>
   798    ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
   799    val ct' = "#2 * a + (#3 * a + b)" : cterm'
   800    ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
   801    val ct' = "#3 * a + b + #2 * a" : cterm'
   802    ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';
   803    val ct' = "#2 * a + (#3 * a + b)" : cterm'
   804               ..........
   805 \end{verbatim}}%size
   806 
   807 Ordered rewriting with the above AC-rewrite system {\tt ac\_plus\_times} performs a kind of bubble sort which can be traced:
   808 {\footnotesize\begin{verbatim}
   809    ML> toggle trace_rewrite;
   810    val it = true : bool
   811    ML>
   812    ML> rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;
   813    ### trying thm 'radd_commute'
   814    ### not: "a + (b * (c * d) + e)" > "b * (c * d) + e + a"
   815    ### rewrite_set_: a + (e + b * (c * d))
   816    ### trying thm 'radd_commute'
   817    ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"
   818    ### not: "e + b * (c * d)" > "b * (c * d) + e"
   819    ### trying thm 'radd_left_commute'
   820    ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"
   821    ### trying thm 'radd_assoc'
   822    ### trying thm 'rmult_commute'
   823    ### not: "b * (c * d)" > "c * d * b"
   824    ### not: "c * d" > "d * c"
   825    ### trying thm 'rmult_left_commute'
   826    ### not: "b * (c * d)" > "c * (b * d)"
   827    ### trying thm 'rmult_assoc'
   828    ### trying thm 'radd_commute'
   829    ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"
   830    ### not: "e + b * (c * d)" > "b * (c * d) + e"
   831    ### trying thm 'radd_left_commute'
   832    ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"
   833    ### trying thm 'radd_assoc'
   834    ### trying thm 'rmult_commute'
   835    ### not: "b * (c * d)" > "c * d * b"
   836    ### not: "c * d" > "d * c"
   837    ### trying thm 'rmult_left_commute'
   838    ### not: "b * (c * d)" > "c * (b * d)"
   839    ### trying thm 'rmult_assoc'
   840    val it = Some ("a + (e + b * (c * d))",[]) : (string * string list) option     \end{verbatim}}%size
   841 Notice that {\tt +} is left-associative where the parentheses are omitted for {\tt (a + b) + c = a + b + c}, but not for {\tt a + (b + c)}. Ordered rewriting necessarily terminates with parentheses which could be omitted due to associativity.
   842 
   843 
   844 \chapter{The hierarchy of problem types}\label{pbt}
   845 \section{The standard-function for 'matching'}
   846 Matching \cite{nipk:rew-all-that} is a technique used within rewriting, and used by \isac{} also for (a generalized) 'matching' a problem with a problem type. The function which tests for matching has the following signature:
   847 {\footnotesize\begin{verbatim}
   848    ML> matches;
   849    val it = fn : theory -> term -> term -> bool
   850 \end{verbatim}}%size
   851 where the first of the two {\tt term} arguments is the particular term to be tested, and the second one is the pattern:
   852 {\footnotesize\begin{verbatim}
   853    ML> val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1";
   854    val t = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#1","RealDef.real") : term
   855    ML>
   856    ML> val p = (term_of o the o (parse thy)) "a * b^^^#2 = c";
   857    val p = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("c","RealDef.real") : term
   858    ML> atomt p;
   859    *** -------------
   860    *** Const ( op =)
   861    *** . Const ( op *)
   862    *** . . Free ( a, )
   863    *** . . Const ( RatArith.pow)
   864    *** . . . Free ( b, )
   865    *** . . . Free ( #2, )
   866    *** . Free ( c, )
   867    val it = () : unit
   868    ML>
   869    ML> mk_Var;
   870    val it = fn : term -> term
   871    ML>
   872    ML> val pat = mk_Var p;
   873    val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term
   874    ML> Sign.string_of_term (sign_of thy) pat;
   875    val it = "?a * ?b ^^^ #2 = ?c" : cterm' 
   876    ML> atomt pat;
   877    *** -------------
   878    *** Const ( op =)
   879    *** . Const ( op *)
   880    *** . . Var ((a, 0), )
   881    *** . . Const ( RatArith.pow)
   882    *** . . . Var ((b, 0), )
   883    *** . . . Free ( #2, )
   884    *** . Var ((c, 0), )
   885    val it = () : unit
   886 \end{verbatim}}%size % $ 
   887 Note that the pattern {\tt pat} contains so-called {\it scheme variables} decorated with a {\tt ?} (analoguous to theorems). The pattern is generated by the function {\tt mk_Var}. This format of the pattern is necessary in order to obtain results like these:
   888 {\footnotesize\begin{verbatim}
   889    ML> matches thy t pat;
   890    val it = true : bool
   891    ML>
   892    ML> val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1";
   893    val t2 = Const (#,#) $ (# $ # $ Free #) $ Free ("#1","RealDef.real") : term
   894    ML> matches thy t2 pat;
   895    val it = false : bool    
   896    ML>
   897    ML> val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v";
   898    val pat2 = Const (#,#) $ (# $ # $ Free #) $ Var ((#,#),"RealDef.real") : term
   899    ML> matches thy t2 pat2;
   900    val it = true : bool 
   901 \end{verbatim}}%size % $
   902 
   903 \section{Accessing the hierarchy}
   904 The hierarchy of problem types is encapsulated; it can be accessed by the following functions. {\tt show\_ptyps} retrieves all leaves of the hierarchy (here in an early version for testing):
   905 {\footnotesize\begin{verbatim}
   906    ML> show_ptyps;
   907    val it = fn : unit -> unit
   908    ML> show_ptyps();
   909    [
   910     ["e_pblID"],
   911     ["equation", "univariate", "linear"],
   912     ["equation", "univariate", "plain_square"],
   913     ["equation", "univariate", "polynomial", "degree_two", "pq_formula"],
   914     ["equation", "univariate", "polynomial", "degree_two", "abc_formula"],
   915     ["equation", "univariate", "squareroot"],
   916     ["equation", "univariate", "normalize"],
   917     ["equation", "univariate", "sqroot-test"],
   918     ["function", "derivative_of"],
   919     ["function", "maximum_of", "on_interval"],
   920     ["function", "make"],
   921     ["tool", "find_values"],
   922     ["functional", "inssort"]
   923    ]
   924    val it = () : unit
   925 \end{verbatim}}%size
   926 The retrieve function for individual problem types is {\tt get\_pbt}
   927 \footnote{A function providing better readable output is in preparation}. Note that its argument, the 'problem identifier' {\tt pblID}, has the strings listed in reverse order w.r.t. the hierarchy, i.e. from the leave to the root. This order makes the {\tt pblID} closer to a natural description:
   928 {\footnotesize\begin{verbatim}
   929    ML> get_pbt;
   930    val it = fn : pblID -> pbt
   931    ML> get_pbt ["squareroot", "univariate", "equation"];
   932    val it =
   933      {met=[("SqRoot.thy","square_equation")],
   934       model=[("#Given",(Const (#,#),Free (#,#))),
   935            ("#Given",(Const (#,#),Free (#,#))),
   936            ("#Given",(Const (#,#),Free (#,#))),
   937            ("#Find",(Const (#,#),Free (#,#)))],
   938       thy={ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,
   939             Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat,
   940             Arith, Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype,
   941             Numeral, Bin, IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option,
   942             Map, Record, RelPow, Sexp, String, Calculation, SVC_Oracle, Main,
   943             Zorn, Filter, PNat, PRat, PReal, RealDef, RealOrd, RealInt, RealBin,
   944             HyperDef, Descript, ListG, Tools, Script, Typefix, Atools, RatArith,
   945             SqRoot},
   946       where_=[Const ("SqRoot.contains'_root","bool => bool") $
   947               Free ("e_","bool")]} : pbt
   948 \end{verbatim}}%size %$
   949 where the records fields hold the following data:
   950 \begin{description}
   951 \item [\tt thy]: the theory necessary for parsing the formulas
   952 \item [\tt model]: the items of the problem type, divided into those {\tt Given}, the precondition {\tt Where} and the output item(s) {\tt Find}. The items of {\tt Given} and {\tt Find} are all headed by so-called descriptions, which determine the type. These descriptions are defined in {\tt [isac-src]/Isa99/Descript.thy}.
   953 \item [\tt met]: the list of methods solving this problem type.\\
   954 \end{description}
   955 
   956 The following function adds or replaces a problem type (after having it prepared using {\tt prep\_pbt})
   957 {\footnotesize\begin{verbatim}
   958    ML> store_pbt;
   959    val it = fn : pbt * pblID -> unit
   960    ML> store_pbt
   961     (prep_pbt SqRoot.thy
   962     (["newtype","univariate","equation"],
   963      [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),
   964       ("#Where" ,["contains_root (e_::bool)"]),
   965       ("#Find"  ,["solutions v_i_"])
   966      ],
   967      [("SqRoot.thy","square_equation")]));
   968    val it = () : unit
   969 \end{verbatim}}%size
   970 When adding a new type with argument {\tt pblID}, an immediate parent must already exist in the hierarchy (this is the one with the tail of {\tt pblID}).
   971 
   972 \section{Internals of the datastructure}
   973 This subsection only serves for the implementation of the hierarchy browser and can be skipped by the authors of math knowledge.
   974 
   975 A problem type is described by the following record type (in the file {\tt [isac-src]/globals.sml}, the respective functions are in {\tt [isac-src]/ME/ptyps.sml}), and held in a global reference variable:
   976 {\footnotesize\begin{verbatim}
   977    type pbt = 
   978         {thy   : theory,       (* the nearest to the root,
   979                                   which allows to compile that pbt  *)
   980          where_: term list,    (* where - predicates                *)
   981          model   : ((string *    (* fields "#Given","#Find"           *)
   982                    (term *     (* description                       *)
   983                     term))     (* id                                *)
   984                       list),                                        
   985          met   : metID list};  (* methods solving the pbt           *)
   986    datatype ptyp = 
   987             Ptyp of string *   (* key within pblID                  *)
   988                     pbt list * (* several pbts with different domIDs*)
   989                     ptyp list;
   990    val e_Ptyp = Ptyp ("empty",[],[]);
   991    
   992    type ptyps = ptyp list;
   993    val ptyps = ref ([e_Ptyp]:ptyps);
   994 \end{verbatim}}%size
   995 The predicates in {\tt where\_} (i.e. the preconditions) usually are defined in the respective theory in {\tt[isac-src]/knowledge}. Most of the predicates are not defined by rewriting, but by SML-code contained in the respective {\tt *.ML} file.
   996 
   997 Each item is headed by a so-called description which provides some guidance for interactive input. The descriptions are defined in {\tt[isac-src]/Isa99/Descript.thy}.
   998 
   999 
  1000 
  1001 \section{Match a formalization with a problem type}\label{pbl}
  1002 A formalization is {\it match}ed with a problem type which yields a problem. A formal description of this kind of {\it match}ing can be found in \\{\tt ftp://ft.ist.tugraz.at/projects/isac/publ/calculemus01.ps.gz}. A formalization of an equation is e.g.
  1003 {\footnotesize\begin{verbatim}
  1004    ML> val fmz = ["equality (#1 + #2 * x = #0)",
  1005                   "solveFor x",
  1006                   "solutions L"] : fmz;
  1007    val fmz = ["equality (#1 + #2 * x = #0)","solveFor x","solutions L"] : fmz
  1008 \end{verbatim}}%size
  1009 Given a formalization (and a specification of the problem, i.e. a theory, a problemtype, and a method) \isac{} can solve the respective problem automatically. The formalization must match the problem type for this purpose:
  1010 {\footnotesize\begin{verbatim}
  1011    ML> by_formalise;
  1012    val it = fn : fmz -> pbt -> match'
  1013    ML>
  1014    ML> by_formalise fmz (get_pbt ["univariate","equation"]);
  1015    val it =
  1016      Matches'
  1017        {Find=[Correct "solutions L"],
  1018         Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
  1019         Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]}
  1020      : match'
  1021    ML>
  1022    ML> by_formalise fmz (get_pbt ["linear","univariate","equation"]);
  1023    val it =
  1024      Matches'
  1025        {Find=[Correct "solutions L"],
  1026         Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],
  1027         Relate=[],
  1028         Where=[Correct
  1029                  "matches (          x = #0) (#1 + #2 * x = #0) |
  1030                   matches (     ?b * x = #0) (#1 + #2 * x = #0) |
  1031                   matches (?a      + x = #0) (#1 + #2 * x = #0) |
  1032                   matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"],
  1033         With=[]} : match'
  1034    ML>
  1035    ML> by_formalise fmz (get_pbt ["squareroot","univariate","equation"]);
  1036    val it =
  1037      NoMatch'
  1038        {Find=[Correct "solutions L"],
  1039         Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x",
  1040                Missing "errorBound err_"],Relate=[],
  1041         Where=[False "contains_root #1 + #2 * x = #0 "],With=[]} : match'
  1042 \end{verbatim}}%size
  1043 The above formalization does not match the problem type \\{\tt["squareroot","univariate","equation"]} which is explained by the tags:
  1044 \begin{tabbing}
  1045 123\=\kill
  1046 \> {\tt Missing:} the item is missing in the formalization as required by the problem type\\
  1047 \> {\tt Superfl:} the item is not required by the problem type\\
  1048 \> {\tt Correct:} the item is correct, or the precondition ({\tt Where}) is true\\
  1049 \> {\tt False:} the precondition ({\tt Where}) is false\\
  1050 \> {\tt Incompl:} the item is incomlete, or not yet input.\\
  1051 \end{tabbing}
  1052 
  1053 
  1054 
  1055 \section{Refine a problem specification}
  1056 The challenge in constructing the problem hierarchy is, to design the branches in such a way, that problem refinement can be done automatically (as it is done in algebra system e.g. by a internal hierarchy of equations).
  1057 
  1058 For this purpose the hierarchy must be built using the following rules: Let $F$ be a formalization and $P$ and $P_i,\:i=1\cdots n$ problem types, where the $P_i$ are specialized problem types w.r.t. $P$ (i.e. $P$ is a parent node of $P_i$), then
  1059 {\small
  1060 \begin{enumerate}
  1061 \item for all $F$ matching some $P_i$ must follow, that $F$ matches $P$
  1062 \item an $F$ matching $P$ should not have more than {\em one} $P_i,\:i=1\cdots n-1$ with $F$ matching $P_i$ (if there are more than one $P_i$, the first one will be taken)
  1063 \item for all $F$ matching some $P$ must follow, that $F$ matches $P_n$\\
  1064 \end{enumerate}}%small
  1065 \noindent Let us give an example for the point (1.) and (2.) first:
  1066 {\footnotesize\begin{verbatim}
  1067    ML> refine;
  1068    val it = fn : fmz -> pblID -> match list
  1069    ML>
  1070    ML> val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
  1071               "solveFor x","errorBound (eps=#0)",
  1072               "solutions L"];
  1073    ML>
  1074    ML> refine fmz ["univariate","equation"];
  1075    *** pass ["equation","univariate"]
  1076    *** pass ["equation","univariate","linear"]
  1077    *** pass ["equation","univariate","plain_square"]
  1078    *** pass ["equation","univariate","polynomial"]
  1079    *** pass ["equation","univariate","squareroot"]
  1080    val it =
  1081      [Matches
  1082         (["univariate","equation"],
  1083          {Find=[Correct "solutions L"],
  1084           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
  1085                  Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
  1086           Where=[Correct
  1087                    "matches (?a = ?b) (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"],
  1088           With=[]}),
  1089       NoMatch
  1090         (["linear","univariate","equation"],
  1091          {Find=[Correct "solutions L"],
  1092           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
  1093                  Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
  1094           Where=[False "(?a + ?b * x = #0) (sqrt (#9 + #4 * x#"],
  1095           With=[]}),
  1096       NoMatch
  1097         (["plain_square","univariate","equation"],
  1098          {Find=[Correct "solutions L"],
  1099           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
  1100                  Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
  1101           Where=[False
  1102                    "matches (?a + ?b * x ^^^ #2 = #0)"],
  1103           With=[]}),
  1104       NoMatch
  1105         (["polynomial","univariate","equation"],
  1106          {Find=[Correct "solutions L"],
  1107           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
  1108                  Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],
  1109           Where=[False 
  1110                  "is_polynomial_in sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) x"],
  1111           With=[]}),
  1112       Matches
  1113         (["squareroot","univariate","equation"],
  1114          {Find=[Correct "solutions L"],
  1115           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",
  1116                  Correct "solveFor x",Correct "errorBound (eps = #0)"],Relate=[],
  1117           Where=[Correct
  1118                    "contains_root sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) "],
  1119           With=[]})] : match list
  1120 \end{verbatim}}%size}%footnotesize\label{refine}
  1121 This example shows, that in order to refine an {\tt["univariate","equation"]}, the formalization must match respective respective problem type (rule (1.)) and one of the descendants which should match selectively (rule (2.)).
  1122 
  1123 If no one of the descendants of {\tt["univariate","equation"]} match, rule (3.) comes into play: The {\em last} problem type on this level ($P_n$) provides for a special 'problem type' {\tt["normalize"]}. This node calls a method transforming the equation to a (or another) normal form, which then may match. Look at this example:
  1124 {\footnotesize\begin{verbatim}
  1125    ML>  val fmz = ["equality (x+#1=#2)",
  1126                "solveFor x","errorBound (eps=#0)",
  1127                "solutions L"];
  1128    [...]
  1129    ML>
  1130    ML>  refine fmz ["univariate","equation"];
  1131    *** pass ["equation","univariate"]
  1132    *** pass ["equation","univariate","linear"]
  1133    *** pass ["equation","univariate","plain_square"]
  1134    *** pass ["equation","univariate","polynomial"]
  1135    *** pass ["equation","univariate","squareroot"]
  1136    *** pass ["equation","univariate","normalize"]
  1137    val it =
  1138      [Matches
  1139         (["univariate","equation"],
  1140          {Find=[Correct "solutions L"],
  1141           Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
  1142                  Superfl "errorBound (eps = #0)"],Relate=[],
  1143           Where=[Correct "matches (?a = ?b) (x + #1 = #2)"],With=[]}),
  1144       NoMatch
  1145         (["linear","univariate","equation"],
  1146    [...]
  1147           With=[]}),
  1148       NoMatch
  1149         (["squareroot","univariate","equation"],
  1150          {Find=[Correct "solutions L"],
  1151           Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
  1152                  Correct "errorBound (eps = #0)"],Relate=[],
  1153           Where=[False "contains_root x + #1 = #2 "],With=[]}),
  1154       Matches
  1155         (["normalize","univariate","equation"],
  1156          {Find=[Correct "solutions L"],
  1157           Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",
  1158                  Superfl "errorBound (eps = #0)"],Relate=[],Where=[],With=[]})]
  1159      : match list
  1160 \end{verbatim}}%size
  1161 The problem type $P_n$, {\tt["normalize","univariate","equation"]}, will transform the equation {\tt x + \#1 = \#2} to the normal form {\tt \#-1 + x = \#0}, which then will match {\tt["linear","univariate","equation"]}.
  1162 
  1163 This recursive search on the problem hierarchy can be  done within a proof state. This leads to the next section.
  1164 
  1165 
  1166 \chapter{Methods}
  1167 A problem type can have one ore more methods solving a respective problem. A method is described by means of another new program language. The language itself looks like a simple functional language, but constructs an imperative proof-state behind the scenes (thus liberating the programer from dealing with technical details and also prohibiting incorrect construction of the proof tree). The interpreter of 'scripts' written in this language evaluates the scriptexpressions, and also delivers certain parts of the script itself for discussion with the user.
  1168 
  1169 \section{The scripts' syntax}
  1170 The syntax of scripts follows the definition given in Backus-normal-form:
  1171 {\it
  1172 \begin{tabbing}
  1173 123\=123\=expr ::=\=$|\;\;$\=\kill
  1174 \>script ::= {\tt Script} id arg$\,^*$ = body\\
  1175 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
  1176 \>\>body ::= expr\\
  1177 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
  1178 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
  1179 \>\>\>$|\;$\>listexpr\\
  1180 \>\>\>$|\;$\>id\\
  1181 \>\>\>$|\;$\>seqex id\\
  1182 \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
  1183 \>\>\>$|\;$\>{\tt Repeat} seqex\\
  1184 \>\>\>$|\;$\>{\tt Try} seqex\\
  1185 \>\>\>$|\;$\>seqex {\tt Or} seqex\\
  1186 \>\>\>$|\;$\>seqex {\tt @@} seqex\\
  1187 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
  1188 \>\>type ::= id\\
  1189 \>\>tac ::= id
  1190 \end{tabbing}}
  1191 where {\it id} is an identifier with the usual syntax, {\it prop} is a proposition constructed by Isabelles logical operators (see \cite{Isa-obj} {\tt [isabelle]/src/HOL/HOL.thy}), {\it listexpr} (called {\bf list-expression}) is constructed by Isabelles list functions like {\tt hd, tl, nth} described in {\tt [isabelle]/src/HOL/List.thy}, and {\it type} are (virtually) all types declared in Isabelles version 99.
  1192 
  1193 Expressions containing some of the keywords {\tt let}, {\tt if} etc. are called {\bf script-expressions}.
  1194 
  1195 Tactics {\it tac} are (curried) functions. For clarity and simplicity reasons, {\it listexpr} must not contain a {\it tac}, and {\it tac}s must not be nested,
  1196 
  1197 
  1198 \section{Control the flow of evaluation}
  1199 The flow of control is managed by the following script-expressions called {\it tacticals}.
  1200 \begin{description}
  1201 \item{{\tt while} prop {\tt Do} expr id} 
  1202 \item{{\tt if} prop {\tt then} expr {\tt else} expr}
  1203 \end{description}
  1204 While the the above script-expressions trigger the flow of control by evaluating the current formula, the other expressions depend on the applicability of the tactics within their respective subexpressions (which in turn depends on the proofstate)
  1205 \begin{description}
  1206 \item{{\tt Repeat} expr id}
  1207 \item{{\tt Try} expr id}
  1208 \item{expr {\tt Or} expr id}
  1209 \item{expr {\tt @@} expr id}
  1210 \end{description}
  1211 
  1212 \begin{description}
  1213 \item xxx
  1214 
  1215 \end{description}
  1216 
  1217 \chapter{Do a calculational proof}
  1218 First we list all the tactics available so far (this list may be extended during further development of \isac).
  1219 
  1220 \section{Tactics for doing steps in calculations}
  1221 \input{tactics}
  1222 
  1223 \section{The functionality of the math engine}
  1224 A proof is being started in the math engine {\tt me} by the tactic
  1225 \footnote{In the present version a tactic is of type {\tt mstep}.}
  1226  {\tt Init\_Proof}, and interactively promoted by other tactics. On input of each tactic the {\tt me} returns the resulting formula and the next tactic applicable. The proof is finished, when the {\tt me} proposes {\tt End\_Proof} as the next tactic.
  1227 
  1228 We show a calculation (calculational proof) concerning equation solving, where the type of equation is refined automatically: The equation is given by the respective formalization ...
  1229 {\footnotesize\begin{verbatim}
  1230    ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
  1231                   "errorBound (eps=#0)","solutions L"];
  1232    val fmz =
  1233      ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
  1234       "solutions L"] : string list
  1235    ML>
  1236    ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
  1237                                  ("SqRoot.thy","no_met"));
  1238    val dom = "SqRoot.thy" : string
  1239    val pbt = ["univariate","equation"] : string list
  1240    val met = ("SqRoot.thy","no_met") : string * string
  1241 \end{verbatim}}%size
  1242 ... and the specification {\tt spec} of a domain {\tt dom}, a problem type {\tt pbt} and a method {\tt met}. Note that the equation is such, that it is not immediatly clear, what type it is in particular (it could be a polynomial of degree 2; but, for sure, the type is some specialized type of a univariate equation). Thus, no method ({\tt no\_met}) can be specified for solving the problem.
  1243 
  1244 Nevertheless this specification is sufficient for automatically solving the equation --- the appropriate method will be found by refinement within the hierarchy of problem types.
  1245 
  1246 
  1247 \section{Initialize the calculation}
  1248 The start of a new proof requires the following initializations: The proof state is given by a proof tree {\tt ctree} and a position {\tt pos'}; both are empty at the beginning. The tactic {\tt Init\_Proof} is, like all other tactics, paired with an identifier of type {\tt string} for technical reasons.
  1249 {\footnotesize\begin{verbatim}
  1250    ML>  val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
  1251    val mID = "Init_Proof" : string
  1252    val m =
  1253      Init_Proof
  1254        (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
  1255          "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep
  1256    ML>
  1257    ML>  val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;
  1258    val p = ([],Pbl) : pos'
  1259    val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
  1260    val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
  1261      : string * mstep
  1262    val pt =
  1263      Nd
  1264        (PblObj
  1265           {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
  1266            result=#,spec=#},[]) : ctree
  1267    \end{verbatim}}%size
  1268 The mathematics engine {\tt me} returns the resulting formula {\tt f} of type {\tt mout} (which in this case is a problem), the next tactic {\tt nxt}, and a new proof state ({\tt ctree}, {\tt pos'}).
  1269 
  1270 We can convince ourselves, that the problem is still empty, by increasing {\tt Compiler.Control.Print.printDepth}:
  1271 {\footnotesize\begin{verbatim}
  1272    ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
  1273    val it = () : unit
  1274    ML>
  1275    ML> f;
  1276    val it =
  1277      Form'
  1278        (PpcKF
  1279           (0,EdUndef,0,Nundef,
  1280            (Problem [],
  1281             {Find=[Incompl "solutions []"],
  1282              Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
  1283              Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
  1284 \end{verbatim}}%size
  1285 Recall, please, the format of a problem as presented in sect.\ref{pbl} on p.\pageref{pbl}; such an 'empty' problem can be found above encapsulated by several constructors containing additional data (necessary for the dialog guide, not relevant here).\\
  1286 
  1287 {\it In the sequel we will omit output of the {\tt me} if it is not important for the respective context}.\\
  1288 
  1289 In general, the dialog guide will hide the following two tactics {\tt Refine\_Tacitly} and {\tt Model\_Problem} from the user.
  1290 {\footnotesize\begin{verbatim}
  1291    ML>  nxt;
  1292    val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
  1293      : string * mstep
  1294    ML>
  1295    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1296    val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])
  1297      : string * mstep
  1298    ML>
  1299    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1300 \end{verbatim}}%size
  1301 
  1302 
  1303 \section{The phase of modeling} 
  1304 comprises the input of the items of the problem; the {\tt me} can help by use of the formalization tacitly transferred by {\tt Init\_Proof}. In particular, the {\tt me} in general 'knows' the next promising tactic; the first one has been returned by the (hidden) tactic {\tt Model\_Problem}.
  1305 
  1306 {\footnotesize\begin{verbatim}
  1307    ML>  nxt;
  1308    val it =
  1309      ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
  1310      : string * mstep
  1311    ML>
  1312    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1313    val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep
  1314    ML>
  1315    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1316    val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep
  1317    ML>
  1318    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 
  1319    val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
  1320 \end{verbatim}}%size
  1321 \noindent Now the problem is 'modeled', all items are input. We convince ourselves by increasing {\tt Compiler.Control.Print.printDepth} once more.
  1322 {\footnotesize\begin{verbatim}
  1323    ML>  Compiler.Control.Print.printDepth:=8;
  1324    ML>  f;
  1325    val it =
  1326      Form'
  1327        (PpcKF
  1328           (0,EdUndef,0,Nundef,
  1329            (Problem [],
  1330             {Find=[Correct "solutions L"],
  1331              Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
  1332                     Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
  1333 \end{verbatim}}%size
  1334 %One of the input items is considered {\tt Superfluous} by the {\tt me} consulting the problem type {\tt ["univariate","equation"]}. The {\tt ErrorBound}, however, could become important in case the equation only could be solved by some iteration method.
  1335 
  1336 \section{The phase of specification} 
  1337 This phase provides for explicit determination of the domain, the problem type, and the method to be used. In particular, the search for the appropriate problem type is being supported. There are two tactics for this purpose: {\tt Specify\_Problem} generates feedback on how a candidate of a problem type matches the current problem, and {\tt Refine\_Problem} provides help by the system, if the user gets lost.
  1338 {\footnotesize\begin{verbatim}
  1339 ML> nxt;
  1340    val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
  1341    ML>
  1342    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1343    val nxt =
  1344      ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"])
  1345      : string * mstep
  1346    val pt =
  1347      Nd
  1348        (PblObj
  1349           {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
  1350               result=#,spec=#},[]) : ctree
  1351 \end{verbatim}}%size
  1352 The {\tt me} is smart enough to know the appropriate problem type (transferred tacitly with {\tt Init\_Proof}). In order to challenge the student, the dialog guide may hide this information; then the {\tt me} works as follows.
  1353 {\footnotesize\begin{verbatim}
  1354    ML> val nxt = ("Specify_Problem",
  1355                Specify_Problem ["polynomial","univariate","equation"]);
  1356    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1357    val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
  1358    val nxt =
  1359      ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"])
  1360      : string * mstep
  1361    ML>
  1362    ML> val nxt = ("Specify_Problem",
  1363                Specify_Problem ["linear","univariate","equation"]);
  1364    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1365    val f =
  1366      Form'
  1367        (PpcKF
  1368           (0,EdUndef,0,Nundef,
  1369            (Problem ["linear","univariate","equation"],
  1370             {Find=[Correct "solutions L"],
  1371              Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
  1372                     Correct "solveFor x"],Relate=[],
  1373              Where=[False
  1374                     "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
  1375              With=[]}))) : mout 
  1376 \end{verbatim}}%size
  1377 Again assuming that the dialog guide hide the next tactic proposed by the {\tt me}, and the student gets lost, {\tt Refine\_Problem} always 'knows' the way out, if applied to the problem type {\tt["univariate","equation"]}.
  1378 {\footnotesize\begin{verbatim}
  1379    ML> val nxt = ("Refine_Problem",
  1380                   Refine_Problem ["linear","univariate","equation
  1381    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1382    val f = Problems (RefinedKF [NoMatch #]) : mout
  1383    ML>
  1384    ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
  1385    val f =
  1386      Problems
  1387        (RefinedKF
  1388           [NoMatch
  1389              (["linear","univariate","equation"],
  1390               {Find=[Correct "solutions L"],
  1391                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
  1392                       Correct "solveFor x"],Relate=[],
  1393                Where=[False
  1394                      "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
  1395                With=[]})]) : mout
  1396    ML>
  1397    ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
  1398    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1399    val f =
  1400      Problems
  1401        (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])
  1402      : mout
  1403    ML>
  1404    ML>
  1405    ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
  1406    val f =
  1407      Problems
  1408        (RefinedKF
  1409           [Matches
  1410              (["univariate","equation"],
  1411               {Find=[Correct "solutions L"],
  1412                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
  1413                       Correct "solveFor x"],Relate=[],
  1414                Where=[Correct
  1415                With=[]}),
  1416            NoMatch
  1417              (["linear","univariate","equation"],
  1418               {Find=[Correct "solutions L"],
  1419                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
  1420                       Correct "solveFor x"],Relate=[],
  1421                Where=[False
  1422                       "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
  1423                   With=[]}),
  1424            NoMatch
  1425              ...
  1426              ...   
  1427            Matches
  1428              (["normalize","univariate","equation"],
  1429               {Find=[Correct "solutions L"],
  1430                Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
  1431                       Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
  1432 \end{verbatim}}%size
  1433 The tactic {\tt Refine\_Problem} returns all matches to problem types along the path traced in the problem hierarchy (anlogously to the authoring tool for refinement in sect.\ref{refine} on p.\pageref{refine}) --- a lot of information to be displayed appropriately in the hiearchy browser~!
  1434 
  1435 \section{The phase of solving} 
  1436 This phase starts by invoking a method, which acchieves the normal form within two tactics, {\tt Rewrite rnorm\_equation\_add} and {\tt Rewrite\_Set SqRoot\_simplify}:
  1437 {\footnotesize\begin{verbatim} 
  1438    ML> nxt;
  1439    val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
  1440      : string * mstep
  1441    ML>
  1442    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1443    val f =
  1444      Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8"))
  1445    val nxt =
  1446      ("Rewrite", Rewrite
  1447         ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)"))
  1448    ML>
  1449    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1450    val f =
  1451      Form' (FormKF (~1,EdUndef,1,Nundef,
  1452            "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout
  1453    val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep
  1454    ML>
  1455    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1456    val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
  1457    val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
  1458 \end{verbatim}}%size
  1459 Now the normal form {\tt \#-6 + \#3 * x = \#0} is the input to a subproblem, which again allows for specification of the type of equation, and the respective method:
  1460 {\footnotesize\begin{verbatim}
  1461    ML> nxt;
  1462    val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
  1463    ML>   
  1464    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1465    val f =
  1466      Form' (FormKF
  1467           (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])"))
  1468      : mout
  1469    val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
  1470    ML>
  1471    ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1472    val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
  1473 \end{verbatim}}%size
  1474 As required, the tactic {\tt Refine ["univariate","equation"]} selects the appropriate type of equation from the problem hierarchy, which can be seen by the tactic {\tt Model\_Problem ["linear","univariate","equation"]} prosed by the system.
  1475 
  1476 Again the whole phase of modeling and specification follows; we skip it here, and \isac's dialog guide may decide to do so as well.
  1477 
  1478 
  1479 \section{The final phase: check the post-condition}
  1480 The type of problems solved by \isac{} are so-called 'example construction problems' as shown above. The most characteristic point of such a problem is the post-condition. The handling of the post-condition in the given context is an open research question.
  1481 
  1482 Thus the post-condition is just mentioned, in our example for both, the problem and the subproblem:
  1483 {\footnotesize\begin{verbatim}
  1484    ML> nxt;
  1485    val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
  1486    ML>
  1487    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1488    val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout
  1489    val nxt =
  1490      ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"])
  1491    ML>
  1492    ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
  1493    val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
  1494    val nxt = ("End_Proof'",End_Proof') : string * mstep
  1495 \end{verbatim}}%size
  1496 The next tactic proposed by the system, {\tt End\_Proof'} indicates that the proof has finished successfully.\\
  1497 
  1498 {\it The tactics proposed by the system need {\em not} be followed by the user; the user is free to choose other tactics, and the system will report, if this is applicable at the respective proof state, or not~! The reader may try out~!}
  1499 
  1500 
  1501 
  1502 \part{Systematic description}
  1503 
  1504 
  1505 \chapter{The structure of the knowledge base}
  1506 
  1507 \section{Tactics and data}
  1508 First we view the ME from outside, i.e. we regard tactics and relate them to the knowledge base (KB). W.r.t. the KB we address the atomic items which have to be implemented in detail by the authors of the KB
  1509 \footnote{Some of these items are fetched by the tactics from intermediate storage within the ME, and not directly from the KB.}
  1510 . The items are listed in alphabetical order in Tab.\ref{kb-items} on p.\pageref{kb-items}.
  1511 {\begin{table}[h]
  1512 \caption{Atomic items of the KB} \label{kb-items}
  1513 %\tabcolsep=0.3mm
  1514 \begin{center}
  1515 \def\arraystretch{1.0}
  1516 \begin{tabular}{lp{9.0cm}}
  1517 abbrevation & description \\
  1518 \hline
  1519 &\\
  1520 {\it calc\_list}
  1521 & associationlist of the evaluation-functions {\it eval\_fn}\\
  1522 {\it eval\_fn}
  1523 & evaluation-function for numerals and for predicates coded in SML\\
  1524 {\it eval\_rls   }
  1525 & ruleset {\it rls} for simplifying expressions with {\it eval\_fn}s\\
  1526 {\it fmz}
  1527 & formalization, i.e. a minimal formula representation of an example \\
  1528 {\it met}
  1529 & a method, i.e. a datastructure holding all informations for the solving phase ({\it rew\_ord}, {\it program}, etc.)\\
  1530 {\it metID}
  1531 & reference to a {\it met}\\
  1532 {\it op}
  1533 & operator as key to an {\it eval\_fn} in a {\it calc\_list}\\
  1534 {\it pbl}
  1535 & problem, i.e. a node in the problem-hierarchy\\
  1536 {\it pblID}
  1537 & reference to a {\it pbl}\\
  1538 {\it rew\_ord}
  1539 & rewrite-order\\
  1540 {\it rls}
  1541 & ruleset, i.e. a datastructure holding theorems {\it thm} and operators {\it op} for simplification (with a {\it rew\_ord})\\
  1542 {\it Rrls}
  1543 & ruleset for 'reverse rewriting' (an \isac-technique generating stepwise rewriting, e.g. for cancelling fractions)\\
  1544 {\it program}
  1545 & script describing algorithms by tactics, part of a {\it met} \\
  1546 {\it norm\_rls}
  1547 & special ruleset calculating a normalform, associated with a {\it thy}\\
  1548 {\it spec}
  1549 & specification, i.e. a tripel ({\it thyID, pblID, metID})\\
  1550 {\it subs}
  1551 & substitution, i.e. a list of variable-value-pairs\\
  1552 {\it term}
  1553 & Isabelle term, i.e. a formula\\
  1554 {\it thm}
  1555 & theorem\\     
  1556 {\it thy}
  1557 & theory\\
  1558 {\it thyID}
  1559 & reference to a {\it thy} \\
  1560 \end{tabular}\end{center}\end{table}
  1561 }
  1562 The relations between tactics and data items are shown in Tab.\ref{tac-kb}on p.\pageref{tac-kb}.
  1563 {\def\arraystretch{1.2}
  1564 \begin{table}[h]
  1565 \caption{Which tactic uses which KB's item~?} \label{tac-kb}
  1566 \tabcolsep=0.3mm
  1567 \begin{center}
  1568 \begin{tabular}{|ll||cccc|ccc|cccc|} \hline
  1569 tactic  &input &    &    &    &norm\_&   &rew\_&rls &eval\_&eval\_&calc\_&   \\
  1570         &      &thy &program &Rrls&rls  &thm &ord  &Rrls&fn    &rls   &list  &dsc\\
  1571 \hline\hline
  1572 Init\_Proof
  1573         &fmz   & x  &    &    & x   &    &     &    &      &      &      & x \\
  1574         &spec  &    &    &    &     &    &     &    &      &      &      &   \\
  1575 \hline
  1576 \multicolumn{13}{|l|}{model phase}\\
  1577 \hline
  1578 Add\_*  &term  & x  &    &    & x   &    &     &    &      &      &      & x \\
  1579 FormFK  &model & x  &    &    & x   &    &     &    &      &      &      & x \\
  1580 \hline
  1581 \multicolumn{13}{|l|}{specify phase}\\
  1582 \hline
  1583 Specify\_Theory 
  1584         &thyID & x  &    &    & x   &    &     &    & x    & x    &      & x \\
  1585 Specify\_Problem 
  1586         &pblID & x  &    &    & x   &    &     &    & x    & x    &      & x \\
  1587 Refine\_Problem 
  1588            &pblID & x  &    &    & x   &    &     &    & x    & x    &      & x \\
  1589 Specify\_Method 
  1590         &metID & x  &    &    & x   &    &     &    & x    & x    &      & x \\
  1591 Apply\_Method 
  1592         &metID & x  & x  &    & x   &    &     &    & x    & x    &      & x \\
  1593 \hline
  1594 \multicolumn{13}{|l|}{solve phase}\\
  1595 \hline
  1596 Rewrite,\_Inst 
  1597         &thm   & x  & x  &    &     & x  &met  &    & x    &met   &      &   \\
  1598 Rewrite, Detail
  1599         &thm   & x  & x  &    &     & x  &rls  &    & x    &rls   &      &   \\
  1600 Rewrite, Detail
  1601         &thm   & x  & x  &    &     & x  &Rrls &    & x    &Rrls  &      &   \\
  1602 Rewrite\_Set,\_Inst
  1603         &rls   & x  & x  &    &     &    &     & x  & x    & x    &      &   \\
  1604 Calculate  
  1605         &op    & x  & x  &    &     &    &     &    &      &      & x    &   \\
  1606 Substitute 
  1607         &subs  & x  &    &    & x   &    &     &    &      &      &      &   \\
  1608         &      &    &    &    &     &    &     &    &      &      &      &   \\
  1609 SubProblem 
  1610         &spec  & x  & x  &    & x   &    &     &    & x    & x    &      & x \\
  1611         &fmz   &    &    &    &     &    &     &    &      &      &      &   \\
  1612 \hline
  1613 \end{tabular}\end{center}\end{table}
  1614 }
  1615 
  1616 \section{\isac's theories}
  1617 \isac's theories build upon Isabelles theories for high-order-logic (HOL) up to the respective development of real numbers ({\tt HOL/Real}). Theories have a special format defined in \cite{Isa-ref} and the suffix {\tt *.thy}; usually theories are paired with SML-files having the same filename and the suffix {\tt *.ML}.
  1618 
  1619 \isac's theories represent the deductive part of \isac's knowledge base, the hierarchy of theories is structured accordingly. The {\tt *.ML}-files, however, contain {\em all} data of the other two axes of the knowledge base, the problems and the methods (without presenting their respective structure, which is done by the problem browser and the method browser, see \ref{pbt}).
  1620 
  1621 Tab.\ref{theories} on p.\pageref{theories} lists the basic theories planned to be implemented in version \isac.1. We expext the list to be expanded in the near future, actually, have a look to the theory browser~!
  1622 
  1623 The first three theories in the list do {\em not} belong to \isac's knowledge base; they are concerned with \isac's script-language for methods and listed here for completeness.
  1624 {\begin{table}[h]
  1625 \caption{Theories in \isac-version I} \label{theories}
  1626 %\tabcolsep=0.3mm
  1627 \begin{center}
  1628 \def\arraystretch{1.0}
  1629 \begin{tabular}{lp{9.0cm}}
  1630 theory & description \\
  1631 \hline
  1632 &\\
  1633 ListI.thy
  1634 & assigns identifiers to the functions defined in {\tt Isabelle2002/src/HOL/List.thy} and (intermediatly~?) defines some more list functions\\
  1635 ListI.ML
  1636 & {\tt eval\_fn} for the additional list functions\\
  1637 Tools.thy
  1638 & functions required for the evaluation of scripts\\
  1639 Tools.ML
  1640 & the respective {\tt eval\_fn}s\\
  1641 Script.thy
  1642 & prerequisites for scripts: types, tactics, tacticals,\\
  1643 Script.ML
  1644 & sets of tactics and functions for internal use\\
  1645 & \\
  1646 \hline
  1647 & \\
  1648 Typefix.thy
  1649 & an intermediate hack for escaping type errors\\
  1650 Descript.thy
  1651 & {\it description}s for the formulas in {\it model}s and {\it problem}s\\
  1652 Atools
  1653 & (re-)definition of operators; general predicates and functions for preconditions; theorems for the {\tt eval\_rls}\\
  1654 Float
  1655 & floating point numerals\\
  1656 Equation
  1657 & basic notions for equations and equational systems\\
  1658 Poly
  1659 & polynomials\\
  1660 PolyEq
  1661 & polynomial equations and equational systems \\
  1662 Rational.thy
  1663 & additional theorems for rationals\\
  1664 Rational.ML
  1665 & cancel, add and simplify rationals using (a generalization of) Euclids algorithm; respective reverse rulesets\\
  1666 RatEq
  1667 & equations on rationals\\
  1668 Root
  1669 & radicals; calculate normalform; respective reverse rulesets\\
  1670 RootEq
  1671 & equations on roots\\
  1672 RatRootEq
  1673 & equations on rationals and roots (i.e. on terms containing both operations)\\
  1674 Vect
  1675 & vector analysis\\
  1676 Trig
  1677 & trigonometriy\\
  1678 LogExp
  1679 & logarithms and exponential functions\\
  1680 Calculus
  1681 & nonstandard analysis\\
  1682 Diff
  1683 & differentiation\\
  1684 DiffApp
  1685 & applications of differentiaten (maxima-minima-problems)\\
  1686 Test
  1687 & (old) data for the test suite\\
  1688 Isac
  1689 & collects all \isac-theoris.\\
  1690 \end{tabular}\end{center}\end{table}
  1691 }
  1692 
  1693 
  1694 \section{Data in {\tt *.thy}- and {\tt *.ML}-files}
  1695 As already mentioned, theories come in pairs of {\tt *.thy}- and {\tt *.ML}-files with the same respective filename. How data are distributed between the two files is shown in Tab.\ref{thy-ML} on p.\pageref{thy-ML}.
  1696 {\begin{table}[h]
  1697 \caption{Data in {\tt *.thy}- and {\tt *.ML}-files} \label{thy-ML}
  1698 \tabcolsep=2.0mm
  1699 \begin{center}
  1700 \def\arraystretch{1.0}
  1701 \begin{tabular}{llp{7.7cm}}
  1702 file & data & description \\
  1703 \hline
  1704 & &\\
  1705 {\tt *.thy}
  1706 & consts 
  1707 & operators, predicates, functions, script-names ('{\tt Script} name \dots{\tt arguments}')
  1708 \\
  1709 & rules  
  1710 & theorems: \isac{} uses Isabelles theorems if possible; additional theorems analoguous to such existing in Isabelle get the Isabelle-identifier attached an {\it I}
  1711 \\& &\\
  1712 {\tt *.ML}
  1713 & {\tt theory' :=} 
  1714 & the theory defined by the actual {\tt *.thy}-file is made accessible to \isac
  1715 \\
  1716 & {\tt eval\_fn}
  1717 & evaluation function for operators and predicates, coded on the meta-level (SML); the identifier of such a function is a combination of the keyword {\tt eval\_} with the identifier of the function as defined in {\tt *.thy}
  1718 \\
  1719 & {\tt *\_simplify} 
  1720 & the canonical simplifier for the actual theory, i.e. the identifier for this ruleset is a combination of the theories identifier and the keyword {\tt *\_simplify}
  1721 \\
  1722 & {\tt norm\_rls :=}
  1723 & the canonical simplifier {\tt *\_simplify} is stored such that it is accessible for \isac
  1724 \\
  1725 & {\tt rew\_ord' :=}
  1726 & the same for rewrite orders, if needed outside of one particular ruleset
  1727 \\
  1728 & {\tt ruleset' :=}
  1729 & the same for rulesets (ordinary rulesets, reverse rulesets and {\tt eval\_rls})
  1730 \\
  1731 & {\tt calc\_list :=}
  1732 & the same for {\tt eval\_fn}s, if needed outside of one particular ruleset (e.g. for a tactic {\tt Calculate} in a script)
  1733 \\
  1734 & {\tt store\_pbl}
  1735 & problems defined within this {\tt *.ML}-file are made accessible for \isac
  1736 \\
  1737 & {\tt methods :=}
  1738 & methods defined within this {\tt *.ML}-file are made accessible for \isac
  1739 \\
  1740 \end{tabular}\end{center}\end{table}
  1741 }
  1742 The order of the data-items within the theories should adhere to the order given in this list.
  1743 
  1744 \section{Formal description of the problem-hierarchy}
  1745 %for Richard Lang
  1746 
  1747 \section{Script tactics}
  1748 The tactics actually promote the calculation: they construct the prooftree behind the scenes, and they are the points during evaluation where the script-interpreter transfers control to the user. Here we only describe the sytax of the tactics; the semantics is described on p.\pageref{user-tactics} below in context with the tactics the student uses ('user-tactics'): there is a 1-to-1 correspondence between user-tactics and script-tactics.
  1749 
  1750 
  1751 
  1752 
  1753 
  1754 \part{Authoring on the knowledge}
  1755 
  1756 
  1757 \section{Add a theorem}
  1758 \section{Define and add a problem}
  1759 \section{Define and add a predicate}
  1760 \section{Define and add a method}
  1761 \section{}
  1762 \section{}
  1763 \section{}
  1764 \section{}
  1765 
  1766 
  1767 
  1768 \newpage
  1769 \bibliography{bib/isac,bib/from-theses}
  1770 
  1771 \end{document}