%WN051006 dropped in code, but interesting for case study 'order a list'

%EqSystem.thy

%---------------------------------------------------------------------------

%

% order'_system      :: "bool list => bool list " ("order'_system _")

%

%EqSystem.ML

%---------------------------------------------------------------------------

%(*("order_system", ("EqSystem.order'_system", 

%                   eval_order_system "#eval_order_system_"))*)

%fun eval_order_system _ "EqSystem.order'_system"

%                         (p as (Const ("EqSystem.order'_system",_) $ ts)) _ =

%    let val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") [])

%                (isalist2list ts)

%       val ts'' = list2isalist HOLogic.boolT ts'

%    in if ts <> ts''

%       then Some (term2str p ^ " = " ^ term2str ts'',

%              Trueprop $ (mk_equality (p,ts'')))

%       else None

%    end

%  | eval_order_system _ _ _ _ = None;

%

%

%"Script Norm2SystemScript (es_::bool list) (vs_::real list) = \

%\  (let es__ = Try (Rewrite_Set simplify_Integral_parenthesized False) es_; \

%\       es__ = (Try (Calculate order_system_) (order_system es__))\

%\in (SubProblem (Biegelinie_,[linear,system],[no_met])\

%\                  [bool_list_ es__, real_list_ vs_]))"

%              ));

%

%eqsystem.sml

%---------------------------------------------------------------------------

%"----------- eval_sort -------------------------------------------";

%"----------- eval_sort -------------------------------------------";

%"----------- eval_sort -------------------------------------------";

%val ts = TermC.parse_test @{context} "[c_2 = 0, -1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";

%val ts' = sort (ord_simplify_Integral_ false (assoc_thy"Isac.thy") [])

%              (isalist2list ts);

%terms2str ts';

%val ts'' = list2isalist HOLogic.boolT ts';

%if term2str ts'' = "[-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0, c_2 = 0]"

%then () else raise error "eqsystem.sml eval_sort 1";

%

%val t = TermC.parse_test @{context} "order_system [c_2 = 0,\

%                \-1 * (q_0 * L ^^^ 2) / 2 + (L * c + c_2) = 0]";

%val Some (str,_) = eval_order_system "" "EqSystem.order'_system" t "";

%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 ()

%else raise error "eqsystem.sml eval_sort 2";

%

%

%

%  calculate_ thy ("EqSystem.order'_system", 

%                 eval_order_system "#eval_order_system_") t;

%

%---------------------------------------------------------------------------

%---------------------------------------------------------------------------

%---------------------------------------------------------------------------

%In the following this text is not compatible with isac-code:

%* move termorder to knowledge: FIXXXmat0201a

%

%

\documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}

\usepackage{latexsym}           % recommended by Ch.Schinagl 10.98

\bibliographystyle{alpha}

\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

\title{\isac --- Interface for\\

  Developers of Math Knowledge\\[1.0ex]

  and\\[1.0ex]

  Tools for Experiments in\\

  Symbolic Computation\\[1.0ex]}

\author{The \isac-Team\\

  \tt isac-users@ist.tugraz.at\\[1.0ex]}

\date{\today}

\begin{document}

\maketitle

\newpage

\tableofcontents

\newpage

\listoftables

\newpage

\chapter{Introduction}

\section{The scope of this document}

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

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

The document is selfcontained; basic knowledge about SML (as an introduction \cite{Paulson:91} is recommended), terms and rewriting is assumed.

%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.

Notation: SML code, directories, file names are {\tt written in 'tt'}; in particular {\tt ML>} is the KE prompt.

\paragraph{Give it a try !} Another aim of this text is to give the reader hints for experiments with the tools introduced.

\section{Related documents}\label{related-docs}

Isabelle reference manual \cite{Isa-ref}, also contained in the Isabelle distribution under $\sim${\tt /doc/}.

{\bf The actual locations of files is being recorded in \\{\tt /software/services/isac/README}

\footnote{The KEs current version is {\tt isac.020120-math/} which is based on the version Isabelle99 at {\tt http://isabelle.in.tum.de}.\\

The current locations at IST are\\

{\tt [isabelle]\hspace{3em}      /software/sol26/Isabelle99/}\\

{\tt [isac-src]\hspace{3em}      /software/services/isac/src/ke/}\\ 

{\tt [isac-bin]\hspace{3em}      /software/services/isac/bin/ke/}

} 

and rigorously updated.} In this document we refer to the following directories

\begin{tabbing}

xxx\=Isabelle sources1234 \=\kill

\>Isabelle sources \> {\tt [isabelle]/}\\

\>KE sources       \> {\tt [isac-src]/\dots{version}\dots/}\\

\>KE binary        \> {\tt [isac-bin]/\dots{version}\dots/}

\end{tabbing}

where {\tt\dots version\dots} stands for a directory-name containing information on the version.

\section{Getting started}

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):

\begin{verbatim}

   > [isac-bin]/sml @SMLload=isac.020120-math

   val it = false : bool

   ML>

\end{verbatim}

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~!

\part{Experimental approach}

\chapter{Basics, terms and parsing}

Isabelle implements terms of the {\it simply typed lambda calculus} \cite{typed-lambda} defined in $\sim${\tt/src/Pure.ML}. 

\section{The definition of terms}

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. 

{\footnotesize\begin{verbatim}

   datatype term = 

       Const of string * typ

     | Free  of string * typ 

     | Var   of indexname * typ

     | Bound of int

     | Abs   of string * typ * term

     | op $  of term * term;

   datatype typ = Type  of string * typ list

                | TFree of string * sort

                | TVar  of indexname * sort;

\end{verbatim}}%size % $

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).

\section{Theories and parsing}

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;

{\footnotesize\begin{verbatim}

   ML> thy;

   val it =

     {ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,

       Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat, Arith,

       Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype, Numeral, Bin,

       IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option, Map, Record,

       RelPow, Sexp, String, Calculation, SVC_Oracle, Main, Zorn, Filter, PNat,

       PRat, PReal, RealDef, RealOrd, RealInt, RealBin, HyperDef, Descript, ListG,

       Tools, Script, Typefix, Atools, RatArith, SqRoot, Differentiate, DiffAppl,

       InsSort, Isac} : theory                                                    ML>

   ML> HOL.thy;

   val it = {ProtoPure, CPure, HOL} : theory 

   ML>

   ML> parse;

   val it = fn : theory -> string -> cterm option

   ML> parse thy "a + b * #3";

   val it = Some "a + b * #3" : cterm option

   ML>

   ML> val t = (term_of o the) it;

   val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term

\end{verbatim}}%size

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

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.

\section{Displaying terms}

The print depth on the SML top-level can be set in order to produce output in the amount of detail desired:

{\footnotesize\begin{verbatim}

   ML> Compiler.Control.Print.printDepth;

   val it = ref 4 : int ref

   ML>

   ML> Compiler.Control.Print.printDepth:= 2;

   val it = () : unit

   ML> t;

   val it = # $ # $ (# $ #) : term

   ML>

   ML> Compiler.Control.Print.printDepth:= 6;

   val it = () : unit

   ML> t;

   val it =

     Const ("op +","[RealDef.real, RealDef.real] => RealDef.real") $

     Free ("a","RealDef.real") $

     (Const ("op *","[RealDef.real, RealDef.real] => RealDef.real") $

      Free ("b","RealDef.real") $ Free ("#3","RealDef.real")) : term

\end{verbatim}}%size % $

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:

{\footnotesize\begin{verbatim}

   ML> Compiler.Control.Print.printLength;

   val it = ref 8 : int ref

   ML> Compiler.Control.Print.stringDepth;

   val it = ref 250 : int ref

\end{verbatim}}%size

Anyway, the SML output of terms is not very readable; there are functions in the KE to display them:

{\footnotesize\begin{verbatim}

   ML> atomt;

   val it = fn : term -> unit

   ML> atomt t; 

   *** -------------

   *** Const ( op +)

   *** . Free ( a, )

   *** . Const ( op *)

   *** . . Free ( b, )

   *** . . Free ( #3, )

   val it = () : unit

   ML>

   ML> TermC.atom_trace_detail \@\{context\};

   val it = fn : theory -> term -> unit

   ML> TermC.atom_trace_detail \@\{context\} t;

   *** -------------

   *** Const ( op +, [real, real] => real)

   *** . Free ( a, real)

   *** . Const ( op *, [real, real] => real)

   *** . . Free ( b, real)

   *** . . Free ( #3, real)

   val it = () : unit

\end{verbatim}}%size

where again the {\tt typ}s are rendered as strings, but more elegantly by use of the information contained in {\tt thy}..

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

{\footnotesize\begin{verbatim}

   ML> (*-1-*) parse HOL.thy "#2^^^#3";

   *** Inner lexical error at: "^^^#3"

   val it = None : cterm option

   ML>

   ML> (*-2-*) parse HOL.thy "d_d x (a + x)";

   val it = None : cterm option

   ML>

   ML>

   ML> (*-3-*) parse RatArith.thy "#2^^^#3";

   val it = Some "#2 ^^^ #3" : cterm option

   ML>

   ML> (*-4-*) parse RatArith.thy "d_d x (a + x)";

   val it = Some "d_d x (a + x)" : cterm option

   ML>

   ML>

   ML> (*-5-*) parse Differentiate.thy "d_d x (a + x)";

   val it = Some "d_d x (a + x)" : cterm option

   ML>

   ML> (*-6-*) parse Differentiate.thy "#2^^^#3";

   val it = Some "#2 ^^^ #3" : cterm option

\end{verbatim}}%size

Don't trust the string representation: if we convert {\tt(*-4-*)} and {\tt(*-6-*)} to terms \dots

{\footnotesize\begin{verbatim}

   ML> (*-4-*) val thy = RatArith.thy;

   ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";

   *** -------------

   *** Free ( d_d, [real, real] => real)

   *** . Free ( x, real)

   *** . Const ( op +, [real, real] => real)

   *** . . Free ( a, real)

   *** . . Free ( x, real)

   val it = () : unit

   ML>

   ML> (*-6-*) val thy = Differentiate.thy;

   ML> ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";

   *** -------------

   *** Const ( Differentiate.d_d, [real, real] => real)

   *** . Free ( x, real)

   *** . Const ( op +, [real, real] => real)

   *** . . Free ( a, real)

   *** . . Free ( x, real)

   val it = () : unit

\end{verbatim}}%size

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

\section{Converting terms}

The conversion from {\tt cterm} to {\tt term} has been shown above:

{\footnotesize\begin{verbatim}

   ML> term_of;

   val it = fn : cterm -> term

   ML>

   ML> the;

   val it = fn : 'a option -> 'a

   ML>

   ML> val t = (term_of o the o (parse thy)) "a + b * #3";

   val t = Const (#,#) $ Free (#,#) $ (Const # $ Free # $ Free (#,#)) : term

\end{verbatim}}%size

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.

The other conversions are the following, some of which use the {\it signature} {\tt sign} of a theory:

{\footnotesize\begin{verbatim}

   ML> sign_of;

   val it = fn : theory -> Sign.sg

   ML>

   ML> cterm_of;

   val it = fn : Sign.sg -> term -> cterm

   ML> val ct = cterm_of (sign_of thy) t;

   val ct = "a + b * #3" : cterm

   ML>

   ML> Sign.string_of_term;

   val it = fn : Sign.sg -> term -> string

   ML> Sign.string_of_term (sign_of thy) t;

   val it = "a + b * #3" : ctem'

   ML>

   ML> string_of_cterm;

   val it = fn : cterm -> string

   ML> string_of_cterm ct;

   val it = "a + b * #3" : ctem'

\end{verbatim}}%size

\section{Theorems}

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:

{\footnotesize\begin{verbatim}

   ML> theorem' := overwritel (!theorem',

   [("diff_const",num_str diff_const)

   ]);

\end{verbatim}}%size

The additional recording of theorems and other values will disappear in later versions of \isac.

\chapter{Rewriting}

\section{The arguments for rewriting}

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.

{\footnotesize\begin{verbatim}

   ML> HOL.thy;

   val it = {ProtoPure, CPure, HOL} : theory

   ML> "HOL.thy" : theory';

   val it = "HOL.thy" : theory'

   ML>

   ML> sqrt_right;

   val it = fn : rew_ord (* term * term -> bool *)

   ML> "sqrt_right" : rew_ord;

   val it = "sqrt_right" : rew_ord

   ML>

   ML> eval_rls;

   val it =

     Rls

       {preconds=[],rew_ord=("sqrt_right",fn),

        rules=[Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,Thm #,

               Thm #,Thm #,Thm #,Thm #,Thm #,Calc #,Calc #,...],

        program=Script (Free #)} : rls

   ML> "eval_rls" : rls';

   val it = "eval_rls" : rls'

   ML>

   ML> diff_sum;

   val it = "d_d ?bdv (?u + ?v) = d_d ?bdv ?u + d_d ?bdv ?v" : thm

   ML> ("diff_sum", "") : thm';

   val it = ("diff_sum","") : thm'

\end{verbatim}}%size

where a {\tt thm'} is a pair, eventually with the string-representation of the respective theorem.

\section{The functions for rewriting}\label{rewrite}

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: 

{\footnotesize\begin{verbatim}

   ML> rewrite_;

   val it = fn

     : theory

       -> rew_ord

          -> rls -> bool -> thm -> term -> (term * term list) option

   ML>

   ML> rewrite;

   val it = fn

     : theory'

       -> rew_ord

          -> rls' -> bool -> thm' -> cterm' -> (cterm' * cterm' list) option

\end{verbatim}}%size

The arguments are the following:\\

\tabcolsep=4mm

\def\arraystretch{1.5}

\begin{tabular}{lp{11.0cm}}

  {\tt theory}  & the Isabelle theory containing the definitions necessary for parsing the {\tt term} \\

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

  {\tt rls}     & the rule set for evaluating the condition within {\tt thm} in case {\tt thm} is a conditional rule \\

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

  {\tt thm}     & the theorem used to try to rewrite {\tt term} \\

  {\tt term}    & the term eventually rewritten by {\tt thm} \\

\end{tabular}\\

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

\begin{tabular}{lp{10.4cm}}

  {\tt term}     & the term rewritten \\

  {\tt term list}& the assumptions eventually generated if the {\tt bool} flag is set to {\tt true} and {\tt thm} is applicable. \\

\end{tabular}\\

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

{\footnotesize\begin{verbatim}

   ML> val thy' = "Differentiate.thy";

   val thy' = "Differentiate.thy" : string

   ML> val ct = "d_d x (x ^^^ #2 + #3 * x + #4)";

   val ct = "d_d x (x ^^^ #2 + #3 * x + #4)" : cterm'

   ML>

   ML> val thm = ("diff_sum","");

   val thm = ("diff_sum","") : thm'

   ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true

                     [("bdv","x::real")] thm ct;

   val ct = "d_d x (x ^^^ #2 + #3 * x) + d_d x #4" : cterm'

   ML>

   ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true

                     [("bdv","x::real")] thm ct;

   val ct = "d_d x (x ^^^ #2) + d_d x (#3 * x) + d_d x #4" : cterm'

   ML>

   ML> val thm = ("diff_prod_const","");

   val thm = ("diff_prod_const","") : thm'

   ML> val Some (ct,_) = rewrite_inst thy' "tless_true" "eval_rls" true

                     [("bdv","x::real")] thm ct;

   val ct = "d_d x (x ^^^ #2) + #3 * d_d x x + d_d x #4" : cterm'

\end{verbatim}}%size

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.

\footnote{Hint: At the end you will need {\tt val (ct,\_) = the (rewrite\_set thy' "eval\_rls" false "SqRoot\_simplify" ct);}}

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

{\footnotesize\begin{verbatim}

   ML> val thy' = "Isac.thy";

   val thy' = "Isac.thy" : string

   ML> val ct' = "#3 * a + #2 * (a + #1)";

   val ct' = "#3 * a + #2 * (a + #1)" : cterm'

   ML>

   ML> val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n");

   val thm' = ("radd_mult_distrib2","?k * (?m + ?n) = ?k * ?m + ?k * ?n")

     : thm'

   ML> (*1*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';

   val ct' = "#3 * a + (#2 * a + #2 * #1)" : cterm'

   ML>

   ML> val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1");

   val thm' = ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1")

     : thm'

   ML> (*2*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';

   val ct' = "#3 * a + #2 * a + #2 * #1" : cterm'

   ML>

   ML> val thm' = ("rcollect_right",

     "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n");

   val thm' =

     ("rcollect_right",

      "[| ?l is_const; ?m is_const |] ==> ?l * ?n + ?m * ?n = (?l + ?m) * ?n")

     : thm'

   ML> (*3*) val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';

   val ct' = "(#3 + #2) * a + #2 * #1" : cterm'

   ML>

   ML> (*4*) val Some (ct',_) = calculate' thy' "plus" ct';

   val ct' = "#5 * a + #2 * #1" : cterm'

   ML>

   ML> (*5*) val Some (ct',_) = calculate' thy' "times" ct';

   val ct' = "#5 * a + #2" : cterm'

\end{verbatim}}%size

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

\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'):

{\footnotesize\begin{verbatim}

   sort_def   "sort ls = foldr ins ls []"

   ins_base   "ins [] a = [a]"

   ins_rec    "ins (x#xs) a = (if x < a then x#(ins xs a) else a#(x#xs))"  

   foldr_base "foldr f [] a = a"

   foldr_rec  "foldr f (x#xs) a = foldr f xs (f a x)"

   if_True    "(if True then ?x else ?y) = ?x"

   if_False   "(if False then ?x else ?y) = ?y"

\end{verbatim}}%size

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:

{\footnotesize\begin{verbatim}

   ML>  val thy' = "InsSort.thy";

   val thy' = "InsSort.thy" : theory'

   ML>  val ct = "sort [#1,#3,#2]" : cterm';

   val ct = "sort [#1,#3,#2]" : cterm'

   ML>

   ML>  val thm = ("sort_def","");

   ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

   val ct = "foldr ins [#1, #3, #2] []" : cterm'

   ML>

   ML>  val thm = ("foldr_rec","");

   ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

   val ct = "foldr ins [#3, #2] (ins [] #1)" : cterm'

   ML>

   ML>  val thm = ("ins_base","");

   ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

   val ct = "foldr ins [#3, #2] [#1]" : cterm'

   ML>

   ML>  val thm = ("foldr_rec","");

   ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

   val ct = "foldr ins [#2] (ins [#1] #3)" : cterm'

   ML>

   ML>  val thm = ("ins_rec","");

   ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

   val ct = "foldr ins [#2] (if #1 < #3 then #1 # ins [] #3 else [#3, #1])"

     : cterm'

   ML>

   ML>  val (ct,_) = the (calculate' thy' "le" ct);

   val ct = "foldr ins [#2] (if True then #1 # ins [] #3 else [#3, #1])" : cterm'

   ML>

   ML>  val thm = ("if_True","(if True then ?x else ?y) = ?x");

   ML>  val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct);

   val ct = "foldr ins [#2] (#1 # ins [] #3)" : cterm'

   ML> 

   ...

   val ct = "sort [#1,#3,#2]" : cterm'

\end{verbatim}}%size

\section{Variants of rewriting}

Some of the above examples already used variants of {\tt rewrite} all of which have the same value, and very similar arguments:

{\footnotesize\begin{verbatim}

   ML> rewrite_inst_;

   val it = fn

     : theory

       -> rew_ord

          -> rls

             -> bool

             -> (cterm' * cterm') list

                   -> thm -> term -> (term * term list) option

   ML> rewrite_inst;

   val it = fn

     : theory'

       -> rew_ord

          -> rls'

             -> bool

                -> (cterm' * cterm') list

                   -> thm' -> cterm' -> (cterm' * cterm' list) option

   ML>

   ML> rewrite_set_;

   val it = fn 

     : theory -> rls -> bool -> rls -> term -> (term * term list) option

   ML> rewrite_set;

   val it = fn

     : theory' -> rls' -> bool -> rls' -> cterm' -> (cterm' * cterm' list) option

   ML>

   ML> rewrite_set_inst_;

   val it = fn

     : theory

       -> rls

          -> bool

             -> (cterm' * cterm') list

                -> rls -> term -> (term * term list) option

   ML> rewrite_set_inst;

   val it = fn

     : theory'

       -> rls'

          -> bool

             -> (cterm' * cterm') list

                -> rls' -> cterm' -> (cterm' * cterm' list) option

\end{verbatim}}%size

\noindent The variant {\tt rewrite\_inst} substitutes {\tt (term * term) list} in {\tt thm} before rewriting,\\

the variant {\tt rewrite\_set} rewrites with a whole rule set {\tt rls} (instead with a {\tt thm} only),\\

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

{\footnotesize\begin{verbatim}

   ML> toggle;

   val it = fn : bool ref -> bool

   ML>

   ML> toggle trace_rewrite;

   val it = true : bool

   ML> toggle trace_rewrite;

   val it = false : bool

\end{verbatim}}%size

\section{Rule sets}

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').

A simple example of a rule set is {\tt rearrange\_assoc} which is defined in {\tt knowledge/RatArith.ML} as:

{\footnotesize\begin{verbatim}

   val rearrange_assoc = 

     Rls{preconds = [], rew_ord = ("tless_true",tless_true), 

         rules = 

         [Thm ("radd_assoc_RS_sym",num_str (radd_assoc RS sym)),

          Thm ("rmult_assoc_RS_sym",num_str (rmult_assoc RS sym))],

         program = Script ((term_of o the o (parse thy)) 

         "empty_script")

         }:rls;

\end{verbatim}}%size

where 

\begin{description}

\item [\tt preconds] are conditions which must be true in order to make the rule set applicable (the empty list evaluates to {\tt true})

\item [\tt rew\_ord] concerns term orders introduced below in \ref{term-order}

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

\item [\tt program] is the script applying the ruleset; it will disappear in later versions of \isac.

\end{description}

These variables evaluate to

{\footnotesize\begin{verbatim}

   ML> sym;

   val it = "?s = ?t ==> ?t = ?s" : thm 

   ML> rearrange_assoc;

   val it =

     Rls

       {preconds=[],rew_ord=("tless_true",fn),

        rules=[Thm ("radd_assoc_RS_sym","?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"),

               Thm ("rmult_assoc_RS_sym","?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1")],

        program=Script (Free ("empty_script","RealDef.real"))} : rls 

\end{verbatim}}%size

\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 

{\footnotesize\begin{verbatim}

   ML> val ct = (string_of_cterm o the o (parse RatArith.thy))

                "a + (b * (c * d) + e)";

   val ct = "a + ((b * (c * d) + e) + f)" : cterm'

   ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;

   val it = Some ("a + b * c * d + e + f",[]) : (string * string list) option

\end{verbatim}}%size

For acchieving this result the rule set has to be surprisingly busy:

{\footnotesize\begin{verbatim}

   ML> toggle trace_rewrite;

   val it = true : bool

   ML> rewrite_set "RatArith.thy" "eval_rls" false "rearrange_assoc" ct;

   ### trying thm 'radd_assoc_RS_sym'

   ### rewrite_set_: a + b * (c * d) + e

   ### trying thm 'radd_assoc_RS_sym'

   ### trying thm 'rmult_assoc_RS_sym'

   ### rewrite_set_: a + b * c * d + e

   ### trying thm 'rmult_assoc_RS_sym'

   ### trying thm 'radd_assoc_RS_sym'

   ### trying thm 'rmult_assoc_RS_sym'

   val it = Some ("a + b * c * d + e",[]) : (string * string list) option

\end{verbatim}}%size

\section{Calculate numeric constants}

As soon as numeric constants are in adjacent subterms (see the example on p.\pageref{cond-rew}), they can be calculated by the function

{\footnotesize\begin{verbatim}

   ML> calculate;

   val it = fn : theory' -> string -> cterm' -> (cterm' * thm') option

   ML> calculate_;

   val it = fn : theory -> string -> term -> (term * (string * thm)) option

\end{verbatim}}%size

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:

{\footnotesize\begin{verbatim}

   ML> calc_list;

   val it =

     ref

       [("plus",("op +",fn)),

        ("times",("op *",fn)),

        ("cancel_",("cancel",fn)),

        ("power",("pow",fn)),

        ("sqrt",("sqrt",fn)),

        ("Var",("Var",fn)),

        ("Length",("Length",fn)),

        ("Nth",("Nth",fn)),

        ("power",("pow",fn)),

        ("le",("op <",fn)),

        ("leq",("op <=",fn)),

        ("is_const",("is'_const",fn)),

        ("is_root_free",("is'_root'_free",fn)),

        ("contains_root",("contains'_root",fn)),

        ("ident",("ident",fn))]

     : (string * (string * (string -> term -> theory -> 

        (string * term) option))) list ref

\end{verbatim}}%size

These operations can be used in the following way.

{\footnotesize\begin{verbatim}

   ML> calculate' "Isac.thy" "plus" "#1 + #2";

   val it = Some ("#3",("#add_#1_#2","\"#1 + #2 = #3\"")) : (string * thm') option

   ML>

   ML> calculate' "Isac.thy" "times" "#2 * #3";

   val it = Some ("#6",("#mult_#2_#3","\"#2 * #3 = #6\""))

     : (string * thm') option

   ML>

   ML> calculate' "Isac.thy" "power" "#2 ^^^ #3";

   val it = Some ("#8",("#power_#2_#3","\"#2 ^^^ #3 = #8\""))

     : (string * thm') option

   ML>

   ML> calculate' "Isac.thy" "cancel_" "#9 // #12";

   val it = Some ("#3 // #4",("#cancel_#9_#12","\"#9 // #12 = #3 // #4\""))

     : (string * thm') option

   ML>

   ML> ...

\end{verbatim}}%size

\chapter{Term orders}\label{term-order}

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

\section{Examples for term orders}

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

e.g.

{\footnotesize\begin{verbatim}

   ML> sqrt_right;

   val it = fn : bool -> theory -> term * term -> bool

   ML> tless_true;

   val it = fn : 'a -> bool 

\end{verbatim}}%size

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:

{\footnotesize\begin{verbatim}

   ML> val t1 = (term_of o the o (parse thy)) "(sqrt a) + b";

   val t1 = Const # $ (# $ #) $ Free (#,#) : term

   ML>

   ML> val t2 = (term_of o the o (parse thy)) "b + (sqrt a)";

   val t2 = Const # $ Free # $ (Const # $ Free #) : term

   ML>

   ML> sqrt_right false SqRoot.thy (t1, t2);

   val it = false : bool

   ML> sqrt_right false SqRoot.thy (t2, t1);

   val it = true : bool

\end{verbatim}}%size

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:

{\footnotesize\begin{verbatim}

   ML> val t1 = (term_of o the o (parse thy)) "a + b*(sqrt c) + d";

   val t1 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term

   ML>

   ML> val t2 = (term_of o the o (parse thy)) "a + (sqrt b)*c + d";

   val t2 = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("d","RealDef.real") : term

   ML>

   ML> sqrt_right true SqRoot.thy (t1, t2);

   t= f@ts= "op +" @ "[a + b * sqrt c,d]"

   u= g@us= "op +" @ "[a + sqrt b * c,d]"

   size_of_term(t,u)= (8, 8)

   hd_ord(f,g)      = EQUAL

   terms_ord(ts,us) = LESS

   -------

   t= f@ts= "op +" @ "[a,b * sqrt c]"

   u= g@us= "op +" @ "[a,sqrt b * c]"

   size_of_term(t,u)= (6, 6)

   hd_ord(f,g)      = EQUAL

   terms_ord(ts,us) = LESS

   -------

   t= f@ts= "a" @ "[]"

   u= g@us= "a" @ "[]"

   size_of_term(t,u)= (1, 1)

   hd_ord(f,g)      = EQUAL

   terms_ord(ts,us) = EQUAL

   -------

   t= f@ts= "op *" @ "[b,sqrt c]"

   u= g@us= "op *" @ "[sqrt b,c]"

   size_of_term(t,u)= (4, 4)

   hd_ord(f,g)      = EQUAL

   terms_ord(ts,us) = LESS

   -------

   t= f@ts= "b" @ "[]"

   u= g@us= "sqrt" @ "[b]"

   size_of_term(t,u)= (1, 2)

   hd_ord(f,g)      = LESS

   terms_ord(ts,us) = LESS

   -------

   val it = true : bool 

\end{verbatim}}%size

\section{Ordered rewriting}

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}).

Such a rule set {\tt ac\_plus\_times}, called an AC-rewrite system, can be found in {\tt[isac-src]/knowledge/RathArith.ML}:

{\footnotesize\begin{verbatim}

   val ac_plus_times =

     Rls{preconds = [], rew_ord = ("term_order",term_order),

         rules =

         [Thm ("radd_commute",radd_commute),

          Thm ("radd_left_commute",radd_left_commute),

          Thm ("radd_assoc",radd_assoc),

          Thm ("rmult_commute",rmult_commute),

          Thm ("rmult_left_commute",rmult_left_commute),

          Thm ("rmult_assoc",rmult_assoc)],

         program = Script ((term_of o the o (parse thy))

         "empty_script")

         }:rls;

   val ac_plus_times =

     Rls

       {preconds=[],rew_ord=("term_order",fn),

        rules=[Thm ("radd_commute","?m + ?n = ?n + ?m"),

               Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"),

               Thm ("radd_assoc","?m + ?n + ?k = ?m + (?n + ?k)"),

               Thm ("rmult_commute","?m * ?n = ?n * ?m"),

               Thm ("rmult_left_commute","?x * (?y * ?z) = ?y * (?x * ?z)"),

               Thm ("rmult_assoc","?m * ?n * ?k = ?m * (?n * ?k)")],

        program=Script (Free ("empty_script","RealDef.real"))} : rls 

\end{verbatim}}%size

Note that the theorems {\tt radd\_left\_commute} and {\tt rmult\_left\_commute} are really necessary in order to make the rule set 'confluent'~!

\paragraph{Give it a try !} Ordered rewriting is one technique to produce polynomial normal from from arbitrary integer terms:

{\footnotesize\begin{verbatim}

   ML> val ct' = "#3 * a + b + #2 * a";

   val ct' = "#3 * a + b + #2 * a" : cterm'

   ML>

   ML> (*-1-*) radd_commute; val thm' = ("radd_commute","") : thm';

   val it = "?m + ?n = ?n + ?m" : thm

   val thm' = ("radd_commute","") : thm'

   ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';

   val ct' = "#2 * a + (#3 * a + b)" : cterm'

   ML>

   ML> (*-2-*) rdistr_right_assoc_p; val thm' = ("rdistr_right_assoc_p","") : thm';

   val it = "?l * ?n + (?m * ?n + ?k) = (?l + ?m) * ?n + ?k" : thm

   val thm' = ("rdistr_right_assoc_p","") : thm'

   ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';

   val ct' = "(#2 + #3) * a + b" : cterm'

   ML>

   ML> (*-3-*)

   ML> val Some (ct',_) = calculate thy' "plus" ct';

   val ct' = "#5 * a + b" : cterm'

\end{verbatim}}%size %FIXXXmat0201b ... calculate !

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

{\footnotesize\begin{verbatim}

   ML> val ct' = "#3 * a + b + #2 * a" : cterm';

   val ct' = "#3 * a + b + #2 * a" : cterm'

   ML> val thm' = ("radd_commute","") : thm';

   val thm' = ("radd_commute","") : thm'

   ML>

   ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';

   val ct' = "#2 * a + (#3 * a + b)" : cterm'

   ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';

   val ct' = "#3 * a + b + #2 * a" : cterm'

   ML> val Some (ct',_) = rewrite thy' "tless_true" "eval_rls" true thm' ct';

   val ct' = "#2 * a + (#3 * a + b)" : cterm'

              ..........

\end{verbatim}}%size

Ordered rewriting with the above AC-rewrite system {\tt ac\_plus\_times} performs a kind of bubble sort which can be traced:

{\footnotesize\begin{verbatim}

   ML> toggle trace_rewrite;

   val it = true : bool

   ML>

   ML> rewrite_set "RatArith.thy" "eval_rls" false "ac_plus_times" ct;

   ### trying thm 'radd_commute'

   ### not: "a + (b * (c * d) + e)" > "b * (c * d) + e + a"

   ### rewrite_set_: a + (e + b * (c * d))

   ### trying thm 'radd_commute'

   ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"

   ### not: "e + b * (c * d)" > "b * (c * d) + e"

   ### trying thm 'radd_left_commute'

   ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"

   ### trying thm 'radd_assoc'

   ### trying thm 'rmult_commute'

   ### not: "b * (c * d)" > "c * d * b"

   ### not: "c * d" > "d * c"

   ### trying thm 'rmult_left_commute'

   ### not: "b * (c * d)" > "c * (b * d)"

   ### trying thm 'rmult_assoc'

   ### trying thm 'radd_commute'

   ### not: "a + (e + b * (c * d))" > "e + b * (c * d) + a"

   ### not: "e + b * (c * d)" > "b * (c * d) + e"

   ### trying thm 'radd_left_commute'

   ### not: "a + (e + b * (c * d))" > "e + (a + b * (c * d))"

   ### trying thm 'radd_assoc'

   ### trying thm 'rmult_commute'

   ### not: "b * (c * d)" > "c * d * b"

   ### not: "c * d" > "d * c"

   ### trying thm 'rmult_left_commute'

   ### not: "b * (c * d)" > "c * (b * d)"

   ### trying thm 'rmult_assoc'

   val it = Some ("a + (e + b * (c * d))",[]) : (string * string list) option     \end{verbatim}}%size

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.

\chapter{The hierarchy of problem types}\label{pbt}

\section{The standard-function for 'matching'}

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:

{\footnotesize\begin{verbatim}

   ML> matches;

   val it = fn : theory -> term -> term -> bool

\end{verbatim}}%size

where the first of the two {\tt term} arguments is the particular term to be tested, and the second one is the pattern:

{\footnotesize\begin{verbatim}

   ML> val t = (term_of o the o (parse thy)) "#3 * x^^^#2 = #1";

   val t = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("#1","RealDef.real") : term

   ML>

   ML> val p = (term_of o the o (parse thy)) "a * b^^^#2 = c";

   val p = Const (#,#) $ (# $ # $ (# $ #)) $ Free ("c","RealDef.real") : term

   ML> atomt p;

   *** -------------

   *** Const ( op =)

   *** . Const ( op *)

   *** . . Free ( a, )

   *** . . Const ( RatArith.pow)

   *** . . . Free ( b, )

   *** . . . Free ( #2, )

   *** . Free ( c, )

   val it = () : unit

   ML>

   ML> mk_Var;

   val it = fn : term -> term

   ML>

   ML> val pat = mk_Var p;

   val pat = Const (#,#) $ (# $ # $ (# $ #)) $ Var ((#,#),"RealDef.real") : term

   ML> Sign.string_of_term (sign_of thy) pat;

   val it = "?a * ?b ^^^ #2 = ?c" : cterm' 

   ML> atomt pat;

   *** -------------

   *** Const ( op =)

   *** . Const ( op *)

   *** . . Var ((a, 0), )

   *** . . Const ( RatArith.pow)

   *** . . . Var ((b, 0), )

   *** . . . Free ( #2, )

   *** . Var ((c, 0), )

   val it = () : unit

\end{verbatim}}%size % $ 

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:

{\footnotesize\begin{verbatim}

   ML> matches thy t pat;

   val it = true : bool

   ML>

   ML> val t2 = (term_of o the o (parse thy)) "x^^^#2 = #1";

   val t2 = Const (#,#) $ (# $ # $ Free #) $ Free ("#1","RealDef.real") : term

   ML> matches thy t2 pat;

   val it = false : bool    

   ML>

   ML> val pat2 = (term_of o the o (parse thy)) "?u^^^#2 = ?v";

   val pat2 = Const (#,#) $ (# $ # $ Free #) $ Var ((#,#),"RealDef.real") : term

   ML> matches thy t2 pat2;

   val it = true : bool 

\end{verbatim}}%size % $

\section{Accessing the hierarchy}

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):

{\footnotesize\begin{verbatim}

   ML> show_ptyps;

   val it = fn : unit -> unit

   ML> show_ptyps();

   [

    ["e_pblID"],

    ["equation", "univariate", "linear"],

    ["equation", "univariate", "plain_square"],

    ["equation", "univariate", "polynomial", "degree_two", "pq_formula"],

    ["equation", "univariate", "polynomial", "degree_two", "abc_formula"],

    ["equation", "univariate", "squareroot"],

    ["equation", "univariate", "normalize"],

    ["equation", "univariate", "sqroot-test"],

    ["function", "derivative_of"],

    ["function", "maximum_of", "on_interval"],

    ["function", "make"],

    ["tool", "find_values"],

    ["functional", "inssort"]

   ]

   val it = () : unit

\end{verbatim}}%size

The retrieve function for individual problem types is {\tt get\_pbt}

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

{\footnotesize\begin{verbatim}

   ML> get_pbt;

   val it = fn : pblID -> pbt

   ML> get_pbt ["squareroot", "univariate", "equation"];

   val it =

     {met=[("SqRoot.thy","square_equation")],

      model=[("#Given",(Const (#,#),Free (#,#))),

           ("#Given",(Const (#,#),Free (#,#))),

           ("#Given",(Const (#,#),Free (#,#))),

           ("#Find",(Const (#,#),Free (#,#)))],

      thy={ProtoPure, CPure, HOL, Ord, Set, subset, equalities, mono, Vimage, Fun,

            Prod, Lfp, Relation, Trancl, WF, NatDef, Gfp, Sum, Inductive, Nat,

            Arith, Divides, Power, Finite, Equiv, IntDef, Int, Univ, Datatype,

            Numeral, Bin, IntArith, WF_Rel, Recdef, IntDiv, NatBin, List, Option,

            Map, Record, RelPow, Sexp, String, Calculation, SVC_Oracle, Main,

            Zorn, Filter, PNat, PRat, PReal, RealDef, RealOrd, RealInt, RealBin,

            HyperDef, Descript, ListG, Tools, Script, Typefix, Atools, RatArith,

            SqRoot},

      where_=[Const ("SqRoot.contains'_root","bool => bool") $

              Free ("e_","bool")]} : pbt

\end{verbatim}}%size %$

where the records fields hold the following data:

\begin{description}

\item [\tt thy]: the theory necessary for parsing the formulas

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

\item [\tt met]: the list of methods solving this problem type.\\

\end{description}

The following function adds or replaces a problem type (after having it prepared using {\tt prep\_pbt})

{\footnotesize\begin{verbatim}

   ML> store_pbt;

   val it = fn : pbt * pblID -> unit

   ML> store_pbt

    (prep_pbt SqRoot.thy

    (["newtype","univariate","equation"],

     [("#Given" ,["equality e_","solveFor v_","errorBound err_"]),

      ("#Where" ,["contains_root (e_::bool)"]),

      ("#Find"  ,["solutions v_i_"])

     ],

     [("SqRoot.thy","square_equation")]));

   val it = () : unit

\end{verbatim}}%size

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}).

\section{Internals of the datastructure}

This subsection only serves for the implementation of the hierarchy browser and can be skipped by the authors of math knowledge.

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:

{\footnotesize\begin{verbatim}

   type pbt = 

        {thy   : theory,       (* the nearest to the root,

                                  which allows to compile that pbt  *)

         where_: term list,    (* where - predicates                *)

         model   : ((string *    (* fields "#Given","#Find"           *)

                   (term *     (* description                       *)

                    term))     (* id                                *)

                      list),                                        

         met   : metID list};  (* methods solving the pbt           *)

   datatype ptyp = 

            Ptyp of string *   (* key within pblID                  *)

                    pbt list * (* several pbts with different domIDs*)

                    ptyp list;

   val e_Ptyp = Ptyp ("empty",[],[]);

   type ptyps = ptyp list;

   val ptyps = ref ([e_Ptyp]:ptyps);