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