1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/isac/CTP-userinterfaces.tex Wed Dec 15 11:05:07 2010 +0100
1.3 @@ -0,0 +1,163 @@
1.4 +\documentclass{article}
1.5 +\usepackage{a4}
1.6 +\usepackage{times}
1.7 +\usepackage{latexsym}
1.8 +\bibliographystyle{alpha}
1.9 +\usepackage{graphicx}
1.10 +
1.11 +\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.12 +\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
1.13 +\def\Problem{ {\tt Problem }}
1.14 +
1.15 +\title{Upcoming Userinterfaces for Computer Theorem Provers.\\
1.16 + The case of Isabelle
1.17 +}
1.18 +
1.19 +\author{G. Schafhauser, A. Schulhofer, M. Steger\\
1.20 +Knowledge Management Institute (KMI)\\
1.21 +TU Graz}
1.22 +
1.23 +\begin{document}
1.24 +\maketitle
1.25 +\abstract{
1.26 +TODO}
1.27 +
1.28 +\section{Introduction}\label{intro} (WN)
1.29 + Computer theorem proving (CTP)\footnote{The term CTP is used to address two different things in this paper: (1) the academic discipline comprising respective theories as well as (2) the products developed within this discipline, the provers and the respective technology.},
1.30 +
1.31 +graphical user interfaces (GUI)
1.32 +
1.33 +%Georg
1.34 +\section{State of the art in CTP Interfaces}
1.35 +
1.36 +\subsection{A European technology: Coq and Isabelle}\label{ctp-techn}
1.37 + http://en.wikipedia.org/wiki/Coq\\
1.38 + http://coq.inria.fr/
1.39 +
1.40 + http://en.wikipedia.org/wiki/Isabelle\_(theorem\_prover)\\
1.41 + http://isabelle.in.tum.de/index.html
1.42 +
1.43 +why math -- functional: some of the languages have been specifically designed for constructing software for symbolic computation (SC).
1.44 +%+ required for \ref{ml-users}
1.45 +
1.46 +SC http://en.wikipedia.org/wiki/Symbolic\_computation
1.47 +% mainly does not compute numerical values, but terms containing variables like functions (symbols)
1.48 +
1.49 +The LCF project
1.50 +http://hopl.murdoch.edu.au/showlanguage.prx?exp=8177
1.51 +specifically designed a 'meta language' (ML)
1.52 +http://en.wikipedia.org/wiki/ML\_(programming\_language)
1.53 +\cite{pl:milner97}
1.54 +for developing CTP
1.55 +
1.56 +
1.57 +\subsection{Userinterfaces for CTP: Coq and Isabelle}\label{gui-coq-isa}
1.58 + CoqIDE, ..
1.59 + http://coq.inria.fr/what-is-coq?q=node/57\\
1.60 + earlier than Isabelle/jEdit
1.61 +
1.62 + ProofGeneral for Isabelle
1.63 + http://proofgeneral.inf.ed.ac.uk/\\
1.64 + emacs stone age ?
1.65 +
1.66 +\subsection{Upcoming requirements for userinterfaces in CTP}\label{gui-requir}
1.67 + @ interaction close to tty (Telegraph)\\
1.68 + BUT: separate parts in {\em one} proof could be processed in parallel
1.69 +
1.70 + @ http://www.informatik.uni-bremen.de/uitp/
1.71 +
1.72 + @ ... see\\
1.73 + http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\
1.74 + http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
1.75 +
1.76 +%Andreas
1.77 +\section{Isabelle's plans for new user-interfaces}\label{gui-plans}
1.78 + http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf,\\
1.79 + http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
1.80 +
1.81 +theorem proving will be integrated into software development
1.82 +
1.83 +hundreds of proof obligations are generated during a software verification process
1.84 +
1.85 +so the final goald of Isabelle's planning is integration with other software development tools in an integrated development environment (IDE).
1.86 +
1.87 +still many principal issues need to be clarified with respect to integration of CTP and other development tools. So engaging into details makes no sense at the present, and Isabelle will approach the final goal via experimental intermediate steps of integration.
1.88 +
1.89 +\subsection{Connect ML-world to the users' world via JVM}\label{ml-users}
1.90 +In Sect.\ref{ctp-techn} reasons have been given, why mathematics software at the state-of-the-art cannot be written in Java or the like. On the other side, Sect.\ref{gui-requir} stated requirements for mathematical user interfaces, which cannot be accomplished by ML-like languages. These requirements can be best accomplished by languages like Java, which have powerful libraries available for convenient assembly of GUIs.
1.91 +
1.92 +\paragraph{Example: a functional mathematics engine} as the experimental one in the \sisac-project is given by the following signature:
1.93 +{\it
1.94 +\begin{tabbing}
1.95 +\=xx\=xxxxxxxxxxxxxxxxxxxxxxxxx\=\kill
1.96 +\>signature INTERPRETER =\\
1.97 +\>sig\\
1.98 +\>\>type calcstate\\
1.99 +\>\>type step = formula * position * tactic\\
1.100 +\>\> \\
1.101 +\>\>val do\_next : program $\rightarrow$ calcstate $\rightarrow$ (calcstate * step)\\
1.102 +\>\>val apply\_tactic : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ tactic $\rightarrow$ (calcstate * step list)\\
1.103 +\>\>val apply\_formula : program $\rightarrow$ calcstate $\rightarrow$ position $\rightarrow$ formula $\rightarrow$ (calcstate * step list)\\
1.104 +%\\
1.105 +%\>\>val get\_next : program $\rightarrow$ calcstate $\rightarrow$ step\\
1.106 +%\>\>val get\_applicable\_tactics : program $\rightarrow$ calcstate $\rightarrow$ tactic list\\
1.107 +%\>\>val get\_intermediate : program $\rightarrow$ calcstate $\rightarrow$ position * position $\rightarrow$ step list\\
1.108 +\>end
1.109 +\end{tabbing}}
1.110 +The three essential functions are \textit{do\_next}, which reads a \textit{program} for determining the next \textit{step} in a calculation, the function \textit{apply\_tactic}, which applies a \textit{tactic} input by the user to the current \textit{position} in a calculation and thus may produce a list of \textit{step}s and the function \textit{apply\_formula}, which applies an input \textit{formula} accordingly.
1.111 +
1.112 +Now, the point with functional programming is, that the functions do {\em not} cause persistent updates in some memory, rather: all three functions above take the current state of the calculation, \textit{calcstate}, as an argument and after they have done they work return the updated \textit{calcstate}.
1.113 +
1.114 +There are several advantages of this kind of programming: more straight forward verification, which is not discussed here, and other features. For instance, given the three functions above, it is easy to undo steps of calculations, or go back to an earlier step of calculations: one just needs to store the \textit{calcstate}s (in a list), even without knowing the details of the \textit{calcstate}, which thus can be encapsulated for internal access only.
1.115 +
1.116 +\paragraph{Example: an object-oriented wrapper} as required for embedding the above mathematics engine into an object-oriented system. Such a wrapper looks like this:
1.117 +
1.118 +TODO
1.119 +
1.120 +\subsection{Scala as a mediator between ML and JVM}\label{scala-medi}
1.121 +{\em new} language --- what for, ideas ...
1.122 +
1.123 +\subsection{Support for parallel processing}\label{actors}
1.124 +actors copied from erlang
1.125 +
1.126 +% Marco
1.127 +\section{Planned contributions at TU Graz}
1.128 +
1.129 +\subsection{Make Isabelle process structured derivations}\label{struct-der}
1.130 +Structured Derivations (SD) is a format for calculational reasoning, which has been established by \cite{back-grundy-wright-98}. This is an example calculation:
1.131 +{\it\begin{tabbing}
1.132 +123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=123\=\kill
1.133 +\> $\bullet$\> \Problem [ maximum\_by, calculus ]\\
1.134 +\>\> $\vdash$\> $A = 2\cdot u\cdot v - u^2$\\
1.135 +\>\> $\bullet$\> \Problem [make, diffable, funtion]\\
1.136 +\>\> \dots\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\
1.137 +\>\> $\bullet$\> \Problem [on\_interval, for\_maximum, differentiate, function]\\
1.138 +\>\>\> $\vdash$\> $\overline{A}(\alpha) = 8\cdot r^2\cdot\sin\alpha\cdot\cos\alpha - 4\cdot r^2\cdot(\sin\alpha)^2$\\
1.139 +\>\>\> $\bullet$\> \Problem [differentiate, funtion]\\
1.140 +\>\>\> \dots\> $\overline{A}^\prime(\alpha) = 8\cdot r^2\cdot(-(\sin\alpha)^2+(\cos\alpha)^2 - 2\cdot\sin\alpha\cdot\cos\alpha)$\\
1.141 +\>\>\> $\bullet$\> \Problem [on\_interval, goniometric, equation]\\
1.142 +\>\>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\
1.143 +\>\> \dots\> $\alpha = \tan^{-1}(-1+\sqrt{2})$\\
1.144 +\>\> $\bullet$\> \Problem [tool, find\_values]\\
1.145 +\>\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ]\\
1.146 +\> \dots\> [ $u=0.23\cdot r, \:v=0.76\cdot r$ ] %TODO calculate !
1.147 +\end{tabbing}}
1.148 +The plan is to use the machinery provided Isabelle/Isar as a 'logical operating system' ~\cite{isar-impl} and adapt the machinery such that is accepts SC in parallel to the Isar proof language~\cite{wenzel:isar}.
1.149 +
1.150 +This plan involves the following details.
1.151 +
1.152 +\subsection{Add a plug-in to jEdit}\label{plugin}
1.153 + file structure, copied from example project ...
1.154 +
1.155 +\subsection{Details of NetBeans projects}\label{netbeans}
1.156 + Scala + Java: html project files
1.157 +
1.158 +\subsection{Use interfaces between Java and Scala}\label{java-scala}
1.159 + how are data exchanged between Scala and Java ...
1.160 +
1.161 +
1.162 +\section{Conclusion and future work}
1.163 +
1.164 +
1.165 +\bibliography{bib/math-eng,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math,bib/pl}
1.166 +\end{document}
1.167 \ No newline at end of file
2.1 --- a/test/Tools/isac/ADDTESTS/course/T1_Basics.thy Wed Nov 24 15:00:23 2010 +0100
2.2 +++ b/test/Tools/isac/ADDTESTS/course/T1_Basics.thy Wed Dec 15 11:05:07 2010 +0100
2.3 @@ -1,102 +1,98 @@
2.4 (*
2.5 -/usr/local/isabisac/bin/isabelle jedit -l Isac T1_Basics.thy &
2.6 +/usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy &
2.7 +####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.
2.8 +0 1 2 3 4 5 6 7 8
2.9 *)
2.10
2.11 theory T1_Basics imports Isac begin
2.12
2.13 chapter {* Basics on Linux, Isabelle and ISAC *}
2.14
2.15 -text {*This is an Isabelle/Isar theory, that means: in between the text there are parts which
2.16 - can be evaluated by the theorem prover Isabelle if installed properly.
2.17 +text {*This is an Isabelle/Isar theory, that means: in between the text there
2.18 + are parts which can be evaluated by the theorem prover Isabelle, if installed
2.19 + properly.
2.20
2.21 - The goal of the sequence beginning with this theory is to give a quick introduction to
2.22 - authoring the mathematics knowledge for the math assistant ISAC www.ist.tugraz.at/projects/isac.
2.23 + The goal of the course beginning with this theory is to give a quick
2.24 + introduction to authoring the mathematics knowledge for the math assistant
2.25 + ISAC www.ist.tugraz.at/projects/isac.
2.26
2.27 - The course is self-contained for mathematics teachers, and probably for interested students.
2.28 + The course is self-contained for mathematics teachers, and probably for
2.29 + interested students.
2.30 *}
2.31
2.32 section {* Linux *}
2.33 +text {* Isabelle is a computer theorem prover (CTP) under ongoing development.
2.34 + This development is done using Linux. However, now Isabelle supports cygwin
2.35 + and thus also can be run on Microsoft Windows.
2.36
2.37 -text {* Isabelle is a computer theorem prover (CTP) under ongoing development. This
2.38 - development is done using Linux. However, now Isabelle supports cygwin and thus also can
2.39 - be run on Microsoft Windows.
2.40 + ISAC uses Isabelle as 'logical operating system'. You get both, ISAC and
2.41 + Isabelle installed into cygwin on an USB-stick at the beginning of the course.
2.42
2.43 - ISAC uses Isabelle as 'logical operating system'. You get both, ISAC and Isabelle
2.44 - installed into cygwin on an USB-stick at the beginning of the course.
2.45 + Authoring mathematics knowledge for ISAC (for instance, extending) requires
2.46 + basics in handling Linux (cygwin is Linux-like). Please note that ISAC is an
2.47 + experimental system and as such usability in authoring has not yet been considered.
2.48
2.49 - Authoring mathematics knowledge for ISAC (for instance, extending) requires basics
2.50 - in handling Linux (cygwin is Linux-like). Please notethat ISAC is an experimental system
2.51 - and as such usability has not yet been considered.
2.52 -
2.53 - Having started cygwin you see a prompt '$' at the beginning of a line
2.54 - where you can input commands ('#' is the begin of a comment not interpreted by cygwin),
2.55 - for instance:
2.56 + Having started cygwin you see a prompt '$' at the beginning of a line where
2.57 + you can input commands ('#' is the begin of a comment not interpreted by
2.58 + cygwin), for instance:
2.59 \begin{itemize}
2.60 \item $ cd /usr/local/Isabelle # changes to directory of Isabelle
2.61 \item $ ls -l # lists all files and subdirectories
2.62 \item $ cd test/Tools/isac/ADDTESTS/course # go on to start the course
2.63 - \item $ /usr/local/isabisac/bin/isabelle jedit -l Isac T1_Basics.thy &
2.64 + \item $ /usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy &
2.65 \item $ # starts the first exercise
2.66 \end{itemize}
2.67
2.68 - The arguments required for starting the first exercise tell about the underlying technology:
2.69 + The arguments required for starting the first exercise tell about the
2.70 + underlying technology:
2.71 \begin{itemize}
2.72 \item $ \emph{jedit} is the editor to be used. jEdit www.jedit.org will be introduced to
2.73 - Isabelle users within the next few years (so we are front-of-the-wave ;-).
2.74 + Isabelle-users within the next few years (so we are front-of-the-wave ;-).
2.75 \item $ \emph{-l Isac} loads all functionality and knowledge of ISAC
2.76 \item $ \emph{T1_Basics.thy} is the file name of the first exercise
2.77 \item $ \emph{&} allows to use the same command line for further commands.
2.78 \end{itemize}
2.79
2.80 - Furhter useful Linus commands are:
2.81 - \begin{itemize}
2.82 - \item $ TODO #
2.83 - \end{itemize}
2.84 + Since paths are long, we abbreviate '/usr/local/Isabelle/' to '~~' below.
2.85 *}
2.86
2.87 section {* Isabelle terms *}
2.88 -
2.89 -text {* One basic kind of data required for mathematics are terms. ISAC uses Isabelle's terms.
2.90 - In order to allow for 'symbolic computation' terms require representation in an
2.91 - appropriate data structure, which is defined at [ISABELLE_HOME]/src/Pure/term.ML.
2.92 +text {* The most basic kind of data required for mathematics are terms.
2.93 + ISAC uses Isabelle's terms.
2.94 + In order to allow for 'symbolic computation' terms require representation in
2.95 + an appropriate data structure, which is defined at ~~/src/Pure/term.ML
2.96 + ().
2.97
2.98 Let us give an example:
2.99 *}
2.100 -
2.101 ML {* @{term "a + b * 9"}*}
2.102
2.103 -text {* In the 'Output' window below you see what the above command produces, the internal
2.104 - representation of "a + b * 3". The '...' indicate that some details are still hidden;
2.105 - further details are received this way:
2.106 +text {* In the 'Output' window below you see what the above command produces,
2.107 + the internal representation of "a + b * 3". The '...' indicate that some
2.108 + details are still hidden; further details are received this way:
2.109 *}
2.110 -
2.111 ML {* print_depth 99;
2.112 @{term "a + b * 9"}
2.113 *}
2.114 -
2.115 -text {* The internal representation is too comprehensive for several kinds of inspection.
2.116 - Thus ISAC provides additional features, as we see below. First let us store the term
2.117 - in a variable 't':
2.118 +text {* The internal representation is too comprehensive for several kinds of
2.119 + inspection. Thus ISAC provides additional features, as we see below. First
2.120 + let us store the term in a variable 't':
2.121 *}
2.122 -
2.123 ML {*
2.124 val t = @{term "a + b * 9"};
2.125 atomwy t;
2.126 *}
2.127 +text {* Please, observe that in this case (whenever 'writeln' is involved, even
2.128 + invisibly) the output of 'atomwy t' is placed on top of the 'Output' window.
2.129
2.130 -text {* Please, observe that in this case (whenever 'writeln' is involved, even invisibly)
2.131 - the output of 'atomwy t' is placed on top of the 'Output' window.
2.132 -
2.133 - Presently, ISAC uses a slightly different representation for terms (which soon will disappear),
2.134 - which does not encode numerals as binary numbers:
2.135 + Presently, ISAC uses a slightly different representation for terms (which soon
2.136 + will disappear), which does not encode numerals as binary numbers:
2.137 *}
2.138 -
2.139 ML {* val SOME t = parse (theory "Isac") "a + b * 3";
2.140 atomwy (term_of t);
2.141 *}
2.142 -
2.143 -text {* From the above we see: the internal representation of a term contains all the
2.144 - knowledge it is built from, see
2.145 +text {* From the above we see: the internal representation of a term contains
2.146 + all the knowledge it is built from, see
2.147 http://isabelle.in.tum.de/dist/library/HOL/Groups.html for the definitions
2.148 \begin{itemize}
2.149 \item plus :: "'a => 'a => 'a" (infixl "+" 65)
2.150 @@ -104,25 +100,22 @@
2.151 \end{itemize}
2.152 together with relevant theorems about + and *.
2.153
2.154 - In the near future you will just click in order to get the requested knowledge. (The
2.155 - present experimental state of Isabelle/jEdit already shows the signature of the function
2.156 - under the cursor, if kept on place for a second.)
2.157 + In the near future you will just click in order to get the requested knowledge.
2.158 + (The present experimental state of Isabelle/jEdit already shows the signature
2.159 + of the function under the cursor, if kept on place for a second.)
2.160 *}
2.161
2.162 section {* Isabelle theories *}
2.163 -
2.164 -text {* As just mentioned, (almost) all the math knowledge used in a theorem prover is
2.165 - explicitly defined (and not built into the code like in a CAS). The knowledge is
2.166 - organised in \emph{theories}.
2.167 +text {* As just mentioned, (almost) all the math knowledge used in a theorem
2.168 + prover is explicitly defined (and not built into the code like in a CAS). The
2.169 + knowledge is organised in \emph{theories}.
2.170
2.171 Without these theories Isabelle cannot do any thing, it even does not understand '+' or '*'.
2.172 For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is
2.173 defined ('=' etc), but not yet '+' and '*', so you get 'NONE':
2.174 *}
2.175 -
2.176 ML {* parse (theory "HOL") "a + b * 3";
2.177 *}
2.178 -
2.179 text {* ISAC uses comparatively few definitions and theorems from Isabelle, see
2.180 \begin{itemize}
2.181 \item http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html
2.182 @@ -144,5 +137,4 @@
2.183
2.184 This coures intends to provide basic knowledge for authoring new examples in ISAC.
2.185 *}
2.186 -
2.187 end
3.1 --- a/test/Tools/isac/ADDTESTS/course/T2_Rewriting.thy Wed Nov 24 15:00:23 2010 +0100
3.2 +++ b/test/Tools/isac/ADDTESTS/course/T2_Rewriting.thy Wed Dec 15 11:05:07 2010 +0100
3.3 @@ -1,62 +1,233 @@
3.4 (*
3.5 -/usr/local/isabisac/bin/isabelle jedit -l Isac T2_Rewriting.thy &
3.6 +cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/course/
3.7 +/usr/local/Isabelle/bin/isabelle jedit -l Isac T2_Rewriting.thy &
3.8 *)
3.9
3.10 theory T2_Rewriting imports Isac begin
3.11
3.12 section {* Rewriting *}
3.13
3.14 -text {* \emph{Rewriting} is a technique of Symbolic Computation, which is appropriate
3.15 - to make a 'transparent system', because it is intuitively comprehensible. For a thourogh
3.16 - introduction see the book of Tobias Nipkow,
3.17 +text {* \emph{Rewriting} is a technique of Symbolic Computation, which is
3.18 + appropriate to make a 'transparent system', because it is intuitively
3.19 + comprehensible. For a thourogh introduction see the book of Tobias Nipkow,
3.20 http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/
3.21
3.22 -section {* Introduction to rewriting *}
3.23 +subsection {* Introduction to rewriting *}
3.24
3.25 text {* Rewriting creates calculations which look like written by hand; see the
3.26 ISAC tutoring system ! ISAC finds the rules automatically. Here we start by
3.27 + telling the rules ourselves.
3.28 + Let's differentiate after we have identified the rules for differentiation, as
3.29 + found in ~~/src/Tools/isac/Knowledge/Diff.thy:
3.30 +*}
3.31 +ML {*
3.32 +val diff_sum = num_str @{thm diff_sum};
3.33 +val diff_pow = num_str @{thm diff_pow};
3.34 +val diff_var = num_str @{thm diff_var};
3.35 +val diff_const = num_str @{thm diff_const};
3.36 +*}
3.37 +text {* Looking at the rules (abbreviated by 'thm' above), we see the
3.38 + differential operator abbreviated by 'd_d ?bdv', where '?bdv' is the bound
3.39 + variable.
3.40 + Can you read diff_const in the Ouput window ?
3.41
3.42 -Just to show, how simple rewriting is
3.43 + Please, skip this introductory ML-section in the first go ...*}
3.44 +ML {*
3.45 +print_depth 1;
3.46 +val (thy, ro, er, inst) =
3.47 + (theory "Isac", tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
3.48 +*}
3.49 +text {* ... and let us differentiate the term t: *}
3.50 +ML {*
3.51 +val t = (term_of o the o (parse thy)) "d_d x (x^^^2 + x + y)";
3.52
3.53 -=======================================================================================
3.54 -???????????????????? star with diff --- this allows trial and error from the beginning,
3.55 -!!!!!!!!!!!!!!!!!!!! if all the thems are given: here +?+ .thy (code or html?)
3.56 -=======================================================================================
3.57 +val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
3.58 +val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_sum t; term2str t;
3.59 +val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_pow t; term2str t;
3.60 +val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_var t; term2str t;
3.61 +val SOME (t, _) = rewrite_inst_ thy ro er true inst diff_const t; term2str t;
3.62 +*}
3.63 +text {* Please, scoll up the Output-window to check the 5 steps of rewriting !
3.64 + You might not be satisfied by the result "2 * x ^^^ (2 - 1) + 1 + 0".
3.65
3.66 -The following
3.67 -
3.68 -Please, skip the following ML-section in the first go ...*}
3.69 -
3.70 -ML {*
3.71 -print_depth 5;
3.72 -val (thy, ro, er, inst) = (theory "Isac", tless_true, eval_rls, [("bdv", "x::real")]);
3.73 + ISAC has a set of rules called 'make_polynomial', which simplifies the result:
3.74 +*}
3.75 +ML {*
3.76 +val SOME (t, _) = rewrite_set_ thy true make_polynomial t; term2str t;
3.77 +trace_rewrite := false;
3.78 *}
3.79
3.80 +subsection {* Note on bound variables *}
3.81 +text {* You may have noticed that rewrite_ above could distinguish between x
3.82 + (d_d x x = 1) and y (d_d x y = 0). ISAC does this by instantiating theorems
3.83 + before application: given [(@{term "bdv::real"}, @{term "x::real"})] the
3.84 + theorem diff_sum becomes "d_d x (?u + ?v) = d_d x ?u + d_d x ?v".
3.85 +
3.86 + Isabelle does this differently by variables bound by a 'lambda' %, see
3.87 + http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate_Analysis/Derivative.html
3.88 +*}
3.89 ML {*
3.90 -val t = (term_of o the o (parse thy)) "2 * a + 3 * (a - b)";
3.91 +val t = @{term "%x. x^2 + x + y"}; atomwy t; term2str t;
3.92 +*}
3.93 +text {* Since this notation does not conform to present high-school matheatics
3.94 + ISAC introduced the 'bdv' mechanism. This mechanism is also used for equation
3.95 + solving in ISAC.
3.96 *}
3.97
3.98 -ML {*
3.99 -val SOME (t, _) = rewrite_ thy ro er true (@{thm "klammer_mult_minus"}) t; term2str t;
3.100 -val SOME (t, _) = rewrite_ thy ro er true (@{thm "klammer_plus_minus"}) t; term2str t;
3.101 -val SOME (t, _) = rewrite_ thy ro er true (@{thm "real_num_collect"}) t; term2str t;
3.102 +subsection {* Conditional and ordered rewriting *}
3.103 +text {* We have already seen conditional rewriting above when we used the rule
3.104 + diff_const; let us try: *}
3.105 +ML {*
3.106 +val t1 = (term_of o the o (parse thy)) "d_d x (a*BC*x*z)";
3.107 +rewrite_inst_ thy ro er true inst diff_const t1;
3.108 +
3.109 +val t2 = (term_of o the o (parse thy)) "d_d x (a*BC*y*z)";
3.110 +rewrite_inst_ thy ro er true inst diff_const t2;
3.111 +*}
3.112 +text {* For term t1 the assumption 'not (x occurs_in "a*BC*x*z")' is false,
3.113 + since x occurs in t1 actually; thus the rule following implication '==>' is
3.114 + not applied and rewrite_inst_ returns NONE.
3.115 + For term t2 is 'not (x occurs_in "a*BC*y*z")' true, thus the rule is applied.
3.116 *}
3.117
3.118 +subsubsection {* ordered rewriting *}
3.119 +text {* Let us start with an example; in order to see what is going on we tell
3.120 + Isabelle to show all brackets:
3.121 +*}
3.122 ML {*
3.123 -("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"));
3.124 -get_calculation_ thy ;
3.125 -calculate_ thy ;
3.126 +show_brackets := true;
3.127 +val t0 = (term_of o the o (parse thy)) "2*a + 3*b + 4*a"; term2str t0;
3.128 +(*show_brackets := false;*)
3.129 +*}
3.130 +text {* Now we want to bring 4*a close to 2*a in order to get 6*a:
3.131 +*}
3.132 +ML {*
3.133 +val SOME (t, _) = rewrite_ thy ro er true @{thm add_assoc} t0; term2str t;
3.134 +val SOME (t, _) = rewrite_ thy ro er true @{thm add_left_commute} t; term2str t;
3.135 +val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t;
3.136 +val SOME (t, _) = rewrite_ thy ro er true @{thm real_num_collect} t; term2str t;
3.137 +*}
3.138 +text {* That is fine, we just need to add 2+4 !!!!! See the next section below.
3.139 +
3.140 + But we cannot automate such ordering with what we know so far: If we put
3.141 + add_assoc, add_left_commute and add_commute into one ruleset (your have used
3.142 + ruleset 'make_polynomial' already), then all the rules are applied as long
3.143 + as one rule is applicable (that is the way such rulesets work).
3.144 + Try to step through the ML-sections without skipping one of them ...
3.145 +*}
3.146 +ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
3.147 +ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
3.148 +ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
3.149 +ML {*val SOME (t, _) = rewrite_ thy ro er true @{thm add_commute} t; term2str t*}
3.150 +text {* ... you can go forever, the ruleset is 'not terminating'.
3.151 + The theory of rewriting makes this kind of rulesets terminate by the use of
3.152 + 'rewrite orders':
3.153 + Given two terms t1 and t2 we describe rewriting by: t1 ~~> t2. Then
3.154 + 'ordered rewriting' is: t2 < t1 ==> t1 ~~> t2. That means, a rule is only
3.155 + applied, when the result t2 is 'smaller', '<', than the one to be rewritten.
3.156 + Defining such a '<' is not trivial, see ~~/src/Tools/isacKnowledge/Poly.thy
3.157 + for 'fun has_degree_in' etc.
3.158 *}
3.159
3.160 -ML {*
3.161 -111
3.162 +subsection {* Simplification in ISAC *}
3.163 +text {*
3.164 + With the introduction into rewriting, ordered rewriting and conditional
3.165 + rewriting we have seen all what is necessary for the practice of rewriting.
3.166 +
3.167 + One basic technique of 'symbolic computation' which uses rewriting is
3.168 + simplification, that means: transform terms into an equivalent form which is
3.169 + as simple as possible.
3.170 + Isabelle has powerful and efficient simplifiers. Nevertheless, ISAC has another
3.171 + kind of simplifiers, which groups rulesets such that the trace of rewrites is
3.172 + more readable in ISAC's worksheets.
3.173 +
3.174 + Here are examples of of how ISAC's simplifier work:
3.175 +*}
3.176 +ML {*
3.177 +show_brackets := false;
3.178 +val t1 = (term_of o the o (parse thy)) "(a - b) * (a^^^2 + a*b + b^^^2)";
3.179 +val SOME (t, _) = rewrite_set_ thy true make_polynomial t1; term2str t;
3.180 +*}
3.181 +ML {*
3.182 +val t2 = (term_of o the o (parse thy))
3.183 + "(2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^^^ 2 - 9))";
3.184 +val SOME (t, _) = rewrite_set_ thy true norm_Rational t2; term2str t;
3.185 +*}
3.186 +text {* The simplifiers are quite busy when finding the above results. you can
3.187 + watch them at work by setting the switch 'trace_rewrite:*}
3.188 +ML {*
3.189 +trace_rewrite := true;
3.190 +tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
3.191 +val SOME (t, _) = rewrite_set_ thy true norm_Rational t2; term2str t;
3.192 +tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
3.193 +trace_rewrite := false;
3.194 +*}
3.195 +text {* You see what happend when you click the checkbox <Tracing> on the bar
3.196 + separating this window from the Output-window.
3.197 +
3.198 + So, it might be better to take simpler examples for watching the simplifiers.
3.199 *}
3.200
3.201 -text {* ... and let's start with an example:
3.202 +
3.203 +section {* Experiments with a simplifier conserving minus *}
3.204 +
3.205 +text {* We conclude the section on rewriting with starting into an experimental
3.206 + development. This development has been urged by teachers using ISAC for
3.207 + introduction to algebra with students at the age of 12-14.
3.208 +
3.209 + The teachers requested ISAC to keep the minus, for instance in the above
3.210 + result "a^3 + -1 * b^3" (here ISAC should write "a^3 - * b^3") and also
3.211 + in all intermediate steps.
3.212 +
3.213 + So we started to develop (in German !) such a simplifier in
3.214 + ~~/src/Tools/isac/Knowledge/PolyMinus.thy
3.215 *}
3.216
3.217 -ML {* val t = parse (theory "PolyMinus") "2 * a + 3 * a + 4 * b";
3.218 +subsection {* What already works *}
3.219 +ML {*
3.220 +val t2 = (term_of o the o (parse thy))
3.221 + "- r - 2 * s - 3 * t + 5 + 4 * r + 8 * s - 5 * t - 2";
3.222 +val SOME (t, _) = rewrite_set_ thy true rls_p_33 t2; term2str t;
3.223 +*}
3.224 +text {* Try your own examples ! *}
3.225
3.226 +subsection {* This raises questions about didactics *}
3.227 +text {* Oberserve the '-' ! That works out. But see the efforts in PolyMinus.thy
3.228 +*}
3.229 +ML {*
3.230 +@{thm subtrahiere};
3.231 +@{thm subtrahiere_von_1};
3.232 +@{thm subtrahiere_1};
3.233 +*}
3.234 +text {* That would not be so bad. But it is only a little part of what else is
3.235 + required:
3.236 +*}
3.237 +ML {*
3.238 +@{thm subtrahiere_x_plus_minus};
3.239 +@{thm subtrahiere_x_plus1_minus};
3.240 +@{thm subtrahiere_x_plus_minus1};
3.241 +@{thm subtrahiere_x_minus_plus};
3.242 +@{thm subtrahiere_x_minus1_plus};
3.243 +@{thm subtrahiere_x_minus_plus1};
3.244 +@{thm subtrahiere_x_minus_minus};
3.245 +@{thm subtrahiere_x_minus1_minus};
3.246 +@{thm subtrahiere_x_minus_minus1};
3.247 +*}
3.248 +text {* So, learning so many rules, and learning to apply these rules, is futile.
3.249 + Actually, most of our students are unable to apply theorems.
3.250 +
3.251 + But if you look at 'make_polynomial' or even 'norm_Rational' you see,
3.252 + that these general simplifiers require about 10% than rulesets for '-'.
3.253 +
3.254 + So, we might have better chances to teach our student to apply theorems
3.255 + without '-' ?
3.256 +*}
3.257 +
3.258 +subsection {* This does not yet work *}
3.259 +ML {*
3.260 +val t = (term_of o the o (parse thy))
3.261 + "(2*a - 5*b) * (2*a + 5*b)";
3.262 +rewrite_set_ thy true rls_p_33 t; term2str t;
3.263 *}
3.264
3.265 end