(*

 /usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy &

 ####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.####.

 0         1         2         3         4         5         6         7         8

 *)

 theory T1_Basics imports Isac begin

 chapter {* Basics on Linux, Isabelle and ISAC *}

 text {*This is an Isabelle/Isar theory, that means: in between the text there 

   are parts which can be evaluated by the theorem prover Isabelle, if installed 

   properly.

   The goal of the course beginning with this theory is to give a quick 

   introduction to authoring the mathematics knowledge for the math assistant 

   ISAC www.ist.tugraz.at/projects/isac.

   The course is self-contained for mathematics teachers, and probably for 

   interested students.

 *}

 section {* Linux *}

 text {* Isabelle is a computer theorem prover (CTP) under ongoing development. 

   This development is done using Linux. However, now Isabelle supports cygwin 

   and thus also can be run on Microsoft Windows.

   ISAC uses Isabelle as 'logical operating system'. You get both, ISAC and 

   Isabelle installed into cygwin on an USB-stick at the beginning of the course.

   Authoring mathematics knowledge for ISAC (for instance, extending) requires 

   basics in handling Linux (cygwin is Linux-like). Please note that ISAC is an 

   experimental system and as such usability in authoring has not yet been considered.

   Having started cygwin you see a prompt '$' at the beginning of a line where 

   you can input commands ('#' is the begin of a comment not interpreted by 

   cygwin), for instance:

   \begin{itemize}

   \item $ cd /usr/local/Isabelle             # changes to directory of Isabelle

   \item $ ls -l                              # lists all files and subdirectories

   \item $ cd test/Tools/isac/ADDTESTS/course # go on to start the course

   \item $ /usr/local/Isabelle/bin/isabelle jedit -l Isac T1_Basics.thy &

   \item $                                    # starts the first exercise

   \end{itemize}

   The arguments required for starting the first exercise tell about the 

   underlying technology:

   \begin{itemize}

   \item $ \emph{jedit} is the editor to be used. jEdit www.jedit.org will be introduced to 

           Isabelle-users within the next few years (so we are front-of-the-wave ;-).

   \item $ \emph{-l Isac} loads all functionality and knowledge of ISAC

   \item $ \emph{T1_Basics.thy} is the file name of the first exercise

   \item $ \emph{&} allows to use the same command line for further commands.

   \end{itemize}

   Since paths are long, we abbreviate '/usr/local/Isabelle/' to '~~' below.

 *}

 section {* Isabelle terms *}

 text {* The most basic kind of data required for mathematics are terms. 

   ISAC uses Isabelle's terms.

   In order to allow for 'symbolic computation' terms require representation in 

   an  appropriate data structure, which is defined at ~~/src/Pure/term.ML

   ().

   Let us give an example:

 *}

 ML {* @{term "a + b * 9"}*}

 text {* In the 'Output' window below you see what the above command produces, 

   the internal representation of "a + b * 3". The '...' indicate that some 

   details are still hidden; further details are received this way:

 *}

 ML {* print_depth 99; @{term "a + b * 9"}; print_depth 5;

 *}

 text {* The internal representation is too comprehensive for several kinds of 

   inspection. Thus ISAC provides additional features, as we see below. First 

   let us store the term in a variable 't':

 *}

 ML {* 

   val t = @{term "a + b * 9"};

   atomwy t;

 *}

 text {* Please, observe that in this case (whenever 'writeln' is involved, even 

   invisibly) the output of 'atomwy t' is placed on top of the 'Output' window.

   Presently, ISAC uses a slightly different representation for terms (which soon

   will disappear), which does not encode numerals as binary numbers:

 *}

 ML {* val SOME t = parse @{theory "Isac"} "a + b * 3";

   atomwy (term_of t);

 *}

 text {* From the above we see: the internal representation of a term contains 

   all the knowledge it is built from, see

   http://isabelle.in.tum.de/dist/library/HOL/Groups.html for the definitions

   \begin{itemize}

   \item plus  :: "'a => 'a => 'a"  (infixl "+" 65)

   \item times :: "'a => 'a => 'a"  (infixl "*" 70)

   \end{itemize}

   together with relevant theorems about + and *.

   In the near future you will just click in order to get the requested knowledge.

   (The present experimental state of Isabelle/jEdit already shows the signature 

   of the function under the cursor, if kept on place for a second.)

 *}

 section {* Isabelle theories *}

 text {* As just mentioned, (almost) all the math knowledge used in a theorem 

   prover is explicitly defined (and not built into the code like in a CAS). The 

   knowledge is organised in \emph{theories}.

   Without these theories Isabelle cannot do any thing, it even does not understand '+' or '*'.

   For instance, in the theory 'HOL' (short for high order logic) even more basic knowledge is 

   defined ('=' etc), but not yet '+' and '*', so you get 'NONE':

 *}

 ML {*  parse @{theory "HOL"} "a + b * 3";

 *}

 text {* ISAC uses comparatively few definitions and theorems from Isabelle, see 

   \begin{itemize}

   \item http://www.ist.tugraz.at/projects/isac/www/kbase/thy/index_thy.html

   \end{itemize}

   We call this the dimension of 'deductive knowledge'.

   \bigskip However, ISAC provides two additional dimensions of knowledge, 'application

   oriented knowledge' (simply called \emph{problems}) and 'algorithmic knowledge' 

   (simply called \emph{methods}); See

   \begin{itemize}

   \item problems http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html

   \item methods http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html

   \end{itemize}

   \bigskip The three dimensions of knowledge together provide all what a 

   \emph{mechanized math assistant} like ISAC requires for autonomously solving problems.

   So, in ISAC too, is (almost) nothing built into the program code, rather, all

   is up to authoring.

   This coures intends to provide basic knowledge for authoring new examples in ISAC.

 *}

 end