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

    val it = fn : term -> term

    ML>

    ML> val pat = free2var 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 free2var}. 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")],

       ppc=[("#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 ppc]: 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                *)

          ppc   : ((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);

 \end{verbatim}}%size

 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.

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

 \section{Match a formalization with a problem type}\label{pbl}

 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.

 {\footnotesize\begin{verbatim}

    ML> val fmz = ["equality (#1 + #2 * x = #0)",

                   "solveFor x",

                   "solutions L"] : fmz;

    val fmz = ["equality (#1 + #2 * x = #0)","solveFor x","solutions L"] : fmz

 \end{verbatim}}%size

 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:

 {\footnotesize\begin{verbatim}

    ML> match_pbl;

    val it = fn : fmz -> pbt -> match'

    ML>

    ML> match_pbl fmz (get_pbt ["univariate","equation"]);

    val it =

      Matches'

        {Find=[Correct "solutions L"],

         Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],

         Relate=[],Where=[Correct "matches (?a = ?b) (#1 + #2 * x = #0)"],With=[]}

      : match'

    ML>

    ML> match_pbl fmz (get_pbt ["linear","univariate","equation"]);

    val it =

      Matches'

        {Find=[Correct "solutions L"],

         Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x"],

         Relate=[],

         Where=[Correct

                  "matches (          x = #0) (#1 + #2 * x = #0) |

                   matches (     ?b * x = #0) (#1 + #2 * x = #0) |

                   matches (?a      + x = #0) (#1 + #2 * x = #0) |

                   matches (?a + ?b * x = #0) (#1 + #2 * x = #0)"],

         With=[]} : match'

    ML>

    ML> match_pbl fmz (get_pbt ["squareroot","univariate","equation"]);

    val it =

      NoMatch'

        {Find=[Correct "solutions L"],

         Given=[Correct "equality (#1 + #2 * x = #0)",Correct "solveFor x",

                Missing "errorBound err_"],Relate=[],

         Where=[False "contains_root #1 + #2 * x = #0 "],With=[]} : match'

 \end{verbatim}}%size

 The above formalization does not match the problem type \\{\tt["squareroot","univariate","equation"]} which is explained by the tags:

 \begin{tabbing}

 123\=\kill

 \> {\tt Missing:} the item is missing in the formalization as required by the problem type\\

 \> {\tt Superfl:} the item is not required by the problem type\\

 \> {\tt Correct:} the item is correct, or the precondition ({\tt Where}) is true\\

 \> {\tt False:} the precondition ({\tt Where}) is false\\

 \> {\tt Incompl:} the item is incomlete, or not yet input.\\

 \end{tabbing}

 \section{Refine a problem specification}

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

 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

 {\small

 \begin{enumerate}

 \item for all $F$ matching some $P_i$ must follow, that $F$ matches $P$

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

 \item for all $F$ matching some $P$ must follow, that $F$ matches $P_n$\\

 \end{enumerate}}%small

 \noindent Let us give an example for the point (1.) and (2.) first:

 {\footnotesize\begin{verbatim}

    ML> refine;

    val it = fn : fmz -> pblID -> match list

    ML>

    ML> val fmz = ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",

               "solveFor x","errorBound (eps=#0)",

               "solutions L"];

    ML>

    ML> refine fmz ["univariate","equation"];

    *** pass ["equation","univariate"]

    *** pass ["equation","univariate","linear"]

    *** pass ["equation","univariate","plain_square"]

    *** pass ["equation","univariate","polynomial"]

    *** pass ["equation","univariate","squareroot"]

    val it =

      [Matches

         (["univariate","equation"],

          {Find=[Correct "solutions L"],

           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                  Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],

           Where=[Correct

                    "matches (?a = ?b) (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"],

           With=[]}),

       NoMatch

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

          {Find=[Correct "solutions L"],

           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                  Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],

           Where=[False "(?a + ?b * x = #0) (sqrt (#9 + #4 * x#"],

           With=[]}),

       NoMatch

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

          {Find=[Correct "solutions L"],

           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                  Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],

           Where=[False

                    "matches (?a + ?b * x ^^^ #2 = #0)"],

           With=[]}),

       NoMatch

         (["polynomial","univariate","equation"],

          {Find=[Correct "solutions L"],

           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                  Correct "solveFor x",Superfl "errorBound (eps = #0)"],Relate=[],

           Where=[False 

                  "is_polynomial_in sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) x"],

           With=[]}),

       Matches

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

          {Find=[Correct "solutions L"],

           Given=[Correct "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))",

                  Correct "solveFor x",Correct "errorBound (eps = #0)"],Relate=[],

           Where=[Correct

                    "contains_root sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) "],

           With=[]})] : match list

 \end{verbatim}}%size}%footnotesize\label{refine}

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

 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:

 {\footnotesize\begin{verbatim}

    ML>  val fmz = ["equality (x+#1=#2)",

                "solveFor x","errorBound (eps=#0)",

                "solutions L"];

    [...]

    ML>

    ML>  refine fmz ["univariate","equation"];

    *** pass ["equation","univariate"]

    *** pass ["equation","univariate","linear"]

    *** pass ["equation","univariate","plain_square"]

    *** pass ["equation","univariate","polynomial"]

    *** pass ["equation","univariate","squareroot"]

    *** pass ["equation","univariate","normalize"]

    val it =

      [Matches

         (["univariate","equation"],

          {Find=[Correct "solutions L"],

           Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",

                  Superfl "errorBound (eps = #0)"],Relate=[],

           Where=[Correct "matches (?a = ?b) (x + #1 = #2)"],With=[]}),

       NoMatch

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

    [...]

           With=[]}),

       NoMatch

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

          {Find=[Correct "solutions L"],

           Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",

                  Correct "errorBound (eps = #0)"],Relate=[],

           Where=[False "contains_root x + #1 = #2 "],With=[]}),

       Matches

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

          {Find=[Correct "solutions L"],

           Given=[Correct "equality (x + #1 = #2)",Correct "solveFor x",

                  Superfl "errorBound (eps = #0)"],Relate=[],Where=[],With=[]})]

      : match list

 \end{verbatim}}%size

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

 This recursive search on the problem hierarchy can be  done within a proof state. This leads to the next section.

 \chapter{Methods}\label{met}

 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.

 \section{The scripts' syntax}

 The syntax of scripts follows the definition given in Backus-normal-form:

 {\it

 \begin{tabbing}

 123\=123\=expr ::=\=$|\;\;$\=\kill

 \>script ::= {\tt Script} id arg$\,^*$ = body\\

 \>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\

 \>\>body ::= expr\\

 \>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\

 \>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\

 \>\>\>$|\;$\>listexpr\\

 \>\>\>$|\;$\>id\\

 \>\>\>$|\;$\>seqex id\\

 \>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\

 \>\>\>$|\;$\>{\tt Repeat} seqex\\

 \>\>\>$|\;$\>{\tt Try} seqex\\

 \>\>\>$|\;$\>seqex {\tt Or} seqex\\

 \>\>\>$|\;$\>seqex {\tt @@} seqex\\

 \>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\

 \>\>type ::= id\\

 \>\>tac ::= id

 \end{tabbing}}

 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.

 Expressions containing some of the keywords {\tt let}, {\tt if} etc. are called {\bf script-expressions}.

 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,

 \section{Control the flow of evaluation}

 The flow of control is managed by the following script-expressions called {\it tacticals}.

 \begin{description}

 \item{{\tt while} prop {\tt Do} expr id} 

 \item{{\tt if} prop {\tt then} expr {\tt else} expr}

 \end{description}

 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)

 \begin{description}

 \item{{\tt Repeat} expr id}

 \item{{\tt Try} expr id}

 \item{expr {\tt Or} expr id}

 \item{expr {\tt @@} expr id}

 \end{description}

 \begin{description}

 \item xxx

 \end{description}