1.1 --- a/doc-src/isac/dmeindl/proposal.tex Tue Sep 13 10:51:56 2011 +0200
1.2 +++ b/doc-src/isac/dmeindl/proposal.tex Sun Sep 18 15:21:46 2011 +0200
1.3 @@ -1,177 +1,241 @@
1.4 +%WN mit diesen 3 Zeichen beginnen meine Kommentare
1.5 +
1.6 \documentclass[12pt,a4paper]{article}
1.7 -\usepackage{a4}
1.8 -\usepackage[naustrian]{babel}
1.9 -\usepackage[latin1]{inputenc}
1.10 -\usepackage{calc}
1.11 -\usepackage{amsmath}
1.12 -\usepackage{epsfig}
1.13 -\usepackage{graphicx}
1.14 -\usepackage{xcolor}
1.15 -\usepackage{amsfonts}
1.16 -
1.17 -% Seitenräder einstellen und Höhe der Seitenzahlen
1.18 -\usepackage{geometry}
1.19 -\geometry{a4paper, left=2.5cm, right=2cm, top=3cm, bottom=2.8cm}
1.20 -\setlength{\footskip}{2cm}
1.21 -
1.22 -
1.23 -%Zähler definieren und Starwert setzen:
1.24 -\newcommand{\R}{\mathbb R}
1.25 -%\newcommand{\N}{\mathbb N}
1.26 -%\newcommand{\Q}{\mathbb Q}
1.27 -%\newcommand{\C}{\mathbb C}
1.28 -
1.29 -
1.30 -\newcounter{ctr}
1.31 -\setcounter{ctr}{0}
1.32 -
1.33 -\newcounter{Teubner}
1.34 -\newcounter{Klingenberg}
1.35 -\newcounter{T}
1.36 -\newcounter{Vo}
1.37 -\newcounter{Se}
1.38 -\newcounter{E}
1.39 -\newcounter{Bwl}
1.40 -\newcounter{Int}
1.41 -\newcounter{Prim}
1.42 -\newcounter{Z}
1.43 -\setcounter{Z}{0}
1.44 -\setcounter{Teubner}{1}
1.45 -\setcounter{Klingenberg}{2}
1.46 -\setcounter{T}{1}
1.47 -\setcounter{Vo}{7}
1.48 -\setcounter{Se}{2}
1.49 -\setcounter{E}{3}
1.50 -\setcounter{Bwl}{4}
1.51 -\setcounter{Int}{5}
1.52 -\setcounter{Prim}{6}
1.53 -%BSP
1.54 -\newenvironment{myBsp}{
1.55 - \begin{list}{\textbf{\textsc{Bsp:}}}{
1.56 - \setlength{\labelwidth}{8Pc}
1.57 - \setlength{\labelsep}{0.5Pc}
1.58 - \setlength{\rightmargin}{0Pc}
1.59 - \setlength{\leftmargin}{2Pc}
1.60 - \setlength{\parsep}{0ex plus 0.5ex}
1.61 - \setlength{\listparindent}{1em}
1.62 - \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.63 - \setlength{\topsep}{0.5Pc}
1.64 - }}
1.65 - {\end{list}
1.66 -}
1.67 -
1.68 -
1.69 -%Lemma
1.70 -\newenvironment{myLemma}{
1.71 - \begin{list}{\textsc{\textbf{Lemma:\ \ \ }}}{
1.72 - \setlength{\labelsep}{-0.5Pc}
1.73 - \setlength{\leftmargin}{1Pc}
1.74 - \setlength{\parsep}{0ex plus 0.5ex}
1.75 - \setlength{\listparindent}{1em}
1.76 - \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.77 - \setlength{\topsep}{0.5Pc}
1.78 - }}
1.79 - {\end{list}
1.80 -}
1.81 -%Korollar
1.82 -\newenvironment{myKorollar}{
1.83 - \begin{list}{\textsc{\textbf{Korollar: }}}{
1.84 - \setlength{\labelwidth}{8Pc}
1.85 - \setlength{\labelsep}{0.5Pc}
1.86 - \setlength{\rightmargin}{0Pc}
1.87 - \setlength{\leftmargin}{4Pc}
1.88 - \setlength{\parsep}{0ex plus 0.5ex}
1.89 - \setlength{\listparindent}{1em}
1.90 - \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.91 - \setlength{\topsep}{0.5Pc}
1.92 - }}
1.93 - {\end{list}
1.94 -}
1.95 -
1.96 -%Theorem
1.97 -\newenvironment{myTheorem}{
1.98 - \begin{list}{\textsc{\textbf{Theorem: }}}{
1.99 - \setlength{\labelwidth}{8Pc}
1.100 - \setlength{\labelsep}{0.5Pc}
1.101 - \setlength{\rightmargin}{0Pc}
1.102 - \setlength{\leftmargin}{5Pc}
1.103 - \setlength{\parsep}{0ex plus 0.5ex}
1.104 - \setlength{\listparindent}{1em}
1.105 - \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.106 - \setlength{\topsep}{0.5Pc}
1.107 - }}
1.108 - {\end{list}
1.109 -}
1.110 -
1.111 -
1.112 -%Proportion
1.113 -\newenvironment{myProp}{
1.114 - \begin{list}{\textsc{\textbf{Proportion: }}}{
1.115 - \setlength{\labelwidth}{8Pc}
1.116 - \setlength{\labelsep}{0.5Pc}
1.117 - \setlength{\rightmargin}{0Pc}
1.118 - \setlength{\leftmargin}{4Pc}
1.119 - \setlength{\parsep}{0ex plus 0.5ex}
1.120 - \setlength{\listparindent}{1em}
1.121 - \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.122 - \setlength{\topsep}{0.5Pc}
1.123 - }}
1.124 - {\end{list}
1.125 -}
1.126 -
1.127 -%Farben
1.128 -
1.129 -\newcommand{\red}[1]{\textcolor[rgb]{0.7,0,0}{\bf #1}}
1.130 -\newcommand{\rd}[1]{\color{red}{#1}}
1.131 -\newcommand{\white}[1]{\textcolor[rgb]{1,0,0}{\bf #1}}
1.132 -\newcommand{\w}[1]{\color{white}{#1}}
1.133 -\newcommand{\g}[1]{\color{myColor}{#1}}
1.134 -
1.135 -\usepackage{color}
1.136 -\definecolor{myColor}{rgb}{0.9,0.9,0.9}% Wir definieren im RGB-Farbraum
1.137 -
1.138 -
1.139 -\newcommand{\myDef}[1]{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\w .}\\[-0.2cm]\textbf{Definition\ \Nummer:}\\#1}}
1.140 -\newcommand{\mySatz}[2]{\colorbox{myColor}{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\g .}\\[-0.2cm]\textbf{Satz\ \Nummer:}\ #1\\ #2}}}
1.141 -\newcommand{\myBeweis}[1]{\textit{\textbf{Beweis:}\\ #1}}
1.142 -\newcommand{\myAlg}[2]{\parbox{\columnwidth}{\addtocounter{ctr}{1}\textbf{Algorithmus\ \Nummer:}\ \ #1\\#2}}
1.143 -\newcommand{\myProg}[1]{\fbox{\parbox{\columnwidth}{#1}}}
1.144 -
1.145 -\newcommand{\add}[1]{\addtocounter{#1}{1}}
1.146 -\newcommand{\zahl}[1]{\setcounter{#1}{Z}}
1.147 -\newcommand{\Q}[2]{\parbox{\columnwidth}{$^{[\arabic{#1}/#2]}$ }}
1.148 -
1.149 -\newcommand{\Nummer}{\thesection.\arabic{ctr}}
1.150 -
1.151 +\bibliographystyle{alpha}
1.152 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.153 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.154 +%\usepackage{a4}
1.155 +%\usepackage[naustrian]{babel}
1.156 +%\usepackage[latin1]{inputenc}
1.157 +%\usepackage{calc}
1.158 +%\usepackage{amsmath}
1.159 +%\usepackage{epsfig}
1.160 +%\usepackage{graphicx}
1.161 +%\usepackage{xcolor}
1.162 +%\usepackage{amsfonts}
1.163 +%
1.164 +%WN BITTE DIESE DEFINITIONEN WEGLASSEN ...
1.165 +%% Seitenräder einstellen und Höhe der Seitenzahlen
1.166 +%\usepackage{geometry}
1.167 +%\geometry{a4paper, left=2.5cm, right=2cm, top=3cm, bottom=2.8cm}
1.168 +%\setlength{\footskip}{2cm}
1.169 +%
1.170 +%
1.171 +%%Zähler definieren und Starwert setzen:
1.172 +%\newcommand{\R}{\mathbb R}
1.173 +%%\newcommand{\N}{\mathbb N}
1.174 +%%\newcommand{\Q}{\mathbb Q}
1.175 +%%\newcommand{\C}{\mathbb C}
1.176 +%
1.177 +%
1.178 +%\newcounter{ctr}
1.179 +%\setcounter{ctr}{0}
1.180 +%
1.181 +%\newcounter{Teubner}
1.182 +%\newcounter{Klingenberg}
1.183 +%\newcounter{T}
1.184 +%\newcounter{Vo}
1.185 +%\newcounter{Se}
1.186 +%\newcounter{E}
1.187 +%\newcounter{Bwl}
1.188 +%\newcounter{Int}
1.189 +%\newcounter{Prim}
1.190 +%\newcounter{Z}
1.191 +%\setcounter{Z}{0}
1.192 +%\setcounter{Teubner}{1}
1.193 +%\setcounter{Klingenberg}{2}
1.194 +%\setcounter{T}{1}
1.195 +%\setcounter{Vo}{7}
1.196 +%\setcounter{Se}{2}
1.197 +%\setcounter{E}{3}
1.198 +%\setcounter{Bwl}{4}
1.199 +%\setcounter{Int}{5}
1.200 +%\setcounter{Prim}{6}
1.201 +%%BSP
1.202 +%\newenvironment{myBsp}{
1.203 +% \begin{list}{\textbf{\textsc{Bsp:}}}{
1.204 +% \setlength{\labelwidth}{8Pc}
1.205 +% \setlength{\labelsep}{0.5Pc}
1.206 +% \setlength{\rightmargin}{0Pc}
1.207 +% \setlength{\leftmargin}{2Pc}
1.208 +% \setlength{\parsep}{0ex plus 0.5ex}
1.209 +% \setlength{\listparindent}{1em}
1.210 +% \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.211 +% \setlength{\topsep}{0.5Pc}
1.212 +% }}
1.213 +% {\end{list}
1.214 +%}
1.215 +%
1.216 +%
1.217 +%%Lemma
1.218 +%\newenvironment{myLemma}{
1.219 +% \begin{list}{\textsc{\textbf{Lemma:\ \ \ }}}{
1.220 +% \setlength{\labelsep}{-0.5Pc}
1.221 +% \setlength{\leftmargin}{1Pc}
1.222 +% \setlength{\parsep}{0ex plus 0.5ex}
1.223 +% \setlength{\listparindent}{1em}
1.224 +% \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.225 +% \setlength{\topsep}{0.5Pc}
1.226 +% }}
1.227 +% {\end{list}
1.228 +%}
1.229 +%%Korollar
1.230 +%\newenvironment{myKorollar}{
1.231 +% \begin{list}{\textsc{\textbf{Korollar: }}}{
1.232 +% \setlength{\labelwidth}{8Pc}
1.233 +% \setlength{\labelsep}{0.5Pc}
1.234 +% \setlength{\rightmargin}{0Pc}
1.235 +% \setlength{\leftmargin}{4Pc}
1.236 +% \setlength{\parsep}{0ex plus 0.5ex}
1.237 +% \setlength{\listparindent}{1em}
1.238 +% \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.239 +% \setlength{\topsep}{0.5Pc}
1.240 +% }}
1.241 +% {\end{list}
1.242 +%}
1.243 +%
1.244 +%%Theorem
1.245 +%\newenvironment{myTheorem}{
1.246 +% \begin{list}{\textsc{\textbf{Theorem: }}}{
1.247 +% \setlength{\labelwidth}{8Pc}
1.248 +% \setlength{\labelsep}{0.5Pc}
1.249 +% \setlength{\rightmargin}{0Pc}
1.250 +% \setlength{\leftmargin}{5Pc}
1.251 +% \setlength{\parsep}{0ex plus 0.5ex}
1.252 +% \setlength{\listparindent}{1em}
1.253 +% \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.254 +% \setlength{\topsep}{0.5Pc}
1.255 +% }}
1.256 +% {\end{list}
1.257 +%}
1.258 +%
1.259 +%
1.260 +%%Proportion
1.261 +%\newenvironment{myProp}{
1.262 +% \begin{list}{\textsc{\textbf{Proportion: }}}{
1.263 +% \setlength{\labelwidth}{8Pc}
1.264 +% \setlength{\labelsep}{0.5Pc}
1.265 +% \setlength{\rightmargin}{0Pc}
1.266 +% \setlength{\leftmargin}{4Pc}
1.267 +% \setlength{\parsep}{0ex plus 0.5ex}
1.268 +% \setlength{\listparindent}{1em}
1.269 +% \setlength{\itemsep}{1ex plus 0.5ex minus 0.2ex}
1.270 +% \setlength{\topsep}{0.5Pc}
1.271 +% }}
1.272 +% {\end{list}
1.273 +%}
1.274 +%
1.275 +%%Farben
1.276 +%
1.277 +%\newcommand{\red}[1]{\textcolor[rgb]{0.7,0,0}{\bf #1}}
1.278 +%\newcommand{\rd}[1]{\color{red}{#1}}
1.279 +%\newcommand{\white}[1]{\textcolor[rgb]{1,0,0}{\bf #1}}
1.280 +%\newcommand{\w}[1]{\color{white}{#1}}
1.281 +%\newcommand{\g}[1]{\color{myColor}{#1}}
1.282 +%
1.283 +%\usepackage{color}
1.284 +%\definecolor{myColor}{rgb}{0.9,0.9,0.9}% Wir definieren im RGB-Farbraum
1.285 +%
1.286 +%
1.287 +%\newcommand{\myDef}[1]{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\w .}\\[-0.2cm]\textbf{Definition\ \Nummer:}\\#1}}
1.288 +%\newcommand{\mySatz}[2]{\colorbox{myColor}{\parbox{\columnwidth}{\addtocounter{ctr}{1}{\g .}\\[-0.2cm]\textbf{Satz\ \Nummer:}\ #1\\ #2}}}
1.289 +%\newcommand{\myBeweis}[1]{\textit{\textbf{Beweis:}\\ #1}}
1.290 +%\newcommand{\myAlg}[2]{\parbox{\columnwidth}{\addtocounter{ctr}{1}\textbf{Algorithmus\ \Nummer:}\ \ #1\\#2}}
1.291 +%\newcommand{\myProg}[1]{\fbox{\parbox{\columnwidth}{#1}}}
1.292 +%
1.293 +%\newcommand{\add}[1]{\addtocounter{#1}{1}}
1.294 +%\newcommand{\zahl}[1]{\setcounter{#1}{Z}}
1.295 +%\newcommand{\Q}[2]{\parbox{\columnwidth}{$^{[\arabic{#1}/#2]}$ }}
1.296 +%
1.297 +%\newcommand{\Nummer}{\thesection.\arabic{ctr}}
1.298 +%
1.299 %---------- --------------------------------------------------- Beginn -----------------------------------------------------------------------
1.300
1.301 -\title{Greates common divisor \\ for multivariable Polynomials}
1.302 -\author{By\\Diana Meindl\\meindl$_-$diana@yahoo.com}
1.303 -\date{}
1.304 +\title{Greatest Common Divisor \\ for Multivariate Polynomials}
1.305 +\author{Diana Meindl\\meindl\_diana@yahoo.com}
1.306 +\date{\today}
1.307
1.308 \begin{document}
1.309 \maketitle
1.310 -{\w .}\\[12cm]
1.311 -\begin{center}
1.312 -Presented to \\
1.313 -A.Univ.Prof. Dipl.-Ing. Dr. Wolfgang Schreiner (RISC Insitute)\\
1.314 -and\\
1.315 -Dr. techn. Walther Neuper (Institut für Softwaretechnologie, TU Graz)
1.316 -\end{center}
1.317 +%{\w .}\\[12cm]
1.318 +%\begin{center}
1.319 +%Presented to \\
1.320 +%A.Univ.Prof. Dipl.-Ing. Dr. Wolfgang Schreiner (RISC Insitute)\\
1.321 +%and\\
1.322 +%Dr. techn. Walther Neuper (Institut für Softwaretechnologie, TU Graz)
1.323 +%\end{center}
1.324 +%\newpage
1.325 +%{\w .}\hspace{6.5cm}\textbf{Abstact}\\[0.5cm]
1.326 +
1.327 +\abstract{
1.328 +This is a proposal for a Masters Thesis at RISC, the Research Institute for Symbolic Computation at Linz University.\\
1.329 +
1.330 +Calculation with fractions is an important part of Computer Algebra Systems (CAS). This proposal aims at a specific part of such calculations, the greatest common divisor (GCD) used for cancellation, but in the very general context of multivariate polynomials. Cancellation of multivariate polynomials is a settled topic in Computer Algebra, respective algorithms well documented and implementations available in all CASs.
1.331 +
1.332 +This proposal claims for novelty with respect to the context of implementation in Computer Theorem Proving (CTP). On CTP's present development towards industrial use in software and systems verification, specific domain models involve demand on more and more mathematics, and within mathematics involve demand for more and more features. The proposed implementation of GCD and cancellation follows an actual demand.
1.333 +
1.334 +If the implementation is successful, it might be included into the distribution of Isabelle, one of the two dominating CTPs in Europe.
1.335 +}
1.336 +
1.337 \newpage
1.338 -{\w .}\hspace{6.5cm}\textbf{Abstact}\\[0.5cm]
1.339 -Calculation with fractions is an importent part of Computer-Algebra-Systems (CAS). Therefor you need algorithms for canceling fractions, respectively for the greatest common divisor (GCD).
1.340 +%WN vorerst zu Zwecken der "Ubersicht lassen ...
1.341 +\tableofcontents
1.342 +
1.343 \section{Background}
1.344 -The ISAC-project is a research and development project at the Institute for Software Technology of the Graz University of Technology. It is an educational mathematics assistant, a single-stepping system for applied mathematics based on the computer theorem prover Isabelle. The special is an easy readable knowledge base including Isabelles HOL-theories and a transparently working knowledge interpreter (a generalization of 'single stepping' algebra systems).
1.345 +The \sisac-project is a research and development project at the Institute for Software Technology of the Graz University of Technology. It is an educational mathematics assistant, a single-stepping system for applied mathematics based on the computer theorem prover Isabelle. The special is an easy readable knowledge base including Isabelles HOL-theories and a transparently working knowledge interpreter (a generalization of 'single stepping' algebra systems).
1.346 The background to both, development and research, is given by actual needs in math education as well as by foundamental questions about 'the mechanization of thinking' as an essential aspect in mathematics and in technology.
1.347 -The ISAC-system under construction comprises a tutoring-system and an authoring-system. The latter provides for adaption to various needs of individual users and educational institutions and for extensions to arbitrary fields of applied mathematics.
1.348 -
1.349 +The \sisac-system under construction comprises a tutoring-system and an authoring-system. The latter provides for adaption to various needs of individual users and educational institutions and for extensions to arbitrary fields of applied mathematics.
1.350 +
1.351 +TODO:\\
1.352 +European provers: Isabelle \cite{Nipkow-Paulson-Wenzel:2002}, Coq \cite{Huet_all:94}\\
1.353 +American provers: PVS~\cite{pvs}, ACL2~\footnote{http://userweb.cs.utexas.edu/~moore/acl2/}\\
1.354 +
1.355 \section{Goal of the thesis}
1.356 \subsection{Current situation}
1.357 -At the time there is no good implimentation for the problem of canceling fractions in Isac and or in Isabelle. But because canceling is important for calculating with fractions a new implimentation is necessary.
1.358 +At the time there is no good implimentation for the problem of canceling fractions in \sisac and or in Isabelle. But because canceling is important for calculating with fractions a new implimentation is necessary.
1.359
1.360 \subsection{Problem}
1.361 -The wish is to handle fractions in Isac not only in one variable also in more. So the goal of this thesis ist to find, assess and evaluate the existing algorithms and methods for finding the GCD. This will be an functional programm with the posibility to include it into Isabelle.
1.362 +The wish is to handle fractions in \sisac not only in one variable also in more. So the goal of this thesis ist to find, assess and evaluate the existing algorithms and methods for finding the GCD. This will be an functional programm with the posibility to include it into Isabelle.
1.363 +
1.364 +%WN eine pr"azisere Beschreibung des Problems kann ich mir nicht vorstellen (englische Version der Mail haben wir auch, aber sie passt nicht zur deutschen Antwort von Prof.Nipkow) ...
1.365 +\bigskip
1.366 +TODO Mail to Prof. Nipkow, leader of the development of Isabelle \cite{Nipkow-Paulson-Wenzel:2002} at TU M\"unchen, Mon, 23 May 2011 08:58:14 +0200:
1.367 +\begin{verbatim}
1.368 +Eine erste Idee, wie die Integration der Diplomarbeit f"ur
1.369 +einen Benutzer von Isabelle aussehen k"onnte, w"are zum
1.370 +Beispiel im
1.371 +
1.372 + lemma cancel:
1.373 + assumes asm3: "x2 - x*y \<noteq> 0" and asm4: "x \<noteq> 0"
1.374 + shows "(x2 - y2) / (x2 - x*y) = (x + y) / (x::real)"
1.375 + apply (insert asm3 asm4)
1.376 + apply simp
1.377 + sorry
1.378 +
1.379 +die Assumptions
1.380 +
1.381 + asm1: "(x2 - y2) = (x + y) * (x - y)" and asm2: "x2 - x*y = x * (x - y)"
1.382 +
1.383 +im Hintergrund automatisch zu erzeugen (mit der Garantie,
1.384 +dass "(x - y)" der GCD ist) und sie dem Simplifier (f"ur die
1.385 +Rule nonzero_mult_divide_mult_cancel_right) zur Verf"ugung zu
1.386 +stellen, sodass anstelle von "sorry" einfach "done" stehen kann.
1.387 +Und weiters w"are eventuell asm3 zu "x - y \<noteq> 0" zu vereinfachen,
1.388 +eine Rewriteorder zum Herstellen einer Normalform festzulegen, etc.
1.389 +\end{verbatim}
1.390 +%WN und eine bessere Motivation f"ur eine Master Thesis kann ich mir auch nicht vorstellen ...
1.391 +Response of Prof. Nipkow:
1.392 +
1.393 +\begin{verbatim}
1.394 +Unser Spezialist fuer die mathematischen Theorien ist Johannes H"olzl.
1.395 +Etwas allgemeinere Fragen sollten auf jeden Fall an isabelle-dev@
1.396 +gestellt werden.
1.397 +
1.398 +Viel Erfolg bei der Arbeit!
1.399 +Tobias Nipkow
1.400 +\end{verbatim}
1.401 +
1.402 +
1.403 \subsection{Expected results}
1.404 Find good algorithms for the different problems, and find out which one will be the best for the special problem.\\
1.405 The program should handeling:
1.406 @@ -179,29 +243,184 @@
1.407 \item[]real and rational coefficients. Maybe also imaginary coefficients.
1.408 \item[]Mulivariable polynomials canceling and adding, when they are in normalform.
1.409 \end{itemize}
1.410 -For the program should be used a functional programming language with good commentaries. And it should be based on Isabelle and works correctly in Isac.
1.411 -\newpage
1.412 +For the program should be used a functional programming language with good commentaries. And it should be based on Isabelle and works correctly in \sisac.
1.413
1.414 \section{State of the art}
1.415 -Was ist vorhanden, was kann ich aus welchen Büchern für meine Arbeit verwenden
1.416 -Es gibt verschiedene CAS die bereits einen Algrotihmus implimentiert haben, wie haben die das gemacht, und welcher ist für mich am besten.
1.417 +In a broad view the context of this thesis can be seen as ``computation and deduction'': simplification and in particular cancellation of rational terms is concern of \textbf{computation} implemented in Computer Algebra Systems (CAS) --- whereas the novelty within the thesis is given by an implementation of cancellation in a computer theorem prover (CTP), i.e. in the domain of \textbf{deduction} with respective logical rigor not addressed in the realm of CAS.
1.418
1.419 -\newpage
1.420 +Below, after a general survey on computation, represented by CAS, and on deduction, represented by CTP, a more narrow view on ``CAS-functionality in CTP'' is pursued.
1.421 +
1.422 +\subsection{Computer Algebra and Proof Assistants}
1.423 +%WN achtung: diese subsection is fast w"ortlich kopiert aus \cite{plmms10} -- also in der Endfassung bitte "uberarbeiten !!!
1.424 +Computer Algebra and Proof Assistants have coexisted for a many years so there is much research trying to bridge the gap between these approaches from both sides. We shall continue to abbreviate Computer Algebra (Systems) by ``CAS'', and in analogy we shall abbreviate proof assistants by CTP, computer theorem provig (comprising both, interactive theorem proving (ITP) and automated theorem proving (ATP), since in CTP there are ATP-tools included today.)
1.425 +
1.426 +First, many CTPs already have CAS-like functionality,
1.427 +especially for domains like arithmetic. They provide the user
1.428 +with conversions, tactics or decision procedures that solve
1.429 +problems in a particular domain. Such decision procedures present
1.430 +in the standard library of HOL Light~\footnote{http://www.cl.cam.ac.uk/~jrh13/hol-light/} are used inside the
1.431 +prototype described in Sect.\ref{cas-funct} on p.\pageref{part-cond} for arithmetic's,
1.432 +symbolic differentiation and others.
1.433 +
1.434 +Similarly some CAS systems provide environments that allow
1.435 +logical reasoning and proving properties within the system. Such
1.436 +environments are provided either as logical
1.437 +extensions (e.g.~\cite{logicalaxiom}) or are implemented within a
1.438 +CAS using its language~\cite{theorema00}.
1.439 +
1.440 +There are numerous architectures for information exchange between
1.441 +CAS and CTP with different levels of \emph{degree of trust}
1.442 +between the prover and the CAS. In principle, there are several approaches.
1.443 +If CAS-functionality is not fully embedded in CTP, CAS can be called as ``oracles'' nevertheless (for efficiency reasons, in general) --- their results are regarded like prophecies of Pythia in Delphi. There are three kinds of checking oracles, however:
1.444 +\begin{enumerate}
1.445 +\item Just adopt the CAS result without any check. Isabelle internally marks such results.
1.446 +\item Check the result inside CTP. There are many cases, where such checks are straight forward, for instance, checking the result of factorization by multiplication of the factors, or checking integrals by differentiation.
1.447 +\item Generate a derivation of the result within CTP; in Isabelle this is called ``proof reconstruction''.
1.448 +\end{enumerate}
1.449 +A longer list of frameworks for
1.450 +information exchange and bridges between systems can be found
1.451 +in~\cite{casproto}.
1.452 +
1.453 +There are many approaches to defining partial functions in proof
1.454 +assistants. Since we would like the user to define functions
1.455 +without being exposed to the underlying logic of the proof
1.456 +assistant we only mention some automated mechanisms for defining
1.457 +partial functions in the logic of a CTP.
1.458 +Krauss~\cite{krauss} has developed a framework for defining
1.459 +partial recursive functions in Isabelle/HOL, which formally
1.460 +proves termination by searching for lexicographic combinations of
1.461 +size measures. Farmer~\cite{farmer} implements a scheme for
1.462 +defining partial recursive functions in \textrm{IMPS}.
1.463 +
1.464 +\subsection{Motivation for CAS-functionality in CTP}
1.465 +In the realm of CTP formuas are dominated by quantifiers $\forall$, $\exists$ and $\epsilon$ (such) and by operations like $\Rightarrow$, $\land$ and $\lor$. Numbers were strangers initially; numerals have been introduced to Isabelle not much before the year 2000~\footnote{In directory src/Provers/Arith/ see the files cancel\_numerals.ML and cancel\_numeral\_factor.ML in the Isabelle distribution 2011. They still use the notation $\#1,\#2,\#3,\dots$ from before 2000~!}. However, then numerals have been implemented with {\em polymorphic type} such that $2\cdot r\cdot\pi$ ($2$ is type \textit{real}) and $\pi_{\it approx}=3.14\,\land\, 2\cdot r\cdot\pi_{\it approx}$ can be written as well as $\sum_i^n i=\frac{n\cdot(n+1)}{2}$ ($2$ is type \textit{nat}). The different types are inferred by Hindle-Milner type inference \cite{damas-milner-82,Milner-78,Hindley-69}.
1.466 +
1.467 +1994 was an important year for CTP: the Pentium Bug caused excitement in the IT community all around the world and motivated INTEL to invest greatly into formal verification of circuits (which carried over to verification of software). Not much later John Harrison mechanized real numbers as Dedekind Cuts in HOL Light \footnote{http://www.cl.cam.ac.uk/~jrh13/hol-light/} and derived calculus, derivative and integral from that definition \cite{harr:thesis}, an implementation which has been transferred to Isabelle very soon after that~\footnote{In the directory src/HOL/Multivariate\_Analysis/ see the files Gauge\_Measure.thy, Integration.thy, Derivative.thy, Real\_Integration.thy, Brouwer\_Fixpoint.thy, Fashoda.thy}.
1.468 +
1.469 +Harrison also says that ``CAS are ill-defined'' and gives, among others, an example relevant for this thesis on cancellation: TODO ... meromorphic functions ...
1.470 +
1.471 +\medskip
1.472 +The main motivation for further introduction of CAS-functionality to CTP is also technology-driven: In this decade domain engineering is becoming an academic discipline with industrial relevance \cite{db:dom-eng}: vigorous efforts extend the scope of formal specifications even beyond software technology, and thus respective domains of mathematical knowledge are being mechanized in CTP. The Archive of Formal Proofs~\footnote{http://afp.sourceforge.net/} is Isabelle's repository for such work.
1.473 +
1.474 +\subsection{Simplification within CTP}
1.475 +Cancellation, the topic of this thesis, is a specific part of simplification of rationals. In the realm of CAS cancellation is {\em not} an interesting part of the state of the art, because cancellation has been implemented in the prevailing CAS more than thirty years ago --- however, cancellation of multivariate polynomials is {\em not} yet implemted in any of the dominating CTPs.
1.476 +%WN: bitte mit Anfragen an die Mailing-Listen nachpr"ufen: Coq, HOL, ACL2, PVS
1.477 +
1.478 +As in other CTPs, in Isabelle the simplifier is a powerful software component; the sets of rewrite rules, called \textit{simpsets}, contain several hundreds of elements. Rewriting is still very efficient, because the simpsets are transformed to term nets \cite{term-nets}.
1.479 +
1.480 +Rational terms of multivariate polynomials still have a normal form \cite{bb-loos} and thus equivalence of respective terms is decidable. This is not the case, however, with terms containing roots or transcedent functions. Thus, CAS are unreliable by design in these cases.
1.481 +
1.482 +In CTP, simplification of non-decidable domains is already an issue, as can be seem in the mail with subject ``simproc divide\_cancel\_factor produces error'' in the mailing-list \textit{isabelle-dev@mailbroy.informatik.tu-muenchen.de} from Thu, 15 Sep 2011 16:34:12 +0200
1.483 +{%\footnotesize --- HILFT NICHTS
1.484 +\begin{verbatim}
1.485 +Hi everyone,
1.486 +
1.487 +in the following snippet, applying the simplifier causes an error:
1.488 +
1.489 +------------------------------------------
1.490 +theory Scratch
1.491 + imports Complex_Main
1.492 +begin
1.493 +
1.494 +lemma
1.495 + shows "(3 / 2) * ln n = ((6 * k * ln n) / n) * ((1 / 2 * n / k) / 2)"
1.496 +apply simp
1.497 +------------------------------------------
1.498 +
1.499 +outputs
1.500 +
1.501 +------------------------------------------
1.502 +Proof failed.
1.503 +(if n = 0 then 0 else 6 * (k * ln n) / 1) * 2 / (4 * k) =
1.504 +2 * (Numeral1 * (if n = 0 then 0 else 6 * (k * ln n) / 1)) / (2 * (2 * k))
1.505 + 1. n \not= Numeral0 \rightarrow k * (ln n * (2 * 6)) / (k * 4) = k * (ln n * 12) / (k * 4)
1.506 +1 unsolved goal(s)!
1.507 +The error(s) above occurred for the goal statement:
1.508 +(if n = 0 then 0 else 6 * (k * ln n) / 1) * 2 / (4 * k) =
1.509 +2 * (Numeral1 * (if n = 0 then 0 else 6 * (k * ln n) / 1)) / (2 * (2 * k))
1.510 +------------------------------------------
1.511 +\end{verbatim}
1.512 +}
1.513 +Mail ``Re: simproc divide\_cancel\_factor produces error'' on Fri, 16 Sep 2011 22:33:36 +0200
1.514 +\begin{verbatim}
1.515 +> > After the release, I'll have to think about doing a complete overhaul
1.516 +> > of all of the cancellation simprocs.
1.517 +You are very welcome to do so. Before you start, call on me and I will
1.518 +write down some ideas I had long ago (other may want to join, too).
1.519 +\end{verbatim}
1.520 +%WN: bist du schon angemeldet in den Mailing-Listen isabelle-users@ und isabelle-dev@ ? WENN NICHT, DANN WIRD ES H"OCHSTE ZEIT !!!
1.521 +
1.522 +\subsection{Open Issues with CAS-functionality in CTP}\label{cas-funct}
1.523 +There is at least one effort explicitly dedicated to implement CAS-functionality in CTP \cite{cezary-phd}. %WN bitte unbedingt lesen (kann von mir in Papierform ausgeborgt werden) !!!
1.524 +In this work three issues has been identified: partiality conditions, multi-valued functions and real numbers. These issues are addressed in the subsequent paragraphs, followed by a forth issue raised by \sisac.
1.525 +
1.526 +\paragraph{Partiality conditions}\label{part-cond} are introduced by partial functions or by conditional rewriting. An example of how the CAS-functionality \cite{cezary-phd} looks like is given on p.\pageref{fig:casproto}.
1.527 +\cite{cezary-phd} gives an introductory example (floated to p.\pageref{fig:casproto}) which will be referred to in the sequel.
1.528 +\input{thol.tex}
1.529 +%WN das nachfolgende Format-Problem l"osen wir sp"ater ...
1.530 +\begin{figure}[hbt]
1.531 +\begin{center}
1.532 +\begin{holnb}
1.533 + In1 := vector [\&2; \&2] - vector [\&1; \&0] + vec 1
1.534 + Out1 := vector [\&2; \&3]
1.535 + In2 := diff (diff (\Lam{}x. \&3 * sin (\&2 * x) +
1.536 + \&7 + exp (exp x)))
1.537 + Out2 := \Lam{}x. exp x pow 2 * exp (exp x) +
1.538 + exp x * exp (exp x) + -- \&12 * sin (\&2 * x)
1.539 + In3 := N (exp (\&1)) 10
1.540 + Out3 := #2.7182818284 + ... (exp (\&1)) 10 F
1.541 + In4 := x + \&1 - x / \&1 + \&7 * (y + x) pow 2
1.542 + Out4 := \&7 * x pow 2 + \&14 * x * y + \&7 * y pow 2 + \&1
1.543 + In5 := sum (0,5) (\Lam{}x. \&x * \&x)
1.544 + Out5 := \&30
1.545 + In6 := sqrt (x * x) assuming x > &1
1.546 + Out6 := x
1.547 +\end{holnb}
1.548 +\end{center}
1.549 +\caption{\label{fig:casproto}Example interaction with the prototype
1.550 + CAS-like input-response loop. For the user input given in the
1.551 + \texttt{In} lines, the system produces the output in \texttt{Out}
1.552 + lines together with HOL Light theorems that state the equality
1.553 + between the input and the output.}
1.554 +\end{figure}
1.555 +In lines {\tt In6, Out6} this examples shows how to reliably simplify $\sqrt{x}$. \cite{caspartial} %TODO
1.556 +gives more details on handling side conditions in formalized partial functions.
1.557 +
1.558 +Analoguous to this example, cancellations (this thesis is concerned with) like
1.559 +$$\frac{x^2-y^2}{x^2-x\cdot y}=\frac{x+y}{x}\;\;\;\;{\it assuming}\;x-y\not=0\land x\not=0$$
1.560 +produce assumptions, $x-y\not=0, x\not=0$ here. Since the code produced in the framework of this thesis will be implemented in Isabelle's simplifier (outside this thesis), the presentation to the user will be determined by Isabelle and \sisac{} using the respective component of Isabelle. Also reliable handling of assumptions like $x-y\not=0, x\not=0$ is up to these systems.
1.561 +
1.562 +\paragraph{Multi-valued functions:}\label{multi-valued}
1.563 +\cite{seeingroots,davenp-multival-10} discuss cases where CAS are error prone when dropping a branch of a multi-valued function~\footnote{``Multivalued \textit{function}'' is a misnomer, since the value of a function applied to a certain argument is unique by definition of function.}. Familiar examples are ...
1.564 +%WN ... zur Erkl"arung ein paar Beispiele von http://en.wikipedia.org/wiki/Multivalued_function
1.565 +
1.566 +\paragraph{Real numbers} cannot be represented by numerals. In engineering applications, however, approximation by floating-point numbers are frequently useful. In CTP floating-point numbers must be handled rigorously as approximations. Already \cite{harr:thesis} introduced operations on real numerals accompanied by rigorous calculation of precision. \cite{russellphd} describes efficient implementation of infinite precision real numbers in Coq.
1.567 +
1.568 +\paragraph{All solutions for equations} must be guaranted, if equation solving is embedded within CTP. So, given an equation $f(x)=0$ and the set of solutions $S$ of this equation, we want to have both,
1.569 +\begin{eqnarray}
1.570 + \exists x_s.\;x_s\in S &\Rightarrow& f(x_s) = 0 \\\label{is-solut}
1.571 + x_s\in S &\Leftarrow& \exists x_s.\;f(x_s) = 0 \label{all-solut}
1.572 +\end{eqnarray}
1.573 +where (\ref{all-solut}) ensures that $S$ contains {\em all} solutions of the equation. The \sisac-project has implemented a prototype of an equation solver~\footnote{See \textit{equations} in the hierarchy of specifications at http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}.
1.574 +
1.575 +There is demand for fullfledged equation solving in CTP, including equational systems and differential equations, because \sisac{} has a prototype of a CTP-based programming language calling CAS functions; and Lucas-Interpretation \cite{wn:lucas-interp-12} makes these functions accessible by single-stepping and ``next step guidance'', which would automatically generate a learning system for equation solving.
1.576 +
1.577 +
1.578 \section{Thesis structure}
1.579 The proposed table of contents of the thesis on the chapter level is as follows:
1.580 \begin{enumerate}
1.581 \item Introduction (2-3 pages)
1.582 \item Computer Algebra Systems (CAS) (5 - 7 pages)\\
1.583 Which different CAS exists and whats the foucus of them.
1.584 - \item The \textit{ISAC}-Project (5 - 7 pages)\\
1.585 - This chapter will describe the \textit{ISAC}-Project and the goals of the project.
1.586 + \item The \textit{\sisac}-Project (5 - 7 pages)\\
1.587 + This chapter will describe the \textit{\sisac}-Project and the goals of the project.
1.588 \item Univariate Polynomials (15-20 pages)\\
1.589 This chapter will describe different Algorithms for univariate polynomials, with different coefficients.
1.590 \item Multivariate Polynomials (20-25 pages)\\
1.591 This chapter will describe different Algorithms for multivariate polynomials, with different coefficients
1.592 \item Functional programming and SML(2-5 pages)\\
1.593 The basic idea of this programming languages.
1.594 - \item Implimentation in \textit{ISAC}-Project (15-20 pages)
1.595 + \item Implimentation in \textit{\sisac}-Project (15-20 pages)
1.596 \item Conclusion (2-3 pages)
1.597 \end{enumerate}
1.598 %\newpage
1.599 @@ -222,28 +441,58 @@
1.600 & & for univariate Polynomials \\ \hline
1.601 & Multivariate Polynomials & Implimentation of the Algorithm\\
1.602 & & for multivariate Polynomials \\ \hline
1.603 - & The Isac-Project &\\ \hline
1.604 + & The \sisac-Project &\\ \hline
1.605 & Conclusion and Introduction & Find good examples for testing\\
1.606 \hline
1.607 \end{tabular}
1.608 \end{center}
1.609
1.610 \newpage
1.611 +
1.612 +\cite{einf-funct-progr} \cite{Winkler:96}
1.613
1.614 -\section{Bibliography}
1.615 -%mindestens 10
1.616 -\begin{enumerate}
1.617 - \item Bird/Wadler, \textit{Einführung in die funktionale Programmierung}, Carl Hanser and Prentice-Hall International, 1992
1.618 - \item Franz Winkler, \textit{Polynomial Algorithms in Computer Algebra}, Springer,1996
1.619 - \item %M. Mignotte, \textit{An inequality about factors of polynomial}
1.620 - \item %M. Mignotte, \textit{Some useful bounds}
1.621 - \item %W. S. Brown and J. F. Traub. \textit{On euclid's algorithm and the theory of subresultans}, Journal of the ACM (JACM), 1971
1.622 - \item %Bruno Buchberger, \textit{Algorhimic mathematics: Problem types, data types, algorithm types}, Lecture notes, RISC Jku A-4040 Linz, 1982
1.623 -
1.624 - \item %Tateaki Sasaki and Masayuki Suzuki, \textit{Thre new algorithms for multivariate polynomial GCD}, J. Symbolic Combutation, 1992
1.625 - \item
1.626 - \item
1.627 - \item
1.628 -\end{enumerate}
1.629 +\bibliography{references}
1.630 +%\section{Bibliography}
1.631 +%%mindestens 10
1.632 +%\begin{enumerate}
1.633 +% \item Bird/Wadler, \textit{Einführung in die funktionale Programmierung}, Carl Hanser and Prentice-Hall International, 1992
1.634 +% \item Franz Winkler, \textit{Polynomial Algorithms in Computer Algebra}, Springer,1996
1.635 +% \item %M. Mignotte, \textit{An inequality about factors of polynomial}
1.636 +% \item %M. Mignotte, \textit{Some useful bounds}
1.637 +% \item %W. S. Brown and J. F. Traub. \textit{On euclid's algorithm and the theory of subresultans}, Journal of the ACM (JACM), 1971
1.638 +% \item %Bruno Buchberger, \textit{Algorhimic mathematics: Problem types, data types, algorithm types}, Lecture notes, RISC Jku A-4040 Linz, 1982
1.639 +%
1.640 +% \item %Tateaki Sasaki and Masayuki Suzuki, \textit{Thre new algorithms for multivariate polynomial GCD}, J. Symbolic Combutation, 1992
1.641 +% \item
1.642 +% \item
1.643 +% \item
1.644 +%\end{enumerate}
1.645
1.646 -\end{document}
1.647 \ No newline at end of file
1.648 +\end{document}
1.649 +
1.650 +WN110916 grep-ing through Isabelle code:
1.651 +
1.652 +neuper@neuper:/usr/local/isabisac/src$ find -name "*umeral*"
1.653 +./HOL/ex/Numeral.thy
1.654 +./HOL/Tools/nat_numeral_simprocs.ML
1.655 +./HOL/Tools/numeral_syntax.ML
1.656 +./HOL/Tools/numeral.ML
1.657 +./HOL/Tools/numeral_simprocs.ML
1.658 +./HOL/Matrix/ComputeNumeral.thy
1.659 +./HOL/Library/Numeral_Type.thy
1.660 +./HOL/Numeral_Simprocs.thy
1.661 +./HOL/Import/HOL/numeral.imp
1.662 +./HOL/Code_Numeral.thy
1.663 +./HOL/Nat_Numeral.thy
1.664 +./ZF/Tools/numeral_syntax.ML
1.665 +./Provers/Arith/cancel_numeral_factor.ML
1.666 +./Provers/Arith/cancel_numerals.ML
1.667 +./Provers/Arith/combine_numerals.ML
1.668 +
1.669 +neuper@neuper:/usr/local/isabisac/src$ find -name "*ancel*"
1.670 +./HOL/Tools/abel_cancel.ML
1.671 +./Provers/Arith/cancel_div_mod.ML
1.672 +./Provers/Arith/cancel_numeral_factor.ML Paulson 2000 !!!
1.673 +./Provers/Arith/cancel_sums.ML
1.674 +./Provers/Arith/cancel_numerals.ML Paulson 2000
1.675 +
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/isac/dmeindl/references.bib Sun Sep 18 15:21:46 2011 +0200
2.3 @@ -0,0 +1,300 @@
2.4 +@proceedings{DBLP:conf/mkm/2007,
2.5 + editor = {Manuel Kauers and
2.6 + Manfred Kerber and
2.7 + Robert Miner and
2.8 + Wolfgang Windsteiger},
2.9 + title = {Towards Mechanized Mathematical Assistants, 14th Symposium,
2.10 + Calculemus 2007, 6th International Conference, MKM 2007,
2.11 + Hagenberg, Austria, June 27-30, 2007, Proceedings},
2.12 + booktitle = {Calculemus/MKM},
2.13 + publisher = {Springer},
2.14 + series = {Lecture Notes in Computer Science},
2.15 + volume = {4573},
2.16 + year = {2007},
2.17 + isbn = {978-3-540-73083-5},
2.18 + bibsource = {DBLP, http://dblp.uni-trier.de}
2.19 +}
2.20 +
2.21 +@proceedings{DBLP:conf/cade/2006,
2.22 + editor = {Ulrich Furbach and
2.23 + Natarajan Shankar},
2.24 + title = {Automated Reasoning, Third International Joint Conference,
2.25 + IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
2.26 + booktitle = {IJCAR},
2.27 + publisher = {Springer},
2.28 + series = {Lecture Notes in Computer Science},
2.29 + volume = {4130},
2.30 + year = {2006},
2.31 + isbn = {3-540-37187-7},
2.32 + bibsource = {DBLP, http://dblp.uni-trier.de}
2.33 +}
2.34 +
2.35 +@proceedings{DBLP:conf/iwfm/1999,
2.36 + editor = {Andrew Butterfield and
2.37 + Klemens Haegele},
2.38 + title = {3rd Irish Workshop on Formal Methods, Galway, Eire, July
2.39 + 1999},
2.40 + booktitle = {IWFM},
2.41 + publisher = {BCS},
2.42 + series = {Workshops in Computing},
2.43 + year = {1999},
2.44 + bibsource = {DBLP, http://dblp.uni-trier.de}
2.45 +}
2.46 +
2.47 +@proceedings{DBLP:conf/aisc/2008,
2.48 + editor = {Serge Autexier and
2.49 + John Campbell and
2.50 + Julio Rubio and
2.51 + Volker Sorge and
2.52 + Masakazu Suzuki and
2.53 + Freek Wiedijk},
2.54 + title = {Intelligent Computer Mathematics, 9th International Conference,
2.55 + AISC 2008, 15th Symposium, Calculemus 2008, 7th International
2.56 + Conference, MKM 2008, Birmingham, UK, July 28 - August 1,
2.57 + 2008. Proceedings},
2.58 + booktitle = {AISC/MKM/Calculemus},
2.59 + publisher = {Springer},
2.60 + series = {Lecture Notes in Computer Science},
2.61 + volume = {5144},
2.62 + year = {2008},
2.63 + isbn = {978-3-540-85109-7},
2.64 + bibsource = {DBLP, http://dblp.uni-trier.de}
2.65 +}
2.66 +
2.67 +@InProceedings{wn:lucas-interp-12,
2.68 + author = {Neuper, Walther},
2.69 + title = {Automated Generation of User Guidance by Combining Computation and Deduction},
2.70 + booktitle = {THedu'11: CTP-compontents for educational software},
2.71 + year = {2012},
2.72 + editor = {Quaresma, Pedro},
2.73 + publisher = {EPTCS},
2.74 + note = {To appear}
2.75 +}
2.76 +
2.77 +@InProceedings{davenp-multival-10,
2.78 + author = {Davenport, James},
2.79 + title = {The Challenges of Multivalued "Functions"},
2.80 + booktitle = {Proceedings of the Conferences on Intelligent Computer Mathematics (CICM)},
2.81 + year = {2010}
2.82 +}
2.83 +
2.84 +@PhdThesis{cezary-phd,
2.85 + author = {Kalisyk, Cezary},
2.86 + title = {TODO},
2.87 + school = {},
2.88 + year = {},
2.89 + OPTkey = {},
2.90 + OPTtype = {},
2.91 + OPTaddress = {},
2.92 + OPTmonth = {},
2.93 + OPTnote = {},
2.94 + OPTannote = {}
2.95 +}
2.96 +
2.97 +@Book{bb-loos,
2.98 + editor = {Buchberger, Bruno and Collins, George Edwin and Loos,
2.99 + R\"udiger and Albrecht, Rudolf},
2.100 + title = {Computer Algebra. Symbolic and Algebraic Computation},
2.101 + publisher = {Springer Verlag},
2.102 + year = {1982},
2.103 + edition = {2}
2.104 +}
2.105 +
2.106 +@Book{term-nets,
2.107 + author = {Charniak, E. and Riesbeck, C. K. and McDermott, D. V.},
2.108 + title = {Artificial Intelligence Programming},
2.109 + publisher = {Lawrence Erlbaum Associates},
2.110 + year = {1980},
2.111 + note = {(Chapter 14)}
2.112 +}
2.113 +
2.114 +@Book{db:dom-eng,
2.115 + author = {Bj{\o}rner, Dines},
2.116 + title = {Domain Engineering. Technology Management, Research and Engineering},
2.117 + publisher = {JAIST Press},
2.118 + year = {2009},
2.119 + month = {Feb},
2.120 + series = {COE Research Monograph Series},
2.121 + volume = {4},
2.122 + address = {Nomi, Japan}
2.123 +}
2.124 +
2.125 +@techreport{harr:thesis,
2.126 + author={Harrison, John R.},
2.127 + title={Theorem proving with the real numbers},
2.128 + institution={University of Cambridge, Computer Laboratory},year={1996},
2.129 + type={Technical Report},number={408},address={},month={November},
2.130 + note={},status={},source={},location={loc?}
2.131 + }
2.132 +
2.133 +@InProceedings{damas-milner-82,
2.134 + author = {Damas, Luis and Milner, Robin},
2.135 + title = {Principal type-schemes for functional programs},
2.136 + booktitle = {9th Symposium on Principles of programming languages (POPL'82)},
2.137 + pages = {207-212},
2.138 + year = {1982},
2.139 + editor = {ACM}
2.140 +}
2.141 +
2.142 +@Article{Milner-78,
2.143 + author = {Milner, R.},
2.144 + title = {A Theory of Type Polymorphism in Programming},
2.145 + journal = {Journal of Computer and System Science (JCSS)},
2.146 + year = {1978},
2.147 + number = {17},
2.148 + pages = {348-374}
2.149 +}
2.150 +
2.151 +@Article{Hindley-69,
2.152 + author = {Hindley, R.},
2.153 + title = {The Principal Type-Scheme of an Object in Combinatory Logic},
2.154 + journal = {Transactions of the American Mathematical Society},
2.155 + year = {1969},
2.156 + volume = {146},
2.157 + pages = {29-60}
2.158 +}
2.159 +
2.160 +@article{seeingroots,
2.161 + author = {Jeffrey, D.J. and Norman, A.C.},
2.162 + title = {Not seeing the roots for the branches: multivalued functions in computer algebra},
2.163 + journal = {SIGSAM Bull.},
2.164 + volume = {38},
2.165 + number = {3},
2.166 + year = {2004},
2.167 + issn = {0163-5824},
2.168 + pages = {57--66},
2.169 + doi = {http://doi.acm.org/10.1145/1040034.1040036},
2.170 + publisher = {ACM},
2.171 + address = {New York, NY, USA},
2.172 + }
2.173 +
2.174 +@PhdThesis{russellphd,
2.175 + author = {Russell O'Connor},
2.176 + title = {Incompleteness and Completeness.},
2.177 + school = {Radboud University Nijmegen},
2.178 + year = {2009},
2.179 +}
2.180 +
2.181 +@inproceedings{caspartial,
2.182 + author = {Cezary Kaliszyk},
2.183 + title = {Automating Side Conditions in Formalized Partial Functions},
2.184 + booktitle = {AISC/MKM/Calculemus},
2.185 + year = {2008},
2.186 + pages = {300-314},
2.187 + ee = {http://dx.doi.org/10.1007/978-3-540-85110-3_26},
2.188 + crossref = {DBLP:conf/aisc/2008},
2.189 + bibsource = {DBLP, http://dblp.uni-trier.de}
2.190 +}
2.191 +
2.192 +@inproceedings{farmer,
2.193 + author = {Farmer, William M.},
2.194 + title = {A Scheme for Defining Partial Higher-Order Functions by
2.195 + Recursion.},
2.196 + booktitle = {IWFM},
2.197 + year = {1999},
2.198 + crossref = {DBLP:conf/iwfm/1999},
2.199 + bibsource = {DBLP, http://dblp.uni-trier.de}
2.200 +}
2.201 +
2.202 +@inproceedings{krauss,
2.203 + author = {Krauss, Alexander},
2.204 + title = {Partial Recursive Functions in Higher-Order Logic},
2.205 + booktitle = {IJCAR},
2.206 + year = {2006},
2.207 + pages = {589-603},
2.208 + ee = {http://dx.doi.org/10.1007/11814771_48},
2.209 + crossref = {DBLP:conf/cade/2006},
2.210 + bibsource = {DBLP, http://dblp.uni-trier.de}
2.211 +}
2.212 +
2.213 +@inproceedings{casproto,
2.214 + author = {Cezary Kaliszyk and
2.215 + Freek Wiedijk},
2.216 + title = {Certified Computer Algebra on Top of an Interactive Theorem
2.217 + Prover},
2.218 + booktitle = {Calculemus},
2.219 + year = {2007},
2.220 + pages = {94-105},
2.221 + ee = {http://dx.doi.org/10.1007/978-3-540-73086-6_8},
2.222 + crossref = {DBLP:conf/mkm/2007},
2.223 + bibsource = {DBLP, http://dblp.uni-trier.de}
2.224 +}
2.225 +
2.226 +@inproceedings{theorema00,
2.227 + author = "Buchberger, B. and
2.228 + Dupre, C. and
2.229 + Jebelean, T. and
2.230 + Kriftner, F. and
2.231 + Nakagawa, K. and
2.232 + Vasaru, D. and
2.233 + Windsteiger, W.",
2.234 + title = "{The Theorema Project: A Progress Report}",
2.235 + booktitle = "Symbolic Computation and Automated Reasoning
2.236 + (Proceedings of CALCULEMUS 2000, Symposium on the Integration of
2.237 + Symbolic Computation and Mechanized Reasoning)",
2.238 + editor = "Kerber, M. and
2.239 + Kohlhase, M.",
2.240 + publisher = "A.K.~Peters",
2.241 + address = "Natick, Massachusetts",
2.242 + isbn = "1-56881-145-4",
2.243 + year = 2000
2.244 +}
2.245 +
2.246 +@inproceedings{logicalaxiom,
2.247 + author = {E. Poll and S. Thompson},
2.248 + title = {{Adding the axioms to Axiom: Towards a system of automated reasoning in Aldor}},
2.249 + booktitle = {Calculemus and Types '98},
2.250 + year = {1998},
2.251 + place = {Eindhoven, The Netherlands},
2.252 + month = {July},
2.253 + note = {Also as technical report 6-98, Computing Laboratory, University of Kent}
2.254 +}
2.255 +
2.256 +@InProceedings{pvs,
2.257 + author = {Owre, S. and Rajan, S. and Rushby, J. and Shankar, N. and Srivas, M.},
2.258 + title = {{PVS}: Combining specification, proof checking, and model checking},
2.259 + booktitle = {Computer-Aided Verification},
2.260 + pages = {411-414},
2.261 + year = {1996},
2.262 + editor = {Alur, R. and Henzinger, T.A.},
2.263 + organization = {CAV'96},
2.264 + annote = {}
2.265 +}
2.266 +
2.267 +@Book{Nipkow-Paulson-Wenzel:2002,
2.268 + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
2.269 + title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
2.270 + publisher = {Springer},
2.271 + series = {LNCS},
2.272 + volume = 2283,
2.273 + year = 2002
2.274 +}
2.275 +
2.276 +@Manual{Huet_all:94,
2.277 + author = {Huet, G. and Kahn, G. and and Paulin-Mohring, C.},
2.278 + title = {The Coq Proof Assistant},
2.279 + institution = {INRIA-Rocquencourt},
2.280 + year = {1994},
2.281 + type = {Tutorial},
2.282 + number = {Version 5.10},
2.283 + address = {CNRS-ENS Lyon},
2.284 + status={},source={Theorema},location={-}
2.285 +}
2.286 +
2.287 +@Book{einf-funct-progr,
2.288 + author = {Richard Bird and Philip Wadler},
2.289 + title = {Introduction to Functional Programming},
2.290 + publisher = {Prentice Hall},
2.291 + year = 1988,
2.292 + editor = {C. A. R. Hoare},
2.293 + series = {Prentice Hall International Series in Computer Science},
2.294 + address = {New York, London, Toronto, Sydney, Tokyo},
2.295 + annote = {88bok371}
2.296 +}
2.297 +@Book{Winkler:96,
2.298 + author = {F. Winkler},
2.299 + title = {{Polynomial Algorithms in Computer Algebra}},
2.300 + publisher = {Springer-Verlag Wien New York},
2.301 + year = {1996}
2.302 +}
2.303 +
3.1 Binary file doc-src/isac/dmeindl/thol.tex has changed
4.1 --- a/src/Tools/isac/Interpret/mstools.sml Tue Sep 13 10:51:56 2011 +0200
4.2 +++ b/src/Tools/isac/Interpret/mstools.sml Sun Sep 18 15:21:46 2011 +0200
4.3 @@ -976,7 +976,8 @@
4.4 let
4.5 fun get_vars ((v,T)::vs) = (case raw_explode v |> Library.read_int of
4.6 (_, _::_) => (Free (v,T)::get_vars vs)
4.7 - | (_, [] ) => get_vars vs) (*filter out nums as long as *)
4.8 + | (_, [] ) => get_vars vs) (*filter out nums as long as
4.9 + we have Free ("123",_)*)
4.10 | get_vars [] = [];
4.11 val ts = Term.add_frees (Syntax.read_term ctxt t) [] |> get_vars;
4.12 in fold Variable.declare_constraints ts ctxt end;
5.1 --- a/test/Tools/isac/Interpret/mstools.sml Tue Sep 13 10:51:56 2011 +0200
5.2 +++ b/test/Tools/isac/Interpret/mstools.sml Sun Sep 18 15:21:46 2011 +0200
5.3 @@ -47,6 +47,16 @@
5.4 if ((lhs t) |> type_of) = @{typ int} then ()
5.5 else error "mstools: incorrect type inference from parseNEW ctxt";
5.6
5.7 +val t_bit = Syntax.read_term ctxt "11::int";
5.8 +val t_free = numbers_to_string t_bit;
5.9 +val ctxt = ProofContext.init_global @{theory "Isac"};
5.10 +val SOME t = parseNEW ctxt "11";
5.11 +if (t |> type_of) = TFree ("'a", ["Int.number"]) then ()
5.12 +else error "parsed numeral correct";
5.13 +val ctxt' = Variable.declare_constraints t_free ctxt;
5.14 +val SOME t' = parseNEW ctxt' "11";
5.15 +if (t' |> type_of) = TFree ("'a", ["Int.number"]) then ()
5.16 +else error "Variable.declare_constraints did not recognize numeral";
5.17
5.18 "----------- fun get_assumptions, fun get_environments --";
5.19 "----------- fun get_assumptions, fun get_environments --";
6.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Tue Sep 13 10:51:56 2011 +0200
6.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Sun Sep 18 15:21:46 2011 +0200
6.3 @@ -25,8 +25,6 @@
6.4 "-----------------------------------------------------------------";
6.5 "-----------------------------------------------------------------";
6.6
6.7 -val c = []; print_depth 5;
6.8 -
6.9 "----------- tests on predicates in problems ---------------------";
6.10 "----------- tests on predicates in problems ---------------------";
6.11 "----------- tests on predicates in problems ---------------------";
6.12 @@ -112,35 +110,34 @@
6.13 "----------- lin.eq degree_0 -------------------------------------";
6.14 "----------- lin.eq degree_0 -------------------------------------";
6.15 "----- d0_false ------";
6.16 -(*=== inhibit exn WN110906 ======================================================
6.17 +(*=== inhibit exn WN110914: declare_constraints doesnt work with num_str ========
6.18 val fmz = ["equality (1 = (0::real))", "solveFor x", "solutions L"];
6.19 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
6.20 ["PolyEq","solve_d0_polyeq_equation"]);
6.21 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.22 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.23 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.24 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.25 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.26 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.27 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.30 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.31 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.33 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.34 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
6.35 | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
6.36
6.37 "----- d0_true ------";
6.38 -(*EP-7*)
6.39 val fmz = ["equality (0 = (0::real))", "solveFor x","solutions L"];
6.40 val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
6.41 ["PolyEq","solve_d0_polyeq_equation"]);
6.42 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.43 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.44 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.45 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.46 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.47 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.48 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.49 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.50 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.51 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.52 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.53 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.54 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.55 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
6.56 | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
6.57 -============ inhibit exn WN110906 ============================================*)
6.58 +============ inhibit exn WN110914 ============================================*)
6.59
6.60 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
6.61 "----------- test thm's d2_pq_formulsxx[_neg]---------------------";
6.62 @@ -230,47 +227,51 @@
6.63 term2str consts';
6.64 if consts = consts' (*WAS false*) then () else error "Check_elementwise changed";
6.65 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
6.66 +*}
6.67 +
6.68 +
6.69 +ML {*
6.70
6.71 "----- d2_pqformula1_neg ------";
6.72 -(*EP-8*)
6.73 -val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
6.74 +val fmz = ["equality (2 +(-1)*x + x^^^2 = (0::real))", "solveFor x","solutions L"];
6.75 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
6.76 -(*val p = e_pos'; val c = [];
6.77 -val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.78 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.79 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.80 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.81 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.82 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.83 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.84 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.85 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.86 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.87 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.88 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.89 +*}
6.90 +ML {*
6.91 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.92 (*### or2list False
6.93 ([1],Res) False Or_to_List)*)
6.94 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.95 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.96 (*### or2list False
6.97 ([2],Res) [] Check_elementwise "Assumptions"*)
6.98 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.99 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.100 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.101 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.102 val asm = get_assumptions_ pt p;
6.103 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
6.104 else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
6.105 +*}
6.106 +ML {*
6.107
6.108 "----- d2_pqformula2 ------";
6.109 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
6.110 val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
6.111 ["PolyEq","solve_d2_polyeq_pq_equation"]);
6.112 -(*val p = e_pos'; val c = [];
6.113 +(*val p = e_pos';
6.114 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.115 -val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.116 +val (p,_,f,nxt,_,pt) = me (mI,m) p [] EmptyPtree;*)
6.117 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.118 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.119 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.120 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.121 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.122 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.123 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.124 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.125 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.126 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.127 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.128 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.129 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.130 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.131 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.132 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.133 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.134 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
6.135 | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
6.136
6.137 @@ -283,13 +284,13 @@
6.138 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.139 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.140 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.141 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.142 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.143 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.144 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.145 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.146 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.147 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.148 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.149 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.150 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.151 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.152 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.153 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.154 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.155 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
6.156 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
6.157 "TODO 2 +(-1)*x + 1*x^^^2 = 0";
6.158 @@ -304,14 +305,14 @@
6.159 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.160 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.161 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.162 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.163 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.164 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.165 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.166 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.167 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.168 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.169 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.170 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.171 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.172 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.173 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.174 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.175 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.176 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.177 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.178 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
6.179 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
6.180
6.181 @@ -323,13 +324,13 @@
6.182 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.183 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.184 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.185 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.186 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.187 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.188 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.189 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.190 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.191 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.192 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.193 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.194 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.195 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.196 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.197 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.198 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.199 "TODO 2 + x + x^^^2 = 0";
6.200 "TODO 2 + x + x^^^2 = 0";
6.201 "TODO 2 + x + x^^^2 = 0";
6.202 @@ -343,14 +344,14 @@
6.203 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.204 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.205 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.206 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.207 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.208 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.209 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.210 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.211 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.212 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.213 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.214 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.215 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.216 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.217 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.218 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.219 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.220 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.221 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.222 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
6.223 | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
6.224
6.225 @@ -362,12 +363,12 @@
6.226 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.227 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.228 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.229 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.230 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.231 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.232 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.233 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.234 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.235 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.236 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.237 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.238 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.239 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.240 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.241 "TODO 2 + x + 1*x^^^2 = 0";
6.242 "TODO 2 + x + 1*x^^^2 = 0";
6.243 "TODO 2 + x + 1*x^^^2 = 0";
6.244 @@ -380,14 +381,14 @@
6.245 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.246 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.247 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.248 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.249 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.250 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.251 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.252 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.253 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.254 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.255 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.256 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.257 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.258 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.259 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.260 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.261 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.262 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.263 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.264 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
6.265 | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
6.266
6.267 @@ -399,14 +400,14 @@
6.268 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.269 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.270 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.271 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.272 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.273 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.274 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.275 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.276 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.277 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.278 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.279 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.280 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.281 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.282 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.283 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.284 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.285 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.286 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.287 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
6.288 | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
6.289
6.290 @@ -419,14 +420,14 @@
6.291 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
6.292 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.293 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.294 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.295 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.296 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.297 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.298 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.299 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.300 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.301 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.302 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.303 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.304 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.305 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.306 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.307 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.308 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.309 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.310 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
6.311 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
6.312
6.313 @@ -439,14 +440,14 @@
6.314 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.315
6.316 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.317 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.318 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.319 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.320 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.321 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.322 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.323 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.324 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.325 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.326 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.327 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.328 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.329 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.330 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.331 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.332 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.333 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
6.334 | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
6.335
6.336 @@ -459,13 +460,13 @@
6.337 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.338
6.339 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.340 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.341 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.342 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.343 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.344 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.345 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.346 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.347 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.348 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.349 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.350 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.351 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.352 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.353 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.354 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
6.355 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
6.356
6.357 @@ -479,13 +480,13 @@
6.358 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.359
6.360 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.361 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.362 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.363 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.364 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.365 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.366 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.367 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.368 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.369 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.370 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.371 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.372 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.373 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.374 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.375 "TODO 4 + x^^^2 = 0";
6.376 "TODO 4 + x^^^2 = 0";
6.377 "TODO 4 + x^^^2 = 0";
6.378 @@ -499,13 +500,13 @@
6.379 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.380
6.381 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.382 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.383 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.384 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.385 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.386 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.387 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.388 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.389 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.390 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.391 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.392 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.393 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.394 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.395 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.396 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
6.397 | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
6.398
6.399 @@ -518,12 +519,12 @@
6.400 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.401
6.402 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.403 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.404 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.405 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.406 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.407 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.408 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.409 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.410 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.411 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.412 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.413 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.414 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.415 "TODO 4 + 1*x^^^2 = 0";
6.416 "TODO 4 + 1*x^^^2 = 0";
6.417 "TODO 4 + 1*x^^^2 = 0";
6.418 @@ -540,13 +541,13 @@
6.419 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.420
6.421 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.422 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.423 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.424 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.425 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.426 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.427 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.428 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.429 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.430 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.431 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.432 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.433 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.434 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.435 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.436 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
6.437 | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
6.438
6.439 @@ -558,12 +559,12 @@
6.440 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.441
6.442 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.443 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.444 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.445 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.446 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.447 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.448 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.449 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.450 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.451 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.452 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.453 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.454 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.455 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
6.456 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
6.457 "TODO 1 +(-1)*x + 2*x^^^2 = 0";
6.458 @@ -577,13 +578,13 @@
6.459 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.460
6.461 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.462 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.463 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.464 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.465 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.466 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.467 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.468 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.469 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.470 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.471 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.472 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.473 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.474 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.475 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.476 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
6.477 | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
6.478
6.479 @@ -595,13 +596,13 @@
6.480 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.481
6.482 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.483 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.484 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.485 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.486 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.487 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.488 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.489 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.490 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.491 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.492 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.493 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.494 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.495 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.496 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.497 "TODO 1 + x + 2*x^^^2 = 0";
6.498 "TODO 1 + x + 2*x^^^2 = 0";
6.499 "TODO 1 + x + 2*x^^^2 = 0";
6.500 @@ -614,13 +615,13 @@
6.501 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.502
6.503 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.504 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.505 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.506 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.507 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.508 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.509 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.510 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.511 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.512 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.513 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.514 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.515 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.516 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.517 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.518 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
6.519 | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
6.520
6.521 @@ -632,13 +633,13 @@
6.522 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.523
6.524 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.525 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.526 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.527 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.528 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.529 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.530 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.531 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.532 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.533 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.534 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.535 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.536 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.537 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.538 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.539 "TODO 2 + 1*x + x^^^2 = 0";
6.540 "TODO 2 + 1*x + x^^^2 = 0";
6.541 "TODO 2 + 1*x + x^^^2 = 0";
6.542 @@ -652,13 +653,13 @@
6.543 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.544
6.545 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.546 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.547 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.548 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.549 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.550 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.551 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.552 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.553 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.554 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.555 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.556 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.557 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.558 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.559 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.560 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
6.561 | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
6.562
6.563 @@ -670,13 +671,13 @@
6.564 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.565
6.566 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.567 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.568 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.569 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.570 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.571 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.572 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.573 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.574 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.575 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.576 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.577 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.578 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.579 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.580 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.581 "TODO 2 + x + x^^^2 = 0";
6.582 "TODO 2 + x + x^^^2 = 0";
6.583 "TODO 2 + x + x^^^2 = 0";
6.584 @@ -690,13 +691,13 @@
6.585 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.586
6.587 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.588 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.589 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.590 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.591 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.592 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.593 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.594 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.595 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.596 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.597 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.598 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.599 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.600 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.601 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.602 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
6.603 | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
6.604
6.605 @@ -708,12 +709,12 @@
6.606 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.607
6.608 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.609 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.610 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.611 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.612 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.613 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.614 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.615 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.616 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.617 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.618 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.619 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.620 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.621 "TODO 8+ 2*x^^^2 = 0";
6.622 "TODO 8+ 2*x^^^2 = 0";
6.623 "TODO 8+ 2*x^^^2 = 0";
6.624 @@ -726,13 +727,13 @@
6.625 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.626
6.627 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.628 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.629 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.630 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.631 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.632 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.633 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.634 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.635 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.636 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.637 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.638 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.639 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.640 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.641 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.642 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
6.643 | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
6.644
6.645 @@ -744,12 +745,12 @@
6.646 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.647
6.648 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.649 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.650 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.651 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.652 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.653 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.654 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.655 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.656 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.657 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.658 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.659 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.660 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.661 "TODO 4+ x^^^2 = 0";
6.662 "TODO 4+ x^^^2 = 0";
6.663 "TODO 4+ x^^^2 = 0";
6.664 @@ -763,13 +764,13 @@
6.665 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.666
6.667 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.668 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.669 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.670 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.671 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.672 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.673 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.674 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.675 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.676 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.677 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.678 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.679 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.680 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.681 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.682 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
6.683 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
6.684
6.685 @@ -781,13 +782,13 @@
6.686 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.687
6.688 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.689 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.690 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.691 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.692 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.693 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.694 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.695 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.696 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.697 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.698 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.699 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.700 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.701 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.702 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.703 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
6.704 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
6.705
6.706 @@ -800,13 +801,13 @@
6.707 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.708
6.709 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.710 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.711 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.712 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.713 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.714 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.715 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.716 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.717 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.718 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.719 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.720 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.721 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.722 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.723 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.724 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
6.725 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
6.726
6.727 @@ -819,13 +820,13 @@
6.728 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.729
6.730 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.731 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.732 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.733 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.734 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.735 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.736 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.737 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.738 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.739 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.740 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.741 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.742 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.743 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.744 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.745 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
6.746 | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
6.747
6.748 @@ -842,37 +843,37 @@
6.749 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.750
6.751 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.752 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.753 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.754 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.755 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.756 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.757 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.758 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.759 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.760 (*Apply_Method ("PolyEq","complete_square")*)
6.761 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.762 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.763 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
6.764 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.765 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.766 (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
6.767 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.768 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.769 (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
6.770 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.771 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.772 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
6.773 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
6.774 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.775 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.776 (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
6.777 -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
6.778 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.779 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.780 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
6.781 -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
6.782 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.783 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.784 (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
6.785 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
6.786 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.787 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.788 (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
6.789 x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
6.790 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.791 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.792 (*"x = -2 | x = 4" nxt = Or_to_List*)
6.793 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.794 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.795 (*"[x = -2, x = 4]" nxt = Check_Postcond*)
6.796 - val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.797 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
6.798 (* FIXXXME
6.799 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
6.800 | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
6.801 @@ -901,15 +902,15 @@
6.802 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.803
6.804 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.805 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.806 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.807 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.808 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.809 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.810 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.811 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.812 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.813 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.814 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.815 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.816 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.817 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.818 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.819 (*Apply_Method ("PolyEq","complete_square")*)
6.820 - val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.821 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
6.822
6.823 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
6.824 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
6.825 @@ -924,24 +925,24 @@
6.826 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.827
6.828 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.829 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.830 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.831 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.832 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.833 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.834 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.835 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.836 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.837 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.838 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.839 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.840 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.841 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.842 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.843 (*Apply_Method ("PolyEq","complete_square")*)
6.844 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.845 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.846 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.847 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.848 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.849 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.850 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.851 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.852 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.853 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.854 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.855 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.856 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.857 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.858 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.859 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.860 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.861 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.862 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.863 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.864 (* FIXXXXME n1.,
6.865 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
6.866 | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
6.867 @@ -960,25 +961,25 @@
6.868 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.869
6.870 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.871 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.872 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.873 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.874 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.875 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.876 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.877 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.878 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.879 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.880 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.881 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.882 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.883 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.884 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.885 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.886 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.887 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.888 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.889 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.890 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.891
6.892 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.893 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.894 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.895 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.896 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.897 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.898 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.899 - val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.900 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.901 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.902 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.903 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.904 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.905 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.906 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.907 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
6.908 (*WN.2.5.03 TODO FIXME Matthias ?
6.909 case f of
6.910 Form'
6.911 @@ -1003,19 +1004,19 @@
6.912 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.913
6.914 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.915 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.916 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.917 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.918 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.919 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.920 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.921 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.922 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.923 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.924 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.925 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.926 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.927 - val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
6.928 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.929 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.930 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.931 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.932 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.933 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.934 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.935 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.936 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.937 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.938 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.939 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.940 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; f2str f;
6.941 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
6.942 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
6.943 | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
6.944 @@ -1034,14 +1035,14 @@
6.945 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
6.946
6.947 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
6.948 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.949 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.950 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.951 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.952 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.953 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.954 - val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.955 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
6.956 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.957 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.958 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.959 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.960 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.961 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.962 + val (p,_,f,nxt,_,pt) = me nxt p [] pt; val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.963 + val (p,_,f,nxt,_,pt) = me nxt p [] pt;
6.964 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
6.965 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
6.966 | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
7.1 --- a/test/Tools/isac/Test_Some.thy Tue Sep 13 10:51:56 2011 +0200
7.2 +++ b/test/Tools/isac/Test_Some.thy Sun Sep 18 15:21:46 2011 +0200
7.3 @@ -7,7 +7,24 @@
7.4
7.5 theory Test_Some imports Isac begin
7.6
7.7 -use"../../../test/Tools/isac/Frontend/interface.sml"
7.8 +use"../../../test/Tools/isac/Knowledge/polyeq.sml"
7.9 +
7.10 +ML {*
7.11 +(*GOON: polyeq first ML, test 1 above, and the all below piecewiese*)
7.12 +*}
7.13 +ML {*
7.14 +val t = @{term "(2::real)*r*2.14"};
7.15 +term2str t;
7.16 +*}
7.17 +ML {*
7.18 +
7.19 +*}
7.20 +ML {*
7.21 +
7.22 +*}
7.23 +ML {*
7.24 +
7.25 +*}
7.26
7.27 ML {*
7.28 val c = [];
7.29 @@ -16,6 +33,18 @@
7.30 ML {*
7.31
7.32 *}
7.33 +ML {*
7.34 +
7.35 +*}
7.36 +ML {*
7.37 +
7.38 +*}
7.39 +ML {*
7.40 +
7.41 +*}
7.42 +ML {*
7.43 +
7.44 +*}
7.45 ML{*
7.46 *}
7.47 ML{*