doc-isac/mat-eng-de.tex
author wneuper <Walther.Neuper@jku.at>
Sun, 31 Dec 2023 09:42:27 +0100
changeset 60787 26037efefd61
parent 60650 06ec8abfd3bc
permissions -rw-r--r--
Doc/Specify_Phase 2: copy finished
ahirn@37877
     1
\documentclass[11pt,a4paper,headline,headcount,towside,nocenter]{report}
ahirn@37877
     2
\usepackage{latexsym} 
alexandra@37882
     3
ahirn@37877
     4
%\usepackage{ngerman}
ahirn@37877
     5
%\grmn@dq@error ...and \dq \string #1 is undefined}
ahirn@37877
     6
%l.989 ...tch the problem type \\{\tt["squareroot",
ahirn@37877
     7
%                                                  "univ
ahirn@37877
     8
\bibliographystyle{alpha}
ahirn@37877
     9
ahirn@37877
    10
\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
neuper@37896
    11
\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
ahirn@37877
    12
neuper@37896
    13
\title{\isac \\
neuper@37896
    14
  Experimente zur Computermathematik\\[1.0ex]
neuper@37896
    15
  und\\[1.0ex]
neuper@37896
    16
  Handbuch f\"ur Autoren der\\
neuper@37896
    17
  Mathematik-Wissensbasis\\[1.0ex]}
alexandra@37889
    18
\author{Alexandra Hirn und Eva Rott\\
ahirn@37877
    19
  \tt isac-users@ist.tugraz.at\\[1.0ex]}
ahirn@37877
    20
\date{\today}
ahirn@37877
    21
ahirn@37877
    22
\begin{document}
ahirn@37877
    23
\maketitle
ahirn@37877
    24
\newpage
ahirn@37877
    25
\tableofcontents
ahirn@37877
    26
\newpage
ahirn@37877
    27
\listoftables
ahirn@37877
    28
\newpage
ahirn@37877
    29
alexandra@37887
    30
\chapter{Einleitung}
neuper@37896
    31
Dies ist die \"Ubersetzung der dersten Kapitel einer englischen Version \footnote{http://www.ist.tugraz.at/projects/isac/publ/mat-eng.pdf}, auf den Stand von \sisac{} 2008 gebracht. Die \"Ubersetzung und Anpassung erfolgte durch die Autorinnen im Rahmen einer Ferialpraxis am Institut f\"ur Softwaretechnologie der TU Graz.
neuper@37896
    32
neuper@37896
    33
Diese Version zeichnet sich dadurch aus, dass sie von ``Nicht-Computer-Freaks''  f\"ur ``Nicht-Computer-Freaks'' geschrieben wurde.
neuper@37896
    34
ahirn@37877
    35
\section{``Authoring'' und ``Tutoring''}
alexandra@37891
    36
\paragraph{TO DO} Mathematik lernen -- verschiedene Autoren -- Isabelle
ahirn@37877
    37
Die Grundlage f\"ur \isac{} bildet Isabelle. Dies ist ein ``theorem prover'', der von L. Paulson und T. Nipkow entwickelt wird und Hard- und Software pr\"uft.
ahirn@37877
    38
\section{Der Inhalt des Dokuments}
ahirn@37877
    39
\paragraph{TO DO} {Als Anleitung:} Dieses Dokument beschreibt das Kerngebiet (KE) von \isac{}, das Gebiet der mathematics engine (ME) im Kerngebiet und die verschiedenen Funktionen wie das Umschreiben und der Vergleich.
ahirn@37877
    40
alexandra@37891
    41
\isac{} und KE wurden in SML geschrieben, die Sprache in Verbindung mit dem Vorg\"anger des theorem Provers Isabelle entwickelt. So kam es, dass in diesem Dokument die Ebene ASCII als SML Code pr\"asentiert wird. Der Leser wird vermutlich erkennen, dass der \isac{} Benutzer eine vollkommen andere Sichtweise auf eine grafische Benutzeroberfl\"ache bekommt.
ahirn@37877
    42
alexandra@37891
    43
Das Dokument ist eigenst\"andig; Basiswissen \"uber SML (f\"ur eine Einf\"uhrung siehe \cite{Paulson:91}), Terme und Umschreibung wird vorrausgesetzt.
ahirn@37877
    44
ahirn@37877
    45
%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.
ahirn@37877
    46
ahirn@37877
    47
Hinweis: SML Code, Verzeichnis, Dateien sind {\tt in 'tt' geschrieben}; besonders in {\tt ML>} ist das Kerngebiet schnell.
ahirn@37877
    48
ahirn@37877
    49
\paragraph{Versuchen Sie es!}  Ein weiteres Anliegen dieses Textes ist, dem Leser Tipps f\"ur Versuche mit den Anwendungen zu geben.
ahirn@37877
    50
ahirn@37877
    51
\section{Gleich am Computer ausprobieren!}\label{get-started}
alexandra@37891
    52
\paragraph{TO DO screenshot} Bevor Sie mit Ihren Versuchen beginnen, m\"ochten wir Ihnen noch einige Hinweise geben:
ahirn@37877
    53
\begin{itemize}
ahirn@37877
    54
 \item System starten
ahirn@37877
    55
 \item Shell aufmachen und die Datei mat-eng-de.sml \"offnen.
ahirn@37877
    56
 \item $>$  :  Hinter diesem Zeichen (``Prompt'') stehen jene, die Sie selbst eingeben bzw. mit Copy und Paste aus der Datei kopieren.
ahirn@37877
    57
 \item Die Eingabe wird mit ``;'' und ``Enter'' abgeschlossen.
ahirn@37877
    58
 \item Zeilen, die nicht mit Prompt beginnen, werden vom Computer ausgegeben.
ahirn@37877
    59
 
ahirn@37877
    60
\end{itemize}
ahirn@37877
    61
ahirn@37877
    62
\part{Experimentelle Ann\"aherung}
ahirn@37877
    63
ahirn@37877
    64
\chapter{Terme und Theorien}
alexandra@37891
    65
Wie bereits erw\"ahnt, geht es um Computer-Mathematik. In den letzten Jahren hat die ``computer science'' grosse Fortschritte darin gemacht, Mathematik auf dem Computer verst\"andlich darzustellen. Dies gilt f\"ur mathematische Formeln, f\"ur die Beschreibung von Problemen, f\"ur L\"osungsmethoden etc. Wir beginnen mit mathematischen Formeln.
ahirn@37877
    66
ahirn@37877
    67
\section{Von der Formel zum Term}
ahirn@37877
    68
Um ein Beispiel zu nennen: Die Formel $a+b\cdot 3$ l\"asst sich in lesbarer Form so eingeben:
ahirn@37877
    69
{\footnotesize\begin{verbatim}
alexandra@37891
    70
   > "a + b * 3";
alexandra@37891
    71
      val it = "a + b * 3" : string
ahirn@37877
    72
\end{verbatim}}
Walther@60566
    73
\noindent ``a + b * 3'' ist also ein string (eine Zeichenfolge). In dieser Form weiss der Computer nicht, dass z.B. eine Multiplikation {\em vor} einer Addition zu rechnen ist. Isabelle braucht dazu eine andere Darstellung f\"ur Formeln. In diese kann man mit der Funktion {\tt TermC.parse_test @{context}} (string to term) umrechnen:
ahirn@37877
    74
{\footnotesize\begin{verbatim}
Walther@60566
    75
   > TermC.parse_test @{context} "a + b * 3";
alexandra@37891
    76
      val it =
alexandra@37891
    77
         Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37891
    78
               Free ("a", "RealDef.real") $
alexandra@37891
    79
            (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
alexandra@37891
    80
               ...) : Term.term
ahirn@37877
    81
\end{verbatim}}
alexandra@37892
    82
\noindent Diese Form heisst {\tt term} und ist nicht f\"ur den Menschen zum lesen gedacht. Isabelle braucht sie aber intern zum Rechnen. Wir wollen sie mit Hilfe von {\tt val} (value) auf der Variable {\tt t} speichern:
ahirn@37877
    83
{\footnotesize\begin{verbatim}
Walther@60566
    84
   > val t = TermC.parse_test @{context} "a + b * 3";
alexandra@37891
    85
      val t =  
alexandra@37891
    86
         Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37891
    87
               Free ("a", "RealDef.real") $
alexandra@37891
    88
            (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
alexandra@37891
    89
               ...) : Term.term
neuper@37896
    90
\end{verbatim}}
neuper@37896
    91
Von dieser Variablen {\tt t} kann man den Wert jederzeit abrufen:
neuper@37896
    92
{\footnotesize\begin{verbatim}
alexandra@37891
    93
   > t;
alexandra@37891
    94
      val it =
alexandra@37891
    95
         Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37891
    96
               Free ("a", "RealDef.real") $
alexandra@37891
    97
            (Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
alexandra@37891
    98
               ...) : Term.term
neuper@37896
    99
\end{verbatim}}
Walther@60650
   100
Der auf {\tt t} gespeicherte Term kann einer Funktion {\tt TermC.atom_trace_detail @{context}} \"ubergeben werden, die diesen in einer dritten Form zeigt:
ahirn@37877
   101
{\footnotesize\begin{verbatim}
Walther@60650
   102
   > TermC.atom_trace_detail \@\{context\} term;
ahirn@37877
   103
 
alexandra@37891
   104
   ***
alexandra@37891
   105
   *** Const (op +, [real, real] => real)
alexandra@37891
   106
   *** . Free (a, real)
alexandra@37891
   107
   *** . Const (op *, [real, real] => real)
alexandra@37891
   108
   *** . . Free (b, real)
alexandra@37891
   109
   *** . . Free (3, real)
alexandra@37891
   110
   ***
ahirn@37877
   111
 
alexandra@37891
   112
   val it = () : unit
neuper@37896
   113
\end{verbatim}}
alexandra@37891
   114
Diese Darstellung nennt man ``abstract syntax'' und macht unmittelbar klar, dass man a und b nicht addieren kann, weil ein Mal vorhanden ist.
alexandra@37892
   115
\newline Es gibt noch eine vierte Art von Term, den cterm. Er wird weiter unten verwendet, weil er sich als string lesbar darstellt.
ahirn@37877
   116
ahirn@37877
   117
\section{``Theory'' und ``Parsing``}
alexandra@37892
   118
Der Unterschied zwischen \isac{} und bisheriger Mathematiksoftware (GeoGebra, Mathematica, Maple, Derive etc.) ist, dass das mathematische Wissen nicht im Programmcode steht, sondern in sogenannten theories (Theorien).
alexandra@37892
   119
Dort wird das Mathematikwissen in einer f\"ur nicht Programmierer lesbaren Form geschrieben. Das Wissen von \isac{} ist in folgenden Theorien entahlten:
ahirn@37877
   120
{\footnotesize\begin{verbatim}
alexandra@37891
   121
   > Isac.thy;
alexandra@37891
   122
      val it =
alexandra@37891
   123
         {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
alexandra@37891
   124
         Sum_Type, Relation, Record, Inductive, Transitive_Closure,
alexandra@37891
   125
         Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
alexandra@37891
   126
         SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
alexandra@37891
   127
         Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
alexandra@37891
   128
         IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
alexandra@37891
   129
         Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
alexandra@37891
   130
         RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
alexandra@37891
   131
         Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
alexandra@37891
   132
         Float, ComplexI, Descript, Atools, Simplify, Poly, Rational, PolyMinus,
alexandra@37891
   133
         Equation, LinEq, Root, RootEq, RatEq, RootRat, RootRatEq, PolyEq, Vect,
alexandra@37891
   134
         Calculus, Trig, LogExp, Diff, DiffApp, Integrate, EqSystem, Biegelinie,
alexandra@37891
   135
         AlgEin, Test, Isac} : Theory.theory
neuper@37896
   136
\end{verbatim}}
alexandra@37892
   137
{\tt ProtoPure} und {\tt CPure} enthalten diese logischen Grundlagen, die in {\tt HOL} und den nachfolgenden Theorien erweitert werden. \isac{} als letzte Theorie beinhaltet das gesamte Wissen.
alexandra@37891
   138
Dass das Mal vor dem Plus berechnet wird, ist so festgelegt:
neuper@37896
   139
{\footnotesize\begin{verbatim}
alexandra@37892
   140
   class plus =
alexandra@37892
   141
   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
alexandra@37892
   142
alexandra@37892
   143
   class minus =
alexandra@37892
   144
   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
alexandra@37892
   145
alexandra@37892
   146
   class uminus =
alexandra@37892
   147
   fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
alexandra@37892
   148
alexandra@37892
   149
   class times =
alexandra@37892
   150
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) 
neuper@37896
   151
\end{verbatim}}
alexandra@37892
   152
{\tt infix} gibt an, dass der Operator zwischen den Zahlen steht und nicht, wie in ''abstract syntax``, vorne oben.
alexandra@37892
   153
Die Zahlen rechts davon legen die Priorit\"at fest. 70 f\"ur Mal ist gr\"osser als 65 f\"ur Plus und wird daher zuerst berechnet.
ahirn@37877
   154
alexandra@37892
   155
Wollen Sie wissen, wie die einzelnen Rechengesetze aussehen, k\"onnen Sie im Internet folgenden Link ansehen: http://isabelle.in.tum.de/dist/library/HOL/Groups.html
alexandra@37892
   156
Walther@60566
   157
\paragraph{} Der Vorgang, bei dem aus einem {\tt string} ein Term entsteht, nennt man Parsing. Dazu wird Wissen aus der Theorie ben\"otigt, denn {\tt TermC.parse_test @{context}} nimmt intern eine parse-Funktion, bei der immer das gesamte \isac{}-Wissen verwendet wird. Bei dieser Funktion wird weiters festgelegt, aus welcher Theorie das Wissen genommen werden soll.
neuper@37896
   158
{\footnotesize\begin{verbatim}
alexandra@37892
   159
   > parse Isac.thy "a + b";
alexandra@37892
   160
      val it = Some "a + b" : Thm.cterm Library.option
neuper@37896
   161
\end{verbatim}}
alexandra@37892
   162
Um sich das Weiterrechnen zu erleichtern, kann das Ergebnis vom Parsing auf eine Variable, wie zum Beispiel {\tt t} gespeichert werden:
neuper@37896
   163
{\footnotesize\begin{verbatim}
alexandra@37892
   164
   > val t = parse Isac.thy "a + b";
alexandra@37892
   165
      val t = Some "a + b" : Thm.cterm Library.option
neuper@37896
   166
\end{verbatim}}
alexandra@37892
   167
{\tt Some} bedeutet, dass das n\"otige Wissen vorhanden ist, um die Rechnung durchzuf\"uhren. {\tt None} zeigt uns, dass das Wissen fehlt oder ein Fehler aufgetreten ist. Daher sieht man im folgenden Beispiel, dass {\tt HOL.thy} nicht ausreichend Wissen enth\"alt:
neuper@37896
   168
{\footnotesize\begin{verbatim}
alexandra@37892
   169
   > parse HOL.thy "a + b";
alexandra@37892
   170
      val it = None : Thm.cterm Library.option
neuper@37896
   171
\end{verbatim}}
alexandra@37892
   172
Anschliessend zeigen wir Ihnen noch ein zweites Beispiel, bei dem sowohl ein Fehler aufgetreten ist, als auch das Wissen fehlt:
neuper@37896
   173
{\footnotesize\begin{verbatim}
alexandra@37892
   174
   > parse Isac.thy "a + ";
alexandra@37892
   175
      *** Inner syntax error: unexpected end of input
alexandra@37892
   176
      *** Expected tokens: "contains_root" "is_root_free" "q_" "M_b" "M_b'"
alexandra@37892
   177
      *** "Integral" "differentiate" "E_" "some_of" "||" "|||" "argument_in"
alexandra@37892
   178
      *** "filter_sameFunId" "I__" "letpar" "Rewrite_Inst" "Rewrite_Set"
alexandra@37892
   179
      *** "Rewrite_Set_Inst" "Check_elementwise" "Or_to_List" "While" "Script"
alexandra@37892
   180
      *** "\\" "\\" "\\" "CHR" "xstr" "SOME" "\\" "@"
alexandra@37892
   181
      *** "GREATEST" "[" "[]" "num" "\\" "{)" "{.." "\\" "(|"
alexandra@37892
   182
      *** "\\" "SIGMA" "()" "\\" "PI" "\\" "\\" "{" "INT"
alexandra@37892
   183
      *** "UN" "{}" "LEAST" "\\" "0" "1" "-" "!" "?" "?!" "\\"
alexandra@37892
   184
      *** "\\" "\\" "\\!" "THE" "let" "case" "~" "if" "ALL"
alexandra@37892
   185
      *** "EX" "EX!" "!!" "_" "\\" "\\" "PROP" "[|" "OFCLASS"
alexandra@37892
   186
      *** "\\" "op" "\\" "%" "TYPE" "id" "longid" "var" "..."
alexandra@37892
   187
      *** "\\" "("
alexandra@37892
   188
      val it = None : Thm.cterm Library.option
neuper@37896
   189
\end{verbatim}}
ahirn@37877
   190
alexandra@37892
   191
Das mathematische Wissen w\"achst mit jeder Theorie von ProtoPure bis Isac. In den folgenden Beispielen wird gezeigt, wie das Wissen w\"achst.
ahirn@37877
   192
ahirn@37877
   193
{\footnotesize\begin{verbatim}
ahirn@37877
   194
   > (*-1-*);
ahirn@37877
   195
   > parse HOL.thy "2^^^3";
ahirn@37877
   196
      *** Inner lexical error at: "^^^3"
ahirn@37877
   197
      val it = None : Thm.cterm Library.option         
neuper@37896
   198
\end{verbatim}}
alexandra@37892
   199
''Inner lexical error`` und ''None`` bedeuten, dass ein Fehler aufgetreten ist, denn das Wissen \"uber {\tt *} findet sich erst in der {\tt theorie group}.
ahirn@37877
   200
ahirn@37877
   201
{\footnotesize\begin{verbatim}
ahirn@37877
   202
   > (*-2-*);
ahirn@37877
   203
   > parse HOL.thy "d_d x (a + x)";
ahirn@37877
   204
      val it = None : Thm.cterm Library.option               
neuper@37896
   205
\end{verbatim}}
alexandra@37891
   206
Hier wiederum ist noch kein Wissen \"uber das Differenzieren vorhanden.
ahirn@37877
   207
ahirn@37877
   208
{\footnotesize\begin{verbatim}
ahirn@37877
   209
   > (*-3-*);
ahirn@37877
   210
   > parse Rational.thy "2^^^3";
ahirn@37877
   211
      val it = Some "2 ^^^ 3" : Thm.cterm Library.option               
neuper@37896
   212
\end{verbatim}}
ahirn@37877
   213
ahirn@37877
   214
{\footnotesize\begin{verbatim}
ahirn@37877
   215
   > (*-4-*);
ahirn@37877
   216
   > val Some t4 = parse Rational.thy "d_d x (a + x)";
ahirn@37877
   217
      val t4 = "d_d x (a + x)" : Thm.cterm              
neuper@37896
   218
\end{verbatim}}
ahirn@37877
   219
ahirn@37877
   220
{\footnotesize\begin{verbatim}
ahirn@37877
   221
   > (*-5-*);
ahirn@37877
   222
   > val Some t5 = parse Diff.thy  "d_d x (a + x)";
ahirn@37877
   223
      val t5 = "d_d x (a + x)" : Thm.cterm             
neuper@37896
   224
\end{verbatim}}
alexandra@37892
   225
Die letzen drei Aufgaben k\"onnen schon gel\"ost werden, da {\tt Rational.thy} \"uber das n\"otige Wissen verf\"ugt.
ahirn@37877
   226
ahirn@37877
   227
\section{Details von Termen}
alexandra@37892
   228
Mit Hilfe der darunterliegenden Darstellung sieht man, dass ein cterm in einen Term umgewandelt werden kann.
ahirn@37877
   229
{\footnotesize\begin{verbatim}
ahirn@37877
   230
   > term_of;
ahirn@37877
   231
      val it = fn : Thm.cterm -> Term.term
neuper@37896
   232
\end{verbatim}}
alexandra@37892
   233
Durch die Umwandlung eines cterms in einen Term sieht man die einzelnen Teile des Terms. ''Free`` bedeutet, dass man die Variable \"andern kann.
ahirn@37877
   234
{\footnotesize\begin{verbatim}
ahirn@37877
   235
   > term_of t4;
ahirn@37877
   236
      val it =
ahirn@37877
   237
         Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
ahirn@37877
   238
         ...: Term.term
ahirn@37877
   239
neuper@37896
   240
\end{verbatim}}
alexandra@37891
   241
In diesem Fall sagt uns das ''Const``, dass die Variable eine Konstante ist, also ein Fixwert, der immer die selbe Funktion hat.
ahirn@37877
   242
{\footnotesize\begin{verbatim}
ahirn@37877
   243
   > term_of t5;
ahirn@37877
   244
      val it =
ahirn@37877
   245
         Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $ ... $
ahirn@37877
   246
         ... : Term.term
neuper@37896
   247
\end{verbatim}}
alexandra@37891
   248
Sollten verschiedene Teile des ''output`` (= das vom Computer Ausgegebene) nicht sichtbar sein, kann man mit einem bestimmten Befehl alles angezeigt werden.
ahirn@37877
   249
{\footnotesize\begin{verbatim}
ahirn@37877
   250
   > print_depth;
ahirn@37877
   251
      val it = fn : int -> unit
neuper@37896
   252
 \end{verbatim}}
alexandra@37892
   253
Zuerst gibt man den Befehl ein, danach den Term, der gr\"osser werden soll. Dabei kann man selbst einen Wert f\"ur die L\"ange bestimmen.
ahirn@37877
   254
{\footnotesize\begin{verbatim}
ahirn@37877
   255
   > print_depth 10;
ahirn@37877
   256
      val it = () : unit
ahirn@37877
   257
   > term_of t4;
ahirn@37877
   258
         val it =
ahirn@37877
   259
            Free ("d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877
   260
                Free ("x", "RealDef.real") $
ahirn@37877
   261
            (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877
   262
                Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
ahirn@37877
   263
         : Term.term
ahirn@37877
   264
ahirn@37877
   265
   > print_depth 10;
ahirn@37877
   266
         val it = () : unit
ahirn@37877
   267
   > term_of t5;
ahirn@37877
   268
         val it =
ahirn@37877
   269
            Const ("Diff.d_d", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877
   270
                Free ("x", "RealDef.real") $
ahirn@37877
   271
            (Const ("op +", "[RealDef.real, RealDef.real] => RealDef.real") $
ahirn@37877
   272
                Free ("a", "RealDef.real") $ Free ("x", "RealDef.real"))
ahirn@37877
   273
         : Term.term
neuper@37896
   274
\end{verbatim}}
alexandra@37891
   275
\paragraph{Versuchen Sie es!}
ahirn@37877
   276
Eine andere Variante um den Unterschied der beiden Terme zu sehen ist folgende: 
ahirn@37877
   277
{\footnotesize\begin{verbatim}
ahirn@37877
   278
   > (*-4-*) val thy = Rational.thy;
ahirn@37877
   279
      val thy =
ahirn@37877
   280
         {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
ahirn@37877
   281
         Sum_Type, Relation, Record, Inductive, Transitive_Closure,
ahirn@37877
   282
         Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
ahirn@37877
   283
         SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
ahirn@37877
   284
         Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
ahirn@37877
   285
         IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
ahirn@37877
   286
         Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
ahirn@37877
   287
         RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
ahirn@37877
   288
         Ring_and_Field, Complex_Numbers, Real, ListG, Tools, Script, Typefix,
ahirn@37877
   289
         Float, ComplexI, Descript, Atools, Simplify, Poly, Rational}
ahirn@37877
   290
     : Theory.theory
Walther@60650
   291
   > ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
ahirn@37877
   292
 
ahirn@37877
   293
      ***
ahirn@37877
   294
      *** Free (d_d, [real, real] => real)
ahirn@37877
   295
      *** . Free (x, real)
ahirn@37877
   296
      *** . Const (op +, [real, real] => real)
ahirn@37877
   297
      *** . . Free (a, real)
ahirn@37877
   298
      *** . . Free (x, real)
ahirn@37877
   299
      ***
ahirn@37877
   300
 
ahirn@37877
   301
      val it = () : unit
ahirn@37877
   302
ahirn@37877
   303
ahirn@37877
   304
   > (*-5-*) val thy = Diff.thy;
ahirn@37877
   305
      val thy =
ahirn@37877
   306
         {ProtoPure, CPure, HOL, Set, Typedef, Fun, Product_Type, Lfp, Gfp,
ahirn@37877
   307
         Sum_Type, Relation, Record, Inductive, Transitive_Closure,
ahirn@37877
   308
         Wellfounded_Recursion, NatDef, Nat, NatArith, Divides, Power,
ahirn@37877
   309
         SetInterval, Finite_Set, Equiv, IntDef, Int, Datatype_Universe,
ahirn@37877
   310
         Datatype, Numeral, Bin, IntArith, Wellfounded_Relations, Recdef, IntDiv,
ahirn@37877
   311
         IntPower, NatBin, NatSimprocs, Relation_Power, PreList, List, Map,
ahirn@37877
   312
         Hilbert_Choice, Main, Lubs, PNat, PRat, PReal, RealDef, RealOrd,
ahirn@37877
   313
         RealInt, RealBin, RealArith0, RealArith, RComplete, RealAbs, RealPow,
ahirn@37877
   314
         Ring_and_Field, Complex_Numbers, Real, Calculus, Trig, ListG, Tools,
ahirn@37877
   315
         Script, Typefix, Float, ComplexI, Descript, Atools, Simplify, Poly,
ahirn@37877
   316
         Equation, LinEq, Root, RootEq, Rational, RatEq, RootRat, RootRatEq,
ahirn@37877
   317
         PolyEq, LogExp, Diff} : Theory.theory
ahirn@37877
   318
 
Walther@60650
   319
   > ((TermC.atom_trace_detail \@\{context\}) o term_of o the o (parse thy)) "d_d x (a + x)";
ahirn@37877
   320
 
ahirn@37877
   321
      ***
ahirn@37877
   322
      *** Const (Diff.d_d, [real, real] => real)
ahirn@37877
   323
      *** . Free (x, real)
ahirn@37877
   324
      *** . Const (op +, [real, real] => real)
ahirn@37877
   325
      *** . . Free (a, real)
ahirn@37877
   326
      *** . . Free (x, real)
ahirn@37877
   327
      ***
ahirn@37877
   328
 
ahirn@37877
   329
      val it = () : unit
neuper@37896
   330
\end{verbatim}}
ahirn@37877
   331
ahirn@37877
   332
alexandra@37891
   333
\chapter{''Rewriting``}
alexandra@37891
   334
\section{Was ist Rewriting?}
alexandra@37891
   335
Bei Rewriting handelt es sich um das Umformen von Termen nach vorgegebenen Regeln. Folgende zwei Funktionen sind notwendig:
neuper@37896
   336
{\footnotesize\begin{verbatim}
alexandra@37892
   337
   > rewrite;
alexandra@37892
   338
      val it = fn
alexandra@37892
   339
      :
alexandra@37892
   340
      theory' ->
Walther@60586
   341
      rew_ord ->
alexandra@37892
   342
      rls' -> bool -> thm' -> cterm' -> (string * string list) Library.option
neuper@37896
   343
\end{verbatim}}
alexandra@37892
   344
Die Funktion hat zwei Argumente, die mitgeschickt werden m\"ussen, damit die Funktion arbeiten kann. Das letzte Element {\tt (cterm' * cterm' list) Library.option} im unteren Term ist das Ergebnis, das die Funktionen {\tt rewrite} zur\"uckgeben und die zwei vorhergehenden Argumente, {\tt theorem} und {\tt cterm}, sind die f\"ur uns wichtigen. {\tt Theorem} ist die Rechenregel und {\tt cterm} jene Formel auf die die Rechenregel angewendet wird.
neuper@37896
   345
{\footnotesize\begin{verbatim}
alexandra@37892
   346
   > rewrite_inst;
alexandra@37892
   347
      val it = fn
alexandra@37892
   348
      :
alexandra@37892
   349
      theory' ->
Walther@60586
   350
      rew_ord ->
alexandra@37892
   351
      rls' ->bool -> 'a -> thm' -> cterm' -> (cterm' * cterm' list) Library.option
neuper@37896
   352
\end{verbatim}}
alexandra@37892
   353
Die Funktion {\tt rewrite\_inst} wird ben\"otigt, um Gleichungen, Rechnungen zum Differenzieren etc. zu l\"osen. Dabei wird die gebundene Variable (bdv) instanziiert, d.h. es wird die Variable angegeben, nach der man differenzieren will, bzw. f\"ur die ein Wert bei einer Gleichung herauskommen soll.
alexandra@37892
   354
Um zu sehen wie der Computer vorgeht nehmen wir folgendes Beispiel, dessen Ergebnis offenbar 0 ist, was der Computer jedoch erst nach einer Reihe von Schritten herausfindet.
alexandra@37892
   355
Im Beispiel wird differenziert, wobei \isac's Schreibweise jene von Computer Algebra Systemen (CAS) anzugleichen: in CAS wird differenziert mit $\frac{d}{dx}\; x^2 + 3 \cdot x + 4$, in \isac{} mit {\tt d\_d x (x \^{ }\^{ }\^{ } 2 + 3 * x + 4)}.
alexandra@37891
   356
Zuerst werden die einzelnen Werte als Variablen gespeichert:
neuper@37896
   357
{\footnotesize\begin{verbatim}
alexandra@37892
   358
   > val thy' = "Diff.thy";
alexandra@37892
   359
      val thy' = "Diff.thy" : string
alexandra@37892
   360
   > val ro = "tless_true";
alexandra@37892
   361
      val ro = "tless_true" : string
alexandra@37892
   362
   > val er = "eval_rls";
alexandra@37892
   363
      val er = "eval_rls" : string
alexandra@37892
   364
   > val inst = [("bdv","x::real")];
alexandra@37892
   365
      val inst = [("bdv", "x::real")] : (string * string) list
alexandra@37892
   366
   > val ct = "d_d x (a + a * (2 + b))";
alexandra@37892
   367
      val ct = "d_d x (a + a * (2 + b))" : string
neuper@37896
   368
\end{verbatim}}
alexandra@37892
   369
Nun wird die Rechnung nach den Regeln ausgerechnet, wobei am Ende mehrere Dinge zugleich gemacht werden.
alexandra@37892
   370
Folgende Regeln werden ben\"otigt: Summenregel, Produktregel, Multiplikationsregel mit einem konstanten Faktor und zum Schluss die Additionsregel.
neuper@37896
   371
{\footnotesize\begin{verbatim}
alexandra@37892
   372
   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_sum","") ct;
alexandra@37892
   373
      val ct = "d_d x a + d_d x (a * (2 + b))" : cterm'
alexandra@37892
   374
   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_prod","") ct;
alexandra@37892
   375
      val ct = "d_d x a + (d_d x a * (2 + b) + a * d_d x (2 + b))" : cterm'
alexandra@37892
   376
   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;
alexandra@37892
   377
      val ct = "d_d x a + (d_d x a * (2 + b) + a * 0) " : cterm'
alexandra@37892
   378
   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;
alexandra@37892
   379
      val ct = "d_d x a + (0 * (2 + b) + a * 0)" : cterm'
alexandra@37892
   380
   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_const","") ct;
alexandra@37892
   381
      val ct = "0 + (0 * (2 + b) + a * 0)" : cterm'
alexandra@37892
   382
   > val Some (ct,_) = rewrite_set thy' true "make_polynomial" ct;
alexandra@37892
   383
      val ct = "0" : string
neuper@37896
   384
\end{verbatim}}
alexandra@37892
   385
Was {\tt rewrite\_set} genau macht, finden Sie im n\"achsten Kapitel.
alexandra@37892
   386
alexandra@37892
   387
Dies w\"are ein etwas ernsthafteres Beispiel zum Differenzieren:
neuper@37896
   388
{\footnotesize\begin{verbatim}
alexandra@37892
   389
   > val ct = "d_d x (x ^^^ 2 + 3 * x + 4)";
alexandra@37892
   390
   > val Some (ct,_) = rewrite_inst thy' ro er true inst ("diff_sum","") ct;
neuper@37896
   391
\end{verbatim}}
neuper@37896
   392
\paragraph{Versuchen Sie es,} diese Beispiel zu Ende zu f\"uhren! Die Regeln, die \isac{} kennt und zum Umformen verwenden kann, finden Sie im Internet \footnote{{\tiny\tt http://www.ist.tugraz.at/projects/isac/www/kbase/thy/browser\_info/HOL/HOL-Real/Isac/Diff.html}}.
alexandra@37891
   393
neuper@37896
   394
\section{Welche W\"unsche kann man an Rewriting stellen?}
alexandra@37891
   395
Es gibt verschiedene Varianten von Rewriting, die alle eine bestimmte Bedeutung haben.
alexandra@37892
   396
{\tt rewrite\_ set} wandelt Terme in ein ganzes rule set um, die normalerweise nur mit einem Theorem vereinfacht dargestellt werden.
alexandra@37891
   397
Hierbei werden auch folgende Argumente verwendet:\\
alexandra@37891
   398
\tabcolsep=4mm
alexandra@37891
   399
\def\arraystretch{1.5}
alexandra@37891
   400
\begin{tabular}{lp{11.0cm}}
alexandra@37892
   401
{\tt theory} & Die Theory von Isabelle, die alle n\"otigen Informationen f\"ur das Parsing {\tt term} enth\"alt. \\
alexandra@37892
   402
{\tt rew\_ord}& die Ordnung f\"ur das geordnete Rewriting. F\"ur {\em no} ben\"otigt das geordnete Rewriting {\tt tless\_true}, eine Ordnung, die f\"ur alle nachgiebigen Argumente true ist \\
alexandra@37891
   403
{\tt rls} & Das rule set; zur Auswertung von bestimmten Bedingungen in {\tt thm} falls {\tt thm} eine conditional rule ist \\
alexandra@37892
   404
{\tt bool} & ein Bitschalter, der die Berechnungen der m\"oglichen condition in {\tt thm} ausl\"ost: wenn sie {\tt false} ist, dann wird die condition bewertet und auf Grund des Resultats wendet man {\tt thm} an, oder nicht; wenn {\tt true} dann wird die condition nicht ausgewertet, aber man gibt sie in eine Menge von Hypothesen \\
alexandra@37891
   405
{\tt thm} & das theorem versucht den {\tt term} zu \"uberschreiben \\
alexandra@37891
   406
{\tt term} & {\tt thm} wendet Rewriting m\"oglicherweise auf den Term an \\
alexandra@37891
   407
\end{tabular}\\
alexandra@37891
   408
neuper@37896
   409
{\footnotesize\begin{verbatim}
alexandra@37892
   410
   > rewrite_set;
alexandra@37892
   411
      val it = fn : theory' -> bool -> rls' -> ...
neuper@37896
   412
\end{verbatim}}
neuper@37896
   413
{\footnotesize\begin{verbatim}
alexandra@37892
   414
   > rewrite_set_inst;
alexandra@37892
   415
      val it = fn : theory' -> bool -> subs' -> .
neuper@37896
   416
\end{verbatim}}
alexandra@37892
   417
Wenn man sehen m\"ochte wie Rewriting bei den einzelnen theorems funktioniert kann man dies mit {\tt trace\_rewrite} versuchen.
neuper@37896
   418
{\footnotesize\begin{verbatim}
alexandra@37892
   419
   > trace_rewrite := true;
alexandra@37892
   420
      val it = () : unit
neuper@37896
   421
\end{verbatim}}
alexandra@37891
   422
alexandra@37891
   423
alexandra@37882
   424
\section{Rule sets}
alexandra@37891
   425
Einige der oben genannten Varianten von Rewriting beziehen sich nicht nur auf einen theorem, sondern auf einen ganzen Block von theorems, die man als rule set bezeichnet.
alexandra@37882
   426
Dieser wird so lange angewendet, bis ein Element davon f\"ur Rewriting verwendet werden kann. Sollte der Begriff ''terminate`` fehlen, wird das Rule set nicht beendet und l\"auft weiter.
alexandra@37891
   427
Ein Beispiel f\"ur einen rule set ist folgendes:
neuper@37896
   428
{\footnotesize\begin{verbatim}
alexandra@37882
   429
???????????
neuper@37896
   430
\end{verbatim}}
ahirn@37877
   431
neuper@37896
   432
{\footnotesize\begin{verbatim}
alexandra@37882
   433
   > sym;
alexandra@37882
   434
      val it = "?s = ?t ==> ?t = ?s" : Thm.thm
alexandra@37882
   435
   > rearrange_assoc;
alexandra@37882
   436
      val it =
alexandra@37882
   437
         Rls
alexandra@37882
   438
            {id = "rearrange_assoc",
Walther@60586
   439
               program = Script (Free ("empty_script", "RealDef.real")),
alexandra@37882
   440
               calc = [],
Walther@60586
   441
               asm_rls =
alexandra@37882
   442
               Rls
alexandra@37882
   443
                  {id = "e_rls",
Walther@60586
   444
                     program = EmptyScr,
alexandra@37882
   445
                     calc = [],
Walther@60586
   446
                     asm_rls = Erls,
Walther@60586
   447
                     prog_rls = Erls,
alexandra@37882
   448
                     rules = [],
alexandra@37882
   449
                     rew_ord = ("dummy_ord", fn),
alexandra@37882
   450
                     preconds = []},
Walther@60586
   451
               prog_rls =
alexandra@37882
   452
               Rls
alexandra@37882
   453
                  {id = "e_rls",
Walther@60586
   454
                     program = EmptyScr,
alexandra@37882
   455
                     calc = [],
Walther@60586
   456
                     asm_rls = Erls,
Walther@60586
   457
                     prog_rls = Erls,
alexandra@37882
   458
                     rules = [],
alexandra@37882
   459
                     rew_ord = ("dummy_ord", fn),
alexandra@37882
   460
                     preconds = []},
alexandra@37882
   461
               rules =
alexandra@37882
   462
               [Thm ("sym_radd_assoc", "?m1 + (?n1 + ?k1) = ?m1 + ?n1 + ?k1"  [.]),
alexandra@37882
   463
                  Thm
alexandra@37882
   464
                     ("sym_rmult_assoc",
alexandra@37882
   465
                        "?m1 * (?n1 * ?k1) = ?m1 * ?n1 * ?k1"  [.])],
Walther@60509
   466
               rew_ord = ("Rewrite_Ord.id_empty", fn),
alexandra@37882
   467
               preconds = []} : rls
neuper@37896
   468
\end{verbatim}}
ahirn@37877
   469
ahirn@37877
   470
alexandra@37882
   471
\section{Berechnung von Konstanten}
alexandra@37882
   472
Sobald Konstanten in dem Bereich des Subterms sind, k\"onnen sie von einer Funktion berechnet werden:
neuper@37896
   473
{\footnotesize\begin{verbatim}
alexandra@37882
   474
   > calculate;
alexandra@37882
   475
      val it = fn
alexandra@37882
   476
      :
alexandra@37882
   477
         theory' ->
alexandra@37882
   478
         string *
alexandra@37882
   479
         (
alexandra@37882
   480
         string ->
alexandra@37882
   481
         Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
alexandra@37882
   482
         cterm' -> (string * thm') Library.option
ahirn@37877
   483
alexandra@37882
   484
   > calculate_;
alexandra@37882
   485
      val it = fn
alexandra@37882
   486
      :
alexandra@37882
   487
         Theory.theory ->
alexandra@37882
   488
         string *
alexandra@37882
   489
         (
alexandra@37882
   490
         string ->
alexandra@37882
   491
         Term.term -> Theory.theory -> (string * Term.term) Library.option) ->
alexandra@37882
   492
         Term.term -> (Term.term * (string * Thm.thm)) Library.option
neuper@37896
   493
\end{verbatim}}
alexandra@37891
   494
Man bekommt das Ergebnis und das theorem bezieht sich darauf. Daher sind die folgenden mathematischen Rechnungen m\"oglich:
neuper@37896
   495
{\footnotesize\begin{verbatim}
alexandra@37882
   496
   > calclist;
alexandra@37882
   497
      val it =
alexandra@37882
   498
         [("Vars", ("Tools.Vars", fn)), ("matches", ("Tools.matches", fn)),
alexandra@37882
   499
            ("lhs", ("Tools.lhs", fn)), ("plus", ("op +", fn)),
alexandra@37882
   500
            ("times", ("op *", fn)), ("divide_", ("HOL.divide", fn)),
alexandra@37882
   501
            ("power_", ("Atools.pow", fn)), ("is_const", ("Atools.is'_const", fn)),
alexandra@37882
   502
            ("le", ("op <", fn)), ("leq", ("op <=", fn)),
alexandra@37882
   503
            ("ident", ("Atools.ident", fn)), ("sqrt", ("Root.sqrt", fn)),
alexandra@37882
   504
            ("Test.is_root_free", ("is'_root'_free", fn)),
alexandra@37882
   505
            ("Test.contains_root", ("contains'_root", fn))]
alexandra@37882
   506
      :
alexandra@37882
   507
         (
alexandra@37882
   508
         string *
alexandra@37882
   509
         (
alexandra@37882
   510
         string *
alexandra@37882
   511
         (
alexandra@37882
   512
         string ->
alexandra@37882
   513
         Term.term -> Theory.theory -> (string * Term.term) Library.option))) list
neuper@37896
   514
\end{verbatim}}
alexandra@37891
   515
ahirn@37877
   516
ahirn@37877
   517
ahirn@37877
   518
alexandra@37882
   519
\chapter{Termordnung}
alexandra@37891
   520
Die Anordnungen der Begriffe sind unverzichtbar f\"ur den Gebrauch des Umschreibens von normalen Funktionen und von normalen Formeln, die n\"otig sind um passende Modelle f\"ur Probleme zu finden.
alexandra@37882
   521
alexandra@37882
   522
\section{Beispiel f\"ur Termordnungen}
alexandra@37891
   523
Es ist nicht unbedeutend, eine Verbindung zu Termen herzustellen, die wirklich eine Ordnung besitzen. Diese Ordnungen sind selbstaufrufende Bahnordnungen:
alexandra@37882
   524
alexandra@37882
   525
{\footnotesize\begin{verbatim}
alexandra@37882
   526
   > sqrt_right;
alexandra@37882
   527
      val it = fn : bool -> Theory.theory -> subst -> Term.term * Term.term -> b       ool
alexandra@37882
   528
   > tless_true;
alexandra@37882
   529
      val it = fn : subst -> Term.term * Term.term -> bool
neuper@37896
   530
\end{verbatim}}
alexandra@37882
   531
alexandra@37891
   532
Das ''bool`` Argument gibt Ihnen die M\"oglichkeit, die Kontrolle zu den zugeh\"origen Unterordunungen zur\"uck zu verfolgen, damit sich die Unterordnungen, die 'true' sind, als strings anzeigen lassen.
alexandra@37882
   533
alexandra@37888
   534
{\section{Geordnetes Rewriting}}
alexandra@37892
   535
Beim Rewriting entstehen Probleme, die vom ''law of commutativity`` (= Kommutativgesetz) durch '+' und '*' verursacht werden. Diese Probleme k\"onnen nur durch geordnetes Rewriting gel\"ost werden, da hier ein Term nur umgeschrieben wird, wenn ein kleinerer dadurch entsteht.
alexandra@37888
   536
alexandra@37888
   537
alexandra@37891
   538
\chapter{Problem hierachy}
alexandra@37888
   539
\section{''Matching``}
alexandra@37891
   540
Matching ist eine Technik von Rewriting, die von \isac{} verwendet wird, um ein Problem und den passenden problem type daf\"ur zu finden. Die folgende Funktion \"uberpr\"uft, ob Matching m\"oglich ist:
alexandra@37888
   541
{\footnotesize\begin{verbatim}
alexandra@37888
   542
> matches;
alexandra@37888
   543
val it = fn : Theory.theory -> Term.term -> Term.term -> bool
neuper@37896
   544
\end{verbatim}}
alexandra@37888
   545
Die folgende Gleichung wird in Operatoren und freie Variablen zerlegt.
alexandra@37888
   546
{\footnotesize\begin{verbatim}
alexandra@37888
   547
> val t = (term_of o the o (parse thy)) "3 * x^^^2 = 1";
alexandra@37888
   548
val t =
alexandra@37888
   549
Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888
   550
(Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888
   551
Free ("3", "RealDef.real") $
alexandra@37888
   552
(Const
alexandra@37888
   553
("Atools.pow",
alexandra@37888
   554
"[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888
   555
Free ("x", "RealDef.real") $ Free ("2", " RealDef.real"))) $
alexandra@37888
   556
Free ("1", "RealDef.real") : Term.term
neuper@37896
   557
\end{verbatim}}
alexandra@37891
   558
Nun wird ein Modell erstellt, das sich nicht auf bestimmte Zahlen bezieht, sondern nur eine generelle Zerlegung durchf\"uhrt.
alexandra@37888
   559
{\footnotesize\begin{verbatim}
alexandra@37888
   560
> val p = (term_of o the o (parse thy)) "a * b^^^2 = c";
alexandra@37888
   561
val p =
alexandra@37888
   562
Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888
   563
(Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888
   564
Free ("a", "RealDef.real") $
alexandra@37888
   565
(Const
alexandra@37888
   566
("Atools.pow",
alexandra@37888
   567
"[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888
   568
Free ("b", "RealDef.real") $ Free ("2", "RealDef.real"))) $
alexandra@37888
   569
Free ("c", "RealDef.real") : Term.term
neuper@37896
   570
\end{verbatim}}
alexandra@37891
   571
Dieses Modell enth\"alt sogenannte \textit{scheme variables}.
alexandra@37888
   572
{\footnotesize\begin{verbatim}
alexandra@37888
   573
> atomt p;
alexandra@37888
   574
"*** -------------"
alexandra@37888
   575
"*** Const (op =)"
alexandra@37888
   576
"*** . Const (op *)""*** . . Free (a, )"
alexandra@37888
   577
"*** . . Const (Atools.pow)"
alexandra@37888
   578
"*** . . . Free (b, )"
alexandra@37888
   579
"*** . . . Free (2, )"
alexandra@37888
   580
"*** . Free (c, )"
alexandra@37888
   581
"\n"
alexandra@37888
   582
val it = "\n" : string
neuper@37896
   583
\end{verbatim}}
Walther@60650
   584
Das Modell wird durch den Befehl \textit{mk_Var} erstellt.
alexandra@37888
   585
{\footnotesize\begin{verbatim}
Walther@60650
   586
> mk_Var;
alexandra@37888
   587
val it = fn : Term.term -> Term.term
Walther@60650
   588
> val pat = mk_Var p;
alexandra@37888
   589
val pat =
alexandra@37888
   590
Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888
   591
(Const ("op *", "[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888
   592
Var (("a", 0), "RealDef.real") $
alexandra@37888
   593
(Const
alexandra@37888
   594
("Atools.pow",
alexandra@37888
   595
"[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888
   596
Var (("b", 0), "RealDef.real") $
alexandra@37888
   597
Free ("2", "RealDef.real"))) $ Var (("c", 0), "RealDef.real")
alexandra@37888
   598
: Term.term
alexandra@37888
   599
> Sign.string_of_term (sign_of thy) pat;
alexandra@37888
   600
val it = "?a * ?b ^^^ 2 = ?c" : string
neuper@37896
   601
\end{verbatim}}
alexandra@37892
   602
Durch \textit{atomt pat} wird der Term aufgespalten und in eine Form gebracht, die f\"ur die weiteren Schritte ben\"otigt wird.
alexandra@37888
   603
{\footnotesize\begin{verbatim}
alexandra@37888
   604
> atomt pat;
alexandra@37888
   605
"*** -------------"
alexandra@37888
   606
"*** Const (op =)"
alexandra@37888
   607
"*** . Const (op *)"
alexandra@37888
   608
"*** . . Var ((a, 0), )"
alexandra@37888
   609
"*** . . Const (Atools.pow)"
alexandra@37888
   610
"*** . . . Var ((b, 0), )"
alexandra@37888
   611
"*** . . . Free (2, )"
alexandra@37888
   612
"*** . Var ((c, 0), )"
alexandra@37888
   613
"\n"
alexandra@37888
   614
val it = "\n" : string
neuper@37896
   615
\end{verbatim}}
alexandra@37891
   616
Jetzt kann das Matching an den beiden vorigen Terme angewendet werden.
alexandra@37888
   617
{\footnotesize\begin{verbatim}
alexandra@37888
   618
> matches thy t pat;
alexandra@37888
   619
val it = true : bool
alexandra@37888
   620
> val t2 = (term_of o the o (parse thy)) "x^^^2 = 1";
alexandra@37888
   621
val t2 =
alexandra@37888
   622
Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888
   623
(Const
alexandra@37888
   624
("Atools.pow",
alexandra@37888
   625
"[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888
   626
Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
alexandra@37888
   627
Free ("1", "RealDef.real") : Term.term
alexandra@37888
   628
> matches thy t2 pat;
alexandra@37888
   629
val it = false : bool
alexandra@37888
   630
> val pat2 = (term_of o the o (parse thy)) "?u^^^2 = ?v";
alexandra@37888
   631
val pat2 =
alexandra@37888
   632
Const ("op =", "[RealDef.real, RealDef.real] => bool") $
alexandra@37888
   633
(Const
alexandra@37888
   634
("Atools.pow",
alexandra@37888
   635
"[RealDef.real, RealDef.real] => RealDef.real") $
alexandra@37888
   636
Var (("u", 0), "RealDef.real") $ Free ("2", "RealDef.real")) $
alexandra@37888
   637
Var (("v", 0), "RealDef.real") : Term.term
alexandra@37888
   638
> matches thy t2 pat2;
alexandra@37888
   639
val it = true : bool
neuper@37896
   640
\end{verbatim}}
alexandra@37888
   641
alexandra@37891
   642
\section{Zugriff auf die hierachy}
alexandra@37891
   643
Man verwendet folgenden Befehl, um sich Zugang zur hierachy von problem type zu verschaffen.
alexandra@37888
   644
{\footnotesize\begin{verbatim}
alexandra@37888
   645
> show_ptyps;
alexandra@37888
   646
val it = fn : unit -> unit
alexandra@37888
   647
> show_ptyps();
alexandra@37888
   648
[
alexandra@37888
   649
["e_pblID"],
alexandra@37888
   650
["simplification", "polynomial"],
alexandra@37888
   651
["simplification", "rational"],
alexandra@37888
   652
["vereinfachen", "polynom", "plus_minus"],
alexandra@37888
   653
["vereinfachen", "polynom", "klammer"],
alexandra@37888
   654
["vereinfachen", "polynom", "binom_klammer"],
alexandra@37888
   655
["probe", "polynom"],
alexandra@37888
   656
["probe", "bruch"],
alexandra@37888
   657
["equation", "univariate", "linear"],
alexandra@37888
   658
["equation", "univariate", "root", "sq", "rat"],
alexandra@37888
   659
["equation", "univariate", "root", "normalize"],
alexandra@37888
   660
["equation", "univariate", "rational"],
alexandra@37888
   661
["equation", "univariate", "polynomial", "degree_0"],
alexandra@37888
   662
["equation", "univariate", "polynomial", "degree_1"],
alexandra@37888
   663
["equation", "univariate", "polynomial", "degree_2", "sq_only"],
alexandra@37888
   664
["equation", "univariate", "polynomial", " 
alexandra@37888
   665
 degree_2", "bdv_only"],
alexandra@37888
   666
["equation", "univariate", "polynomial", "degree_2", "pqFormula"],
alexandra@37888
   667
["equation", "univariate", "polynomial", "degree_2", "abcFormula"],
alexandra@37888
   668
["equation", "univariate", "polynomial", "degree_3"],
alexandra@37888
   669
["equation", "univariate", "polynomial", "degree_4"],
alexandra@37888
   670
["equation", "univariate", "polynomial", "normalize"],
alexandra@37888
   671
["equation", "univariate", "expanded", "degree_2"],
alexandra@37888
   672
["equation", "makeFunctionTo"],
alexandra@37888
   673
["function", "derivative_of", "named"],
alexandra@37888
   674
["function", "maximum_of", "on_interval"],
alexandra@37888
   675
["function", "make", "by_explicit"],
alexandra@37888
   676
["function", "make", "by_new_variable"],
alexandra@37888
   677
["function", "integrate", "named"],
alexandra@37888
   678
["tool", "find_values"],
alexandra@37888
   679
["system", "linear", "2x2", "triangular"],
alexandra@37888
   680
["system", "linear", "2x2", "normalize"],
alexandra@37888
   681
["system", "linear", "3x3"],
alexandra@37888
   682
["system", "linear", "4x4", "triangular"],
alexandra@37888
   683
["system", "linear", "4x4", "normalize"],
alexandra@37888
   684
["Biegelinien", "
alexandra@37888
   685
MomentBestimmte"],
alexandra@37888
   686
["Biegelinien", "MomentGegebene"],
alexandra@37888
   687
["Biegelinien", "einfache"],
alexandra@37888
   688
["Biegelinien", "QuerkraftUndMomentBestimmte"],
alexandra@37888
   689
["Biegelinien", "vonBelastungZu"],
alexandra@37888
   690
["Biegelinien", "setzeRandbedingungen"],
alexandra@37888
   691
["Berechnung", "numerischSymbolische"],
alexandra@37888
   692
["test", "equation", "univariate", "linear"],
alexandra@37888
   693
["test", "equation", "univariate", "plain_square"],
alexandra@37888
   694
["test", "equation", "univariate", "polynomial", "degree_two", "pq_formula"],
alexandra@37888
   695
["test", "equation", "univariate", "polynomial", "degree_two", "abc_formula"],
alexandra@37888
   696
["test", "equation", "univariate", "squareroot"],
alexandra@37888
   697
["test", "equation", "univariate", "normalize"],
alexandra@37888
   698
["test", "equation", "univariate", "sqroot-test"]
alexandra@37888
   699
]
alexandra@37888
   700
val it = () : unit
neuper@37896
   701
\end{verbatim}}
alexandra@37888
   702
alexandra@37891
   703
\section{Die passende ''formalization`` f\"ur den problem type}
alexandra@37891
   704
Eine andere Art des Matching ist es die richtige ''formalization`` zum jeweiligen problem type zu finden. Wenn eine solche vorhanden ist, kann \isac{} selbstst\"andig die Probleme l\"osen.
alexandra@37888
   705
alexandra@37891
   706
\section{''problem-refinement``}
alexandra@37891
   707
Will man die problem hierachy (= ) aufstellen, so ist darauf zu achten, dass man die verschiedenen Branches so konstruiert, dass das problem-refinement automatisch durchgef\"uhrt werden kann.
alexandra@37888
   708
{\footnotesize\begin{verbatim}
alexandra@37888
   709
> refine;
alexandra@37888
   710
val it = fn : fmz_ -> pblID -> SpecifyTools.match list
alexandra@37888
   711
> val fmz = ["equality (sqrt(9 + 4 * x)=sqrt x 
alexandra@37888
   712
+ sqrt (5 + x))",
alexandra@37888
   713
# "soleFor x","errorBound (eps=0)",
alexandra@37888
   714
# "solutions L"];
alexandra@37888
   715
val fmz =
alexandra@37888
   716
["equality (sqrt(9 + 4 * x)=sqrt x + sqrt (5 + x))", "soleFor x",
alexandra@37888
   717
"errorBound (eps=0)", ...] : string list
alexandra@37888
   718
> refine fmz ["univariate","equation"];
alexandra@37888
   719
*** pass ["equation","univariate"]
alexandra@37888
   720
*** comp_dts: ??.empty $ soleFor x
alexandra@37888
   721
Exception- ERROR raised
neuper@37896
   722
\end{verbatim}}
alexandra@37891
   723
Wenn die ersten zwei Regeln nicht angewendet werden k\"onnen, kommt die dritte zum Einsatz:
alexandra@37888
   724
{\footnotesize\begin{verbatim}
alexandra@37888
   725
> val fmz = ["equality (x + 1 = 2)",
alexandra@37888
   726
# "solveFor x","errorBound (eps=0)",
alexandra@37888
   727
# "solutions L"];
alexandra@37888
   728
val fmz = ["equality (x + 1 = 2)", "solveFor x", "errorBound (eps=0)", ...]
alexandra@37888
   729
: string list
alexandra@37888
   730
> refine fmz ["univariate","equation"];
alexandra@37888
   731
*** pass ["equation","univariate"]
alexandra@37888
   732
*** pass ["equation","univariate","linear"]
alexandra@37888
   733
*** pass ["equation","univariate","root"]
alexandra@37888
   734
*** pass ["equation","univariate","rational"]
alexandra@37888
   735
*** pass ["equation","univariate","polynomial" ]
alexandra@37888
   736
*** pass ["equation","univariate","polynomial","degree_0"]
alexandra@37888
   737
*** pass ["equation","univariate","polynomial","degree_1"]
alexandra@37888
   738
*** pass ["equation","univariate","polynomial","degree_2"]
alexandra@37888
   739
*** pass ["equation","univariate","polynomial","degree_3"]
alexandra@37888
   740
*** pass ["equation","univariate","polynomial","degree_4"]
alexandra@37888
   741
*** pass ["equation","univariate","polynomial","normalize"]
alexandra@37888
   742
val it =
alexandra@37888
   743
[Matches
alexandra@37888
   744
(["univariate", "equation"],
alexandra@37888
   745
{Find = [Correct "solutions L"], With = [...], ...}),
alexandra@37888
   746
NoMatch (["linear", "univariate", ...], {Find = [...], ...}),
alexandra@37888
   747
NoMatch (["root", ...], ...), ...] : SpecifyTools.match list
neuper@37896
   748
\end{verbatim}}
alexandra@37891
   749
Der problem type wandelt $x + 1 = 2$ in die normale Form $-1 + x = 0$ um. Diese Suche nach der jeweiligen problem hierachy kann mit Hilfe eines ''proof state`` durchgef\"uhrt werden (siehe n\"achstes Kapitel).
alexandra@37882
   750
alexandra@37887
   751
alexandra@37891
   752
\chapter{''Methods``}
alexandra@37891
   753
Methods werden dazu verwendet, Probleme von type zu l\"osen. Sie sind in einer anderen Programmiersprache beschrieben. Die Sprache sieht einfach aus, betreibt aber im Hintergrund einen enormen Pr\"ufaufwand. So muss sich der Programmierer nicht mit technischen Details befassen, gleichzeitig k\"onnen aber auch keine falschen Anweisungen eingegeben werden.
alexandra@37891
   754
\section{Der ''Syntax`` des script}
alexandra@37882
   755
Syntax beschreibt den Zusammenhang der einzelnen Zeichen und Zeichenfolgen mit den Theorien.
alexandra@37882
   756
Er kann so definiert werden:
alexandra@37882
   757
\begin{tabbing}
alexandra@37882
   758
123\=123\=expr ::=\=$|\;\;$\=\kill
alexandra@37882
   759
\>script ::= {\tt Script} id arg$\,^*$ = body\\
alexandra@37882
   760
\>\>arg ::= id $\;|\;\;($ ( id :: type ) $)$\\
alexandra@37882
   761
\>\>body ::= expr\\
alexandra@37882
   762
\>\>expr ::= \>\>{\tt let} id = expr $($ ; id = expr$)^*$ {\tt in} expr\\
alexandra@37882
   763
\>\>\>$|\;$\>{\tt if} prop {\tt then} expr {\tt else} expr\\
alexandra@37882
   764
\>\>\>$|\;$\>listexpr\\
alexandra@37882
   765
\>\>\>$|\;$\>id\\
alexandra@37882
   766
\>\>\>$|\;$\>seqex id\\
alexandra@37882
   767
\>\>seqex ::= \>\>{\tt While} prop {\tt Do} seqex\\
alexandra@37882
   768
\>\>\>$|\;$\>{\tt Repeat} seqex\\
alexandra@37882
   769
\>\>\>$|\;$\>{\tt Try} seqex\\
alexandra@37882
   770
\>\>\>$|\;$\>seqex {\tt Or} seqex\\
alexandra@37882
   771
\>\>\>$|\;$\>seqex {\tt @@} seqex\\
alexandra@37882
   772
\>\>\>$|\;$\>tac $($ id $|$ listexpr $)^*$\\
alexandra@37882
   773
\>\>type ::= id\\
alexandra@37882
   774
\>\>tac ::= id
neuper@37896
   775
\end{tabbing}
ahirn@37877
   776
alexandra@37887
   777
\section{\"Uberpr\"ufung der Auswertung}
alexandra@37887
   778
Das Kontrollsystem arbeitet mit den folgenden Script-Ausdr\"ucken, die {\it tacticals} genannt werden:
alexandra@37887
   779
\begin{description}
alexandra@37887
   780
\item{{\tt while} prop {\tt Do} expr id} 
alexandra@37887
   781
\item{{\tt if} prop {\tt then} expr {\tt else} expr}
alexandra@37887
   782
\end{description}
alexandra@37891
   783
W\"ahrend die genannten Befehle das Kontrollsystem durch Auswertung der Formeln ausl\"osen, h\"angen die anderen von der Anwendbarkeit der Formel in den entsprechenden Unterbegriffen ab:
alexandra@37887
   784
\begin{description}
alexandra@37887
   785
\item{{\tt Repeat} expr id}
alexandra@37887
   786
\item{{\tt Try} expr id}
alexandra@37887
   787
\item{expr {\tt Or} expr id}
alexandra@37887
   788
\item{expr {\tt @@} expr id}
alexandra@37887
   789
\item xxx
alexandra@37887
   790
\end{description}
alexandra@37887
   791
alexandra@37887
   792
alexandra@37888
   793
alexandra@37888
   794
\chapter{Befehle von \isac{}}
alexandra@37889
   795
In diesem Kapitel werden alle schon zur Verf\"ugung stehenden Schritte aufgelistet. Diese Liste kann sich auf Grund von weiteren Entwicklungen von \isac{} noch \"andern.\
alexandra@37891
   796
\newline\linebreak \textbf{Init\_Proof\_Hid (dialogmode, formalization, specifictaion)} gibt die eingegebenen Befehle an die mathematic engine weiter, wobei die beiden letzten Begriffe die Beispiele automatisch speichern. Es ist nicht vorgesehen, dass der Sch\"uler tactic verwendet.\
alexandra@37891
   797
\newline\linebreak \textbf{Init\_Proof} bildet mit einem ''proof tree`` ein leeres Modell.\
alexandra@37891
   798
\newline\linebreak \textbf{Model\_Problem problem} bestimmt ein problemtype, das wom\"oglich in der ''hierachy`` gefunden wurde, und verwendet es f\"ur das Umformen.\
alexandra@37891
   799
\newline\linebreak \textbf{Add\_Given, Add\_Find, Add\_Relation formula} f\"ugt eine Formel in ein bestimmtes Feld eines Modells ein. Dies ist notwendig, solange noch kein Objekt f\"ur den Benutzer vorhanden ist, in dem man die Formel eingeben kann, und nicht die gew\"unschte tactic und Formel von einer Liste w\"ahlen will.\
alexandra@37891
   800
\newline\linebreak \textbf{Specify\_Theorie theory, Specify\_Problem proble, Specify\_Method method} gibt das entsprechende Element des Basiswissens an.\
alexandra@37891
   801
\newline\linebreak \textbf{Refine\_Problem problem} sucht nach einem Problem in der hierachy, das auf das vorhandene zutrifft.\
alexandra@37891
   802
\newline\linebreak \textbf{Apply\_Method method} beendet das Modell und die Beschreibung. Danach wird die L\"osungmeldung ge\"offnet.\
alexandra@37891
   803
\newline\linebreak \textbf{Free\_Solve} beginnt eine L\"osungsmeldung ohne die Hilfe einer method.\
alexandra@37891
   804
\newline\linebreak \textbf{Rewrite theorem} bef\"ordert ein theorem in die aktuelle Formel und wandelt es demenetsprechend um. Wenn dies nicht m\"oglich ist, kommt eine Meldung mit ''error``.\
alexandra@37891
   805
\newline\linebreak \textbf{Rewrite\_Asm theorem} hat die gleiche Funktion wie Rewrite, speichert jedoch eine endg\"ultige Vorraussetzung des theorems, anstatt diese zu sch\"atzen.\
alexandra@37891
   806
\newline\linebreak \textbf{Rewrite\_Set ruleset} hat \"ahnliche Funktionen wie Rewrite, gilt aber f\"ur einen ganzen Satz von theorems, dem rule set.\
alexandra@37891
   807
\newline\linebreak \textbf{Rewrite\_Inst (substitution, theorem), Rewrite\_Set\_Inst (substitution, rule set)} ist vergleichbar mit besonderen tactics, ersetzt aber Konstanten im theorem, bevor es zu einer Anwendung kommt.\
alexandra@37891
   808
\newline\linebreak \textbf{Calculate operation} berechnet das Ergebnis der Eingabe mit der aktuellen Formel (plus, minus, times, cancel, pow, sqrt).\
alexandra@37891
   809
\newline\linebreak \textbf{Substitute substitution} f\"ugt der momentanen Formel {\tt substitution} hinzu und wandelt es um.\
alexandra@37891
   810
\newline\linebreak \textbf{Take formula} startet eine neue Reihe von Rechnungen in den Formeln, wo sich schon eine andere Rechnung befindet.\
alexandra@37891
   811
\newline\linebreak \textbf{Subproblem (theory, problem)} beginnt ein subproblem innerhalb einer Rechnung.\
alexandra@37891
   812
\newline\linebreak \textbf{Function formula} ruft eine Funktion auf, in der der Name in der Formel enthalten ist. ???????\
alexandra@37891
   813
\newline\linebreak \textbf{Split\_And, Conclude\_And, Split\_Or, Conclude\_Or, Begin\_Trans, End\_Trans, Begin\_Sequ, End\_Sequ, Split\_Intersect, End\_Intersect} betreffen den Bau einzelner branches des proof trees. Normalerweise werden sie vom dialog guide verdr\"angt.\
alexandra@37891
   814
\newline\linebreak \textbf{Check\_elementwise assumption} wird in Bezug auf die aktuelle Formel verwendet, die Elemente in einer Liste enth\"alt.\
alexandra@37891
   815
\newline\linebreak \textbf{Or\_to\_List} wandelt eine Verbindung von Gleichungen in eine Liste von Gleichungen um.\
alexandra@37891
   816
\newline\linebreak \textbf{Check\_postcond} \"uberpr\"uft die momentane Formel im Bezug auf die Nachbedinung beim Beenden des subproblem.\
alexandra@37891
   817
\newline\linebreak \textbf{End\_Proof} beendet eine \"Uberpr\"ufung und gibt erst dann ein Ergebnis aus, wenn Check\_postcond erfolgreich abgeschlossen wurde.
alexandra@37888
   818
alexandra@37889
   819
\section{Die Funktionsweise der mathematic engine}
alexandra@37891
   820
Ein proof (= Beweis) wird in der mathematic engine me von der tactic {\tt Init\_Proof} gestartet und wird wechselwirkend mit anderen tactics vorangebracht. Auf den input (= das, was eingegeben wurde) einzelner tactics folgt eine Formel, die von der me ausgegeben wird, und die darauf folgende tactic gilt. Der proof ist beendet, sobald die me {\tt End\_Proof} als n\"achste tactic vorschl\"agt.
alexandra@37889
   821
\newline Im Anschluss werden Sie einen Rechenbeweis sehen, der von der L\"osung einer Gleichung (= equation) handelt, bei der diese automatisch differenziert wird. 
alexandra@37889
   822
{\footnotesize\begin{verbatim}
alexandra@37889
   823
??????????????????????????????????????????????????????????????????????????????????   
alexandra@37888
   824
alexandra@37889
   825
ML> val fmz = ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x",
ahirn@37877
   826
                  "errorBound (eps=#0)","solutions L"];
ahirn@37877
   827
   val fmz =
ahirn@37877
   828
     ["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
ahirn@37877
   829
      "solutions L"] : string list
ahirn@37877
   830
   ML>
ahirn@37877
   831
   ML> val spec as (dom, pbt, met) = ("SqRoot.thy",["univariate","equation"],
ahirn@37877
   832
                                 ("SqRoot.thy","no_met"));
ahirn@37877
   833
   val dom = "SqRoot.thy" : string
ahirn@37877
   834
   val pbt = ["univariate","equation"] : string list
ahirn@37877
   835
   val met = ("SqRoot.thy","no_met") : string * string
neuper@37896
   836
\end{verbatim}}
ahirn@37877
   837
alexandra@37889
   838
\section{Der Beginn einer Rechnung}
alexandra@37891
   839
alexandra@37891
   840
Der proof state wird von einem proof tree und einer position ausgegeben. Beide sind zu Beginn leer. Die tactic {\tt Init\_Proof} ist, wie alle anderen tactics auch, an einen string gekoppelt. Um einen neuen proof beginnen zu k\"onnen, werden folgende Schritte durchgef\"uhrt:
neuper@37896
   841
{\footnotesize\begin{verbatim}
alexandra@37889
   842
???????????????????????????????????????????????????????????????????????????????????????????? 
alexandra@37889
   843
ML>  val (mID,m) = ("Init_Proof",Init_Proof (fmz, (dom,pbt,met)));
ahirn@37877
   844
   val mID = "Init_Proof" : string
ahirn@37877
   845
   val m =
ahirn@37877
   846
     Init_Proof
ahirn@37877
   847
       (["equality ((x+#1)*(x+#2)=x^^^#2+#8)","solveFor x","errorBound (eps=#0)",
ahirn@37877
   848
         "solutions L"],("SqRoot.thy",[#,#],(#,#))) : mstep
ahirn@37877
   849
   ML>
ahirn@37877
   850
   ML>  val (p,_,f,nxt,_,pt) = me (mID,m) e_pos' c EmptyPtree;
ahirn@37877
   851
   val p = ([],Pbl) : pos'
ahirn@37877
   852
   val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
ahirn@37877
   853
   val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
ahirn@37877
   854
     : string * mstep
ahirn@37877
   855
   val pt =
ahirn@37877
   856
     Nd
ahirn@37877
   857
       (PblObj
ahirn@37877
   858
          {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
wneuper@59279
   859
           result=#,spec=#},[]) : ctree
neuper@37896
   860
\end{verbatim}}
alexandra@37891
   861
Die mathematics engine gibt etwas mit dem type {\tt mout} aus, was in unserem Fall ein Problem darstellt. Sobald mehr angezeigt wird, m\"usste dieses jedoch gel\"ost sein.
neuper@37896
   862
{\footnotesize\begin{verbatim}
alexandra@37889
   863
?????????????????????????????????????????????????????????????????????????????????????????????
ahirn@37877
   864
   ML> Compiler.Control.Print.printDepth:=8; (*4 default*)
ahirn@37877
   865
   val it = () : unit
ahirn@37877
   866
   ML>
ahirn@37877
   867
   ML> f;
ahirn@37877
   868
   val it =
ahirn@37877
   869
     Form'
ahirn@37877
   870
       (PpcKF
ahirn@37877
   871
          (0,EdUndef,0,Nundef,
ahirn@37877
   872
           (Problem [],
ahirn@37877
   873
            {Find=[Incompl "solutions []"],
ahirn@37877
   874
             Given=[Incompl "equality",Incompl "solveFor"],Relate=[],
ahirn@37877
   875
             Where=[False "matches (?a = ?b) e_"],With=[]}))) : mout
neuper@37896
   876
\end{verbatim}}
ahirn@37877
   877
{\footnotesize\begin{verbatim}
alexandra@37889
   878
?????????????????????????????????????????????????????????????????????????????????????????????
ahirn@37877
   879
   ML>  nxt;
ahirn@37877
   880
   val it = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
ahirn@37877
   881
     : string * mstep
ahirn@37877
   882
   ML>
ahirn@37877
   883
   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
   884
   val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equation"])
ahirn@37877
   885
     : string * mstep
ahirn@37877
   886
   ML>
ahirn@37877
   887
   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37896
   888
\end{verbatim}}
ahirn@37877
   889
alexandra@37889
   890
\section{The phase of modeling}
alexandra@37891
   891
Dieses Kapitel besch\"aftigt sich mit dem input der Einzelheiten bei einem Problem. Die me kann dabei helfen, wenn man die formalization durch {\tt Init\_Proof} darauf hinweist. Normalerweise weiss die mathematics engine die n\"achste gute tactic.
ahirn@37877
   892
{\footnotesize\begin{verbatim}
alexandra@37889
   893
?????????????????????????????????????????????????????????????????????????????????????????????
ahirn@37877
   894
   ML>  nxt;
ahirn@37877
   895
   val it =
ahirn@37877
   896
     ("Add_Given",Add_Given "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)")
ahirn@37877
   897
     : string * mstep
ahirn@37877
   898
   ML>
ahirn@37877
   899
   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
   900
   val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep
ahirn@37877
   901
   ML>
ahirn@37877
   902
   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
   903
   val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep
ahirn@37877
   904
   ML>
ahirn@37877
   905
   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 
ahirn@37877
   906
   val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
neuper@37896
   907
\end{verbatim}}
ahirn@37877
   908
{\footnotesize\begin{verbatim}
alexandra@37889
   909
?????????????????????????????????????????????????????????????????????????????????????????????
ahirn@37877
   910
   ML>  Compiler.Control.Print.printDepth:=8;
ahirn@37877
   911
   ML>  f;
ahirn@37877
   912
   val it =
ahirn@37877
   913
     Form'
ahirn@37877
   914
       (PpcKF
ahirn@37877
   915
          (0,EdUndef,0,Nundef,
ahirn@37877
   916
           (Problem [],
ahirn@37877
   917
            {Find=[Correct "solutions L"],
ahirn@37877
   918
             Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877
   919
                    Correct "solveFor x"],Relate=[],Where=[],With=[]}))) : mout
neuper@37896
   920
\end{verbatim}}
ahirn@37877
   921
alexandra@37889
   922
alexandra@37889
   923
\section{The phase of specification}
alexandra@37891
   924
Diese phase liefert eindeutige Bestimmungen einer domain, den problem type und die method damit man sie verwenden kann. F\"ur gew\"ohnlich wird die Suche nach dem richtigen problem type unterst\"utzt. Dazu sind zwei tactics verwendbar: {\tt Specify\_Problem} entwickelt ein Feedback, wie ein problem type bei dem jetzigen problem zusammenpasst und {\tt Refine\_Problem} stellt Hilfe durch das System bereit, falls der Benutzer die \"Ubersicht verliert.
ahirn@37877
   925
{\footnotesize\begin{verbatim}
alexandra@37889
   926
??????????????????????????????????????????????????????????????????????????????????????????
alexandra@37889
   927
   ML> nxt;
ahirn@37877
   928
   val it = ("Specify_Domain",Specify_Domain "SqRoot.thy") : string * mstep
ahirn@37877
   929
   ML>
ahirn@37877
   930
   ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
   931
   val nxt =
ahirn@37877
   932
     ("Specify_Problem",Specify_Problem ["normalize","univariate","equation"])
ahirn@37877
   933
     : string * mstep
ahirn@37877
   934
   val pt =
ahirn@37877
   935
     Nd
ahirn@37877
   936
       (PblObj
ahirn@37877
   937
          {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
wneuper@59279
   938
              result=#,spec=#},[]) : ctree
neuper@37896
   939
\end{verbatim}}
alexandra@37891
   940
Die me erkennt den richtigen Problem type und arbeitet so weiter:
ahirn@37877
   941
{\footnotesize\begin{verbatim}
alexandra@37889
   942
?????????????????????????????????????????????????????????????????????????????????????????
ahirn@37877
   943
   ML> val nxt = ("Specify_Problem",
ahirn@37877
   944
               Specify_Problem ["polynomial","univariate","equation"]);
ahirn@37877
   945
   ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
   946
   val f = Form' (PpcKF (0,EdUndef,0,Nundef,(#,#))) : mout
ahirn@37877
   947
   val nxt =
ahirn@37877
   948
     ("Refine_Problem",Refine_Problem ["normalize","univariate","equation"])
ahirn@37877
   949
     : string * mstep
ahirn@37877
   950
   ML>
ahirn@37877
   951
   ML> val nxt = ("Specify_Problem",
ahirn@37877
   952
               Specify_Problem ["linear","univariate","equation"]);
ahirn@37877
   953
   ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
   954
   val f =
ahirn@37877
   955
     Form'
ahirn@37877
   956
       (PpcKF
ahirn@37877
   957
          (0,EdUndef,0,Nundef,
ahirn@37877
   958
           (Problem ["linear","univariate","equation"],
ahirn@37877
   959
            {Find=[Correct "solutions L"],
ahirn@37877
   960
             Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877
   961
                    Correct "solveFor x"],Relate=[],
ahirn@37877
   962
             Where=[False
ahirn@37877
   963
                    "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
ahirn@37877
   964
             With=[]}))) : mout 
neuper@37896
   965
\end{verbatim}}
alexandra@37889
   966
Wir nehmen wieder an, dass der dialog guide die n\"achsten tactics, veranlasst von der mathematic engine, versteckt und der Sch\"uler Hilfe ben\"otigt. Dann muss {\tt Refine\_Problem} angewandt werden. Dieser Befehl findet immer den richtigen Weg, wenn man es auf den problem type bezieht [''univariate``, ''equation``].
ahirn@37877
   967
{\footnotesize\begin{verbatim}
alexandra@37889
   968
????????????????????????????????????????????????????????????????????????????????????????????
ahirn@37877
   969
   ML> val nxt = ("Refine_Problem",
ahirn@37877
   970
                  Refine_Problem ["linear","univariate","equation
ahirn@37877
   971
   ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
   972
   val f = Problems (RefinedKF [NoMatch #]) : mout
ahirn@37877
   973
   ML>
ahirn@37877
   974
   ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
ahirn@37877
   975
   val f =
ahirn@37877
   976
     Problems
ahirn@37877
   977
       (RefinedKF
ahirn@37877
   978
          [NoMatch
ahirn@37877
   979
             (["linear","univariate","equation"],
ahirn@37877
   980
              {Find=[Correct "solutions L"],
ahirn@37877
   981
               Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877
   982
                      Correct "solveFor x"],Relate=[],
ahirn@37877
   983
               Where=[False
ahirn@37877
   984
                     "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
ahirn@37877
   985
               With=[]})]) : mout
ahirn@37877
   986
   ML>
ahirn@37877
   987
   ML> val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation"]);
ahirn@37877
   988
   ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
   989
   val f =
ahirn@37877
   990
     Problems
ahirn@37877
   991
       (RefinedKF [Matches #,NoMatch #,NoMatch #,NoMatch #,NoMatch #,Matches #])
ahirn@37877
   992
     : mout
ahirn@37877
   993
   ML>
ahirn@37877
   994
   ML>
ahirn@37877
   995
   ML>  Compiler.Control.Print.printDepth:=9;f;Compiler.Control.Print.printDepth:=4;
ahirn@37877
   996
   val f =
ahirn@37877
   997
     Problems
ahirn@37877
   998
       (RefinedKF
ahirn@37877
   999
          [Matches
ahirn@37877
  1000
             (["univariate","equation"],
ahirn@37877
  1001
              {Find=[Correct "solutions L"],
ahirn@37877
  1002
               Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877
  1003
                      Correct "solveFor x"],Relate=[],
ahirn@37877
  1004
               Where=[Correct
ahirn@37877
  1005
               With=[]}),
ahirn@37877
  1006
           NoMatch
ahirn@37877
  1007
             (["linear","univariate","equation"],
ahirn@37877
  1008
              {Find=[Correct "solutions L"],
ahirn@37877
  1009
               Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877
  1010
                      Correct "solveFor x"],Relate=[],
ahirn@37877
  1011
               Where=[False
ahirn@37877
  1012
                      "matches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"],
ahirn@37877
  1013
                  With=[]}),
ahirn@37877
  1014
           NoMatch
ahirn@37877
  1015
             ...
ahirn@37877
  1016
             ...   
ahirn@37877
  1017
           Matches
ahirn@37877
  1018
             (["normalize","univariate","equation"],
ahirn@37877
  1019
              {Find=[Correct "solutions L"],
ahirn@37877
  1020
               Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
ahirn@37877
  1021
                      Correct "solveFor x"],Relate=[],Where=[],With=[]})]) : mout
neuper@37896
  1022
\end{verbatim}}
alexandra@37889
  1023
Die tactic {\tt Refine\_Problem} wandelt alle matches wieder in problem types um und sucht in der problem hierachy weiter.
ahirn@37877
  1024
alexandra@37889
  1025
alexandra@37889
  1026
\section{The phase of solving}
alexandra@37891
  1027
Diese phase beginnt mit dem Aufruf einer method, die eine normale form innerhalb einer tactic ausf\"uhrt: {\tt Rewrite rnorm\_equation\_add} und {\tt Rewrite\_Set SqRoot\_simplify}:
ahirn@37877
  1028
{\footnotesize\begin{verbatim} 
ahirn@37877
  1029
   ML> nxt;
ahirn@37877
  1030
   val it = ("Apply_Method",Apply_Method ("SqRoot.thy","norm_univar_equation"))
ahirn@37877
  1031
     : string * mstep
ahirn@37877
  1032
   ML>
ahirn@37877
  1033
   ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
  1034
   val f =
ahirn@37877
  1035
     Form' (FormKF (~1,EdUndef,1,Nundef,"(x + #1) * (x + #2) = x ^^^ #2 + #8"))
ahirn@37877
  1036
   val nxt =
ahirn@37877
  1037
     ("Rewrite", Rewrite
ahirn@37877
  1038
        ("rnorm_equation_add","~ ?b =!= #0 ==> (?a = ?b) = (?a + #-1 * ?b = #0)"))
ahirn@37877
  1039
   ML>
ahirn@37877
  1040
   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
  1041
   val f =
ahirn@37877
  1042
     Form' (FormKF (~1,EdUndef,1,Nundef,
ahirn@37877
  1043
           "(x + #1) * (x + #2) + #-1 * (x ^^^ #2 + #8) = #0")) : mout
ahirn@37877
  1044
   val nxt = ("Rewrite_Set",Rewrite_Set "SqRoot_simplify") : string * mstep
ahirn@37877
  1045
   ML>
ahirn@37877
  1046
   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
  1047
   val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#-6 + #3 * x = #0")) : mout
ahirn@37877
  1048
   val nxt = ("Subproblem",Subproblem ("SqRoot.thy",[#,#])) : string * mstep
neuper@37896
  1049
\end{verbatim}}
alexandra@37891
  1050
Die Formel $-6 + 3\cdot x = 0$ ist die Eingabe eine subproblems, das wiederum gebraucht wird, um die Gleichungsart zu erkennen und die entsprechende method auszuf\"uhren:
ahirn@37877
  1051
{\footnotesize\begin{verbatim}
ahirn@37877
  1052
   ML> nxt;
ahirn@37877
  1053
   val it = ("Subproblem",Subproblem ("SqRoot.thy",["univariate","equation"]))
ahirn@37877
  1054
   ML>   
ahirn@37877
  1055
   ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
  1056
   val f =
ahirn@37877
  1057
     Form' (FormKF
ahirn@37877
  1058
          (~1,EdUndef,1,Nundef,"Subproblem (SqRoot.thy, [univariate, equation])"))
ahirn@37877
  1059
     : mout
ahirn@37877
  1060
   val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])
ahirn@37877
  1061
   ML>
ahirn@37877
  1062
   ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
  1063
   val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"])
neuper@37896
  1064
\end{verbatim}}
alexandra@37889
  1065
{\tt Refine [''univariate``, ''equation``]} sucht die passende Gleichungsart aus der problem hierachy heraus, welche man mit {\tt Model\_Problem [''linear``, ''univariate``, ''equation``]} \"uber das System ansehen kann.
alexandra@37889
  1066
Nun folgt erneut die phase of modeling und die phase of specification.
ahirn@37877
  1067
alexandra@37889
  1068
\section{The final phase: \"Uberpr\"ufung der ''post-condition``}
alexandra@37891
  1069
Die gezeigten problems, die durch \isac{} gel\"ost wurden, sind so genannte 'example construction problems'. Das massivste Merkmal solcher problems ist die post-condition. Im Umgang mit dieser gibt es noch offene Fragen.
alexandra@37889
  1070
Dadurch wird die post-condition im folgenden Beispiel als problem und subproblem erw\"ahnt.
ahirn@37877
  1071
{\footnotesize\begin{verbatim}
ahirn@37877
  1072
   ML> nxt;
ahirn@37877
  1073
   val it = ("Check_Postcond",Check_Postcond ["linear","univariate","equation"])
ahirn@37877
  1074
   ML>
ahirn@37877
  1075
   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
  1076
   val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = #2]")) : mout
ahirn@37877
  1077
   val nxt =
ahirn@37877
  1078
     ("Check_Postcond",Check_Postcond ["normalize","univariate","equation"])
ahirn@37877
  1079
   ML>
ahirn@37877
  1080
   ML>  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
ahirn@37877
  1081
   val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #2]")) : mout
ahirn@37877
  1082
   val nxt = ("End_Proof'",End_Proof') : string * mstep
neuper@37896
  1083
\end{verbatim}}
alexandra@37889
  1084
Die tactic {\tt End\_Proof'} bedeutet, dass der proof erflogreich beendet wurde.\\
ahirn@37877
  1085
alexandra@37891
  1086
\paragraph{Versuchen Sie es!} Die tactics, die vom System vorgeschlagen werden, m\"ussen vom Benutzer nicht angewendet werden. Er kann selbstverst\"andlich auch andere tactics verwenden und das System wird melden, ob dieser Befehl zutreffend ist oder nicht.
ahirn@37877
  1087
ahirn@37877
  1088
alexandra@37891
  1089
\part{Handbuch f\"ur Autoren}
ahirn@37877
  1090
alexandra@37889
  1091
\chapter{Die Struktur des Grundlagenwissens}
ahirn@37877
  1092
alexandra@37891
  1093
\section{''tactics`` und Daten}
alexandra@37891
  1094
Zuerst betrachten wir die me von aussen. Wir sehen uns tactics und an und verbinden sie mit unserem Grundwissen (KB). Im Bezug auf das KB befassen wir uns mit den kleinsten Teilchen, die von den Autoren des KB sehr genau durchgef\"uhrt werden m\"ussen.
alexandra@37889
  1095
Diese Teile sind in alphabetischer Anordnung in Tab.\ref{kb-items} auf Seite \pageref{kb-items} aufgelistet.
ahirn@37877
  1096
ahirn@37877
  1097
{\begin{table}[h]
alexandra@37889
  1098
\caption{Kleinste Teilchen des KB} \label{kb-items}
ahirn@37877
  1099
%\tabcolsep=0.3mm
ahirn@37877
  1100
\begin{center}
ahirn@37877
  1101
\def\arraystretch{1.0}
ahirn@37877
  1102
\begin{tabular}{lp{9.0cm}}
alexandra@37889
  1103
Abk\"urzung & Beschreibung \\
ahirn@37877
  1104
\hline
ahirn@37877
  1105
&\\
ahirn@37877
  1106
{\it calc\_list}
alexandra@37891
  1107
& gesammelte Liste von allen ausgewerteten Funktionen\\
ahirn@37877
  1108
{\it eval\_fn}
alexandra@37891
  1109
& ausgewertete Funktionen f\"ur Zahlen und f\"ur Eigenschaften, die in SML kodiert sind\\
alexandra@37889
  1110
{\it eval\_rls }
alexandra@37891
  1111
& rule set {\it rls} f\"ur einfache Ausdr\"ucke mit {\it eval\_fn}s\\
ahirn@37877
  1112
{\it fmz}
alexandra@37889
  1113
& Formalisierung, d.h. eine sehr geringe Darstellung von einem Beispiel \\
ahirn@37877
  1114
{\it met}
Walther@60586
  1115
& eine method d.h. eine Datenstruktur, die alle Informationen zum L\"osen einer phase enth\"alt ({\it rew\_ord}, {\it program}, etc.)\\
ahirn@37877
  1116
{\it metID}
alexandra@37889
  1117
& bezieht sich auf {\it met}\\
ahirn@37877
  1118
{\it op}
alexandra@37889
  1119
& ein Operator, der der Schl\"ussel zu {\it eval\_fn} in einer {\it calc\_list} ist \\
ahirn@37877
  1120
{\it pbl}
alexandra@37891
  1121
& Problem d.h. der Knotenpunkt in der problem hierachy\\
ahirn@37877
  1122
{\it pblID}
alexandra@37889
  1123
& bezieht sich auf {\it pbl}\\
ahirn@37877
  1124
{\it rew\_ord}
alexandra@37889
  1125
& Anordnung beim Rewriting\\
ahirn@37877
  1126
{\it rls}
alexandra@37891
  1127
& rule set, d.h. eine Datenstruktur, die theorems {\it thm} und Operatoren {\it op} zur Vereinfachung (mit {\it rew\_ord}) enth\"alt \\
ahirn@37877
  1128
{\it Rrls}
alexandra@37891
  1129
& rule set f\"ur das 'reverse rewriting' (eine \isac-Technik, die schrittweise Rewriting entwickelt, z.B. f\"ur die zur\"uckgenommenen Teile)\\
Walther@60586
  1130
{\it program}
alexandra@37891
  1131
& script, das die Algorithmen durch Anwenden von tactics beschreibt und ein Teil von {\it met} ist \\
ahirn@37877
  1132
{\it norm\_rls}
alexandra@37889
  1133
& spezielles Regelwerk zum Berechnen von Normalformen, im Zusammenhang mit {\it thy}\\
ahirn@37877
  1134
{\it spec}
alexandra@37889
  1135
& Spezifikation, z.B, ein Tripel ({\it thyID, pblID, metID})\\
ahirn@37877
  1136
{\it subs}
alexandra@37889
  1137
& Ersatz, z.B. eine Liste von Variablen und ihren jeweiligen Werten\\
alexandra@37892
  1138
{\it Term}
alexandra@37889
  1139
& Term von Isabelle, z.B. eine Formel\\
ahirn@37877
  1140
{\it thm}
alexandra@37889
  1141
& theorem\\
ahirn@37877
  1142
{\it thy}
alexandra@37891
  1143
& theory\\
ahirn@37877
  1144
{\it thyID}
alexandra@37889
  1145
& im Bezug auf {\it thy} \\
alexandra@37889
  1146
\end{tabular}\end{center}\end{table}}
alexandra@37889
  1147
alexandra@37891
  1148
Die Verbindung zwischen tactics und Daten werden in Tab.\ref{tac-kb} auf Seite \pageref{tac-kb} dargestellt.
alexandra@37889
  1149
alexandra@37889
  1150
ahirn@37877
  1151
\begin{table}[h]
alexandra@37891
  1152
\caption{Welche tactics verwenden die Teile des KB~?} \label{tac-kb}
ahirn@37877
  1153
\tabcolsep=0.3mm
ahirn@37877
  1154
\begin{center}
ahirn@37877
  1155
\begin{tabular}{|ll||cccc|ccc|cccc|} \hline
alexandra@37891
  1156
tactic &Eingabe & & & &norm\_& &rew\_&rls &eval\_&eval\_&calc\_& \\
Walther@60586
  1157
& &thy &program &Rrls&rls &thm &ord &Rrls&fn &rls &list &dsc\\
ahirn@37877
  1158
\hline\hline
ahirn@37877
  1159
Init\_Proof
alexandra@37889
  1160
&fmz & x & & & x & & & & & & & x \\
alexandra@37889
  1161
&spec & & & & & & & & & & & \\
ahirn@37877
  1162
\hline
ahirn@37877
  1163
\multicolumn{13}{|l|}{model phase}\\
ahirn@37877
  1164
\hline
alexandra@37889
  1165
Add\_*
alexandra@37892
  1166
&Term & x & & & x & & & & & & & x \\
alexandra@37889
  1167
FormFK &model & x & & & x & & & & & & & x \\
ahirn@37877
  1168
\hline
ahirn@37877
  1169
\multicolumn{13}{|l|}{specify phase}\\
ahirn@37877
  1170
\hline
alexandra@37889
  1171
Specify\_Theory
alexandra@37889
  1172
&thyID & x & & & x & & & & x & x & & x \\
alexandra@37889
  1173
Specify\_Problem
alexandra@37889
  1174
&pblID & x & & & x & & & & x & x & & x \\
alexandra@37889
  1175
Refine\_Problem
alexandra@37889
  1176
&pblID & x & & & x & & & & x & x & & x \\
alexandra@37889
  1177
Specify\_Method
alexandra@37889
  1178
&metID & x & & & x & & & & x & x & & x \\
alexandra@37889
  1179
Apply\_Method
alexandra@37889
  1180
&metID & x & x & & x & & & & x & x & & x \\
ahirn@37877
  1181
\hline
ahirn@37877
  1182
\multicolumn{13}{|l|}{solve phase}\\
ahirn@37877
  1183
\hline
alexandra@37889
  1184
Rewrite,\_Inst
alexandra@37889
  1185
&thm & x & x & & & x &met & & x &met & & \\
ahirn@37877
  1186
Rewrite, Detail
alexandra@37889
  1187
&thm & x & x & & & x &rls & & x &rls & & \\
ahirn@37877
  1188
Rewrite, Detail
alexandra@37889
  1189
&thm & x & x & & & x &Rrls & & x &Rrls & & \\
ahirn@37877
  1190
Rewrite\_Set,\_Inst
alexandra@37889
  1191
&rls & x & x & & & & & x & x & x & & \\
alexandra@37889
  1192
Calculate
alexandra@37889
  1193
&op & x & x & & & & & & & & x & \\
alexandra@37889
  1194
Substitute
alexandra@37889
  1195
&subs & x & & & x & & & & & & & \\
alexandra@37889
  1196
& & & & & & & & & & & & \\
alexandra@37889
  1197
SubProblem
alexandra@37889
  1198
&spec & x & x & & x & & & & x & x & & x \\
alexandra@37889
  1199
&fmz & & & & & & & & & & & \\
ahirn@37877
  1200
\hline
neuper@37896
  1201
\end{tabular}\end{center}\end{table}
ahirn@37877
  1202
ahirn@37877
  1203
alexandra@37889
  1204
\section{Die theories von \isac{}}
alexandra@37891
  1205
Die theories von \isac{} basieren auf den theories f\"ur HOL und Real von Isabelle. Diese theories haben eine spezielle Form, die durch die Endung {\tt *.thy} gekennzeichnet sind; normalerweise werden diese theories zusammen mit SML verwendet. Dann haben sie den selben Dateinamen, aber die Endung {\tt *.ML}.
alexandra@37891
  1206
Die theories von \isac{} representieren den Teil vom Basiswissen von \isac{}, die hierachy von den zwei theories ist nach diesen strukturiert. Die {\tt *.ML} Dateien beinhalten {\em alle} Daten von den anderen zwei Hauptlinien des Basiswissens, die problems und methods (ohne ihre jeweilige Struktur, die von den problem Browsern und den method Browsern gemacht wird, zu pr\"asentieren.
alexandra@37891
  1207
Die Tab.\ref{theories} auf Seite \pageref{theories} listet die base theories auf, die geplant sind in der Version \isac{} 1 angewendet zu werden. Wir erwarten, dass die Liste erweitert wird in n\"aherer Zukunft, und wir werden uns auch den theorie Browser genauer ansehen.
alexandra@37891
  1208
Die ersten drei theories auf der Liste geh\"oren {\em nicht} zum Grundwissen von \isac{}; sie besch\"aftigen sich mit der Skriptsprache f\"ur methods und ist hier nur zur Vollst\"andigkeit angef\"uhrt.
ahirn@37877
  1209
ahirn@37877
  1210
{\begin{table}[h]
alexandra@37891
  1211
\caption{theory von der ersten Version von \isac} \label{theories}
ahirn@37877
  1212
%\tabcolsep=0.3mm
ahirn@37877
  1213
\begin{center}
ahirn@37877
  1214
\def\arraystretch{1.0}
ahirn@37877
  1215
\begin{tabular}{lp{9.0cm}}
alexandra@37891
  1216
theory & Beschreibung \\
ahirn@37877
  1217
\hline
ahirn@37877
  1218
&\\
ahirn@37877
  1219
ListI.thy
alexandra@37891
  1220
& ordnet die Bezeichnungen den Funktionen, die in {\tt Isabelle2002/src/HOL/List.thy} sind, zu und (intermediatly~?) definiert einige weitere Listen von Funktionen\\
ahirn@37877
  1221
ListI.ML
alexandra@37889
  1222
& {\tt eval\_fn} f\"ur die zus\"atzliche Listen von Funktionen\\
ahirn@37877
  1223
Tools.thy
alexandra@37889
  1224
& Funktion, die f\"ur die Auswertung von Skripten ben\"otigt wird\\
ahirn@37877
  1225
Tools.ML
alexandra@37889
  1226
& bezieht sich auf {\tt eval\_fn}s\\
ahirn@37877
  1227
Script.thy
alexandra@37891
  1228
& Vorraussetzung f\"ur script: types, tactics, tacticals\\
ahirn@37877
  1229
Script.ML
alexandra@37891
  1230
& eine Reihe von tactics und Funktionen f\"ur den internen Gebrauch\\
ahirn@37877
  1231
& \\
ahirn@37877
  1232
\hline
ahirn@37877
  1233
& \\
ahirn@37877
  1234
Typefix.thy
alexandra@37889
  1235
& fortgeschrittener Austritt, um den type Fehlern zu entkommen\\
ahirn@37877
  1236
Descript.thy
alexandra@37889
  1237
& {\it Beschreibungen} f\"ur die Formeln von {\it Modellen} und {\it Problemen}\\
ahirn@37877
  1238
Atools
alexandra@37891
  1239
& Neudefinierung von Operatoren; allgemeine Eigenschaften und Funktionen f\"ur Vorraussetzungen; theorems f\"ur {\tt eval\_rls}\\
ahirn@37877
  1240
Float
alexandra@37889
  1241
& Gleitkommerzahlendarstellung\\
ahirn@37877
  1242
Equation
alexandra@37889
  1243
& grunds\"atzliche Vorstellung f\"ur  Gleichungen und Gleichungssysteme\\
ahirn@37877
  1244
Poly
alexandra@37889
  1245
& Polynome\\
ahirn@37877
  1246
PolyEq
alexandra@37889
  1247
& polynomiale Gleichungen und Gleichungssysteme \\
ahirn@37877
  1248
Rational.thy
alexandra@37891
  1249
& zus\"atzliche theorems f\"ur Rationale Zahlen\\
ahirn@37877
  1250
Rational.ML
alexandra@37889
  1251
& abbrechen, hinzuf\"ugen und vereinfachen von Rationalen Zahlen durch Verwenden von (einer allgemeineren Form von) Euclids Algorithmus; die entsprechenden umgekehrten Regels\"atze\\
ahirn@37877
  1252
RatEq
alexandra@37889
  1253
& Gleichung mit rationalen Zahlen\\
ahirn@37877
  1254
Root
alexandra@37889
  1255
& Radikanten; berechnen der Normalform; das betreffende umgekehrte Regelwerk\\
ahirn@37877
  1256
RootEq
alexandra@37889
  1257
& Gleichungen mit Wurzeln\\
ahirn@37877
  1258
RatRootEq
alexandra@37889
  1259
& Gleichungen mit rationalen Zahlen und Wurzeln (z.B. mit Termen, die beide Vorg\"ange enthalten)\\
ahirn@37877
  1260
Vect
alexandra@37889
  1261
& Vektoren Analysis\\
ahirn@37877
  1262
Trig
alexandra@37889
  1263
& Trigonometrie\\
ahirn@37877
  1264
LogExp
alexandra@37889
  1265
& Logarithmus und Exponentialfunktionen\\
ahirn@37877
  1266
Calculus
alexandra@37889
  1267
& nicht der Norm entsprechende Analysis\\
ahirn@37877
  1268
Diff
alexandra@37889
  1269
& Differenzierung\\
ahirn@37877
  1270
DiffApp
alexandra@37889
  1271
& Anwendungen beim Differenzieren (Maximum-Minimum-Probleme)\\
ahirn@37877
  1272
Test
alexandra@37889
  1273
& (alte) Daten f\"ur Testfolgen\\
ahirn@37877
  1274
Isac
alexandra@37889
  1275
& enth\"alt alle Theorien von\isac{}\\
alexandra@37889
  1276
\end{tabular}\end{center}\end{table}}
ahirn@37877
  1277
ahirn@37877
  1278
alexandra@37889
  1279
\section{Daten in {\tt *.thy} und {\tt *.ML}}
alexandra@37891
  1280
Wie schon zuvor angesprochen, haben die Arbeiten die theories von *.thy und *.ML zusammen und haben deswegen den selben Dateiname. Wie diese Daten zwischen den zwei Dateien verteilt werden wird in der
alexandra@37891
  1281
Tab.\ref{thy-ML} auf Seite \pageref{thy-ML} gezeigt. Die Ordnung von den Datenteilchen in den theories sollte an der Ordnung von der Liste festhalten.
alexandra@37889
  1282
ahirn@37877
  1283
{\begin{table}[h]
alexandra@37889
  1284
\caption{Daten in {\tt *.thy}- und {\tt *.ML}-files} \label{thy-ML}
ahirn@37877
  1285
\tabcolsep=2.0mm
ahirn@37877
  1286
\begin{center}
ahirn@37877
  1287
\def\arraystretch{1.0}
ahirn@37877
  1288
\begin{tabular}{llp{7.7cm}}
alexandra@37889
  1289
Datei & Daten & Beschreibung \\
ahirn@37877
  1290
\hline
ahirn@37877
  1291
& &\\
ahirn@37877
  1292
{\tt *.thy}
alexandra@37889
  1293
& consts
alexandra@37889
  1294
& Operatoren, Eigenschaften, Funktionen und Skriptnamen ('{\tt Skript} Name \dots{\tt Argumente}')
ahirn@37877
  1295
\\
alexandra@37889
  1296
& rules
alexandra@37891
  1297
& theorems: \isac{} verwendet theorems von Isabelle, wenn m\"oglich; zus\"atzliche theorems, die jenen von Isabelle entsprechen, bekommen ein {\it I} angeh\"angt
ahirn@37877
  1298
\\& &\\
ahirn@37877
  1299
{\tt *.ML}
alexandra@37889
  1300
& {\tt theory' :=}
alexandra@37891
  1301
& Die theory, die 
alexandra@37889
  1302
abgegrenzt ist von der {\tt *.thy}-Datei, wird durch \isac{} zug\"anglich gemacht
ahirn@37877
  1303
\\
ahirn@37877
  1304
& {\tt eval\_fn}
alexandra@37891
  1305
& die Auswertungsfunktion f\"ur die Operatoren und Eigenschaften, kodiert im meta-Level (SML); die Bezeichnugn von so einer Funktion ist eine Kombination von Schl\"usselw\"ortern {\tt eval\_} und einer Bezeichnung von der Funktion, die in in {\tt *.thy} erkl\"art ist
alexandra@37891
  1306
\\
alexandra@37889
  1307
& {\tt *\_simplify}
alexandra@37889
  1308
& der automatisierte Vereinfacher f\"ur die tats\"achliche Theorie, z.B. die Bezeichnung von diesem Regelwerk ist eine Kombination aus den Theorienbezeichnungen und dem Schl\"usselwort {\tt *\_simplify}
ahirn@37877
  1309
\\
ahirn@37877
  1310
& {\tt norm\_rls :=}
alexandra@37891
  1311
& der automatisierte Vereinfacher {\tt *\_simplify} wird so aufgehoben, dass er \"uber \isac{}  zug\"anglich ist
ahirn@37877
  1312
\\
ahirn@37877
  1313
& {\tt rew\_ord' :=}
alexandra@37889
  1314
& das Gleiche f\"ur die Anordnung des Rewriting, wenn es ausserhalb eines speziellen Regelwerks gebraucht wird
ahirn@37877
  1315
\\
ahirn@37877
  1316
& {\tt ruleset' :=}
alexandra@37889
  1317
& dasselbe wie f\"ur Regels\"atze (gew\"ohnliche Regels\"atze, umgekehrte Regels\"atze, und {\tt eval\_rls})
ahirn@37877
  1318
\\
ahirn@37877
  1319
& {\tt calc\_list :=}
alexandra@37891
  1320
& dasselbe f\"ur {\tt eval\_fn}s, wenn es ausserhalb eines bestimmten Regelwerks gebraucht wird (wenn es ausserhalb eines bestimmten Regelwerks ben\"otigt wird) (z.B. f\"ur eine tactic {\tt Calculate} in einem Skript)
ahirn@37877
  1321
\\
ahirn@37877
  1322
& {\tt store\_pbl}
alexandra@37891
  1323
& Problems, die in {\tt *.ML}-Dateien definiert sind, werden zug\"anglich f\"ur \isac{}
ahirn@37877
  1324
\\
ahirn@37877
  1325
& {\tt methods :=}
alexandra@37891
  1326
& methods, die in {\tt *.ML}-Dateien definiert sind werden zug\"anglich f\"ur \isac{}
ahirn@37877
  1327
\\
alexandra@37889
  1328
\end{tabular}\end{center}\end{table}}
ahirn@37877
  1329
alexandra@37889
  1330
\section{Formale Beschreibung der Hierarchie von Problemen}
ahirn@37877
  1331
alexandra@37889
  1332
\section{Skripttaktiken}
alexandra@37891
  1333
Tats\"achlich sind es die tactics, die die Berechnungen vorantreiben: im Hintergrund bauen sie den proof tree und sie \"ubernehmen die wichtigsten Aufgaben w\"ahrend der Auswertung bei der der ''script-interpreter`` zur Steuerung des Benutzers transferiert wird. Hier beschreiben wir nur den Syntax von tactics; die Semantik ist beschrieben etwas weiter unten im Kontext mit tactics, die die Benutzer/Innen dieses Programmes verwenden: Es gibt einen Schriftverkehr zwischen den user-tactics und den script tactics.
ahirn@37877
  1334
ahirn@37877
  1335
ahirn@37877
  1336
ahirn@37877
  1337
\part{Authoring on the knowledge}
ahirn@37877
  1338
ahirn@37877
  1339
ahirn@37877
  1340
\section{Add a theorem}
ahirn@37877
  1341
\section{Define and add a problem}
ahirn@37877
  1342
\section{Define and add a predicate}
ahirn@37877
  1343
\section{Define and add a method}
ahirn@37877
  1344
\section{}
ahirn@37877
  1345
\section{}
ahirn@37877
  1346
\section{}
ahirn@37877
  1347
\section{}
ahirn@37877
  1348
ahirn@37877
  1349
ahirn@37877
  1350
ahirn@37877
  1351
\newpage
ahirn@37877
  1352
\bibliography{bib/isac,bib/from-theses}
ahirn@37877
  1353
ahirn@37877
  1354
\end{document}