neuper@38067: (* neuper@38077: /usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy & neuper@38077: ####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.####. neuper@38077: 0 1 2 3 4 5 6 7 8 neuper@38067: *) neuper@38067: wneuper@59592: theory T1_Basics imports Isac.Isac_Knowledge wneuper@59460: begin neuper@38067: wneuper@59472: chapter \Basics on Linux, Isabelle and ISAC\ neuper@38067: wneuper@59472: text \This is an Isabelle/Isar theory, that means: in between the text there neuper@38077: are parts which can be evaluated by the theorem prover Isabelle, if installed neuper@38077: properly. neuper@38067: neuper@38077: The goal of the course beginning with this theory is to give a quick neuper@38077: introduction to authoring the mathematics knowledge for the math assistant neuper@38077: ISAC www.ist.tugraz.at/projects/isac. neuper@38067: neuper@38077: The course is self-contained for mathematics teachers, and probably for neuper@38077: interested students. wneuper@59472: \ neuper@38067: wneuper@59472: section \Linux\ wneuper@59472: text \Isabelle is a computer theorem prover (CTP) under ongoing development. neuper@38077: This development is done using Linux. However, now Isabelle supports cygwin neuper@38077: and thus also can be run on Microsoft Windows. neuper@38067: neuper@38077: ISAC uses Isabelle as 'logical operating system'. You get both, ISAC and neuper@38077: Isabelle installed into cygwin on an USB-stick at the beginning of the course. neuper@38067: neuper@38077: Authoring mathematics knowledge for ISAC (for instance, extending) requires neuper@38077: basics in handling Linux (cygwin is Linux-like). Please note that ISAC is an neuper@38077: experimental system and as such usability in authoring has not yet been considered. neuper@38067: neuper@38077: Having started cygwin you see a prompt '$' at the beginning of a line where neuper@38077: you can input commands ('#' is the begin of a comment not interpreted by neuper@38077: cygwin), for instance: neuper@38067: \begin{itemize} neuper@38067: \item $ cd /usr/local/Isabelle # changes to directory of Isabelle neuper@38067: \item $ ls -l # lists all files and subdirectories neuper@38067: \item $ cd test/Tools/isac/ADDTESTS/course # go on to start the course neuper@38077: \item $ /usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy & neuper@38067: \item $ # starts the first exercise neuper@38067: \end{itemize} neuper@38067: neuper@38077: The arguments required for starting the first exercise tell about the neuper@38077: underlying technology: neuper@38067: \begin{itemize} neuper@38067: \item $ \emph{jedit} is the editor to be used. jEdit www.jedit.org will be introduced to neuper@38077: Isabelle-users within the next few years (so we are front-of-the-wave ;-). neuper@38067: \item $ \emph{-l Isac} loads all functionality and knowledge of ISAC neuper@38067: \item $ \emph{T1_Basics.thy} is the file name of the first exercise neuper@38067: \item $ \emph{&} allows to use the same command line for further commands. neuper@38067: \end{itemize} neuper@38067: neuper@38077: Since paths are long, we abbreviate '/usr/local/Isabelle/' to '~~' below. wneuper@59472: \ neuper@38067: wneuper@59472: section \Isabelle terms\ wneuper@59472: text \The most basic kind of data required for mathematics are terms. neuper@38077: ISAC uses Isabelle's terms. neuper@38077: In order to allow for 'symbolic computation' terms require representation in neuper@38077: an appropriate data structure, which is defined at ~~/src/Pure/term.ML neuper@38077: (). neuper@38067: neuper@38067: Let us give an example: wneuper@59472: \ wneuper@59472: ML \@{term "a + b * 9"}\ neuper@38067: wneuper@59472: text \In the 'Output' window below you see what the above command produces, neuper@38077: the internal representation of "a + b * 3". The '...' indicate that some neuper@38077: details are still hidden; further details are received this way: wneuper@59472: \ wneuper@59472: ML \(*default_print_depth 99;*) @{term "a + b * 9"}; (*default_print_depth 5;*) wneuper@59472: \ wneuper@59472: text \The internal representation is too comprehensive for several kinds of neuper@38077: inspection. Thus ISAC provides additional features, as we see below. First neuper@38077: let us store the term in a variable 't': wneuper@59472: \ wneuper@59472: ML \ neuper@38067: val t = @{term "a + b * 9"}; Walther@60650: TermC.atom_write_detail @{context} t; wneuper@59472: \ wneuper@59472: text \Please, observe that in this case (whenever 'writeln' is involved, even neuper@38077: invisibly) the output of 'atomwy t' is placed on top of the 'Output' window. neuper@38067: neuper@38077: Presently, ISAC uses a slightly different representation for terms (which soon neuper@38077: will disappear), which does not encode numerals as binary numbers: wneuper@59472: \ Walther@60424: ML \ Walther@60424: val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3"; wneuper@59472: \ wneuper@59472: text \From the above we see: the internal representation of a term contains neuper@38077: all the knowledge it is built from, see neuper@38067: http://isabelle.in.tum.de/dist/library/HOL/Groups.html for the definitions neuper@38067: \begin{itemize} neuper@38067: \item plus :: "'a => 'a => 'a" (infixl "+" 65) neuper@38067: \item times :: "'a => 'a => 'a" (infixl "*" 70) neuper@38067: \end{itemize} neuper@38067: together with relevant theorems about + and *. neuper@38067: neuper@38077: In the near future you will just click in order to get the requested knowledge. neuper@38077: (The present experimental state of Isabelle/jEdit already shows the signature neuper@38077: of the function under the cursor, if kept on place for a second.) wneuper@59472: \ neuper@38067: wneuper@59472: section \Isabelle theories\ wneuper@59472: text \As just mentioned, (almost) all the math knowledge used in a theorem neuper@38077: prover is explicitly defined (and not built into the code like in a CAS). The neuper@38077: knowledge is organised in \emph{theories}. neuper@38067: neuper@38067: Without these theories Isabelle cannot do any thing, it even does not understand '+' or '*'. neuper@38067: For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is neuper@38067: defined ('=' etc), but not yet '+' and '*', so you get 'NONE': wneuper@59472: \ Walther@60424: ML \ Walther@60424: val t = TermC.parseNEW' (ThyC.id_to_ctxt "Isac_Knowledge") "a + b * 3"; wneuper@59472: \ wneuper@59472: text \ISAC uses comparatively few definitions and theorems from Isabelle, see neuper@38067: \begin{itemize} neuper@38067: \item http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html neuper@38067: \end{itemize} neuper@38067: We call this the dimension of 'deductive knowledge'. neuper@38067: neuper@38067: \bigskip However, ISAC provides two additional dimensions of knowledge, 'application neuper@38067: oriented knowledge' (simply called \emph{problems}) and 'algorithmic knowledge' neuper@38067: (simply called \emph{methods}); See neuper@38067: \begin{itemize} neuper@38067: \item problems http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html neuper@38067: \item methods http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html neuper@38067: \end{itemize} neuper@38067: neuper@38067: \bigskip The three dimensions of knowledge together provide all what a neuper@38067: \emph{mechanized math assistant} like ISAC requires for autonomously solving problems. neuper@38067: So, in ISAC too, is (almost) nothing built into the program code, rather, all neuper@38067: is up to authoring. neuper@38067: neuper@38067: This coures intends to provide basic knowledge for authoring new examples in ISAC. wneuper@59472: \ neuper@38067: end